MAYBE
(ignored inputs)COMMENT doi:10.1137/0215084 [119] p. 1173 submitted by: Aart Middeldorp
Rewrite Rules:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(1,-(1)) = 0,
     +(+(?x_3,+(?y_3,1)),-(1)) = +(?x_3,?y_3),
     +(+(1,?x_4),-(1)) = ?x_4,
     +(?x_2,?x) = +(+(?x_2,0),?x),
     +(?x_2,0) = +(+(?x_2,1),-(1)),
     +(?x_2,?x_1) = +(+(?x_2,+(?x_1,1)),-(1)),
     +(?x_2,+(?x_3,+(?y_3,?z_3))) = +(+(?x_2,+(?x_3,?y_3)),?z_3),
     +(?x_2,+(?y_4,?x_4)) = +(+(?x_2,?x_4),?y_4),
     +(?x,?z_3) = +(0,+(?x,?z_3)),
     +(0,?z_3) = +(1,+(-(1),?z_3)),
     +(?x_1,?z_3) = +(+(?x_1,1),+(-(1),?z_3)),
     +(+(+(?x_2,?y_2),?z_2),?z_3) = +(?x_2,+(+(?y_2,?z_2),?z_3)),
     +(+(?y_4,?x_4),?z_3) = +(?x_4,+(?y_4,?z_3)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?y_2,?z_2) = +(+(0,?y_2),?z_2),
     ?x = +(?x,0),
     0 = +(-(1),1),
     ?x_1 = +(?x_1,+(1,-(1))),
     ?x_1 = +(-(1),+(?x_1,1)),
     +(+(+(?x_3,?y_3),?y_2),?z_2) = +(?x_3,+(?y_3,+(?y_2,?z_2))),
     +(+(?x_2,?y_2),?z_2) = +(+(?y_2,?z_2),?x_2),
     +(?x_3,+(?y_3,?z_3)) = +(?z_3,+(?x_3,?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:
   [ +(+(0,?y_2),?z_2) = +(?y_2,?z_2),
     +(?x,0) = ?x,
     0 = +(1,-(1)),
     +(+(?x_3,0),?x) = +(?x_3,?x),
     +(0,+(?x,?z_4)) = +(?x,?z_4),
     +(-(1),1) = 0,
     +(+(?x_2,1),-(1)) = +(?x_2,0),
     +(1,+(-(1),?z_3)) = +(0,?z_3),
     +(-(1),+(?x_4,+(?y_4,1))) = +(?x_4,?y_4),
     +(-(1),+(1,?x)) = ?x,
     +(?x,+(1,-(1))) = ?x,
     +(-(1),+(?x,1)) = ?x,
     +(1,-(1)) = 0,
     +(+(?x_4,+(?y_4,1)),-(1)) = +(?x_4,?y_4),
     +(+(1,?x),-(1)) = ?x,
     +(+(?x_3,+(?x_7,+(?y_7,1))),-(1)) = +(?x_3,+(?x_7,?y_7)),
     +(+(?x_3,+(1,?x)),-(1)) = +(?x_3,?x),
     +(+(?x_8,+(?y_8,1)),+(-(1),?z_4)) = +(+(?x_8,?y_8),?z_4),
     +(+(1,?x),+(-(1),?z_4)) = +(?x,?z_4),
     +(+(?x,1),+(-(1),?z_4)) = +(?x,?z_4),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     ?z = +(+(0,0),?z),
     0 = +(+(0,1),-(1)),
     ?x_3 = +(+(0,+(?x_3,1)),-(1)),
     +(?x_4,+(?y_4,?z)) = +(+(0,+(?x_4,?y_4)),?z),
     +(?z,?y) = +(+(0,?y),?z),
     +(?x_3,+(?y_3,+(+(?y,?y_4),?z_4))) = +(+(+(?x_3,?y_3),?y),+(?y_4,?z_4)),
     +(?x_3,+(?y_3,?z)) = +(+(+(?x_3,?y_3),0),?z),
     +(?x_3,+(?y_3,0)) = +(+(+(?x_3,?y_3),1),-(1)),
     +(?x_3,+(?y_3,?x_6)) = +(+(+(?x_3,?y_3),+(?x_6,1)),-(1)),
     +(?x_3,+(?y_3,+(?x_7,+(?y_7,?z)))) = +(+(+(?x_3,?y_3),+(?x_7,?y_7)),?z),
     +(?x_3,+(?y_3,+(?z,?y))) = +(+(+(?x_3,?y_3),?y),?z),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?z,?x) = +(+(?x,0),?z),
     +(0,?x) = +(+(?x,1),-(1)),
     +(?x_3,?x) = +(+(?x,+(?x_3,1)),-(1)),
     +(+(?x_4,+(?y_4,?z)),?x) = +(+(?x,+(?x_4,?y_4)),?z),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(?y,?z) = +(+(0,?y),?z),
     +(?x_3,+(?y_3,+(?y,?z))) = +(+(+(?x_3,?y_3),?y),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,?z) = +(+(?x,0),?z),
     +(?x,0) = +(+(?x,1),-(1)),
     +(?x,?x_3) = +(+(?x,+(?x_3,1)),-(1)),
     +(?x,+(?x_4,+(?y_4,?z))) = +(+(?x,+(?x_4,?y_4)),?z),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)),
     +(+(?x_1,?x),0) = +(?x_1,+(+(?x,1),-(1))),
     +(+(?x_1,?x),?x_4) = +(?x_1,+(+(?x,+(?x_4,1)),-(1))),
     +(+(?x_1,?x),+(?x_5,+(?y_5,?z))) = +(?x_1,+(+(?x,+(?x_5,?y_5)),?z)),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(+(?y,?y_5),?z_5),?z_4)) = +(+(+(?x,?y),+(?y_5,?z_5)),?z_4),
     +(?x,+(?z,?z_4)) = +(+(+(?x,0),?z),?z_4),
     +(?x,+(0,?z_4)) = +(+(+(?x,1),-(1)),?z_4),
     +(?x,+(?x_7,?z_4)) = +(+(+(?x,+(?x_7,1)),-(1)),?z_4),
     +(?x,+(+(?x_8,+(?y_8,?z)),?z_4)) = +(+(+(?x,+(?x_8,?y_8)),?z),?z_4),
     +(?x,+(+(?z,?y),?z_4)) = +(+(+(?x,?y),?z),?z_4),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_4)) = +(+(+(?x,?y),?z),?z_4),
     +(+(+(?x_4,+(?y_4,?y)),?y_3),?z_3) = +(+(?x_4,?y_4),+(?y,+(?y_3,?z_3))),
     +(+(?y,?y_3),?z_3) = +(0,+(?y,+(?y_3,?z_3))),
     +(+(0,?y_3),?z_3) = +(1,+(-(1),+(?y_3,?z_3))),
     +(+(?x_6,?y_3),?z_3) = +(+(?x_6,1),+(-(1),+(?y_3,?z_3))),
     +(+(+(+(?x,?y_7),?z_7),?y_3),?z_3) = +(?x,+(+(?y_7,?z_7),+(?y_3,?z_3))),
     +(+(+(?y,?x),?y_3),?z_3) = +(?x,+(?y,+(?y_3,?z_3))),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,0) = +(1,+(-(1),?z)),
     +(?z,?x_3) = +(+(?x_3,1),+(-(1),?z)),
     +(?z,+(+(?x,?y_4),?z_4)) = +(?x,+(+(?y_4,?z_4),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     ?x = +(?x,+(1,-(1))),
     +(+(+(?x,?y),?y_3),?z_3) = +(?x,+(?y,+(?y_3,?z_3))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(0,?z) = +(1,+(-(1),?z)),
     +(?x_3,?z) = +(+(?x_3,1),+(-(1),?z)),
     +(+(+(?x,?y_4),?z_4),?z) = +(?x,+(+(?y_4,?z_4),?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(0,+(?z,?z_1)) = +(+(1,+(-(1),?z)),?z_1),
     +(?x_4,+(?z,?z_1)) = +(+(+(?x_4,1),+(-(1),?z)),?z_1),
     +(+(+(?x,?y_5),?z_5),+(?z,?z_1)) = +(+(?x,+(+(?y_5,?z_5),?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     0 = +(+(1,+(-(1),1)),-(1)),
     ?x_3 = +(+(+(?x_3,1),+(-(1),1)),-(1)),
     +(+(?x,?y_4),?z_4) = +(+(?x,+(+(?y_4,?z_4),1)),-(1)),
     +(+(?x_4,+(?x_5,+(?y_5,?y))),?z) = +(?x_4,+(+(?x_5,?y_5),+(?y,?z))),
     +(+(?x_4,?y),?z) = +(?x_4,+(0,+(?y,?z))),
     +(+(?x_4,0),?z) = +(?x_4,+(1,+(-(1),?z))),
     +(+(?x_4,?x_7),?z) = +(?x_4,+(+(?x_7,1),+(-(1),?z))),
     +(+(?x_4,+(+(?x,?y_8),?z_8)),?z) = +(?x_4,+(?x,+(+(?y_8,?z_8),?z))),
     +(+(?x_4,+(?y,?x)),?z) = +(?x_4,+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_4,+(?x,?y)),?z) = +(?x_4,+(?x,+(?y,?z))),
     ?y = +(?y,0),
     0 = +(-(1),1),
     ?x_2 = +(-(1),+(?x_2,1)),
     +(+(?x,?y_3),?z_3) = +(+(?y_3,?z_3),?x),
     +(?x_4,+(?y_4,?y)) = +(?y,+(?x_4,?y_4)),
     ?x = +(+(1,?x),-(1)),
     +(+(?x_4,?x),?y) = +(?x_4,+(?y,?x)),
     +(?x,+(?y,?z_5)) = +(+(?y,?x),?z_5) ]
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 <+(1,-(1)), 0> by Rules <0, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <+(+(?x_3,+(?y_3,1)),-(1)), +(?x_3,?y_3)> by Rules <4, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],3),([],2)], []>
 joinable by a reduction of rules <[([],4),([(+,2)],2)], []>
Critical Pair <+(+(1,?x_4),-(1)), ?x_4> by Rules <5, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],5),([],2)], []>
Critical Pair <+(?x_2,?x), +(+(?x_2,0),?x)> by Rules <0, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],5),([(+,1)],0)]>
 joinable by a reduction of rules <[], [([],4),([(+,2)],0)]>
