MAYBE (ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z110 Rewrite Rules: [ a(a(?x)) -> b(?x), b(a(?x)) -> a(b(?x)), b(b(c(?x))) -> c(a(?x)), b(b(?x)) -> a(a(a(?x))), c(a(?x)) -> b(a(c(?x))) ] Apply Direct Methods... Inner CPs: [ b(b(?x)) = a(b(a(?x))), b(b(b(a(c(?x_4))))) = c(a(a(?x_4))), b(a(b(?x_1))) = a(a(a(a(?x_1)))), b(c(a(?x_2))) = a(a(a(b(c(?x_2))))), c(b(?x)) = b(a(c(a(?x)))), a(b(?x)) = b(a(?x)), b(a(a(a(?x)))) = a(a(a(b(?x)))) ] Outer CPs: [ c(a(?x_2)) = a(a(a(c(?x_2)))) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ a(b(?x_1)) = b(a(?x_1)), b(b(?x_1)) = a(b(a(?x_1))), a(b(b(?x_1))) = b(b(a(?x_1))), b(a(c(b(?x_1)))) = c(b(a(?x_1))), b(a(?x)) = a(b(?x)), a(b(a(?x))) = b(b(?x)), b(a(c(a(?x)))) = c(b(?x)), a(a(a(b(?x_2)))) = b(a(b(a(?x_2)))), a(a(a(a(?x)))) = b(a(b(?x))), a(a(a(b(a(c(?x_5)))))) = c(a(a(?x_5))), a(a(a(c(?x)))) = c(a(?x)), b(b(b(a(c(?x_5))))) = c(a(a(?x_5))), a(a(a(b(b(a(c(?x_5))))))) = b(c(a(a(?x_5)))), a(a(a(b(c(?x))))) = b(c(a(?x))), c(a(?x_3)) = a(a(a(c(?x_3)))), b(a(a(a(?x_1)))) = a(a(a(b(?x_1)))), b(a(b(?x_3))) = a(a(a(a(?x_3)))), b(c(a(?x_4))) = a(a(a(b(c(?x_4))))), a(a(a(a(a(a(?x_1)))))) = b(a(a(a(b(?x_1))))), a(a(a(a(b(?x_3))))) = b(a(a(a(a(?x_3))))), a(a(a(c(a(?x_4))))) = b(a(a(a(b(c(?x_4)))))), a(a(a(b(?x)))) = b(a(a(a(?x)))), c(b(?x_2)) = b(a(c(a(?x_2)))), c(a(b(?x_2))) = b(b(b(a(c(a(?x_2)))))), c(a(a(?x))) = b(b(b(a(c(?x))))) ] 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 <0, 1> preceded by [(b,1)] joinable by a reduction of rules <[], [([(a,1)],1),([],0)]> Critical Pair by Rules <4, 2> preceded by [(b,1),(b,1)] joinable by a reduction of rules <[([(b,1)],3),([(b,1),(a,1)],0)], [([],4),([(b,1),(a,1)],4)]> joinable by a reduction of rules <[([],3),([],0)], [([],4),([(b,1),(a,1)],4)]> Critical Pair by Rules <1, 3> preceded by [(b,1)] joinable by a reduction of rules <[([],1),([(a,1)],3)], []> Critical Pair by Rules <2, 3> preceded by [(b,1)] joinable by a reduction of rules <[([(b,1)],4),([(b,1)],1)], [([],0)]> joinable by a reduction of rules <[([(b,1)],4),([],3)], [([(a,1)],0),([(a,1)],3)]> Critical Pair by Rules <0, 4> preceded by [(c,1)] unknown Diagram Decreasing check Non-Confluence... obtain 7 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... failure(empty P) unknown Reduction-Preserving Completion check by Ordered Rewriting... remove redundants rules and split R-part: [ a(a(?x)) -> b(?x), b(a(?x)) -> a(b(?x)), b(b(c(?x))) -> c(a(?x)), b(b(?x)) -> a(a(a(?x))), c(a(?x)) -> b(a(c(?x))) ] E-part: [ ] ...failed to find a suitable LPO. unknown Confluence by Ordered Rewriting Direct Methods: Can't judge Try Persistent Decomposition for... [ a(a(?x)) -> b(?x), b(a(?x)) -> a(b(?x)), b(b(c(?x))) -> c(a(?x)), b(b(?x)) -> a(a(a(?x))), c(a(?x)) -> b(a(c(?x))) ] Sort Assignment: a : 12=>12 b : 12=>12 c : 12=>12 maximal types: {12} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ a(a(?x)) -> b(?x), b(a(?x)) -> a(b(?x)), b(b(c(?x))) -> c(a(?x)), b(b(?x)) -> a(a(a(?x))), c(a(?x)) -> b(a(c(?x))) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ a(a(?x)) -> b(?x), b(a(?x)) -> a(b(?x)), b(b(c(?x))) -> c(a(?x)), b(b(?x)) -> a(a(a(?x))), c(a(?x)) -> b(a(c(?x))) ] Outside Critical Pair: by Rules <3, 2> develop reducts from lhs term... <{0}, b(a(c(?x_2)))> <{0}, a(b(c(?x_2)))> <{}, a(a(a(c(?x_2))))> develop reducts from rhs term... <{4}, b(a(c(?x_2)))> <{}, c(a(?x_2))> Inside Critical Pair: by Rules <0, 1> develop reducts from lhs term... <{3}, a(a(a(?x)))> <{}, b(b(?x))> develop reducts from rhs term... <{1}, a(a(b(?x)))> <{}, a(b(a(?x)))> Inside Critical Pair: by Rules <4, 2> develop reducts from lhs term... <{1,3}, a(a(a(a(b(c(?x_4))))))> <{3}, a(a(a(b(a(c(?x_4))))))> <{3}, b(a(a(a(a(c(?x_4))))))> <{1}, b(b(a(b(c(?x_4)))))> <{}, b(b(b(a(c(?x_4)))))> develop reducts from rhs term... <{4}, b(a(c(a(?x_4))))> <{0}, c(b(?x_4))> <{}, c(a(a(?x_4)))> Inside Critical Pair: by Rules <1, 3> develop reducts from lhs term... <{1}, a(b(b(?x_1)))> <{}, b(a(b(?x_1)))> develop reducts from rhs term... <{0}, b(b(?x_1))> <{0}, b(a(a(?x_1)))> <{0}, a(b(a(?x_1)))> <{0}, a(a(b(?x_1)))> <{}, a(a(a(a(?x_1))))> Inside Critical Pair: by Rules <2, 3> develop reducts from lhs term... <{4}, b(b(a(c(?x_2))))> <{}, b(c(a(?x_2)))> develop reducts from rhs term... <{0}, b(a(b(c(?x_2))))> <{0}, a(b(b(c(?x_2))))> <{}, a(a(a(b(c(?x_2)))))> Inside Critical Pair: by Rules <0, 4> develop reducts from lhs term... <{}, c(b(?x))> develop reducts from rhs term... <{1,4}, a(b(b(a(c(?x)))))> <{1}, a(b(c(a(?x))))> <{4}, b(a(b(a(c(?x)))))> <{}, b(a(c(a(?x))))> Commutative Decomposition failed: Can't judge No further decomposition possible Combined result: Can't judge 986.trs: Failure(unknown CR) (2356 msec.)