(ignored inputs)COMMENT doi:10.4230/LIPIcs.RTA.2013.319 [115] Example 4.1 submitted by: Aart Middeldorp
Rewrite Rules:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_2,a) = +(+(?x_2,a),?x),
     +(?x_2,a) = +(+(?x_2,b),g(a)),
     +(?x_2,?x_1) = +(+(?x_2,0),?x_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),
     +(a,?z_3) = +(a,+(?x,?z_3)),
     +(a,?z_3) = +(b,+(g(a),?z_3)),
     +(?x_1,?z_3) = +(0,+(?x_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:
   [ a = +(+(a,?y_2),?z_2),
     a = +(?x,a),
     a = +(g(a),b),
     +(?y_2,?z_2) = +(+(0,?y_2),?z_2),
     ?x_1 = +(?x_1,0),
     +(+(+(?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:
   [ +(+(a,?y_2),?z_2) = a,
     +(?x,a) = a,
     +(+(?x_3,a),?x) = +(?x_3,a),
     +(a,+(?x,?z_4)) = +(a,?z_4),
     +(g(a),b) = a,
     +(+(?x_2,b),g(a)) = +(?x_2,a),
     +(b,+(g(a),?z_3)) = +(a,?z_3),
     +(+(0,?y_2),?z_2) = +(?y_2,?z_2),
     +(?x,0) = ?x,
     +(+(?x_3,0),?x) = +(?x_3,?x),
     +(0,+(?x,?z_4)) = +(?x,?z_4),
     a = +(+(a,?y),+(?y_1,?z_1)),
     a = +(+(a,a),?z),
     a = +(+(a,b),g(a)),
     a = +(+(a,0),?z),
     a = +(+(a,+(?x_4,?y_4)),?z),
     a = +(+(a,?y),?z),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     a = +(+(0,a),?z),
     a = +(+(0,b),g(a)),
     ?z = +(+(0,0),?z),
     +(?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,a)) = +(+(+(?x_3,?y_3),a),?z),
     +(?x_3,+(?y_3,a)) = +(+(+(?x_3,?y_3),b),g(a)),
     +(?x_3,+(?y_3,?z)) = +(+(+(?x_3,?y_3),0),?z),
     +(?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)),
     +(a,?x) = +(+(?x,a),?z),
     +(a,?x) = +(+(?x,b),g(a)),
     +(?z,?x) = +(+(?x,0),?z),
     +(+(?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,a) = +(+(?x,a),?z),
     +(?x,a) = +(+(?x,b),g(a)),
     +(?x,?z) = +(+(?x,0),?z),
     +(?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),a) = +(?x_1,+(+(?x,a),?z)),
     +(+(?x_1,?x),a) = +(?x_1,+(+(?x,b),g(a))),
     +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)),
     +(+(?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,+(a,?z_4)) = +(+(+(?x,a),?z),?z_4),
     +(?x,+(a,?z_4)) = +(+(+(?x,b),g(a)),?z_4),
     +(?x,+(?z,?z_4)) = +(+(+(?x,0),?z),?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))),
     +(+(a,?y_3),?z_3) = +(a,+(?y,+(?y_3,?z_3))),
     +(+(a,?y_3),?z_3) = +(b,+(g(a),+(?y_3,?z_3))),
     +(+(?y,?y_3),?z_3) = +(0,+(?y,+(?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,a) = +(a,+(?y,?z)),
     +(?z,a) = +(b,+(g(a),?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,+(+(?x,?y_4),?z_4)) = +(?x,+(+(?y_4,?z_4),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(+(+(?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)),
     +(a,?z) = +(a,+(?y,?z)),
     +(a,?z) = +(b,+(g(a),?z)),
     +(?y,?z) = +(0,+(?y,?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),
     +(a,+(?z,?z_1)) = +(+(a,+(?y,?z)),?z_1),
     +(a,+(?z,?z_1)) = +(+(b,+(g(a),?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),
     +(+(?x_4,+(?x_5,+(?y_5,?y))),?z) = +(?x_4,+(+(?x_5,?y_5),+(?y,?z))),
     +(+(?x_4,a),?z) = +(?x_4,+(a,+(?y,?z))),
     +(+(?x_4,a),?z) = +(?x_4,+(b,+(g(a),?z))),
     +(+(?x_4,?y),?z) = +(?x_4,+(0,+(?y,?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))),
     a = +(?y,a),
     a = +(g(a),b),
     ?y = +(?y,0),
     +(+(?x,?y_3),?z_3) = +(+(?y_3,?z_3),?x),
     +(?x_4,+(?y_4,?y)) = +(?y,+(?x_4,?y_4)),
     +(+(?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 <+(?x_2,a), +(+(?x_2,a),?x)> by Rules <0, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],4),([(+,2)],0)]>
Critical Pair <+(?x_2,a), +(+(?x_2,b),g(a))> by Rules <1, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],4),([(+,2)],1)]>
Critical Pair <+(?x_2,?x_1), +(+(?x_2,0),?x_1)> by Rules <2, 3> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],5),([(+,1)],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 <+(a,?z_3), +(a,+(?x,?z_3))> by Rules <0, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([],0)], [([],0)]>
Critical Pair <+(a,?z_3), +(b,+(g(a),?z_3))> by Rules <1, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3),([(+,1)],1)]>
Critical Pair <+(?x_1,?z_3), +(0,+(?x_1,?z_3))> by Rules <2, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],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 <+(+(a,?y_2),?z_2), a> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[([(+,1)],0),([],0)], []>
 joinable by a reduction of rules <[([],4),([],0)], []>
Critical Pair <+(?y_4,a), a> by Rules <5, 0> preceded by []
 joinable by a reduction of rules <[([],5),([],0)], []>
Critical Pair <+(g(a),b), a> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],5),([],1)], []>
Critical Pair <+(+(0,?y_2),?z_2), +(?y_2,?z_2)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([(+,1)],2)], []>
Critical Pair <+(?y_4,0), ?y_4> 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:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (8)
  a:= 0
  b:= (10)
  g:= (4)*x1+(6)*x1*x1
