NO af/ONE-SORTED/684.trs Input rules: [ b -> c, b -> f(c), c -> c ] Sorts having no ground terms: Rules applicable to ground terms: [ b -> c, b -> f(c), c -> c ] Constructor pattern: [f(?x_1)] Defined pattern: [c,b] Constructor subsystem: [ ] Modified Constructor subsystem: [ ] No orientable rules for c. Add rules, and retry... failed to construct defining rules Retry with a different D/C-partition. Constructor pattern: [f(?x_1),c] Defined pattern: [b] Constructor subsystem: [ c -> c ] c -> c {} [ ] Modified Constructor subsystem: [ ] candidate for b: [ b -> c ] [ b -> f(c) ] Find a quasi-ordering ... order successfully found Precedence: b : Mul; f : Mul; c : Mul; Rules: [ b -> c ] Conjectures: [ b = f(c) ] STEP 0 ES: [ b = f(c) ] HS: [ ] ES0: [ c = f(c) ] HS0: [ ] ES1: [ c = f(c) ] HS1: [ ] : Success(not GCR) (2 msec.) 0.02