YES Did not drop rules. Inlined conditions for 2 rules: f(k(z),a()) -> g(h(z),h(z)) | h(z) ->* b() f(k(a()),h(a())) -> k(a()) | Left-inlined conditions for 0 rules. Due to Ifrit-method removed 1 infeasible rules: f(k(z),a()) -> g(h(z),h(z)) | h(z) ->* b() Did not use redundant rules method. INFEASIBLE because problem obtained from root-nonreachability is proven infeasible using the symbol transition graph on f(x,y) ->* g(z,z) where | is used as a fresh function symbol, since it is illegal in the input format.