MAYBE
(ignored inputs)COMMENT Queue.
Rewrite Rules:
   [ q(e,?x) -> ?x,
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ q(?x,?z_1) = q(e,q(?x,?z_1)),
     q(q(q(?x_2,?y_2),?z_2),?z_1) = q(?x_2,q(q(?y_2,?z_2),?z_1)),
     q(?x_2,?x) = q(q(?x_2,e),?x),
     q(?x_2,q(?x_1,q(?y_1,?z_1))) = q(q(?x_2,q(?x_1,?y_1)),?z_1),
     eq(e,q(q(a,?y_2),?z_2)) = false,
     eq(q(q(a,?y_2),?z_2),q(a,?y_4)) = eq(q(?y_2,?z_2),?y_4),
     eq(q(a,?x_4),q(q(a,?y_2),?z_2)) = eq(?x_4,q(?y_2,?z_2)),
     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(?y_2,?z_2) = q(q(e,?y_2),?z_2),
     q(?x_1,q(?y_1,q(?y_2,?z_2))) = q(q(q(?x_1,?y_1),?y_2),?z_2),
     false = eq(q(a,?x_3),e),
     eq(?x_4,?y_4) = eq(q(a,?y_4),q(a,?x_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
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ q(q(e,?y_2),?z_2) = q(?y_2,?z_2),
     q(e,q(?x,?z_2)) = q(?x,?z_2),
     q(q(?x_3,e),?x) = q(?x_3,?x),
     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(?y,?y_2),?z_2) = q(e,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(q(?x,?y),?y_2),?z_2) = q(?x,q(?y,q(?y_2,?z_2))),
     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(q(q(?x,?y_3),?z_3),?z) = q(?x,q(q(?y_3,?z_3),?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(q(q(?x,?y_4),?z_4),q(?z,?z_1)) = q(q(?x,q(q(?y_4,?z_4),?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,?y),?z) = q(?x_3,q(e,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,?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(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?z = q(q(e,e),?z),
     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,?z)) = q(q(q(?x_2,?y_2),e),?z),
     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(?y,?z) = q(q(e,?y),?z),
     q(?x_2,q(?y_2,q(?y,?z))) = q(q(q(?x_2,?y_2),?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,q(?x_3,q(?y_3,?z))) = q(q(?x,q(?x_3,?y_3)),?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_4,q(?y_4,?z))) = q(?x_1,q(q(?x,q(?x_4,?y_4)),?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(?z,?z_3)) = q(q(q(?x,e),?z),?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),
     false = eq(e,q(q(a,?y),q(?y_1,?z_1))),
     false = eq(e,q(q(a,e),?z)),
     false = eq(e,q(q(a,q(?x_3,?y_3)),?z)),
     eq(q(q(?y,?y_6),?z_6),?y_5) = eq(q(q(a,?y),q(?y_6,?z_6)),q(a,?y_5)),
     eq(?z,?y_5) = eq(q(q(a,e),?z),q(a,?y_5)),
     eq(q(?x_8,q(?y_8,?z)),?y_5) = eq(q(q(a,q(?x_8,?y_8)),?z),q(a,?y_5)),
     eq(?x_5,q(q(?y,?y_6),?z_6)) = eq(q(a,?x_5),q(q(a,?y),q(?y_6,?z_6))),
     eq(?x_5,?z) = eq(q(a,?x_5),q(q(a,e),?z)),
     eq(?x_5,q(?x_8,q(?y_8,?z))) = eq(q(a,?x_5),q(q(a,q(?x_8,?y_8)),?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),
     false = eq(e,q(q(a,?y),?z)),
     eq(q(?y,?z),?y_5) = eq(q(q(a,?y),?z),q(a,?y_5)),
     eq(?x_5,q(?y,?z)) = eq(q(a,?x_5),q(q(a,?y),?z)),
     eq(q(q(a,?y_4),?z_4),e) = false,
     eq(q(a,?x),e) = false,
     eq(e,q(q(a,?y_4),?z_4)) = false,
     eq(q(q(a,?y_8),?z_8),q(q(a,?y_4),?z_4)) = eq(q(?y_4,?z_4),q(?y_8,?z_8)),
     eq(q(a,?y),q(q(a,?y_4),?z_4)) = eq(q(?y_4,?z_4),?y),
     eq(q(q(a,?y_4),?z_4),q(a,?x)) = eq(?x,q(?y_4,?z_4)),
     eq(q(q(a,?y_4),?z_4),q(q(a,?y_8),?z_8)) = eq(q(?y_4,?z_4),q(?y_8,?z_8)),
     eq(q(a,?y),q(a,?x)) = eq(?x,?y),
     eq(q(q(a,?y_4),?z_4),q(a,?y)) = eq(q(?y_4,?z_4),?y),
     eq(q(a,?x),q(q(a,?y_4),?z_4)) = eq(?x,q(?y_4,?z_4)),
     false = eq(q(a,?x_4),e),
     eq(?x_5,?y_5) = eq(q(a,?y_5),q(a,?x_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(e,q(?x,?z_1))> by Rules <0, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <q(q(q(?x_2,?y_2),?z_2),?z_1), q(?x_2,q(q(?y_2,?z_2),?z_1))> by Rules <2, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],1)], [([],2)]>
Critical Pair <q(?x_2,?x), q(q(?x_2,e),?x)> by Rules <0, 2> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([],1),([(q,2)],0)]>
Critical Pair <q(?x_2,q(?x_1,q(?y_1,?z_1))), q(q(?x_2,q(?x_1,?y_1)),?z_1)> by Rules <1, 2> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],2)], [([],1)]>
Critical Pair <eq(e,q(q(a,?y_2),?z_2)), false> by Rules <2, 3> preceded by [(eq,2)]
 joinable by a reduction of rules <[([(eq,2)],1),([],3)], []>
Critical Pair <eq(q(q(a,?y_2),?z_2),q(a,?y_4)), eq(q(?y_2,?z_2),?y_4)> by Rules <2, 4> preceded by [(eq,1)]
 joinable by a reduction of rules <[([(eq,1)],1),([],4)], []>
Critical Pair <eq(q(a,?x_4),q(q(a,?y_2),?z_2)), eq(?x_4,q(?y_2,?z_2))> by Rules <2, 4> preceded by [(eq,2)]
 joinable by a reduction of rules <[([(eq,2)],1),([],4)], []>
Critical Pair <q(q(?x,q(?y,?z)),?z_1), q(q(?x,?y),q(?z,?z_1))> by Rules <1, 1> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],2)], [([],2)]>
Critical Pair <q(?x_1,q(q(?x,?y),?z)), q(q(?x_1,?x),q(?y,?z))> by Rules <2, 2> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],1)], [([],1)]>
Critical Pair <q(q(e,?y_2),?z_2), q(?y_2,?z_2)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([(q,1)],0)], []>
Critical Pair <q(q(q(?x_1,?y_1),?y_2),?z_2), q(?x_1,q(?y_1,q(?y_2,?z_2)))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],1)], [([],2)]>
Critical Pair <eq(q(a,?x_3),e), false> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([],5),([],3)], []>
Critical Pair <eq(q(a,?y_4),q(a,?x_4)), eq(?x_4,?y_4)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],4)], [([],5)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten q(e,?x) and ?x
strenghten eq(?x_8,?y_8) and eq(?y_8,?x_8)
strenghten q(q(e,e),?x_11) and ?x_11
strenghten eq(e,q(a,?x_3)) and false
strenghten eq(q(a,?x_3),e) and false
strenghten q(e,q(?x,?z_1)) and q(?x,?z_1)
strenghten q(q(?x_2,e),?x) and q(?x_2,?x)
strenghten q(q(e,?y_2),?z_2) and q(?y_2,?z_2)
strenghten eq(e,q(q(a,?y_2),?z_2)) and false
strenghten q(e,q(q(e,?x_11),?z_1)) and q(?x_11,?z_1)
strenghten q(q(?x_2,e),q(e,?x_11)) and q(?x_2,?x_11)
strenghten eq(q(a,?x_4),q(a,?y_4)) and eq(?x_4,?y_4)
strenghten eq(q(a,?y_4),q(a,?x_4)) and eq(?x_4,?y_4)
strenghten q(?x_1,q(?y_1,q(?y_2,?z_2))) and q(q(q(?x_1,?y_1),?y_2),?z_2)
strenghten q(?x_2,q(q(?y_2,?z_2),?z_1)) and q(q(q(?x_2,?y_2),?z_2),?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_2,q(?x_1,?y_1)),?z_1) and q(?x_2,q(?x_1,q(?y_1,?z_1)))
strenghten eq(q(a,?x_4),q(q(a,?y_2),?z_2)) and eq(?x_4,q(?y_2,?z_2))
strenghten eq(q(q(a,?y_2),?z_2),q(a,?y_4)) and eq(q(?y_2,?z_2),?y_4)
obtain 56 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,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z) ]
   [ eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  eq:= (9)+(8)*x1+(8)*x2
  false:= 0
retract eq(e,q(a,?x)) -> false
Polynomial Interpretation:
  a:= 0
  e:= (12)
  q:= (1)*x1+(1)*x2
  eq:= (8)+(8)*x1+(8)*x2
  false:= 0
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
Polynomial Interpretation:
  a:= (4)
  e:= (8)
  q:= (1)*x1+(1)*x2
  eq:= (2)+(1)*x1+(1)*x2
  false:= 0
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
retract eq(q(a,?x),q(a,?y)) -> eq(?x,?y)
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
retract eq(q(a,?x),q(a,?y)) -> eq(?x,?y)
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(e,q(q(a,?y_1),?z_1)), false> --> <eq(e,q(q(a,?y_1),?z_1)), false> => no
<eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> --> <eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> => no
<eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> --> <eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> => no
<eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> --> <eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> => 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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, eq(q(a,?x),e)> => no
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
check joinability condition:
check modulo reachablity from false to eq(e,q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from eq(?x,q(?y_1,?z_1)) to eq(q(a,?x),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),?y) to eq(q(q(?x_3,?y_3),?z_3),q(a,?y)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),q(?y_1,?z_1)) to eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
check modulo reachablity from false to eq(q(a,?x),e): maybe not reachable
failed
failure(Step 1)
   [ eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
Added S-Rules:
   [ eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(e,q(q(a,?y),?z)), false> --> <eq(e,q(q(a,?y),?z)), false> => no
<eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> --> <eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> => no
<eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,q(?y,?z))> --> <eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, eq(q(a,?x),e)> => no
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
check joinability condition:
check modulo reachablity from false to eq(e,q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from eq(q(?y,?z),?y_1) to eq(q(q(a,?y),?z),q(a,?y_1)): maybe not reachable
check modulo reachablity from eq(?x_1,q(?y,?z)) to eq(q(a,?x_1),q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
check modulo reachablity from false to eq(q(a,?x),e): maybe not reachable
failed
failure(Step 2)
   [ eq(e,q(q(a,?y),?z)) -> false,
     eq(q(a,?x),e) -> false ]
Added S-Rules:
   [ eq(e,q(q(a,?y),?z)) -> false,
     eq(q(a,?x),e) -> false ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y) ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y) ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  eq:= (4)+(4)*x1+(4)*x1*x1+(4)*x2+(4)*x2*x2
  false:= 0
retract eq(e,q(a,?x)) -> false
Polynomial Interpretation:
  a:= 0
  e:= (8)
  q:= (1)*x1+(1)*x2
  eq:= (1)+(13)*x1+(14)*x1*x1+(13)*x2+(14)*x2*x2
  false:= 0
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
Polynomial Interpretation:
  a:= 0
  e:= 0
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  eq:= (5)+(4)*x1+(6)*x1*x1+(1)*x1*x2+(4)*x2+(6)*x2*x2
  false:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(e,q(q(a,?y_1),?z_1)), false> --> <false, false> => yes
<eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> --> <eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> => no
<eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> --> <eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> => no
<eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> --> <eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> => no
<eq(e,q(q(q(?x_4,?y_4),?z_4),?z)), false> --> <eq(e,q(q(q(?x_4,?y_4),?z_4),?z)), false> => no
<eq(e,q(a,q(?y_2,?z_2))), false> --> <false, false> => yes
<eq(e,q(q(q(a,?y),?y_1),?z_1)), false> --> <eq(e,q(q(q(a,?y),?y_1),?z_1)), false> => no
<eq(q(q(a,?y_1),?z_1),e), false> --> <eq(q(q(a,?y_1),?z_1),e), false> => 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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, false> => yes
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
<false, eq(q(q(a,?y),?z),e)> --> <false, eq(q(q(a,?y),?z),e)> => no
<false, eq(e,q(a,?x))> --> <false, false> => yes
check joinability condition:
check modulo reachablity from eq(?x,q(?y_1,?z_1)) to eq(q(a,?x),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),?y) to eq(q(q(?x_3,?y_3),?z_3),q(a,?y)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),q(?y_1,?z_1)) to eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(?x_4,?y_4),?z_4),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y),?y_1),?z_1)): maybe not reachable
check modulo reachablity from false to eq(q(q(a,?y_1),?z_1),e): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
check modulo reachablity from false to eq(q(q(a,?y),?z),e): maybe not reachable
failed
failure(Step 4)
   [ eq(q(q(a,?y_1),?z_1),e) -> false ]
