YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)),
     eq(?x,?x) -> true,
     neq(?x,s(?x)) -> true ]
Constructors: {0,s,true,false}
Defined function symbols: {eq,neq,not}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)) ]
   [ eq(?x,?x) -> true,
     neq(?x,s(?x)) -> true ]
Trying with:
R:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)) ]
E:
   [ eq(?x,?x) = true,
     neq(?x,s(?x)) = true ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ eq : Nat,Nat -> Bool,
     neq : Nat,Nat -> Bool,
     not : Bool -> Bool,
     true : Bool,
     false : Bool,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)) ]
Conjecture Part:
   [ eq(?x,?x) = true,
     neq(?x,s(?x)) = true ]
Precedence (by weight): {(0,7),(s,5),(eq,2),(neq,6),(not,4),(true,1),(false,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)) ]
Conjectures:
   [ eq(?x,?x) = true,
     neq(?x,s(?x)) = true ]
STEP 0
ES:
   [ eq(?x,?x) = true,
     neq(?x,s(?x)) = true ]
HS:
   [ ]
ES0:
   [ eq(?x,?x) = true,
     not(eq(?x,s(?x))) = true ]
HS0:
   [ ]
ES1:
   [ eq(?x,?x) = true,
     not(eq(?x,s(?x))) = true ]
HS1:
   [ ]
Expand eq(?x,?x) = true
   [ true = true,
     eq(?y_3,?y_3) = true ]
ES2:
   [ true = true,
     eq(?y_3,?y_3) = true,
     not(eq(?x,s(?x))) = true ]
HS2:
   [ eq(?x,?x) -> true ]
STEP 1
ES:
   [ true = true,
     eq(?y_3,?y_3) = true,
     not(eq(?x,s(?x))) = true ]
HS:
   [ eq(?x,?x) -> true ]
ES0:
   [ true = true,
     true = true,
     not(eq(?x,s(?x))) = true ]
HS0:
   [ eq(?x,?x) -> true ]
ES1:
   [ not(eq(?x,s(?x))) = true ]
HS1:
   [ eq(?x,?x) -> true ]
Expand not(eq(?x,s(?x))) = true
   [ not(false) = true,
     not(eq(?x_3,s(?x_3))) = true ]
ES2:
   [ true = true,
     not(eq(?x_3,s(?x_3))) = true ]
HS2:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
STEP 2
ES:
   [ true = true,
     not(eq(?x_3,s(?x_3))) = true ]
HS:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
ES0:
   [ true = true,
     true = true ]
HS0:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
ES1:
   [ ]
HS1:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
Conj part consisits of inductive theorems of R0.
new/eq.trs: Success(GCR)
(24 msec.)