YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/eq3.trs
Input rules:
   [ 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 ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ 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 ]
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):
No canditates. Supplement rules, and retry...
patlist: 
{0,0}
{0,s(?y)}
{s(?x),s(?y)}
Required Patterns: {eq(s(?x_1),0)}
Added rules:
   [ eq(s(?x_1),0) -> false ]
candidate for eq(?x_2,?x_3):
   [ eq(0,0) -> true,
     eq(0,s(?y)) -> false,
     eq(s(?x),s(?y)) -> eq(?x,?y),
     eq(s(?x_1),0) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 neq : Mul;
 s : Mul;
 eq : Mul;
 false : Mul,  true : Mul;
 0 : Mul;
 not : 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),s(?y)) -> eq(?x,?y),
     eq(s(?x_1),0) -> false ]
Conjectures:
   [ neq(?x,s(?x)) = true,
     eq(?x,?y) = eq(?y,?x) ]
STEP 0
ES:
   [ neq(?x,s(?x)) = true,
     eq(?x,?y) = eq(?y,?x) ]
HS:
   [ ]
ES0:
   [ not(eq(?x,s(?x))) = true,
     eq(?x,?y) = eq(?y,?x) ]
HS0:
   [ ]
ES1:
   [ not(eq(?x,s(?x))) = true,
     eq(?x,?y) = eq(?y,?x) ]
HS1:
   [ ]
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,
     eq(?x,?y) = eq(?y,?x) ]
HS2:
   [ not(eq(?x,s(?x))) -> true ]
STEP 1
ES:
   [ true = true,
     not(eq(?x_3,s(?x_3))) = true,
     eq(?x,?y) = eq(?y,?x) ]
HS:
   [ not(eq(?x,s(?x))) -> true ]
ES0:
   [ true = true,
     true = true,
     eq(?x,?y) = eq(?y,?x) ]
HS0:
   [ not(eq(?x,s(?x))) -> true ]
ES1:
   [ eq(?x,?y) = eq(?y,?x) ]
HS1:
   [ not(eq(?x,s(?x))) -> true ]
Expand eq(?x,?y) = eq(?y,?x)
   [ true = eq(0,0),
     false = eq(s(?y_2),0),
     eq(?x_3,?y_3) = eq(s(?y_3),s(?x_3)),
     false = eq(0,s(?x_4)) ]
ES2:
   [ true = eq(0,0),
     false = eq(s(?y_2),0),
     eq(?x_3,?y_3) = eq(s(?y_3),s(?x_3)),
     false = eq(0,s(?x_4)) ]
HS2:
   [ eq(?x,?y) -> eq(?y,?x),
     not(eq(?x,s(?x))) -> true ]
STEP 2
ES:
   [ true = eq(0,0),
     false = eq(s(?y_2),0),
     eq(?x_3,?y_3) = eq(s(?y_3),s(?x_3)),
     false = eq(0,s(?x_4)) ]
HS:
   [ eq(?x,?y) -> eq(?y,?x),
     not(eq(?x,s(?x))) -> true ]
ES0:
   [ true = true,
     false = false,
     eq(?x_3,?y_3) = eq(?y_3,?x_3),
     false = false ]
HS0:
   [ eq(?x,?y) -> eq(?y,?x),
     not(eq(?x,s(?x))) -> true ]
ES1:
   [ ]
HS1:
   [ eq(?x,?y) -> eq(?y,?x),
     not(eq(?x,s(?x))) -> true ]
: Success(GCR)
(13 msec.)