Critical Pair <+(?x_2,0), +(+(?x_2,1),-(1))> by Rules <1, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[([],5),([],0)], [([],2)]>
 joinable by a reduction of rules <[], [([],4),([(+,2)],1)]>
Critical Pair <+(?x_2,?x_1), +(+(?x_2,+(?x_1,1)),-(1))> by Rules <2, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],3),([],2)]>
 joinable by a reduction of rules <[], [([],4),([(+,2)],2)]>
Critical Pair <+(?x_2,+(?x_3,+(?y_3,?z_3))), +(+(?x_2,+(?x_3,?y_3)),?z_3)> by Rules <4, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],3)], [([],4)]>
Critical Pair <+(?x_2,+(?y_4,?x_4)), +(+(?x_2,?x_4),?y_4)> by Rules <5, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],5)], [([],4)]>
Critical Pair <+(?x,?z_3), +(0,+(?x,?z_3))> by Rules <0, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <+(0,?z_3), +(1,+(-(1),?z_3))> by Rules <1, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3),([(+,1)],1)]>
Critical Pair <+(?x_1,?z_3), +(+(?x_1,1),+(-(1),?z_3))> by Rules <2, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3),([(+,1)],2)]>
Critical Pair <+(+(+(?x_2,?y_2),?z_2),?z_3), +(?x_2,+(+(?y_2,?z_2),?z_3))> by Rules <3, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],4)], [([],3)]>
Critical Pair <+(+(?y_4,?x_4),?z_3), +(?x_4,+(?y_4,?z_3))> by Rules <5, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],5)], [([],3)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <3, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],4)], [([],4)]>
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 <[([(+,1)],3)], [([],3)]>
Critical Pair <+(+(0,?y_2),?z_2), +(?y_2,?z_2)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([(+,1)],0)], []>
Critical Pair <+(?y_4,0), ?y_4> by Rules <5, 0> preceded by []
 joinable by a reduction of rules <[([],5),([],0)], []>
