MAYBE
(ignored inputs)COMMENT there are no composable subsystems
Rewrite Rules:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(0,?x) -> ?x,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ ++(++(++(?x_2,?y_2),?z_2),?z_1) = ++(?x_2,++(++(?y_2,?z_2),?z_1)),
     ++(?x_3,?z_1) = ++(0,++(?x_3,?z_1)),
     ++(?x_2,++(?x_1,++(?y_1,?z_1))) = ++(++(?x_2,++(?x_1,?y_1)),?z_1),
     ++(?x_2,?x_3) = ++(++(?x_2,0),?x_3),
     +(+(?y_4,?x_4),?z_5) = +(?x_4,+(?y_4,?z_5)),
     +(?x_6,?z_5) = +(0,+(?x_6,?z_5)),
     +(s(+(?x_7,?y_7)),?z_5) = +(s(?x_7),+(?y_7,?z_5)),
     ++(++(?x,++(?y,?z)),?z_1) = ++(++(?x,?y),++(?z,?z_1)),
     ++(?x_1,++(++(?x,?y),?z)) = ++(++(?x_1,?x),++(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ ++(?x_1,++(?y_1,++(?y_2,?z_2))) = ++(++(++(?x_1,?y_1),?y_2),?z_2),
     ++(++(0,?y_2),?z_2) = ++(?y_2,?z_2),
     +(?y_4,+(?x_5,?y_5)) = +(?x_5,+(?y_5,?y_4)),
     +(?y_4,0) = ?y_4,
     +(?y_4,s(?x_7)) = s(+(?x_7,?y_4)) ]
not Overlay, check Termination...
unknown/not 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:
   [ ++(++(++(?x_3,++(?y_3,?y)),?y_2),?z_2) = ++(++(?x_3,?y_3),++(?y,++(?y_2,?z_2))),
     ++(++(++(++(?x,?y_5),?z_5),?y_2),?z_2) = ++(?x,++(++(?y_5,?z_5),++(?y_2,?z_2))),
     ++(++(?y,?y_2),?z_2) = ++(0,++(?y,++(?y_2,?z_2))),
     ++(++(++(?x,?y),?y_2),?z_2) = ++(?x,++(?y,++(?y_2,?z_2))),
     ++(++(?x_1,++(?y_1,?y)),?z) = ++(++(?x_1,?y_1),++(?y,?z)),
     ++(++(++(?x,?y_3),?z_3),?z) = ++(?x,++(++(?y_3,?z_3),?z)),
     ++(?y,?z) = ++(0,++(?y,?z)),
     ++(++(?x_2,++(?y_2,?y)),++(?z,?z_1)) = ++(++(++(?x_2,?y_2),++(?y,?z)),?z_1),
     ++(++(++(?x,?y_4),?z_4),++(?z,?z_1)) = ++(++(?x,++(++(?y_4,?z_4),?z)),?z_1),
     ++(?y,++(?z,?z_1)) = ++(++(0,++(?y,?z)),?z_1),
     ++(++(?x_3,++(?x_4,++(?y_4,?y))),?z) = ++(?x_3,++(++(?x_4,?y_4),++(?y,?z))),
     ++(++(?x_3,++(++(?x,?y_6),?z_6)),?z) = ++(?x_3,++(?x,++(++(?y_6,?z_6),?z))),
     ++(++(?x_3,?y),?z) = ++(?x_3,++(0,++(?y,?z))),
     ++(++(?x,?y),++(?z,?z_1)) = ++(++(?x,++(?y,?z)),?z_1),
     ++(++(?x_3,++(?x,?y)),?z) = ++(?x_3,++(?x,++(?y,?z))),
     ++(?x_2,++(?y_2,++(++(?y,?y_3),?z_3))) = ++(++(++(?x_2,?y_2),?y),++(?y_3,?z_3)),
     ++(?x_2,++(?y_2,++(?x_5,++(?y_5,?z)))) = ++(++(++(?x_2,?y_2),++(?x_5,?y_5)),?z),
     ++(?x_2,++(?y_2,?z)) = ++(++(++(?x_2,?y_2),0),?z),
     ++(++(?y,?y_1),?z_1) = ++(++(0,?y),++(?y_1,?z_1)),
     ?z = ++(++(0,0),?z),
     ++(?x_2,++(?y_2,++(?y,?z))) = ++(++(++(?x_2,?y_2),?y),?z),
     ++(?y,?z) = ++(++(0,?y),?z),
     ++(?x,++(++(?y,?y_1),?z_1)) = ++(++(?x,?y),++(?y_1,?z_1)),
     ++(?x,++(?x_3,++(?y_3,?z))) = ++(++(?x,++(?x_3,?y_3)),?z),
     ++(?x,?z) = ++(++(?x,0),?z),
     ++(++(?x_1,?x),++(++(?y,?y_2),?z_2)) = ++(?x_1,++(++(?x,?y),++(?y_2,?z_2))),
     ++(++(?x_1,?x),++(?x_4,++(?y_4,?z))) = ++(?x_1,++(++(?x,++(?x_4,?y_4)),?z)),
     ++(++(?x_1,?x),?z) = ++(?x_1,++(++(?x,0),?z)),
     ++(?x,++(++(++(?y,?y_4),?z_4),?z_3)) = ++(++(++(?x,?y),++(?y_4,?z_4)),?z_3),
     ++(?x,++(++(?x_6,++(?y_6,?z)),?z_3)) = ++(++(++(?x,++(?x_6,?y_6)),?z),?z_3),
     ++(?x,++(?z,?z_3)) = ++(++(++(?x,0),?z),?z_3),
     ++(++(?x_1,?x),++(?y,?z)) = ++(?x_1,++(++(?x,?y),?z)),
     ++(?x,++(++(?y,?z),?z_3)) = ++(++(++(?x,?y),?z),?z_3),
     ++(++(0,?y_3),?z_3) = ++(?y_3,?z_3),
     ++(0,++(?x,?z_3)) = ++(?x,?z_3),
     ++(++(?x_4,0),?x) = ++(?x_4,?x),
     +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)),
     ?y = +(?y,0),
     s(+(?x_7,?y)) = +(?y,s(?x_7)),
     +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,s(+(?x_8,?y))) = +(s(?x_8),+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(s(+(?x_8,?y)),?z) = +(s(?x_8),+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(s(+(?x_9,?y)),+(?z,?z_1)) = +(+(s(?x_9),+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?x,0) = ?x,
     +(0,+(?x,?z_7)) = +(?x,?z_7),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_7)) = +(s(+(?x,?y)),?z_7) ]
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,?y_2),?z_2),?z_1), ++(?x_2,++(++(?y_2,?z_2),?z_1))> by Rules <2, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[([(++,1)],1)], [([],2)]>
Critical Pair <++(?x_3,?z_1), ++(0,++(?x_3,?z_1))> by Rules <3, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <++(?x_2,++(?x_1,++(?y_1,?z_1))), ++(++(?x_2,++(?x_1,?y_1)),?z_1)> by Rules <1, 2> preceded by [(++,2)]
 joinable by a reduction of rules <[([(++,2)],2)], [([],1)]>
