MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) -> +(?y,?x),
     if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s}
Defined function symbols: {+,-,if}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> +(?y,?x) ]
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     if(?x,?y,?y) -> ?y ]
Rule part & Conj Part:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))) ]
   [ +(?x,?y) -> +(?y,?x),
     if(?x,?y,?y) -> ?y ]
Trying with:
R:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> +(?y,?x) ]
E:
   [ +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     if(?x,?y,?y) = ?y ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     if : Nat,Nat,Nat -> Nat,
     - : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> +(?y,?x) ]
Conjecture Part:
   [ +(?x,?y) = if(?y,?x,s(+(?x,-(?y,s(0))))),
     if(?x,?y,?y) = ?y ]
Termination proof failed.
Trying with:
R:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))) ]
E:
   [ +(?x,?y) = +(?y,?x),
     if(?x,?y,?y) = ?y ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     if : Nat,Nat,Nat -> Nat,
     - : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))) ]
Conjecture Part:
   [ +(?x,?y) = +(?y,?x),
     if(?x,?y,?y) = ?y ]
Termination proof failed.
new/if2.trs: Failure(unknown)
(1674 msec.)