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 = { U101(tt,A,B) -> _xor_(_and_(A,B),A,B),
             U11(tt,A) -> A,
             U111(tt) -> false,
             U121(tt,A) -> A,
             U131(tt,B,U') -> U132(equal(_isNotEqualTo_(B,true),true),U'),
             U132(tt,U') -> U',
             U141(tt,U) -> U,
             U151(tt,A) -> _xor_(true,A),
             U21(tt,A,B,C) -> _xor_(_and_(A,B),_and_(A,C)),
             U31(tt) -> false,
             U41(tt,A) -> A,
             U51(tt,A,B) -> not_(_xor_(_and_(A,B),A)),
             U61(tt,U',U) -> U62(equal(_isNotEqualTo_(U,U'),true)),
             U62(tt) -> false,
             U71(tt) -> true,
             U81(tt,U',U) -> if_then_else_fi(_isEqualTo_(U,U'),false,true),
             U91(tt) -> false,
             _and_(A,A) -> U11(isBool(A),A),
             _and_(_xor_(B,C),A) ->
             U21(and(isBool(A),and(isBool(B),isBool(C))),A,B,C),
             _and_(false,A) -> U31(isBool(A)),
             _and_(true,A) -> U41(isBool(A),A),
             _implies_(A,B) -> U51(and(isBool(A),isBool(B)),A,B),
             _isEqualTo_(U,U') -> U61(and(isS(U'),isS(U)),U',U),
             _isEqualTo_(U,U) -> U71(isS(U)),
             _isNotEqualTo_(U,U') -> U81(and(isS(U'),isS(U)),U',U),
             _isNotEqualTo_(U,U) -> U91(isS(U)),
             _or_(A,B) -> U101(and(isBool(A),isBool(B)),A,B),
             _xor_(A,A) -> U111(isBool(A)),
             _xor_(false,A) -> U121(isBool(A),A),
             and(tt,X) -> X,
             equal(X,X) -> tt,
             if_then_else_fi(B,U,U') ->
             U131(and(isBool(B),and(isS(U'),isS(U))),B,U'),
             if_then_else_fi(true,U,U') -> U141(and(isS(U'),isS(U)),U),
             isBool(false) -> tt,
             isBool(true) -> tt,
             isBool(_and_(V1,V2)) -> and(isBool(V1),isBool(V2)),
             isBool(_implies_(V1,V2)) -> and(isBool(V1),isBool(V2)),
             isBool(_isEqualTo_(V1,V2)) ->
             and(isUniversal(V1),isUniversal(V2)),
             isBool(_isNotEqualTo_(V1,V2)) ->
             and(isUniversal(V1),isUniversal(V2)),
             isBool(_or_(V1,V2)) -> and(isBool(V1),isBool(V2)),
             isBool(_xor_(V1,V2)) -> and(isBool(V1),isBool(V2)),
             isBool(not_(V1)) -> isBool(V1),
             not_(A) -> U151(isBool(A),A),
             not_(false) -> true,
             not_(true) -> false } (45 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:
{}

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:
{ U71(tt) -> true } (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:
{ U62(tt) -> false } (1 rules)

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

Checking module:
{ equal(V_7,V_7) -> tt } (1 rules)

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

Checking module:
{ U91(tt) -> false } (1 rules)

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

Checking module:
{ U141(tt,V_4) -> V_4 } (1 rules)

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

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

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

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

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

Checking module:
{ U111(tt) -> false } (1 rules)

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

Checking module:
{ U41(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) -> false } (1 rules)

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

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

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

Checking module:
{ _implies_(V_0,V_1) -> U51(and(isBool(V_0),isBool(V_1)),V_0,V_1),
  isBool(false) -> tt,
  isBool(true) -> tt,
  isBool(_and_(V_5,V_6)) -> and(isBool(V_5),isBool(V_6)),
  isBool(_implies_(V_5,V_6)) -> and(isBool(V_5),isBool(V_6)),
  isBool(_isEqualTo_(V_5,V_6)) -> and(isUniversal(V_5),isUniversal(V_6)),
  isBool(_isNotEqualTo_(V_5,V_6)) -> and(isUniversal(V_5),isUniversal(V_6)),
  isBool(_or_(V_5,V_6)) -> and(isBool(V_5),isBool(V_6)),
  isBool(_xor_(V_5,V_6)) -> and(isBool(V_5),isBool(V_6)),
  isBool(not_(V_5)) -> isBool(V_5),
  _xor_(false,V_0) -> U121(isBool(V_0),V_0),
  _xor_(V_0,V_0) -> U111(isBool(V_0)),
  U151(tt,V_0) -> _xor_(true,V_0),
  _and_(true,V_0) -> U41(isBool(V_0),V_0),
  _and_(false,V_0) -> U31(isBool(V_0)),
  _and_(_xor_(V_1,V_2),V_0) ->
  U21(and(isBool(V_0),and(isBool(V_1),isBool(V_2))),V_0,V_1,V_2),
  _and_(V_0,V_0) -> U11(isBool(V_0),V_0),
  U101(tt,V_0,V_1) -> _xor_(_and_(V_0,V_1),V_0,V_1),
  _or_(V_0,V_1) -> U101(and(isBool(V_0),isBool(V_1)),V_0,V_1),
  U21(tt,V_0,V_1,V_2) -> _xor_(_and_(V_0,V_1),_and_(V_0,V_2)),
  not_(true) -> false,
  not_(false) -> true,
  not_(V_0) -> U151(isBool(V_0),V_0),
  U51(tt,V_0,V_1) -> not_(_xor_(_and_(V_0,V_1),V_0)),
  if_then_else_fi(true,V_4,V_3) -> U141(and(isS(V_3),isS(V_4)),V_4),
  if_then_else_fi(V_1,V_4,V_3) ->
  U131(and(isBool(V_1),and(isS(V_3),isS(V_4))),V_1,V_3),
  U81(tt,V_3,V_4) -> if_then_else_fi(_isEqualTo_(V_4,V_3),false,true),
  _isNotEqualTo_(V_4,V_4) -> U91(isS(V_4)),
  _isNotEqualTo_(V_4,V_3) -> U81(and(isS(V_3),isS(V_4)),V_3,V_4),
  U131(tt,V_1,V_3) -> U132(equal(_isNotEqualTo_(V_1,true),true),V_3),
  U61(tt,V_3,V_4) -> U62(equal(_isNotEqualTo_(V_4,V_3),true)),
  _isEqualTo_(V_4,V_3) -> U61(and(isS(V_3),isS(V_4)),V_3,V_4),
  _isEqualTo_(V_4,V_4) -> U71(isS(V_4)) } (33 rules)

The dependency graph is
(1 nodes)
Checking each of the 5 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(46 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 0; 
[and](X0,X1) = X1; 
[false] = 0; 
[true] = 0; 
[isUniversal](X0) = 0; 
[U111](X0) = 0; 
[U121](X0,X1) = X1; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1) = X1; 
[U141](X0,X1) = X1; 
[isS](X0) = 0; 
[U91](X0) = 0; 
[equal](X0,X1) = 0; 
[U132](X0,X1) = X1; 
[U62](X0) = 0; 
[U71](X0) = 0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = 0; 
[U131](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 0; 
[U81](X0,X1,X2) = 0; 
[if_then_else_fi](X0,X1,X2) = X2 + X1; 
[U51](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 2; 
[not_](X0) = X0 + 1; 
[U21](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[_or_](X0,X1) = 2*X1*X0 + 3*X1 + 3*X0 + 3; 
[U101](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; 
[_and_](X0,X1) = X1*X0 + X1 + X0; 
[U151](X0,X1) = X1 + 1; 
[_xor_](X0,X1) = X1 + X0 + 1; 
[isBool](X0) = 0; 
[_implies_](X0,X1) = X1*X0 + X1 + 2*X0 + 2; 

Checking component 2
Trying simple graph criterion.
Trying to solve the following constraints:
(53 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 strongly connected part criterion.
Trying to solve the following constraints:
(53 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 1; 
[and](X0,X1) = X1*X0; 
[false] = 0; 
[true] = 1; 
[isUniversal](X0) = 0; 
[U111](X0) = 0; 
[U121](X0,X1) = X1; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1) = X1; 
[U141](X0,X1) = X1; 
[isS](X0) = 0; 
[U91](X0) = 0; 
[equal](X0,X1) = 1; 
[U132](X0,X1) = X1; 
[U62](X0) = 0; 
[U71](X0) = X0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = 0; 
[U131](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 1; 
[U81](X0,X1,X2) = 1; 
[if_then_else_fi](X0,X1,X2) = X2 + X1*X0; 
[U51](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 3; 
[not_](X0) = X0 + 2; 
[U21](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[_or_](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; 
[U101](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; 
[_and_](X0,X1) = X1*X0 + X1 + X0; 
[U151](X0,X1) = X1 + 2; 
[_xor_](X0,X1) = X1 + X0 + 1; 
[isBool](X0) = 1; 
[_implies_](X0,X1) = X1*X0 + X1 + 2*X0 + 3; 
['U21`](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + X1; 

The dependency graph is
(14 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(48 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 strongly connected part criterion.
Trying to solve the following constraints:
(48 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:
(48 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:
(48 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 2; 
[and](X0,X1) = X1; 
[false] = 0; 
[true] = 0; 
[isUniversal](X0) = 0; 
[U111](X0) = 0; 
[U121](X0,X1) = X1; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1) = X1; 
[U141](X0,X1) = X1; 
[isS](X0) = 0; 
[U91](X0) = 0; 
[equal](X0,X1) = 2; 
[U132](X0,X1) = X1; 
[U62](X0) = 0; 
[U71](X0) = 0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = 0; 
[U131](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 0; 
[U81](X0,X1,X2) = 0; 
[if_then_else_fi](X0,X1,X2) = X2 + X1; 
[U51](X0,X1,X2) = 2*X2*X1 + 2*X2 + 3*X1 + 3; 
[not_](X0) = X0 + 1; 
[U21](X0,X1,X2,X3) = 2*X3*X1 + 2*X3 + 2*X2*X1 + 2*X2 + 2*X1*X0 + 3; 
[_or_](X0,X1) = 2*X1*X0 + 3*X1 + 3*X0 + 3; 
[U101](X0,X1,X2) = 2*X2*X1 + 3*X2 + 3*X1 + 3; 
[_and_](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; 
[U151](X0,X1) = X1 + 1; 
[_xor_](X0,X1) = X1 + X0 + 1; 
[isBool](X0) = 2; 
[_implies_](X0,X1) = 2*X1*X0 + 2*X1 + 3*X0 + 3; 

The dependency graph is
(33 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(46 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 strongly connected part criterion.
Trying to solve the following constraints:
(46 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: