MAYBE
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_2,?x) = +(+(?x_2,?x),0),
     +(?x_2,s(+(?x_1,?y_1))) = +(+(?x_2,?x_1),s(?y_1)),
     +(?x_2,+(?x_3,+(?y_3,?z_3))) = +(+(?x_2,+(?x_3,?y_3)),?z_3),
     +(?x,?z_3) = +(?x,+(0,?z_3)),
     +(s(+(?x_1,?y_1)),?z_3) = +(?x_1,+(s(?y_1),?z_3)),
     +(+(+(?x_2,?y_2),?z_2),?z_3) = +(?x_2,+(+(?y_2,?z_2),?z_3)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?x_3,?y_3) = +(?x_3,+(?y_3,0)),
     s(+(+(?x_3,?y_3),?y_1)) = +(?x_3,+(?y_3,s(?y_1))),
     +(+(+(?x_3,?y_3),?y_2),?z_2) = +(?x_3,+(?y_3,+(?y_2,?z_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:
   [ +(?x_3,+(?y_3,0)) = +(?x_3,?y_3),
     +(+(?x_3,?x),0) = +(?x_3,?x),
     +(?x,+(0,?z_4)) = +(?x,?z_4),
     +(?x_3,+(?y_3,s(?y))) = s(+(+(?x_3,?y_3),?y)),
     +(+(?x_3,?x),s(?y)) = +(?x_3,s(+(?x,?y))),
     +(?x,+(s(?y),?z_4)) = +(s(+(?x,?y)),?z_4),
     +(?x_3,+(?y_3,+(+(?y,?y_4),?z_4))) = +(+(+(?x_3,?y_3),?y),+(?y_4,?z_4)),
     +(?x_3,+(?y_3,?y)) = +(+(+(?x_3,?y_3),?y),0),
     +(?x_3,+(?y_3,s(+(?y,?y_6)))) = +(+(+(?x_3,?y_3),?y),s(?y_6)),
     +(?x_3,+(?y_3,+(?x_7,+(?y_7,?z)))) = +(+(+(?x_3,?y_3),+(?x_7,?y_7)),?z),
     +(?x_3,+(?y_3,+(?y,?z))) = +(+(+(?x_3,?y_3),?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,?y) = +(+(?x,?y),0),
     +(?x,s(+(?y,?y_3))) = +(+(?x,?y),s(?y_3)),
     +(?x,+(?x_4,+(?y_4,?z))) = +(+(?x,+(?x_4,?y_4)),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),?y) = +(?x_1,+(+(?x,?y),0)),
     +(+(?x_1,?x),s(+(?y,?y_4))) = +(?x_1,+(+(?x,?y),s(?y_4))),
     +(+(?x_1,?x),+(?x_5,+(?y_5,?z))) = +(?x_1,+(+(?x,+(?x_5,?y_5)),?z)),
     +(?x,+(+(+(?y,?y_5),?z_5),?z_4)) = +(+(+(?x,?y),+(?y_5,?z_5)),?z_4),
     +(?x,+(?y,?z_4)) = +(+(+(?x,?y),0),?z_4),
     +(?x,+(s(+(?y,?y_7)),?z_4)) = +(+(+(?x,?y),s(?y_7)),?z_4),
     +(?x,+(+(?x_8,+(?y_8,?z)),?z_4)) = +(+(+(?x,+(?x_8,?y_8)),?z),?z_4),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_4)) = +(+(+(?x,?y),?z),?z_4),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
     ?x = +(?x,+(0,0)),
     s(+(?x,?y_3)) = +(?x,+(s(?y_3),0)),
     s(+(+(?x_3,+(?y_3,?y)),?y_2)) = +(+(?x_3,?y_3),+(?y,s(?y_2))),
     s(+(?x,?y_2)) = +(?x,+(0,s(?y_2))),
     s(+(s(+(?x,?y_5)),?y_2)) = +(?x,+(s(?y_5),s(?y_2))),
     s(+(+(+(?x,?y_6),?z_6),?y_2)) = +(?x,+(+(?y_6,?z_6),s(?y_2))),
     +(+(+(?x_4,+(?y_4,?y)),?y_3),?z_3) = +(+(?x_4,?y_4),+(?y,+(?y_3,?z_3))),
     +(+(?x,?y_3),?z_3) = +(?x,+(0,+(?y_3,?z_3))),
     +(+(s(+(?x,?y_6)),?y_3),?z_3) = +(?x,+(s(?y_6),+(?y_3,?z_3))),
     +(+(+(+(?x,?y_7),?z_7),?y_3),?z_3) = +(?x,+(+(?y_7,?z_7),+(?y_3,?z_3))),
     +(?x,?y) = +(?x,+(?y,0)),
     s(+(+(?x,?y),?y_2)) = +(?x,+(?y,s(?y_2))),
     +(+(+(?x,?y),?y_3),?z_3) = +(?x,+(?y,+(?y_3,?z_3))),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?x,?z) = +(?x,+(0,?z)),
     +(s(+(?x,?y_3)),?z) = +(?x,+(s(?y_3),?z)),
     +(+(+(?x,?y_4),?z_4),?z) = +(?x,+(+(?y_4,?z_4),?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,?y_4)),+(?z,?z_1)) = +(+(?x,+(s(?y_4),?z)),?z_1),
     +(+(+(?x,?y_5),?z_5),+(?z,?z_1)) = +(+(?x,+(+(?y_5,?z_5),?z)),?z_1),
     +(+(?x_4,+(?x_5,+(?y_5,?y))),?z) = +(?x_4,+(+(?x_5,?y_5),+(?y,?z))),
     +(+(?x_4,?x),?z) = +(?x_4,+(?x,+(0,?z))),
     +(+(?x_4,s(+(?x,?y_7))),?z) = +(?x_4,+(?x,+(s(?y_7),?z))),
     +(+(?x_4,+(+(?x,?y_8),?z_8)),?z) = +(?x_4,+(?x,+(+(?y_8,?z_8),?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_4,+(?x,?y)),?z) = +(?x_4,+(?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_2,?x), +(+(?x_2,?x),0)> by Rules <0, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <+(?x_2,s(+(?x_1,?y_1))), +(+(?x_2,?x_1),s(?y_1))> by Rules <1, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([],1),([(s,1)],2)], [([],1)]>
 joinable by a reduction of rules <[], [([],3),([(+,2)],1)]>
 joinable by a reduction of rules <[([],1)], [([],1),([(s,1)],3)]>
Critical Pair <+(?x_2,+(?x_3,+(?y_3,?z_3))), +(+(?x_2,+(?x_3,?y_3)),?z_3)> by Rules <3, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],2)], [([],3)]>
Critical Pair <+(?x,?z_3), +(?x,+(0,?z_3))> by Rules <0, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],2),([(+,1)],0)]>
Critical Pair <+(s(+(?x_1,?y_1)),?z_3), +(?x_1,+(s(?y_1),?z_3))> by Rules <1, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],2),([(+,1)],1)]>
Critical Pair <+(+(+(?x_2,?y_2),?z_2),?z_3), +(?x_2,+(+(?y_2,?z_2),?z_3))> by Rules <2, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],3)], [([],2)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <2, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],3)], [([],3)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <3, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],2)], [([],2)]>
Critical Pair <+(?x_3,+(?y_3,0)), +(?x_3,?y_3)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([(+,2)],0)], []>
Critical Pair <+(?x_3,+(?y_3,s(?y_1))), s(+(+(?x_3,?y_3),?y_1))> by Rules <3, 1> preceded by []
 joinable by a reduction of rules <[([(+,2)],1),([],1)], [([(s,1)],3)]>
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <+(?x_3,+(?y_3,+(?y_2,?z_2))), +(+(+(?x_3,?y_3),?y_2),?z_2)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([],2)], [([],3)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 14 rules by 3 steps unfolding
strenghten +(?x,0) and ?x
strenghten s(+(?x_5,0)) and s(?x_5)
strenghten +(?x_11,+(0,0)) and ?x_11
strenghten +(+(?x_6,0),0) and ?x_6
strenghten +(?x,+(0,?z_3)) and +(?x,?z_3)
strenghten +(?x_3,+(?y_3,0)) and +(?x_3,?y_3)
strenghten +(+(?x_2,?x),0) and +(?x_2,?x)
strenghten +(?x_3,+(?y_3,s(0))) and s(+(?x_3,?y_3))
strenghten +(?x_5,+(s(0),?z_3)) and +(s(?x_5),?z_3)
strenghten +(+(?x_2,?x_5),s(0)) and +(?x_2,s(?x_5))
strenghten +(?x_3,+(?y_3,+(0,0))) and +(?x_3,?y_3)
strenghten +(?x_6,+(+(0,0),?z_3)) and +(?x_6,?z_3)
strenghten +(+(?x_2,?x_6),+(0,0)) and +(?x_2,?x_6)
strenghten +(+(?x_2,+(?x_11,0)),0) and +(?x_2,?x_11)
strenghten +(+(?x_11,0),+(0,?z_3)) and +(?x_11,?z_3)
strenghten +(?x_1,+(s(?y_1),?z_3)) and +(s(+(?x_1,?y_1)),?z_3)
strenghten +(+(?x_2,?x_1),s(?y_1)) and +(?x_2,s(+(?x_1,?y_1)))
strenghten s(+(+(?x_3,?y_3),?y_1)) and +(?x_3,+(?y_3,s(?y_1)))
strenghten +(?x_2,+(+(?y_2,?z_2),?z_3)) and +(+(+(?x_2,?y_2),?z_2),?z_3)
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_2,+(?x_3,?y_3)),?z_3) and +(?x_2,+(?x_3,+(?y_3,?z_3)))
strenghten +(+(+(?x_3,?y_3),?y_2),?z_2) and +(?x_3,+(?y_3,+(?y_2,?z_2)))
obtain 71 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:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(?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,+(0,?z_1))> => no
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => 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), +(?x,+(s(?y),?z_1))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?x),s(?y))> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
check joinability condition:
check modulo reachablity from +(?x,?z_1) to +(?x,+(0,?z_1)): maybe not reachable
check modulo reachablity from +(s(+(?x,?y)),?z_1) to +(?x,+(s(?y),?z_1)): maybe not reachable
failed
failure(Step 1)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(?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,+(0,?z_1))> => no
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => 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), +(?x,+(s(?y),?z_1))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?x),s(?y))> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
check joinability condition:
check modulo reachablity from +(?x,?z_1) to +(?x,+(0,?z_1)): maybe not reachable
check modulo reachablity from +(s(+(?x,?y)),?z_1) to +(?x,+(s(?y),?z_1)): maybe not reachable
failed
failure(Step 2)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (15)
  s:= (1)*x1
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= 0
  s:= (4)+(1)*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Sort Assignment:
 + : 16*16=>16
 0 : =>16
 s : 16=>16
maximal types: {16}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Outside Critical Pair: <+(?x_3,+(?y_3,0)), +(?x_3,?y_3)> by Rules <3, 0>
develop reducts from lhs term...
<{2}, +(+(?x_3,?y_3),0)>
<{0}, +(?x_3,?y_3)>
<{}, +(?x_3,+(?y_3,0))>
develop reducts from rhs term...
<{}, +(?x_3,?y_3)>
Outside Critical Pair: <+(?x_3,+(?y_3,s(?y_1))), s(+(+(?x_3,?y_3),?y_1))> by Rules <3, 1>
develop reducts from lhs term...
<{2}, +(+(?x_3,?y_3),s(?y_1))>
<{1}, +(?x_3,s(+(?y_3,?y_1)))>
<{}, +(?x_3,+(?y_3,s(?y_1)))>
develop reducts from rhs term...
<{3}, s(+(?x_3,+(?y_3,?y_1)))>
<{}, s(+(+(?x_3,?y_3),?y_1))>
Outside Critical Pair: <+(?x_3,+(?y_3,+(?y_2,?z_2))), +(+(+(?x_3,?y_3),?y_2),?z_2)> by Rules <3, 2>
develop reducts from lhs term...
<{2}, +(+(?x_3,?y_3),+(?y_2,?z_2))>
<{2}, +(?x_3,+(+(?y_3,?y_2),?z_2))>
<{}, +(?x_3,+(?y_3,+(?y_2,?z_2)))>
develop reducts from rhs term...
<{3}, +(+(?x_3,?y_3),+(?y_2,?z_2))>
<{3}, +(+(?x_3,+(?y_3,?y_2)),?z_2)>
<{}, +(+(+(?x_3,?y_3),?y_2),?z_2)>
Inside Critical Pair: <+(?x_2,?x), +(+(?x_2,?x),0)> by Rules <0, 2>
develop reducts from lhs term...
<{}, +(?x_2,?x)>
develop reducts from rhs term...
<{3}, +(?x_2,+(?x,0))>
<{0}, +(?x_2,?x)>
<{}, +(+(?x_2,?x),0)>
Inside Critical Pair: <+(?x_2,s(+(?x_1,?y_1))), +(+(?x_2,?x_1),s(?y_1))> by Rules <1, 2>
develop reducts from lhs term...
<{1}, s(+(?x_2,+(?x_1,?y_1)))>
<{}, +(?x_2,s(+(?x_1,?y_1)))>
develop reducts from rhs term...
<{3}, +(?x_2,+(?x_1,s(?y_1)))>
<{1}, s(+(+(?x_2,?x_1),?y_1))>
<{}, +(+(?x_2,?x_1),s(?y_1))>
Inside Critical Pair: <+(?x_2,+(?x_3,+(?y_3,?z_3))), +(+(?x_2,+(?x_3,?y_3)),?z_3)> by Rules <3, 2>
develop reducts from lhs term...
<{2}, +(+(?x_2,?x_3),+(?y_3,?z_3))>
<{2}, +(?x_2,+(+(?x_3,?y_3),?z_3))>
<{}, +(?x_2,+(?x_3,+(?y_3,?z_3)))>
develop reducts from rhs term...
<{3}, +(?x_2,+(+(?x_3,?y_3),?z_3))>
<{2}, +(+(+(?x_2,?x_3),?y_3),?z_3)>
<{}, +(+(?x_2,+(?x_3,?y_3)),?z_3)>
Inside Critical Pair: <+(?x,?z_3), +(?x,+(0,?z_3))> by Rules <0, 3>
develop reducts from lhs term...
<{}, +(?x,?z_3)>
develop reducts from rhs term...
<{2}, +(+(?x,0),?z_3)>
<{}, +(?x,+(0,?z_3))>
Inside Critical Pair: <+(s(+(?x_1,?y_1)),?z_3), +(?x_1,+(s(?y_1),?z_3))> by Rules <1, 3>
develop reducts from lhs term...
<{}, +(s(+(?x_1,?y_1)),?z_3)>
develop reducts from rhs term...
<{2}, +(+(?x_1,s(?y_1)),?z_3)>
<{}, +(?x_1,+(s(?y_1),?z_3))>
Inside Critical Pair: <+(+(+(?x_2,?y_2),?z_2),?z_3), +(?x_2,+(+(?y_2,?z_2),?z_3))> by Rules <2, 3>
develop reducts from lhs term...
<{3}, +(+(?x_2,?y_2),+(?z_2,?z_3))>
<{3}, +(+(?x_2,+(?y_2,?z_2)),?z_3)>
<{}, +(+(+(?x_2,?y_2),?z_2),?z_3)>
develop reducts from rhs term...
<{2}, +(+(?x_2,+(?y_2,?z_2)),?z_3)>
<{3}, +(?x_2,+(?y_2,+(?z_2,?z_3)))>
<{}, +(?x_2,+(+(?y_2,?z_2),?z_3))>
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
160.trs: Failure(unknown)
(5397 msec.)