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