0.00/0.36	YES
0.00/0.36	/export/starexec/sandbox/benchmark/theBenchmark.trs
0.00/0.36	Input rules:
0.00/0.36	   [ f(a) -> f(f(a)),
0.00/0.36	     a -> b,
0.00/0.36	     f(?x:o) -> f(b) ]
0.00/0.36	Sorts having no ground terms: 
0.00/0.36	Rules applicable to ground terms:
0.00/0.36	   [ f(a) -> f(f(a)),
0.00/0.36	     a -> b,
0.00/0.36	     f(?x:o) -> f(b) ]
0.00/0.36	Constructor pattern: [f(?x_1),b]
0.00/0.36	Defined pattern: [a]
0.00/0.36	Constructor subsystem:
0.00/0.36	   [ f(?x) -> f(b) ]
0.00/0.36	f(?x) -> f(b)
0.00/0.36	{?x:=b}
0.00/0.36	   [ {?x:=f(?x_1)} ]
0.00/0.36	Modified Constructor subsystem:
0.00/0.36	   [ f(f(?x_1)) -> f(b) ]
0.00/0.36	candidate for a:
0.00/0.36	   [ a -> b ]
0.00/0.36	Find a quasi-ordering ...
0.00/0.36	order successfully found
0.00/0.36	Precedence:
0.00/0.36	 f : Mul;
0.00/0.36	 a : Mul;
0.00/0.36	 b : Mul;
0.00/0.36	Rules:
0.00/0.36	   [ a -> b,
0.00/0.36	     f(f(?x_1)) -> f(b) ]
0.00/0.36	Check confluence of constructor subsystem...
0.00/0.36	Check Termination...
0.00/0.36	Terminating, WCR: CR
0.00/0.36	Conjectures:
0.00/0.36	   [ f(a) = f(f(a)) ]
0.00/0.36	STEP 0
0.00/0.36	ES:
0.00/0.36	   [ f(a) = f(f(a)) ]
0.00/0.36	HS:
0.00/0.36	   [ ]
0.00/0.36	ES0:
0.00/0.36	   [ f(b) = f(b) ]
0.00/0.36	HS0:
0.00/0.36	   [ ]
0.00/0.36	ES1:
0.00/0.36	   [ ]
0.00/0.36	HS1:
0.00/0.36	   [ ]
0.00/0.36	: Success(GCR)
0.00/0.36	(4 msec.)
0.00/0.36	
0.00/0.36	=============================
0.00/0.36	Total: 1 Success, 0 Failure: 4 millisec.
0.00/0.36	EOF