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