MAYBE *** Computating Strongly Quasi-Reducible Parts *** TRS: [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))), 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) -> if(?y,?x,s(+(?x,-(?y,s(0))))) ] [ 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) -> if(?y,?x,s(+(?x,-(?y,s(0))))) ] E: [ 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: [ if(?x,?y,?y) = ?y ] Termination proof failed. new/if1.trs: Failure(unknown) (1642 msec.)