Critical Pair <+(-(1),1), 0> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],5),([],1)], []>
Critical Pair <+(?x_3,+(1,-(1))), ?x_3> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([],3),([],2)], []>
Critical Pair <+(-(1),+(?x_1,1)), ?x_1> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],5),([],2)], []>
Critical Pair <+(?x_3,+(?y_3,+(?y_2,?z_2))), +(+(+(?x_3,?y_3),?y_2),?z_2)> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([],3)], [([],4)]>
Critical Pair <+(+(?y_2,?z_2),?x_4), +(+(?x_4,?y_2),?z_2)> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([],5)], [([],4)]>
Critical Pair <+(?y_4,+(?x_3,?y_3)), +(?x_3,+(?y_3,?y_4))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5)], [([],3)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 9 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-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,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (8)+(2)*x1+(4)*x1*x1
  0:= (2)
  1:= 0
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<+(1,-(1)), 0> --> <0, 0> => yes
PCP_in(symP,S):
<+(+(1,?y_3),-(1)), ?y_3> --> <+(+(1,?y_3),-(1)), ?y_3> => no
<+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> --> <+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> => no
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
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <+(?x,0), ?x> => no
<0, +(-(1),1)> --> <0, +(-(1),1)> => no
<?x, +(?x,+(1,-(1)))> --> <?x, +(?x,0)> => no
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, +(-(1),+(?x,1))> => no
check joinability condition:
check modulo reachablity from ?y_3 to +(+(1,?y_3),-(1)): maybe not reachable
check modulo reachablity from +(?x_1,?y_1) to +(+(?x_1,+(?y_1,1)),-(1)): 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
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo joinability of +(?x,0) and ?x: joinable by {2}
check modulo reachablity from 0 to +(-(1),1): maybe not reachable
check modulo joinability of ?x and +(?x,0): joinable by {2}
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from ?x to +(-(1),+(?x,1)): maybe not reachable
failed
failure(Step 1)
   [ +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
Added S-Rules:
   [ +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<+(1,-(1)), 0> --> <0, 0> => yes
CP_in(symP,S):
<+(+(?x,+(?y,1)),-(1)), +(?x,?y)> --> <+(+(?x,+(?y,1)),-(1)), +(?x,?y)> => no
<+(+(1,?y),-(1)), ?y> --> <+(+(1,?y),-(1)), ?y> => no
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
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <+(?x,0), ?x> => no
<0, +(-(1),1)> --> <0, +(-(1),1)> => no
<?x, +(?x,+(1,-(1)))> --> <?x, +(?x,0)> => no
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, +(-(1),+(?x,1))> => no
check joinability condition:
check modulo reachablity from +(?x,?y) to +(+(?x,+(?y,1)),-(1)): maybe not reachable
check modulo reachablity from ?y to +(+(1,?y),-(1)): 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
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo joinability of +(?x,0) and ?x: maybe not joinable
check modulo reachablity from 0 to +(-(1),1): maybe not reachable
check modulo joinability of ?x and +(?x,0): maybe not joinable
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from ?x to +(-(1),+(?x,1)): maybe not reachable
failed
failure(Step 2)
   [ +(+(1,?y),-(1)) -> ?y,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
Added S-Rules:
   [ +(+(1,?y),-(1)) -> ?y,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (8)+(2)*x1+(4)*x1*x1
  0:= (2)
  1:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<1, 1> --> <1, 1> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(?z_4,-(1)), +(-(1),?z_4)> --> <+(?z_4,-(1)), +(-(1),?z_4)> => yes
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_5), +(?x_5,1)> --> <+(1,?x_5), +(?x_5,1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
PCP_in(symP,S):
<+(+(1,?y_3),-(1)), ?y_3> --> <?y_3, ?y_3> => yes
<+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> --> <+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> => no
<+(+(?x_3,1),-(1)), ?x_3> --> <?x_3, ?x_3> => yes
<+(+(+(1,?y_2),?z_2),-(1)), +(?y_2,?z_2)> --> <+(+(+(1,?y_2),?z_2),-(1)), +(?y_2,?z_2)> => no
<+(1,+(?x_3,-(1))), ?x_3> --> <+(1,+(?x_3,-(1))), ?x_3> => no
<+(1,+(+(-(1),?y_2),?z_2)), +(?y_2,?z_2)> --> <+(1,+(+(-(1),?y_2),?z_2)), +(?y_2,?z_2)> => no
<+(-(1),+(1,?y_3)), ?y_3> --> <+(-(1),+(1,?y_3)), ?y_3> => no
<+(-(1),+(?x_1,+(?y_1,1))), +(?x_1,?y_1)> --> <+(-(1),+(?x_1,+(?y_1,1))), +(?x_1,?y_1)> => no
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,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,1),-(1))> --> <?x, ?x> => yes
<0, +(-(1),1)> --> <0, 0> => yes
<?x, +(?x,+(1,-(1)))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, ?x> => yes
<?y, +(1,+(?y,-(1)))> --> <?y, +(1,+(?y,-(1)))> => no
<+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> --> <+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> => no
<+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> --> <+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> => no
<?y, +(-(1),+(1,?y))> --> <?y, +(-(1),+(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_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, ?x> => yes
<+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> --> <+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> => no
<?z, +(+(1,-(1)),?z)> --> <?z, ?z> => yes
<+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> --> <+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> => no
<?z, +(+(-(1),?z),1)> --> <?z, +(+(-(1),?z),1)> => no
<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
<0, +(1,-(1))> --> <0, 0> => yes
<+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> --> <+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> => no
<?x, +(+(-(1),?x),1)> --> <?x, +(+(-(1),?x),1)> => no
<+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> --> <+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> => no
<?x, +(+(?x,1),-(1))> --> <?x, ?x> => yes
check joinability condition:
check modulo reachablity from +(?x_1,?y_1) to +(+(?x_1,+(?y_1,1)),-(1)): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(+(+(1,?y_2),?z_2),-(1)): maybe not reachable
check modulo reachablity from ?x_3 to +(1,+(?x_3,-(1))): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(1,+(+(-(1),?y_2),?z_2)): maybe not reachable
check modulo reachablity from ?y_3 to +(-(1),+(1,?y_3)): maybe not reachable
check modulo reachablity from +(?x_1,?y_1) to +(-(1),+(?x_1,+(?y_1,1))): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from ?y to +(1,+(?y,-(1))): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(+(1,?y),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,+(1,?y)),-(1)): maybe not reachable
check modulo reachablity from ?y to +(-(1),+(1,?y)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(1,+(+(-(1),?z),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,1),+(-(1),?z)): maybe not reachable
check modulo reachablity from ?z to +(+(-(1),?z),1): maybe not reachable
check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(-(1),+(+(?x,1),?z_1)): maybe not reachable
check modulo reachablity from ?x to +(+(-(1),?x),1): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,-(1)),+(?x,1)): maybe not reachable
failed
failure(Step 4)
   [ +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
Added S-Rules:
   [ +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
Added P-Rules:
   [ ]
STEP: 5 (linear)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<1, 1> --> <1, 1> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(?z_4,-(1)), +(-(1),?z_4)> --> <+(?z_4,-(1)), +(-(1),?z_4)> => yes
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_5), +(?x_5,1)> --> <+(1,?x_5), +(?x_5,1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
CP_in(symP,S):
<+(+(?x,+(?y,1)),-(1)), +(?x,?y)> --> <+(+(?x,+(?y,1)),-(1)), +(?x,?y)> => no
<+(-(1),+(?x,+(?y,1))), +(?x,?y)> --> <+(-(1),+(?x,+(?y,1))), +(?x,?y)> => no
<+(+(+(1,?y),?z),-(1)), +(?y,?z)> --> <+(+(+(1,?y),?z),-(1)), +(?y,?z)> => no
<+(1,+(+(-(1),?y),?z)), +(?y,?z)> --> <+(1,+(+(-(1),?y),?z)), +(?y,?z)> => no
<+(+(1,?y),-(1)), ?y> --> <?y, ?y> => yes
<+(+(?x,1),-(1)), ?x> --> <?x, ?x> => yes
<+(1,+(?x,-(1))), ?x> --> <+(1,+(?x,-(1))), ?x> => no
<+(-(1),+(1,?y)), ?y> --> <+(-(1),+(1,?y)), ?y> => no
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,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,1),-(1))> --> <?x, ?x> => yes
<0, +(-(1),1)> --> <0, 0> => yes
<?x, +(?x,+(1,-(1)))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, ?x> => yes
<?y, +(1,+(?y,-(1)))> --> <?y, +(1,+(?y,-(1)))> => no
<+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> --> <+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> => no
<+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> --> <+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> => no
<?y, +(-(1),+(1,?y))> --> <?y, +(-(1),+(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_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, ?x> => yes
<+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> --> <+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> => no
<?z, +(+(1,-(1)),?z)> --> <?z, ?z> => yes
<+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> --> <+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> => no
<?z, +(+(-(1),?z),1)> --> <?z, +(+(-(1),?z),1)> => no
<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
<0, +(1,-(1))> --> <0, 0> => yes
<+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> --> <+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> => no
<?x, +(+(-(1),?x),1)> --> <?x, +(+(-(1),?x),1)> => no
<+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> --> <+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> => no
<?x, +(+(?x,1),-(1))> --> <?x, ?x> => yes
check joinability condition:
check modulo reachablity from +(?x,?y) to +(+(?x,+(?y,1)),-(1)): maybe not reachable
check modulo reachablity from +(?x,?y) to +(-(1),+(?x,+(?y,1))): maybe not reachable
check modulo reachablity from +(?y,?z) to +(+(+(1,?y),?z),-(1)): maybe not reachable
check modulo reachablity from +(?y,?z) to +(1,+(+(-(1),?y),?z)): maybe not reachable
check modulo reachablity from ?x to +(1,+(?x,-(1))): maybe not reachable
check modulo reachablity from ?y to +(-(1),+(1,?y)): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from ?y to +(1,+(?y,-(1))): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(+(1,?y),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,+(1,?y)),-(1)): maybe not reachable
check modulo reachablity from ?y to +(-(1),+(1,?y)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(1,+(+(-(1),?z),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,1),+(-(1),?z)): maybe not reachable
check modulo reachablity from ?z to +(+(-(1),?z),1): maybe not reachable
check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(-(1),+(+(?x,1),?z_1)): maybe not reachable
check modulo reachablity from ?x to +(+(-(1),?x),1): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,-(1)),+(?x,1)): maybe not reachable
failed
failure(Step 5)
   [ +(1,+(?x,-(1))) -> ?x,
     +(-(1),+(1,?y)) -> ?y,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
Added S-Rules:
   [ +(1,+(?x,-(1))) -> ?x,
     +(-(1),+(1,?y)) -> ?y,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
Added P-Rules:
   [ ]
STEP: 6 (relative)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  -:= (3)+(8)*x1*x1
  0:= (12)
  1:= 0
retract +(0,?x) -> ?x
retract +(+(?x,1),-(1)) -> ?x
retract +(+(1,?y_3),-(1)) -> ?y_3
retract +(?x,0) -> ?x
retract +(1,+(-(1),?z)) -> ?z
retract +(-(1),+(?x,1)) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  -:= (4)*x1*x1
  0:= 0
  1:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x,
     +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<1, 1> --> <1, 1> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<+(?z_8,-(1)), +(-(1),?z_8)> --> <+(?z_8,-(1)), +(-(1),?z_8)> => yes
<+(?x_9,-(1)), +(?x_9,-(1))> --> <+(?x_9,-(1)), +(?x_9,-(1))> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(?z_4,-(1)), +(-(1),?z_4)> --> <+(?z_4,-(1)), +(-(1),?z_4)> => yes
<+(?x_6,-(1)), +(?x_6,-(1))> --> <+(?x_6,-(1)), +(?x_6,-(1))> => yes
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_5), +(?x_5,1)> --> <+(1,?x_5), +(?x_5,1)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(1,?y_7), +(1,?y_7)> --> <+(1,?y_7), +(1,?y_7)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(-(1),?z_8), +(-(1),?z_8)> --> <+(-(1),?z_8), +(-(1),?z_8)> => yes
<+(-(1),?x_9), +(?x_9,-(1))> --> <+(-(1),?x_9), +(?x_9,-(1))> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_1), +(?x_1,1)> --> <+(1,?x_1), +(?x_1,1)> => yes
<+(1,?y_2), +(1,?y_2)> --> <+(1,?y_2), +(1,?y_2)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),?z_4), +(-(1),?z_4)> --> <+(-(1),?z_4), +(-(1),?z_4)> => yes
<1, 1> --> <1, 1> => yes
<+(-(1),?x_6), +(?x_6,-(1))> --> <+(-(1),?x_6), +(?x_6,-(1))> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(0,1), 1> --> <1, 1> => yes
<+(?x_5,1), +(?x_5,1)> --> <+(?x_5,1), +(?x_5,1)> => yes
<+(?y_7,1), +(1,?y_7)> --> <+(?y_7,1), +(1,?y_7)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(0,1), 1> --> <1, 1> => yes
<+(?x_1,1), +(?x_1,1)> --> <+(?x_1,1), +(?x_1,1)> => yes
<+(?y_2,1), +(1,?y_2)> --> <+(?y_2,1), +(1,?y_2)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
PCP_in(symP,S):
<+(+(1,?y_3),-(1)), ?y_3> --> <?y_3, ?y_3> => yes
<+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> --> <+(+(?x_1,+(?y_1,1)),-(1)), +(?x_1,?y_1)> => no
<+(+(?x_3,1),-(1)), ?x_3> --> <?x_3, ?x_3> => yes
<+(+(+(1,?y_2),?z_2),-(1)), +(?y_2,?z_2)> --> <+(+(+(1,?y_2),?z_2),-(1)), +(?y_2,?z_2)> => no
<+(1,+(?x_3,-(1))), ?x_3> --> <?x_3, ?x_3> => yes
<+(1,+(+(-(1),?y_2),?z_2)), +(?y_2,?z_2)> --> <+(1,+(+(-(1),?y_2),?z_2)), +(?y_2,?z_2)> => no
<+(-(1),+(1,?y_3)), ?y_3> --> <?y_3, ?y_3> => yes
<+(-(1),+(?x_1,+(?y_1,1))), +(?x_1,?y_1)> --> <+(-(1),+(?x_1,+(?y_1,1))), +(?x_1,?y_1)> => no
<+(1,+(-(1),?y_3)), ?y_3> --> <?y_3, ?y_3> => yes
<+(1,+(?x_1,+(?y_1,-(1)))), +(?x_1,?y_1)> --> <+(1,+(?x_1,+(?y_1,-(1)))), +(?x_1,?y_1)> => no
<+(-(1),+(?x_3,1)), ?x_3> --> <?x_3, ?x_3> => yes
<+(-(1),+(+(1,?y_2),?z_2)), +(?y_2,?z_2)> --> <+(-(1),+(+(1,?y_2),?z_2)), +(?y_2,?z_2)> => no
<+(+(?x_3,-(1)),1), ?x_3> --> <?x_3, ?x_3> => yes
<+(+(+(-(1),?y_2),?z_2),1), +(?y_2,?z_2)> --> <+(+(+(-(1),?y_2),?z_2),1), +(?y_2,?z_2)> => no
<+(+(-(1),?y_3),1), ?y_3> --> <?y_3, ?y_3> => yes
<+(+(?x_1,+(?y_1,-(1))),1), +(?x_1,?y_1)> --> <+(+(?x_1,+(?y_1,-(1))),1), +(?x_1,?y_1)> => no
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,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,1),-(1))> --> <?x, ?x> => yes
<0, +(-(1),1)> --> <0, 0> => yes
<?x, +(?x,+(1,-(1)))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, ?x> => yes
<?y, +(1,+(?y,-(1)))> --> <?y, ?y> => yes
<+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> --> <+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> => no
<+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> --> <+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> => no
<?y, +(-(1),+(1,?y))> --> <?y, ?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
<+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> --> <+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> => no
<?z, +(+(1,-(1)),?z)> --> <?z, ?z> => yes
<+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> --> <+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> => no
<?z, +(+(-(1),?z),1)> --> <?z, ?z> => yes
<+(0,?z), +(-(1),+(1,?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, ?x> => yes
<0, +(1,-(1))> --> <0, 0> => yes
<+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> --> <+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> => no
<?x, +(+(-(1),?x),1)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> --> <+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> => no
<?x, +(+(?x,1),-(1))> --> <?x, ?x> => yes
<+(?x,?z_1), +(1,+(+(?x,-(1)),?z_1))> --> <+(?x,?z_1), +(1,+(+(?x,-(1)),?z_1))> => no
<?x, +(+(1,?x),-(1))> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,1),+(?x,-(1)))> --> <+(?x_1,?x), +(+(?x_1,1),+(?x,-(1)))> => no
<?x, +(+(?x,-(1)),1)> --> <?x, ?x> => yes
<+(?y,?z_1), +(-(1),+(+(1,?y),?z_1))> --> <+(?y,?z_1), +(-(1),+(+(1,?y),?z_1))> => no
<?y, +(+(-(1),1),?y)> --> <?y, ?y> => yes
<+(?x_1,?y), +(+(?x_1,-(1)),+(1,?y))> --> <+(?x_1,?y), +(+(?x_1,-(1)),+(1,?y))> => no
<?y, +(+(1,?y),-(1))> --> <?y, ?y> => yes
<?z, +(-(1),+(?z,1))> --> <?z, ?z> => yes
<+(?z,?z_1), +(+(-(1),?z),+(1,?z_1))> --> <+(?z,?z_1), +(+(-(1),?z),+(1,?z_1))> => no
<+(?x_1,?z), +(+(?x_1,+(-(1),?z)),1)> --> <+(?x_1,?z), +(+(?x_1,+(-(1),?z)),1)> => no
<?z, +(1,+(-(1),?z))> --> <?z, ?z> => yes
<?x, +(?x,+(-(1),1))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,-(1)),+(1,?z_1))> --> <+(?x,?z_1), +(+(?x,-(1)),+(1,?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,-(1))),1)> --> <+(?x_1,?x), +(+(?x_1,+(?x,-(1))),1)> => no
<?x, +(1,+(?x,-(1)))> --> <?x, ?x> => yes
check joinability condition:
check modulo reachablity from +(?x_1,?y_1) to +(+(?x_1,+(?y_1,1)),-(1)): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(+(+(1,?y_2),?z_2),-(1)): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(1,+(+(-(1),?y_2),?z_2)): maybe not reachable
check modulo reachablity from +(?x_1,?y_1) to +(-(1),+(?x_1,+(?y_1,1))): maybe not reachable
check modulo reachablity from +(?x_1,?y_1) to +(1,+(?x_1,+(?y_1,-(1)))): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(-(1),+(+(1,?y_2),?z_2)): maybe not reachable
check modulo reachablity from +(?y_2,?z_2) to +(+(+(-(1),?y_2),?z_2),1): maybe not reachable
check modulo reachablity from +(?x_1,?y_1) to +(+(?x_1,+(?y_1,-(1))),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(+(1,?y),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,+(1,?y)),-(1)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(1,+(+(-(1),?z),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,1),+(-(1),?z)): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(-(1),+(+(?x,1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,-(1)),+(?x,1)): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(1,+(+(?x,-(1)),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,1),+(?x,-(1))): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(-(1),+(+(1,?y),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,-(1)),+(1,?y)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(+(-(1),?z),+(1,?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,+(-(1),?z)),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,-(1)),+(1,?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,-(1))),1): maybe not reachable
failed
failure(Step 7)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 8 (linear)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x,
     +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<1, 1> --> <1, 1> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<+(?z_8,-(1)), +(-(1),?z_8)> --> <+(?z_8,-(1)), +(-(1),?z_8)> => yes
<+(?x_9,-(1)), +(?x_9,-(1))> --> <+(?x_9,-(1)), +(?x_9,-(1))> => yes
<+(0,-(1)), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(?z_4,-(1)), +(-(1),?z_4)> --> <+(?z_4,-(1)), +(-(1),?z_4)> => yes
<+(?x_6,-(1)), +(?x_6,-(1))> --> <+(?x_6,-(1)), +(?x_6,-(1))> => yes
<0, 0> --> <0, 0> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_5), +(?x_5,1)> --> <+(1,?x_5), +(?x_5,1)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(1,?y_7), +(1,?y_7)> --> <+(1,?y_7), +(1,?y_7)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
<1, 1> --> <1, 1> => yes
<+(-(1),?z_8), +(-(1),?z_8)> --> <+(-(1),?z_8), +(-(1),?z_8)> => yes
<+(-(1),?x_9), +(?x_9,-(1))> --> <+(-(1),?x_9), +(?x_9,-(1))> => yes
<+(1,-(1)), 0> --> <0, 0> => yes
<+(1,0), 1> --> <1, 1> => yes
<+(1,?x_1), +(?x_1,1)> --> <+(1,?x_1), +(?x_1,1)> => yes
<+(1,?y_2), +(1,?y_2)> --> <+(1,?y_2), +(1,?y_2)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(-(1),0), -(1)> --> <-(1), -(1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(-(1),?z_4), +(-(1),?z_4)> --> <+(-(1),?z_4), +(-(1),?z_4)> => yes
<1, 1> --> <1, 1> => yes
<+(-(1),?x_6), +(?x_6,-(1))> --> <+(-(1),?x_6), +(?x_6,-(1))> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(0,1), 1> --> <1, 1> => yes
<+(?x_5,1), +(?x_5,1)> --> <+(?x_5,1), +(?x_5,1)> => yes
<+(?y_7,1), +(1,?y_7)> --> <+(?y_7,1), +(1,?y_7)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
<+(-(1),1), 0> --> <0, 0> => yes
<+(0,1), 1> --> <1, 1> => yes
<+(?x_1,1), +(?x_1,1)> --> <+(?x_1,1), +(?x_1,1)> => yes
<+(?y_2,1), +(1,?y_2)> --> <+(?y_2,1), +(1,?y_2)> => yes
<-(1), -(1)> --> <-(1), -(1)> => yes
CP_in(symP,S):
<+(+(?x,+(?y,1)),-(1)), +(?x,?y)> --> <+(+(?x,+(?y,1)),-(1)), +(?x,?y)> => no
<+(-(1),+(?x,+(?y,1))), +(?x,?y)> --> <+(-(1),+(?x,+(?y,1))), +(?x,?y)> => no
<+(1,+(?x,+(?y,-(1)))), +(?x,?y)> --> <+(1,+(?x,+(?y,-(1)))), +(?x,?y)> => no
<+(+(?x,+(?y,-(1))),1), +(?x,?y)> --> <+(+(?x,+(?y,-(1))),1), +(?x,?y)> => no
<+(+(+(1,?y),?z),-(1)), +(?y,?z)> --> <+(+(+(1,?y),?z),-(1)), +(?y,?z)> => no
<+(1,+(+(-(1),?y),?z)), +(?y,?z)> --> <+(1,+(+(-(1),?y),?z)), +(?y,?z)> => no
<+(-(1),+(+(1,?y),?z)), +(?y,?z)> --> <+(-(1),+(+(1,?y),?z)), +(?y,?z)> => no
<+(+(+(-(1),?y),?z),1), +(?y,?z)> --> <+(+(+(-(1),?y),?z),1), +(?y,?z)> => no
<+(+(1,?y),-(1)), ?y> --> <?y, ?y> => yes
<+(+(?x,1),-(1)), ?x> --> <?x, ?x> => yes
<+(1,+(?x,-(1))), ?x> --> <?x, ?x> => yes
<+(-(1),+(1,?y)), ?y> --> <?y, ?y> => yes
<+(1,+(-(1),?y)), ?y> --> <?y, ?y> => yes
<+(-(1),+(?x,1)), ?x> --> <?x, ?x> => yes
<+(+(?x,-(1)),1), ?x> --> <?x, ?x> => yes
<+(+(-(1),?y),1), ?y> --> <?y, ?y> => yes
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,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,1),-(1))> --> <?x, ?x> => yes
<0, +(-(1),1)> --> <0, 0> => yes
<?x, +(?x,+(1,-(1)))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> --> <+(?x,?z_1), +(+(?x,1),+(-(1),?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> --> <+(?x_1,?x), +(+(?x_1,+(?x,1)),-(1))> => no
<?x, +(-(1),+(?x,1))> --> <?x, ?x> => yes
<?y, +(1,+(?y,-(1)))> --> <?y, ?y> => yes
<+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> --> <+(?y,?z_1), +(+(1,?y),+(-(1),?z_1))> => no
<+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> --> <+(?x_1,?y), +(+(?x_1,+(1,?y)),-(1))> => no
<?y, +(-(1),+(1,?y))> --> <?y, ?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
<+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> --> <+(?z,?z_1), +(1,+(+(-(1),?z),?z_1))> => no
<?z, +(+(1,-(1)),?z)> --> <?z, ?z> => yes
<+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> --> <+(?x_1,?z), +(+(?x_1,1),+(-(1),?z))> => no
<?z, +(+(-(1),?z),1)> --> <?z, ?z> => yes
<+(0,?z), +(-(1),+(1,?z))> --> <?z, ?z> => yes
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, ?x> => yes
<0, +(1,-(1))> --> <0, 0> => yes
<+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> --> <+(?x,?z_1), +(-(1),+(+(?x,1),?z_1))> => no
<?x, +(+(-(1),?x),1)> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> --> <+(?x_1,?x), +(+(?x_1,-(1)),+(?x,1))> => no
<?x, +(+(?x,1),-(1))> --> <?x, ?x> => yes
<+(?x,?z_1), +(1,+(+(?x,-(1)),?z_1))> --> <+(?x,?z_1), +(1,+(+(?x,-(1)),?z_1))> => no
<?x, +(+(1,?x),-(1))> --> <?x, ?x> => yes
<+(?x_1,?x), +(+(?x_1,1),+(?x,-(1)))> --> <+(?x_1,?x), +(+(?x_1,1),+(?x,-(1)))> => no
<?x, +(+(?x,-(1)),1)> --> <?x, ?x> => yes
<+(?y,?z_1), +(-(1),+(+(1,?y),?z_1))> --> <+(?y,?z_1), +(-(1),+(+(1,?y),?z_1))> => no
<?y, +(+(-(1),1),?y)> --> <?y, ?y> => yes
<+(?x_1,?y), +(+(?x_1,-(1)),+(1,?y))> --> <+(?x_1,?y), +(+(?x_1,-(1)),+(1,?y))> => no
<?y, +(+(1,?y),-(1))> --> <?y, ?y> => yes
<?z, +(-(1),+(?z,1))> --> <?z, ?z> => yes
<+(?z,?z_1), +(+(-(1),?z),+(1,?z_1))> --> <+(?z,?z_1), +(+(-(1),?z),+(1,?z_1))> => no
<+(?x_1,?z), +(+(?x_1,+(-(1),?z)),1)> --> <+(?x_1,?z), +(+(?x_1,+(-(1),?z)),1)> => no
<?z, +(1,+(-(1),?z))> --> <?z, ?z> => yes
<?x, +(?x,+(-(1),1))> --> <?x, ?x> => yes
<+(?x,?z_1), +(+(?x,-(1)),+(1,?z_1))> --> <+(?x,?z_1), +(+(?x,-(1)),+(1,?z_1))> => no
<+(?x_1,?x), +(+(?x_1,+(?x,-(1))),1)> --> <+(?x_1,?x), +(+(?x_1,+(?x,-(1))),1)> => no
<?x, +(1,+(?x,-(1)))> --> <?x, ?x> => yes
check joinability condition:
check modulo reachablity from +(?x,?y) to +(+(?x,+(?y,1)),-(1)): maybe not reachable
check modulo reachablity from +(?x,?y) to +(-(1),+(?x,+(?y,1))): maybe not reachable
check modulo reachablity from +(?x,?y) to +(1,+(?x,+(?y,-(1)))): maybe not reachable
check modulo reachablity from +(?x,?y) to +(+(?x,+(?y,-(1))),1): maybe not reachable
check modulo reachablity from +(?y,?z) to +(+(+(1,?y),?z),-(1)): maybe not reachable
check modulo reachablity from +(?y,?z) to +(1,+(+(-(1),?y),?z)): maybe not reachable
check modulo reachablity from +(?y,?z) to +(-(1),+(+(1,?y),?z)): maybe not reachable
check modulo reachablity from +(?y,?z) to +(+(+(-(1),?y),?z),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,1),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,1)),-(1)): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(+(1,?y),+(-(1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,+(1,?y)),-(1)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(1,+(+(-(1),?z),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,1),+(-(1),?z)): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(-(1),+(+(?x,1),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,-(1)),+(?x,1)): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(1,+(+(?x,-(1)),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,1),+(?x,-(1))): maybe not reachable
check modulo reachablity from +(?y,?z_1) to +(-(1),+(+(1,?y),?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?y) to +(+(?x_1,-(1)),+(1,?y)): maybe not reachable
check modulo reachablity from +(?z,?z_1) to +(+(-(1),?z),+(1,?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?z) to +(+(?x_1,+(-(1),?z)),1): maybe not reachable
check modulo reachablity from +(?x,?z_1) to +(+(?x,-(1)),+(1,?z_1)): maybe not reachable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,+(?x,-(1))),1): maybe not reachable
failed
failure(Step 8)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 9 (relative)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x,
     +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(1,?y_3),-(1)) -> ?y_3,
     +(?x,0) -> ?x,
     +(1,+(-(1),?z)) -> ?z,
     +(-(1),1) -> 0,
     +(-(1),+(?x,1)) -> ?x,
     +(1,+(?x_3,-(1))) -> ?x_3,
     +(-(1),+(1,?y_3)) -> ?y_3,
     +(+(-(1),?z),1) -> ?z,
     +(+(?x,-(1)),1) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  -:= (8)+(8)*x1*x1
  0:= (5)
  1:= 0
retract +(0,?x) -> ?x
retract +(+(?x,1),-(1)) -> ?x
retract +(+(1,?y_3),-(1)) -> ?y_3
retract +(?x,0) -> ?x
retract +(1,+(-(1),?z)) -> ?z
retract +(-(1),+(?x,1)) -> ?x
retract +(1,+(?x_3,-(1))) -> ?x_3
retract +(-(1),+(1,?y_3)) -> ?y_3
retract +(+(-(1),?z),1) -> ?z
retract +(+(?x,-(1)),1) -> ?x
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (3)+(8)*x1
  0:= 0
  1:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
failure(no possibility remains)
unknown Reduction-Preserving Completion
check by Ordered Rewriting...
remove redundants rules and split
R-part:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x ]
E-part:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
Perform abstraction and check...
Increase tree depth and check...
Apply reduction-preserving transformation...
Rules to add:
   [ +(?y_3,0) -> ?y_3 ]
