DONT KNOW Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : 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,V1,V2) -> U152(isBool(V1),V2), U152(tt,V2) -> U153(isBool(V2)), U153(tt) -> tt, U161(tt,V1,V2) -> U162(isBool(V1),V2), U162(tt,V2) -> U163(isBool(V2)), U163(tt) -> tt, U171(tt,V1,V2) -> U172(isBool(V1),V2), U172(tt,V2) -> U173(isBool(V2)), U173(tt) -> tt, U181(tt,V1,V2) -> U182(isBool(V1),V2), U182(tt,V2) -> U183(isBool(V2)), U183(tt) -> tt, U191(tt,V1) -> U192(isBool(V1)), U192(tt) -> tt, U201(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(and(isBool(A),isBoolKind(A)),A), _and_(_xor_(B,C),A) -> U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))),A,B,C), _and_(false,A) -> U31(and(isBool(A),isBoolKind(A))), _and_(true,A) -> U41(and(isBool(A),isBoolKind(A)),A), _implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B), _isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U), _isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U))), _isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U), _isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U))), _or_(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B), _xor_(A,A) -> U111(and(isBool(A),isBoolKind(A))), _xor_(false,A) -> U121(and(isBool(A),isBoolKind(A)),A), and(tt,X) -> X, equal(X,X) -> tt, if_then_else_fi(B,U,U') -> U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')), and(isS(U),isSKind(U)))),B,U'), if_then_else_fi(true,U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U), isBool(false) -> tt, isBool(true) -> tt, isBool(_and_(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2), isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2), isBool(_isEqualTo_(V1,V2)) -> tt, isBool(_isNotEqualTo_(V1,V2)) -> tt, isBool(_or_(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2), isBool(_xor_(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2), isBool(not_(V1)) -> U191(isBoolKind(V1),V1), isBoolKind(false) -> tt, isBoolKind(true) -> tt, isBoolKind(_and_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)), isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)), isBoolKind(_isEqualTo_(V1,V2)) -> tt, isBoolKind(_isNotEqualTo_(V1,V2)) -> tt, isBoolKind(_or_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)), isBoolKind(_xor_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)), isBoolKind(not_(V1)) -> isBoolKind(V1), not_(A) -> U201(and(isBool(A),isBoolKind(A)),A), not_(false) -> true, not_(true) -> false } (68 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: { 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: { U192(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U183(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U173(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U163(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U153(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: { 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: { _implies_(V_0,V_1) -> U51(and(and(isBool(V_0),isBoolKind(V_0)),and(isBool(V_1),isBoolKind(V_1))),V_0,V_1), isBoolKind(not_(V_5)) -> isBoolKind(V_5), isBoolKind(_xor_(V_5,V_6)) -> and(isBoolKind(V_5),isBoolKind(V_6)), isBoolKind(_or_(V_5,V_6)) -> and(isBoolKind(V_5),isBoolKind(V_6)), isBoolKind(_isNotEqualTo_(V_5,V_6)) -> tt, isBoolKind(_isEqualTo_(V_5,V_6)) -> tt, isBoolKind(_implies_(V_5,V_6)) -> and(isBoolKind(V_5),isBoolKind(V_6)), isBoolKind(_and_(V_5,V_6)) -> and(isBoolKind(V_5),isBoolKind(V_6)), isBoolKind(true) -> tt, isBoolKind(false) -> tt, if_then_else_fi(V_1,V_4,V_3) -> U131(and(and(isBool(V_1),isBoolKind(V_1)),and(and(isS(V_3),isSKind(V_3)), and(isS(V_4),isSKind(V_4)))),V_1,V_3), if_then_else_fi(true,V_4,V_3) -> U141(and(and(isS(V_3),isSKind(V_3)),and(isS(V_4),isSKind(V_4))),V_4), U81(tt,V_3,V_4) -> if_then_else_fi(_isEqualTo_(V_4,V_3),false,true), _isNotEqualTo_(V_4,V_3) -> U81(and(and(isS(V_3),isSKind(V_3)),and(isS(V_4),isSKind(V_4))),V_3,V_4), _isNotEqualTo_(V_4,V_4) -> U91(and(isS(V_4),isSKind(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_4) -> U71(and(isS(V_4),isSKind(V_4))), _isEqualTo_(V_4,V_3) -> U61(and(and(isS(V_3),isSKind(V_3)),and(isS(V_4),isSKind(V_4))),V_3,V_4), isBool(false) -> tt, isBool(true) -> tt, isBool(_and_(V_5,V_6)) -> U151(and(isBoolKind(V_5),isBoolKind(V_6)),V_5,V_6), isBool(_implies_(V_5,V_6)) -> U161(and(isBoolKind(V_5),isBoolKind(V_6)),V_5,V_6), isBool(_isEqualTo_(V_5,V_6)) -> tt, isBool(_isNotEqualTo_(V_5,V_6)) -> tt, isBool(_or_(V_5,V_6)) -> U171(and(isBoolKind(V_5),isBoolKind(V_6)),V_5,V_6), isBool(_xor_(V_5,V_6)) -> U181(and(isBoolKind(V_5),isBoolKind(V_6)),V_5,V_6), isBool(not_(V_5)) -> U191(isBoolKind(V_5),V_5), _xor_(false,V_0) -> U121(and(isBool(V_0),isBoolKind(V_0)),V_0), _xor_(V_0,V_0) -> U111(and(isBool(V_0),isBoolKind(V_0))), U201(tt,V_0) -> _xor_(true,V_0), _and_(true,V_0) -> U41(and(isBool(V_0),isBoolKind(V_0)),V_0), _and_(false,V_0) -> U31(and(isBool(V_0),isBoolKind(V_0))), _and_(_xor_(V_1,V_2),V_0) -> U21(and(and(isBool(V_0),isBoolKind(V_0)),and(and(isBool(V_1),isBoolKind(V_1)), and(isBool(V_2),isBoolKind(V_2)))),V_0,V_1,V_2), _and_(V_0,V_0) -> U11(and(isBool(V_0),isBoolKind(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(and(isBool(V_0),isBoolKind(V_0)),and(isBool(V_1),isBoolKind(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)), U152(tt,V_6) -> U153(isBool(V_6)), U151(tt,V_5,V_6) -> U152(isBool(V_5),V_6), U162(tt,V_6) -> U163(isBool(V_6)), U161(tt,V_5,V_6) -> U162(isBool(V_5),V_6), U172(tt,V_6) -> U173(isBool(V_6)), U171(tt,V_5,V_6) -> U172(isBool(V_5),V_6), U182(tt,V_6) -> U183(isBool(V_6)), U181(tt,V_5,V_6) -> U182(isBool(V_5),V_6), U191(tt,V_5) -> U192(isBool(V_5)), not_(V_0) -> U201(and(isBool(V_0),isBoolKind(V_0)),V_0), not_(false) -> true, not_(true) -> false, U51(tt,V_0,V_1) -> not_(_xor_(_and_(V_0,V_1),V_0)) } (51 rules) The dependency graph is (1 nodes) Checking each of the 6 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (75 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: (75 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: (75 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: (75 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: (75 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: (75 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: (75 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: (75 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: