NO
Rewrite Rules:
   [ +(?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) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) = +(?y,?x),
     ?z_2 = ?z_2,
     ?z_3 = ?z_3 ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
not Left-Linear, not Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
Sort Assignment:
 + : 29*29=>29
 - : 29*29=>29
 0 : =>29
 s : 29=>29
 if : 29*29*29=>29
non-linear variables: {?y_4}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
unknown innermost-termination for terms of non-linear types
unknown Quasi-Left-Linear & Parallel-Closed
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
Sort Assignment:
 + : 29*29=>29
 - : 29*29=>29
 0 : =>29
 s : 29=>29
 if : 29*29*29=>29
non-linear variables: {?y,?x,?y_4}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
Rnl:
0: {0,1,2,3,4,5,6,7}
1: {}
2: {}
3: {}
4: {0,1,2,3,4,5,6,7}
5: {}
6: {}
7: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
Sort Assignment:
 + : 29*29=>29
 - : 29*29=>29
 0 : =>29
 s : 29=>29
 if : 29*29*29=>29
non-linear variables: {?y,?x,?y_4}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     if(0,?y_2,?z_2) -> ?y_2,
     if(s(?x_3),?y_3,?z_3) -> ?z_3,
     if(?x_4,?y_4,?y_4) -> ?y_4,
     -(?x_5,0) -> ?x_5,
     -(0,s(?y_6)) -> 0,
     -(s(?x_7),s(?y_7)) -> -(?x_7,?y_7) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 11 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
   [ +(?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) ]
 (success)
Witness for Non-Confluence: <if(c_1,0,s(-(c_1,s(0)))) <- +(0,c_1) -> c_1>
Direct Methods: not CR

Final result: not CR
new/if2.trs: Success(not CR)
(38 msec.)