Added S-Rules:
   [ eq(q(q(a,?y_1),?z_1),e) -> false ]
Added P-Rules:
   [ ]
STEP: 5 (linear)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(e,q(q(a,?y),?z)), false> --> <false, false> => yes
<eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> --> <eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> => no
<eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,q(?y,?z))> --> <eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,q(?y,?z))> => no
<eq(e,q(q(q(a,?y_2),?y),?z)), false> --> <eq(e,q(q(q(a,?y_2),?y),?z)), false> => no
<eq(e,q(q(q(a,?y),?z),?z_2)), false> --> <eq(e,q(q(q(a,?y),?z),?z_2)), false> => no
<eq(q(q(a,?y),?z),e), false> --> <eq(q(q(a,?y),?z),e), false> => no
<eq(e,q(a,q(?y,?z))), false> --> <false, false> => yes
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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, false> => yes
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
<false, eq(q(q(a,?y),?z),e)> --> <false, eq(q(q(a,?y),?z),e)> => no
<false, eq(e,q(a,?x))> --> <false, false> => yes
check joinability condition:
check modulo reachablity from eq(q(?y,?z),?y_1) to eq(q(q(a,?y),?z),q(a,?y_1)): maybe not reachable
check modulo reachablity from eq(?x_1,q(?y,?z)) to eq(q(a,?x_1),q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y_2),?y),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y),?z),?z_2)): maybe not reachable
check modulo reachablity from false to eq(q(q(a,?y),?z),e): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
check modulo reachablity from false to eq(q(q(a,?y),?z),e): maybe not reachable
failed
failure(Step 5)
   [ eq(q(q(a,?y),?z),e) -> false ]
Added S-Rules:
   [ eq(q(q(a,?y),?z),e) -> false ]
Added P-Rules:
   [ ]
STEP: 6 (relative)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  a:= 0
  e:= (2)
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  eq:= (8)+(4)*x1+(2)*x1*x1+(4)*x2+(2)*x2*x2
  false:= 0
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
retract eq(e,q(q(a,?y_1),?z_1)) -> false
retract eq(q(a,?x),e) -> false
Polynomial Interpretation:
  a:= (1)
  e:= 0
  q:= (1)*x1+(1)*x2
  eq:= (8)+(4)*x1+(2)*x1*x2+(4)*x2
  false:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false,
     eq(q(q(a,?y_1),?z_1),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(e,q(q(a,?y_1),?z_1)), false> --> <false, false> => yes
<eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> --> <eq(q(a,?x),q(q(a,?y_1),?z_1)), eq(?x,q(?y_1,?z_1))> => no
<eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> --> <eq(q(q(?x_3,?y_3),?z_3),q(a,?y)), eq(q(?y_3,?z_3),?y)> => no
<eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> --> <eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)), eq(q(?y_3,?z_3),q(?y_1,?z_1))> => no
<eq(e,q(q(q(?x_4,?y_4),?z_4),?z)), false> --> <eq(e,q(q(q(?x_4,?y_4),?z_4),?z)), false> => no
<eq(e,q(a,q(?y_2,?z_2))), false> --> <false, false> => yes
<eq(e,q(q(q(a,?y),?y_1),?z_1)), false> --> <eq(e,q(q(q(a,?y),?y_1),?z_1)), false> => no
<eq(q(q(a,?y_1),?z_1),e), false> --> <false, false> => yes
<eq(q(q(q(?x_4,?y_4),?z_4),?z),e), false> --> <eq(q(q(q(?x_4,?y_4),?z_4),?z),e), false> => no
<eq(q(a,q(?y_2,?z_2)),e), false> --> <false, false> => yes
<eq(q(q(q(a,?y),?y_1),?z_1),e), false> --> <eq(q(q(q(a,?y),?y_1),?z_1),e), false> => 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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, false> => yes
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
<false, eq(q(q(a,?y),?z),e)> --> <false, false> => yes
<false, eq(e,q(a,?x))> --> <false, false> => yes
<false, eq(e,q(q(a,?y),?z))> --> <false, false> => yes
check joinability condition:
check modulo reachablity from eq(?x,q(?y_1,?z_1)) to eq(q(a,?x),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),?y) to eq(q(q(?x_3,?y_3),?z_3),q(a,?y)): maybe not reachable
check modulo reachablity from eq(q(?y_3,?z_3),q(?y_1,?z_1)) to eq(q(q(?x_3,?y_3),?z_3),q(q(a,?y_1),?z_1)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(?x_4,?y_4),?z_4),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y),?y_1),?z_1)): maybe not reachable
check modulo reachablity from false to eq(q(q(q(?x_4,?y_4),?z_4),?z),e): maybe not reachable
check modulo reachablity from false to eq(q(q(q(a,?y),?y_1),?z_1),e): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
failed
failure(Step 7)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 8 (linear)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false,
     eq(q(q(a,?y_1),?z_1),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(e,q(q(a,?y),?z)), false> --> <false, false> => yes
<eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> --> <eq(q(q(a,?y),?z),q(a,?y_1)), eq(q(?y,?z),?y_1)> => no
<eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,q(?y,?z))> --> <eq(q(a,?x_1),q(q(a,?y),?z)), eq(?x_1,q(?y,?z))> => no
<eq(e,q(q(q(a,?y_2),?y),?z)), false> --> <eq(e,q(q(q(a,?y_2),?y),?z)), false> => no
<eq(e,q(q(q(a,?y),?z),?z_2)), false> --> <eq(e,q(q(q(a,?y),?z),?z_2)), false> => no
<eq(q(q(a,?y),?z),e), false> --> <false, false> => yes
<eq(q(q(q(a,?y_2),?y),?z),e), false> --> <eq(q(q(q(a,?y_2),?y),?z),e), false> => no
<eq(q(q(q(a,?y),?z),?z_2),e), false> --> <eq(q(q(q(a,?y),?z),?z_2),e), false> => no
<eq(e,q(a,q(?y,?z))), false> --> <false, false> => yes
<eq(q(a,q(?y,?z)),e), false> --> <false, false> => yes
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(q(?x_1,e),?x)> => no
<q(?x,?z_1), q(e,q(?x,?z_1))> --> <q(?x,?z_1), q(?x,?z_1)> => yes
<false, eq(q(a,?x),e)> --> <false, false> => yes
<eq(?x,?y), eq(q(a,?y),q(a,?x))> --> <eq(?x,?y), eq(?y,?x)> => yes
<false, eq(q(q(a,?y),?z),e)> --> <false, false> => yes
<false, eq(e,q(a,?x))> --> <false, false> => yes
<false, eq(e,q(q(a,?y),?z))> --> <false, false> => yes
check joinability condition:
check modulo reachablity from eq(q(?y,?z),?y_1) to eq(q(q(a,?y),?z),q(a,?y_1)): maybe not reachable
check modulo reachablity from eq(?x_1,q(?y,?z)) to eq(q(a,?x_1),q(q(a,?y),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y_2),?y),?z)): maybe not reachable
check modulo reachablity from false to eq(e,q(q(q(a,?y),?z),?z_2)): maybe not reachable
check modulo reachablity from false to eq(q(q(q(a,?y_2),?y),?z),e): maybe not reachable
check modulo reachablity from false to eq(q(q(q(a,?y),?z),?z_2),e): maybe not reachable
check modulo reachablity from q(?x_1,?x) to q(q(?x_1,e),?x): maybe not reachable
failed
failure(Step 8)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 9 (relative)
S:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false,
     eq(q(q(a,?y_1),?z_1),e) -> false ]
