YES
Did not drop rules.
Inlined conditions for 0 rules.
Left-inlined conditions for 0 rules.
Due to Ifrit-method removed 0 infeasible rules.
Did not use redundant rules method.
INFEASIBLE because

problem |(f(a(),b())
         ,f(a(),a())) ->* |(b(),a())
obtained from input
requires
  [problem f(a(),b()) ->* b()
  obtained from
  root-nonreachability
  requires
    [problem obtained from
    narrowing is proven infeasible
    using the symbol transition graph on
    a() ->* b()
    ,problem obtained from narrowing
    is proven infeasible
    since unification failed for
    f(a(),b()) ~ b()]]

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