MAYBE
(ignored inputs)COMMENT composable
Rewrite Rules:
   [ ++(++(?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_1,?y_1),?z_1),?z) = ++(?x_1,++(++(?y_1,?z_1),?z)),
     ++(?x_2,?z) = ++(0,++(?x_2,?z)),
     ++(?x_1,++(?x,++(?y,?z))) = ++(++(?x_1,++(?x,?y)),?z),
     ++(?x_1,?x_2) = ++(++(?x_1,0),?x_2),
     +(+(?y_3,?x_3),?z_4) = +(?x_3,+(?y_3,?z_4)),
     +(?x_5,?z_4) = +(0,+(?x_5,?z_4)),
     +(s(+(?x_6,?y_6)),?z_4) = +(s(?x_6),+(?y_6,?z_4)),
     ++(++(?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,++(?y,++(?y_1,?z_1))) = ++(++(++(?x,?y),?y_1),?z_1),
     ++(++(0,?y_1),?z_1) = ++(?y_1,?z_1),
     +(?y_3,+(?x_4,?y_4)) = +(?x_4,+(?y_4,?y_3)),
     +(?y_3,0) = ?y_3,
     +(?y_3,s(?x_6)) = s(+(?x_6,?y_3)) ]
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_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),
     ++(?y,++(?z,?z_1)) = ++(++(0,++(?y,?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))),
     ++(?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)),
     ?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),
     ++(++(0,?y_2),?z_2) = ++(?y_2,?z_2),
     ++(0,++(?x,?z_2)) = ++(?x,?z_2),
     ++(++(?x_3,0),?x) = ++(?x_3,?x),
     +(?x_4,+(?y_4,?y)) = +(?y,+(?x_4,?y_4)),
     ?y = +(?y,0),
     s(+(?x_6,?y)) = +(?y,s(?x_6)),
     +(?x,+(?y,?z_5)) = +(+(?y,?x),?z_5),
     +(?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_7,?y))) = +(s(?x_7),+(?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_7,?y)),?z) = +(s(?x_7),+(?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_8,?y)),+(?z,?z_1)) = +(+(s(?x_8),+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?x,0) = ?x,
     +(0,+(?x,?z_6)) = +(?x,?z_6),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_6)) = +(s(+(?x,?y)),?z_6) ]
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_1,?y_1),?z_1),?z), ++(?x_1,++(++(?y_1,?z_1),?z))> by Rules <1, 0> preceded by [(++,1)]
 joinable by a reduction of rules <[([(++,1)],0)], [([],1)]>
Critical Pair <++(?x_2,?z), ++(0,++(?x_2,?z))> by Rules <2, 0> 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, 1> preceded by [(++,2)]
 joinable by a reduction of rules <[([(++,2)],1)], [([],0)]>
Critical Pair <++(?x_1,?x_2), ++(++(?x_1,0),?x_2)> by Rules <2, 1> preceded by [(++,2)]
 joinable by a reduction of rules <[], [([],0),([(++,2)],2)]>
Critical Pair <+(+(?y_3,?x_3),?z_4), +(?x_3,+(?y_3,?z_4))> by Rules <3, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],3),([],4)], []>
 joinable by a reduction of rules <[([],4),([(+,2)],3)], [([],3),([],4)]>
Critical Pair <+(?x_5,?z_4), +(0,+(?x_5,?z_4))> by Rules <5, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],5)]>
Critical Pair <+(s(+(?x_6,?y_6)),?z_4), +(s(?x_6),+(?y_6,?z_4))> by Rules <6, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([],6),([(s,1)],4)], [([],6)]>
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 <[([(++,1)],1)], [([],1)]>
Critical Pair <++(?x_1,++(++(?x,?y),?z)), ++(++(?x_1,?x),++(?y,?z))> by Rules <1, 1> preceded by [(++,2)]
 joinable by a reduction of rules <[([(++,2)],0)], [([],0)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <4, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],4)], [([],4)]>
Critical Pair <++(++(++(?x,?y),?y_1),?z_1), ++(?x,++(?y,++(?y_1,?z_1)))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <++(?y_1,?z_1), ++(++(0,?y_1),?z_1)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[], [([(++,1)],2)]>
Critical Pair <+(?x_4,+(?y_4,?z_4)), +(?z_4,+(?x_4,?y_4))> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[], [([],3),([],4)]>
Critical Pair <?x_5, +(?x_5,0)> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[], [([],3),([],5)]>
Critical Pair <s(+(?x_6,?y_6)), +(?y_6,s(?x_6))> by Rules <6, 3> preceded by []
 joinable by a reduction of rules <[], [([],3),([],6)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 17 rules by 3 steps unfolding
strenghten +(?x_5,0) and ?x_5
strenghten +(0,?x_7) and ?x_7
strenghten +(?x_13,?y_13) and +(?y_13,?x_13)
strenghten +(?x_16,s(0)) and s(?x_16)
strenghten +(s(0),?x_16) and s(?x_16)
strenghten s(+(?x_6,0)) and s(?x_6)
strenghten +(?y_6,s(?x_6)) and s(+(?x_6,?y_6))
strenghten s(+(?x_6,?x_14)) and +(?x_14,s(?x_6))
strenghten s(+(?x_6,?x_15)) and +(s(?x_6),?x_15)
strenghten +(?x_4,+(?y_4,0)) and +(?x_4,?y_4)
strenghten +(?x_7,+(0,?z_4)) and +(?x_7,?z_4)
strenghten +(0,+(?x_5,?z_4)) and +(?x_5,?z_4)
strenghten s(+(?x_6,s(0))) and s(s(?x_6))
strenghten ++(0,++(?x_2,?z)) and ++(?x_2,?z)
strenghten ++(++(?x_1,0),?x_2) and ++(?x_1,?x_2)
strenghten ++(++(0,?y_1),?z_1) and ++(?y_1,?z_1)
strenghten +(?x_3,+(?y_3,?z_4)) and +(+(?y_3,?x_3),?z_4)
strenghten +(?x_4,+(?y_4,?x_14)) and +(?x_14,+(?x_4,?y_4))
strenghten +(?x_4,+(?y_4,?x_15)) and +(+(?x_4,?y_4),?x_15)
strenghten +(?z_4,+(?x_4,?y_4)) and +(?x_4,+(?y_4,?z_4))
strenghten +(?x_4,+(?y_4,s(0))) and s(+(?x_4,?y_4))
strenghten +(?x_16,+(s(0),?z_4)) and +(s(?x_16),?z_4)
strenghten +(s(?x_6),+(?y_6,?z_4)) and +(s(+(?x_6,?y_6)),?z_4)
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:
   [ ++(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)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (4)
  s:= (1)*x1
  ++:= (1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= 0
  s:= (6)+(2)*x1
  ++:= (1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(s(?x),?y) -> s(+(?x,?y))
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(s(?x),?y) -> s(+(?x,?y))
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ ++(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: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(?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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<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
check joinability condition:
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
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
failed
failure(Step 1)
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 2 (linear)
S:
   [ ++(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: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(?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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), +(?y,s(?x))> => no
<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
check joinability condition:
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
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(?y,s(?x)): maybe not reachable
check modulo reachablity from +(?x_1,s(+(?x,?y))) to +(+(?x_1,s(?x)),?y): maybe not reachable
failed
failure(Step 2)
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?x,?y)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 3 (relative)
S:
   [ ++(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:
   [ ++(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)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (4)
  s:= (1)*x1
  ++:= (1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (4)
  s:= (4)+(1)*x1
  ++:= (1)*x1+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(?x_4,0)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(?x_2,0))> --> <s(?x_2), s(?x_2)> => yes
<s(+(?x_4,s(?x_2))), s(+(?x_2,s(?x_4)))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_4,?x_2)))> => yes
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?x,?y))> => 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
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?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
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(+(?x,?x_1),?y)): joinable by {4}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {4}
check modulo joinability of s(+(+(?x,?y),?z_1)) and s(+(+(?x,?z_1),?y)): joinable by {4}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {4}
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?x,?y)) => +(?y,s(?x)) -> s(+(?y,?x))
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 5 (linear)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(?x_4,0)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(?x_2,0))> --> <s(?x_2), s(?x_2)> => yes
<s(+(?x_4,s(?x_2))), s(+(?x_2,s(?x_4)))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_4,?x_2)))> => yes
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?x,?y))> => 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
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?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
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(+(?x,?x_1),?y)): joinable by {0}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {0}
check modulo joinability of s(+(+(?x,?y),?z_1)) and s(+(+(?x,?z_1),?y)): joinable by {0}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {0}
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?x,?y)) => +(?y,s(?x)) -> s(+(?y,?x))
replace: +(s(?x),?y) -> s(+(?x,?y)) => +(s(?x),?y) -> s(+(?y,?x))
STEP: 6 (relative)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (5)+(1)*x1
  ++:= (1)+(1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (14)
  s:= (1)+(1)*x1
  ++:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(?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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), +(?y,s(?x))> => no
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> => no
check joinability condition:
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
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {0}
check modulo reachablity from s(+(?y,?x)) to +(?y,s(?x)): maybe not reachable
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {0}
check modulo reachablity from +(?x_1,s(+(?y,?x))) to +(+(?x_1,s(?x)),?y): maybe not reachable
failed
failure(Step 7)
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 8 (linear)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(?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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), +(?y,s(?x))> => no
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> => no
check joinability condition:
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
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {4}
check modulo reachablity from s(+(?y,?x)) to +(?y,s(?x)): maybe not reachable
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {4}
check modulo reachablity from +(?x_1,s(+(?y,?x))) to +(+(?x_1,s(?x)),?y): maybe not reachable
failed
failure(Step 8)
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
Added P-Rules:
   [ ]
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 9 (relative)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)) ]
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:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)) ]
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (2)
  s:= (1)*x1
  ++:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= 0
  s:= (5)+(2)*x1
  ++:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
STEP: 10 (parallel)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(?x_4,0)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(0,?x_2))> --> <s(?x_2), s(?x_2)> => yes
<s(+(?x_4,s(?x_2))), s(+(s(?x_4),?x_2))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_2,?x_4)))> => yes
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), s(+(?x,?y))> => yes
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <s(+(+(?y,?x),?x_1)), s(+(?y,+(?x,?x_1)))> => 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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?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(+(?z_1,+(?x,?y))), s(+(+(?z_1,?x),?y))> => yes
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?y,?x))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {0}
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {0}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {4}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {4}
failed
failure(Step 10)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?x,?y)) => +(?y,s(?x)) -> s(+(?y,?x))
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 11 (linear)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(?x_4,0)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(0,?x_2))> --> <s(?x_2), s(?x_2)> => yes
<s(+(?x_4,s(?x_2))), s(+(s(?x_4),?x_2))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_2,?x_4)))> => yes
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), s(+(?x,?y))> => yes
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <s(+(+(?y,?x),?x_1)), s(+(?y,+(?x,?x_1)))> => 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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?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(+(?z_1,+(?x,?y))), s(+(+(?z_1,?x),?y))> => yes
<s(+(?x,?y)), +(s(?x),?y)> --> <s(+(?x,?y)), s(+(?y,?x))> => yes
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?y),s(?x))> --> <s(+(+(?x,?y),?x_1)), s(+(?x,+(?x_1,?y)))> => no
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {4}
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {4}
check modulo joinability of s(+(?x,+(?x_1,?y_1))) and s(+(+(?x,?y_1),?x_1)): joinable by {0}
check modulo joinability of s(+(+(?x,?y),?x_1)) and s(+(?x,+(?x_1,?y))): joinable by {0}
failed
failure(Step 11)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?x,?y)) => +(?y,s(?x)) -> s(+(?y,?x))
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 12 (relative)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> 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)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (4)
  s:= (1)*x1
  ++:= (1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (4)
  s:= (6)+(1)*x1
  ++:= (1)*x1+(2)*x1*x2+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 12)
STEP: 13 (parallel)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?x_4)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(?x_2,0))> --> <s(?x_2), s(?x_2)> => yes
<s(+(s(?x_2),?x_4)), s(+(?x_2,s(?x_4)))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_2,?x_4)))> => yes
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?y,?x))> => 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
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<s(+(+(?x_1,?y_1),?x)), +(?x_1,+(?y_1,s(?x)))> --> <s(+(+(?x_1,?y_1),?x)), s(+(?x_1,+(?y_1,?x)))> => yes
<+(s(+(?y,?x)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(+(?y,?x),?z_1)), s(+(?y,+(?x,?z_1)))> => yes
<s(+(?y,?x)), +(s(?x),?y)> --> <s(+(?y,?x)), s(+(?x,?y))> => yes
<+(?x_1,s(+(?y,?x))), +(+(?x_1,?y),s(?x))> --> <s(+(?x_1,+(?y,?x))), s(+(+(?x_1,?y),?x))> => yes
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
failed
failure(Step 13)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 14 (linear)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?x_4)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(?x_2,0))> --> <s(?x_2), s(?x_2)> => yes
<s(+(s(?x_2),?x_4)), s(+(?x_2,s(?x_4)))> --> <s(s(+(?x_2,?x_4))), s(s(+(?x_2,?x_4)))> => yes
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?x,?y)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(+(?x,?y),?z_1)), s(+(?x,+(?y,?z_1)))> => yes
<s(+(?x,?y)), +(?y,s(?x))> --> <s(+(?x,?y)), s(+(?y,?x))> => 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
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<s(+(+(?x_1,?y_1),?x)), +(?x_1,+(?y_1,s(?x)))> --> <s(+(+(?x_1,?y_1),?x)), s(+(?x_1,+(?y_1,?x)))> => yes
<+(s(+(?y,?x)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(+(?y,?x),?z_1)), s(+(?y,+(?x,?z_1)))> => yes
<s(+(?y,?x)), +(s(?x),?y)> --> <s(+(?y,?x)), s(+(?x,?y))> => yes
<+(?x_1,s(+(?y,?x))), +(+(?x_1,?y),s(?x))> --> <s(+(?x_1,+(?y,?x))), s(+(+(?x_1,?y),?x))> => yes
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
failed
failure(Step 14)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 15 (relative)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
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:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x1*x2+(1)*x2
  0:= (8)
  s:= (13)+(1)*x1
  ++:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (7)
  s:= (4)+(1)*x1
  ++:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 15)
STEP: 16 (parallel)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?x_4)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(0,?x_2))> --> <s(?x_2), s(?x_2)> => yes
<s(+(s(?x_2),?x_4)), s(+(s(?x_4),?x_2))> --> <s(s(+(?x_4,?x_2))), s(s(+(?x_2,?x_4)))> => yes
PCP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), s(+(?y,?x))> => yes
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <s(+(?x_1,+(?y,?x))), s(+(?y,+(?x_1,?x)))> => no
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<s(+(+(?x_1,?y_1),?x)), +(?x_1,+(?y_1,s(?x)))> --> <s(+(+(?x_1,?y_1),?x)), s(+(?x_1,+(?y_1,?x)))> => yes
<+(s(+(?y,?x)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(?y,+(?z_1,?x)))> => no
<s(+(?y,?x)), +(s(?x),?y)> --> <s(+(?y,?x)), s(+(?y,?x))> => yes
<+(?x_1,s(+(?y,?x))), +(+(?x_1,?y),s(?x))> --> <s(+(?x_1,+(?y,?x))), s(+(+(?x_1,?y),?x))> => yes
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {0}
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {0}
check modulo joinability of s(+(?x_1,+(?y,?x))) and s(+(?y,+(?x_1,?x))): joinable by {0}
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(?y,+(?z_1,?x))): joinable by {0}
failed
failure(Step 16)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?y,?x)) => +(?y,s(?x)) -> s(+(?x,?y))
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 17 (linear)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
P:
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?x_4)), s(?x_4)> --> <s(?x_4), s(?x_4)> => yes
<s(?x_2), s(+(0,?x_2))> --> <s(?x_2), s(?x_2)> => yes
<s(+(s(?x_2),?x_4)), s(+(s(?x_4),?x_2))> --> <s(s(+(?x_4,?x_2))), s(s(+(?x_2,?x_4)))> => yes
CP_in(symP,S):
CP(S,symP):
<++(?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,?z_1), ++(0,++(?x,?z_1))> --> <++(?x,?z_1), ++(?x,?z_1)> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<?x, +(?x,0)> --> <?x, ?x> => 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
<+(s(+(?y,?x)),?z_1), +(s(?x),+(?y,?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(+(?y,?z_1),?x))> => no
<s(+(?y,?x)), +(?y,s(?x))> --> <s(+(?y,?x)), s(+(?y,?x))> => yes
<s(+(+(?y_1,?z_1),?x)), +(+(s(?x),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?x)), s(+(?z_1,+(?y_1,?x)))> => no
<+(?x_1,s(+(?y,?x))), +(+(?x_1,s(?x)),?y)> --> <s(+(?x_1,+(?y,?x))), s(+(?y,+(?x_1,?x)))> => no
<+(?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, +(0,?x)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<s(+(+(?x_1,?y_1),?x)), +(?x_1,+(?y_1,s(?x)))> --> <s(+(+(?x_1,?y_1),?x)), s(+(?x_1,+(?y_1,?x)))> => yes
<+(s(+(?y,?x)),?z_1), +(?y,+(s(?x),?z_1))> --> <s(+(?z_1,+(?y,?x))), s(+(?y,+(?z_1,?x)))> => no
<s(+(?y,?x)), +(s(?x),?y)> --> <s(+(?y,?x)), s(+(?y,?x))> => yes
<+(?x_1,s(+(?y,?x))), +(+(?x_1,?y),s(?x))> --> <s(+(?x_1,+(?y,?x))), s(+(+(?x_1,?y),?x))> => yes
check joinability condition:
check modulo reachablity from ++(?x_1,?x) to ++(++(?x_1,0),?x): maybe not reachable
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(+(?y,?z_1),?x)): joinable by {4}
check modulo joinability of s(+(+(?y_1,?z_1),?x)) and s(+(?z_1,+(?y_1,?x))): joinable by {4}
check modulo joinability of s(+(?x_1,+(?y,?x))) and s(+(?y,+(?x_1,?x))): joinable by {4}
check modulo joinability of s(+(?z_1,+(?y,?x))) and s(+(?y,+(?z_1,?x))): joinable by {4}
failed
failure(Step 17)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: +(?y,s(?x)) -> s(+(?y,?x)) => +(?y,s(?x)) -> s(+(?x,?y))
replace: +(s(?x),?y) -> s(+(?y,?x)) => +(s(?x),?y) -> s(+(?x,?y))
STEP: 18 (relative)
S:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
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:
   [ ++(0,?x) -> ?x,
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?y,?x)),
     +(?x,0) -> ?x,
     +(?y,s(?x)) -> s(+(?y,?x)) ]
   [ ++(++(?x,?y),?z) -> ++(?x,++(?y,?z)),
     ++(?x,++(?y,?z)) -> ++(++(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (12)
  s:= (1)*x1
  ++:= (1)*x1+(1)*x2
retract ++(0,?x) -> ?x
retract +(0,?x) -> ?x
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (12)
  s:= (1)+(1)*x1
  ++:= (1)*x1+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 18)
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,
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Sort Assignment:
 + : 20*20=>20
 0 : =>20
 s : 20=>20
 ++ : 20*20=>20
maximal types: {20}
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,
     +(?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...
   [ ++(++(?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,?y),?y_1),?z_1), ++(?x,++(?y,++(?y_1,?z_1)))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, ++(++(?x,?y),++(?y_1,?z_1))>
<{0}, ++(++(?x,++(?y,?y_1)),?z_1)>
<{}, ++(++(++(?x,?y),?y_1),?z_1)>
develop reducts from rhs term...
<{1}, ++(++(?x,?y),++(?y_1,?z_1))>
<{1}, ++(?x,++(++(?y,?y_1),?z_1))>
<{}, ++(?x,++(?y,++(?y_1,?z_1)))>
Outside Critical Pair: <++(?y_1,?z_1), ++(++(0,?y_1),?z_1)> by Rules <2, 1>
develop reducts from lhs term...
<{}, ++(?y_1,?z_1)>
develop reducts from rhs term...
<{0}, ++(0,++(?y_1,?z_1))>
<{2}, ++(?y_1,?z_1)>
<{}, ++(++(0,?y_1),?z_1)>
Outside Critical Pair: <+(?x_4,+(?y_4,?z_4)), +(?z_4,+(?x_4,?y_4))> by Rules <4, 3>
develop reducts from lhs term...
<{3}, +(+(?z_4,?y_4),?x_4)>
<{3}, +(+(?y_4,?z_4),?x_4)>
<{3}, +(?x_4,+(?z_4,?y_4))>
<{}, +(?x_4,+(?y_4,?z_4))>
develop reducts from rhs term...
<{3}, +(+(?y_4,?x_4),?z_4)>
<{3}, +(+(?x_4,?y_4),?z_4)>
<{3}, +(?z_4,+(?y_4,?x_4))>
<{}, +(?z_4,+(?x_4,?y_4))>
Outside Critical Pair: <?x_5, +(?x_5,0)> by Rules <5, 3>
develop reducts from lhs term...
<{}, ?x_5>
develop reducts from rhs term...
<{3}, +(0,?x_5)>
<{}, +(?x_5,0)>
Outside Critical Pair: <s(+(?x_6,?y_6)), +(?y_6,s(?x_6))> by Rules <6, 3>
develop reducts from lhs term...
<{3}, s(+(?y_6,?x_6))>
<{}, s(+(?x_6,?y_6))>
develop reducts from rhs term...
<{3}, +(s(?x_6),?y_6)>
<{}, +(?y_6,s(?x_6))>
Inside Critical Pair: <++(++(++(?x_1,?y_1),?z_1),?z), ++(?x_1,++(++(?y_1,?z_1),?z))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, ++(++(?x_1,?y_1),++(?z_1,?z))>
<{0}, ++(++(?x_1,++(?y_1,?z_1)),?z)>
<{}, ++(++(++(?x_1,?y_1),?z_1),?z)>
develop reducts from rhs term...
<{1}, ++(++(?x_1,++(?y_1,?z_1)),?z)>
<{0}, ++(?x_1,++(?y_1,++(?z_1,?z)))>
<{}, ++(?x_1,++(++(?y_1,?z_1),?z))>
Inside Critical Pair: <++(?x_2,?z), ++(0,++(?x_2,?z))> by Rules <2, 0>
develop reducts from lhs term...
<{}, ++(?x_2,?z)>
develop reducts from rhs term...
<{2}, ++(?x_2,?z)>
<{1}, ++(++(0,?x_2),?z)>
<{}, ++(0,++(?x_2,?z))>
Inside Critical Pair: <++(?x_1,++(?x,++(?y,?z))), ++(++(?x_1,++(?x,?y)),?z)> by Rules <0, 1>
develop reducts from lhs term...
<{1}, ++(++(?x_1,?x),++(?y,?z))>
<{1}, ++(?x_1,++(++(?x,?y),?z))>
<{}, ++(?x_1,++(?x,++(?y,?z)))>
develop reducts from rhs term...
<{0}, ++(?x_1,++(++(?x,?y),?z))>
<{1}, ++(++(++(?x_1,?x),?y),?z)>
<{}, ++(++(?x_1,++(?x,?y)),?z)>
Inside Critical Pair: <++(?x_1,?x_2), ++(++(?x_1,0),?x_2)> by Rules <2, 1>
develop reducts from lhs term...
<{}, ++(?x_1,?x_2)>
develop reducts from rhs term...
<{0}, ++(?x_1,++(0,?x_2))>
<{}, ++(++(?x_1,0),?x_2)>
Inside Critical Pair: <+(+(?y_3,?x_3),?z_4), +(?x_3,+(?y_3,?z_4))> by Rules <3, 4>
develop reducts from lhs term...
<{4}, +(?y_3,+(?x_3,?z_4))>
<{3}, +(?z_4,+(?x_3,?y_3))>
<{3}, +(?z_4,+(?y_3,?x_3))>
<{3}, +(+(?x_3,?y_3),?z_4)>
<{}, +(+(?y_3,?x_3),?z_4)>
develop reducts from rhs term...
<{3}, +(+(?z_4,?y_3),?x_3)>
<{3}, +(+(?y_3,?z_4),?x_3)>
<{3}, +(?x_3,+(?z_4,?y_3))>
<{}, +(?x_3,+(?y_3,?z_4))>
Inside Critical Pair: <+(?x_5,?z_4), +(0,+(?x_5,?z_4))> by Rules <5, 4>
develop reducts from lhs term...
<{3}, +(?z_4,?x_5)>
<{}, +(?x_5,?z_4)>
develop reducts from rhs term...
<{3,5}, +(?z_4,?x_5)>
<{5}, +(?x_5,?z_4)>
<{3}, +(+(?z_4,?x_5),0)>
<{3}, +(+(?x_5,?z_4),0)>
<{3}, +(0,+(?z_4,?x_5))>
<{}, +(0,+(?x_5,?z_4))>
Inside Critical Pair: <+(s(+(?x_6,?y_6)),?z_4), +(s(?x_6),+(?y_6,?z_4))> by Rules <6, 4>
develop reducts from lhs term...
<{3,6}, s(+(+(?y_6,?x_6),?z_4))>
<{6}, s(+(+(?x_6,?y_6),?z_4))>
<{3}, +(?z_4,s(+(?y_6,?x_6)))>
<{3}, +(?z_4,s(+(?x_6,?y_6)))>
<{3}, +(s(+(?y_6,?x_6)),?z_4)>
<{}, +(s(+(?x_6,?y_6)),?z_4)>
develop reducts from rhs term...
<{3,6}, s(+(?x_6,+(?z_4,?y_6)))>
<{6}, s(+(?x_6,+(?y_6,?z_4)))>
<{3}, +(+(?z_4,?y_6),s(?x_6))>
<{3}, +(+(?y_6,?z_4),s(?x_6))>
<{3}, +(s(?x_6),+(?z_4,?y_6))>
<{}, +(s(?x_6),+(?y_6,?z_4))>
Try A Minimal Decomposition {1,2}{4,6,3,5}{0}
{1,2}
(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
{4,6,3,5}
(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:
   [ ++(++(?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 {1,0,2}{4,6,3,5}
{1,0,2}
(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

{4,6,3,5}
(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
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
R7.trs: Failure(unknown)
(22713 msec.)