P:
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ q(e,?x) -> ?x,
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(q(a,?y_1),?z_1)) -> false,
     eq(q(a,?x),e) -> false,
     eq(q(q(a,?y_1),?z_1),e) -> false ]
   [ q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  a:= 0
  e:= 0
  q:= (1)*x1+(1)*x2
  eq:= (8)+(8)*x1*x1+(8)*x2*x2
  false:= 0
retract eq(e,q(a,?x)) -> false
retract eq(e,q(q(a,?y_1),?z_1)) -> false
retract eq(q(a,?x),e) -> false
retract eq(q(q(a,?y_1),?z_1),e) -> false
Polynomial Interpretation:
  a:= 0
  e:= (6)
  q:= (1)*x1+(2)*x1*x2+(1)*x2
  eq:= (5)+(1)*x1+(1)*x2
  false:= (4)
retract q(e,?x) -> ?x
retract eq(e,q(a,?x)) -> false
retract eq(e,q(q(a,?y_1),?z_1)) -> false
retract eq(q(a,?x),e) -> false
retract eq(q(q(a,?y_1),?z_1),e) -> false
Polynomial Interpretation:
  a:= 0
  e:= (6)
  q:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  eq:= (14)+(6)*x1*x1+(11)*x1*x2+(6)*x2*x2
  false:= (4)
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ q(e,?x) -> ?x,
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x) ]
Sort Assignment:
 a : =>19
 e : =>19
 q : 19*19=>19
 eq : 19*19=>22
 false : =>22
