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,U',U) -> U12(equal(_isNotEqualTo_(U,U'),true)),
             U12(tt) -> false,
             U21(tt,B,U') -> U22(equal(_isNotEqualTo_(B,true),true),U'),
             U22(tt,U') -> U',
             _and_(A,A) -> A,
             _and_(_xor_(B,C),A) -> _xor_(_and_(A,B),_and_(A,C)),
             _and_(false,A) -> false,
             _and_(true,A) -> A,
             _implies_(A,B) -> not_(_xor_(_and_(A,B),A)),
             _isEqualTo_(U,U') -> U11(tt,U',U),
             _isEqualTo_(U,U) -> true,
             _isNotEqualTo_(U,U') ->
             if_then_else_fi(_isEqualTo_(U,U'),false,true),
             _isNotEqualTo_(U,U) -> false,
             _or_(A,B) -> _xor_(_and_(A,B),A,B),
             _xor_(A,A) -> false,
             _xor_(false,A) -> A,
             and(tt,X) -> X,
             equal(X,X) -> tt,
             if_then_else_fi(B,U,U') -> U21(tt,B,U'),
             if_then_else_fi(true,U,U') -> U,
             not_(A) -> _xor_(true,A),
             not_(false) -> true,
             not_(true) -> false } (23 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:
{ and(tt,V_5) -> V_5 } (1 rules)

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

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

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

Checking module:
{ equal(V_5,V_5) -> tt } (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:
{ U12(tt) -> false } (1 rules)

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

Checking module:
{ if_then_else_fi(true,V_4,V_3) -> V_4,
  if_then_else_fi(V_1,V_4,V_3) -> U21(tt,V_1,V_3),
  _isNotEqualTo_(V_4,V_3) -> if_then_else_fi(_isEqualTo_(V_4,V_3),false,true),
  _isNotEqualTo_(V_4,V_4) -> false,
  U11(tt,V_3,V_4) -> U12(equal(_isNotEqualTo_(V_4,V_3),true)),
  _isEqualTo_(V_4,V_3) -> U11(tt,V_3,V_4),
  _isEqualTo_(V_4,V_4) -> true,
  U21(tt,V_1,V_3) -> U22(equal(_isNotEqualTo_(V_1,true),true),V_3) }
  (8 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:
(17 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:
(17 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 to solve the following constraints:
(17 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 to solve the following constraints:
(17 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:
(17 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:
(17 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:
(17 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: