YES Did not drop rules. Inlined conditions for 0 rules. Left-inlined conditions for 2 rules: f(g(a())) -> b() | g(c()) -> c() | Due to Ifrit-method removed 0 infeasible rules. Did not use redundant rules method. INFEASIBLE because problem |(x,x) ->* |(a(),c()) obtained from input requires [problem obtained from equal lhs of x ->* a() and x ->* c() is proven infeasible using the symbol transition graph on a() *<- x ->* c()] where | is used as a fresh function symbol, since it is illegal in the input format.