Critical Pair <++(?x_2,?x_3), ++(++(?x_2,0),?x_3)> by Rules <3, 2> preceded by [(++,2)]
 joinable by a reduction of rules <[], [([],1),([(++,2)],3)]>
Critical Pair <+(+(?y_4,?x_4),?z_5), +(?x_4,+(?y_4,?z_5))> by Rules <4, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],4),([],5)], []>
 joinable by a reduction of rules <[([],5),([(+,2)],4)], [([],4),([],5)]>
Critical Pair <+(?x_6,?z_5), +(0,+(?x_6,?z_5))> by Rules <6, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],6)]>
Critical Pair <+(s(+(?x_7,?y_7)),?z_5), +(s(?x_7),+(?y_7,?z_5))> by Rules <7, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([],7),([(s,1)],5)], [([],7)]>
Critical Pair <++(++(?x,++(?y,?z)),?z_1), ++(++(?x,?y),++(?z,?z_1))> by Rules <1, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[([(++,1)],2)], [([],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)],1)], [([],1)]>
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 <[([],5),([(+,2)],5)], [([],5)]>
Critical Pair <++(++(++(?x_1,?y_1),?y_2),?z_2), ++(?x_1,++(?y_1,++(?y_2,?z_2)))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],1)], [([],2)]>
Critical Pair <++(?y_2,?z_2), ++(++(0,?y_2),?z_2)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([(++,1)],3)]>
Critical Pair <+(?x_5,+(?y_5,?z_5)), +(?z_5,+(?x_5,?y_5))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[], [([],4),([],5)]>
Critical Pair <?x_6, +(?x_6,0)> by Rules <6, 4> preceded by []
 joinable by a reduction of rules <[], [([],4),([],6)]>
Critical Pair <s(+(?x_7,?y_7)), +(?y_7,s(?x_7))> by Rules <7, 4> preceded by []
 joinable by a reduction of rules <[], [([],4),([],7)]>
unknown Diagram Decreasing
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x_1,?y_1),?z_1) -> ++(?x_1,++(?y_1,?z_1)),
     ++(?x_2,++(?y_2,?z_2)) -> ++(++(?x_2,?y_2),?z_2),
     ++(0,?x_3) -> ?x_3,
     +(?x_4,?y_4) -> +(?y_4,?x_4),
     +(+(?x_5,?y_5),?z_5) -> +(?x_5,+(?y_5,?z_5)),
     +(0,?x_6) -> ?x_6,
     +(s(?x_7),?y_7) -> s(+(?x_7,?y_7)) ]
Sort Assignment:
 + : 23*23=>23
 0 : =>23
 e : 23=>23
 s : 23=>23
 ++ : 23*23=>23
non-linear variables: {?x}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x_1,?y_1),?z_1) -> ++(?x_1,++(?y_1,?z_1)),
     ++(?x_2,++(?y_2,?z_2)) -> ++(++(?x_2,?y_2),?z_2),
     ++(0,?x_3) -> ?x_3,
     +(?x_4,?y_4) -> +(?y_4,?x_4),
     +(+(?x_5,?y_5),?z_5) -> +(?x_5,+(?y_5,?z_5)),
     +(0,?x_6) -> ?x_6,
     +(s(?x_7),?y_7) -> s(+(?x_7,?y_7)) ]
NLR:
0: {0,1,2,3,4,5,6,7}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x_1,?y_1),?z_1) -> ++(?x_1,++(?y_1,?z_1)),
     ++(?x_2,++(?y_2,?z_2)) -> ++(++(?x_2,?y_2),?z_2),
     ++(0,?x_3) -> ?x_3,
     +(?x_4,?y_4) -> +(?y_4,?x_4),
     +(+(?x_5,?y_5),?z_5) -> +(?x_5,+(?y_5,?z_5)),
     +(0,?x_6) -> ?x_6,
     +(s(?x_7),?y_7) -> s(+(?x_7,?y_7)) ]
Sort Assignment:
 + : 23*23=>23
 0 : =>23
 e : 23=>23
 s : 23=>23
 ++ : 23*23=>23
non-linear variables: {?x}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x_1,?y_1),?z_1) -> ++(?x_1,++(?y_1,?z_1)),
     ++(?x_2,++(?y_2,?z_2)) -> ++(++(?x_2,?y_2),?z_2),
     ++(0,?x_3) -> ?x_3,
     +(?x_4,?y_4) -> +(?y_4,?x_4),
     +(+(?x_5,?y_5),?z_5) -> +(?x_5,+(?y_5,?z_5)),
     +(0,?x_6) -> ?x_6,
     +(s(?x_7),?y_7) -> s(+(?x_7,?y_7)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 18 rules by 3 steps unfolding
strenghten +(?x_6,0) and ?x_6
strenghten +(0,?x_8) and ?x_8
strenghten +(?x_14,?y_14) and +(?y_14,?x_14)
strenghten e(+(0,0)) and e(0)
strenghten s(+(?x_7,0)) and s(?x_7)
strenghten ++(0,e(0)) and e(0)
strenghten +(?y_7,s(?x_7)) and s(+(?x_7,?y_7))
strenghten e(+(0,0)) and ++(0,e(0))
strenghten s(+(?x_7,?y_13)) and +(s(?x_7),?y_13)
strenghten s(+(?x_7,?y_14)) and +(?y_14,s(?x_7))
strenghten +(?x_5,+(?y_5,0)) and +(?x_5,?y_5)
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:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z) ]
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
not relatively terminatiing
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: unknown termination
failure(Step 1)
STEP: 2 (linear)
S:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: not linear
failure(Step 2)
STEP: 3 (relative)
S:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
not relatively terminatiing
S/P: unknown relative termination
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

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

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

Try Commutative Decomposition for...
   [ e(?x) -> ++(?x,e(+(?x,?x))),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(0,?x) -> ?x,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Outside Critical Pair: <++(++(++(?x_1,?y_1),?y_2),?z_2), ++(?x_1,++(?y_1,++(?y_2,?z_2)))> by Rules <2, 1>
develop reducts from lhs term...
<{1}, ++(++(?x_1,?y_1),++(?y_2,?z_2))>
<{1}, ++(++(?x_1,++(?y_1,?y_2)),?z_2)>
<{}, ++(++(++(?x_1,?y_1),?y_2),?z_2)>
develop reducts from rhs term...
<{2}, ++(++(?x_1,?y_1),++(?y_2,?z_2))>
<{2}, ++(?x_1,++(++(?y_1,?y_2),?z_2))>
<{}, ++(?x_1,++(?y_1,++(?y_2,?z_2)))>
Outside Critical Pair: <++(?y_2,?z_2), ++(++(0,?y_2),?z_2)> by Rules <3, 2>
develop reducts from lhs term...
<{}, ++(?y_2,?z_2)>
develop reducts from rhs term...
<{1}, ++(0,++(?y_2,?z_2))>
<{3}, ++(?y_2,?z_2)>
<{}, ++(++(0,?y_2),?z_2)>
Outside Critical Pair: <+(?x_5,+(?y_5,?z_5)), +(?z_5,+(?x_5,?y_5))> by Rules <5, 4>
develop reducts from lhs term...
<{4}, +(+(?z_5,?y_5),?x_5)>
<{4}, +(+(?y_5,?z_5),?x_5)>
<{4}, +(?x_5,+(?z_5,?y_5))>
<{}, +(?x_5,+(?y_5,?z_5))>
develop reducts from rhs term...
<{4}, +(+(?y_5,?x_5),?z_5)>
<{4}, +(+(?x_5,?y_5),?z_5)>
<{4}, +(?z_5,+(?y_5,?x_5))>
<{}, +(?z_5,+(?x_5,?y_5))>
Outside Critical Pair: <?x_6, +(?x_6,0)> by Rules <6, 4>
develop reducts from lhs term...
<{}, ?x_6>
develop reducts from rhs term...
<{4}, +(0,?x_6)>
<{}, +(?x_6,0)>
Outside Critical Pair: <s(+(?x_7,?y_7)), +(?y_7,s(?x_7))> by Rules <7, 4>
develop reducts from lhs term...
<{4}, s(+(?y_7,?x_7))>
<{}, s(+(?x_7,?y_7))>
develop reducts from rhs term...
<{4}, +(s(?x_7),?y_7)>
<{}, +(?y_7,s(?x_7))>
Inside Critical Pair: <++(++(++(?x_2,?y_2),?z_2),?z_1), ++(?x_2,++(++(?y_2,?z_2),?z_1))> by Rules <2, 1>
develop reducts from lhs term...
<{1}, ++(++(?x_2,?y_2),++(?z_2,?z_1))>
<{1}, ++(++(?x_2,++(?y_2,?z_2)),?z_1)>
<{}, ++(++(++(?x_2,?y_2),?z_2),?z_1)>
develop reducts from rhs term...
<{2}, ++(++(?x_2,++(?y_2,?z_2)),?z_1)>
<{1}, ++(?x_2,++(?y_2,++(?z_2,?z_1)))>
<{}, ++(?x_2,++(++(?y_2,?z_2),?z_1))>
Inside Critical Pair: <++(?x_3,?z_1), ++(0,++(?x_3,?z_1))> by Rules <3, 1>
develop reducts from lhs term...
<{}, ++(?x_3,?z_1)>
develop reducts from rhs term...
<{3}, ++(?x_3,?z_1)>
<{2}, ++(++(0,?x_3),?z_1)>
<{}, ++(0,++(?x_3,?z_1))>
Inside Critical Pair: <++(?x_2,++(?x_1,++(?y_1,?z_1))), ++(++(?x_2,++(?x_1,?y_1)),?z_1)> by Rules <1, 2>
develop reducts from lhs term...
<{2}, ++(++(?x_2,?x_1),++(?y_1,?z_1))>
<{2}, ++(?x_2,++(++(?x_1,?y_1),?z_1))>
<{}, ++(?x_2,++(?x_1,++(?y_1,?z_1)))>
develop reducts from rhs term...
<{1}, ++(?x_2,++(++(?x_1,?y_1),?z_1))>
<{2}, ++(++(++(?x_2,?x_1),?y_1),?z_1)>
<{}, ++(++(?x_2,++(?x_1,?y_1)),?z_1)>
Inside Critical Pair: <++(?x_2,?x_3), ++(++(?x_2,0),?x_3)> by Rules <3, 2>
develop reducts from lhs term...
<{}, ++(?x_2,?x_3)>
develop reducts from rhs term...
<{1}, ++(?x_2,++(0,?x_3))>
<{}, ++(++(?x_2,0),?x_3)>
Inside Critical Pair: <+(+(?y_4,?x_4),?z_5), +(?x_4,+(?y_4,?z_5))> by Rules <4, 5>
develop reducts from lhs term...
<{5}, +(?y_4,+(?x_4,?z_5))>
<{4}, +(?z_5,+(?x_4,?y_4))>
<{4}, +(?z_5,+(?y_4,?x_4))>
<{4}, +(+(?x_4,?y_4),?z_5)>
<{}, +(+(?y_4,?x_4),?z_5)>
develop reducts from rhs term...
<{4}, +(+(?z_5,?y_4),?x_4)>
<{4}, +(+(?y_4,?z_5),?x_4)>
<{4}, +(?x_4,+(?z_5,?y_4))>
<{}, +(?x_4,+(?y_4,?z_5))>
Inside Critical Pair: <+(?x_6,?z_5), +(0,+(?x_6,?z_5))> by Rules <6, 5>
develop reducts from lhs term...
<{4}, +(?z_5,?x_6)>
<{}, +(?x_6,?z_5)>
develop reducts from rhs term...
<{4,6}, +(?z_5,?x_6)>
<{6}, +(?x_6,?z_5)>
<{4}, +(+(?z_5,?x_6),0)>
<{4}, +(+(?x_6,?z_5),0)>
<{4}, +(0,+(?z_5,?x_6))>
<{}, +(0,+(?x_6,?z_5))>
Inside Critical Pair: <+(s(+(?x_7,?y_7)),?z_5), +(s(?x_7),+(?y_7,?z_5))> by Rules <7, 5>
develop reducts from lhs term...
<{4,7}, s(+(+(?y_7,?x_7),?z_5))>
<{7}, s(+(+(?x_7,?y_7),?z_5))>
<{4}, +(?z_5,s(+(?y_7,?x_7)))>
<{4}, +(?z_5,s(+(?x_7,?y_7)))>
<{4}, +(s(+(?y_7,?x_7)),?z_5)>
<{}, +(s(+(?x_7,?y_7)),?z_5)>
develop reducts from rhs term...
<{4,7}, s(+(?x_7,+(?z_5,?y_7)))>
<{7}, s(+(?x_7,+(?y_7,?z_5)))>
<{4}, +(+(?z_5,?y_7),s(?x_7))>
<{4}, +(+(?y_7,?z_5),s(?x_7))>
<{4}, +(s(?x_7),+(?z_5,?y_7))>
<{}, +(s(?x_7),+(?y_7,?z_5))>
Try A Minimal Decomposition {2,3}{5,7,4,6}{0}{1}
{2,3}
(cm)Rewrite Rules:
   [ ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ ++(?x,?x_1) = ++(++(?x,0),?x_1),
     ++(?x_1,++(++(?x,?y),?z)) = ++(++(?x_1,?x),++(?y,?z)) ]
Outer CPs:
   [ ++(++(0,?y),?z) = ++(?y,?z) ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR
{5,7,4,6}
(cm)Rewrite Rules:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,?y) -> +(?y,?x),
     +(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ +(s(+(?x_1,?y_1)),?z) = +(s(?x_1),+(?y_1,?z)),
     +(+(?y_2,?x_2),?z) = +(?x_2,+(?y_2,?z)),
     +(?x_3,?z) = +(0,+(?x_3,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?x,+(?y,?z)) = +(?z,+(?x,?y)),
     s(+(?x_1,?y_1)) = +(?y_1,s(?x_1)),
     +(?y_2,0) = ?y_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,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,s(+(?x_2,?y))) = +(s(?x_2),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(s(+(?x_2,?y)),?z) = +(s(?x_2),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(s(+(?x_3,?y)),+(?z,?z_1)) = +(+(s(?x_3),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_2)) = +(s(+(?x,?y)),?z_2),
     +(?x_1,+(?y_1,?y)) = +(?y,+(?x_1,?y_1)),
     s(+(?x_2,?y)) = +(?y,s(?x_2)),
     ?y = +(?y,0),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(?x,0) = ?x,
     +(0,+(?x,?z_2)) = +(?x,?z_2) ]
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(+(?x_1,?y_1)),?z), +(s(?x_1),+(?y_1,?z))> by Rules <1, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([],1),([(s,1)],0)], [([],1)]>
Critical Pair <+(+(?y_2,?x_2),?z), +(?x_2,+(?y_2,?z))> by Rules <2, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(+,2)],2)], [([],2),([],0)]>
Critical Pair <+(?x_3,?z), +(0,+(?x_3,?z))> by Rules <3, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <0, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([],0),([(+,2)],0)], [([],0)]>
Critical Pair <+(?y_2,+(?x,?y)), +(?x,+(?y,?y_2))> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <+(?y_2,s(?x_1)), s(+(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, +(?x_3,0)> 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_3,0) and ?x_3
strenghten +(0,?x_4) and ?x_4
strenghten +(?x_9,?y_9) and +(?y_9,?x_9)
strenghten +(?x_12,s(0)) and s(?x_12)
strenghten +(s(0),?x_12) and s(?x_12)
strenghten s(+(?x_1,0)) and s(?x_1)
strenghten s(+(?x_1,?x_10)) and +(?x_10,s(?x_1))
strenghten s(+(?x_1,?x_11)) and +(s(?x_1),?x_11)
strenghten +(?x,+(?y,0)) and +(?x,?y)
strenghten +(?x_4,+(0,?z)) and +(?x_4,?z)
strenghten +(0,+(?x_3,?z)) and +(?x_3,?z)
strenghten s(+(?x_1,s(0))) and s(s(?x_1))
strenghten +(?x,+(?y,?x_10)) and +(?x_10,+(?x,?y))
strenghten +(?x,+(?y,?x_11)) and +(+(?x,?y),?x_11)
strenghten +(?x_2,+(?y_2,?z)) and +(+(?y_2,?x_2),?z)
strenghten +(?x,+(?y,s(0))) and s(+(?x,?y))
strenghten +(?x_12,+(s(0),?z)) and +(s(?x_12),?z)
strenghten +(s(?x_1),+(?y_1,?z)) and +(s(+(?x_1,?y_1)),?z)
strenghten +(+(?x,?y),+(?z,?z_1)) and +(+(?x,+(?y,?z)),?z_1)
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:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (14)+(1)*x1
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (15)
  s:= (2)+(2)*x1
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(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)> --> <+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?x)),?y)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
check joinability condition:
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
failed
failure(Step 1)
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 2 (linear)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(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)> --> <+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?x)),?y)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
check joinability condition:
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
failed
failure(Step 2)
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 3 (relative)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (14)+(1)*x1
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (15)
  s:= (2)+(2)*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<s(+(?x_2,s(?x))), s(+(?x,s(?x_2)))> --> <s(s(+(?x,?x_2))), s(s(+(?x_2,?x)))> => yes
<s(?x), s(+(?x,0))> --> <s(?x), s(?x)> => yes
<s(+(?x_2,0)), s(?x_2)> --> <s(?x_2), s(?x_2)> => yes
<0, 0> --> <0, 0> => yes
PCP_in(symP,S):
CP(S,symP):
<+(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,?y),?x_1)), s(+(+(?x,?x_1),?y))> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<s(+(?x,+(?x_1,?y_1))), +(?x_1,+(?y_1,s(?x)))> --> <s(+(?x,+(?x_1,?y_1))), s(+(+(?x,?y_1),?x_1))> => no
<+(s(+(?x,?y)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(+(?x,?z_1),?y))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?x,?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
<?x, +(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(+(?x,?x_1),?y)): joinable by {2}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {2}
check modulo joinability of s(+(+(?x,?y),?z_1)) and s(+(+(?x,?z_1),?y)): joinable by {2}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {2}
success
P':
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (1)
  s:= (1)*x1
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (8)
  s:= (2)+(1)*x1
relatively terminating
S/P': relatively terminating
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{0}
(cm)Rewrite Rules:
   [ e(?x) -> ++(?x,e(+(?x,?x))) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
Development Closed
Direct Methods: CR
{1}
(cm)Rewrite Rules:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ ++(++(?x,++(?y,?z)),?z_1) = ++(++(?x,?y),++(?z,?z_1)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR
Try A Minimal Decomposition {2,1,3}{5,7,4,6}{0}
{2,1,3}
(cm)Rewrite Rules:
   [ ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ ++(?x,++(?x_1,++(?y_1,?z_1))) = ++(++(?x,++(?x_1,?y_1)),?z_1),
     ++(?x,?x_2) = ++(++(?x,0),?x_2),
     ++(++(++(?x,?y),?z),?z_1) = ++(?x,++(++(?y,?z),?z_1)),
     ++(?x_2,?z_1) = ++(0,++(?x_2,?z_1)),
     ++(?x_1,++(++(?x,?y),?z)) = ++(++(?x_1,?x),++(?y,?z)),
     ++(++(?x,++(?y,?z)),?z_1) = ++(++(?x,?y),++(?z,?z_1)) ]
Outer CPs:
   [ ++(++(++(?x_1,?y_1),?y),?z) = ++(?x_1,++(?y_1,++(?y,?z))),
     ++(++(0,?y),?z) = ++(?y,?z) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ ++(?x_1,++(?y_1,++(++(?y,?y_2),?z_2))) = ++(++(++(?x_1,?y_1),?y),++(?y_2,?z_2)),
     ++(?x_1,++(?y_1,++(?x_3,++(?y_3,?z)))) = ++(++(++(?x_1,?y_1),++(?x_3,?y_3)),?z),
     ++(?x_1,++(?y_1,?z)) = ++(++(++(?x_1,?y_1),0),?z),
     ++(++(?y,?y_1),?z_1) = ++(++(0,?y),++(?y_1,?z_1)),
     ++(?x_2,++(?y_2,?z)) = ++(++(0,++(?x_2,?y_2)),?z),
     ?z = ++(++(0,0),?z),
     ++(?x_1,++(?y_1,++(?y,?z))) = ++(++(++(?x_1,?y_1),?y),?z),
     ++(?y,?z) = ++(++(0,?y),?z),
     ++(?x,++(++(?y,?y_1),?z_1)) = ++(++(?x,?y),++(?y_1,?z_1)),
     ++(?x,++(?x_2,++(?y_2,?z))) = ++(++(?x,++(?x_2,?y_2)),?z),
     ++(?x,?z) = ++(++(?x,0),?z),
     ++(++(?x_1,?x),++(++(?y,?y_2),?z_2)) = ++(?x_1,++(++(?x,?y),++(?y_2,?z_2))),
     ++(++(?x_1,?x),++(?x_3,++(?y_3,?z))) = ++(?x_1,++(++(?x,++(?x_3,?y_3)),?z)),
     ++(++(?x_1,?x),?z) = ++(?x_1,++(++(?x,0),?z)),
     ++(?x,++(++(++(?y,?y_3),?z_3),?z_2)) = ++(++(++(?x,?y),++(?y_3,?z_3)),?z_2),
     ++(?x,++(++(?x_4,++(?y_4,?z)),?z_2)) = ++(++(++(?x,++(?x_4,?y_4)),?z),?z_2),
     ++(?x,++(?z,?z_2)) = ++(++(++(?x,0),?z),?z_2),
     ++(++(?x_1,?x),++(?y,?z)) = ++(?x_1,++(++(?x,?y),?z)),
     ++(?x,++(++(?y,?z),?z_2)) = ++(++(++(?x,?y),?z),?z_2),
     ++(++(++(?x_2,++(?y_2,?y)),?y_1),?z_1) = ++(++(?x_2,?y_2),++(?y,++(?y_1,?z_1))),
     ++(++(++(++(?x,?y_3),?z_3),?y_1),?z_1) = ++(?x,++(++(?y_3,?z_3),++(?y_1,?z_1))),
     ++(++(?y,?y_1),?z_1) = ++(0,++(?y,++(?y_1,?z_1))),
     ++(++(++(?x,?y),?y_1),?z_1) = ++(?x,++(?y,++(?y_1,?z_1))),
     ++(++(?x_1,++(?y_1,?y)),?z) = ++(++(?x_1,?y_1),++(?y,?z)),
     ++(++(++(?x,?y_2),?z_2),?z) = ++(?x,++(++(?y_2,?z_2),?z)),
     ++(?y,?z) = ++(0,++(?y,?z)),
     ++(++(?x_2,++(?y_2,?y)),++(?z,?z_1)) = ++(++(++(?x_2,?y_2),++(?y,?z)),?z_1),
     ++(++(++(?x,?y_3),?z_3),++(?z,?z_1)) = ++(++(?x,++(++(?y_3,?z_3),?z)),?z_1),
     ++(++(?x_2,++(?x_3,++(?y_3,?y))),?z) = ++(?x_2,++(++(?x_3,?y_3),++(?y,?z))),
     ++(++(?x_2,++(++(?x,?y_4),?z_4)),?z) = ++(?x_2,++(?x,++(++(?y_4,?z_4),?z))),
     ++(++(?x_2,?y),?z) = ++(?x_2,++(0,++(?y,?z))),
     ++(++(?x,?y),++(?z,?z_1)) = ++(++(?x,++(?y,?z)),?z_1),
     ++(++(?x_2,++(?x,?y)),?z) = ++(?x_2,++(?x,++(?y,?z))),
     ++(++(0,?y_1),?z_1) = ++(?y_1,?z_1),
     ++(++(?x_2,0),?x) = ++(?x_2,?x),
     ++(0,++(?x,?z_3)) = ++(?x,?z_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 <++(?x,++(?x_1,++(?y_1,?z_1))), ++(++(?x,++(?x_1,?y_1)),?z_1)> by Rules <1, 0> preceded by [(++,2)]
 joinable by a reduction of rules <[([(++,2)],0)], [([],1)]>
Critical Pair <++(?x,?x_2), ++(++(?x,0),?x_2)> by Rules <2, 0> preceded by [(++,2)]
 joinable by a reduction of rules <[], [([],1),([(++,2)],2)]>
Critical Pair <++(++(++(?x,?y),?z),?z_1), ++(?x,++(++(?y,?z),?z_1))> by Rules <0, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[([(++,1)],1)], [([],0)]>
Critical Pair <++(?x_2,?z_1), ++(0,++(?x_2,?z_1))> by Rules <2, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <++(?x_1,++(++(?x,?y),?z)), ++(++(?x_1,?x),++(?y,?z))> by Rules <0, 0> preceded by [(++,2)]
 joinable by a reduction of rules <[([(++,2)],1)], [([],1)]>
Critical Pair <++(++(?x,++(?y,?z)),?z_1), ++(++(?x,?y),++(?z,?z_1))> by Rules <1, 1> preceded by [(++,1)]
 joinable by a reduction of rules <[([(++,1)],0)], [([],0)]>
Critical Pair <++(?x_1,++(?y_1,++(?y,?z))), ++(++(++(?x_1,?y_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <++(?y,?z), ++(++(0,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[], [([(++,1)],2)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 13 rules by 3 steps unfolding
strenghten ++(0,?x_2) and ?x_2
strenghten ++(0,++(0,?x_11)) and ?x_11
strenghten ++(++(0,0),?x_4) and ?x_4
strenghten ++(0,++(?x_2,?z_1)) and ++(?x_2,?z_1)
strenghten ++(++(?x,0),?x_2) and ++(?x,?x_2)
strenghten ++(++(0,?y),?z) and ++(?y,?z)
strenghten ++(0,++(++(0,?x_4),?z_1)) and ++(?x_4,?z_1)
strenghten ++(++(?x,0),++(0,?x_4)) and ++(?x,?x_4)
strenghten ++(++(?x,++(0,0)),?x_11) and ++(?x,?x_11)
strenghten ++(++(0,0),++(?x_11,?z_1)) and ++(?x_11,?z_1)
strenghten ++(++(++(0,0),?y),?z) and ++(?y,?z)
strenghten ++(?x,++(++(?y,?z),?z_1)) and ++(++(++(?x,?y),?z),?z_1)
strenghten ++(++(?x,?y),++(?z,?z_1)) and ++(++(?x,++(?y,?z)),?z_1)
strenghten ++(++(?x,++(?x_1,?y_1)),?z_1) and ++(?x,++(?x_1,++(?y_1,?z_1)))
strenghten ++(++(?x_1,?x),++(?y,?z)) and ++(?x_1,++(++(?x,?y),?z))
strenghten ++(++(++(?x_1,?y_1),?y),?z) and ++(?x_1,++(?y_1,++(?y,?z)))
obtain 37 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,?x) -> ?x ]
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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<++(?y_1,?z_1), ++(++(0,?y_1),?z_1)> --> <++(?y_1,?z_1), ++(?y_1,?z_1)> => yes
<++(?x_1,?x), ++(++(?x_1,0),?x)> --> <++(?x_1,?x), ++(++(?x_1,0),?x)> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
failed
failure(Step 1)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ ++(0,?x) -> ?x ]
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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<++(?y_1,?z_1), ++(++(0,?y_1),?z_1)> --> <++(?y_1,?z_1), ++(?y_1,?z_1)> => yes
<++(?x_1,?x), ++(++(?x_1,0),?x)> --> <++(?x_1,?x), ++(++(?x_1,0),?x)> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
failed
failure(Step 2)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ ++(0,?x) -> ?x ]
P:
   [ ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)) ]
Check relative termination:
   [ ++(0,?x) -> ?x ]
   [ ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)) ]
Polynomial Interpretation:
  0:= (8)
  ++:= (1)*x1+(1)*x2
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,++(?y,?z)) -> ++(++(?x,?y),?z),
     ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(0,?x) -> ?x ]
Sort Assignment:
 0 : =>12
 ++ : 12*12=>12
maximal types: {12}
Persistent Decomposition failed: Can't judge

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

{5,7,4,6}
(cm)Rewrite Rules:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,?y) -> +(?y,?x),
     +(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ +(s(+(?x_1,?y_1)),?z) = +(s(?x_1),+(?y_1,?z)),
     +(+(?y_2,?x_2),?z) = +(?x_2,+(?y_2,?z)),
     +(?x_3,?z) = +(0,+(?x_3,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?x,+(?y,?z)) = +(?z,+(?x,?y)),
     s(+(?x_1,?y_1)) = +(?y_1,s(?x_1)),
     +(?y_2,0) = ?y_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,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,s(+(?x_2,?y))) = +(s(?x_2),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(s(+(?x_2,?y)),?z) = +(s(?x_2),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(s(+(?x_3,?y)),+(?z,?z_1)) = +(+(s(?x_3),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_2)) = +(s(+(?x,?y)),?z_2),
     +(?x_1,+(?y_1,?y)) = +(?y,+(?x_1,?y_1)),
     s(+(?x_2,?y)) = +(?y,s(?x_2)),
     ?y = +(?y,0),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(?x,0) = ?x,
     +(0,+(?x,?z_2)) = +(?x,?z_2) ]
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(+(?x_1,?y_1)),?z), +(s(?x_1),+(?y_1,?z))> by Rules <1, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([],1),([(s,1)],0)], [([],1)]>
Critical Pair <+(+(?y_2,?x_2),?z), +(?x_2,+(?y_2,?z))> by Rules <2, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(+,2)],2)], [([],2),([],0)]>
Critical Pair <+(?x_3,?z), +(0,+(?x_3,?z))> by Rules <3, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <0, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([],0),([(+,2)],0)], [([],0)]>
Critical Pair <+(?y_2,+(?x,?y)), +(?x,+(?y,?y_2))> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <+(?y_2,s(?x_1)), s(+(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, +(?x_3,0)> 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_3,0) and ?x_3
strenghten +(0,?x_4) and ?x_4
strenghten +(?x_9,?y_9) and +(?y_9,?x_9)
strenghten +(?x_12,s(0)) and s(?x_12)
strenghten +(s(0),?x_12) and s(?x_12)
strenghten s(+(?x_1,0)) and s(?x_1)
strenghten s(+(?x_1,?x_10)) and +(?x_10,s(?x_1))
strenghten s(+(?x_1,?x_11)) and +(s(?x_1),?x_11)
strenghten +(?x,+(?y,0)) and +(?x,?y)
strenghten +(?x_4,+(0,?z)) and +(?x_4,?z)
strenghten +(0,+(?x_3,?z)) and +(?x_3,?z)
strenghten s(+(?x_1,s(0))) and s(s(?x_1))
strenghten +(?x,+(?y,?x_10)) and +(?x_10,+(?x,?y))
strenghten +(?x,+(?y,?x_11)) and +(+(?x,?y),?x_11)
strenghten +(?x_2,+(?y_2,?z)) and +(+(?y_2,?x_2),?z)
strenghten +(?x,+(?y,s(0))) and s(+(?x,?y))
strenghten +(?x_12,+(s(0),?z)) and +(s(?x_12),?z)
strenghten +(s(?x_1),+(?y_1,?z)) and +(s(+(?x_1,?y_1)),?z)
strenghten +(+(?x,?y),+(?z,?z_1)) and +(+(?x,+(?y,?z)),?z_1)
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:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (14)+(1)*x1
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (15)
  s:= (2)+(2)*x1
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(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)> --> <+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?x)),?y)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
check joinability condition:
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
failed
failure(Step 1)
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 2 (linear)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(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)> --> <+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?x)),?y)> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
check joinability condition:
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
failed
failure(Step 2)
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 3 (relative)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (14)+(1)*x1
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (15)
  s:= (2)+(2)*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<s(+(?x_2,s(?x))), s(+(?x,s(?x_2)))> --> <s(s(+(?x,?x_2))), s(s(+(?x_2,?x)))> => yes
