YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_4,?y) = +(+(?x_4,0),?y),
     +(?x_4,?x_1) = +(+(?x_4,?x_1),0),
     +(?x_4,s(+(?y_2,?x_2))) = +(+(?x_4,s(?x_2)),?y_2),
     +(?x_4,s(+(?y_3,?x_3))) = +(+(?x_4,?x_3),s(?y_3)),
     +(?x_4,+(?y_5,?x_5)) = +(+(?x_4,?x_5),?y_5),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ]
Outer CPs:
   [ 0 = 0,
     s(?y_3) = s(+(?y_3,0)),
     +(?y_4,?z_4) = +(+(0,?y_4),?z_4),
     ?y = +(?y,0),
     s(?x_2) = s(+(0,?x_2)),
     ?x_1 = +(0,?x_1),
     s(+(s(?y_3),?x_2)) = s(+(?y_3,s(?x_2))),
     s(+(+(?y_4,?z_4),?x_2)) = +(+(s(?x_2),?y_4),?z_4),
     s(+(?y_2,?x_2)) = +(?y_2,s(?x_2)),
     s(+(?y_3,?x_3)) = +(s(?y_3),?x_3),
     +(+(?x_4,?y_4),?z_4) = +(+(?y_4,?z_4),?x_4) ]
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:
   [ 0 = 0,
     s(+(?y_3,0)) = s(?y_3),
     +(+(0,?y_4),?z_4) = +(?y_4,?z_4),
     +(?y,0) = ?y,
     +(+(?x_5,0),?y) = +(?x_5,?y),
     s(+(0,?x_2)) = s(?x_2),
     +(0,?x) = ?x,
     +(+(?x_5,?x),0) = +(?x_5,?x),
     s(?x) = s(+(0,?x)),
     s(+(?y_3,s(?x))) = s(+(s(?y_3),?x)),
     +(+(s(?x),?y_4),?z_4) = s(+(+(?y_4,?z_4),?x)),
     +(?y,s(?x)) = s(+(?y,?x)),
     +(+(?x_5,s(?x)),?y) = +(?x_5,s(+(?y,?x))),
     s(?y) = s(+(?y,0)),
     s(+(s(?y),?x_3)) = s(+(?y,s(?x_3))),
     +(s(?y),?x) = s(+(?y,?x)),
     +(+(?x_5,?x),s(?y)) = +(?x_5,s(+(?y,?x))),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     ?z = +(+(0,0),?z),
     ?y = +(+(0,?y),0),
     s(+(?z,?x_4)) = +(+(0,s(?x_4)),?z),
     s(+(?y_5,?y)) = +(+(0,?y),s(?y_5)),
     +(?z,?y) = +(+(0,?y),?z),
     s(+(+(+(?y,?y_4),?z_4),?x_3)) = +(+(s(?x_3),?y),+(?y_4,?z_4)),
     s(+(?z,?x_3)) = +(+(s(?x_3),0),?z),
     s(+(?y,?x_3)) = +(+(s(?x_3),?y),0),
     s(+(s(+(?z,?x_7)),?x_3)) = +(+(s(?x_3),s(?x_7)),?z),
     s(+(s(+(?y_8,?y)),?x_3)) = +(+(s(?x_3),?y),s(?y_8)),
     s(+(+(?z,?y),?x_3)) = +(+(s(?x_3),?y),?z),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?z,?x) = +(+(?x,0),?z),
     +(?y,?x) = +(+(?x,?y),0),
     +(s(+(?z,?x_4)),?x) = +(+(?x,s(?x_4)),?z),
     +(s(+(?y_5,?y)),?x) = +(+(?x,?y),s(?y_5)),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(?y,?z) = +(+(0,?y),?z),
     s(+(+(?y,?z),?x_3)) = +(+(s(?x_3),?y),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,?z) = +(+(?x,0),?z),
     +(?x,?y) = +(+(?x,?y),0),
     +(?x,s(+(?z,?x_4))) = +(+(?x,s(?x_4)),?z),
     +(?x,s(+(?y_5,?y))) = +(+(?x,?y),s(?y_5)),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)),
     +(+(?x_1,?x),?y) = +(?x_1,+(+(?x,?y),0)),
     +(+(?x_1,?x),s(+(?z,?x_5))) = +(?x_1,+(+(?x,s(?x_5)),?z)),
     +(+(?x_1,?x),s(+(?y_6,?y))) = +(?x_1,+(+(?x,?y),s(?y_6))),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     ?y = +(?y,0),
     ?x = +(0,?x),
     s(+(?y,?x_3)) = +(?y,s(?x_3)),
     s(+(?y_4,?x)) = +(s(?y_4),?x),
     +(+(?x,?y_5),?z_5) = +(+(?y_5,?z_5),?x),
     +(+(?x_6,?x),?y) = +(?x_6,+(?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_4,?y), +(+(?x_4,0),?y)> by Rules <0, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],1)]>
