NO
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y),
     +(s(s(?x)),?y) -> s(s(+(?y,?x))),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_3,?y) = +(+(?y,0),?x_3),
     +(?x_3,s(?y_1)) = +(+(?y_1,s(0)),?x_3),
     +(?x_3,s(s(+(?y_2,?x_2)))) = +(+(?y_2,s(s(?x_2))),?x_3),
     +(?x_1,+(+(?z,?y),?x)) = +(+(+(?y,?z),?x),?x_1) ]
Outer CPs:
   [ +(?y_3,?z_3) = +(+(?z_3,?y_3),0),
     s(+(?y_3,?z_3)) = +(+(?z_3,?y_3),s(0)),
     s(s(+(+(?y_3,?z_3),?x_2))) = +(+(?z_3,?y_3),s(s(?x_2))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly 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:
   [ +(+(?z_3,?y_3),0) = +(?y_3,?z_3),
     +(+(?y,0),?x_4) = +(?x_4,?y),
     +(+(?z_3,?y_3),s(0)) = s(+(?y_3,?z_3)),
     +(+(?y,s(0)),?x_4) = +(?x_4,s(?y)),
     +(+(?z_3,?y_3),s(s(?x))) = s(s(+(+(?y_3,?z_3),?x))),
     +(+(?y,s(s(?x))),?x_4) = +(?x_4,s(s(+(?y,?x)))),
     +(+(?z_1,?y_1),?y) = +(+(+(?y_1,?z_1),?y),0),
     ?z = +(+(?z,0),0),
     s(?z) = +(+(?z,s(0)),0),
     s(s(+(?z,?x_4))) = +(+(?z,s(s(?x_4))),0),
     s(+(+(?z_1,?y_1),?y)) = +(+(+(?y_1,?z_1),?y),s(0)),
     s(?z) = +(+(?z,0),s(0)),
     s(s(?z)) = +(+(?z,s(0)),s(0)),
     s(s(s(+(?z,?x_4)))) = +(+(?z,s(s(?x_4))),s(0)),
     s(s(+(+(+(?z_4,?y_4),?y),?x_3))) = +(+(+(?y_4,?z_4),?y),s(s(?x_3))),
     s(s(+(?z,?x_3))) = +(+(?z,0),s(s(?x_3))),
     s(s(+(s(?z),?x_3))) = +(+(?z,s(0)),s(s(?x_3))),
     s(s(+(s(s(+(?z,?x_7))),?x_3))) = +(+(?z,s(s(?x_7))),s(s(?x_3))),
     +(?y,?z) = +(+(?z,?y),0),
     s(+(?y,?z)) = +(+(?z,?y),s(0)),
     s(s(+(+(?y,?z),?x_3))) = +(+(?z,?y),s(s(?x_3))),
     +(?x,+(+(?z_1,?y_1),?y)) = +(+(+(?y_1,?z_1),?y),?x),
     +(?x,?z) = +(+(?z,0),?x),
     +(?x,s(?z)) = +(+(?z,s(0)),?x),
     +(?x,s(s(+(?z,?x_4)))) = +(+(?z,s(s(?x_4))),?x),
     +(+(+(+(?z_2,?y_2),?y),?x),?x_1) = +(?x_1,+(+(+(?y_2,?z_2),?y),?x)),
     +(+(?z,?x),?x_1) = +(?x_1,+(+(?z,0),?x)),
     +(+(s(?z),?x),?x_1) = +(?x_1,+(+(?z,s(0)),?x)),
     +(+(s(s(+(?z,?x_5))),?x),?x_1) = +(?x_1,+(+(?z,s(s(?x_5))),?x)),
     +(+(+(?y,?z),?x),?x_1) = +(?x_1,+(+(?z,?y),?x)) ]
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 <+(?x_3,?y), +(+(?y,0),?x_3)> by Rules <0, 3> preceded by [(+,2)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 6 rules by 3 steps unfolding
obtain 25 candidates for checking non-joinability
check by TCAP-Approximation (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
Witness for Non-Confluence: <+(c_1,0) <- +(c_1,+(0,0)) -> c_1>
Direct Methods: not CR

Combined result: not CR
/tmp/fileCzMiHM.trs: Success(not CR)
(59 msec.)