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