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