(ignored inputs)COMMENT submitted by: Hans Zantema
Rewrite Rules:
[ a(b(a(?x))) -> b(a(b(?x))),
b(a(b(?x))) -> a(b(a(?x))),
a(c(a(?x))) -> c(a(c(?x))),
c(a(c(?x))) -> a(c(a(?x))),
b(c(b(?x))) -> c(b(c(?x))),
c(b(c(?x))) -> b(c(b(?x))),
p -> a(p),
p -> b(p),
p -> c(p) ]
Apply Direct Methods...
Inner CPs:
[ a(a(b(a(?x_1)))) = b(a(b(b(?x_1)))),
a(b(c(a(c(?x_2))))) = b(a(b(c(a(?x_2))))),
b(b(a(b(?x)))) = a(b(a(a(?x)))),
b(a(c(b(c(?x_4))))) = a(b(a(c(b(?x_4))))),
a(c(b(a(b(?x))))) = c(a(c(b(a(?x))))),
a(a(c(a(?x_3)))) = c(a(c(c(?x_3)))),
c(c(a(c(?x_2)))) = a(c(a(a(?x_2)))),
c(a(b(c(b(?x_5))))) = a(c(a(b(c(?x_5))))),
b(c(a(b(a(?x_1))))) = c(b(c(a(b(?x_1))))),
b(b(c(b(?x_5)))) = c(b(c(c(?x_5)))),
c(b(a(c(a(?x_3))))) = b(c(b(a(c(?x_3))))),
c(c(b(c(?x_4)))) = b(c(b(b(?x_4)))),
a(b(b(a(b(?x))))) = b(a(b(b(a(?x))))),
b(a(a(b(a(?x))))) = a(b(a(a(b(?x))))),
a(c(c(a(c(?x))))) = c(a(c(c(a(?x))))),
c(a(a(c(a(?x))))) = a(c(a(a(c(?x))))),
b(c(c(b(c(?x))))) = c(b(c(c(b(?x))))),
c(b(b(c(b(?x))))) = b(c(b(b(c(?x))))) ]
Outer CPs:
[ a(p) = b(p),
a(p) = c(p),
b(p) = c(p) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
[ a(a(b(a(?x_2)))) = b(a(b(b(?x_2)))),
a(b(b(a(b(?x_1))))) = b(a(b(b(a(?x_1))))),
a(b(c(a(c(?x_3))))) = b(a(b(c(a(?x_3))))),
b(a(b(a(b(a(?x_2)))))) = a(b(b(a(b(b(?x_2)))))),
b(a(b(b(b(a(b(?x_1))))))) = a(b(b(a(b(b(a(?x_1))))))),
b(a(b(b(c(a(c(?x_3))))))) = a(b(b(a(b(c(a(?x_3))))))),
a(b(a(b(a(b(?x_1)))))) = b(b(a(b(b(a(?x_1)))))),
a(b(a(c(a(c(?x_3)))))) = b(b(a(b(c(a(?x_3)))))),
c(a(c(a(b(a(?x_2)))))) = a(c(b(a(b(b(?x_2)))))),
c(a(c(b(b(a(b(?x_1))))))) = a(c(b(a(b(b(a(?x_1))))))),
c(a(c(b(c(a(c(?x_3))))))) = a(c(b(a(b(c(a(?x_3))))))),
b(a(b(b(a(?x))))) = a(b(b(a(b(?x))))),
a(b(a(a(?x)))) = b(b(a(b(?x)))),
c(a(c(b(a(?x))))) = a(c(b(a(b(?x))))),
b(b(a(b(?x_2)))) = a(b(a(a(?x_2)))),
b(a(a(b(a(?x_1))))) = a(b(a(a(b(?x_1))))),
b(a(c(b(c(?x_5))))) = a(b(a(c(b(?x_5))))),
a(b(a(b(a(b(?x_2)))))) = b(a(a(b(a(a(?x_2)))))),
a(b(a(a(a(b(a(?x_1))))))) = b(a(a(b(a(a(b(?x_1))))))),
a(b(a(a(c(b(c(?x_5))))))) = b(a(a(b(a(c(b(?x_5))))))),
b(a(b(a(b(a(?x_1)))))) = a(a(b(a(a(b(?x_1)))))),
b(a(b(c(b(c(?x_5)))))) = a(a(b(a(c(b(?x_5)))))),
c(b(c(b(a(b(?x_2)))))) = b(c(a(b(a(a(?x_2)))))),
c(b(c(a(a(b(a(?x_1))))))) = b(c(a(b(a(a(b(?x_1))))))),
c(b(c(a(c(b(c(?x_5))))))) = b(c(a(b(a(c(b(?x_5))))))),
a(b(a(a(b(?x))))) = b(a(a(b(a(?x))))),
b(a(b(b(?x)))) = a(a(b(a(?x)))),
c(b(c(a(b(?x))))) = b(c(a(b(a(?x))))),
a(a(c(a(?x_4)))) = c(a(c(c(?x_4)))),
a(c(c(a(c(?x_1))))) = c(a(c(c(a(?x_1))))),
a(c(b(a(b(?x_2))))) = c(a(c(b(a(?x_2))))),
c(a(c(a(c(a(?x_4)))))) = a(c(c(a(c(c(?x_4)))))),
c(a(c(c(c(a(c(?x_1))))))) = a(c(c(a(c(c(a(?x_1))))))),
c(a(c(c(b(a(b(?x_2))))))) = a(c(c(a(c(b(a(?x_2))))))),
b(a(b(a(c(a(?x_4)))))) = a(b(c(a(c(c(?x_4)))))),
b(a(b(c(c(a(c(?x_1))))))) = a(b(c(a(c(c(a(?x_1))))))),
b(a(b(c(b(a(b(?x_2))))))) = a(b(c(a(c(b(a(?x_2))))))),
a(c(a(c(a(c(?x_1)))))) = c(c(a(c(c(a(?x_1)))))),
a(c(a(b(a(b(?x_2)))))) = c(c(a(c(b(a(?x_2)))))),
c(a(c(c(a(?x))))) = a(c(c(a(c(?x))))),
b(a(b(c(a(?x))))) = a(b(c(a(c(?x))))),
a(c(a(a(?x)))) = c(c(a(c(?x)))),
c(c(a(c(?x_4)))) = a(c(a(a(?x_4)))),
c(a(a(c(a(?x_1))))) = a(c(a(a(c(?x_1))))),
c(a(b(c(b(?x_6))))) = a(c(a(b(c(?x_6))))),
a(c(a(c(a(c(?x_4)))))) = c(a(a(c(a(a(?x_4)))))),
a(c(a(a(a(c(a(?x_1))))))) = c(a(a(c(a(a(c(?x_1))))))),
a(c(a(a(b(c(b(?x_6))))))) = c(a(a(c(a(b(c(?x_6))))))),
c(a(c(a(c(a(?x_1)))))) = a(a(c(a(a(c(?x_1)))))),
c(a(c(b(c(b(?x_6)))))) = a(a(c(a(b(c(?x_6)))))),
b(c(b(c(a(c(?x_4)))))) = c(b(a(c(a(a(?x_4)))))),
b(c(b(a(a(c(a(?x_1))))))) = c(b(a(c(a(a(c(?x_1))))))),
b(c(b(a(b(c(b(?x_6))))))) = c(b(a(c(a(b(c(?x_6))))))),
a(c(a(a(c(?x))))) = c(a(a(c(a(?x))))),
c(a(c(c(?x)))) = a(a(c(a(?x)))),
b(c(b(a(c(?x))))) = c(b(a(c(a(?x))))),
b(b(c(b(?x_6)))) = c(b(c(c(?x_6)))),
b(c(c(b(c(?x_1))))) = c(b(c(c(b(?x_1))))),
b(c(a(b(a(?x_3))))) = c(b(c(a(b(?x_3))))),
c(b(c(b(c(b(?x_6)))))) = b(c(c(b(c(c(?x_6)))))),
c(b(c(c(c(b(c(?x_1))))))) = b(c(c(b(c(c(b(?x_1))))))),
c(b(c(c(a(b(a(?x_3))))))) = b(c(c(b(c(a(b(?x_3))))))),
a(b(a(b(c(b(?x_6)))))) = b(a(c(b(c(c(?x_6)))))),
a(b(a(c(c(b(c(?x_1))))))) = b(a(c(b(c(c(b(?x_1))))))),
a(b(a(c(a(b(a(?x_3))))))) = b(a(c(b(c(a(b(?x_3))))))),
b(c(b(c(b(c(?x_1)))))) = c(c(b(c(c(b(?x_1)))))),
b(c(b(a(b(a(?x_3)))))) = c(c(b(c(a(b(?x_3)))))),
c(b(c(c(b(?x))))) = b(c(c(b(c(?x))))),
a(b(a(c(b(?x))))) = b(a(c(b(c(?x))))),
b(c(b(b(?x)))) = c(c(b(c(?x)))),
c(c(b(c(?x_6)))) = b(c(b(b(?x_6)))),
c(b(b(c(b(?x_1))))) = b(c(b(b(c(?x_1))))),
c(b(a(c(a(?x_5))))) = b(c(b(a(c(?x_5))))),
b(c(b(c(b(c(?x_6)))))) = c(b(b(c(b(b(?x_6)))))),
b(c(b(b(b(c(b(?x_1))))))) = c(b(b(c(b(b(c(?x_1))))))),
b(c(b(b(a(c(a(?x_5))))))) = c(b(b(c(b(a(c(?x_5))))))),
a(c(a(c(b(c(?x_6)))))) = c(a(b(c(b(b(?x_6)))))),
a(c(a(b(b(c(b(?x_1))))))) = c(a(b(c(b(b(c(?x_1))))))),
a(c(a(b(a(c(a(?x_5))))))) = c(a(b(c(b(a(c(?x_5))))))),
c(b(c(b(c(b(?x_1)))))) = b(b(c(b(b(c(?x_1)))))),
c(b(c(a(c(a(?x_5)))))) = b(b(c(b(a(c(?x_5)))))),
b(c(b(b(c(?x))))) = c(b(b(c(b(?x))))),
a(c(a(b(c(?x))))) = c(a(b(c(b(?x))))),
c(b(c(c(?x)))) = b(b(c(b(?x)))),
b(p) = a(p),
c(p) = a(p),
a(p) = b(p),
c(p) = b(p),
a(p) = c(p),
b(p) = c(p) ]
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 by Rules <1, 0> preceded by [(a,1)]
joinable by a reduction of rules <[([(a,1)],0)], [([],1)]>
Critical Pair by Rules <2, 0> preceded by [(a,1),(b,1)]
joinable by a reduction of rules <[([(a,1),(b,1)],3)], [([],1)]>
Critical Pair by Rules <0, 1> preceded by [(b,1)]
joinable by a reduction of rules <[([(b,1)],1)], [([],0)]>
Critical Pair by Rules <4, 1> preceded by [(b,1),(a,1)]
joinable by a reduction of rules <[([(b,1),(a,1)],5)], [([],0)]>
Critical Pair by Rules <0, 2> preceded by [(a,1),(c,1)]
joinable by a reduction of rules <[([(a,1),(c,1)],1)], [([],3)]>
Critical Pair by Rules <3, 2> preceded by [(a,1)]
joinable by a reduction of rules <[([(a,1)],2)], [([],3)]>
Critical Pair by Rules <2, 3> preceded by [(c,1)]
joinable by a reduction of rules <[([(c,1)],3)], [([],2)]>
Critical Pair by Rules <5, 3> preceded by [(c,1),(a,1)]
joinable by a reduction of rules <[([(c,1),(a,1)],4)], [([],2)]>
Critical Pair by Rules <1, 4> preceded by [(b,1),(c,1)]
joinable by a reduction of rules <[([(b,1),(c,1)],0)], [([],5)]>
Critical Pair by Rules <5, 4> preceded by [(b,1)]
joinable by a reduction of rules <[([(b,1)],4)], [([],5)]>
Critical Pair by Rules <3, 5> preceded by [(c,1),(b,1)]
joinable by a reduction of rules <[([(c,1),(b,1)],2)], [([],4)]>
Critical Pair by Rules <4, 5> preceded by [(c,1)]
joinable by a reduction of rules <[([(c,1)],5)], [([],4)]>
Critical Pair by Rules <0, 0> preceded by [(a,1),(b,1)]
joinable by a reduction of rules <[([(a,1),(b,1)],1)], [([],1)]>
Critical Pair by Rules <1, 1> preceded by [(b,1),(a,1)]
joinable by a reduction of rules <[([(b,1),(a,1)],0)], [([],0)]>
Critical Pair by Rules <2, 2> preceded by [(a,1),(c,1)]
joinable by a reduction of rules <[([(a,1),(c,1)],3)], [([],3)]>
Critical Pair by Rules <3, 3> preceded by [(c,1),(a,1)]
joinable by a reduction of rules <[([(c,1),(a,1)],2)], [([],2)]>
Critical Pair by Rules <4, 4> preceded by [(b,1),(c,1)]
joinable by a reduction of rules <[([(b,1),(c,1)],5)], [([],5)]>
Critical Pair by Rules <5, 5> preceded by [(c,1),(b,1)]
joinable by a reduction of rules <[([(c,1),(b,1)],4)], [([],4)]>
Critical Pair by Rules <7, 6> preceded by []
joinable by a reduction of rules <[([(b,1)],6),([(b,1),(a,1)],7),([],1)], [([(a,1)],7),([(a,1),(b,1)],6)]>
joinable by a reduction of rules <[([(b,1)],6),([(b,1),(a,1)],7)], [([(a,1)],7),([(a,1),(b,1)],6),([],0)]>
Critical Pair by Rules <8, 6> preceded by []
joinable by a reduction of rules <[([(c,1)],6),([(c,1),(a,1)],8),([],3)], [([(a,1)],8),([(a,1),(c,1)],6)]>
joinable by a reduction of rules <[([(c,1)],6),([(c,1),(a,1)],8)], [([(a,1)],8),([(a,1),(c,1)],6),([],2)]>
Critical Pair by Rules <8, 7> preceded by []
joinable by a reduction of rules <[([(c,1)],7),([(c,1),(b,1)],8),([],5)], [([(b,1)],8),([(b,1),(c,1)],7)]>
joinable by a reduction of rules <[([(c,1)],7),([(c,1),(b,1)],8)], [([(b,1)],8),([(b,1),(c,1)],7),([],4)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
where
F = {(a,1),(b,1),(c,1),(p,0)}
Q = {q_0,q_1,q_{b(a(*))},q_{b(c(*))},q_{a(b(*))},q_{a(c(*))},q_{*},q_{p},q_{a(*)},q_{b(*)},q_{b(p)},q_{c(*)},q_{c(a(*))},q_{c(b(*))}}
Qf = {q_0,q_1}
Delta =
[ a(q_{b(a(*))}) -> q_0,
a(q_{b(a(*))}) -> q_{b(a(*))},
a(q_{b(a(*))}) -> q_{a(b(*))},
a(q_{b(a(*))}) -> q_{p},
a(q_{b(a(*))}) -> q_{a(*)},
a(q_{b(a(*))}) -> q_{b(*)},
a(q_{b(a(*))}) -> q_{b(p)},
a(q_{*}) -> q_{*},
a(q_{*}) -> q_{p},
a(q_{*}) -> q_{a(*)},
a(q_{b(*)}) -> q_{a(b(*))},
a(q_{b(p)}) -> q_0,
a(q_{c(*)}) -> q_{a(c(*))},
a(q_{c(a(*))}) -> q_1,
a(q_{c(a(*))}) -> q_{a(c(*))},
a(q_{c(a(*))}) -> q_{p},
a(q_{c(a(*))}) -> q_{a(*)},
a(q_{c(a(*))}) -> q_{c(*)},
a(q_{c(a(*))}) -> q_{c(a(*))},
b(q_{a(b(*))}) -> q_0,
b(q_{a(b(*))}) -> q_{b(a(*))},
b(q_{a(b(*))}) -> q_{a(b(*))},
b(q_{a(b(*))}) -> q_{p},
b(q_{a(b(*))}) -> q_{a(*)},
b(q_{a(b(*))}) -> q_{b(*)},
b(q_{a(b(*))}) -> q_{b(p)},
b(q_{*}) -> q_{*},
b(q_{*}) -> q_{p},
b(q_{*}) -> q_{b(*)},
b(q_{p}) -> q_{b(p)},
b(q_{a(*)}) -> q_{b(a(*))},
b(q_{c(*)}) -> q_{b(c(*))},
b(q_{c(b(*))}) -> q_1,
b(q_{c(b(*))}) -> q_{b(c(*))},
b(q_{c(b(*))}) -> q_{p},
b(q_{c(b(*))}) -> q_{b(*)},
b(q_{c(b(*))}) -> q_{b(p)},
b(q_{c(b(*))}) -> q_{c(*)},
b(q_{c(b(*))}) -> q_{c(b(*))},
c(q_{b(c(*))}) -> q_1,
c(q_{b(c(*))}) -> q_{b(c(*))},
c(q_{b(c(*))}) -> q_{p},
c(q_{b(c(*))}) -> q_{b(*)},
c(q_{b(c(*))}) -> q_{b(p)},
c(q_{b(c(*))}) -> q_{c(*)},
c(q_{b(c(*))}) -> q_{c(b(*))},
c(q_{a(c(*))}) -> q_1,
c(q_{a(c(*))}) -> q_{a(c(*))},
c(q_{a(c(*))}) -> q_{p},
c(q_{a(c(*))}) -> q_{a(*)},
c(q_{a(c(*))}) -> q_{c(*)},
c(q_{a(c(*))}) -> q_{c(a(*))},
c(q_{*}) -> q_{*},
c(q_{*}) -> q_{p},
c(q_{*}) -> q_{c(*)},
c(q_{p}) -> q_1,
c(q_{a(*)}) -> q_{c(a(*))},
c(q_{b(*)}) -> q_{c(b(*))},
p -> q_{*},
p -> q_{p} ]
Witness for Non-Confluence:
Direct Methods: not CR
Combined result: not CR
1282.trs: Success(not CR)
NO
(937 msec.)