maximal types: {19,22}
Persistent Decomposition failed: Can't judge

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

Try Commutative Decomposition for...
   [ q(e,?x) -> ?x,
     q(q(?x,?y),?z) -> q(?x,q(?y,?z)),
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z),
     eq(e,q(a,?x)) -> false,
     eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x) ]
Outside Critical Pair: <q(q(e,?y_2),?z_2), q(?y_2,?z_2)> by Rules <2, 0>
develop reducts from lhs term...
<{1}, q(e,q(?y_2,?z_2))>
<{0}, q(?y_2,?z_2)>
<{}, q(q(e,?y_2),?z_2)>
develop reducts from rhs term...
<{}, q(?y_2,?z_2)>
Outside Critical Pair: <q(q(q(?x_1,?y_1),?y_2),?z_2), q(?x_1,q(?y_1,q(?y_2,?z_2)))> by Rules <2, 1>
develop reducts from lhs term...
<{1}, q(q(?x_1,?y_1),q(?y_2,?z_2))>
<{1}, q(q(?x_1,q(?y_1,?y_2)),?z_2)>
<{}, q(q(q(?x_1,?y_1),?y_2),?z_2)>
develop reducts from rhs term...
<{2}, q(q(?x_1,?y_1),q(?y_2,?z_2))>
<{2}, q(?x_1,q(q(?y_1,?y_2),?z_2))>
<{}, q(?x_1,q(?y_1,q(?y_2,?z_2)))>
Outside Critical Pair: <eq(q(a,?x_3),e), false> by Rules <5, 3>
develop reducts from lhs term...
<{5}, eq(e,q(a,?x_3))>
<{}, eq(q(a,?x_3),e)>
develop reducts from rhs term...
<{}, false>
Outside Critical Pair: <eq(q(a,?y_4),q(a,?x_4)), eq(?x_4,?y_4)> by Rules <5, 4>
develop reducts from lhs term...
<{5}, eq(q(a,?x_4),q(a,?y_4))>
<{4}, eq(?y_4,?x_4)>
<{}, eq(q(a,?y_4),q(a,?x_4))>
develop reducts from rhs term...
<{5}, eq(?y_4,?x_4)>
<{}, eq(?x_4,?y_4)>
Inside Critical Pair: <q(?x,?z_1), q(e,q(?x,?z_1))> by Rules <0, 1>
develop reducts from lhs term...
<{}, q(?x,?z_1)>
develop reducts from rhs term...
<{2}, q(q(e,?x),?z_1)>
<{0}, q(?x,?z_1)>
<{}, q(e,q(?x,?z_1))>
Inside Critical Pair: <q(q(q(?x_2,?y_2),?z_2),?z_1), q(?x_2,q(q(?y_2,?z_2),?z_1))> by Rules <2, 1>
develop reducts from lhs term...
<{1}, q(q(?x_2,?y_2),q(?z_2,?z_1))>
<{1}, q(q(?x_2,q(?y_2,?z_2)),?z_1)>
<{}, q(q(q(?x_2,?y_2),?z_2),?z_1)>
develop reducts from rhs term...
<{2}, q(q(?x_2,q(?y_2,?z_2)),?z_1)>
<{1}, q(?x_2,q(?y_2,q(?z_2,?z_1)))>
<{}, q(?x_2,q(q(?y_2,?z_2),?z_1))>
Inside Critical Pair: <q(?x_2,?x), q(q(?x_2,e),?x)> by Rules <0, 2>
develop reducts from lhs term...
<{}, q(?x_2,?x)>
develop reducts from rhs term...
<{1}, q(?x_2,q(e,?x))>
<{}, q(q(?x_2,e),?x)>
Inside Critical Pair: <q(?x_2,q(?x_1,q(?y_1,?z_1))), q(q(?x_2,q(?x_1,?y_1)),?z_1)> by Rules <1, 2>
develop reducts from lhs term...
<{2}, q(q(?x_2,?x_1),q(?y_1,?z_1))>
<{2}, q(?x_2,q(q(?x_1,?y_1),?z_1))>
<{}, q(?x_2,q(?x_1,q(?y_1,?z_1)))>
develop reducts from rhs term...
<{1}, q(?x_2,q(q(?x_1,?y_1),?z_1))>
<{2}, q(q(q(?x_2,?x_1),?y_1),?z_1)>
<{}, q(q(?x_2,q(?x_1,?y_1)),?z_1)>
Inside Critical Pair: <eq(e,q(q(a,?y_2),?z_2)), false> by Rules <2, 3>
develop reducts from lhs term...
<{1,5}, eq(q(a,q(?y_2,?z_2)),e)>
<{5}, eq(q(q(a,?y_2),?z_2),e)>
<{1}, eq(e,q(a,q(?y_2,?z_2)))>
<{}, eq(e,q(q(a,?y_2),?z_2))>
develop reducts from rhs term...
<{}, false>
Inside Critical Pair: <eq(q(q(a,?y_2),?z_2),q(a,?y_4)), eq(q(?y_2,?z_2),?y_4)> by Rules <2, 4>
develop reducts from lhs term...
<{1,5}, eq(q(a,?y_4),q(a,q(?y_2,?z_2)))>
<{5}, eq(q(a,?y_4),q(q(a,?y_2),?z_2))>
<{1}, eq(q(a,q(?y_2,?z_2)),q(a,?y_4))>
<{}, eq(q(q(a,?y_2),?z_2),q(a,?y_4))>
develop reducts from rhs term...
<{5}, eq(?y_4,q(?y_2,?z_2))>
<{}, eq(q(?y_2,?z_2),?y_4)>
Inside Critical Pair: <eq(q(a,?x_4),q(q(a,?y_2),?z_2)), eq(?x_4,q(?y_2,?z_2))> by Rules <2, 4>
develop reducts from lhs term...
<{1,5}, eq(q(a,q(?y_2,?z_2)),q(a,?x_4))>
<{5}, eq(q(q(a,?y_2),?z_2),q(a,?x_4))>
<{1}, eq(q(a,?x_4),q(a,q(?y_2,?z_2)))>
<{}, eq(q(a,?x_4),q(q(a,?y_2),?z_2))>
develop reducts from rhs term...
<{5}, eq(q(?y_2,?z_2),?x_4)>
<{}, eq(?x_4,q(?y_2,?z_2))>
Try A Minimal Decomposition {4,3,5,0,2}{1}
{4,3,5,0,2}
(cm)Rewrite Rules:
   [ eq(q(a,?x),q(a,?y)) -> eq(?x,?y),
     eq(e,q(a,?x)) -> false,
     eq(?x,?y) -> eq(?y,?x),
     q(e,?x) -> ?x,
     q(?x,q(?y,?z)) -> q(q(?x,?y),?z) ]
