NO
Rewrite Rules:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)),
     neq(?x,s(?x)) -> true ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ true = eq(0,0),
     false = eq(s(?y),0),
     eq(?x_1,?y_1) = eq(s(?y_1),s(?x_1)),
     not(eq(?x_3,s(?x_3))) = true ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
not Left-Linear, Right-Linear
unknown Simple-Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x_1),s(?y_1)) -> eq(?x_1,?y_1),
     eq(?x_2,?y_2) -> eq(?y_2,?x_2),
     not(true) -> false,
     not(false) -> true,
     neq(?x_3,?y_3) -> not(eq(?x_3,?y_3)),
     neq(?x_4,s(?x_4)) -> true ]
Sort Assignment:
 0 : =>13
 s : 13=>13
 eq : 13*13=>22
 neq : 13*13=>22
 not : 22=>22
 true : =>22
 false : =>22
non-linear variables: {?x_4}
non-linear types: {13}
types leq non-linear types: {13}
rules applicable to terms of non-linear types:
   [ ]
terms of non-linear types are innermost terminating
outer CP <p,q> = <true, eq(0,0)>
parallel reducts of p: {true}
parallel reducts of q: {eq(0,0),true,eq(0,0)}
join at true
check subst from p
check subst from q
is {} ground inst. preserving? (yes)
outer CP <p,q> = <false, eq(s(?y:13),0)>
parallel reducts of p: {false}
parallel reducts of q: {eq(s(?y:13),0),eq(0,s(?y:13))}
unknown Quasi-Left-Linear & Parallel-Closed
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x_1),s(?y_1)) -> eq(?x_1,?y_1),
     eq(?x_2,?y_2) -> eq(?y_2,?x_2),
     not(true) -> false,
     not(false) -> true,
     neq(?x_3,?y_3) -> not(eq(?x_3,?y_3)),
     neq(?x_4,s(?x_4)) -> true ]
Sort Assignment:
 0 : =>13
 s : 13=>13
 eq : 13*13=>22
 neq : 13*13=>22
 not : 22=>22
 true : =>22
 false : =>22
non-linear variables: {?x_4}
non-linear types: {13}
types leq non-linear types: {13}
rules applicable to terms of non-linear types:
   [ ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
terms of non-linear types are innermost terminating
Critical Pair <eq(0,0), true> by Rules <3, 0>
 convertible by a reduction of rules [->(0)]
Critical Pair <eq(s(?y),0), false> by Rules <3, 1>
 convertible by a reduction of rules [->(3),->(1)]
Critical Pair <eq(s(?y_1),s(?x_1)), eq(?x_1,?y_1)> by Rules <3, 2>
 convertible by a reduction of rules [->(2),->(3)]
 convertible by a reduction of rules [->(2),(3)<-]
 convertible by a reduction of rules [->(3),->(2)]
Critical Pair <true, not(eq(?x_4,s(?x_4)))> by Rules <7, 6>
no joinable sequence for some critical pairs
unknown Quasi-Linear & Linearized-Decreasing
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x_1),s(?y_1)) -> eq(?x_1,?y_1),
     eq(?x_2,?y_2) -> eq(?y_2,?x_2),
     not(true) -> false,
     not(false) -> true,
     neq(?x_3,?y_3) -> not(eq(?x_3,?y_3)),
     neq(?x_4,s(?x_4)) -> true ]
Sort Assignment:
 0 : =>13
 s : 13=>13
 eq : 13*13=>22
 neq : 13*13=>22
 not : 22=>22
 true : =>22
 false : =>22
non-linear variables: {?x_4}
non-linear types: {13}
types leq non-linear types: {13}
rules applicable to terms of non-linear types:
   [ ]
terms of non-linear types are terminating
Check Joinablility of CP from NLR:
done.
Critical Pair <eq(0,0), true> by Rules <3, 0>
 convertible by a reduction of rules [->(0)]
Critical Pair <eq(s(?y),0), false> by Rules <3, 1>
 convertible by a reduction of rules [->(3),->(1)]
Critical Pair <eq(s(?y_1),s(?x_1)), eq(?x_1,?y_1)> by Rules <3, 2>
 convertible by a reduction of rules [->(2),->(3)]
 convertible by a reduction of rules [->(2),(3)<-]
 convertible by a reduction of rules [->(3),->(2)]
Critical Pair <true, not(eq(?x_4,s(?x_4)))> by Rules <7, 6>
no joinable sequence for some critical pairs
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 12 rules by 3 steps unfolding
obtain 15 candidates for checking non-joinability
check by TCAP-Approximation   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     eq(?x:Nat,?y:Nat) -> eq(?y:Nat,?x:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     neq(?x:Nat,s(?x:Nat)) -> true ]
 (failure)
 (success)
<F,Q,Q_f,Delta> where
   F = {(0,0),(s,1),(eq,2),(c_1,0),(neq,2),(not,1),(true,0),(false,0)}
   Q = {q_0,q_1,q_{eq(s(c_1),c_1)},q_{c_1},q_{eq(*,*)},q_{s(c_1)},q_{*}}
   Qf = {q_0,q_1}
   Delta = 
   [ 0 -> q_{*},
     s(q_{c_1}) -> q_{s(c_1)},
     s(q_{*}) -> q_{*},
     eq(q_{c_1},q_{s(c_1)}) -> q_{eq(s(c_1),c_1)},
     eq(q_{s(c_1)},q_{c_1}) -> q_{eq(s(c_1),c_1)},
     eq(q_{*},q_{*}) -> q_{eq(*,*)},
     eq(q_{*},q_{*}) -> q_{*},
     c_1 -> q_{c_1},
     c_1 -> q_{*},
     neq(q_{*},q_{*}) -> q_{*},
     not(q_{eq(s(c_1),c_1)}) -> q_0,
     not(q_{*}) -> q_{*},
     true -> q_1,
     true -> q_{eq(*,*)},
     true -> q_{*},
     false -> q_{eq(*,*)},
     false -> q_{*} ]
Witness for Non-Confluence: <not(eq(s(c_1),c_1)), true>
Direct Methods: not CR

Final result: not CR
new/eq3.trs: Success(not CR)
(163 msec.)