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