remove redundants rules and split
R-part:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,0) -> ?y_3 ]
E-part:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
Perform abstraction and check...
Increase tree depth and check...
Apply reduction-preserving transformation...
Rules to add:
   [ +(1,+(?x_4,-(1))) -> ?x_4 ]
remove redundants rules and split
R-part:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,0) -> ?y_3,
     +(1,+(?x_4,-(1))) -> ?x_4 ]
E-part:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
Perform abstraction and check...
Increase tree depth and check...
Apply reduction-preserving transformation...
Rules to add:
   [ +(1,+(-(1),?x_5)) -> ?x_5 ]
remove redundants rules and split
R-part:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,0) -> ?y_3,
     +(1,+(?x_4,-(1))) -> ?x_4,
     +(1,+(-(1),?x_5)) -> ?x_5 ]
E-part:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
Perform abstraction and check...
Increase tree depth and check...
Apply reduction-preserving transformation...
Rules to add:
   [ +(1,+(?x_7,+(?x_4,-(1)))) -> +(?x_7,?x_4) ]
remove redundants rules and split
R-part:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     +(+(?x,1),-(1)) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,0) -> ?y_3,
     +(1,+(?x_4,-(1))) -> ?x_4,
     +(1,+(-(1),?x_5)) -> ?x_5,
     +(1,+(?x_7,+(?x_4,-(1)))) -> +(?x_7,?x_4) ]
E-part:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
Perform abstraction and check...
Increase tree depth and check...
unknown Confluence by Ordered Rewriting
Direct Methods: Can't judge

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

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

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


Combined result: Can't judge
542.trs: Failure(unknown CR)
(4301 msec.)