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