<s(?x), s(+(?x,0))> --> <s(?x), s(?x)> => yes
<s(+(?x_2,0)), s(?x_2)> --> <s(?x_2), s(?x_2)> => yes
<0, 0> --> <0, 0> => yes
PCP_in(symP,S):
CP(S,symP):
<+(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,?y),?x_1)), s(+(+(?x,?x_1),?y))> => no
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<s(+(?x,+(?x_1,?y_1))), +(?x_1,+(?y_1,s(?x)))> --> <s(+(?x,+(?x_1,?y_1))), s(+(+(?x,?y_1),?x_1))> => no
<+(s(+(?x,?y)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(+(?x,?z_1),?y))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?x,?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
<?x, +(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(+(?x,?x_1),?y)): joinable by {2}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {2}
check modulo joinability of s(+(+(?x,?y),?z_1)) and s(+(+(?x,?z_1),?y)): joinable by {2}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {2}
success
P':
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Check relative termination:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (1)
  s:= (1)*x1
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (8)
  s:= (2)+(1)*x1
relatively terminating
S/P': relatively terminating
S:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     +(0,?x) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)),
     +(?x,0) -> ?x ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{0}
(cm)Rewrite Rules:
   [ e(?x) -> ++(?x,e(+(?x,?x))) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
Development Closed
Direct Methods: CR
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
R8.trs: Failure(unknown)
(23308 msec.)