DONT KNOW Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { 1 -> s_(0), 2 -> s_(s_(0)), 3 -> s_(s_(s_(0))), 4 -> s_(s_(s_(s_(0)))), 5 -> s_(s_(s_(s_(s_(0))))), 6 -> s_(s_(s_(s_(s_(s_(0)))))), 7 -> s_(s_(s_(s_(s_(s_(s_(0))))))), U11(tt,M',N') -> U12(equal(_gt_(N',M'),true),M',N'), U12(tt,M',N') -> gcd(d(M',N'),M'), U21(tt,M',N) -> U22(equal(_gt_(M',N),true)), U22(tt) -> 0, U31(tt,M',N) -> U32(equal(_gt_(N,M'),true),M',N), U32(tt,M',N) -> s_(quot(d(M',N),M')), *(0,N) -> 0, *(s_(M),s_(N)) -> s_(+(+(*(M,N),M),N)), +(0,N) -> N, +(s_(M),s_(N)) -> s_(s_(+(M,N))), _lt_(N,M) -> _gt_(M,N), _gt_(0,M) -> false, _gt_(N',0) -> true, _gt_(s_(N),s_(M)) -> _gt_(N,M), and(tt,X) -> X, d(0,N) -> N, d(s_(M),s_(N)) -> d(M,N), equal(X,X) -> tt, gcd(0,N) -> 0, gcd(M',N') -> U11(tt,M',N'), gcd(N',N') -> N', p_(s_(N)) -> N, quot(M',M') -> s_(0), quot(N,M') -> U21(tt,M',N), quot(N,M') -> U31(tt,M',N) } (32 rules) Termination now uses minimal decomposition - : unit = () Entering the termination expert for modules. Verbose level = 0 Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { p_(s_(V_3)) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { and(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: {} The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { _gt_(s_(V_3),s_(V_1)) -> _gt_(V_3,V_1), _gt_(V_2,0) -> true, _gt_(0,V_1) -> false } (3 rules) The dependency graph is (1 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (4 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [0] = 0; [s_](X0) = X0 + 1; [true] = 0; [false] = 0; [_gt_](X0,X1) = 0; ['_gt_`](X0,X1) = X0; Checking module: { _lt_(V_3,V_1) -> _gt_(V_1,V_3) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { d(s_(V_1),s_(V_3)) -> d(V_1,V_3), d(0,V_3) -> V_3 } (2 rules) The dependency graph is (1 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (3 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [0] = 1; [s_](X0) = X0 + 1; [d](X0,X1) = X1*X0; ['d`](X0,X1) = X1*X0; Checking module: { equal(V_4,V_4) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U22(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U21(tt,V_0,V_3) -> U22(equal(_gt_(V_0,V_3),true)) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { quot(V_3,V_0) -> U31(tt,V_0,V_3), quot(V_3,V_0) -> U21(tt,V_0,V_3), quot(V_0,V_0) -> s_(0), U32(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U31(tt,V_0,V_3) -> U32(equal(_gt_(V_3,V_0),true),V_0,V_3) } (5 rules) The dependency graph is (1 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (16 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. No solution found for these parameters. No solution found for these constraints. Trying strongly connected part criterion. Trying to solve the following constraints: (16 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (16 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Time out for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (16 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. No modular termination proof found. - : unit = () The last proof attempt failed. - : unit = () Quitting. Standard error: