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