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) -> U102(isBool(B),A,B),
             U102(tt,A,B) -> _xor_(_and_(A,B),A,B),
             U11(tt,A) -> A,
             U111(tt) -> false,
             U121(tt,A) -> A,
             U131(tt,B,U',U) -> U132(isS(U'),B,U',U),
             U132(tt,B,U',U) -> U133(isS(U),B,U'),
             U133(tt,B,U') -> U134(equal(_isNotEqualTo_(B,true),true),U'),
             U134(tt,U') -> U',
             U141(tt,U) -> U142(isS(U),U),
             U142(tt,U) -> U,
             U151(tt,V2) -> U152(isBool(V2)),
             U152(tt) -> tt,
             U161(tt,V2) -> U162(isBool(V2)),
             U162(tt) -> tt,
             U171(tt,V2) -> U172(isUniversal(V2)),
             U172(tt) -> tt,
             U181(tt,V2) -> U182(isUniversal(V2)),
             U182(tt) -> tt,
             U191(tt,V2) -> U192(isBool(V2)),
             U192(tt) -> tt,
             U201(tt,V2) -> U202(isBool(V2)),
             U202(tt) -> tt,
             U21(tt,A,B,C) -> U22(isBool(B),A,B,C),
             U211(tt) -> tt,
             U22(tt,A,B,C) -> U23(isBool(C),A,B,C),
             U221(tt,A) -> _xor_(true,A),
             U23(tt,A,B,C) -> _xor_(_and_(A,B),_and_(A,C)),
             U31(tt) -> false,
             U41(tt,A) -> A,
             U51(tt,A,B) -> U52(isBool(B),A,B),
             U52(tt,A,B) -> not_(_xor_(_and_(A,B),A)),
             U61(tt,U',U) -> U62(isS(U),U',U),
             U62(tt,U',U) -> U63(equal(_isNotEqualTo_(U,U'),true)),
             U63(tt) -> false,
             U71(tt) -> true,
             U81(tt,U',U) -> U82(isS(U),U',U),
             U82(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(isBool(A),A,B,C),
             _and_(false,A) -> U31(isBool(A)),
             _and_(true,A) -> U41(isBool(A),A),
             _implies_(A,B) -> U51(isBool(A),A,B),
             _isEqualTo_(U,U') -> U61(isS(U'),U',U),
             _isEqualTo_(U,U) -> U71(isS(U)),
             _isNotEqualTo_(U,U') -> U81(isS(U'),U',U),
             _isNotEqualTo_(U,U) -> U91(isS(U)),
             _or_(A,B) -> U101(isBool(A),A,B),
             _xor_(A,A) -> U111(isBool(A)),
             _xor_(false,A) -> U121(isBool(A),A),
             equal(X,X) -> tt,
             if_then_else_fi(B,U,U') -> U131(isBool(B),B,U',U),
             if_then_else_fi(true,U,U') -> U141(isS(U'),U),
             isBool(false) -> tt,
             isBool(true) -> tt,
             isBool(_and_(V1,V2)) -> U151(isBool(V1),V2),
             isBool(_implies_(V1,V2)) -> U161(isBool(V1),V2),
             isBool(_isEqualTo_(V1,V2)) -> U171(isUniversal(V1),V2),
             isBool(_isNotEqualTo_(V1,V2)) -> U181(isUniversal(V1),V2),
             isBool(_or_(V1,V2)) -> U191(isBool(V1),V2),
             isBool(_xor_(V1,V2)) -> U201(isBool(V1),V2),
             isBool(not_(V1)) -> U211(isBool(V1)),
             not_(A) -> U221(isBool(A),A),
             not_(false) -> true,
             not_(true) -> false } (66 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:
{ U121(tt,V_0) -> V_0 } (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:
{ U111(tt) -> false } (1 rules)

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:
{ U63(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:
{ U142(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:
{ U141(tt,V_4) -> U142(isS(V_4),V_4) } (1 rules)

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

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

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

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

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

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

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

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

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

Checking module:
{ U182(tt) -> 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:
{ U181(tt,V_6) -> U182(isUniversal(V_6)) } (1 rules)

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

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

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

Checking module:
{ U171(tt,V_6) -> U172(isUniversal(V_6)) } (1 rules)

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

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

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

Checking module:
{ U152(tt) -> tt } (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(isBool(V_0),V_0,V_1),
  isBool(not_(V_5)) -> U211(isBool(V_5)),
  isBool(_xor_(V_5,V_6)) -> U201(isBool(V_5),V_6),
  isBool(_or_(V_5,V_6)) -> U191(isBool(V_5),V_6),
  isBool(_isNotEqualTo_(V_5,V_6)) -> U181(isUniversal(V_5),V_6),
  isBool(_isEqualTo_(V_5,V_6)) -> U171(isUniversal(V_5),V_6),
  isBool(_implies_(V_5,V_6)) -> U161(isBool(V_5),V_6),
  isBool(_and_(V_5,V_6)) -> U151(isBool(V_5),V_6),
  isBool(true) -> tt,
  isBool(false) -> tt,
  _xor_(V_0,V_0) -> U111(isBool(V_0)),
  _xor_(false,V_0) -> U121(isBool(V_0),V_0),
  U221(tt,V_0) -> _xor_(true,V_0),
  U151(tt,V_6) -> U152(isBool(V_6)),
  U161(tt,V_6) -> U162(isBool(V_6)),
  U191(tt,V_6) -> U192(isBool(V_6)),
  U201(tt,V_6) -> U202(isBool(V_6)),
  U22(tt,V_0,V_1,V_2) -> U23(isBool(V_2),V_0,V_1,V_2),
  U21(tt,V_0,V_1,V_2) -> U22(isBool(V_1),V_0,V_1,V_2),
  _and_(V_0,V_0) -> U11(isBool(V_0),V_0),
  _and_(_xor_(V_1,V_2),V_0) -> U21(isBool(V_0),V_0,V_1,V_2),
  _and_(false,V_0) -> U31(isBool(V_0)),
  _and_(true,V_0) -> U41(isBool(V_0),V_0),
  U102(tt,V_0,V_1) -> _xor_(_and_(V_0,V_1),V_0,V_1),
  U101(tt,V_0,V_1) -> U102(isBool(V_1),V_0,V_1),
  _or_(V_0,V_1) -> U101(isBool(V_0),V_0,V_1),
  U23(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) -> U221(isBool(V_0),V_0),
  U52(tt,V_0,V_1) -> not_(_xor_(_and_(V_0,V_1),V_0)),
  U51(tt,V_0,V_1) -> U52(isBool(V_1),V_0,V_1),
  if_then_else_fi(V_1,V_4,V_3) -> U131(isBool(V_1),V_1,V_3,V_4),
  if_then_else_fi(true,V_4,V_3) -> U141(isS(V_3),V_4),
  U82(tt,V_3,V_4) -> if_then_else_fi(_isEqualTo_(V_4,V_3),false,true),
  U81(tt,V_3,V_4) -> U82(isS(V_4),V_3,V_4),
  _isNotEqualTo_(V_4,V_4) -> U91(isS(V_4)),
  _isNotEqualTo_(V_4,V_3) -> U81(isS(V_3),V_3,V_4),
  U133(tt,V_1,V_3) -> U134(equal(_isNotEqualTo_(V_1,true),true),V_3),
  U132(tt,V_1,V_3,V_4) -> U133(isS(V_4),V_1,V_3),
  U131(tt,V_1,V_3,V_4) -> U132(isS(V_3),V_1,V_3,V_4),
  U62(tt,V_3,V_4) -> U63(equal(_isNotEqualTo_(V_4,V_3),true)),
  U61(tt,V_3,V_4) -> U62(isS(V_4),V_3,V_4),
  _isEqualTo_(V_4,V_4) -> U71(isS(V_4)),
  _isEqualTo_(V_4,V_3) -> U61(isS(V_3),V_3,V_4) } (45 rules)

The dependency graph is
(3 nodes)
Checking each of the 4 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(67 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; 
[false] = 0; 
[true] = 0; 
[isUniversal](X0) = 0; 
[U172](X0) = 0; 
[U171](X0,X1) = 0; 
[U182](X0) = 0; 
[U181](X0,X1) = 0; 
[U211](X0) = 0; 
[U111](X0) = 0; 
[U121](X0,X1) = X1; 
[U152](X0) = 0; 
[U162](X0) = 0; 
[U192](X0) = 0; 
[U202](X0) = 0; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1) = X1; 
[isS](X0) = 0; 
[U142](X0,X1) = X1; 
[U141](X0,X1) = X1; 
[U91](X0) = 0; 
[equal](X0,X1) = 0; 
[U134](X0,X1) = X1; 
[U63](X0) = 0; 
[U71](X0) = 0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = 0; 
[U62](X0,X1,X2) = 0; 
[U131](X0,X1,X2,X3) = X2; 
[U132](X0,X1,X2,X3) = X2; 
[U133](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 0; 
[U81](X0,X1,X2) = 0; 
[U82](X0,X1,X2) = 0; 
[if_then_else_fi](X0,X1,X2) = X2 + X1; 
[U51](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 2; 
[U52](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 2; 
[not_](X0) = X0 + 1; 
[U23](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; 
[U102](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; 
[_and_](X0,X1) = X1*X0 + X1 + X0; 
[U21](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[U22](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[U201](X0,X1) = 0; 
[U191](X0,X1) = 0; 
[U161](X0,X1) = 0; 
[U151](X0,X1) = 0; 
[U221](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:
(76 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:
(76 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; 
[false] = 0; 
[true] = 0; 
[isUniversal](X0) = 0; 
[U172](X0) = 0; 
[U171](X0,X1) = 0; 
[U182](X0) = 0; 
[U181](X0,X1) = 0; 
[U211](X0) = 0; 
[U111](X0) = 0; 
[U121](X0,X1) = X1; 
[U152](X0) = 0; 
[U162](X0) = 0; 
[U192](X0) = 0; 
[U202](X0) = 0; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1) = X1; 
[isS](X0) = 0; 
[U142](X0,X1) = X1; 
[U141](X0,X1) = X1; 
[U91](X0) = 0; 
[equal](X0,X1) = 0; 
[U134](X0,X1) = X1; 
[U63](X0) = 0; 
[U71](X0) = 0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = 0; 
[U62](X0,X1,X2) = 0; 
[U131](X0,X1,X2,X3) = X2; 
[U132](X0,X1,X2,X3) = X2; 
[U133](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 0; 
[U81](X0,X1,X2) = 0; 
[U82](X0,X1,X2) = 0; 
[if_then_else_fi](X0,X1,X2) = X2 + X1; 
[U51](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 2; 
[U52](X0,X1,X2) = X2*X1 + X2 + 2*X1 + 2; 
[not_](X0) = X0 + 1; 
[U23](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; 
[U102](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; 
[_and_](X0,X1) = X1*X0 + X1 + X0; 
[U21](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[U22](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + 2*X1 + 1; 
[U201](X0,X1) = 0; 
[U191](X0,X1) = 0; 
[U161](X0,X1) = 0; 
[U151](X0,X1) = 0; 
[U221](X0,X1) = X1 + 1; 
[_xor_](X0,X1) = X1 + X0 + 1; 
[isBool](X0) = 0; 
[_implies_](X0,X1) = X1*X0 + X1 + 2*X0 + 2; 
['U23`](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + X1; 
['U21`](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + X1 + 1; 
['U22`](X0,X1,X2,X3) = X3*X1 + X3 + X2*X1 + X2 + X1 + 1; 

The dependency graph is
(20 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(70 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:
(70 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:
(70 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; 
[false] = 1; 
[true] = 1; 
[isUniversal](X0) = 0; 
[U172](X0) = X0; 
[U171](X0,X1) = 0; 
[U182](X0) = X0; 
[U181](X0,X1) = 0; 
[U211](X0) = 1; 
[U111](X0) = 1; 
[U121](X0,X1) = X1; 
[U152](X0) = X0; 
[U162](X0) = 1; 
[U192](X0) = 1; 
[U202](X0) = X0; 
[U11](X0,X1) = X1; 
[U31](X0) = 1; 
[U41](X0,X1) = X1; 
[isS](X0) = 0; 
[U142](X0,X1) = X1*X0; 
[U141](X0,X1) = 0; 
[U91](X0) = X0; 
[equal](X0,X1) = 1; 
[U134](X0,X1) = X1; 
[U63](X0) = 1; 
[U71](X0) = X0; 
[_isEqualTo_](X0,X1) = 0; 
[U61](X0,X1,X2) = X0; 
[U62](X0,X1,X2) = 1; 
[U131](X0,X1,X2,X3) = 0; 
[U132](X0,X1,X2,X3) = X2*X0; 
[U133](X0,X1,X2) = X2; 
[_isNotEqualTo_](X0,X1) = 0; 
[U81](X0,X1,X2) = 0; 
[U82](X0,X1,X2) = 0; 
[if_then_else_fi](X0,X1,X2) = 0; 
[U51](X0,X1,X2) = 2*X2*X1 + X2 + 2*X1 + 3; 
[U52](X0,X1,X2) = 2*X2*X1 + X2 + 2*X1 + 3; 
[not_](X0) = X0 + 2; 
[U23](X0,X1,X2,X3) = 2*X3*X1 + X3 + 2*X2*X1 + X2 + 2*X1 + 1; 
[_or_](X0,X1) = 3*X1*X0 + 3*X1 + 3*X0 + 2; 
[U101](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 2; 
[U102](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 2; 
[_and_](X0,X1) = 2*X1*X0 + X1 + X0; 
[U21](X0,X1,X2,X3) = 2*X3*X1 + X3 + 2*X2*X1 + X2 + 2*X1 + X0; 
[U22](X0,X1,X2,X3) = 2*X3*X1 + X3 + 2*X2*X1 + X2 + 2*X1 + 1; 
[U201](X0,X1) = X1; 
[U191](X0,X1) = 1; 
[U161](X0,X1) = 1; 
[U151](X0,X1) = X1; 
[U221](X0,X1) = X1 + 2; 
[_xor_](X0,X1) = X1 + X0 + 1; 
[isBool](X0) = X0; 
[_implies_](X0,X1) = 2*X1*X0 + X1 + 2*X0 + 3; 

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