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(),c()) ->* f(x,x) obtained from root-nonreachability requires [problem obtained from equal rhs of a() ->* x and c() ->* x 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.