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