0.00/0.04	NO
0.00/0.04	(ignored inputs)COMMENT doi:10.1016/0890-5401 ( 90 ) 90015-A [24] Example 1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
0.00/0.04	Rewrite Rules:
0.00/0.04	   [ a -> f(a,b),
0.00/0.04	     f(a,b) -> f(b,a) ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [ f(f(a,b),b) = f(b,a) ]
0.00/0.04	Outer CPs:
0.00/0.04	   [  ]
0.00/0.04	not Overlay, check Termination...
0.00/0.04	unknown/not Terminating
0.00/0.04	unknown Knuth & Bendix
0.00/0.04	Linear
0.00/0.04	unknown Development Closed
0.00/0.04	unknown Strongly Closed
0.00/0.04	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.04	inner CP cond (upside-parallel)
0.00/0.04	innter CP Cond (outside)
0.00/0.04	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.04	(inner) Parallel CPs: (not computed)
0.00/0.04	unknown Toyama (Parallel CPs)
0.00/0.04	Simultaneous CPs:
0.00/0.04	   [ f(b,a) = f(f(a,b),b),
0.00/0.04	     f(f(a,b),b) = f(b,a) ]
0.00/0.04	unknown Okui (Simultaneous CPs)
0.00/0.04	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.04	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.04	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.04	Critical Pair <f(f(a,b),b), f(b,a)> by Rules <0, 1> preceded by [(f,1)]
0.00/0.04	unknown Diagram Decreasing
0.00/0.04	check Non-Confluence...
0.00/0.04	obtain 10 rules by 3 steps unfolding
0.00/0.04	obtain 100 candidates for checking non-joinability
0.00/0.04	check by TCAP-Approximation (success)
0.00/0.04	Witness for Non-Confluence: <f(f(b,a),b) <- a -> f(b,a)>
0.00/0.04	Direct Methods: not CR
0.00/0.04	
0.00/0.04	Combined result: not CR
0.00/0.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.04	(8 msec.)
0.00/0.04	EOF