YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_4,?y) = +(+(?x_4,0),?y),
     +(?x_4,?x_1) = +(+(?x_4,?x_1),0),
     +(?x_4,s(+(?x_2,?y_2))) = +(+(?x_4,s(?x_2)),?y_2),
     +(?x_4,s(+(?x_3,?y_3))) = +(+(?x_4,?x_3),s(?y_3)),
     +(?x_4,+(?x_5,+(?y_5,?z_5))) = +(+(?x_4,+(?x_5,?y_5)),?z_5),
     +(?y,?z_5) = +(0,+(?y,?z_5)),
     +(?x_1,?z_5) = +(?x_1,+(0,?z_5)),
     +(s(+(?x_2,?y_2)),?z_5) = +(s(?x_2),+(?y_2,?z_5)),
     +(s(+(?x_3,?y_3)),?z_5) = +(?x_3,+(s(?y_3),?z_5)),
     +(+(+(?x_4,?y_4),?z_4),?z_5) = +(?x_4,+(+(?y_4,?z_4),?z_5)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ 0 = 0,
     s(?y_3) = s(+(0,?y_3)),
     +(?y_4,?z_4) = +(+(0,?y_4),?z_4),
     s(?x_2) = s(+(?x_2,0)),
     +(?x_5,?y_5) = +(?x_5,+(?y_5,0)),
     s(+(?x_2,s(?y_3))) = s(+(s(?x_2),?y_3)),
     s(+(?x_2,+(?y_4,?z_4))) = +(+(s(?x_2),?y_4),?z_4),
     s(+(+(?x_5,?y_5),?y_3)) = +(?x_5,+(?y_5,s(?y_3))),
     +(+(+(?x_5,?y_5),?y_4),?z_4) = +(?x_5,+(?y_5,+(?y_4,?z_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(+(0,?y_3)) = s(?y_3),
     +(+(0,?y_4),?z_4) = +(?y_4,?z_4),
     +(+(?x_5,0),?y) = +(?x_5,?y),
     +(0,+(?y,?z_6)) = +(?y,?z_6),
     s(+(?x_2,0)) = s(?x_2),
     +(?x_5,+(?y_5,0)) = +(?x_5,?y_5),
     +(+(?x_5,?x),0) = +(?x_5,?x),
     +(?x,+(0,?z_6)) = +(?x,?z_6),
     s(?x) = s(+(?x,0)),
     s(+(s(?x),?y_3)) = s(+(?x,s(?y_3))),
     +(+(s(?x),?y_4),?z_4) = s(+(?x,+(?y_4,?z_4))),
     +(+(?x_5,s(?x)),?y) = +(?x_5,s(+(?x,?y))),
     +(s(?x),+(?y,?z_6)) = +(s(+(?x,?y)),?z_6),
     s(?y) = s(+(0,?y)),
     s(+(?x_3,s(?y))) = s(+(s(?x_3),?y)),
     +(?x_5,+(?y_5,s(?y))) = s(+(+(?x_5,?y_5),?y)),
     +(+(?x_5,?x),s(?y)) = +(?x_5,s(+(?x,?y))),
     +(?x,+(s(?y),?z_6)) = +(s(+(?x,?y)),?z_6),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     ?z = +(+(0,0),?z),
     ?y = +(+(0,?y),0),
     s(+(?x_4,?z)) = +(+(0,s(?x_4)),?z),
     s(+(?y,?y_5)) = +(+(0,?y),s(?y_5)),
     +(?x_6,+(?y_6,?z)) = +(+(0,+(?x_6,?y_6)),?z),
     s(+(?x_3,+(+(?y,?y_4),?z_4))) = +(+(s(?x_3),?y),+(?y_4,?z_4)),
     s(+(?x_3,?z)) = +(+(s(?x_3),0),?z),
     s(+(?x_3,?y)) = +(+(s(?x_3),?y),0),
     s(+(?x_3,s(+(?x_7,?z)))) = +(+(s(?x_3),s(?x_7)),?z),
     s(+(?x_3,s(+(?y,?y_8)))) = +(+(s(?x_3),?y),s(?y_8)),
     s(+(?x_3,+(?x_9,+(?y_9,?z)))) = +(+(s(?x_3),+(?x_9,?y_9)),?z),
     +(?x_5,+(?y_5,+(+(?y,?y_6),?z_6))) = +(+(+(?x_5,?y_5),?y),+(?y_6,?z_6)),
     +(?x_5,+(?y_5,?z)) = +(+(+(?x_5,?y_5),0),?z),
     +(?x_5,+(?y_5,?y)) = +(+(+(?x_5,?y_5),?y),0),
     +(?x_5,+(?y_5,s(+(?x_9,?z)))) = +(+(+(?x_5,?y_5),s(?x_9)),?z),
     +(?x_5,+(?y_5,s(+(?y,?y_10)))) = +(+(+(?x_5,?y_5),?y),s(?y_10)),
     +(?x_5,+(?y_5,+(?x_11,+(?y_11,?z)))) = +(+(+(?x_5,?y_5),+(?x_11,?y_11)),?z),
     +(?y,?z) = +(+(0,?y),?z),
     s(+(?x_3,+(?y,?z))) = +(+(s(?x_3),?y),?z),
     +(?x_5,+(?y_5,+(?y,?z))) = +(+(+(?x_5,?y_5),?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(+(?x_4,?z))) = +(+(?x,s(?x_4)),?z),
     +(?x,s(+(?y,?y_5))) = +(+(?x,?y),s(?y_5)),
     +(?x,+(?x_6,+(?y_6,?z))) = +(+(?x,+(?x_6,?y_6)),?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(+(?x_5,?z))) = +(?x_1,+(+(?x,s(?x_5)),?z)),
     +(+(?x_1,?x),s(+(?y,?y_6))) = +(?x_1,+(+(?x,?y),s(?y_6))),
     +(+(?x_1,?x),+(?x_7,+(?y_7,?z))) = +(?x_1,+(+(?x,+(?x_7,?y_7)),?z)),
     +(?x,+(+(+(?y,?y_7),?z_7),?z_6)) = +(+(+(?x,?y),+(?y_7,?z_7)),?z_6),
     +(?x,+(?z,?z_6)) = +(+(+(?x,0),?z),?z_6),
     +(?x,+(s(+(?x_10,?z)),?z_6)) = +(+(+(?x,s(?x_10)),?z),?z_6),
     +(?x,+(s(+(?y,?y_11)),?z_6)) = +(+(+(?x,?y),s(?y_11)),?z_6),
     +(?x,+(+(?x_12,+(?y_12,?z)),?z_6)) = +(+(+(?x,+(?x_12,?y_12)),?z),?z_6),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_6)) = +(+(+(?x,?y),?z),?z_6),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
     ?y = +(0,+(?y,0)),
     ?x = +(?x,+(0,0)),
     s(+(?x_4,?y)) = +(s(?x_4),+(?y,0)),
     s(+(?x,?y_5)) = +(?x,+(s(?y_5),0)),
     s(+(+(?x_5,+(?y_5,?y)),?y_4)) = +(+(?x_5,?y_5),+(?y,s(?y_4))),
     s(+(?y,?y_4)) = +(0,+(?y,s(?y_4))),
     s(+(?x,?y_4)) = +(?x,+(0,s(?y_4))),
     s(+(s(+(?x_8,?y)),?y_4)) = +(s(?x_8),+(?y,s(?y_4))),
     s(+(s(+(?x,?y_9)),?y_4)) = +(?x,+(s(?y_9),s(?y_4))),
     s(+(+(+(?x,?y_10),?z_10),?y_4)) = +(?x,+(+(?y_10,?z_10),s(?y_4))),
     +(+(+(?x_6,+(?y_6,?y)),?y_5),?z_5) = +(+(?x_6,?y_6),+(?y,+(?y_5,?z_5))),
     +(+(?y,?y_5),?z_5) = +(0,+(?y,+(?y_5,?z_5))),
     +(+(?x,?y_5),?z_5) = +(?x,+(0,+(?y_5,?z_5))),
     +(+(s(+(?x_9,?y)),?y_5),?z_5) = +(s(?x_9),+(?y,+(?y_5,?z_5))),
     +(+(s(+(?x,?y_10)),?y_5),?z_5) = +(?x,+(s(?y_10),+(?y_5,?z_5))),
     +(+(+(+(?x,?y_11),?z_11),?y_5),?z_5) = +(?x,+(+(?y_11,?z_11),+(?y_5,?z_5))),
     +(?x,?y) = +(?x,+(?y,0)),
     s(+(+(?x,?y),?y_4)) = +(?x,+(?y,s(?y_4))),
     +(+(+(?x,?y),?y_5),?z_5) = +(?x,+(?y,+(?y_5,?z_5))),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(?x,?z) = +(?x,+(0,?z)),
     +(s(+(?x_4,?y)),?z) = +(s(?x_4),+(?y,?z)),
     +(s(+(?x,?y_5)),?z) = +(?x,+(s(?y_5),?z)),
     +(+(+(?x,?y_6),?z_6),?z) = +(?x,+(+(?y_6,?z_6),?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1),
     +(s(+(?x_5,?y)),+(?z,?z_1)) = +(+(s(?x_5),+(?y,?z)),?z_1),
     +(s(+(?x,?y_6)),+(?z,?z_1)) = +(+(?x,+(s(?y_6),?z)),?z_1),
     +(+(+(?x,?y_7),?z_7),+(?z,?z_1)) = +(+(?x,+(+(?y_7,?z_7),?z)),?z_1),
     +(+(?x_6,+(?x_7,+(?y_7,?y))),?z) = +(?x_6,+(+(?x_7,?y_7),+(?y,?z))),
     +(+(?x_6,?x),?z) = +(?x_6,+(?x,+(0,?z))),
     +(+(?x_6,s(+(?x_10,?y))),?z) = +(?x_6,+(s(?x_10),+(?y,?z))),
     +(+(?x_6,s(+(?x,?y_11))),?z) = +(?x_6,+(?x,+(s(?y_11),?z))),
     +(+(?x_6,+(+(?x,?y_12),?z_12)),?z) = +(?x_6,+(?x,+(+(?y_12,?z_12),?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_6,+(?x,?y)),?z) = +(?x_6,+(?x,+(?y,?z))) ]
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(+(?x_2,?y_2))), +(+(?x_4,s(?x_2)),?y_2)> by Rules <2, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],5),([(+,2)],2)]>
 joinable by a reduction of rules <[([],3),([(s,1)],4)], [([(+,1)],3),([],2)]>
