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(x,x,x) ->* F(a()
                      ,b()
                      ,y)
obtained from
root-nonreachability
requires
  [problem obtained from
  equal lhs of x ->* a() and
  x ->* b() is proven infeasible
  using the symbol transition graph on
  a() *<- x ->* b()]

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