0.00/0.14 NO 0.00/0.14 (ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z101 0.00/0.14 Rewrite Rules: 0.00/0.14 [ a(a(?x)) -> b(b(b(?x))), 0.00/0.14 b(b(b(b(?x)))) -> a(a(a(?x))) ] 0.00/0.14 Apply Direct Methods... 0.00/0.14 Inner CPs: 0.00/0.14 [ a(b(b(b(?x)))) = b(b(b(a(?x)))), 0.00/0.14 b(a(a(a(?x)))) = a(a(a(b(?x)))), 0.00/0.14 b(b(a(a(a(?x))))) = a(a(a(b(b(?x))))), 0.00/0.14 b(b(b(a(a(a(?x)))))) = a(a(a(b(b(b(?x)))))) ] 0.00/0.14 Outer CPs: 0.00/0.14 [ ] 0.00/0.14 not Overlay, check Termination... 0.00/0.14 unknown/not Terminating 0.00/0.14 unknown Knuth & Bendix 0.00/0.14 Linear 0.00/0.14 unknown Development Closed 0.00/0.14 unknown Strongly Closed 0.00/0.14 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 0.00/0.14 inner CP cond (upside-parallel) 0.00/0.14 innter CP Cond (outside) 0.00/0.14 unknown Upside-Parallel-Closed/Outside-Closed 0.00/0.14 (inner) Parallel CPs: (not computed) 0.00/0.14 unknown Toyama (Parallel CPs) 0.00/0.14 Simultaneous CPs: 0.00/0.14 [ a(b(b(b(?x_1)))) = b(b(b(a(?x_1)))), 0.00/0.14 b(b(b(b(b(b(?x_1)))))) = a(b(b(b(a(?x_1))))), 0.00/0.14 b(b(b(a(?x)))) = a(b(b(b(?x)))), 0.00/0.14 b(a(a(a(?x_1)))) = a(a(a(b(?x_1)))), 0.00/0.14 b(b(a(a(a(?x_1))))) = a(a(a(b(b(?x_1))))), 0.00/0.14 b(b(b(a(a(a(?x_1)))))) = a(a(a(b(b(b(?x_1)))))), 0.00/0.14 a(a(a(a(a(a(?x_1)))))) = b(a(a(a(b(b(b(?x_1))))))), 0.00/0.14 a(a(a(a(a(a(?x_1)))))) = b(b(a(a(a(b(b(?x_1))))))), 0.00/0.14 a(a(a(b(a(a(a(?x_1))))))) = b(b(a(a(a(b(b(b(?x_1)))))))), 0.00/0.14 a(a(a(a(a(a(?x_1)))))) = b(b(b(a(a(a(b(?x_1))))))), 0.00/0.14 a(a(a(b(a(a(a(?x_1))))))) = b(b(b(a(a(a(b(b(?x_1)))))))), 0.00/0.14 a(a(a(b(b(a(a(a(?x_1)))))))) = b(b(b(a(a(a(b(b(b(?x_1))))))))), 0.00/0.14 a(a(a(b(?x)))) = b(a(a(a(?x)))), 0.00/0.14 a(a(a(b(b(?x))))) = b(b(a(a(a(?x))))), 0.00/0.14 a(a(a(b(b(b(?x)))))) = b(b(b(a(a(a(?x)))))) ] 0.00/0.14 unknown Okui (Simultaneous CPs) 0.00/0.14 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.14 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 0.00/0.14 check Locally Decreasing Diagrams by Rule Labelling... 0.00/0.14 Critical Pair by Rules <0, 0> preceded by [(a,1)] 0.00/0.14 unknown Diagram Decreasing 0.00/0.14 check Non-Confluence... 0.00/0.14 obtain 6 rules by 3 steps unfolding 0.00/0.14 obtain 100 candidates for checking non-joinability 0.00/0.14 check by TCAP-Approximation (success) 0.00/0.14 Witness for Non-Confluence: b(b(b(a(c_1))))> 0.00/0.14 Direct Methods: not CR 0.00/0.14 0.00/0.14 Combined result: not CR 0.00/0.14 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not CR) 0.00/0.14 (93 msec.) 0.00/0.14 EOF