DONT KNOW
Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51

- : unit = ()
- : unit = ()
X : variable_set = <variable set>

F : signature = <signature>
R : HTRS = { U11(tt,N,XS) -> U12(tt,N,XS),
             U12(tt,N,XS) -> snd(splitAt(N,XS)),
             U21(tt,X) -> U22(tt,X),
             U22(tt,X) -> X,
             U31(tt,N) -> U32(tt,N),
             U32(tt,N) -> N,
             U41(tt,N,XS) -> U42(tt,N,XS),
             U42(tt,N,XS) -> head(afterNth(N,XS)),
             U51(tt,Y) -> U52(tt,Y),
             U52(tt,Y) -> Y,
             U61(tt,N,X,XS) -> U62(tt,N,X,XS),
             U62(tt,N,X,XS) -> U63(tt,N,X,XS),
             U63(tt,N,X,XS) -> U64(splitAt(N,XS),X),
             U64(pair(YS,ZS),X) -> pair(cons(X,YS),ZS),
             U71(tt,XS) -> U72(tt,XS),
             U72(tt,XS) -> XS,
             U81(tt,N,XS) -> U82(tt,N,XS),
             U82(tt,N,XS) -> fst(splitAt(N,XS)),
             afterNth(N,XS) -> U11(tt,N,XS),
             fst(pair(X,Y)) -> U21(tt,X),
             head(cons(N,XS)) -> U31(tt,N),
             natsFrom(N) -> cons(N,natsFrom(s(N))),
             sel(N,XS) -> U41(tt,N,XS),
             snd(pair(X,Y)) -> U51(tt,Y),
             splitAt(0,XS) -> pair(nil,XS),
             splitAt(s(N),cons(X,XS)) -> U61(tt,N,X,XS),
             tail(cons(N,XS)) -> U71(tt,XS),
             take(N,XS) -> U81(tt,N,XS) } (28 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:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U22(tt,V_1) -> V_1 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U21(tt,V_1) -> U22(tt,V_1) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ fst(pair(V_1,V_3)) -> U21(tt,V_1) } (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:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U64(pair(V_4,V_5),V_1) -> pair(cons(V_1,V_4),V_5) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ splitAt(0,V_2) -> pair(nil,V_2),
  splitAt(s(V_0),cons(V_1,V_2)) -> U61(tt,V_0,V_1,V_2),
  U63(tt,V_0,V_1,V_2) -> U64(splitAt(V_0,V_2),V_1),
  U62(tt,V_0,V_1,V_2) -> U63(tt,V_0,V_1,V_2),
  U61(tt,V_0,V_1,V_2) -> U62(tt,V_0,V_1,V_2) } (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:
(10 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[cons](X0,X1) = 0; 
[s](X0) = X0 + 2; 
[tt] = 2; 
[pair](X0,X1) = 0; 
[0] = 0; 
[nil] = 0; 
[U64](X0,X1) = 0; 
[U61](X0,X1,X2,X3) = 0; 
[U62](X0,X1,X2,X3) = 0; 
[U63](X0,X1,X2,X3) = 0; 
[splitAt](X0,X1) = 0; 
['U61`](X0,X1,X2,X3) = 2*X1 + 2*X0; 
['U62`](X0,X1,X2,X3) = 2*X1 + X0 + 1; 
['U63`](X0,X1,X2,X3) = 2*X1 + X0; 
['splitAt`](X0,X1) = 2*X0 + 1; 


Checking module:
{ U82(tt,V_0,V_2) -> fst(splitAt(V_0,V_2)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U81(tt,V_0,V_2) -> U82(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ take(V_0,V_2) -> U81(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U72(tt,V_2) -> V_2 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U71(tt,V_2) -> U72(tt,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ tail(cons(V_0,V_2)) -> U71(tt,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U32(tt,V_0) -> V_0 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U31(tt,V_0) -> U32(tt,V_0) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ head(cons(V_0,V_2)) -> U31(tt,V_0) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U52(tt,V_3) -> V_3 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U51(tt,V_3) -> U52(tt,V_3) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ snd(pair(V_1,V_3)) -> U51(tt,V_3) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U12(tt,V_0,V_2) -> snd(splitAt(V_0,V_2)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U11(tt,V_0,V_2) -> U12(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ afterNth(V_0,V_2) -> U11(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U42(tt,V_0,V_2) -> head(afterNth(V_0,V_2)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U41(tt,V_0,V_2) -> U42(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ sel(V_0,V_2) -> U41(tt,V_0,V_2) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ natsFrom(V_0) -> cons(V_0,natsFrom(s(V_0))) } (1 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:
(2 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:
(2 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.
No modular termination proof found.
- : unit = ()
The last proof attempt failed.
- : unit = ()

Quitting.
Standard error: