(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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?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(?x_4)))) = a(b(a(c(?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(?x_5)))) = a(c(a(b(?x_5)))), b(a(c(a(?x_3)))) = c(b(a(c(?x_3)))), b(b(c(?x_5))) = c(b(b(?x_5))), c(a(b(a(?x_1)))) = b(c(a(b(?x_1)))), c(c(b(?x_4))) = b(c(c(?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))))) ] 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(?x_5)))) = a(b(a(c(?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(?x_5)))))) = b(a(a(b(a(c(?x_5)))))), b(a(b(a(b(a(?x_1)))))) = a(a(b(a(a(b(?x_1)))))), b(a(b(c(b(?x_5))))) = a(a(b(a(c(?x_5))))), b(c(b(a(b(?x_2))))) = c(a(b(a(a(?x_2))))), b(c(a(a(b(a(?x_1)))))) = c(a(b(a(a(b(?x_1)))))), b(c(a(c(b(?x_5))))) = c(a(b(a(c(?x_5))))), a(b(a(a(b(?x))))) = b(a(a(b(a(?x))))), b(a(b(b(?x)))) = a(a(b(a(?x)))), b(c(a(b(?x)))) = 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(?x_6)))) = a(c(a(b(?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(?x_6)))))) = c(a(a(c(a(b(?x_6)))))), c(a(c(a(c(a(?x_1)))))) = a(a(c(a(a(c(?x_1)))))), c(a(c(b(c(?x_6))))) = a(a(c(a(b(?x_6))))), c(b(c(a(c(?x_4))))) = b(a(c(a(a(?x_4))))), c(b(a(a(c(a(?x_1)))))) = b(a(c(a(a(c(?x_1)))))), c(b(a(b(c(?x_6))))) = b(a(c(a(b(?x_6))))), a(c(a(a(c(?x))))) = c(a(a(c(a(?x))))), c(a(c(c(?x)))) = a(a(c(a(?x)))), c(b(a(c(?x)))) = b(a(c(a(?x)))), b(a(c(a(?x_5)))) = c(b(a(c(?x_5)))), b(b(c(?x_6))) = c(b(b(?x_6))), a(b(a(a(c(a(?x_5)))))) = b(a(c(b(a(c(?x_5)))))), a(b(a(b(c(?x_6))))) = b(a(c(b(b(?x_6))))), b(c(a(c(a(?x_5))))) = c(c(b(a(c(?x_5))))), b(c(b(c(?x_6)))) = c(c(b(b(?x_6)))), a(b(a(c(?x)))) = b(a(c(b(?x)))), b(c(c(?x))) = c(c(b(?x))), c(a(b(a(?x_3)))) = b(c(a(b(?x_3)))), c(c(b(?x_6))) = b(c(c(?x_6))), a(c(a(a(b(a(?x_3)))))) = c(a(b(c(a(b(?x_3)))))), a(c(a(c(b(?x_6))))) = c(a(b(c(c(?x_6))))), c(b(a(b(a(?x_3))))) = b(b(c(a(b(?x_3))))), c(b(c(b(?x_6)))) = b(b(c(c(?x_6)))), a(c(a(b(?x)))) = c(a(b(c(?x)))), c(b(b(?x))) = b(b(c(?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 <3, 4> preceded by [(b,1)] joinable by a reduction of rules <[([(b,1)],2)], [([],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 <1, 5> preceded by [(c,1)] joinable by a reduction of rules <[([(c,1)],0)], [([],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 <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),([],5)], [([(b,1)],8)]> joinable by a reduction of rules <[([(c,1)],7)], [([(b,1)],8),([],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 (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) unknown Non-Confluence unknown Huet (modulo AC) check by Reduction-Preserving Completion... STEP: 1 (parallel) S: [ p -> a(p), p -> b(p), p -> c(p) ] P: [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)) ] S: unknown termination failure(Step 1) STEP: 2 (linear) S: [ p -> a(p), p -> b(p), p -> c(p) ] P: [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)) ] S: unknown termination failure(Step 2) STEP: 3 (relative) S: [ p -> a(p), p -> b(p), p -> c(p) ] P: [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)) ] Check relative termination: [ p -> a(p), p -> b(p), p -> c(p) ] [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)) ] not relatively terminatiing S/P: unknown relative termination failure(Step 3) failure(no possibility remains) unknown Reduction-Preserving Completion Direct Methods: Can't judge Try Persistent Decomposition for... [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)), p -> a(p), p -> b(p), p -> c(p) ] Sort Assignment: a : 14=>14 b : 14=>14 c : 14=>14 p : =>14 maximal types: {14} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)), p -> a(p), p -> b(p), p -> c(p) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ 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(?x)) -> c(b(?x)), c(b(?x)) -> b(c(?x)), p -> a(p), p -> b(p), p -> c(p) ] Outside Critical Pair: by Rules <7, 6> develop reducts from lhs term... <{8}, b(c(p))> <{7}, b(b(p))> <{6}, b(a(p))> <{}, b(p)> develop reducts from rhs term... <{8}, a(c(p))> <{7}, a(b(p))> <{6}, a(a(p))> <{}, a(p)> Outside Critical Pair: by Rules <8, 6> develop reducts from lhs term... <{8}, c(c(p))> <{7}, c(b(p))> <{6}, c(a(p))> <{}, c(p)> develop reducts from rhs term... <{8}, a(c(p))> <{7}, a(b(p))> <{6}, a(a(p))> <{}, a(p)> Outside Critical Pair: by Rules <8, 7> develop reducts from lhs term... <{8}, c(c(p))> <{7}, c(b(p))> <{6}, c(a(p))> <{}, c(p)> develop reducts from rhs term... <{8}, b(c(p))> <{7}, b(b(p))> <{6}, b(a(p))> <{}, b(p)> Inside Critical Pair: by Rules <1, 0> develop reducts from lhs term... <{0}, a(b(a(b(?x_1))))> <{}, a(a(b(a(?x_1))))> develop reducts from rhs term... <{1}, a(b(a(b(?x_1))))> <{}, b(a(b(b(?x_1))))> Inside Critical Pair: by Rules <2, 0> develop reducts from lhs term... <{4}, a(c(b(a(c(?x_2)))))> <{3}, a(b(a(c(a(?x_2)))))> <{}, a(b(c(a(c(?x_2)))))> develop reducts from rhs term... <{1}, a(b(a(c(a(?x_2)))))> <{4}, b(a(c(b(a(?x_2)))))> <{}, b(a(b(c(a(?x_2)))))> Inside Critical Pair: by Rules <0, 1> develop reducts from lhs term... <{1}, b(a(b(a(?x))))> <{}, b(b(a(b(?x))))> develop reducts from rhs term... <{0}, b(a(b(a(?x))))> <{}, a(b(a(a(?x))))> Inside Critical Pair: by Rules <4, 1> develop reducts from lhs term... <{5}, b(a(b(c(?x_4))))> <{}, b(a(c(b(?x_4))))> develop reducts from rhs term... <{0}, b(a(b(c(?x_4))))> <{}, a(b(a(c(?x_4))))> Inside Critical Pair: by Rules <0, 2> develop reducts from lhs term... <{5}, a(b(c(a(b(?x)))))> <{1}, a(c(a(b(a(?x)))))> <{}, a(c(b(a(b(?x)))))> develop reducts from rhs term... <{3}, a(c(a(b(a(?x)))))> <{5}, c(a(b(c(a(?x)))))> <{}, c(a(c(b(a(?x)))))> Inside Critical Pair: by Rules <3, 2> develop reducts from lhs term... <{2}, a(c(a(c(?x_3))))> <{}, a(a(c(a(?x_3))))> develop reducts from rhs term... <{3}, a(c(a(c(?x_3))))> <{}, c(a(c(c(?x_3))))> Inside Critical Pair: by Rules <2, 3> develop reducts from lhs term... <{3}, c(a(c(a(?x_2))))> <{}, c(c(a(c(?x_2))))> develop reducts from rhs term... <{2}, c(a(c(a(?x_2))))> <{}, a(c(a(a(?x_2))))> Inside Critical Pair: by Rules <5, 3> develop reducts from lhs term... <{4}, c(a(c(b(?x_5))))> <{}, c(a(b(c(?x_5))))> develop reducts from rhs term... <{2}, c(a(c(b(?x_5))))> <{}, a(c(a(b(?x_5))))> Inside Critical Pair: by Rules <3, 4> develop reducts from lhs term... <{2}, b(c(a(c(?x_3))))> <{}, b(a(c(a(?x_3))))> develop reducts from rhs term... <{5}, b(c(a(c(?x_3))))> <{}, c(b(a(c(?x_3))))> Inside Critical Pair: by Rules <5, 4> develop reducts from lhs term... <{4}, b(c(b(?x_5)))> <{}, b(b(c(?x_5)))> develop reducts from rhs term... <{5}, b(c(b(?x_5)))> <{}, c(b(b(?x_5)))> Inside Critical Pair: by Rules <1, 5> develop reducts from lhs term... <{0}, c(b(a(b(?x_1))))> <{}, c(a(b(a(?x_1))))> develop reducts from rhs term... <{4}, c(b(a(b(?x_1))))> <{}, b(c(a(b(?x_1))))> Inside Critical Pair: by Rules <4, 5> develop reducts from lhs term... <{5}, c(b(c(?x_4)))> <{}, c(c(b(?x_4)))> develop reducts from rhs term... <{4}, c(b(c(?x_4)))> <{}, b(c(c(?x_4)))> Try A Minimal Decomposition {8,6,7}{5,3,2,4,0,1} {8,6,7} (cm)Rewrite Rules: [ p -> c(p), p -> a(p), p -> b(p) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ c(p) = a(p), c(p) = b(p), a(p) = b(p) ] Overlay, check Innermost Termination... unknown Innermost 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(p) = c(p), b(p) = c(p), c(p) = a(p), b(p) = a(p), c(p) = b(p), a(p) = b(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 [] unknown Diagram Decreasing check Non-Confluence... obtain 10 rules by 3 steps unfolding obtain 100 candidates for checking non-joinability check by TCAP-Approximation (success) Witness for Non-Confluence: b(p)> Direct Methods: not CR {5,3,2,4,0,1} (cm)Rewrite Rules: [ c(b(?x)) -> b(c(?x)), c(a(c(?x))) -> a(c(a(?x))), a(c(a(?x))) -> c(a(c(?x))), b(c(?x)) -> c(b(?x)), a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?x))) ] Apply Direct Methods... Inner CPs: [ c(c(b(?x_3))) = b(c(c(?x_3))), c(a(b(a(?x_5)))) = b(c(a(b(?x_5)))), c(a(b(c(?x)))) = a(c(a(b(?x)))), c(c(a(c(?x_2)))) = a(c(a(a(?x_2)))), a(a(c(a(?x_1)))) = c(a(c(c(?x_1)))), a(c(b(a(b(?x_4))))) = c(a(c(b(a(?x_4))))), b(b(c(?x))) = c(b(b(?x))), b(a(c(a(?x_1)))) = c(b(a(c(?x_1)))), a(b(c(a(c(?x_2))))) = b(a(b(c(a(?x_2))))), a(a(b(a(?x_5)))) = b(a(b(b(?x_5)))), b(a(c(b(?x_3)))) = a(b(a(c(?x_3)))), b(b(a(b(?x_4)))) = a(b(a(a(?x_4)))), c(a(a(c(a(?x))))) = a(c(a(a(c(?x))))), a(c(c(a(c(?x))))) = c(a(c(c(a(?x))))), a(b(b(a(b(?x))))) = b(a(b(b(a(?x))))), b(a(a(b(a(?x))))) = a(b(a(a(b(?x))))) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed Strongly Closed Direct Methods: CR Commutative Decomposition failed: Can't judge No further decomposition possible Combined result: Can't judge 1284.trs: Failure(unknown CR) MAYBE (7293 msec.)