MAYBE af/ONE-SORTED/33.trs Input rules: [ f(a) -> f(g(b,b)), a -> g(c,c), c -> d, d -> b, b -> d ] Sorts having no ground terms: Rules applicable to ground terms: [ f(a) -> f(g(b,b)), a -> g(c,c), c -> d, d -> b, b -> d ] Constructor pattern: [g(?x_1,?x_2)] Defined pattern: [d,c,b,a,f(?x_1)] Constructor subsystem: [ ] Modified Constructor subsystem: [ ] candidate for d: [ d -> b ] candidate for c: [ c -> d ] candidate for b: [ b -> d ] candidate for a: [ a -> g(c,c) ] No orientable rules for f(?x_1). Add rules, and retry... failed to construct defining rules Retry with a different D/C-partition. Constructor pattern: [g(?x_1,?x_2),f(?x_1)] Defined pattern: [d,c,b,a] Constructor subsystem: [ ] Modified Constructor subsystem: [ ] candidate for d: [ d -> b ] candidate for c: [ c -> d ] candidate for b: [ b -> d ] candidate for a: [ a -> g(c,c) ] Find a quasi-ordering ... encodeSameNthStatus g/0, g/1 encodeSameNthStatus(sub) logArF:1, logArG:1 failed to find an ordering. Try to supplement auxiliary rules. {f(g(b,b))}{}{}{}{}Supplemented Rules: [ ] failed to supplement auxiliary rules check Non-Ground-Confluence... ground constructor terms for instantiation: {} ground terms for instantiation: {a:o} obtain 12 rules by 3 steps unfolding obtain 98 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) : Failure(unknown) (538 msec.) 1.96