0.00/0.08	NO
0.00/0.08	/export/starexec/sandbox/benchmark/theBenchmark.trs
0.00/0.08	Input rules:
0.00/0.08	   [ b -> a,
0.00/0.08	     b -> c,
0.00/0.08	     c -> h(b),
0.00/0.08	     c -> d,
0.00/0.08	     a -> h(a),
0.00/0.08	     d -> h(d) ]
0.00/0.08	Sorts having no ground terms: 
0.00/0.08	Rules applicable to ground terms:
0.00/0.08	   [ b -> a,
0.00/0.08	     b -> c,
0.00/0.08	     c -> h(b),
0.00/0.08	     c -> d,
0.00/0.08	     a -> h(a),
0.00/0.08	     d -> h(d) ]
0.00/0.08	Constructor pattern: [h(?x_1)]
0.00/0.08	Defined pattern: [d,c,a,b]
0.00/0.08	Constructor subsystem:
0.00/0.08	   [ ]
0.00/0.08	Modified Constructor subsystem:
0.00/0.08	   [ ]
0.00/0.08	No orientable rules for d. Add rules, and retry...
0.00/0.08	failed to construct defining rules
0.00/0.08	Retry with a different D/C-partition.
0.00/0.08	Constructor pattern: [h(?x_1),d]
0.00/0.08	Defined pattern: [c,a,b]
0.00/0.08	Constructor subsystem:
0.00/0.08	   [ d -> h(d) ]
0.00/0.08	Modified Constructor subsystem:
0.00/0.08	   [ d -> h(d) ]
0.00/0.08	candidate for c:
0.00/0.08	   [ c -> d ]
0.00/0.08	   [ c -> h(b) ]
0.00/0.08	No orientable rules for a. Add rules, and retry...
0.00/0.08	failed to construct defining rules
0.00/0.08	Retry with a different D/C-partition.
0.00/0.08	Constructor pattern: [h(?x_1),d,a]
0.00/0.08	Defined pattern: [c,b]
0.00/0.08	Constructor subsystem:
0.00/0.08	   [ a -> h(a),
0.00/0.08	     d -> h(d) ]
0.00/0.08	Modified Constructor subsystem:
0.00/0.08	   [ a -> h(a),
0.00/0.08	     d -> h(d) ]
0.00/0.08	candidate for c:
0.00/0.08	   [ c -> d ]
0.00/0.08	   [ c -> h(b) ]
0.00/0.08	candidate for b:
0.00/0.08	   [ b -> c ]
0.00/0.08	   [ b -> a ]
0.00/0.08	Find a quasi-ordering ...
0.00/0.08	failed to find an ordering.
0.00/0.08	Try to supplement auxiliary rules.
0.00/0.08	{}{}{}{}{a}{d}Supplemented Rules:
0.00/0.08	   [ ]
0.00/0.08	failed to supplement auxiliary rules
0.00/0.08	check Non-Ground-Confluence...
0.00/0.08	ground constructor terms for instantiation: {}
0.00/0.08	ground terms for instantiation: {b:o}
0.00/0.08	obtain 12 rules by 3 steps unfolding
0.00/0.08	obtain 100 candidates for checking non-joinability
0.00/0.08	check by TCAP-Approximation (failure)
0.00/0.08	check by Ordering(rpo), check by Tree-Automata Approximation (success)
0.00/0.08	Witness for Non-Confluence: <a <- b -> d>
0.00/0.08	: Success(not GCR)
0.00/0.08	(33 msec.)
0.00/0.08	
0.00/0.08	=============================
0.00/0.08	Total: 1 Success, 0 Failure: 33 millisec.
0.00/0.08	EOF