NO
Rewrite Rules:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x) -> if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     +(0,0) -> 0,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ s(+(?x_2,s(?y_3))) = s(+(?y_3,s(?x_2))) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ s(+(?y_3,s(?x))) = s(+(?x,s(?y_3))) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <s(+(?y_3,s(?x_2))), s(+(?x_2,s(?y_3)))> by Rules <5, 4> preceded by []
unknown Diagram Decreasing
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x_1) -> if(zero(?x_1),s(0),*(?x_1,fact(-(?x_1,s(0))))),
     +(0,0) -> 0,
     +(s(?x_2),?y_2) -> s(+(?x_2,?y_2)),
     +(?x_3,s(?y_3)) -> s(+(?y_3,?x_3)),
     *(0,?y_4) -> 0,
     *(s(?x_5),?y_5) -> +(*(?x_5,?y_5),?y_5),
     if(true,?y_6,?z_6) -> ?y_6,
     if(false,?y_7,?z_7) -> ?z_7,
     -(?x_8,0) -> ?x_8,
     -(0,s(?y_9)) -> 0,
     -(s(?x_10),s(?y_10)) -> -(?x_10,?y_10) ]
Sort Assignment:
 * : 40*40=>40
 + : 40*40=>40
 - : 40*40=>40
 0 : =>40
 s : 40=>40
 if : 30*40*40=>40
 fact : 40=>40
 true : =>30
 zero : 40=>30
 false : =>30
non-linear variables: {?x_1,?y_5}
non-linear types: {40}
types leq non-linear types: {40}
rules applicable to terms of non-linear types:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x_1) -> if(zero(?x_1),s(0),*(?x_1,fact(-(?x_1,s(0))))),
     +(0,0) -> 0,
     +(s(?x_2),?y_2) -> s(+(?x_2,?y_2)),
     +(?x_3,s(?y_3)) -> s(+(?y_3,?x_3)),
     *(0,?y_4) -> 0,
     *(s(?x_5),?y_5) -> +(*(?x_5,?y_5),?y_5),
     if(true,?y_6,?z_6) -> ?y_6,
     if(false,?y_7,?z_7) -> ?z_7,
     -(?x_8,0) -> ?x_8,
     -(0,s(?y_9)) -> 0,
     -(s(?x_10),s(?y_10)) -> -(?x_10,?y_10) ]
Rnl:
0: {}
1: {}
2: {0,1,2,3,4,5,6,7,8,9,10,11,12}
3: {}
4: {}
5: {}
6: {}
7: {0,1,2,3,4,5,6,7,8,9,10,11,12}
8: {}
9: {}
10: {}
11: {}
12: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x_1) -> if(zero(?x_1),s(0),*(?x_1,fact(-(?x_1,s(0))))),
     +(0,0) -> 0,
     +(s(?x_2),?y_2) -> s(+(?x_2,?y_2)),
     +(?x_3,s(?y_3)) -> s(+(?y_3,?x_3)),
     *(0,?y_4) -> 0,
     *(s(?x_5),?y_5) -> +(*(?x_5,?y_5),?y_5),
     if(true,?y_6,?z_6) -> ?y_6,
     if(false,?y_7,?z_7) -> ?z_7,
     -(?x_8,0) -> ?x_8,
     -(0,s(?y_9)) -> 0,
     -(s(?x_10),s(?y_10)) -> -(?x_10,?y_10) ]
Sort Assignment:
 * : 40*40=>40
 + : 40*40=>40
 - : 40*40=>40
 0 : =>40
 s : 40=>40
 if : 30*40*40=>40
 fact : 40=>40
 true : =>30
 zero : 40=>30
 false : =>30
non-linear variables: {?x_1,?y_5}
non-linear types: {40}
types leq non-linear types: {40}
rules applicable to terms of non-linear types:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x_1) -> if(zero(?x_1),s(0),*(?x_1,fact(-(?x_1,s(0))))),
     +(0,0) -> 0,
     +(s(?x_2),?y_2) -> s(+(?x_2,?y_2)),
     +(?x_3,s(?y_3)) -> s(+(?y_3,?x_3)),
     *(0,?y_4) -> 0,
     *(s(?x_5),?y_5) -> +(*(?x_5,?y_5),?y_5),
     if(true,?y_6,?z_6) -> ?y_6,
     if(false,?y_7,?z_7) -> ?z_7,
     -(?x_8,0) -> ?x_8,
     -(0,s(?y_9)) -> 0,
     -(s(?x_10),s(?y_10)) -> -(?x_10,?y_10) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
obtain 9 candidates for checking non-joinability
check by TCAP-Approximation   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z: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: <s(s(+(c_2,c_1))) <- +(s(c_1),s(c_2)) -> s(s(+(c_1,c_2)))>
Direct Methods: not CR

Final result: not CR
new/if3.trs: Success(not CR)
(16 msec.)