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