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