Critical Pair <+(?x_4,s(+(?x_3,?y_3))), +(+(?x_4,?x_3),s(?y_3))> by Rules <3, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([],3),([(s,1)],4)], [([],3)]>
 joinable by a reduction of rules <[], [([],5),([(+,2)],3)]>
 joinable by a reduction of rules <[([],3)], [([],3),([(s,1)],5)]>
Critical Pair <+(?x_4,+(?x_5,+(?y_5,?z_5))), +(+(?x_4,+(?x_5,?y_5)),?z_5)> by Rules <5, 4> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],4)], [([],5)]>
Critical Pair <+(?y,?z_5), +(0,+(?y,?z_5))> by Rules <0, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <+(?x_1,?z_5), +(?x_1,+(0,?z_5))> by Rules <1, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([(+,2)],0)]>
Critical Pair <+(s(+(?x_2,?y_2)),?z_5), +(s(?x_2),+(?y_2,?z_5))> by Rules <2, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([],2),([(s,1)],5)], [([],2)]>
 joinable by a reduction of rules <[], [([],4),([(+,1)],2)]>
 joinable by a reduction of rules <[([],2)], [([],2),([(s,1)],4)]>
Critical Pair <+(s(+(?x_3,?y_3)),?z_5), +(?x_3,+(s(?y_3),?z_5))> by Rules <3, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],4),([(+,1)],3)]>
 joinable by a reduction of rules <[([],2),([(s,1)],5)], [([(+,2)],2),([],3)]>
