YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if2.trs
Input rules:
   [ +(?x:Nat,?y:Nat) -> if(?y:Nat,?x:Nat,s(+(?x:Nat,-(?y:Nat,s(0))))),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     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))))),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     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) -> s(+(?x_3,?x_1)),
     +(0,?x_3) -> ?x_3,
     +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(?x_2,0) -> ?x_2,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_2),?x_1)),
     +(s(?x_1),0) -> s(?x_1),
     +(0,s(?x_1)) -> s(?x_1),
     +(0,0) -> 0 ]
candidate for +(?x_2,?x_3):
   [ +(s(?x_1),?x_3) -> s(+(?x_3,?x_1)),
     +(0,?x_3) -> ?x_3 ]
   [ +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(?x_2,0) -> ?x_2 ]
   [ +(s(?x_1),?x_3) -> s(+(?x_3,?x_1)),
     +(0,s(?x_1)) -> s(?x_1),
     +(0,0) -> 0 ]
   [ +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(s(?x_1),0) -> s(?x_1),
     +(0,0) -> 0 ]
   [ +(s(?x_1),?x_3) -> s(+(?x_3,?x_1)),
     +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(0,0) -> 0 ]
   [ +(s(?x_1),?x_3) -> s(+(?x_3,?x_1)),
     +(?x_2,0) -> ?x_2,
     +(0,s(?x_1)) -> s(?x_1) ]
   [ +(0,?x_3) -> ?x_3,
     +(?x_2,s(?x_1)) -> s(+(?x_2,?x_1)),
     +(s(?x_1),0) -> s(?x_1) ]
   [ +(0,?x_3) -> ?x_3,
     +(?x_2,0) -> ?x_2,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_2),?x_1)) ]
   [ +(0,?x_3) -> ?x_3,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_2),?x_1)),
     +(s(?x_1),0) -> s(?x_1) ]
   [ +(?x_2,0) -> ?x_2,
     +(s(?x_1),s(?x_2)) -> s(+(s(?x_2),?x_1)),
     +(0,s(?x_1)) -> s(?x_1) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 - : Mul,  + : Mul;
 s : Mul;
 0 : 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,
     +(s(?x_1),?x_3) -> s(+(?x_3,?x_1)),
     +(0,?x_3) -> ?x_3 ]
Conjectures:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) = +(?y,?x) ]
STEP 0
ES:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) = +(?y,?x) ]
HS:
   [ ]
ES0:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) = +(?y,?x) ]
HS0:
   [ ]
ES1:
   [ if(?x,?y,?y) = ?y,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) = +(?y,?x) ]
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) = +(?y,?x),
     +(?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) = +(?y,?x),
     +(?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) = +(?y,?x),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS0:
   [ if(?x,?y,?y) -> ?y ]
ES1:
   [ +(?x,?y) = +(?y,?x),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS1:
   [ if(?x,?y,?y) -> ?y ]
Expand +(?x,?y) = +(?y,?x)
   [ s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)),
     ?x_9 = +(?x_9,0) ]
ES2:
   [ s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)),
     ?x_9 = +(?x_9,0),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS2:
   [ +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
STEP 2
ES:
   [ s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)),
     ?x_9 = +(?x_9,0),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS:
   [ +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)),
     ?x_9 = +(?x_9,0),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS0:
   [ +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)),
     ?x_9 = +(?x_9,0),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS1:
   [ +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
Expand +(?x_9,0) = ?x_9
   [ s(+(0,?x_6)) = s(?x_6),
     0 = 0 ]
ES2:
   [ s(?x_6) = s(?x_6),
     0 = 0,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)) ]
HS2:
   [ +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
STEP 3
ES:
   [ s(?x_6) = s(?x_6),
     0 = 0,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)) ]
HS:
   [ +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ s(?x_6) = s(?x_6),
     0 = 0,
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)) ]
HS0:
   [ +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     s(+(?x_8,?x_6)) = +(?x_8,s(?x_6)) ]
HS1:
   [ +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
Expand +(?x_8,s(?x_6)) = s(+(?x_8,?x_6))
   [ s(+(s(?x),?x_8)) = s(+(s(?x_8),?x)),
     s(?x) = s(+(0,?x)) ]
ES2:
   [ s(s(+(?x_8,?x))) = s(+(s(?x_8),?x)),
     s(?x) = s(+(0,?x)),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS2:
   [ +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
STEP 4
ES:
   [ s(s(+(?x_8,?x))) = s(+(s(?x_8),?x)),
     s(?x) = s(+(0,?x)),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS:
   [ +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ s(s(+(?x_8,?x))) = s(s(+(?x,?x_8))),
     s(?x) = s(?x),
     +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS0:
   [ +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))) ]
HS1:
   [ +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     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),
     +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
STEP 5
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),
     +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     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),
     +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ ]
HS1:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     +(?x_8,s(?x_6)) -> s(+(?x_8,?x_6)),
     +(?x_9,0) -> ?x_9,
     +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
: Success(GCR)
(30 msec.)