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 = { zeros -> cons(0,zeros),
             U11(tt,L) -> s(length(L)),
             U21(tt) -> nil,
             U31(tt,IL,M,N) -> cons(N,take(M,IL)),
             and(tt,X) -> X,
             isNat(0) -> tt,
             isNat(length(V1)) -> isNatList(V1),
             isNat(s(V1)) -> isNat(V1),
             isNatIList(V) -> isNatList(V),
             isNatIList(zeros) -> tt,
             isNatIList(cons(V1,V2)) -> and(isNat(V1),isNatIList(V2)),
             isNatList(nil) -> tt,
             isNatList(cons(V1,V2)) -> and(isNat(V1),isNatList(V2)),
             isNatList(take(V1,V2)) -> and(isNat(V1),isNatIList(V2)),
             length(nil) -> 0,
             length(cons(N,L)) -> U11(and(isNatList(L),isNat(N)),L),
             take(0,IL) -> U21(isNatIList(IL)),
             take(s(M),cons(N,IL)) ->
             U31(and(isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) }
             (18 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:
{ and(tt,V_7) -> V_7 } (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:
{ U21(tt) -> nil } (1 rules)

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

Checking module:
{ zeros -> cons(0,zeros) } (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: