0.00/0.16	NO
0.00/0.16	/export/starexec/sandbox2/benchmark/theBenchmark.trs
0.00/0.16	Input rules:
0.00/0.16	   [ a -> b,
0.00/0.16	     f(g(a)) -> f(a) ]
0.00/0.16	Sorts having no ground terms: 
0.00/0.16	Rules applicable to ground terms:
0.00/0.16	   [ a -> b,
0.00/0.16	     f(g(a)) -> f(a) ]
0.00/0.16	Constructor pattern: [b,f(?x_1),g(?x_1)]
0.00/0.16	Defined pattern: [a]
0.00/0.16	Constructor subsystem:
0.00/0.16	   [ ]
0.00/0.16	Modified Constructor subsystem:
0.00/0.16	   [ ]
0.00/0.16	candidate for a:
0.00/0.16	   [ a -> b ]
0.00/0.16	Find a quasi-ordering ...
0.00/0.16	order successfully found
0.00/0.16	Precedence:
0.00/0.16	 a : Mul;
0.00/0.16	 b : Mul;
0.00/0.16	 f : Mul,  g : Mul;
0.00/0.16	Rules:
0.00/0.16	   [ a -> b ]
0.00/0.16	Conjectures:
0.00/0.16	   [ f(g(a)) = f(a) ]
0.00/0.16	STEP 0
0.00/0.16	ES:
0.00/0.16	   [ f(g(a)) = f(a) ]
0.00/0.16	HS:
0.00/0.16	   [ ]
0.00/0.16	ES0:
0.00/0.16	   [ f(g(b)) = f(b) ]
0.00/0.16	HS0:
0.00/0.16	   [ ]
0.00/0.16	ES1:
0.00/0.16	   [ f(g(b)) = f(b) ]
0.00/0.16	HS1:
0.00/0.16	   [ ]
0.00/0.16	No equation to expand
0.00/0.16	check Non-Ground-Confluence...
0.00/0.16	ground constructor terms for instantiation: {b,f(b),g(b)}
0.00/0.16	ground terms for instantiation: {b:o,f(b):o,g(b):o}
0.00/0.16	obtain 3 rules by 3 steps unfolding
0.00/0.16	obtain 3 candidates for checking non-joinability
0.00/0.16	check by TCAP-Approximation (success)
0.00/0.16	Witness for Non-Confluence: <f(g(b)) <- f(g(a)) -> f(b)>
0.00/0.16	: Success(not GCR)
0.00/0.16	(4 msec.)
0.00/0.16	
0.00/0.16	=============================
0.00/0.16	Total: 1 Success, 0 Failure: 5 millisec.
0.00/0.16	EOF