Critical Pair <+(?x_4,?x_1), +(+(?x_4,?x_1),0)> by Rules <1, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],1)]>
Critical Pair <+(?x_4,s(+(?y_2,?x_2))), +(+(?x_4,s(?x_2)),?y_2)> by Rules <2, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([],3)], [([(+,1)],3),([],2),([(s,1)],4)]>
 joinable by a reduction of rules <[([(+,2),(s,1)],5),([],3),([(s,1),(+,1)],5)], [([(+,1)],3),([],2),([(s,1)],4)]>
 joinable by a reduction of rules <[([],5),([],2),([(s,1)],5)], [([(+,1)],3),([],2),([(s,1)],4)]>
Critical Pair <+(?x_4,s(+(?y_3,?x_3))), +(+(?x_4,?x_3),s(?y_3))> by Rules <3, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([],3)], [([(+,1)],5),([],3),([(s,1)],4)]>
 joinable by a reduction of rules <[([],3)], [([],3),([(s,1),(+,2)],5),([(s,1)],4)]>
 joinable by a reduction of rules <[([(+,2),(s,1)],5),([],3),([(s,1),(+,1)],5)], [([(+,1)],5),([],3),([(s,1)],4)]>
 joinable by a reduction of rules <[([(+,2),(s,1)],5),([],3),([(s,1),(+,1)],5)], [([],3),([(s,1),(+,2)],5),([(s,1)],4)]>
 joinable by a reduction of rules <[([],5),([],2),([(s,1)],5)], [([(+,1)],5),([],3),([(s,1)],4)]>
 joinable by a reduction of rules <[([],5),([],2),([(s,1)],5)], [([],3),([(s,1),(+,2)],5),([(s,1)],4)]>
 joinable by a reduction of rules <[([],5),([],2),([(s,1)],4)], [([],3),([(s,1)],4),([(s,1),(+,1)],5)]>
 joinable by a reduction of rules <[([],3),([(s,1)],5),([(s,1)],4)], [([],3),([(s,1)],4),([(s,1),(+,1)],5)]>
Critical Pair <+(?x_4,+(?y_5,?x_5)), +(+(?x_4,?x_5),?y_5)> by Rules <5, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],5),([],4)], []>
 joinable by a reduction of rules <[([],4),([(+,1)],5)], [([],5),([],4)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <4, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([],4),([(+,1)],4)], [([],4)]>
Critical Pair <0, 0> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <s(+(?y_3,0)), s(?y_3)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],1)], []>
Critical Pair <+(+(0,?y_4),?z_4), +(?y_4,?z_4)> by Rules <4, 0> preceded by []
 joinable by a reduction of rules <[([(+,1)],0)], []>
Critical Pair <+(?y_5,0), ?y_5> by Rules <5, 0> preceded by []
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <s(+(0,?x_2)), s(?x_2)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], []>
Critical Pair <+(0,?x_5), ?x_5> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <s(+(?y_3,s(?x_2))), s(+(s(?y_3),?x_2))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([(s,1)],3)], [([(s,1)],2)]>
Critical Pair <+(+(s(?x_2),?y_4),?z_4), s(+(+(?y_4,?z_4),?x_2))> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([(+,1)],2),([],2),([(s,1)],4)], [([(s,1),(+,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],5),([(+,1)],3),([],2)], [([(s,1)],5),([(s,1)],4),([(s,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([(+,1),(s,1)],5),([],2)], [([(s,1)],5),([(s,1)],4),([(s,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([],5),([],3)], [([(s,1)],5),([(s,1)],4),([(s,1),(+,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([],2),([(s,1),(+,2)],5)], [([(s,1)],5),([(s,1)],4),([(s,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([],2),([(s,1)],5)], [([(s,1)],5),([(s,1)],4),([(s,1),(+,1)],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([],2),([(s,1)],4)], [([(s,1)],5),([(s,1),(+,2)],5),([(s,1)],5)]>
 joinable by a reduction of rules <[([],5),([(+,2)],2),([],3)], [([(s,1)],5),([(s,1)],4),([(s,1),(+,1)],5)]>
Critical Pair <+(?y_5,s(?x_2)), s(+(?y_5,?x_2))> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],3)], [([(s,1)],5)]>
Critical Pair <+(s(?y_3),?x_5), s(+(?y_3,?x_5))> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([],2)], [([(s,1)],5)]>
Critical Pair <+(+(?y_4,?z_4),?x_5), +(+(?x_5,?y_4),?z_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5),([],4)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten +(?x_8,0) and ?x_8
strenghten +(0,?x_5) and ?x_5
strenghten +(?x_11,?y_11) and +(?y_11,?x_11)
strenghten +(?x_14,s(0)) and s(?x_14)
strenghten +(s(0),?x_14) and s(?x_14)
strenghten s(+(?y_3,0)) and s(?y_3)
strenghten s(+(0,?x_2)) and s(?x_2)
strenghten s(+(?x_12,?x_2)) and +(?x_12,s(?x_2))
strenghten s(+(?x_13,?x_2)) and +(s(?x_2),?x_13)
strenghten s(+(?y_3,?x_5)) and +(s(?y_3),?x_5)
strenghten s(+(?y_3,?x_10)) and +(?x_10,s(?y_3))
strenghten +(+(?x_4,?x_1),0) and +(?x_4,?x_1)
strenghten +(+(?x_4,0),?x_8) and +(?x_4,?x_8)
strenghten +(+(0,?y_4),?z_4) and +(?y_4,?z_4)
strenghten s(+(s(0),?x_2)) and s(s(?x_2))
strenghten +(+(?x_4,?x_5),?y_5) and +(?x_4,+(?y_5,?x_5))
strenghten +(+(?x_4,?x_10),?y_10) and +(?x_4,+(?x_10,?y_10))
strenghten +(+(?x_5,?y_4),?z_4) and +(+(?y_4,?z_4),?x_5)
strenghten s(+(s(?y_3),?x_2)) and s(+(?y_3,s(?x_2)))
strenghten +(+(?x_4,?x_14),s(0)) and +(?x_4,s(?x_14))
strenghten +(+(?x_4,?x_3),s(?y_3)) and +(?x_4,s(+(?y_3,?x_3)))
strenghten +(+(?x_4,s(?x_2)),?y_2) and +(?x_4,s(+(?y_2,?x_2)))
strenghten s(+(+(?y_4,?z_4),?x_2)) and +(+(s(?x_2),?y_4),?z_4)
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (8)
  s:= (1)*x1
retract +(0,?y) -> ?y
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= 0
  s:= (4)+(4)*x1
relatively terminating
Huet (modulo AC)
Direct Methods: CR

Final result: CR
191.trs: Success(CR)
(3837 msec.)