YES
Did not drop rules.
Inlined conditions for 1 rules:
  f(y,a()) -> g(h(z),h(z)) 
   | y ->* k(z)
Left-inlined conditions for 1 rules:
  f(k(z),a()) -> g(h(z),h(z)) 
   | 
Due to Ifrit-method removed 0 infeasible rules.
Did not use redundant rules method.
INFEASIBLE because

problem f(k(b()),x) ->* g(h(a())
                         ,y)
obtained from
root-nonreachability
requires
  [problem obtained from
  narrowing is proven infeasible
  using TCAP on
  f(b(),x) ->* g(h(a()),y)
  ,problem obtained from narrowing
  is proven infeasible
  using TCAP on
  f(h(b()),x) ->* g(h(a()),y)
  ,problem obtained from narrowing
  is proven infeasible
  using TCAP on
  g(h(b()),h(b())) ->* g(h(a()),y)
  ,problem obtained from narrowing
  is proven infeasible
  since unification failed for
  f(k(b()),x) ~ g(h(a()),y)
  ,problem f(a(),x) ->* g(h(a())
                         ,y)
  obtained from narrowing
  requires
    [problem obtained from
    narrowing is proven infeasible
    using TCAP on
    f(b(),x) ->* g(h(a()),y)
    ,problem obtained from narrowing
    is proven infeasible
    since unification failed for
    f(a(),x) ~ g(h(a()),y)]]

where | is used as a fresh function symbol, since it is illegal in the input format.