MAYBE
(ignored inputs)COMMENT the length function for queues.
Rewrite Rules:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ q(q(q(?x_1,?y_1),?z_1),?z) = q(?x_1,q(q(?y_1,?z_1),?z)),
     q(?x_2,?z) = q(e,q(?x_2,?z)),
     q(?x_3,?z) = q(?x_3,q(e,?z)),
     q(?x_1,q(?x,q(?y,?z))) = q(q(?x_1,q(?x,?y)),?z),
     q(?x_1,?x_2) = q(q(?x_1,e),?x_2),
     q(?x_1,?x_3) = q(q(?x_1,?x_3),e),
     plus(?x_4,plus(?y_5,?x_5)) = plus(plus(?x_4,?x_5),?y_5),
     plus(?x_4,?x_6) = plus(plus(?x_4,0),?x_6),
     plus(?x_4,s(plus(?x_7,?y_7))) = plus(plus(?x_4,s(?x_7)),?y_7),
     len(q(q(a,?y_1),?z_1)) = plus(len(a),len(q(?y_1,?z_1))),
     len(a) = plus(len(a),len(e)),
     q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ q(?x,q(?y,q(?y_1,?z_1))) = q(q(q(?x,?y),?y_1),?z_1),
     q(?x,q(?y,e)) = q(?x,?y),
     q(q(e,?y_1),?z_1) = q(?y_1,?z_1),
     e = e,
     plus(plus(?x_4,?y_4),?z_4) = plus(plus(?y_4,?z_4),?x_4),
     plus(plus(0,?y_4),?z_4) = plus(?y_4,?z_4),
     plus(plus(s(?x_7),?y_4),?z_4) = s(plus(?x_7,plus(?y_4,?z_4))),
     plus(?y_5,0) = ?y_5,
     plus(?y_5,s(?x_7)) = s(plus(?x_7,?y_5)) ]
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:
   [ q(q(q(?x_2,q(?y_2,?y)),?y_1),?z_1) = q(q(?x_2,?y_2),q(?y,q(?y_1,?z_1))),
     q(q(q(q(?x,?y_3),?z_3),?y_1),?z_1) = q(?x,q(q(?y_3,?z_3),q(?y_1,?z_1))),
     q(q(?y,?y_1),?z_1) = q(e,q(?y,q(?y_1,?z_1))),
     q(q(?x,?y_1),?z_1) = q(?x,q(e,q(?y_1,?z_1))),
     q(?x_1,q(?y_1,?y)) = q(q(?x_1,?y_1),q(?y,e)),
     q(q(?x,?y_2),?z_2) = q(?x,q(q(?y_2,?z_2),e)),
     ?y = q(e,q(?y,e)),
     ?x = q(?x,q(e,e)),
     q(q(q(?x,?y),?y_1),?z_1) = q(?x,q(?y,q(?y_1,?z_1))),
     q(?x,?y) = q(?x,q(?y,e)),
     q(q(?x_1,q(?y_1,?y)),?z) = q(q(?x_1,?y_1),q(?y,?z)),
     q(q(q(?x,?y_2),?z_2),?z) = q(?x,q(q(?y_2,?z_2),?z)),
     q(?y,?z) = q(e,q(?y,?z)),
     q(?x,?z) = q(?x,q(e,?z)),
     q(q(?x_2,q(?y_2,?y)),q(?z,?z_1)) = q(q(q(?x_2,?y_2),q(?y,?z)),?z_1),
     q(q(q(?x,?y_3),?z_3),q(?z,?z_1)) = q(q(?x,q(q(?y_3,?z_3),?z)),?z_1),
     q(?y,q(?z,?z_1)) = q(q(e,q(?y,?z)),?z_1),
     q(?x,q(?z,?z_1)) = q(q(?x,q(e,?z)),?z_1),
     q(q(?x_2,q(?x_3,q(?y_3,?y))),?z) = q(?x_2,q(q(?x_3,?y_3),q(?y,?z))),
     q(q(?x_2,q(q(?x,?y_4),?z_4)),?z) = q(?x_2,q(?x,q(q(?y_4,?z_4),?z))),
     q(q(?x_2,?x),?z) = q(?x_2,q(?x,q(e,?z))),
     q(q(?x,?y),q(?z,?z_1)) = q(q(?x,q(?y,?z)),?z_1),
     q(q(?x_2,q(?x,?y)),?z) = q(?x_2,q(?x,q(?y,?z))),
     q(?x_1,q(?y_1,q(q(?y,?y_2),?z_2))) = q(q(q(?x_1,?y_1),?y),q(?y_2,?z_2)),
     q(?x_1,q(?y_1,q(?x_3,q(?y_3,?z)))) = q(q(q(?x_1,?y_1),q(?x_3,?y_3)),?z),
     q(?x_1,q(?y_1,?z)) = q(q(q(?x_1,?y_1),e),?z),
     q(?x_1,q(?y_1,?y)) = q(q(q(?x_1,?y_1),?y),e),
     q(q(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?z = q(q(e,e),?z),
     ?y = q(q(e,?y),e),
     q(?x_1,q(?y_1,q(?y,?z))) = q(q(q(?x_1,?y_1),?y),?z),
     q(?y,?z) = q(q(e,?y),?z),
     q(?x,q(q(?y,?y_1),?z_1)) = q(q(?x,?y),q(?y_1,?z_1)),
     q(?x,q(?x_2,q(?y_2,?z))) = q(q(?x,q(?x_2,?y_2)),?z),
     q(?x,?z) = q(q(?x,e),?z),
     q(?x,?y) = q(q(?x,?y),e),
     q(q(?x_1,?x),q(q(?y,?y_2),?z_2)) = q(?x_1,q(q(?x,?y),q(?y_2,?z_2))),
     q(q(?x_1,?x),q(?x_3,q(?y_3,?z))) = q(?x_1,q(q(?x,q(?x_3,?y_3)),?z)),
     q(q(?x_1,?x),?z) = q(?x_1,q(q(?x,e),?z)),
     q(?x,q(q(q(?y,?y_3),?z_3),?z_2)) = q(q(q(?x,?y),q(?y_3,?z_3)),?z_2),
     q(?x,q(q(?x_4,q(?y_4,?z)),?z_2)) = q(q(q(?x,q(?x_4,?y_4)),?z),?z_2),
     q(?x,q(?z,?z_2)) = q(q(q(?x,e),?z),?z_2),
     plus(len(a),len(q(q(?y,?y_1),?z_1))) = len(q(q(a,?y),q(?y_1,?z_1))),
     plus(len(a),len(q(?x_2,q(?y_2,?z)))) = len(q(q(a,q(?x_2,?y_2)),?z)),
     plus(len(a),len(?z)) = len(q(q(a,e),?z)),
     plus(len(a),len(?y)) = len(q(q(a,?y),e)),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     q(?x,q(q(?y,?z),?z_2)) = q(q(q(?x,?y),?z),?z_2),
     plus(len(a),len(q(?y,?z))) = len(q(q(a,?y),?z)),
     q(q(e,?y_2),?z_2) = q(?y_2,?z_2),
     e = e,
     q(e,q(?x,?z_2)) = q(?x,?z_2),
     q(q(?x_3,e),?x) = q(?x_3,?x),
     q(?x_1,q(?y_1,e)) = q(?x_1,?y_1),
     q(?x,q(e,?z_2)) = q(?x,?z_2),
     q(q(?x_3,?x),e) = q(?x_3,?x),
     plus(len(a),len(e)) = len(a),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(s(plus(?x_8,?z)),?x) = plus(plus(?x,s(?x_8)),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_8,?z)) = plus(plus(0,s(?x_8)),?z),
     s(plus(?x_7,plus(plus(?y,?y_8),?z_8))) = plus(plus(s(?x_7),?y),plus(?y_8,?z_8)),
     s(plus(?x_7,plus(?z,?y))) = plus(plus(s(?x_7),?y),?z),
     s(plus(?x_7,?z)) = plus(plus(s(?x_7),0),?z),
     s(plus(?x_7,s(plus(?x_15,?z)))) = plus(plus(s(?x_7),s(?x_15)),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     s(plus(?x_7,plus(?y,?z))) = plus(plus(s(?x_7),?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(?x,s(plus(?x_8,?z))) = plus(plus(?x,s(?x_8)),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),s(plus(?x_9,?z))) = plus(?x_1,plus(plus(?x,s(?x_9)),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x,?y_5),?z_5) = plus(plus(?y_5,?z_5),?x),
     ?y = plus(?y,0),
     s(plus(?x_7,?y)) = plus(?y,s(?x_7)),
     plus(plus(?x_6,?x),?y) = plus(?x_6,plus(?y,?x)),
     plus(plus(0,?y_5),?z_5) = plus(?y_5,?z_5),
     plus(?x,0) = ?x,
     plus(plus(?x_6,0),?x) = plus(?x_6,?x),
     plus(plus(s(?x),?y_5),?z_5) = s(plus(?x,plus(?y_5,?z_5))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_6,s(?x)),?y) = plus(?x_6,s(plus(?x,?y))),
     len(q(q(a,?y_3),?z_3)) = plus(len(a),len(q(?y_3,?z_3))),
     len(a) = plus(len(a),len(e)) ]
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 <q(q(q(?x_1,?y_1),?z_1),?z), q(?x_1,q(q(?y_1,?z_1),?z))> by Rules <1, 0> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],0)], [([],1)]>
Critical Pair <q(?x_2,?z), q(e,q(?x_2,?z))> by Rules <2, 0> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <q(?x_3,?z), q(?x_3,q(e,?z))> by Rules <3, 0> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([(q,2)],2)]>
Critical Pair <q(?x_1,q(?x,q(?y,?z))), q(q(?x_1,q(?x,?y)),?z)> by Rules <0, 1> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],1)], [([],0)]>
Critical Pair <q(?x_1,?x_2), q(q(?x_1,e),?x_2)> by Rules <2, 1> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([(q,1)],3)]>
Critical Pair <q(?x_1,?x_3), q(q(?x_1,?x_3),e)> by Rules <3, 1> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <plus(?x_4,plus(?y_5,?x_5)), plus(plus(?x_4,?x_5),?y_5)> by Rules <5, 4> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],5),([],4)], []>
 joinable by a reduction of rules <[([],4),([(plus,1)],5)], [([],5),([],4)]>
Critical Pair <plus(?x_4,?x_6), plus(plus(?x_4,0),?x_6)> by Rules <6, 4> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],5),([(plus,1)],6)]>
Critical Pair <plus(?x_4,s(plus(?x_7,?y_7))), plus(plus(?x_4,s(?x_7)),?y_7)> by Rules <7, 4> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],5),([],7),([(s,1)],5),([(s,1)],4)], [([(plus,1)],5),([(plus,1)],7),([(plus,1),(s,1)],5),([],7)]>
 joinable by a reduction of rules <[([],5),([],7),([(s,1)],5),([(s,1)],4)], [([(plus,1)],5),([(plus,1)],7),([],7),([(s,1),(plus,1)],5)]>
Critical Pair <len(q(q(a,?y_1),?z_1)), plus(len(a),len(q(?y_1,?z_1)))> by Rules <1, 10> preceded by [(len,1)]
 joinable by a reduction of rules <[([(len,1)],0),([],10)], []>
Critical Pair <len(a), plus(len(a),len(e))> by Rules <3, 10> preceded by [(len,1)]
 joinable by a reduction of rules <[], [([(plus,2)],8),([],5),([],6)]>
 joinable by a reduction of rules <[], [([],5),([(plus,1)],8),([],6)]>
Critical Pair <q(q(?x,q(?y,?z)),?z_1), q(q(?x,?y),q(?z,?z_1))> by Rules <0, 0> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],1)], [([],1)]>
Critical Pair <q(?x_1,q(q(?x,?y),?z)), q(q(?x_1,?x),q(?y,?z))> by Rules <1, 1> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],0)], [([],0)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <4, 4> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],4),([(plus,1)],4)], [([],4)]>
Critical Pair <q(q(q(?x,?y),?y_1),?z_1), q(?x,q(?y,q(?y_1,?z_1)))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <q(?x,?y), q(?x,q(?y,e))> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(q,2)],3)]>
Critical Pair <q(?y_1,?z_1), q(q(e,?y_1),?z_1)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[], [([(q,1)],2)]>
Critical Pair <e, e> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <plus(plus(?y_4,?z_4),?x_5), plus(plus(?x_5,?y_4),?z_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5),([],4)], []>
Critical Pair <plus(?y_4,?z_4), plus(plus(0,?y_4),?z_4)> by Rules <6, 4> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],6)]>
Critical Pair <s(plus(?x_7,plus(?y_4,?z_4))), plus(plus(s(?x_7),?y_4),?z_4)> by Rules <7, 4> preceded by []
 joinable by a reduction of rules <[([(s,1)],4)], [([(plus,1)],7),([],7)]>
Critical Pair <?x_6, plus(?x_6,0)> by Rules <6, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],6)]>
Critical Pair <s(plus(?x_7,?y_7)), plus(?y_7,s(?x_7))> by Rules <7, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],7)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 21 rules by 3 steps unfolding
strenghten len(e) and 0
strenghten q(0,e) and 0
strenghten q(e,0) and 0
strenghten plus(?x_6,0) and ?x_6
strenghten plus(0,?x_11) and ?x_11
strenghten s(plus(?x_7,0)) and s(?x_7)
strenghten plus(len(a),len(e)) and len(a)
strenghten plus(?y_7,s(?x_7)) and s(plus(?x_7,?y_7))
strenghten q(?x,q(?y,e)) and q(?x,?y)
strenghten q(?x_3,q(e,?z)) and q(?x_3,?z)
strenghten q(e,q(?x_2,?z)) and q(?x_2,?z)
strenghten q(q(?x_1,?x_3),e) and q(?x_1,?x_3)
strenghten q(q(?x_1,e),?x_2) and q(?x_1,?x_2)
strenghten q(q(e,?y_1),?z_1) and q(?y_1,?z_1)
strenghten plus(plus(?x_4,?x_11),0) and plus(?x_4,?x_11)
strenghten plus(plus(?x_4,0),?x_6) and plus(?x_4,?x_6)
strenghten plus(plus(0,?y_4),?z_4) and plus(?y_4,?z_4)
strenghten q(e,q(len(e),?z)) and q(0,?z)
strenghten q(q(?x_1,e),len(e)) and q(?x_1,0)
strenghten q(q(?x_1,len(e)),e) and q(?x_1,0)
strenghten q(len(e),q(e,?z)) and q(0,?z)
strenghten plus(plus(?x_4,?x_5),?y_5) and plus(?x_4,plus(?y_5,?x_5))
strenghten plus(plus(?x_5,?y_4),?z_4) and plus(plus(?y_4,?z_4),?x_5)
strenghten plus(plus(?x_4,s(?x_7)),?y_7) and plus(?x_4,s(plus(?x_7,?y_7)))
strenghten plus(plus(s(?x_7),?y_4),?z_4) and s(plus(?x_7,plus(?y_4,?z_4)))
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:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z) ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)*x1
  len:= (2)*x1
  plus:= (2)+(1)*x1+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= 0
  q:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  s:= (1)*x1
  len:= (2)*x1
  plus:= (2)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (2)
  q:= (1)*x1+(1)*x2
  s:= (2)+(1)*x1
  len:= (2)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
  len:= (1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract plus(s(?x),?y) -> s(plus(?x,?y))
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract plus(s(?x),?y) -> s(plus(?x,?y))
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(len(q(?y_2,?z_2)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from s(len(q(?y_2,?z_2))) to len(q(q(a,?y_2),?z_2)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
failed
failure(Step 1)
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
Added S-Rules:
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(len(q(?y,?z)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from s(len(q(?y,?z))) to len(q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
failed
failure(Step 2)
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
Added S-Rules:
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)*x1
  len:= (1)+(2)*x1*x1
  plus:= (1)+(1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  s:= (1)*x1
  len:= (1)+(2)*x1*x1
  plus:= (1)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
  len:= (1)+(2)*x1*x1
  plus:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(?x_6,0)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(?x_3,0))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(?x_6,s(?x_3))), s(plus(?x_3,s(?x_6)))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_6,?x_3)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(len(q(?y_2,?z_2)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y_2,?z_2))) to len(q(q(a,?y_2),?z_2)): maybe not reachable
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?x,?y)) => plus(?y,s(?x)) -> s(plus(?y,?x))
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 5 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(?x_6,0)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(?x_3,0))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(?x_6,s(?x_3))), s(plus(?x_3,s(?x_6)))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_6,?x_3)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(len(q(?y,?z)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y,?z))) to len(q(q(a,?y),?z)): maybe not reachable
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {3}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {3}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {3}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {3}
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?x,?y)) => plus(?y,s(?x)) -> s(plus(?y,?x))
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 6 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (8)
  q:= (1)*x1+(2)*x1*x2+(1)*x2
  s:= (1)*x1
  len:= (1)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)*x1
  len:= (2)*x1
  plus:= (2)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (7)
  q:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  s:= (1)*x1
  len:= (2)*x1
  plus:= (2)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= (2)
  a:= 0
  e:= (14)
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  s:= (4)+(2)*x1
  len:= (2)*x1
  plus:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract plus(s(?x),?y) -> s(plus(?x,?y))
retract len(e) -> 0
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
retract plus(?y,s(?x)) -> s(plus(?x,?y))
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= 0
  q:= (2)+(1)*x1+(1)*x2
  s:= (8)*x1
  len:= (2)*x1+(2)*x1*x1
  plus:= (1)*x1+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(plus(len(q(?y_2,?z_2)),0))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), plus(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from s(plus(len(q(?y_2,?z_2)),0)) to len(q(q(a,?y_2),?z_2)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {4}
check modulo reachablity from plus(?x_1,s(plus(?y,?x))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {4}
check modulo reachablity from s(plus(?y,?x)) to plus(?y,s(?x)): maybe not reachable
failed
failure(Step 7)
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
Added S-Rules:
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 8 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(plus(len(q(?y,?z)),0))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), plus(?y,s(?x))> => no
check joinability condition:
check modulo reachablity from s(plus(len(q(?y,?z)),0)) to len(q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {0}
check modulo reachablity from plus(?x_1,s(plus(?y,?x))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {0}
check modulo reachablity from s(plus(?y,?x)) to plus(?y,s(?x)): maybe not reachable
failed
failure(Step 8)
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
Added S-Rules:
   [ plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 9 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
  len:= (3)*x1*x1
  plus:= (3)+(1)*x1+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (3)
  q:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
  len:= (3)*x1*x1
  plus:= (3)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (3)
  q:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
  len:= (2)+(3)*x1*x1
  plus:= (3)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (1)+(1)*x1+(1)*x2
  s:= (1)*x1
  len:= (3)*x1+(1)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= (3)
  q:= (3)+(1)*x1+(1)*x2
  s:= (2)+(2)*x1
  len:= (1)*x1*x1
  plus:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
STEP: 10 (parallel)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(?x_6,0)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(0,?x_3))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(?x_6,s(?x_3))), s(plus(s(?x_6),?x_3))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(len(q(?y_2,?z_2)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?y,?x),?x_1)), s(plus(?y,plus(?x,?x_1)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(?z_1,plus(?x,?y))), s(plus(plus(?z_1,?x),?y))> => yes
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?y,?x))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y_2,?z_2))) to len(q(q(a,?y_2),?z_2)): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {4}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {4}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
failed
failure(Step 10)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?x,?y)) => plus(?y,s(?x)) -> s(plus(?y,?x))
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 11 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(?x_6,0)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(0,?x_3))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(?x_6,s(?x_3))), s(plus(s(?x_6),?x_3))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(len(q(?y,?z)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?y,?x),?x_1)), s(plus(?y,plus(?x,?x_1)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(?z_1,plus(?x,?y))), s(plus(plus(?z_1,?x),?y))> => yes
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?y,?x))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y,?z))) to len(q(q(a,?y),?z)): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {0}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {0}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {3}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {3}
failed
failure(Step 11)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?x,?y)) => plus(?y,s(?x)) -> s(plus(?y,?x))
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 12 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= 0
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  s:= (7)+(8)*x1
  len:= (3)*x1+(2)*x1*x1
  plus:= (1)*x1+(1)*x1*x2+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= (1)
  a:= 0
  e:= (12)
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  s:= (7)+(8)*x1
  len:= (1)+(3)*x1+(2)*x1*x1
  plus:= (1)*x1+(1)*x1*x2+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= (2)
  a:= (1)
  e:= 0
  q:= (1)*x1+(2)*x1*x2+(1)*x2
  s:= (1)*x1
  len:= (3)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (8)
  q:= (1)*x1+(2)*x1*x2+(1)*x2
  s:= (1)+(1)*x1
  len:= (3)*x1
  plus:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 12)
