(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.)