9.58/8.61	MAYBE
9.58/8.61	/export/starexec/sandbox/benchmark/theBenchmark.trs
9.58/8.61	Input rules:
9.58/8.61	   [ a -> b,
9.58/8.61	     a -> f(a),
9.58/8.61	     b -> f(f(b)),
9.58/8.61	     f(f(f(b))) -> b ]
9.58/8.61	Sorts having no ground terms: 
9.58/8.61	Rules applicable to ground terms:
9.58/8.61	   [ a -> b,
9.58/8.61	     a -> f(a),
9.58/8.61	     b -> f(f(b)),
9.58/8.61	     f(f(f(b))) -> b ]
9.58/8.61	Constructor pattern: []
9.58/8.61	Defined pattern: [f(?x_1),b,a]
9.58/8.61	Constructor subsystem:
9.58/8.61	   [ ]
9.58/8.61	Modified Constructor subsystem:
9.58/8.61	   [ ]
9.58/8.61	No orientable rules for f(?x_1). Add rules, and retry...
9.58/8.61	failed to construct defining rules
9.58/8.61	Retry with a different D/C-partition.
9.58/8.61	Constructor pattern: [f(?x_1)]
9.58/8.61	Defined pattern: [b,a]
9.58/8.61	Constructor subsystem:
9.58/8.61	   [ ]
9.58/8.61	Modified Constructor subsystem:
9.58/8.61	   [ ]
9.58/8.61	No orientable rules for b. Add rules, and retry...
9.58/8.61	failed to construct defining rules
9.58/8.61	Retry with a different D/C-partition.
9.58/8.61	Constructor pattern: [f(?x_1),b]
9.58/8.61	Defined pattern: [a]
9.58/8.61	Constructor subsystem:
9.58/8.61	   [ b -> f(f(b)),
9.58/8.61	     f(f(f(b))) -> b ]
9.58/8.61	Modified Constructor subsystem:
9.58/8.61	   [ b -> f(f(b)),
9.58/8.61	     f(f(f(b))) -> b ]
9.58/8.61	candidate for a:
9.58/8.61	   [ a -> b ]
9.58/8.61	Find a quasi-ordering ...
9.58/8.61	order successfully found
9.58/8.61	Precedence:
9.58/8.61	 a : Mul;
9.58/8.61	 b : Mul;
9.58/8.61	 f : Mul;
9.58/8.61	Rules:
9.58/8.61	   [ a -> b,
9.58/8.61	     f(f(f(b))) -> b ]
9.58/8.61	Check confluence of constructor subsystem...
9.58/8.61	Check Termination...
9.58/8.61	Terminating, WCR: CR
9.58/8.61	Conjectures:
9.58/8.61	   [ a = f(a),
9.58/8.61	     b = f(f(b)) ]
9.58/8.61	STEP 0
9.58/8.61	ES:
9.58/8.61	   [ a = f(a),
9.58/8.61	     b = f(f(b)) ]
9.58/8.61	HS:
9.58/8.61	   [ ]
9.58/8.61	ES0:
9.58/8.61	   [ b = f(b),
9.58/8.61	     b = f(f(b)) ]
9.58/8.61	HS0:
9.58/8.61	   [ ]
9.58/8.61	ES1:
9.58/8.61	   [ b = f(b),
9.58/8.61	     b = f(f(b)) ]
9.58/8.61	HS1:
9.58/8.61	   [ ]
9.58/8.61	No equation to expand
9.58/8.61	check Non-Ground-Confluence...
9.58/8.61	ground constructor terms for instantiation: {}
9.58/8.61	ground terms for instantiation: {a:o}
9.58/8.61	obtain 11 rules by 3 steps unfolding
9.58/8.61	obtain 100 candidates for checking non-joinability
9.58/8.61	check by TCAP-Approximation (failure)
9.58/8.61	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
9.58/8.61	check by Interpretation(mod2) (failure)
9.58/8.61	check by Descendants-Approximation, check by Ordering(poly) (failure)
9.58/8.61	: Failure(unknown)
9.58/8.61	(1833 msec.)
9.58/8.61	
9.58/8.61	=============================
9.58/8.61	Total: 0 Success, 1 Failure: 1835 millisec.
9.58/8.61	EOF