YES Did not drop rules. Inlined conditions for 0 rules. Left-inlined conditions for 0 rules. Due to Ifrit-method removed 1 infeasible rules: g(x) -> a() | h(x) ->* b() Did not use redundant rules method. INFEASIBLE because problem h(x) ->* b() obtained from root-nonreachability requires [problem obtained from narrowing is proven infeasible using TCAP on a() ->* b() ,problem obtained from narrowing is proven infeasible since unification failed for h(x) ~ b()] where | is used as a fresh function symbol, since it is illegal in the input format.