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