NO
af/ONE-SORTED/668.trs
Input rules:
   [ a -> c,
     a -> h(c,a),
     h(b,f(c)) -> b,
     c -> h(a,h(h(b,a),a)) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ a -> c,
     a -> h(c,a),
     h(b,f(c)) -> b,
     c -> h(a,h(h(b,a),a)) ]
Constructor pattern: [h(?x_1,?x_2),b,f(?x_1)]
Defined pattern: [c,a]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for c:
   [ c -> h(a,h(h(b,a),a)) ]
candidate for a:
   [ a -> c ]
Find a quasi-ordering ...
encodeSameNthStatus h/0, h/1
encodeSameNthStatus(sub) logArF:1, logArG:1
failed to find an ordering.
Try to supplement auxiliary rules.
{}{a}{}{}Supplemented Rules:
   [ ]
failed to supplement auxiliary rules
check Non-Ground-Confluence...
ground constructor terms for instantiation: {b,h(b,b),f(b)}
ground terms for instantiation: {b:o,h(b,b):o,f(b):o}
obtain 11 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
<F,Q,Q_f,Delta> where
   F = {(a,0),(b,0),(c,0),(f,1),(h,2)}
   Q = {q_0,q_1,q_{a},q_{b},q_{c},q_{h(h(b,a),a)},q_{h(b,a)}}
   Qf = {q_0,q_1}
   Delta = 
   [ a -> q_{a},
     b -> q_{b},
     c -> q_1,
     c -> q_{a},
     c -> q_{c},
     h(q_{a},q_{h(h(b,a),a)}) -> q_1,
     h(q_{a},q_{h(h(b,a),a)}) -> q_{a},
     h(q_{a},q_{h(h(b,a),a)}) -> q_{c},
     h(q_{b},q_{a}) -> q_{h(b,a)},
     h(q_{c},q_{a}) -> q_0,
     h(q_{c},q_{a}) -> q_{a},
     h(q_{h(b,a)},q_{a}) -> q_{h(h(b,a),a)} ]
Witness for Non-Confluence: <h(c,a), c>
: Success(not GCR)
(33 msec.)
0.05