STEP: 13 (parallel)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(0,?x_6)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(?x_3,0))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(s(?x_3),?x_6)), s(plus(?x_3,s(?x_6)))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(len(q(?y_2,?z_2)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(?x_1,plus(?x,?y))), s(plus(plus(?x_1,?x),?y))> => yes
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?y,?x))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(?x_1,plus(?y,?x))), s(plus(plus(?x_1,?y),?x))> => yes
<s(plus(plus(?x_1,?y_1),?x)), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(plus(?x_1,?y_1),?x)), s(plus(?x_1,plus(?y_1,?x)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?y,?x),?z_1)), s(plus(?y,plus(?x,?z_1)))> => yes
<s(plus(?y,?x)), plus(s(?x),?y)> --> <s(plus(?y,?x)), s(plus(?x,?y))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y_2,?z_2))) to len(q(q(a,?y_2),?z_2)): maybe not reachable
failed
failure(Step 13)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 14 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(0,?x_6)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(?x_3,0))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(s(?x_3),?x_6)), s(plus(?x_3,s(?x_6)))> --> <s(s(plus(?x_3,?x_6))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(len(q(?y,?z)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(?x_1,plus(?x,?y))), s(plus(plus(?x_1,?x),?y))> => yes
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?y,?x))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(?x_1,plus(?y,?x))), s(plus(plus(?x_1,?y),?x))> => yes
<s(plus(plus(?x_1,?y_1),?x)), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(plus(?x_1,?y_1),?x)), s(plus(?x_1,plus(?y_1,?x)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?y,?x),?z_1)), s(plus(?y,plus(?x,?z_1)))> => yes
<s(plus(?y,?x)), plus(s(?x),?y)> --> <s(plus(?y,?x)), s(plus(?x,?y))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y,?z))) to len(q(q(a,?y),?z)): maybe not reachable
failed
failure(Step 14)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 15 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= 0
  q:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  s:= (7)+(4)*x1
  len:= (2)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (4)
  q:= (1)*x1+(1)*x2
  s:= (14)+(13)*x1
  len:= (2)*x1
  plus:= (1)*x1+(1)*x1*x2+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (1)
  q:= (1)+(1)*x1+(1)*x2
  s:= (7)+(1)*x1
  len:= (3)*x1
  plus:= (1)*x1+(1)*x1*x2+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= 0
  q:= (1)*x1+(1)*x2
  s:= (2)+(1)*x1
  len:= (1)*x1+(3)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= (2)
  q:= (1)*x1+(1)*x2
  s:= (2)+(1)*x1
  len:= (2)*x1
  plus:= (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:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(0,?x_6)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(0,?x_3))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(s(?x_3),?x_6)), s(plus(s(?x_6),?x_3))> --> <s(s(plus(?x_6,?x_3))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
PCP_in(symP,S):
<len(q(q(a,?y_2),?z_2)), plus(len(a),len(q(?y_2,?z_2)))> --> <len(q(q(a,?y_2),?z_2)), s(len(q(?y_2,?z_2)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(?x_1,plus(?y,?x))), s(plus(?y,plus(?x_1,?x)))> => no
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), s(plus(?y,?x))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(?x_1,plus(?y,?x))), s(plus(plus(?x_1,?y),?x))> => yes
<s(plus(plus(?x_1,?y_1),?x)), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(plus(?x_1,?y_1),?x)), s(plus(?x_1,plus(?y_1,?x)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(?y,plus(?z_1,?x)))> => no
<s(plus(?y,?x)), plus(s(?x),?y)> --> <s(plus(?y,?x)), s(plus(?y,?x))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y_2,?z_2))) to len(q(q(a,?y_2),?z_2)): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {4}
check modulo joinability of s(plus(?x_1,plus(?y,?x))) and s(plus(?y,plus(?x_1,?x))): joinable by {4}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {4}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(?y,plus(?z_1,?x))): joinable by {4}
failed
failure(Step 16)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?y,?x)) => plus(?y,s(?x)) -> s(plus(?x,?y))
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 17 (linear)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<e, e> --> <e, e> => yes
<0, 0> --> <0, 0> => yes
<s(plus(0,?x_6)), s(?x_6)> --> <s(?x_6), s(?x_6)> => yes
<s(?x_3), s(plus(0,?x_3))> --> <s(?x_3), s(?x_3)> => yes
<s(plus(s(?x_3),?x_6)), s(plus(s(?x_6),?x_3))> --> <s(s(plus(?x_6,?x_3))), s(s(plus(?x_3,?x_6)))> => yes
<len(a), plus(len(a),len(e))> --> <s(0), s(0)> => yes
CP_in(symP,S):
<len(q(q(a,?y),?z)), plus(len(a),len(q(?y,?z)))> --> <len(q(q(a,?y),?z)), s(len(q(?y,?z)))> => no
CP(S,symP):
<q(?y_1,?z_1), q(q(e,?y_1),?z_1)> --> <q(?y_1,?z_1), q(?y_1,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,e),?x)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<q(?x_1,?x), q(q(?x_1,?x),e)> --> <q(?x_1,?x), q(?x_1,?x)> => yes
<q(?x_1,?y_1), q(?x_1,q(?y_1,e))> --> <q(?x_1,?y_1), q(?x_1,?y_1)> => yes
<q(?x,?z_1), q(?x,q(e,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<s(plus(plus(?y_1,?z_1),?x)), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(plus(?y_1,?z_1),?x)), s(plus(?z_1,plus(?y_1,?x)))> => no
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(?x_1,plus(?y,?x))), s(plus(?y,plus(?x_1,?x)))> => no
<plus(s(plus(?y,?x)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(plus(?y,?z_1),?x))> => no
<s(plus(?y,?x)), plus(?y,s(?x))> --> <s(plus(?y,?x)), s(plus(?y,?x))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?y,?x))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(?x_1,plus(?y,?x))), s(plus(plus(?x_1,?y),?x))> => yes
<s(plus(plus(?x_1,?y_1),?x)), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(plus(?x_1,?y_1),?x)), s(plus(?x_1,plus(?y_1,?x)))> => yes
<plus(s(plus(?y,?x)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(?z_1,plus(?y,?x))), s(plus(?y,plus(?z_1,?x)))> => no
<s(plus(?y,?x)), plus(s(?x),?y)> --> <s(plus(?y,?x)), s(plus(?y,?x))> => yes
check joinability condition:
check modulo reachablity from s(len(q(?y,?z))) to len(q(q(a,?y),?z)): maybe not reachable
check modulo joinability of s(plus(plus(?y_1,?z_1),?x)) and s(plus(?z_1,plus(?y_1,?x))): joinable by {0}
check modulo joinability of s(plus(?x_1,plus(?y,?x))) and s(plus(?y,plus(?x_1,?x))): joinable by {0}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(plus(?y,?z_1),?x)): joinable by {0}
check modulo joinability of s(plus(?z_1,plus(?y,?x))) and s(plus(?y,plus(?z_1,?x))): joinable by {0}
failed
failure(Step 17)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: plus(?y,s(?x)) -> s(plus(?y,?x)) => plus(?y,s(?x)) -> s(plus(?x,?y))
replace: plus(s(?x),?y) -> s(plus(?y,?x)) => plus(s(?x),?y) -> s(plus(?x,?y))
STEP: 18 (relative)
S:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?y,?x)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)),
     plus(?x,0) -> ?x,
     plus(?y,s(?x)) -> s(plus(?y,?x)) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (1)
  q:= (1)*x1+(1)*x2
  s:= (1)*x1
  len:= (2)*x1
  plus:= (1)+(1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= 0
  e:= (1)
  q:= (1)+(1)*x1+(1)*x2
  s:= (1)*x1
  len:= (1)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= (1)
  q:= (1)*x1+(1)*x2
  s:= (1)*x1
  len:= (1)+(2)*x1*x1
  plus:= (1)*x1+(1)*x2
retract q(e,?x) -> ?x
retract q(?x,e) -> ?x
retract plus(0,?x) -> ?x
retract len(e) -> 0
retract len(a) -> s(0)
retract len(q(a,?y)) -> plus(len(a),len(?y))
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  a:= (1)
  e:= (1)
  q:= (1)*x1+(1)*x2
  s:= (4)+(1)*x1
  len:= (2)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*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...
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
Sort Assignment:
 0 : =>31
 a : =>26
 e : =>26
 q : 26*26=>26
 s : 31=>31
 len : 26=>31
 plus : 31*31=>31
maximal types: {26,31}
Persistent Decomposition failed: Can't judge

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

Try Commutative Decomposition for...
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     len(e) -> 0,
     len(a) -> s(0),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
Outside Critical Pair: <q(q(q(?x,?y),?y_1),?z_1), q(?x,q(?y,q(?y_1,?z_1)))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, q(q(?x,?y),q(?y_1,?z_1))>
<{0}, q(q(?x,q(?y,?y_1)),?z_1)>
<{}, q(q(q(?x,?y),?y_1),?z_1)>
develop reducts from rhs term...
<{1}, q(q(?x,?y),q(?y_1,?z_1))>
<{1}, q(?x,q(q(?y,?y_1),?z_1))>
<{}, q(?x,q(?y,q(?y_1,?z_1)))>
Outside Critical Pair: <q(?x,?y), q(?x,q(?y,e))> by Rules <3, 0>
develop reducts from lhs term...
<{}, q(?x,?y)>
develop reducts from rhs term...
<{1}, q(q(?x,?y),e)>
<{3}, q(?x,?y)>
<{}, q(?x,q(?y,e))>
Outside Critical Pair: <q(?y_1,?z_1), q(q(e,?y_1),?z_1)> by Rules <2, 1>
develop reducts from lhs term...
<{}, q(?y_1,?z_1)>
develop reducts from rhs term...
<{0}, q(e,q(?y_1,?z_1))>
<{2}, q(?y_1,?z_1)>
<{}, q(q(e,?y_1),?z_1)>
Outside Critical Pair: <e, e> by Rules <3, 2>
develop reducts from lhs term...
<{}, e>
develop reducts from rhs term...
<{}, e>
Outside Critical Pair: <plus(plus(?y_4,?z_4),?x_5), plus(plus(?x_5,?y_4),?z_4)> by Rules <5, 4>
develop reducts from lhs term...
<{5}, plus(?x_5,plus(?z_4,?y_4))>
<{5}, plus(?x_5,plus(?y_4,?z_4))>
<{5}, plus(plus(?z_4,?y_4),?x_5)>
<{}, plus(plus(?y_4,?z_4),?x_5)>
develop reducts from rhs term...
<{5}, plus(?z_4,plus(?y_4,?x_5))>
<{5}, plus(?z_4,plus(?x_5,?y_4))>
<{5}, plus(plus(?y_4,?x_5),?z_4)>
<{}, plus(plus(?x_5,?y_4),?z_4)>
Outside Critical Pair: <plus(?y_4,?z_4), plus(plus(0,?y_4),?z_4)> by Rules <6, 4>
develop reducts from lhs term...
<{5}, plus(?z_4,?y_4)>
<{}, plus(?y_4,?z_4)>
develop reducts from rhs term...
<{5,6}, plus(?z_4,?y_4)>
<{5}, plus(?z_4,plus(?y_4,0))>
<{5}, plus(?z_4,plus(0,?y_4))>
<{6}, plus(?y_4,?z_4)>
<{5}, plus(plus(?y_4,0),?z_4)>
<{}, plus(plus(0,?y_4),?z_4)>
Outside Critical Pair: <s(plus(?x_7,plus(?y_4,?z_4))), plus(plus(s(?x_7),?y_4),?z_4)> by Rules <7, 4>
develop reducts from lhs term...
<{5}, s(plus(plus(?z_4,?y_4),?x_7))>
<{5}, s(plus(plus(?y_4,?z_4),?x_7))>
<{4}, s(plus(plus(?x_7,?y_4),?z_4))>
<{5}, s(plus(?x_7,plus(?z_4,?y_4)))>
<{}, s(plus(?x_7,plus(?y_4,?z_4)))>
develop reducts from rhs term...
<{5,7}, plus(?z_4,s(plus(?x_7,?y_4)))>
<{5}, plus(?z_4,plus(?y_4,s(?x_7)))>
<{5}, plus(?z_4,plus(s(?x_7),?y_4))>
<{7}, plus(s(plus(?x_7,?y_4)),?z_4)>
<{5}, plus(plus(?y_4,s(?x_7)),?z_4)>
<{}, plus(plus(s(?x_7),?y_4),?z_4)>
Outside Critical Pair: <?x_6, plus(?x_6,0)> by Rules <6, 5>
develop reducts from lhs term...
<{}, ?x_6>
develop reducts from rhs term...
<{5}, plus(0,?x_6)>
<{}, plus(?x_6,0)>
Outside Critical Pair: <s(plus(?x_7,?y_7)), plus(?y_7,s(?x_7))> by Rules <7, 5>
develop reducts from lhs term...
<{5}, s(plus(?y_7,?x_7))>
<{}, s(plus(?x_7,?y_7))>
develop reducts from rhs term...
<{5}, plus(s(?x_7),?y_7)>
<{}, plus(?y_7,s(?x_7))>
Inside Critical Pair: <q(q(q(?x_1,?y_1),?z_1),?z), q(?x_1,q(q(?y_1,?z_1),?z))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, q(q(?x_1,?y_1),q(?z_1,?z))>
<{0}, q(q(?x_1,q(?y_1,?z_1)),?z)>
<{}, q(q(q(?x_1,?y_1),?z_1),?z)>
develop reducts from rhs term...
<{1}, q(q(?x_1,q(?y_1,?z_1)),?z)>
<{0}, q(?x_1,q(?y_1,q(?z_1,?z)))>
<{}, q(?x_1,q(q(?y_1,?z_1),?z))>
Inside Critical Pair: <q(?x_2,?z), q(e,q(?x_2,?z))> by Rules <2, 0>
develop reducts from lhs term...
<{}, q(?x_2,?z)>
develop reducts from rhs term...
<{2}, q(?x_2,?z)>
<{1}, q(q(e,?x_2),?z)>
<{}, q(e,q(?x_2,?z))>
Inside Critical Pair: <q(?x_3,?z), q(?x_3,q(e,?z))> by Rules <3, 0>
develop reducts from lhs term...
<{}, q(?x_3,?z)>
develop reducts from rhs term...
<{1}, q(q(?x_3,e),?z)>
<{2}, q(?x_3,?z)>
<{}, q(?x_3,q(e,?z))>
Inside Critical Pair: <q(?x_1,q(?x,q(?y,?z))), q(q(?x_1,q(?x,?y)),?z)> by Rules <0, 1>
develop reducts from lhs term...
<{1}, q(q(?x_1,?x),q(?y,?z))>
<{1}, q(?x_1,q(q(?x,?y),?z))>
<{}, q(?x_1,q(?x,q(?y,?z)))>
develop reducts from rhs term...
<{0}, q(?x_1,q(q(?x,?y),?z))>
<{1}, q(q(q(?x_1,?x),?y),?z)>
<{}, q(q(?x_1,q(?x,?y)),?z)>
Inside Critical Pair: <q(?x_1,?x_2), q(q(?x_1,e),?x_2)> by Rules <2, 1>
develop reducts from lhs term...
<{}, q(?x_1,?x_2)>
develop reducts from rhs term...
<{0}, q(?x_1,q(e,?x_2))>
<{3}, q(?x_1,?x_2)>
<{}, q(q(?x_1,e),?x_2)>
Inside Critical Pair: <q(?x_1,?x_3), q(q(?x_1,?x_3),e)> by Rules <3, 1>
develop reducts from lhs term...
<{}, q(?x_1,?x_3)>
develop reducts from rhs term...
<{3}, q(?x_1,?x_3)>
<{0}, q(?x_1,q(?x_3,e))>
<{}, q(q(?x_1,?x_3),e)>
Inside Critical Pair: <plus(?x_4,plus(?y_5,?x_5)), plus(plus(?x_4,?x_5),?y_5)> by Rules <5, 4>
develop reducts from lhs term...
<{5}, plus(plus(?x_5,?y_5),?x_4)>
<{5}, plus(plus(?y_5,?x_5),?x_4)>
<{4}, plus(plus(?x_4,?y_5),?x_5)>
<{5}, plus(?x_4,plus(?x_5,?y_5))>
<{}, plus(?x_4,plus(?y_5,?x_5))>
develop reducts from rhs term...
<{5}, plus(?y_5,plus(?x_5,?x_4))>
<{5}, plus(?y_5,plus(?x_4,?x_5))>
<{5}, plus(plus(?x_5,?x_4),?y_5)>
<{}, plus(plus(?x_4,?x_5),?y_5)>
Inside Critical Pair: <plus(?x_4,?x_6), plus(plus(?x_4,0),?x_6)> by Rules <6, 4>
develop reducts from lhs term...
<{5}, plus(?x_6,?x_4)>
<{}, plus(?x_4,?x_6)>
develop reducts from rhs term...
<{5}, plus(?x_6,plus(0,?x_4))>
<{5}, plus(?x_6,plus(?x_4,0))>
<{5}, plus(plus(0,?x_4),?x_6)>
<{}, plus(plus(?x_4,0),?x_6)>
Inside Critical Pair: <plus(?x_4,s(plus(?x_7,?y_7))), plus(plus(?x_4,s(?x_7)),?y_7)> by Rules <7, 4>
develop reducts from lhs term...
<{5}, plus(s(plus(?y_7,?x_7)),?x_4)>
<{5}, plus(s(plus(?x_7,?y_7)),?x_4)>
<{5}, plus(?x_4,s(plus(?y_7,?x_7)))>
<{}, plus(?x_4,s(plus(?x_7,?y_7)))>
develop reducts from rhs term...
<{5}, plus(?y_7,plus(s(?x_7),?x_4))>
<{5}, plus(?y_7,plus(?x_4,s(?x_7)))>
<{5}, plus(plus(s(?x_7),?x_4),?y_7)>
<{}, plus(plus(?x_4,s(?x_7)),?y_7)>
Inside Critical Pair: <len(q(q(a,?y_1),?z_1)), plus(len(a),len(q(?y_1,?z_1)))> by Rules <1, 10>
develop reducts from lhs term...
<{0}, len(q(a,q(?y_1,?z_1)))>
<{}, len(q(q(a,?y_1),?z_1))>
develop reducts from rhs term...
<{5,9}, plus(len(q(?y_1,?z_1)),s(0))>
<{5}, plus(len(q(?y_1,?z_1)),len(a))>
<{9}, plus(s(0),len(q(?y_1,?z_1)))>
<{}, plus(len(a),len(q(?y_1,?z_1)))>
Inside Critical Pair: <len(a), plus(len(a),len(e))> by Rules <3, 10>
develop reducts from lhs term...
<{9}, s(0)>
<{}, len(a)>
develop reducts from rhs term...
<{5,8,9}, plus(0,s(0))>
<{5,8}, plus(0,len(a))>
<{5,9}, plus(len(e),s(0))>
<{5}, plus(len(e),len(a))>
<{8,9}, plus(s(0),0)>
<{9}, plus(s(0),len(e))>
<{8}, plus(len(a),0)>
<{}, plus(len(a),len(e))>
Try A Minimal Decomposition {4,7,5,6}{2,3,1,10}{0}{8}{9}
{4,7,5,6}
(cm)Rewrite Rules:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x,s(plus(?x_1,?y_1))) = plus(plus(?x,s(?x_1)),?y_1),
     plus(?x,plus(?y_2,?x_2)) = plus(plus(?x,?x_2),?y_2),
     plus(?x,?x_3) = plus(plus(?x,0),?x_3),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ plus(plus(s(?x_1),?y),?z) = s(plus(?x_1,plus(?y,?z))),
     plus(plus(?x,?y),?z) = plus(plus(?y,?z),?x),
     plus(plus(0,?y),?z) = plus(?y,?z),
     s(plus(?x_1,?y_1)) = plus(?y_1,s(?x_1)),
     plus(?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:
   [ s(plus(?x_1,plus(plus(?y,?y_2),?z_2))) = plus(plus(s(?x_1),?y),plus(?y_2,?z_2)),
     s(plus(?x_1,s(plus(?x_3,?z)))) = plus(plus(s(?x_1),s(?x_3)),?z),
     s(plus(?x_1,plus(?z,?y))) = plus(plus(s(?x_1),?y),?z),
     s(plus(?x_1,?z)) = plus(plus(s(?x_1),0),?z),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(s(plus(?x_2,?z)),?x) = plus(plus(?x,s(?x_2)),?z),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     s(plus(?x_2,?z)) = plus(plus(0,s(?x_2)),?z),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_1,plus(?y,?z))) = plus(plus(s(?x_1),?y),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,s(plus(?x_2,?z))) = plus(plus(?x,s(?x_2)),?z),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),s(plus(?x_3,?z))) = plus(?x_1,plus(plus(?x,s(?x_3)),?z)),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(s(?x),?y_1),?z_1) = s(plus(?x,plus(?y_1,?z_1))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_2,s(?x)),?y) = plus(?x_2,s(plus(?x,?y))),
     plus(plus(?x,?y_1),?z_1) = plus(plus(?y_1,?z_1),?x),
     s(plus(?x_2,?y)) = plus(?y,s(?x_2)),
     ?y = plus(?y,0),
     plus(plus(?x_2,?x),?y) = plus(?x_2,plus(?y,?x)),
     plus(plus(0,?y_1),?z_1) = plus(?y_1,?z_1),
     plus(?x,0) = ?x,
     plus(plus(?x_2,0),?x) = plus(?x_2,?x) ]
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 <plus(?x,s(plus(?x_1,?y_1))), plus(plus(?x,s(?x_1)),?y_1)> by Rules <1, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([(plus,1),(s,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([],1),([(s,1),(plus,1)],2)]>
Critical Pair <plus(?x,plus(?y_2,?x_2)), plus(plus(?x,?x_2),?y_2)> by Rules <2, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(plus,1)],2)], [([],2),([],0)]>
Critical Pair <plus(?x,?x_3), plus(plus(?x,0),?x_3)> by Rules <3, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],2),([(plus,1)],3)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <0, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],0),([(plus,1)],0)], [([],0)]>
Critical Pair <s(plus(?x_1,plus(?y,?z))), plus(plus(s(?x_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], [([(plus,1)],1),([],1)]>
Critical Pair <plus(plus(?y,?z),?x_2), plus(plus(?x_2,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <plus(?y,?z), plus(plus(0,?y),?z)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],3)]>
Critical Pair <plus(?y_2,s(?x_1)), s(plus(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, plus(?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 plus(?x_3,0) and ?x_3
strenghten plus(0,?x_4) and ?x_4
strenghten plus(?x_9,?y_9) and plus(?y_9,?x_9)
strenghten s(plus(?x_1,0)) and s(?x_1)
strenghten plus(?x_12,s(0)) and s(?x_12)
strenghten plus(s(0),?x_12) and s(?x_12)
strenghten s(plus(?x_1,?x_10)) and plus(?x_10,s(?x_1))
strenghten s(plus(?x_1,?x_11)) and plus(s(?x_1),?x_11)
strenghten s(plus(?x_1,s(0))) and s(s(?x_1))
strenghten plus(plus(?x,?x_4),0) and plus(?x,?x_4)
strenghten plus(plus(?x,0),?x_3) and plus(?x,?x_3)
strenghten plus(plus(0,?y),?z) and plus(?y,?z)
strenghten plus(plus(?x,?x_2),?y_2) and plus(?x,plus(?y_2,?x_2))
strenghten plus(plus(?x,?x_8),?y_8) and plus(?x,plus(?x_8,?y_8))
strenghten plus(plus(?x_2,?y),?z) and plus(plus(?y,?z),?x_2)
strenghten plus(plus(?x,?x_12),s(0)) and plus(?x,s(?x_12))
strenghten plus(plus(?x,s(?x_1)),?y_1) and plus(?x,s(plus(?x_1,?y_1)))
strenghten plus(plus(s(?x_1),?y),?z) and s(plus(?x_1,plus(?y,?z)))
strenghten plus(plus(?x_1,?x),plus(?y,?z)) and plus(?x_1,plus(plus(?x,?y),?z))
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:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 1)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 2)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<s(plus(?x_2,s(?x))), s(plus(?x,s(?x_2)))> --> <s(s(plus(?x,?x_2))), s(s(plus(?x_2,?x)))> => yes
<s(?x), s(plus(?x,0))> --> <s(?x), s(?x)> => yes
<s(plus(?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(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
success
P':
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Polynomial Interpretation:
  0:= (4)
  s:= (1)*x1
  plus:= (1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (1)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{2,3,1,10}
(cm)Rewrite Rules:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ q(?x_2,?x) = q(q(?x_2,e),?x),
     q(?x_2,?x_1) = q(q(?x_2,?x_1),e),
     len(a) = plus(len(a),len(e)),
     len(q(q(a,?y_2),?z_2)) = plus(len(a),len(q(?y_2,?z_2))),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)) ]
Outer CPs:
   [ e = e,
     q(?y_2,?z_2) = q(q(e,?y_2),?z_2) ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR
{0}
(cm)Rewrite Rules:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR
{8}
(cm)Rewrite Rules:
   [ len(e) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{9}
(cm)Rewrite Rules:
   [ len(a) -> s(0) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Try A Minimal Decomposition {4,7,5,6}{3,0,2,1,10}{8}{9}
{4,7,5,6}
(cm)Rewrite Rules:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x,s(plus(?x_1,?y_1))) = plus(plus(?x,s(?x_1)),?y_1),
     plus(?x,plus(?y_2,?x_2)) = plus(plus(?x,?x_2),?y_2),
     plus(?x,?x_3) = plus(plus(?x,0),?x_3),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ plus(plus(s(?x_1),?y),?z) = s(plus(?x_1,plus(?y,?z))),
     plus(plus(?x,?y),?z) = plus(plus(?y,?z),?x),
     plus(plus(0,?y),?z) = plus(?y,?z),
     s(plus(?x_1,?y_1)) = plus(?y_1,s(?x_1)),
     plus(?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:
   [ s(plus(?x_1,plus(plus(?y,?y_2),?z_2))) = plus(plus(s(?x_1),?y),plus(?y_2,?z_2)),
     s(plus(?x_1,s(plus(?x_3,?z)))) = plus(plus(s(?x_1),s(?x_3)),?z),
     s(plus(?x_1,plus(?z,?y))) = plus(plus(s(?x_1),?y),?z),
     s(plus(?x_1,?z)) = plus(plus(s(?x_1),0),?z),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(s(plus(?x_2,?z)),?x) = plus(plus(?x,s(?x_2)),?z),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     s(plus(?x_2,?z)) = plus(plus(0,s(?x_2)),?z),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_1,plus(?y,?z))) = plus(plus(s(?x_1),?y),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,s(plus(?x_2,?z))) = plus(plus(?x,s(?x_2)),?z),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),s(plus(?x_3,?z))) = plus(?x_1,plus(plus(?x,s(?x_3)),?z)),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(s(?x),?y_1),?z_1) = s(plus(?x,plus(?y_1,?z_1))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_2,s(?x)),?y) = plus(?x_2,s(plus(?x,?y))),
     plus(plus(?x,?y_1),?z_1) = plus(plus(?y_1,?z_1),?x),
     s(plus(?x_2,?y)) = plus(?y,s(?x_2)),
     ?y = plus(?y,0),
     plus(plus(?x_2,?x),?y) = plus(?x_2,plus(?y,?x)),
     plus(plus(0,?y_1),?z_1) = plus(?y_1,?z_1),
     plus(?x,0) = ?x,
     plus(plus(?x_2,0),?x) = plus(?x_2,?x) ]
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 <plus(?x,s(plus(?x_1,?y_1))), plus(plus(?x,s(?x_1)),?y_1)> by Rules <1, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([(plus,1),(s,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([],1),([(s,1),(plus,1)],2)]>
Critical Pair <plus(?x,plus(?y_2,?x_2)), plus(plus(?x,?x_2),?y_2)> by Rules <2, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(plus,1)],2)], [([],2),([],0)]>
Critical Pair <plus(?x,?x_3), plus(plus(?x,0),?x_3)> by Rules <3, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],2),([(plus,1)],3)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <0, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],0),([(plus,1)],0)], [([],0)]>
Critical Pair <s(plus(?x_1,plus(?y,?z))), plus(plus(s(?x_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], [([(plus,1)],1),([],1)]>
Critical Pair <plus(plus(?y,?z),?x_2), plus(plus(?x_2,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <plus(?y,?z), plus(plus(0,?y),?z)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],3)]>
Critical Pair <plus(?y_2,s(?x_1)), s(plus(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, plus(?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 plus(?x_3,0) and ?x_3
strenghten plus(0,?x_4) and ?x_4
strenghten plus(?x_9,?y_9) and plus(?y_9,?x_9)
strenghten s(plus(?x_1,0)) and s(?x_1)
strenghten plus(?x_12,s(0)) and s(?x_12)
strenghten plus(s(0),?x_12) and s(?x_12)
strenghten s(plus(?x_1,?x_10)) and plus(?x_10,s(?x_1))
strenghten s(plus(?x_1,?x_11)) and plus(s(?x_1),?x_11)
strenghten s(plus(?x_1,s(0))) and s(s(?x_1))
strenghten plus(plus(?x,?x_4),0) and plus(?x,?x_4)
strenghten plus(plus(?x,0),?x_3) and plus(?x,?x_3)
strenghten plus(plus(0,?y),?z) and plus(?y,?z)
strenghten plus(plus(?x,?x_2),?y_2) and plus(?x,plus(?y_2,?x_2))
strenghten plus(plus(?x,?x_8),?y_8) and plus(?x,plus(?x_8,?y_8))
strenghten plus(plus(?x_2,?y),?z) and plus(plus(?y,?z),?x_2)
strenghten plus(plus(?x,?x_12),s(0)) and plus(?x,s(?x_12))
strenghten plus(plus(?x,s(?x_1)),?y_1) and plus(?x,s(plus(?x_1,?y_1)))
strenghten plus(plus(s(?x_1),?y),?z) and s(plus(?x_1,plus(?y,?z)))
strenghten plus(plus(?x_1,?x),plus(?y,?z)) and plus(?x_1,plus(plus(?x,?y),?z))
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:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 1)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 2)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<s(plus(?x_2,s(?x))), s(plus(?x,s(?x_2)))> --> <s(s(plus(?x,?x_2))), s(s(plus(?x_2,?x)))> => yes
<s(?x), s(plus(?x,0))> --> <s(?x), s(?x)> => yes
<s(plus(?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(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
success
P':
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Polynomial Interpretation:
  0:= (4)
  s:= (1)*x1
  plus:= (1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (1)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{3,0,2,1,10}
(cm)Rewrite Rules:
   [ q(?x,e) -> ?x,
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(e,?x) -> ?x,
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     len(q(a,?y)) -> plus(len(a),len(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ q(?x,?z_1) = q(?x,q(e,?z_1)),
     q(?x_2,?z_1) = q(e,q(?x_2,?z_1)),
     q(q(q(?x_3,?y_3),?z_3),?z_1) = q(?x_3,q(q(?y_3,?z_3),?z_1)),
     q(?x_3,?x) = q(q(?x_3,?x),e),
     q(?x_3,q(?x_1,q(?y_1,?z_1))) = q(q(?x_3,q(?x_1,?y_1)),?z_1),
     q(?x_3,?x_2) = q(q(?x_3,e),?x_2),
     len(a) = plus(len(a),len(e)),
     len(q(q(a,?y_3),?z_3)) = plus(len(a),len(q(?y_3,?z_3))),
     q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)) ]
Outer CPs:
   [ q(?x_1,?y_1) = q(?x_1,q(?y_1,e)),
     e = e,
     q(?x_1,q(?y_1,q(?y_3,?z_3))) = q(q(q(?x_1,?y_1),?y_3),?z_3),
     q(?y_3,?z_3) = q(q(e,?y_3),?z_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
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:
   [ q(?x_1,q(?y_1,e)) = q(?x_1,?y_1),
     e = e,
     q(?x,q(e,?z_2)) = q(?x,?z_2),
     q(q(?x_4,?x),e) = q(?x_4,?x),
     plus(len(a),len(e)) = len(a),
     q(?x_1,q(?y_1,?y)) = q(q(?x_1,?y_1),q(?y,e)),
     ?x = q(?x,q(e,e)),
     ?y = q(e,q(?y,e)),
     q(q(?x,?y_4),?z_4) = q(?x,q(q(?y_4,?z_4),e)),
     q(q(q(?x_4,q(?y_4,?y)),?y_3),?z_3) = q(q(?x_4,?y_4),q(?y,q(?y_3,?z_3))),
     q(q(?x,?y_3),?z_3) = q(?x,q(e,q(?y_3,?z_3))),
     q(q(?y,?y_3),?z_3) = q(e,q(?y,q(?y_3,?z_3))),
     q(q(q(q(?x,?y_7),?z_7),?y_3),?z_3) = q(?x,q(q(?y_7,?z_7),q(?y_3,?z_3))),
     q(?x,?y) = q(?x,q(?y,e)),
     q(q(q(?x,?y),?y_3),?z_3) = q(?x,q(?y,q(?y_3,?z_3))),
     q(q(?x_1,q(?y_1,?y)),?z) = q(q(?x_1,?y_1),q(?y,?z)),
     q(?x,?z) = q(?x,q(e,?z)),
     q(?y,?z) = q(e,q(?y,?z)),
     q(q(q(?x,?y_4),?z_4),?z) = q(?x,q(q(?y_4,?z_4),?z)),
     q(q(?x_2,q(?y_2,?y)),q(?z,?z_1)) = q(q(q(?x_2,?y_2),q(?y,?z)),?z_1),
     q(?x,q(?z,?z_1)) = q(q(?x,q(e,?z)),?z_1),
     q(?y,q(?z,?z_1)) = q(q(e,q(?y,?z)),?z_1),
     q(q(q(?x,?y_5),?z_5),q(?z,?z_1)) = q(q(?x,q(q(?y_5,?z_5),?z)),?z_1),
     q(q(?x_4,q(?x_5,q(?y_5,?y))),?z) = q(?x_4,q(q(?x_5,?y_5),q(?y,?z))),
     q(q(?x_4,?x),?z) = q(?x_4,q(?x,q(e,?z))),
     q(q(?x_4,q(q(?x,?y_8),?z_8)),?z) = q(?x_4,q(?x,q(q(?y_8,?z_8),?z))),
     q(q(?x,?y),q(?z,?z_1)) = q(q(?x,q(?y,?z)),?z_1),
     q(q(?x_4,q(?x,?y)),?z) = q(?x_4,q(?x,q(?y,?z))),
     q(q(e,?y_3),?z_3) = q(?y_3,?z_3),
     q(e,q(?x,?z_3)) = q(?x,?z_3),
     q(q(?x_4,e),?x) = q(?x_4,?x),
     q(?x_2,q(?y_2,q(q(?y,?y_3),?z_3))) = q(q(q(?x_2,?y_2),?y),q(?y_3,?z_3)),
     q(?x_2,q(?y_2,?y)) = q(q(q(?x_2,?y_2),?y),e),
     q(?x_2,q(?y_2,q(?x_5,q(?y_5,?z)))) = q(q(q(?x_2,?y_2),q(?x_5,?y_5)),?z),
     q(?x_2,q(?y_2,?z)) = q(q(q(?x_2,?y_2),e),?z),
     q(q(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?y = q(q(e,?y),e),
     ?z = q(q(e,e),?z),
     q(?x_2,q(?y_2,q(?y,?z))) = q(q(q(?x_2,?y_2),?y),?z),
     q(?y,?z) = q(q(e,?y),?z),
     q(?x,q(q(?y,?y_1),?z_1)) = q(q(?x,?y),q(?y_1,?z_1)),
     q(?x,?y) = q(q(?x,?y),e),
     q(?x,q(?x_3,q(?y_3,?z))) = q(q(?x,q(?x_3,?y_3)),?z),
     q(?x,?z) = q(q(?x,e),?z),
     q(q(?x_1,?x),q(q(?y,?y_2),?z_2)) = q(?x_1,q(q(?x,?y),q(?y_2,?z_2))),
     q(q(?x_1,?x),q(?x_4,q(?y_4,?z))) = q(?x_1,q(q(?x,q(?x_4,?y_4)),?z)),
     q(q(?x_1,?x),?z) = q(?x_1,q(q(?x,e),?z)),
     q(?x,q(q(q(?y,?y_4),?z_4),?z_3)) = q(q(q(?x,?y),q(?y_4,?z_4)),?z_3),
     q(?x,q(q(?x_6,q(?y_6,?z)),?z_3)) = q(q(q(?x,q(?x_6,?y_6)),?z),?z_3),
     q(?x,q(?z,?z_3)) = q(q(q(?x,e),?z),?z_3),
     plus(len(a),len(q(q(?y,?y_1),?z_1))) = len(q(q(a,?y),q(?y_1,?z_1))),
     plus(len(a),len(?y)) = len(q(q(a,?y),e)),
     plus(len(a),len(q(?x_3,q(?y_3,?z)))) = len(q(q(a,q(?x_3,?y_3)),?z)),
     plus(len(a),len(?z)) = len(q(q(a,e),?z)),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     q(?x,q(q(?y,?z),?z_3)) = q(q(q(?x,?y),?z),?z_3),
     plus(len(a),len(q(?y,?z))) = len(q(q(a,?y),?z)),
     len(a) = plus(len(a),len(e)),
     len(q(q(a,?y_5),?z_5)) = plus(len(a),len(q(?y_5,?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 <q(?x,?z_1), q(?x,q(e,?z_1))> by Rules <0, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([(q,2)],2)]>
Critical Pair <q(?x_2,?z_1), q(e,q(?x_2,?z_1))> by Rules <2, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <q(q(q(?x_3,?y_3),?z_3),?z_1), q(?x_3,q(q(?y_3,?z_3),?z_1))> by Rules <3, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],1)], [([],3)]>
Critical Pair <q(?x_3,?x), q(q(?x_3,?x),e)> by Rules <0, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <q(?x_3,q(?x_1,q(?y_1,?z_1))), q(q(?x_3,q(?x_1,?y_1)),?z_1)> by Rules <1, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],3)], [([],1)]>
Critical Pair <q(?x_3,?x_2), q(q(?x_3,e),?x_2)> by Rules <2, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([(q,1)],0)]>
Critical Pair <len(a), plus(len(a),len(e))> by Rules <0, 4> preceded by [(len,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten q(?x_7,e) and ?x_7
strenghten q(e,?x) and ?x
strenghten q(e,e) and e
strenghten q(q(?x_7,e),e) and ?x_7
strenghten q(q(e,?x_12),e) and ?x_12
strenghten plus(len(a),len(e)) and len(a)
strenghten q(?x,q(e,?z_1)) and q(?x,?z_1)
strenghten q(?x_1,q(?y_1,e)) and q(?x_1,?y_1)
strenghten q(e,q(?x_2,?z_1)) and q(?x_2,?z_1)
strenghten q(q(?x_3,?x),e) and q(?x_3,?x)
strenghten q(q(?x_3,e),?x_2) and q(?x_3,?x_2)
strenghten q(q(e,?y_3),?z_3) and q(?y_3,?z_3)
strenghten plus(len(a),len(q(e,e))) and len(a)
strenghten q(?x_1,q(?y_1,q(e,e))) and q(?x_1,?y_1)
strenghten q(?x_7,q(q(e,e),?z_1)) and q(?x_7,?z_1)
strenghten q(e,q(?x_1,q(?y_1,e))) and q(?x_1,?y_1)
strenghten q(e,q(q(?x_12,e),?z_1)) and q(?x_12,?z_1)
strenghten q(q(?x_3,?x_7),q(e,e)) and q(?x_3,?x_7)
strenghten q(q(?x_3,e),q(?x_12,e)) and q(?x_3,?x_12)
strenghten plus(len(a),len(q(?y_3,?z_3))) and len(q(q(a,?y_3),?z_3))
strenghten q(?x_1,q(?y_1,q(?y_3,?z_3))) and q(q(q(?x_1,?y_1),?y_3),?z_3)
strenghten q(?x_3,q(q(?y_3,?z_3),?z_1)) and q(q(q(?x_3,?y_3),?z_3),?z_1)
strenghten q(q(?x,?y),q(?z,?z_1)) and q(q(?x,q(?y,?z)),?z_1)
strenghten q(q(?x_1,?x),q(?y,?z)) and q(?x_1,q(q(?x,?y),?z))
strenghten q(q(?x_3,q(?x_1,?y_1)),?z_1) and q(?x_3,q(?x_1,q(?y_1,?z_1)))
obtain 62 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <plus(len(a),len(e)), len(a)>
Direct Methods: not CR
{8}
(cm)Rewrite Rules:
   [ len(e) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{9}
(cm)Rewrite Rules:
   [ len(a) -> s(0) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Try A Minimal Decomposition {4,7,5,6}{2,3,10,0,1}{8}{9}
{4,7,5,6}
(cm)Rewrite Rules:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x,s(plus(?x_1,?y_1))) = plus(plus(?x,s(?x_1)),?y_1),
     plus(?x,plus(?y_2,?x_2)) = plus(plus(?x,?x_2),?y_2),
     plus(?x,?x_3) = plus(plus(?x,0),?x_3),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ plus(plus(s(?x_1),?y),?z) = s(plus(?x_1,plus(?y,?z))),
     plus(plus(?x,?y),?z) = plus(plus(?y,?z),?x),
     plus(plus(0,?y),?z) = plus(?y,?z),
     s(plus(?x_1,?y_1)) = plus(?y_1,s(?x_1)),
     plus(?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:
   [ s(plus(?x_1,plus(plus(?y,?y_2),?z_2))) = plus(plus(s(?x_1),?y),plus(?y_2,?z_2)),
     s(plus(?x_1,s(plus(?x_3,?z)))) = plus(plus(s(?x_1),s(?x_3)),?z),
     s(plus(?x_1,plus(?z,?y))) = plus(plus(s(?x_1),?y),?z),
     s(plus(?x_1,?z)) = plus(plus(s(?x_1),0),?z),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(s(plus(?x_2,?z)),?x) = plus(plus(?x,s(?x_2)),?z),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     s(plus(?x_2,?z)) = plus(plus(0,s(?x_2)),?z),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_1,plus(?y,?z))) = plus(plus(s(?x_1),?y),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,s(plus(?x_2,?z))) = plus(plus(?x,s(?x_2)),?z),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),s(plus(?x_3,?z))) = plus(?x_1,plus(plus(?x,s(?x_3)),?z)),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(s(?x),?y_1),?z_1) = s(plus(?x,plus(?y_1,?z_1))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_2,s(?x)),?y) = plus(?x_2,s(plus(?x,?y))),
     plus(plus(?x,?y_1),?z_1) = plus(plus(?y_1,?z_1),?x),
     s(plus(?x_2,?y)) = plus(?y,s(?x_2)),
     ?y = plus(?y,0),
     plus(plus(?x_2,?x),?y) = plus(?x_2,plus(?y,?x)),
     plus(plus(0,?y_1),?z_1) = plus(?y_1,?z_1),
     plus(?x,0) = ?x,
     plus(plus(?x_2,0),?x) = plus(?x_2,?x) ]
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 <plus(?x,s(plus(?x_1,?y_1))), plus(plus(?x,s(?x_1)),?y_1)> by Rules <1, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([(plus,1),(s,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([],1),([(s,1),(plus,1)],2)]>
Critical Pair <plus(?x,plus(?y_2,?x_2)), plus(plus(?x,?x_2),?y_2)> by Rules <2, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(plus,1)],2)], [([],2),([],0)]>
Critical Pair <plus(?x,?x_3), plus(plus(?x,0),?x_3)> by Rules <3, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],2),([(plus,1)],3)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <0, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],0),([(plus,1)],0)], [([],0)]>
Critical Pair <s(plus(?x_1,plus(?y,?z))), plus(plus(s(?x_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], [([(plus,1)],1),([],1)]>
Critical Pair <plus(plus(?y,?z),?x_2), plus(plus(?x_2,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <plus(?y,?z), plus(plus(0,?y),?z)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],3)]>
Critical Pair <plus(?y_2,s(?x_1)), s(plus(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, plus(?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 plus(?x_3,0) and ?x_3
strenghten plus(0,?x_4) and ?x_4
strenghten plus(?x_9,?y_9) and plus(?y_9,?x_9)
strenghten s(plus(?x_1,0)) and s(?x_1)
strenghten plus(?x_12,s(0)) and s(?x_12)
strenghten plus(s(0),?x_12) and s(?x_12)
strenghten s(plus(?x_1,?x_10)) and plus(?x_10,s(?x_1))
strenghten s(plus(?x_1,?x_11)) and plus(s(?x_1),?x_11)
strenghten s(plus(?x_1,s(0))) and s(s(?x_1))
strenghten plus(plus(?x,?x_4),0) and plus(?x,?x_4)
strenghten plus(plus(?x,0),?x_3) and plus(?x,?x_3)
strenghten plus(plus(0,?y),?z) and plus(?y,?z)
strenghten plus(plus(?x,?x_2),?y_2) and plus(?x,plus(?y_2,?x_2))
strenghten plus(plus(?x,?x_8),?y_8) and plus(?x,plus(?x_8,?y_8))
strenghten plus(plus(?x_2,?y),?z) and plus(plus(?y,?z),?x_2)
strenghten plus(plus(?x,?x_12),s(0)) and plus(?x,s(?x_12))
strenghten plus(plus(?x,s(?x_1)),?y_1) and plus(?x,s(plus(?x_1,?y_1)))
strenghten plus(plus(s(?x_1),?y),?z) and s(plus(?x_1,plus(?y,?z)))
strenghten plus(plus(?x_1,?x),plus(?y,?z)) and plus(?x_1,plus(plus(?x,?y),?z))
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:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 1)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 2)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<s(plus(?x_2,s(?x))), s(plus(?x,s(?x_2)))> --> <s(s(plus(?x,?x_2))), s(s(plus(?x_2,?x)))> => yes
<s(?x), s(plus(?x,0))> --> <s(?x), s(?x)> => yes
<s(plus(?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(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
success
P':
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Polynomial Interpretation:
  0:= (4)
  s:= (1)*x1
  plus:= (1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (1)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{2,3,10,0,1}
(cm)Rewrite Rules:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?x,
     len(q(a,?y)) -> plus(len(a),len(?y)),
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z) ]
Apply Direct Methods...
Inner CPs:
   [ len(a) = plus(len(a),len(e)),
     len(q(q(a,?y_4),?z_4)) = plus(len(a),len(q(?y_4,?z_4))),
     q(?x,?z_3) = q(e,q(?x,?z_3)),
     q(?x_1,?z_3) = q(?x_1,q(e,?z_3)),
     q(q(q(?x_4,?y_4),?z_4),?z_3) = q(?x_4,q(q(?y_4,?z_4),?z_3)),
     q(?x_4,?x) = q(q(?x_4,e),?x),
     q(?x_4,?x_1) = q(q(?x_4,?x_1),e),
     q(?x_4,q(?x_3,q(?y_3,?z_3))) = q(q(?x_4,q(?x_3,?y_3)),?z_3),
     q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)) ]
Outer CPs:
   [ e = e,
     q(?y_4,?z_4) = q(q(e,?y_4),?z_4),
     q(?x_3,?y_3) = q(?x_3,q(?y_3,e)),
     q(?x_3,q(?y_3,q(?y_4,?z_4))) = q(q(q(?x_3,?y_3),?y_4),?z_4) ]
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:
   [ e = e,
     q(q(e,?y_4),?z_4) = q(?y_4,?z_4),
     q(e,q(?x,?z_4)) = q(?x,?z_4),
     q(q(?x_5,e),?x) = q(?x_5,?x),
     q(?x_3,q(?y_3,e)) = q(?x_3,?y_3),
     plus(len(a),len(e)) = len(a),
     q(?x,q(e,?z_4)) = q(?x,?z_4),
     q(q(?x_5,?x),e) = q(?x_5,?x),
     len(a) = plus(len(a),len(e)),
     len(q(q(a,?y_5),?z_5)) = plus(len(a),len(q(?y_5,?z_5))),
     q(?x_1,q(?y_1,?y)) = q(q(?x_1,?y_1),q(?y,e)),
     ?y = q(e,q(?y,e)),
     ?x = q(?x,q(e,e)),
     q(q(?x,?y_5),?z_5) = q(?x,q(q(?y_5,?z_5),e)),
     q(q(q(?x_5,q(?y_5,?y)),?y_4),?z_4) = q(q(?x_5,?y_5),q(?y,q(?y_4,?z_4))),
     q(q(?y,?y_4),?z_4) = q(e,q(?y,q(?y_4,?z_4))),
     q(q(?x,?y_4),?z_4) = q(?x,q(e,q(?y_4,?z_4))),
     q(q(q(q(?x,?y_9),?z_9),?y_4),?z_4) = q(?x,q(q(?y_9,?z_9),q(?y_4,?z_4))),
     q(?x,?y) = q(?x,q(?y,e)),
     q(q(q(?x,?y),?y_4),?z_4) = q(?x,q(?y,q(?y_4,?z_4))),
     q(q(?x_1,q(?y_1,?y)),?z) = q(q(?x_1,?y_1),q(?y,?z)),
     q(?y,?z) = q(e,q(?y,?z)),
     q(?x,?z) = q(?x,q(e,?z)),
     q(q(q(?x,?y_5),?z_5),?z) = q(?x,q(q(?y_5,?z_5),?z)),
     q(q(?x_2,q(?y_2,?y)),q(?z,?z_1)) = q(q(q(?x_2,?y_2),q(?y,?z)),?z_1),
     q(?y,q(?z,?z_1)) = q(q(e,q(?y,?z)),?z_1),
     q(?x,q(?z,?z_1)) = q(q(?x,q(e,?z)),?z_1),
     q(q(q(?x,?y_6),?z_6),q(?z,?z_1)) = q(q(?x,q(q(?y_6,?z_6),?z)),?z_1),
     q(q(?x_5,q(?x_6,q(?y_6,?y))),?z) = q(?x_5,q(q(?x_6,?y_6),q(?y,?z))),
     q(q(?x_5,?x),?z) = q(?x_5,q(?x,q(e,?z))),
     q(q(?x_5,q(q(?x,?y_10),?z_10)),?z) = q(?x_5,q(?x,q(q(?y_10,?z_10),?z))),
     q(q(?x,?y),q(?z,?z_1)) = q(q(?x,q(?y,?z)),?z_1),
     q(q(?x_5,q(?x,?y)),?z) = q(?x_5,q(?x,q(?y,?z))),
     q(q(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?z = q(q(e,e),?z),
     ?y = q(q(e,?y),e),
     q(?x_4,q(?y_4,q(q(?y,?y_5),?z_5))) = q(q(q(?x_4,?y_4),?y),q(?y_5,?z_5)),
     q(?x_4,q(?y_4,?z)) = q(q(q(?x_4,?y_4),e),?z),
     q(?x_4,q(?y_4,?y)) = q(q(q(?x_4,?y_4),?y),e),
     q(?x_4,q(?y_4,q(?x_9,q(?y_9,?z)))) = q(q(q(?x_4,?y_4),q(?x_9,?y_9)),?z),
     q(?y,?z) = q(q(e,?y),?z),
     q(?x_4,q(?y_4,q(?y,?z))) = q(q(q(?x_4,?y_4),?y),?z),
     q(?x,q(q(?y,?y_1),?z_1)) = q(q(?x,?y),q(?y_1,?z_1)),
     q(?x,?z) = q(q(?x,e),?z),
     q(?x,?y) = q(q(?x,?y),e),
     q(?x,q(?x_5,q(?y_5,?z))) = q(q(?x,q(?x_5,?y_5)),?z),
     q(q(?x_1,?x),q(q(?y,?y_2),?z_2)) = q(?x_1,q(q(?x,?y),q(?y_2,?z_2))),
     q(q(?x_1,?x),?z) = q(?x_1,q(q(?x,e),?z)),
     q(q(?x_1,?x),q(?x_6,q(?y_6,?z))) = q(?x_1,q(q(?x,q(?x_6,?y_6)),?z)),
     plus(len(a),len(q(q(?y,?y_1),?z_1))) = len(q(q(a,?y),q(?y_1,?z_1))),
     plus(len(a),len(?z)) = len(q(q(a,e),?z)),
     plus(len(a),len(?y)) = len(q(q(a,?y),e)),
     plus(len(a),len(q(?x_5,q(?y_5,?z)))) = len(q(q(a,q(?x_5,?y_5)),?z)),
     q(?x,q(q(q(?y,?y_6),?z_6),?z_5)) = q(q(q(?x,?y),q(?y_6,?z_6)),?z_5),
     q(?x,q(?z,?z_5)) = q(q(q(?x,e),?z),?z_5),
     q(?x,q(q(?x_10,q(?y_10,?z)),?z_5)) = q(q(q(?x,q(?x_10,?y_10)),?z),?z_5),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     plus(len(a),len(q(?y,?z))) = len(q(q(a,?y),?z)),
     q(?x,q(q(?y,?z),?z_5)) = q(q(q(?x,?y),?z),?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 <len(a), plus(len(a),len(e))> by Rules <1, 2> preceded by [(len,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten q(?x_7,e) and ?x_7
strenghten q(e,?x_1) and ?x_1
strenghten q(e,e) and e
strenghten q(q(?x_7,e),e) and ?x_7
strenghten q(q(e,?x_12),e) and ?x_12
strenghten plus(len(a),len(e)) and len(a)
strenghten q(?x_1,q(e,?z_3)) and q(?x_1,?z_3)
strenghten q(?x_3,q(?y_3,e)) and q(?x_3,?y_3)
strenghten q(e,q(?x,?z_3)) and q(?x,?z_3)
strenghten q(q(?x_4,?x_1),e) and q(?x_4,?x_1)
strenghten q(q(?x_4,e),?x) and q(?x_4,?x)
strenghten q(q(e,?y_4),?z_4) and q(?y_4,?z_4)
strenghten plus(len(a),len(q(e,e))) and len(a)
strenghten q(?x_3,q(?y_3,q(e,e))) and q(?x_3,?y_3)
strenghten q(?x_7,q(q(e,e),?z_3)) and q(?x_7,?z_3)
strenghten q(e,q(?x_3,q(?y_3,e))) and q(?x_3,?y_3)
strenghten q(e,q(q(?x_12,e),?z_3)) and q(?x_12,?z_3)
strenghten q(q(?x_4,?x_7),q(e,e)) and q(?x_4,?x_7)
strenghten q(q(?x_4,e),q(?x_12,e)) and q(?x_4,?x_12)
strenghten plus(len(a),len(q(?y_4,?z_4))) and len(q(q(a,?y_4),?z_4))
strenghten q(?x_3,q(?y_3,q(?y_4,?z_4))) and q(q(q(?x_3,?y_3),?y_4),?z_4)
strenghten q(?x_4,q(q(?y_4,?z_4),?z_3)) and q(q(q(?x_4,?y_4),?z_4),?z_3)
strenghten q(q(?x,?y),q(?z,?z_1)) and q(q(?x,q(?y,?z)),?z_1)
strenghten q(q(?x_1,?x),q(?y,?z)) and q(?x_1,q(q(?x,?y),?z))
strenghten q(q(?x_4,q(?x_3,?y_3)),?z_3) and q(?x_4,q(?x_3,q(?y_3,?z_3)))
obtain 62 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <plus(len(a),len(e)), len(a)>
Direct Methods: not CR
{8}
(cm)Rewrite Rules:
   [ len(e) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{9}
(cm)Rewrite Rules:
   [ len(a) -> s(0) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Try A Minimal Decomposition {4,7,5,6}{10,1,2,3}{0}{8}{9}
{4,7,5,6}
(cm)Rewrite Rules:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x,s(plus(?x_1,?y_1))) = plus(plus(?x,s(?x_1)),?y_1),
     plus(?x,plus(?y_2,?x_2)) = plus(plus(?x,?x_2),?y_2),
     plus(?x,?x_3) = plus(plus(?x,0),?x_3),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ plus(plus(s(?x_1),?y),?z) = s(plus(?x_1,plus(?y,?z))),
     plus(plus(?x,?y),?z) = plus(plus(?y,?z),?x),
     plus(plus(0,?y),?z) = plus(?y,?z),
     s(plus(?x_1,?y_1)) = plus(?y_1,s(?x_1)),
     plus(?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:
   [ s(plus(?x_1,plus(plus(?y,?y_2),?z_2))) = plus(plus(s(?x_1),?y),plus(?y_2,?z_2)),
     s(plus(?x_1,s(plus(?x_3,?z)))) = plus(plus(s(?x_1),s(?x_3)),?z),
     s(plus(?x_1,plus(?z,?y))) = plus(plus(s(?x_1),?y),?z),
     s(plus(?x_1,?z)) = plus(plus(s(?x_1),0),?z),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(s(plus(?x_2,?z)),?x) = plus(plus(?x,s(?x_2)),?z),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     s(plus(?x_2,?z)) = plus(plus(0,s(?x_2)),?z),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_1,plus(?y,?z))) = plus(plus(s(?x_1),?y),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,s(plus(?x_2,?z))) = plus(plus(?x,s(?x_2)),?z),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),s(plus(?x_3,?z))) = plus(?x_1,plus(plus(?x,s(?x_3)),?z)),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(s(?x),?y_1),?z_1) = s(plus(?x,plus(?y_1,?z_1))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_2,s(?x)),?y) = plus(?x_2,s(plus(?x,?y))),
     plus(plus(?x,?y_1),?z_1) = plus(plus(?y_1,?z_1),?x),
     s(plus(?x_2,?y)) = plus(?y,s(?x_2)),
     ?y = plus(?y,0),
     plus(plus(?x_2,?x),?y) = plus(?x_2,plus(?y,?x)),
     plus(plus(0,?y_1),?z_1) = plus(?y_1,?z_1),
     plus(?x,0) = ?x,
     plus(plus(?x_2,0),?x) = plus(?x_2,?x) ]
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 <plus(?x,s(plus(?x_1,?y_1))), plus(plus(?x,s(?x_1)),?y_1)> by Rules <1, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([(plus,1),(s,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([],1),([(s,1),(plus,1)],2)]>
Critical Pair <plus(?x,plus(?y_2,?x_2)), plus(plus(?x,?x_2),?y_2)> by Rules <2, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(plus,1)],2)], [([],2),([],0)]>
Critical Pair <plus(?x,?x_3), plus(plus(?x,0),?x_3)> by Rules <3, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],2),([(plus,1)],3)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <0, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],0),([(plus,1)],0)], [([],0)]>
Critical Pair <s(plus(?x_1,plus(?y,?z))), plus(plus(s(?x_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], [([(plus,1)],1),([],1)]>
Critical Pair <plus(plus(?y,?z),?x_2), plus(plus(?x_2,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <plus(?y,?z), plus(plus(0,?y),?z)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],3)]>
Critical Pair <plus(?y_2,s(?x_1)), s(plus(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, plus(?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 plus(?x_3,0) and ?x_3
strenghten plus(0,?x_4) and ?x_4
strenghten plus(?x_9,?y_9) and plus(?y_9,?x_9)
strenghten s(plus(?x_1,0)) and s(?x_1)
strenghten plus(?x_12,s(0)) and s(?x_12)
strenghten plus(s(0),?x_12) and s(?x_12)
strenghten s(plus(?x_1,?x_10)) and plus(?x_10,s(?x_1))
strenghten s(plus(?x_1,?x_11)) and plus(s(?x_1),?x_11)
strenghten s(plus(?x_1,s(0))) and s(s(?x_1))
strenghten plus(plus(?x,?x_4),0) and plus(?x,?x_4)
strenghten plus(plus(?x,0),?x_3) and plus(?x,?x_3)
strenghten plus(plus(0,?y),?z) and plus(?y,?z)
strenghten plus(plus(?x,?x_2),?y_2) and plus(?x,plus(?y_2,?x_2))
strenghten plus(plus(?x,?x_8),?y_8) and plus(?x,plus(?x_8,?y_8))
strenghten plus(plus(?x_2,?y),?z) and plus(plus(?y,?z),?x_2)
strenghten plus(plus(?x,?x_12),s(0)) and plus(?x,s(?x_12))
strenghten plus(plus(?x,s(?x_1)),?y_1) and plus(?x,s(plus(?x_1,?y_1)))
strenghten plus(plus(s(?x_1),?y),?z) and s(plus(?x_1,plus(?y,?z)))
strenghten plus(plus(?x_1,?x),plus(?y,?z)) and plus(?x_1,plus(plus(?x,?y),?z))
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:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 1)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 2)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<s(plus(?x_2,s(?x))), s(plus(?x,s(?x_2)))> --> <s(s(plus(?x,?x_2))), s(s(plus(?x_2,?x)))> => yes
<s(?x), s(plus(?x,0))> --> <s(?x), s(?x)> => yes
<s(plus(?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(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
success
P':
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Polynomial Interpretation:
  0:= (4)
  s:= (1)*x1
  plus:= (1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (1)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{10,1,2,3}
(cm)Rewrite Rules:
   [ len(q(a,?y)) -> plus(len(a),len(?y)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     q(e,?x) -> ?x,
     q(?x,e) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ len(q(q(a,?y_1),?z_1)) = plus(len(a),len(q(?y_1,?z_1))),
     len(a) = plus(len(a),len(e)),
     q(?x_1,?x_2) = q(q(?x_1,e),?x_2),
     q(?x_1,?x_3) = q(q(?x_1,?x_3),e),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)) ]
Outer CPs:
   [ q(q(e,?y_1),?z_1) = q(?y_1,?z_1),
     e = e ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR
{0}
(cm)Rewrite Rules:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR
{8}
(cm)Rewrite Rules:
   [ len(e) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{9}
(cm)Rewrite Rules:
   [ len(a) -> s(0) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Try A Minimal Decomposition {4,7,5,6}{10,1,3,0,2}{8}{9}
{4,7,5,6}
(cm)Rewrite Rules:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(?x,?y) -> plus(?y,?x),
     plus(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ plus(?x,s(plus(?x_1,?y_1))) = plus(plus(?x,s(?x_1)),?y_1),
     plus(?x,plus(?y_2,?x_2)) = plus(plus(?x,?x_2),?y_2),
     plus(?x,?x_3) = plus(plus(?x,0),?x_3),
     plus(?x_1,plus(plus(?x,?y),?z)) = plus(plus(?x_1,?x),plus(?y,?z)) ]
Outer CPs:
   [ plus(plus(s(?x_1),?y),?z) = s(plus(?x_1,plus(?y,?z))),
     plus(plus(?x,?y),?z) = plus(plus(?y,?z),?x),
     plus(plus(0,?y),?z) = plus(?y,?z),
     s(plus(?x_1,?y_1)) = plus(?y_1,s(?x_1)),
     plus(?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:
   [ s(plus(?x_1,plus(plus(?y,?y_2),?z_2))) = plus(plus(s(?x_1),?y),plus(?y_2,?z_2)),
     s(plus(?x_1,s(plus(?x_3,?z)))) = plus(plus(s(?x_1),s(?x_3)),?z),
     s(plus(?x_1,plus(?z,?y))) = plus(plus(s(?x_1),?y),?z),
     s(plus(?x_1,?z)) = plus(plus(s(?x_1),0),?z),
     plus(plus(plus(?y,?y_1),?z_1),?x) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(s(plus(?x_2,?z)),?x) = plus(plus(?x,s(?x_2)),?z),
     plus(plus(?z,?y),?x) = plus(plus(?x,?y),?z),
     plus(?z,?x) = plus(plus(?x,0),?z),
     plus(plus(?y,?y_1),?z_1) = plus(plus(0,?y),plus(?y_1,?z_1)),
     s(plus(?x_2,?z)) = plus(plus(0,s(?x_2)),?z),
     plus(?z,?y) = plus(plus(0,?y),?z),
     ?z = plus(plus(0,0),?z),
     s(plus(?x_1,plus(?y,?z))) = plus(plus(s(?x_1),?y),?z),
     plus(plus(?y,?z),?x) = plus(plus(?x,?y),?z),
     plus(?y,?z) = plus(plus(0,?y),?z),
     plus(?x,plus(plus(?y,?y_1),?z_1)) = plus(plus(?x,?y),plus(?y_1,?z_1)),
     plus(?x,s(plus(?x_2,?z))) = plus(plus(?x,s(?x_2)),?z),
     plus(?x,plus(?z,?y)) = plus(plus(?x,?y),?z),
     plus(?x,?z) = plus(plus(?x,0),?z),
     plus(plus(?x_1,?x),plus(plus(?y,?y_2),?z_2)) = plus(?x_1,plus(plus(?x,?y),plus(?y_2,?z_2))),
     plus(plus(?x_1,?x),s(plus(?x_3,?z))) = plus(?x_1,plus(plus(?x,s(?x_3)),?z)),
     plus(plus(?x_1,?x),plus(?z,?y)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(?x_1,?x),?z) = plus(?x_1,plus(plus(?x,0),?z)),
     plus(plus(?x_1,?x),plus(?y,?z)) = plus(?x_1,plus(plus(?x,?y),?z)),
     plus(plus(s(?x),?y_1),?z_1) = s(plus(?x,plus(?y_1,?z_1))),
     plus(?y,s(?x)) = s(plus(?x,?y)),
     plus(plus(?x_2,s(?x)),?y) = plus(?x_2,s(plus(?x,?y))),
     plus(plus(?x,?y_1),?z_1) = plus(plus(?y_1,?z_1),?x),
     s(plus(?x_2,?y)) = plus(?y,s(?x_2)),
     ?y = plus(?y,0),
     plus(plus(?x_2,?x),?y) = plus(?x_2,plus(?y,?x)),
     plus(plus(0,?y_1),?z_1) = plus(?y_1,?z_1),
     plus(?x,0) = ?x,
     plus(plus(?x_2,0),?x) = plus(?x_2,?x) ]
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 <plus(?x,s(plus(?x_1,?y_1))), plus(plus(?x,s(?x_1)),?y_1)> by Rules <1, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([(plus,1),(s,1)],2),([],1)]>
 joinable by a reduction of rules <[([],2),([],1),([(s,1)],2),([(s,1)],0)], [([(plus,1)],2),([(plus,1)],1),([],1),([(s,1),(plus,1)],2)]>
Critical Pair <plus(?x,plus(?y_2,?x_2)), plus(plus(?x,?x_2),?y_2)> by Rules <2, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([(plus,2)],2),([],0)], []>
 joinable by a reduction of rules <[([],0),([(plus,1)],2)], [([],2),([],0)]>
Critical Pair <plus(?x,?x_3), plus(plus(?x,0),?x_3)> by Rules <3, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[], [([(plus,1)],2),([(plus,1)],3)]>
Critical Pair <plus(?x_1,plus(plus(?x,?y),?z)), plus(plus(?x_1,?x),plus(?y,?z))> by Rules <0, 0> preceded by [(plus,2)]
 joinable by a reduction of rules <[([],0),([(plus,1)],0)], [([],0)]>
Critical Pair <s(plus(?x_1,plus(?y,?z))), plus(plus(s(?x_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([(s,1)],0)], [([(plus,1)],1),([],1)]>
Critical Pair <plus(plus(?y,?z),?x_2), plus(plus(?x_2,?y),?z)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <plus(?y,?z), plus(plus(0,?y),?z)> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([(plus,1)],3)]>
Critical Pair <plus(?y_2,s(?x_1)), s(plus(?x_1,?y_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <?x_3, plus(?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 plus(?x_3,0) and ?x_3
strenghten plus(0,?x_4) and ?x_4
strenghten plus(?x_9,?y_9) and plus(?y_9,?x_9)
strenghten s(plus(?x_1,0)) and s(?x_1)
strenghten plus(?x_12,s(0)) and s(?x_12)
strenghten plus(s(0),?x_12) and s(?x_12)
strenghten s(plus(?x_1,?x_10)) and plus(?x_10,s(?x_1))
strenghten s(plus(?x_1,?x_11)) and plus(s(?x_1),?x_11)
strenghten s(plus(?x_1,s(0))) and s(s(?x_1))
strenghten plus(plus(?x,?x_4),0) and plus(?x,?x_4)
strenghten plus(plus(?x,0),?x_3) and plus(?x,?x_3)
strenghten plus(plus(0,?y),?z) and plus(?y,?z)
strenghten plus(plus(?x,?x_2),?y_2) and plus(?x,plus(?y_2,?x_2))
strenghten plus(plus(?x,?x_8),?y_8) and plus(?x,plus(?x_8,?y_8))
strenghten plus(plus(?x_2,?y),?z) and plus(plus(?y,?z),?x_2)
strenghten plus(plus(?x,?x_12),s(0)) and plus(?x,s(?x_12))
strenghten plus(plus(?x,s(?x_1)),?y_1) and plus(?x,s(plus(?x_1,?y_1)))
strenghten plus(plus(s(?x_1),?y),?z) and s(plus(?x_1,plus(?y,?z)))
strenghten plus(plus(?x_1,?x),plus(?y,?z)) and plus(?x_1,plus(plus(?x,?y),?z))
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:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 1)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 2 (linear)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
CP(S,symP):
<s(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), plus(?y,s(?x))> => no
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(plus(?x_1,0),?x)> => no
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, plus(?x,0)> => no
check joinability condition:
check modulo reachablity from plus(?x_1,s(plus(?x,?y))) to plus(plus(?x_1,s(?x)),?y): maybe not reachable
check modulo reachablity from s(plus(?x,?y)) to plus(?y,s(?x)): maybe not reachable
check modulo reachablity from plus(?x_1,?x) to plus(plus(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to plus(?x,0): maybe not reachable
failed
failure(Step 2)
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added S-Rules:
   [ plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
Added P-Rules:
   [ ]
replace: plus(s(?x),?y) -> s(plus(?x,?y)) => plus(s(?x),?y) -> s(plus(?y,?x))
STEP: 3 (relative)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x ]
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Polynomial Interpretation:
  0:= (2)
  s:= (4)+(8)*x1
  plus:= (1)*x1+(2)*x1*x2+(1)*x2
retract plus(0,?x) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (4)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
S: terminating
CP(S,S):
<s(plus(?x_2,s(?x))), s(plus(?x,s(?x_2)))> --> <s(s(plus(?x,?x_2))), s(s(plus(?x_2,?x)))> => yes
<s(?x), s(plus(?x,0))> --> <s(?x), s(?x)> => yes
<s(plus(?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(plus(?x,plus(?y_1,?z_1))), plus(plus(s(?x),?y_1),?z_1)> --> <s(plus(?x,plus(?y_1,?z_1))), s(plus(plus(?x,?y_1),?z_1))> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,s(?x)),?y)> --> <s(plus(plus(?x,?y),?x_1)), s(plus(plus(?x,?x_1),?y))> => no
<plus(s(plus(?x,?y)),?z_1), plus(s(?x),plus(?y,?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(?x,plus(?y,?z_1)))> => yes
<s(plus(?x,?y)), plus(?y,s(?x))> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?y_1,?z_1), plus(plus(0,?y_1),?z_1)> --> <plus(?y_1,?z_1), plus(?y_1,?z_1)> => yes
<plus(?x_1,?x), plus(plus(?x_1,0),?x)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x,?z_1), plus(0,plus(?x,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(?x,0)> --> <?x, ?x> => yes
<plus(?x_1,s(plus(?x,?y))), plus(plus(?x_1,?y),s(?x))> --> <s(plus(plus(?x,?y),?x_1)), s(plus(?x,plus(?x_1,?y)))> => no
<s(plus(?x,plus(?x_1,?y_1))), plus(?x_1,plus(?y_1,s(?x)))> --> <s(plus(?x,plus(?x_1,?y_1))), s(plus(plus(?x,?y_1),?x_1))> => no
<plus(s(plus(?x,?y)),?z_1), plus(?y,plus(s(?x),?z_1))> --> <s(plus(plus(?x,?y),?z_1)), s(plus(plus(?x,?z_1),?y))> => no
<s(plus(?x,?y)), plus(s(?x),?y)> --> <s(plus(?x,?y)), s(plus(?x,?y))> => yes
<plus(?x_1,?x), plus(plus(?x_1,?x),0)> --> <plus(?x_1,?x), plus(?x_1,?x)> => yes
<plus(?x_1,?y_1), plus(?x_1,plus(?y_1,0))> --> <plus(?x_1,?y_1), plus(?x_1,?y_1)> => yes
<plus(?x,?z_1), plus(?x,plus(0,?z_1))> --> <plus(?x,?z_1), plus(?x,?z_1)> => yes
<?x, plus(0,?x)> --> <?x, ?x> => yes
check joinability condition:
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(plus(?x,?x_1),?y)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?x_1)) and s(plus(?x,plus(?x_1,?y))): joinable by {1}
check modulo joinability of s(plus(?x,plus(?x_1,?y_1))) and s(plus(plus(?x,?y_1),?x_1)): joinable by {1}
check modulo joinability of s(plus(plus(?x,?y),?z_1)) and s(plus(plus(?x,?z_1),?y)): joinable by {1}
success
P':
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Check relative termination:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
   [ plus(plus(?x,?y),?z) -> plus(?x,plus(?y,?z)) ]
Polynomial Interpretation:
  0:= (4)
  s:= (1)*x1
  plus:= (1)*x1+(1)*x2
retract plus(0,?x) -> ?x
retract plus(?x,0) -> ?x
Polynomial Interpretation:
  0:= 0
  s:= (1)+(1)*x1
  plus:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ plus(s(?x),?y) -> s(plus(?x,?y)),
     plus(0,?x) -> ?x,
     plus(?y,s(?x)) -> s(plus(?x,?y)),
     plus(?x,0) -> ?x ]
P:
   [ plus(?x,plus(?y,?z)) -> plus(plus(?x,?y),?z),
     plus(?x,?y) -> plus(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR
{10,1,3,0,2}
(cm)Rewrite Rules:
   [ len(q(a,?y)) -> plus(len(a),len(?y)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     q(?x,e) -> ?x,
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(e,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ len(q(q(a,?y_1),?z_1)) = plus(len(a),len(q(?y_1,?z_1))),
     len(a) = plus(len(a),len(e)),
     q(?x_1,?x_2) = q(q(?x_1,?x_2),e),
     q(?x_1,q(?x_3,q(?y_3,?z_3))) = q(q(?x_1,q(?x_3,?y_3)),?z_3),
     q(?x_1,?x_4) = q(q(?x_1,e),?x_4),
     q(q(q(?x_1,?y_1),?z_1),?z_3) = q(?x_1,q(q(?y_1,?z_1),?z_3)),
     q(?x_2,?z_3) = q(?x_2,q(e,?z_3)),
     q(?x_4,?z_3) = q(e,q(?x_4,?z_3)),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)),
     q(q(?x,q(?y,?z)),?z_1) = q(q(?x,?y),q(?z,?z_1)) ]
Outer CPs:
   [ q(q(q(?x_3,?y_3),?y_1),?z_1) = q(?x_3,q(?y_3,q(?y_1,?z_1))),
     q(q(e,?y_1),?z_1) = q(?y_1,?z_1),
     q(?x_3,?y_3) = q(?x_3,q(?y_3,e)),
     e = e ]
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:
   [ len(q(q(a,?y_2),?z_2)) = plus(len(a),len(q(?y_2,?z_2))),
     len(a) = plus(len(a),len(e)),
     q(?x_3,q(?y_3,q(q(?y,?y_4),?z_4))) = q(q(q(?x_3,?y_3),?y),q(?y_4,?z_4)),
     q(?x_3,q(?y_3,?y)) = q(q(q(?x_3,?y_3),?y),e),
     q(?x_3,q(?y_3,q(?x_7,q(?y_7,?z)))) = q(q(q(?x_3,?y_3),q(?x_7,?y_7)),?z),
     q(?x_3,q(?y_3,?z)) = q(q(q(?x_3,?y_3),e),?z),
     q(q(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?y = q(q(e,?y),e),
     q(?x_4,q(?y_4,?z)) = q(q(e,q(?x_4,?y_4)),?z),
     ?z = q(q(e,e),?z),
     q(?x_3,q(?y_3,q(?y,?z))) = q(q(q(?x_3,?y_3),?y),?z),
     q(?y,?z) = q(q(e,?y),?z),
     q(?x,q(q(?y,?y_1),?z_1)) = q(q(?x,?y),q(?y_1,?z_1)),
     q(?x,?y) = q(q(?x,?y),e),
     q(?x,q(?x_4,q(?y_4,?z))) = q(q(?x,q(?x_4,?y_4)),?z),
     q(?x,?z) = q(q(?x,e),?z),
     q(q(?x_1,?x),q(q(?y,?y_2),?z_2)) = q(?x_1,q(q(?x,?y),q(?y_2,?z_2))),
     q(q(?x_1,?x),?y) = q(?x_1,q(q(?x,?y),e)),
     q(q(?x_1,?x),q(?x_5,q(?y_5,?z))) = q(?x_1,q(q(?x,q(?x_5,?y_5)),?z)),
     q(q(?x_1,?x),?z) = q(?x_1,q(q(?x,e),?z)),
     plus(len(a),len(q(q(?y,?y_1),?z_1))) = len(q(q(a,?y),q(?y_1,?z_1))),
     plus(len(a),len(?y)) = len(q(q(a,?y),e)),
     plus(len(a),len(q(?x_4,q(?y_4,?z)))) = len(q(q(a,q(?x_4,?y_4)),?z)),
     plus(len(a),len(?z)) = len(q(q(a,e),?z)),
     q(?x,q(q(q(?y,?y_5),?z_5),?z_4)) = q(q(q(?x,?y),q(?y_5,?z_5)),?z_4),
     q(?x,q(q(?x_8,q(?y_8,?z)),?z_4)) = q(q(q(?x,q(?x_8,?y_8)),?z),?z_4),
     q(?x,q(?z,?z_4)) = q(q(q(?x,e),?z),?z_4),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     plus(len(a),len(q(?y,?z))) = len(q(q(a,?y),?z)),
     q(?x,q(q(?y,?z),?z_4)) = q(q(q(?x,?y),?z),?z_4),
     q(?x_3,q(?y_3,e)) = q(?x_3,?y_3),
     e = e,
     plus(len(a),len(e)) = len(a),
     q(q(?x_3,?x),e) = q(?x_3,?x),
     q(?x,q(e,?z_4)) = q(?x,?z_4),
     q(q(q(?x_3,q(?y_3,?y)),?y_2),?z_2) = q(q(?x_3,?y_3),q(?y,q(?y_2,?z_2))),
     q(q(q(q(?x,?y_5),?z_5),?y_2),?z_2) = q(?x,q(q(?y_5,?z_5),q(?y_2,?z_2))),
     q(q(?x,?y_2),?z_2) = q(?x,q(e,q(?y_2,?z_2))),
     q(q(?y,?y_2),?z_2) = q(e,q(?y,q(?y_2,?z_2))),
     q(?x_1,q(?y_1,?y)) = q(q(?x_1,?y_1),q(?y,e)),
     ?x = q(?x,q(e,e)),
     ?y = q(e,q(?y,e)),
     q(q(q(?x,?y),?y_2),?z_2) = q(?x,q(?y,q(?y_2,?z_2))),
     q(?x,?y) = q(?x,q(?y,e)),
     q(q(?x_1,q(?y_1,?y)),?z) = q(q(?x_1,?y_1),q(?y,?z)),
     q(q(q(?x,?y_3),?z_3),?z) = q(?x,q(q(?y_3,?z_3),?z)),
     q(?x,?z) = q(?x,q(e,?z)),
     q(?y,?z) = q(e,q(?y,?z)),
     q(q(?x_2,q(?y_2,?y)),q(?z,?z_1)) = q(q(q(?x_2,?y_2),q(?y,?z)),?z_1),
     q(q(q(?x,?y_4),?z_4),q(?z,?z_1)) = q(q(?x,q(q(?y_4,?z_4),?z)),?z_1),
     q(?x,q(?z,?z_1)) = q(q(?x,q(e,?z)),?z_1),
     q(q(?x_3,q(?x_4,q(?y_4,?y))),?z) = q(?x_3,q(q(?x_4,?y_4),q(?y,?z))),
     q(q(?x_3,q(q(?x,?y_6),?z_6)),?z) = q(?x_3,q(?x,q(q(?y_6,?z_6),?z))),
     q(q(?x_3,?x),?z) = q(?x_3,q(?x,q(e,?z))),
     q(q(?x,?y),q(?z,?z_1)) = q(q(?x,q(?y,?z)),?z_1),
     q(q(?x_3,q(?x,?y)),?z) = q(?x_3,q(?x,q(?y,?z))),
     q(q(e,?y_2),?z_2) = q(?y_2,?z_2),
     q(q(?x_3,e),?x) = q(?x_3,?x),
     q(e,q(?x,?z_5)) = q(?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 <len(q(q(a,?y_1),?z_1)), plus(len(a),len(q(?y_1,?z_1)))> by Rules <1, 0> preceded by [(len,1)]
 joinable by a reduction of rules <[([(len,1)],3),([],0)], []>
Critical Pair <len(a), plus(len(a),len(e))> by Rules <2, 0> preceded by [(len,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten q(?x_7,e) and ?x_7
strenghten q(e,?x_2) and ?x_2
strenghten q(e,e) and e
strenghten q(q(?x_7,e),e) and ?x_7
strenghten q(q(e,?x_12),e) and ?x_12
strenghten plus(len(a),len(e)) and len(a)
strenghten q(?x_2,q(e,?z_3)) and q(?x_2,?z_3)
strenghten q(?x_3,q(?y_3,e)) and q(?x_3,?y_3)
strenghten q(e,q(?x_4,?z_3)) and q(?x_4,?z_3)
strenghten q(q(?x_1,?x_2),e) and q(?x_1,?x_2)
strenghten q(q(?x_1,e),?x_4) and q(?x_1,?x_4)
strenghten q(q(e,?y_1),?z_1) and q(?y_1,?z_1)
strenghten plus(len(a),len(q(e,e))) and len(a)
strenghten q(?x_3,q(?y_3,q(e,e))) and q(?x_3,?y_3)
strenghten q(?x_7,q(q(e,e),?z_3)) and q(?x_7,?z_3)
strenghten q(e,q(?x_3,q(?y_3,e))) and q(?x_3,?y_3)
strenghten q(e,q(q(?x_12,e),?z_3)) and q(?x_12,?z_3)
strenghten q(q(?x_1,?x_7),q(e,e)) and q(?x_1,?x_7)
strenghten q(q(?x_1,e),q(?x_12,e)) and q(?x_1,?x_12)
strenghten plus(len(a),len(q(?y_1,?z_1))) and len(q(q(a,?y_1),?z_1))
strenghten q(?x_1,q(q(?y_1,?z_1),?z_3)) and q(q(q(?x_1,?y_1),?z_1),?z_3)
strenghten q(q(?x,?y),q(?z,?z_1)) and q(q(?x,q(?y,?z)),?z_1)
strenghten q(q(?x_1,?x),q(?y,?z)) and q(?x_1,q(q(?x,?y),?z))
strenghten q(q(?x_1,q(?x_3,?y_3)),?z_3) and q(?x_1,q(?x_3,q(?y_3,?z_3)))
strenghten q(q(q(?x_3,?y_3),?y_1),?z_1) and q(?x_3,q(?y_3,q(?y_1,?z_1)))
obtain 62 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <plus(len(a),len(e)), len(a)>
Direct Methods: not CR
{8}
(cm)Rewrite Rules:
   [ len(e) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{9}
(cm)Rewrite Rules:
   [ len(a) -> s(0) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
R11.trs: Failure(unknown)
(40485 msec.)