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