22.60/20.67 MAYBE 22.60/20.67 (ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z110 22.60/20.67 Rewrite Rules: 22.60/20.67 [ a(a(?x)) -> b(?x), 22.60/20.67 b(a(?x)) -> a(b(?x)), 22.60/20.67 b(b(c(?x))) -> c(a(?x)), 22.60/20.67 b(b(?x)) -> a(a(a(?x))), 22.60/20.67 c(a(?x)) -> b(a(c(?x))) ] 22.60/20.67 Apply Direct Methods... 22.60/20.67 Inner CPs: 22.60/20.67 [ b(b(?x)) = a(b(a(?x))), 22.60/20.67 b(b(b(a(c(?x_4))))) = c(a(a(?x_4))), 22.60/20.67 b(a(b(?x_1))) = a(a(a(a(?x_1)))), 22.60/20.67 b(c(a(?x_2))) = a(a(a(b(c(?x_2))))), 22.60/20.67 c(b(?x)) = b(a(c(a(?x)))), 22.60/20.67 a(b(?x)) = b(a(?x)), 22.60/20.67 b(a(a(a(?x)))) = a(a(a(b(?x)))) ] 22.60/20.67 Outer CPs: 22.60/20.67 [ c(a(?x_2)) = a(a(a(c(?x_2)))) ] 22.60/20.67 not Overlay, check Termination... 22.60/20.67 unknown/not Terminating 22.60/20.67 unknown Knuth & Bendix 22.60/20.67 Linear 22.60/20.67 unknown Development Closed 22.60/20.67 unknown Strongly Closed 22.60/20.67 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 22.60/20.67 inner CP cond (upside-parallel) 22.60/20.67 innter CP Cond (outside) 22.60/20.67 unknown Upside-Parallel-Closed/Outside-Closed 22.60/20.67 (inner) Parallel CPs: (not computed) 22.60/20.67 unknown Toyama (Parallel CPs) 22.60/20.67 Simultaneous CPs: 22.60/20.67 [ a(b(?x_1)) = b(a(?x_1)), 22.60/20.67 b(b(?x_1)) = a(b(a(?x_1))), 22.60/20.67 a(b(b(?x_1))) = b(b(a(?x_1))), 22.60/20.67 b(a(c(b(?x_1)))) = c(b(a(?x_1))), 22.60/20.67 b(a(?x)) = a(b(?x)), 22.60/20.67 a(b(a(?x))) = b(b(?x)), 22.60/20.67 b(a(c(a(?x)))) = c(b(?x)), 22.60/20.67 a(a(a(b(?x_2)))) = b(a(b(a(?x_2)))), 22.60/20.67 a(a(a(a(?x)))) = b(a(b(?x))), 22.60/20.67 a(a(a(b(a(c(?x_5)))))) = c(a(a(?x_5))), 22.60/20.67 a(a(a(c(?x)))) = c(a(?x)), 22.60/20.67 b(b(b(a(c(?x_5))))) = c(a(a(?x_5))), 22.60/20.67 a(a(a(b(b(a(c(?x_5))))))) = b(c(a(a(?x_5)))), 22.60/20.67 a(a(a(b(c(?x))))) = b(c(a(?x))), 22.60/20.67 c(a(?x_3)) = a(a(a(c(?x_3)))), 22.60/20.67 b(a(a(a(?x_1)))) = a(a(a(b(?x_1)))), 22.60/20.67 b(a(b(?x_3))) = a(a(a(a(?x_3)))), 22.60/20.67 b(c(a(?x_4))) = a(a(a(b(c(?x_4))))), 22.60/20.67 a(a(a(a(a(a(?x_1)))))) = b(a(a(a(b(?x_1))))), 22.60/20.67 a(a(a(a(b(?x_3))))) = b(a(a(a(a(?x_3))))), 22.60/20.67 a(a(a(c(a(?x_4))))) = b(a(a(a(b(c(?x_4)))))), 22.60/20.67 a(a(a(b(?x)))) = b(a(a(a(?x)))), 22.60/20.67 c(b(?x_2)) = b(a(c(a(?x_2)))), 22.60/20.67 c(a(b(?x_2))) = b(b(b(a(c(a(?x_2)))))), 22.60/20.67 c(a(a(?x))) = b(b(b(a(c(?x))))) ] 22.60/20.67 unknown Okui (Simultaneous CPs) 22.60/20.67 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 22.60/20.67 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 22.60/20.67 check Locally Decreasing Diagrams by Rule Labelling... 22.60/20.67 Critical Pair by Rules <0, 1> preceded by [(b,1)] 22.60/20.67 joinable by a reduction of rules <[], [([(a,1)],1),([],0)]> 22.60/20.67 Critical Pair by Rules <4, 2> preceded by [(b,1),(b,1)] 22.60/20.67 joinable by a reduction of rules <[([(b,1)],3),([(b,1),(a,1)],0)], [([],4),([(b,1),(a,1)],4)]> 22.60/20.67 joinable by a reduction of rules <[([],3),([],0)], [([],4),([(b,1),(a,1)],4)]> 22.60/20.67 Critical Pair by Rules <1, 3> preceded by [(b,1)] 22.60/20.67 joinable by a reduction of rules <[([],1),([(a,1)],3)], []> 22.60/20.67 Critical Pair by Rules <2, 3> preceded by [(b,1)] 22.60/20.67 joinable by a reduction of rules <[([(b,1)],4),([(b,1)],1)], [([],0)]> 22.60/20.67 joinable by a reduction of rules <[([(b,1)],4),([],3)], [([(a,1)],0),([(a,1)],3)]> 22.60/20.67 Critical Pair by Rules <0, 4> preceded by [(c,1)] 22.60/20.67 unknown Diagram Decreasing 22.60/20.67 check Non-Confluence... 22.60/20.67 obtain 7 rules by 3 steps unfolding 22.60/20.67 obtain 100 candidates for checking non-joinability 22.60/20.67 check by TCAP-Approximation (failure) 22.60/20.67 check by Ordering(rpo), check by Tree-Automata Approximation (failure) 22.60/20.67 check by Interpretation(mod2) (failure) 22.60/20.67 check by Descendants-Approximation, check by Ordering(poly) (failure) 22.60/20.67 unknown Non-Confluence 22.60/20.67 unknown Huet (modulo AC) 22.60/20.67 check by Reduction-Preserving Completion... 22.60/20.67 failure(empty P) 22.60/20.67 unknown Reduction-Preserving Completion 22.60/20.67 check by Ordered Rewriting... 22.60/20.67 remove redundants rules and split 22.60/20.67 R-part: 22.60/20.67 [ a(a(?x)) -> b(?x), 22.60/20.67 b(a(?x)) -> a(b(?x)), 22.60/20.67 b(b(c(?x))) -> c(a(?x)), 22.60/20.67 b(b(?x)) -> a(a(a(?x))), 22.60/20.67 c(a(?x)) -> b(a(c(?x))) ] 22.60/20.67 E-part: 22.60/20.67 [ ] 22.60/20.67 ...failed to find a suitable LPO. 22.60/20.67 unknown Confluence by Ordered Rewriting 22.60/20.67 Direct Methods: Can't judge 22.60/20.67 22.60/20.67 Try Persistent Decomposition for... 22.60/20.67 [ a(a(?x)) -> b(?x), 22.60/20.67 b(a(?x)) -> a(b(?x)), 22.60/20.67 b(b(c(?x))) -> c(a(?x)), 22.60/20.67 b(b(?x)) -> a(a(a(?x))), 22.60/20.67 c(a(?x)) -> b(a(c(?x))) ] 22.60/20.67 Sort Assignment: 22.60/20.67 a : 12=>12 22.60/20.67 b : 12=>12 22.60/20.67 c : 12=>12 22.60/20.67 maximal types: {12} 22.60/20.68 Persistent Decomposition failed: Can't judge 22.60/20.68 22.60/20.68 Try Layer Preserving Decomposition for... 22.60/20.68 [ a(a(?x)) -> b(?x), 22.60/20.68 b(a(?x)) -> a(b(?x)), 22.60/20.68 b(b(c(?x))) -> c(a(?x)), 22.60/20.68 b(b(?x)) -> a(a(a(?x))), 22.60/20.68 c(a(?x)) -> b(a(c(?x))) ] 22.60/20.68 Layer Preserving Decomposition failed: Can't judge 22.60/20.68 22.60/20.68 Try Commutative Decomposition for... 22.60/20.68 [ a(a(?x)) -> b(?x), 22.60/20.68 b(a(?x)) -> a(b(?x)), 22.60/20.68 b(b(c(?x))) -> c(a(?x)), 22.60/20.68 b(b(?x)) -> a(a(a(?x))), 22.60/20.68 c(a(?x)) -> b(a(c(?x))) ] 22.60/20.68 Outside Critical Pair: by Rules <3, 2> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{0}, b(a(c(?x_2)))> 22.60/20.68 <{0}, a(b(c(?x_2)))> 22.60/20.68 <{}, a(a(a(c(?x_2))))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{4}, b(a(c(?x_2)))> 22.60/20.68 <{}, c(a(?x_2))> 22.60/20.68 Inside Critical Pair: by Rules <0, 1> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{3}, a(a(a(?x)))> 22.60/20.68 <{}, b(b(?x))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{1}, a(a(b(?x)))> 22.60/20.68 <{}, a(b(a(?x)))> 22.60/20.68 Inside Critical Pair: by Rules <4, 2> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{1,3}, a(a(a(a(b(c(?x_4))))))> 22.60/20.68 <{3}, a(a(a(b(a(c(?x_4))))))> 22.60/20.68 <{3}, b(a(a(a(a(c(?x_4))))))> 22.60/20.68 <{1}, b(b(a(b(c(?x_4)))))> 22.60/20.68 <{}, b(b(b(a(c(?x_4)))))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{4}, b(a(c(a(?x_4))))> 22.60/20.68 <{0}, c(b(?x_4))> 22.60/20.68 <{}, c(a(a(?x_4)))> 22.60/20.68 Inside Critical Pair: by Rules <1, 3> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{1}, a(b(b(?x_1)))> 22.60/20.68 <{}, b(a(b(?x_1)))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{0}, b(b(?x_1))> 22.60/20.68 <{0}, b(a(a(?x_1)))> 22.60/20.68 <{0}, a(b(a(?x_1)))> 22.60/20.68 <{0}, a(a(b(?x_1)))> 22.60/20.68 <{}, a(a(a(a(?x_1))))> 22.60/20.68 Inside Critical Pair: by Rules <2, 3> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{4}, b(b(a(c(?x_2))))> 22.60/20.68 <{}, b(c(a(?x_2)))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{0}, b(a(b(c(?x_2))))> 22.60/20.68 <{0}, a(b(b(c(?x_2))))> 22.60/20.68 <{}, a(a(a(b(c(?x_2)))))> 22.60/20.68 Inside Critical Pair: by Rules <0, 4> 22.60/20.68 develop reducts from lhs term... 22.60/20.68 <{}, c(b(?x))> 22.60/20.68 develop reducts from rhs term... 22.60/20.68 <{1,4}, a(b(b(a(c(?x)))))> 22.60/20.68 <{1}, a(b(c(a(?x))))> 22.60/20.68 <{4}, b(a(b(a(c(?x)))))> 22.60/20.68 <{}, b(a(c(a(?x))))> 22.60/20.68 Commutative Decomposition failed: Can't judge 22.60/20.68 No further decomposition possible 22.60/20.68 22.60/20.68 22.60/20.68 Combined result: Can't judge 22.60/20.68 /export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR) 22.60/20.68 (8026 msec.) 22.60/20.68 EOF