YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if1.trs
Input rules:
   [ +(?x:Nat,?y:Nat) -> if(?y:Nat,?x:Nat,s(+(?x:Nat,-(?y:Nat,s(0))))),
     if(0,?y:Nat,?z:Nat) -> ?y:Nat,
     if(s(?x:Nat),?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Nat,?y:Nat,?y:Nat) -> ?y:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ +(?x:Nat,?y:Nat) -> if(?y:Nat,?x:Nat,s(+(?x:Nat,-(?y:Nat,s(0))))),
     if(0,?y:Nat,?z:Nat) -> ?y:Nat,
     if(s(?x:Nat),?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Nat,?y:Nat,?y:Nat) -> ?y:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
Constructor pattern: [s(?x_1),0]
Defined pattern: [-(?x_2,?x_3),if(?x_3,?x_4,?x_5),+(?x_2,?x_3)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for -(?x_2,?x_3):
   [ -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z ]
No orientable rules for +(?x_2,?x_3). Add rules, and retry...
Added rules:
   [ +(s(?x_1),?x_3) -> if(?x_3,s(?x_1),s(+(s(?x_1),-(?x_3,s(0))))),
     +(0,?x_3) -> if(?x_3,0,s(+(0,-(?x_3,s(0))))),
     +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(?x_2,0) -> ?x_2,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_1),?x_2)),
     +(s(?x_1),0) -> s(?x_1),
     +(0,s(?x_1)) -> s(+(0,?x_1)),
     +(0,0) -> 0 ]
candidate for +(?x_2,?x_3):
   [ +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(?x_2,0) -> ?x_2 ]
   [ +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(s(?x_1),0) -> s(?x_1),
     +(0,0) -> 0 ]
   [ +(?x_2,0) -> ?x_2,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_1),?x_2)),
     +(0,s(?x_1)) -> s(+(0,?x_1)) ]
   [ +(s(?x_1),s(?x_2)) -> s(+(s(?x_1),?x_2)),
     +(s(?x_1),0) -> s(?x_1),
     +(0,s(?x_1)) -> s(+(0,?x_1)),
     +(0,0) -> 0 ]
Find a quasi-ordering ...
order successfully found
Precedence:
 - : Mul,  + : Mul;
 0 : Mul;
 s : Mul;
 if : Mul;
Rules:
   [ -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(?x_2,0) -> ?x_2 ]
Conjectures:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
STEP 0
ES:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS:
   [ ]
ES0:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS0:
   [ ]
ES1:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS1:
   [ ]
Expand if(?x,?y,?y) = ?y
   [ ?z_4 = ?z_4,
     ?z_5 = ?z_5 ]
ES2:
   [ ?z_4 = ?z_4,
     ?z_5 = ?z_5,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS2:
   [ if(?x,?y,?y) -> ?y ]
STEP 1
ES:
   [ ?z_4 = ?z_4,
     ?z_5 = ?z_5,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS:
   [ if(?x,?y,?y) -> ?y ]
ES0:
   [ ?z_4 = ?z_4,
     ?z_5 = ?z_5,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS0:
   [ if(?x,?y,?y) -> ?y ]
ES1:
   [ +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS1:
   [ if(?x,?y,?y) -> ?y ]
Expand if(?y,?x,s(+(?x,-(?y,s(0))))) = +(?x,?y)
   [ ?y_4 = +(?y_4,0),
     s(+(?y_5,-(s(?x_5),s(0)))) = +(?y_5,s(?x_5)) ]
ES2:
   [ ?y_4 = +(?y_4,0),
     s(+(?y_5,?x_5)) = +(?y_5,s(?x_5)) ]
HS2:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     if(?x,?y,?y) -> ?y ]
STEP 2
ES:
   [ ?y_4 = +(?y_4,0),
     s(+(?y_5,?x_5)) = +(?y_5,s(?x_5)) ]
HS:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ ?y_4 = ?y_4,
     s(+(?y_5,?x_5)) = s(+(?y_5,?x_5)) ]
HS0:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ ]
HS1:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     if(?x,?y,?y) -> ?y ]
: Success(GCR)
(25 msec.)