NO
af/ONE-SORTED/680.trs
Input rules:
   [ b -> f(a),
     a -> c,
     a -> a,
     h(c,f(f(f(a)))) -> h(f(f(c)),h(b,a)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b))))))) -> c ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ b -> f(a),
     a -> c,
     a -> a,
     h(c,f(f(f(a)))) -> h(f(f(c)),h(b,a)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b))))))) -> c ]
Constructor pattern: [f(?x_1),c,h(?x_1,?x_2)]
Defined pattern: [a,b]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for a:
   [ a -> c ]
candidate for b:
   [ b -> f(a) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 b : Mul;
 h : Mul;
 f : Mul;
 a : Mul;
 c : Mul;
Rules:
   [ a -> c,
     b -> f(a) ]
Conjectures:
   [ h(c,f(f(f(a)))) = h(f(f(c)),h(b,a)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b))))))) = c,
     a = a ]
STEP 0
ES:
   [ h(c,f(f(f(a)))) = h(f(f(c)),h(b,a)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b))))))) = c,
     a = a ]
HS:
   [ ]
ES0:
   [ h(c,f(f(f(c)))) = h(f(f(c)),h(f(c),c)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(c),c),c),c),h(h(h(f(c),c),f(h(f(h(f(f(c)),f(f(f(c))))),c))),h(c,f(h(f(c),f(f(h(h(c,f(c)),c)))))))))))),f(f(f(c)))))))) = c,
     c = c ]
HS0:
   [ ]
ES1:
   [ h(c,f(f(f(c)))) = h(f(f(c)),h(f(c),c)),
     f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(c),c),c),c),h(h(h(f(c),c),f(h(f(h(f(f(c)),f(f(f(c))))),c))),h(c,f(h(f(c),f(f(h(h(c,f(c)),c)))))))))))),f(f(f(c)))))))) = c ]
HS1:
   [ ]
No equation to expand
check Non-Ground-Confluence...
ground constructor terms for instantiation: {c,f(c),h(c,c)}
ground terms for instantiation: {c:o,f(c):o,h(c,c):o}
obtain 12 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <h(f(f(c)),h(b,a)) <- h(c,f(f(b))) -> h(c,f(f(f(c))))>
: Success(not GCR)
(556 msec.)
0.54