0.00/0.07	YES
0.00/0.07	/export/starexec/sandbox/benchmark/theBenchmark.trs
0.00/0.07	Input rules:
0.00/0.07	   [ f(a,b) -> c,
0.00/0.07	     a -> a',
0.00/0.07	     b -> b',
0.00/0.07	     c -> f(a',b),
0.00/0.07	     c -> f(a,b'),
0.00/0.07	     c -> f(a,b) ]
0.00/0.07	Sorts having no ground terms: 
0.00/0.07	Rules applicable to ground terms:
0.00/0.07	   [ f(a,b) -> c,
0.00/0.07	     a -> a',
0.00/0.07	     b -> b',
0.00/0.07	     c -> f(a',b),
0.00/0.07	     c -> f(a,b'),
0.00/0.07	     c -> f(a,b) ]
0.00/0.07	Constructor pattern: [f(?x_1,?x_2),a',b']
0.00/0.07	Defined pattern: [c,b,a]
0.00/0.07	Constructor subsystem:
0.00/0.07	   [ ]
0.00/0.07	Modified Constructor subsystem:
0.00/0.07	   [ ]
0.00/0.07	candidate for c:
0.00/0.07	   [ c -> f(a,b) ]
0.00/0.07	   [ c -> f(a,b') ]
0.00/0.07	   [ c -> f(a',b) ]
0.00/0.07	candidate for b:
0.00/0.07	   [ b -> b' ]
0.00/0.07	candidate for a:
0.00/0.07	   [ a -> a' ]
0.00/0.07	Find a quasi-ordering ...
0.00/0.07	order successfully found
0.00/0.07	Precedence:
0.00/0.07	 c : Mul,  b : Mul;
0.00/0.07	 f : Mul;
0.00/0.07	 b' : Mul;
0.00/0.07	 a : Mul;
0.00/0.07	 a' : Mul;
0.00/0.07	Rules:
0.00/0.07	   [ c -> f(a,b'),
0.00/0.07	     b -> b',
0.00/0.07	     a -> a' ]
0.00/0.07	Conjectures:
0.00/0.07	   [ f(a,b) = c,
0.00/0.07	     c = f(a',b),
0.00/0.07	     c = f(a,b) ]
0.00/0.07	STEP 0
0.00/0.07	ES:
0.00/0.07	   [ f(a,b) = c,
0.00/0.07	     c = f(a',b),
0.00/0.07	     c = f(a,b) ]
0.00/0.07	HS:
0.00/0.07	   [ ]
0.00/0.07	ES0:
0.00/0.07	   [ f(a',b') = f(a',b'),
0.00/0.07	     f(a',b') = f(a',b'),
0.00/0.07	     f(a',b') = f(a',b') ]
0.00/0.07	HS0:
0.00/0.07	   [ ]
0.00/0.07	ES1:
0.00/0.07	   [ ]
0.00/0.07	HS1:
0.00/0.07	   [ ]
0.00/0.07	: Success(GCR)
0.00/0.07	(12 msec.)
0.00/0.07	
0.00/0.07	=============================
0.00/0.07	Total: 1 Success, 0 Failure: 13 millisec.
0.00/0.07	EOF