0.00/0.03	YES
0.00/0.03	/export/starexec/sandbox2/benchmark/theBenchmark.trs
0.00/0.03	Input rules:
0.00/0.03	   [ f(a) -> b,
0.00/0.03	     f(a) -> f(c),
0.00/0.03	     a -> d,
0.00/0.03	     f(d) -> b,
0.00/0.03	     f(c) -> b,
0.00/0.03	     d -> c ]
0.00/0.03	Sorts having no ground terms: 
0.00/0.03	Rules applicable to ground terms:
0.00/0.03	   [ f(a) -> b,
0.00/0.03	     f(a) -> f(c),
0.00/0.03	     a -> d,
0.00/0.03	     f(d) -> b,
0.00/0.03	     f(c) -> b,
0.00/0.03	     d -> c ]
0.00/0.03	Constructor pattern: [f(?x_1),b,c]
0.00/0.03	Defined pattern: [d,a]
0.00/0.03	Constructor subsystem:
0.00/0.03	   [ f(c) -> b ]
0.00/0.03	Modified Constructor subsystem:
0.00/0.03	   [ f(c) -> b ]
0.00/0.03	candidate for d:
0.00/0.03	   [ d -> c ]
0.00/0.03	candidate for a:
0.00/0.03	   [ a -> d ]
0.00/0.03	Find a quasi-ordering ...
0.00/0.03	order successfully found
0.00/0.03	Precedence:
0.00/0.03	 a : Mul;
0.00/0.03	 d : Mul;
0.00/0.03	 f : Mul;
0.00/0.03	 b : Mul,  c : Mul;
0.00/0.03	Rules:
0.00/0.03	   [ d -> c,
0.00/0.03	     a -> d,
0.00/0.03	     f(c) -> 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) = b,
0.00/0.03	     f(a) = f(c),
0.00/0.03	     f(d) = b ]
0.00/0.03	STEP 0
0.00/0.03	ES:
0.00/0.03	   [ f(a) = b,
0.00/0.03	     f(a) = f(c),
0.00/0.03	     f(d) = b ]
0.00/0.03	HS:
0.00/0.03	   [ ]
0.00/0.03	ES0:
0.00/0.03	   [ b = b,
0.00/0.03	     b = b,
0.00/0.03	     b = 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	(5 msec.)
0.00/0.03	
0.00/0.03	=============================
0.00/0.03	Total: 1 Success, 0 Failure: 6 millisec.
0.00/0.03	EOF