retract +(b,g(a)) -> a
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (12)
  a:= (4)
  b:= 0
  g:= (12)+(8)*x1+(6)*x1*x1
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<+(a,?z_1), +(a,+(?x,?z_1))> --> <a, a> => yes
<a, +(+(a,?y_1),?z_1)> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,a),?x)> --> <+(?x_1,a), +(+(?x_1,a),?x)> => no
<a, +(?x,a)> --> <a, +(?x,a)> => no
<+(a,?z), +(b,+(g(a),?z))> --> <a, +(b,+(g(a),?z))> => no
<+(?x,a), +(+(?x,b),g(a))> --> <+(?x,a), +(+(?x,b),g(a))> => no
<a, +(g(a),b)> --> <a, +(g(a),b)> => 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,a) to +(+(?x_1,a),?x): maybe not reachable
check modulo reachablity from a to +(?x,a): maybe not reachable
check modulo reachablity from a to +(b,+(g(a),?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,b),g(a)): maybe not reachable
check modulo reachablity from a to +(g(a),b): 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)
   [ +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<+(a,?z_1), +(a,+(?x,?z_1))> --> <a, a> => yes
<a, +(+(a,?y_1),?z_1)> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,a),?x)> --> <+(?x_1,a), +(+(?x_1,a),?x)> => no
<a, +(?x,a)> --> <a, +(?x,a)> => no
<+(a,?z), +(b,+(g(a),?z))> --> <a, +(b,+(g(a),?z))> => no
<+(?x,a), +(+(?x,b),g(a))> --> <+(?x,a), +(+(?x,b),g(a))> => no
<a, +(g(a),b)> --> <a, +(g(a),b)> => 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,a) to +(+(?x_1,a),?x): maybe not reachable
check modulo reachablity from a to +(?x,a): maybe not reachable
check modulo reachablity from a to +(b,+(g(a),?z)): maybe not reachable
check modulo reachablity from +(?x,a) to +(+(?x,b),g(a)): maybe not reachable
check modulo reachablity from a to +(g(a),b): 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)
   [ +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
Added S-Rules:
   [ +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (8)
  a:= 0
  b:= (10)
  g:= (4)*x1+(6)*x1*x1
retract +(b,g(a)) -> a
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  0:= (12)
  a:= (4)
  b:= 0
  g:= (12)+(8)*x1+(6)*x1*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<0, 0> --> <0, 0> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<0, 0> --> <0, 0> => yes
PCP_in(symP,S):
CP(S,symP):
<+(a,?z_1), +(a,+(?x,?z_1))> --> <a, a> => yes
<a, +(+(a,?y_1),?z_1)> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,a),?x)> --> <a, a> => yes
<a, +(?x,a)> --> <a, a> => yes
<+(a,?z), +(b,+(g(a),?z))> --> <a, +(b,+(g(a),?z))> => no
<+(?x,a), +(+(?x,b),g(a))> --> <a, +(+(?x,b),g(a))> => no
<a, +(g(a),b)> --> <a, a> => 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
<a, +(?x_1,+(?y_1,a))> --> <a, a> => yes
<+(a,?z_1), +(?x,+(a,?z_1))> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,?x),a)> --> <a, a> => yes
<a, +(a,?x)> --> <a, a> => yes
<+(a,?z), +(g(a),+(b,?z))> --> <a, +(g(a),+(b,?z))> => no
<+(?x,a), +(+(?x,g(a)),b)> --> <a, +(+(?x,g(a)),b)> => no
<a, +(b,g(a))> --> <a, a> => 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 reachablity from a to +(b,+(g(a),?z)): maybe not reachable
check modulo reachablity from a to +(+(?x,b),g(a)): maybe not reachable
check modulo reachablity from a to +(g(a),+(b,?z)): maybe not reachable
check modulo reachablity from a to +(+(?x,g(a)),b): maybe not reachable
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 5 (linear)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<0, 0> --> <0, 0> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<a, a> --> <a, a> => yes
<0, 0> --> <0, 0> => yes
CP_in(symP,S):
CP(S,symP):
<+(a,?z_1), +(a,+(?x,?z_1))> --> <a, a> => yes
<a, +(+(a,?y_1),?z_1)> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,a),?x)> --> <a, a> => yes
<a, +(?x,a)> --> <a, a> => yes
<+(a,?z), +(b,+(g(a),?z))> --> <a, +(b,+(g(a),?z))> => no
<+(?x,a), +(+(?x,b),g(a))> --> <a, +(+(?x,b),g(a))> => no
<a, +(g(a),b)> --> <a, a> => 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
<a, +(?x_1,+(?y_1,a))> --> <a, a> => yes
<+(a,?z_1), +(?x,+(a,?z_1))> --> <a, a> => yes
<+(?x_1,a), +(+(?x_1,?x),a)> --> <a, a> => yes
<a, +(a,?x)> --> <a, a> => yes
<+(a,?z), +(g(a),+(b,?z))> --> <a, +(g(a),+(b,?z))> => no
<+(?x,a), +(+(?x,g(a)),b)> --> <a, +(+(?x,g(a)),b)> => no
<a, +(b,g(a))> --> <a, a> => 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 reachablity from a to +(b,+(g(a),?z)): maybe not reachable
check modulo reachablity from a to +(+(?x,b),g(a)): maybe not reachable
check modulo reachablity from a to +(g(a),+(b,?z)): maybe not reachable
check modulo reachablity from a to +(+(?x,g(a)),b): maybe not reachable
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 6 (relative)
S:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?x ]
P:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,a) -> a,
     +(g(a),b) -> a,
     +(?x,0) -> ?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
  0:= (12)
  a:= (9)
  b:= 0
  g:= (11)+(2)*x1
