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