Critical Pair <+(+(+(?x_4,?y_4),?z_4),?z_5), +(?x_4,+(+(?y_4,?z_4),?z_5))> by Rules <4, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],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 <[([(+,2)],5)], [([],5)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <5, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],4)], [([],4)]>
Critical Pair <0, 0> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <s(+(0,?y_3)), s(?y_3)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], []>
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 <s(+(?x_2,0)), s(?x_2)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([(s,1)],1)], []>
Critical Pair <+(?x_5,+(?y_5,0)), +(?x_5,?y_5)> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([(+,2)],1)], []>
Critical Pair <s(+(s(?x_2),?y_3)), s(+(?x_2,s(?y_3)))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([(s,1)],2)], [([(s,1)],3)]>
Critical Pair <+(+(s(?x_2),?y_4),?z_4), s(+(?x_2,+(?y_4,?z_4)))> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([(+,1)],2),([],2)], [([(s,1)],4)]>
 joinable by a reduction of rules <[([],5),([],2)], []>
Critical Pair <+(?x_5,+(?y_5,s(?y_3))), s(+(+(?x_5,?y_5),?y_3))> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([(+,2)],3),([],3)], [([(s,1)],5)]>
 joinable by a reduction of rules <[([],4),([],3)], []>
Critical Pair <+(?x_5,+(?y_5,+(?y_4,?z_4))), +(+(+(?x_5,?y_5),?y_4),?z_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],4)], [([],5)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten +(?x_12,0) and ?x_12
strenghten +(0,0) and 0
strenghten s(+(?x_2,0)) and s(?x_2)
strenghten s(+(0,?y_3)) and s(?y_3)
strenghten s(+(0,0)) and s(0)
strenghten +(+(?x_12,0),0) and ?x_12
strenghten +(?x_1,+(0,?z_5)) and +(?x_1,?z_5)
strenghten +(?x_5,+(?y_5,0)) and +(?x_5,?y_5)
strenghten +(+(?x_4,?x_1),0) and +(?x_4,?x_1)
strenghten +(+(?x_4,0),?y) and +(?x_4,?y)
strenghten +(+(0,?y_4),?z_4) and +(?y_4,?z_4)
strenghten +(0,+(?y,?z_5)) and +(?y,?z_5)
strenghten s(+(?x_2,s(0))) and s(s(?x_2))
strenghten s(+(s(0),?y_3)) and s(s(?y_3))
strenghten s(+(?x_2,+(0,0))) and s(?x_2)
strenghten s(+(?x_2,s(?y_3))) and s(+(s(?x_2),?y_3))
strenghten +(?x_5,+(?y_5,s(0))) and s(+(?x_5,?y_5))
strenghten +(?x_8,+(s(0),?z_5)) and +(s(?x_8),?z_5)
strenghten +(+(?x_4,?x_8),s(0)) and +(?x_4,s(?x_8))
strenghten +(+(?x_4,0),s(?y_9)) and +(?x_4,s(?y_9))
strenghten +(+(?x_4,s(?x_10)),0) and +(?x_4,s(?x_10))
strenghten +(+(?x_4,s(0)),?y_11) and +(?x_4,s(?y_11))
strenghten +(+(s(0),?y_4),?z_4) and s(+(?y_4,?z_4))
strenghten +(0,+(s(?y_9),?z_5)) and +(s(?y_9),?z_5)
strenghten +(s(?x_10),+(0,?z_5)) and +(s(?x_10),?z_5)
strenghten +(s(0),+(?y_11,?z_5)) and +(s(?y_11),?z_5)
strenghten +(?x_5,+(?y_5,+(0,0))) and +(?x_5,?y_5)
strenghten +(?x_12,+(+(0,0),?z_5)) and +(?x_12,?z_5)
strenghten +(+(?x_4,?x_12),+(0,0)) and +(?x_4,?x_12)
strenghten +(?x_3,+(s(?y_3),?z_5)) and +(s(+(?x_3,?y_3)),?z_5)
strenghten +(+(?x_4,?x_3),s(?y_3)) and +(?x_4,s(+(?x_3,?y_3)))
strenghten +(+(?x_4,s(?x_2)),?y_2) and +(?x_4,s(+(?x_2,?y_2)))
strenghten +(s(?x_2),+(?y_2,?z_5)) and +(s(+(?x_2,?y_2)),?z_5)
strenghten s(+(?x_2,+(?y_4,?z_4))) and +(+(s(?x_2),?y_4),?z_4)
strenghten s(+(+(?x_5,?y_5),?y_3)) and +(?x_5,+(?y_5,s(?y_3)))
strenghten +(?x_4,+(+(?y_4,?z_4),?z_5)) and +(+(+(?x_4,?y_4),?z_4),?z_5)
strenghten +(+(?x,?y),+(?z,?z_1)) and +(+(?x,+(?y,?z)),?z_1)
strenghten +(+(?x_1,?x),+(?y,?z)) and +(?x_1,+(+(?x,?y),?z))
strenghten +(+(?x_4,+(?x_5,?y_5)),?z_5) and +(?x_4,+(?x_5,+(?y_5,?z_5)))
strenghten +(+(+(?x_5,?y_5),?y_4),?z_4) and +(?x_5,+(?y_5,+(?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
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?x,?y)) ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?y_3)), s(?y_3)> --> <s(?y_3), s(?y_3)> => yes
<s(+(?x_2,0)), s(?x_2)> --> <s(?x_2), s(?x_2)> => yes
<s(+(s(?x_2),?y_3)), s(+(?x_2,s(?y_3)))> --> <s(s(+(?x_2,?y_3))), s(s(+(?x_2,?y_3)))> => yes
PCP_in(symP,S):
CP(S,symP):
<+(?y,?z_1), +(0,+(?y,?z_1))> --> <+(?y,?z_1), +(?y,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?y), +(+(?x_1,0),?y)> --> <+(?x_1,?y), +(?x_1,?y)> => yes
<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,+(?y_1,?z_1))), +(+(s(?x),?y_1),?z_1)> --> <s(+(?x,+(?y_1,?z_1))), s(+(+(?x,?y_1),?z_1))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?x)),?y)> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
<s(+(+(?x_1,?y_1),?y)), +(?x_1,+(?y_1,s(?y)))> --> <s(+(+(?x_1,?y_1),?y)), s(+(?x_1,+(?y_1,?y)))> => yes
<+(s(+(?x,?y)),?z_1), +(?x,+(s(?y),?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?x),s(?y))> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
S:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?x,?y)) ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Success
Reduction-Preserving Completion
Direct Methods: CR

Final result: CR
138.trs: Success(CR)
(4411 msec.)