NO
(ignored inputs)COMMENT Queue. not confluent
Rewrite Rules:
   [ q(e,?x) -> ?x,
     q(?x,e) -> ?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_2) = q(e,q(?x,?z_2)),
     q(?x_1,?z_2) = q(?x_1,q(e,?z_2)),
     q(q(q(?x_3,?y_3),?z_3),?z_2) = q(?x_3,q(q(?y_3,?z_3),?z_2)),
     q(?x_3,?x) = q(q(?x_3,e),?x),
     q(?x_3,?x_1) = q(q(?x_3,?x_1),e),
     q(?x_3,q(?x_2,q(?y_2,?z_2))) = q(q(?x_3,q(?x_2,?y_2)),?z_2),
     eq(e,a) = false,
     eq(e,q(q(a,?y_3),?z_3)) = false,
     eq(a,q(a,?y_5)) = eq(e,?y_5),
     eq(q(a,?x_5),a) = eq(?x_5,e),
     eq(q(q(a,?y_3),?z_3),q(a,?y_5)) = eq(q(?y_3,?z_3),?y_5),
     eq(q(a,?x_5),q(q(a,?y_3),?z_3)) = eq(?x_5,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:
   [ e = e,
     q(?y_3,?z_3) = q(q(e,?y_3),?z_3),
     q(?x_2,?y_2) = q(?x_2,q(?y_2,e)),
     q(?x_2,q(?y_2,q(?y_3,?z_3))) = q(q(q(?x_2,?y_2),?y_3),?z_3),
     false = eq(q(a,?x_4),e),
     eq(?x_5,?y_5) = eq(q(a,?y_5),q(a,?x_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:
   [ e = e,
     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,e)) = q(?x_2,?y_2),
     q(?x,q(e,?z_3)) = q(?x,?z_3),
     q(q(?x_4,?x),e) = q(?x_4,?x),
     false = eq(e,a),
     eq(e,?y_6) = eq(a,q(a,?y_6)),
     eq(?x_6,e) = eq(q(a,?x_6),a),
     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_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(?y,?y_3),?z_3) = q(e,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(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(?y,?z) = q(e,q(?y,?z)),
     q(?x,?z) = q(?x,q(e,?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(?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_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(?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_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,?z)) = q(q(q(?x_3,?y_3),e),?z),
     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(?y,?z) = q(q(e,?y),?z),
     q(?x_3,q(?y_3,q(?y,?z))) = q(q(q(?x_3,?y_3),?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_4,q(?y_4,?z))) = q(q(?x,q(?x_4,?y_4)),?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_5,q(?y_5,?z))) = q(?x_1,q(q(?x,q(?x_5,?y_5)),?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(?z,?z_4)) = q(q(q(?x,e),?z),?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),
     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,?y),e)),
     false = eq(e,q(q(a,q(?x_4,?y_4)),?z)),
     eq(q(q(?y,?y_7),?z_7),?y_6) = eq(q(q(a,?y),q(?y_7,?z_7)),q(a,?y_6)),
     eq(?z,?y_6) = eq(q(q(a,e),?z),q(a,?y_6)),
     eq(?y,?y_6) = eq(q(q(a,?y),e),q(a,?y_6)),
     eq(q(?x_10,q(?y_10,?z)),?y_6) = eq(q(q(a,q(?x_10,?y_10)),?z),q(a,?y_6)),
     eq(?x_6,q(q(?y,?y_7),?z_7)) = eq(q(a,?x_6),q(q(a,?y),q(?y_7,?z_7))),
     eq(?x_6,?z) = eq(q(a,?x_6),q(q(a,e),?z)),
     eq(?x_6,?y) = eq(q(a,?x_6),q(q(a,?y),e)),
     eq(?x_6,q(?x_10,q(?y_10,?z))) = eq(q(a,?x_6),q(q(a,q(?x_10,?y_10)),?z)),
     q(q(?x_1,?x),q(?y,?z)) = q(?x_1,q(q(?x,?y),?z)),
     q(?x,q(q(?y,?z),?z_4)) = q(q(q(?x,?y),?z),?z_4),
     false = eq(e,q(q(a,?y),?z)),
     eq(q(?y,?z),?y_6) = eq(q(q(a,?y),?z),q(a,?y_6)),
     eq(?x_6,q(?y,?z)) = eq(q(a,?x_6),q(q(a,?y),?z)),
     eq(a,e) = false,
     eq(q(q(a,?y_5),?z_5),e) = false,
     eq(q(a,?x),e) = false,
     eq(e,a) = false,
     eq(e,q(q(a,?y_5),?z_5)) = false,
     eq(a,a) = eq(e,e),
     eq(q(q(a,?y_5),?z_5),a) = eq(e,q(?y_5,?z_5)),
     eq(a,q(q(a,?y_5),?z_5)) = eq(q(?y_5,?z_5),e),
     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),a) = eq(e,?y),
     eq(q(a,?y),q(q(a,?y_5),?z_5)) = eq(q(?y_5,?z_5),?y),
     eq(a,q(a,?x)) = eq(?x,e),
     eq(q(q(a,?y_5),?z_5),q(a,?x)) = eq(?x,q(?y_5,?z_5)),
     eq(a,q(q(a,?y_5),?z_5)) = eq(e,q(?y_5,?z_5)),
     eq(q(q(a,?y_5),?z_5),a) = eq(q(?y_5,?z_5),e),
     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(a,q(a,?y)) = eq(e,?y),
     eq(q(q(a,?y_5),?z_5),q(a,?y)) = eq(q(?y_5,?z_5),?y),
     eq(q(a,?x),a) = eq(?x,e),
     eq(q(a,?x),q(q(a,?y_5),?z_5)) = eq(?x,q(?y_5,?z_5)),
     false = eq(q(a,?x_5),e),
     eq(?x_6,?y_6) = eq(q(a,?y_6),q(a,?x_6)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <q(?x,?z_2), q(e,q(?x,?z_2))> by Rules <0, 2> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <q(?x_1,?z_2), q(?x_1,q(e,?z_2))> by Rules <1, 2> preceded by [(q,1)]
 joinable by a reduction of rules <[], [([(q,2)],0)]>
Critical Pair <q(q(q(?x_3,?y_3),?z_3),?z_2), q(?x_3,q(q(?y_3,?z_3),?z_2))> by Rules <3, 2> preceded by [(q,1)]
 joinable by a reduction of rules <[([(q,1)],2)], [([],3)]>
Critical Pair <q(?x_3,?x), q(q(?x_3,e),?x)> by Rules <0, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([(q,1)],1)]>
Critical Pair <q(?x_3,?x_1), q(q(?x_3,?x_1),e)> by Rules <1, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[], [([],1)]>
Critical Pair <q(?x_3,q(?x_2,q(?y_2,?z_2))), q(q(?x_3,q(?x_2,?y_2)),?z_2)> by Rules <2, 3> preceded by [(q,2)]
 joinable by a reduction of rules <[([(q,2)],3)], [([],2)]>
Critical Pair <eq(e,a), false> by Rules <1, 4> preceded by [(eq,2)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 17 rules by 3 steps unfolding
strenghten q(?x_13,e) and ?x_13
strenghten q(e,e) and e
strenghten eq(e,a) and false
strenghten eq(?x_10,?y_10) and eq(?y_10,?x_10)
strenghten q(q(?x_13,e),e) and ?x_13
strenghten eq(e,q(a,?x_4)) and false
strenghten eq(q(a,?x_4),e) and false
strenghten q(?x_1,q(e,?z_2)) and q(?x_1,?z_2)
strenghten q(?x_2,q(?y_2,e)) and q(?x_2,?y_2)
strenghten q(e,q(?x,?z_2)) and q(?x,?z_2)
strenghten q(q(?x_3,?x_1),e) and q(?x_3,?x_1)
strenghten q(q(?x_3,e),?x) and q(?x_3,?x)
strenghten q(q(e,?y_3),?z_3) and q(?y_3,?z_3)
strenghten eq(a,q(a,?y_5)) and eq(e,?y_5)
strenghten eq(q(a,?x_5),a) and eq(?x_5,e)
strenghten eq(e,q(q(a,?y_3),?z_3)) and false
strenghten eq(?x_5,q(e,e)) and eq(q(a,?x_5),a)
strenghten eq(q(e,e),?y_5) and eq(a,q(a,?y_5))
strenghten q(?x_2,q(?y_2,q(e,e))) and q(?x_2,?y_2)
strenghten q(?x_13,q(q(e,e),?z_2)) and q(?x_13,?z_2)
strenghten q(q(?x_3,?x_13),q(e,e)) and q(?x_3,?x_13)
strenghten eq(q(a,?x_5),q(a,?y_5)) and eq(?x_5,?y_5)
strenghten eq(q(a,?y_5),q(a,?x_5)) and eq(?x_5,?y_5)
strenghten q(?x_2,q(?y_2,q(?y_3,?z_3))) and q(q(q(?x_2,?y_2),?y_3),?z_3)
strenghten q(?x_3,q(q(?y_3,?z_3),?z_2)) and q(q(q(?x_3,?y_3),?z_3),?z_2)
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_2,?y_2)),?z_2) and q(?x_3,q(?x_2,q(?y_2,?z_2)))
strenghten eq(q(a,?x_5),q(q(a,?y_3),?z_3)) and eq(?x_5,q(?y_3,?z_3))
strenghten eq(q(q(a,?y_3),?z_3),q(a,?y_5)) and eq(q(?y_3,?z_3),?y_5)
obtain 69 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
<F,Q,Q_f,Delta> where
   F = {(a,0),(e,0),(q,2),(eq,2),(false,0)}
   Q = {q_0,q_1,q_{q(*,*)},q_{*},q_{a},q_{e}}
   Qf = {q_0,q_1}
   Delta = 
   [ a -> q_{q(*,*)},
     a -> q_{*},
     a -> q_{a},
     e -> q_{q(*,*)},
     e -> q_{*},
     e -> q_{e},
     q(q_{q(*,*)},q_{q(*,*)}) -> q_{q(*,*)},
     q(q_{q(*,*)},q_{*}) -> q_{q(*,*)},
     q(q_{*},q_{q(*,*)}) -> q_{q(*,*)},
     q(q_{*},q_{*}) -> q_{q(*,*)},
     q(q_{*},q_{*}) -> q_{*},
     eq(q_{*},q_{*}) -> q_{q(*,*)},
     eq(q_{*},q_{*}) -> q_{*},
     eq(q_{a},q_{e}) -> q_0,
     eq(q_{e},q_{a}) -> q_0,
     false -> q_1,
     false -> q_{q(*,*)},
     false -> q_{*} ]
Witness for Non-Confluence: <eq(a,e), false>
Direct Methods: not CR

Final result: not CR
R9.trs: Success(not CR)
(94 msec.)