YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/eq.trs
Input rules:
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     eq(?x:Nat,?x:Nat) -> true,
     neq(?x:Nat,s(?x:Nat)) -> true ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ eq(0,0) -> true,
     eq(0,s(?y:Nat)) -> false,
     eq(s(?x:Nat),0) -> false,
     eq(s(?x:Nat),s(?y:Nat)) -> eq(?x:Nat,?y:Nat),
     not(true) -> false,
     not(false) -> true,
     neq(?x:Nat,?y:Nat) -> not(eq(?x:Nat,?y:Nat)),
     eq(?x:Nat,?x:Nat) -> true,
     neq(?x:Nat,s(?x:Nat)) -> true ]
Constructor pattern: [true,false,s(?x_1),0]
Defined pattern: [not(?x_1),neq(?x_2,?x_3),eq(?x_2,?x_3)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for not(?x_1):
   [ not(true) -> false,
     not(false) -> true ]
candidate for neq(?x_2,?x_3):
   [ neq(?x,?y) -> not(eq(?x,?y)) ]
candidate for eq(?x_2,?x_3):
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 neq : Mul;
 0 : Mul;
 false : Mul,  true : Mul;
 eq : Mul;
 not : Mul,  s : Mul;
Rules:
   [ not(true) -> false,
     not(false) -> true,
     neq(?x,?y) -> not(eq(?x,?y)),
     eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),0) -> false,
     eq(s(?x),s(?y)) -> 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_4,?y_4) = true ]
ES2:
   [ true = true,
     eq(?y_4,?y_4) = true,
     not(eq(?x,s(?x))) = true ]
HS2:
   [ eq(?x,?x) -> true ]
STEP 1
ES:
   [ true = true,
     eq(?y_4,?y_4) = true,
     not(eq(?x,s(?x))) = true ]
HS:
   [ eq(?x,?x) -> true ]
ES0:
   [ true = true,
     eq(?y_4,?y_4) = 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_4,s(?x_4))) = true ]
ES2:
   [ true = true,
     not(eq(?x_4,s(?x_4))) = true ]
HS2:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
STEP 2
ES:
   [ true = true,
     not(eq(?x_4,s(?x_4))) = true ]
HS:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
ES0:
   [ true = true,
     not(eq(?x_4,s(?x_4))) = true ]
HS0:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
ES1:
   [ ]
HS1:
   [ not(eq(?x,s(?x))) -> true,
     eq(?x,?x) -> true ]
: Success(GCR)
(18 msec.)