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