YES af/ONE-SORTED/648.trs Input rules: [ c -> b, b -> a ] Sorts having no ground terms: Rules applicable to ground terms: [ c -> b, b -> a ] Constructor pattern: [a] Defined pattern: [b,c] Constructor subsystem: [ ] Modified Constructor subsystem: [ ] candidate for b: [ b -> a ] candidate for c: [ c -> b ] Find a quasi-ordering ... order successfully found Precedence: c : Mul; b : Mul; a : Mul; Rules: [ b -> a, c -> b ] Conjectures: [ ] STEP 0 ES: [ ] HS: [ ] ES0: [ ] HS0: [ ] ES1: [ ] HS1: [ ] : Success(GCR) (2 msec.) 0.02