(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))), p -> a(p), p -> b(p) ] Apply Direct Methods... Inner CPs: [ a(a(b(a(?x_1)))) = b(a(b(b(?x_1)))), b(b(a(b(?x)))) = a(b(a(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: [ a(p) = b(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))))), 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))))))), a(b(a(b(a(b(?x_1)))))) = b(b(a(b(b(a(?x_1)))))), b(a(b(b(a(?x))))) = a(b(b(a(b(?x))))), a(b(a(a(?x)))) = b(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))))), 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))))))), b(a(b(a(b(a(?x_1)))))) = a(a(b(a(a(b(?x_1)))))), a(b(a(a(b(?x))))) = b(a(a(b(a(?x))))), b(a(b(b(?x)))) = a(a(b(a(?x)))), b(p) = a(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 [(a,1)] joinable by a reduction of rules <[([(a,1)],0)], [([],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 <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 <3, 2> preceded by [] joinable by a reduction of rules <[([(b,1)],2),([(b,1),(a,1)],3),([],1)], [([(a,1)],3),([(a,1),(b,1)],2)]> joinable by a reduction of rules <[([(b,1)],2),([(b,1),(a,1)],3)], [([(a,1)],3),([(a,1),(b,1)],2),([],0)]> unknown Diagram Decreasing check Non-Confluence... obtain 12 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: [ a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?x))) ] S: unknown termination failure(Step 1) STEP: 2 (linear) S: [ p -> a(p), p -> b(p) ] P: [ a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?x))) ] S: unknown termination failure(Step 2) STEP: 3 (relative) S: [ p -> a(p), p -> b(p) ] P: [ a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?x))) ] Check relative termination: [ p -> a(p), p -> b(p) ] [ a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?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))), p -> a(p), p -> b(p) ] Sort Assignment: a : 8=>8 b : 8=>8 p : =>8 maximal types: {8} 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))), p -> a(p), p -> b(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))), p -> a(p), p -> b(p) ] Outside Critical Pair: by Rules <3, 2> develop reducts from lhs term... <{3}, b(b(p))> <{2}, b(a(p))> <{}, b(p)> develop reducts from rhs term... <{3}, a(b(p))> <{2}, a(a(p))> <{}, a(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 <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))))> Try A Minimal Decomposition {2,3}{0,1} {2,3} (cm)Rewrite Rules: [ p -> a(p), p -> b(p) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ 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: [ b(p) = a(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 {0,1} (cm)Rewrite Rules: [ a(b(a(?x))) -> b(a(b(?x))), b(a(b(?x))) -> a(b(a(?x))) ] Apply Direct Methods... Inner CPs: [ a(a(b(a(?x_1)))) = b(a(b(b(?x_1)))), b(b(a(b(?x)))) = a(b(a(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 1285.trs: Failure(unknown CR) MAYBE (3337 msec.)