retract +(b,g(a)) -> a
retract +(0,?x) -> ?x
retract +(g(a),b) -> a
retract +(?x,0) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (15)
  a:= (1)
  b:= 0
  g:= (11)+(2)*x1*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

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

Try Layer Preserving Decomposition for...
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?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...
   [ +(a,?x) -> a,
     +(b,g(a)) -> a,
     +(0,?x) -> ?x,
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Outside Critical Pair: <+(+(a,?y_2),?z_2), a> by Rules <3, 0>
develop reducts from lhs term...
<{5}, +(?z_2,+(?y_2,a))>
<{0,5}, +(?z_2,a)>
<{5}, +(?z_2,+(a,?y_2))>
<{4}, +(a,+(?y_2,?z_2))>
<{5}, +(+(?y_2,a),?z_2)>
<{0}, +(a,?z_2)>
<{}, +(+(a,?y_2),?z_2)>
develop reducts from rhs term...
<{}, a>
Outside Critical Pair: <+(?y_4,a), a> by Rules <5, 0>
develop reducts from lhs term...
<{5}, +(a,?y_4)>
<{}, +(?y_4,a)>
develop reducts from rhs term...
<{}, a>
Outside Critical Pair: <+(g(a),b), a> by Rules <5, 1>
develop reducts from lhs term...
<{5}, +(b,g(a))>
<{}, +(g(a),b)>
develop reducts from rhs term...
<{}, a>
Outside Critical Pair: <+(+(0,?y_2),?z_2), +(?y_2,?z_2)> by Rules <3, 2>
develop reducts from lhs term...
<{5}, +(?z_2,+(?y_2,0))>
<{2,5}, +(?z_2,?y_2)>
<{5}, +(?z_2,+(0,?y_2))>
<{4}, +(0,+(?y_2,?z_2))>
<{5}, +(+(?y_2,0),?z_2)>
<{2}, +(?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, 2>
develop reducts from lhs term...
<{5}, +(0,?y_4)>
<{}, +(?y_4,0)>
develop reducts from rhs term...
<{}, ?y_4>
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: <+(?x_2,a), +(+(?x_2,a),?x)> by Rules <0, 3>
develop reducts from lhs term...
<{5}, +(a,?x_2)>
<{}, +(?x_2,a)>
develop reducts from rhs term...
<{5}, +(?x,+(a,?x_2))>
<{5}, +(?x,+(?x_2,a))>
<{4}, +(?x_2,+(a,?x))>
<{5}, +(+(a,?x_2),?x)>
<{}, +(+(?x_2,a),?x)>
Inside Critical Pair: <+(?x_2,a), +(+(?x_2,b),g(a))> by Rules <1, 3>
develop reducts from lhs term...
<{5}, +(a,?x_2)>
<{}, +(?x_2,a)>
develop reducts from rhs term...
<{5}, +(g(a),+(b,?x_2))>
<{5}, +(g(a),+(?x_2,b))>
<{4}, +(?x_2,+(b,g(a)))>
<{5}, +(+(b,?x_2),g(a))>
<{}, +(+(?x_2,b),g(a))>
Inside Critical Pair: <+(?x_2,?x_1), +(+(?x_2,0),?x_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}, +(?x_1,+(0,?x_2))>
<{5}, +(?x_1,+(?x_2,0))>
<{4}, +(?x_2,+(0,?x_1))>
<{5}, +(+(0,?x_2),?x_1)>
<{}, +(+(?x_2,0),?x_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: <+(a,?z_3), +(a,+(?x,?z_3))> by Rules <0, 4>
develop reducts from lhs term...
<{5}, +(?z_3,a)>
<{0}, a>
<{}, +(a,?z_3)>
develop reducts from rhs term...
<{5}, +(+(?z_3,?x),a)>
<{5}, +(+(?x,?z_3),a)>
<{3}, +(+(a,?x),?z_3)>
<{0}, a>
<{5}, +(a,+(?z_3,?x))>
<{}, +(a,+(?x,?z_3))>
Inside Critical Pair: <+(a,?z_3), +(b,+(g(a),?z_3))> by Rules <1, 4>
develop reducts from lhs term...
<{5}, +(?z_3,a)>
<{0}, a>
<{}, +(a,?z_3)>
develop reducts from rhs term...
<{5}, +(+(?z_3,g(a)),b)>
<{5}, +(+(g(a),?z_3),b)>
<{3}, +(+(b,g(a)),?z_3)>
<{5}, +(b,+(?z_3,g(a)))>
<{}, +(b,+(g(a),?z_3))>
Inside Critical Pair: <+(?x_1,?z_3), +(0,+(?x_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,?x_1),0)>
<{5}, +(+(?x_1,?z_3),0)>
<{3}, +(+(0,?x_1),?z_3)>
<{2,5}, +(?z_3,?x_1)>
<{2}, +(?x_1,?z_3)>
<{5}, +(0,+(?z_3,?x_1))>
<{}, +(0,+(?x_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
538.trs: Failure(unknown CR)
MAYBE
(2465 msec.)