Apply Direct Methods...
Inner CPs:
   [ eq(q(q(a,?y_4),?z_4),q(a,?y)) = eq(q(?y_4,?z_4),?y),
     eq(q(a,?x),q(q(a,?y_4),?z_4)) = eq(?x,q(?y_4,?z_4)),
     eq(e,q(q(a,?y_4),?z_4)) = false,
     q(?x_4,?x_3) = q(q(?x_4,e),?x_3),
     q(?x_1,q(q(?x,?y),?z)) = q(q(?x_1,?x),q(?y,?z)) ]
Outer CPs:
   [ eq(?x,?y) = eq(q(a,?y),q(a,?x)),
     false = eq(q(a,?x_1),e),
     q(?y_4,?z_4) = q(q(e,?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
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ eq(q(q(a,?y_10),?z_10),q(q(a,?y_5),?z_5)) = eq(q(?y_5,?z_5),q(?y_10,?z_10)),
     eq(q(a,?y),q(q(a,?y_5),?z_5)) = eq(q(?y_5,?z_5),?y),
     eq(q(q(a,?y_5),?z_5),q(a,?x)) = eq(?x,q(?y_5,?z_5)),
     eq(q(q(a,?y_5),?z_5),q(q(a,?y_10),?z_10)) = eq(q(?y_5,?z_5),q(?y_10,?z_10)),
     eq(q(a,?y),q(a,?x)) = eq(?x,?y),
     eq(q(q(a,?y_5),?z_5),q(a,?y)) = eq(q(?y_5,?z_5),?y),
     eq(q(a,?x),q(q(a,?y_5),?z_5)) = eq(?x,q(?y_5,?z_5)),
     eq(q(q(a,?y_5),?z_5),e) = false,
     eq(q(a,?x),e) = false,
     eq(e,q(q(a,?y_5),?z_5)) = false,
     eq(?x_1,?y_1) = eq(q(a,?y_1),q(a,?x_1)),
     false = eq(q(a,?x_2),e),
     q(q(e,?y_4),?z_4) = q(?y_4,?z_4),
     q(q(?x_5,e),?x) = q(?x_5,?x),
     q(q(?y,?y_1),?z_1) = q(q(e,?y),q(?y_1,?z_1)),
     ?z = q(q(e,e),?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,?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),?z) = q(?x_1,q(q(?x,e),?z)),
     eq(q(q(?y,?y_3),?z_3),?y_2) = eq(q(q(a,?y),q(?y_3,?z_3)),q(a,?y_2)),
     eq(?z,?y_2) = eq(q(q(a,e),?z),q(a,?y_2)),
     eq(?x_2,q(q(?y,?y_3),?z_3)) = eq(q(a,?x_2),q(q(a,?y),q(?y_3,?z_3))),
     eq(?x_2,?z) = eq(q(a,?x_2),q(q(a,e),?z)),
     false = eq(e,q(q(a,?y),q(?y_1,?z_1))),
     false = eq(e,q(q(a,e),?z)),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     eq(q(?y,?z),?y_2) = eq(q(q(a,?y),?z),q(a,?y_2)),
     eq(?x_2,q(?y,?z)) = eq(q(a,?x_2),q(q(a,?y),?z)),
     false = eq(e,q(q(a,?y),?z)) ]
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 <eq(q(q(a,?y_4),?z_4),q(a,?y)), eq(q(?y_4,?z_4),?y)> by Rules <4, 0> preceded by [(eq,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten q(e,?x_3) and ?x_3
strenghten eq(?x_7,?y_7) and eq(?y_7,?x_7)
strenghten q(q(e,e),?x_10) and ?x_10
strenghten eq(e,q(a,?x_1)) and false
strenghten eq(q(a,?x_1),e) and false
strenghten q(q(?x_4,e),?x_3) and q(?x_4,?x_3)
strenghten q(q(e,?y_4),?z_4) and q(?y_4,?z_4)
strenghten eq(e,q(q(a,?y_4),?z_4)) and false
strenghten q(e,q(q(e,?y_4),?z_4)) and q(?y_4,?z_4)
strenghten q(q(?x_4,e),q(e,?x_10)) and q(?x_4,?x_10)
strenghten eq(q(a,?x),q(a,?y)) and eq(?x,?y)
strenghten eq(q(a,?y),q(a,?x)) and eq(?x,?y)
strenghten q(q(?x_1,?x),q(?y,?z)) and q(?x_1,q(q(?x,?y),?z))
strenghten eq(q(a,?x),q(q(a,?y_4),?z_4)) and eq(?x,q(?y_4,?z_4))
strenghten eq(q(q(a,?y_4),?z_4),q(a,?y)) and eq(q(?y_4,?z_4),?y)
obtain 26 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <q(q(c_1,e),c_2), q(c_1,c_2)>
Direct Methods: not CR
{1}
(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
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
R10.trs: Failure(unknown)
(18171 msec.)