YES Did not drop rules. Inlined conditions for 3 rules: div(s(x) ,s(y)) -> s(div(minus(x,y) ,s(y))) | lte(s(x) ,y) ->* false() power(x,n) -> mult(mult(power(x ,div(n,s(s(0())))) ,power(x,div(n,s(s(0()))))) ,s(0())) | mod(n ,s(s(0()))) ->* 0() power(x,n) -> mult(mult(power(x ,div(n,s(s(0())))) ,power(x,div(n,s(s(0()))))) ,x) | mod(n,s(s(0()))) ->* s(z) Left-inlined conditions for 0 rules. Due to Ifrit-method removed 0 infeasible rules. Did not use redundant rules method. INFEASIBLE because problem |(mod(0(),s(s(0()))) ,power(x2 ,div(0() ,s(s(0()))))) ->* |(s(x1),x4) obtained from input requires [problem mod(0() ,s(s(0()))) ->* s(x1) obtained from root-nonreachability requires [problem obtained from narrowing is proven infeasible using the symbol transition graph on 0() ->* s(x1) ,problem mod(0() ,s(s(0()))) ->* s(x1) obtained from root-nonreachability requires [problem obtained from narrowing is proven infeasible using the symbol transition graph on 0() ->* s(x1)] ,problem obtained from narrowing is proven infeasible since unification failed for mod(0(),s(s(0()))) ~ s(x1) ,problem mod(0() ,s(s(0()))) ->* s(x1) obtained from root-nonreachability requires [problem lte(s(s(0())) ,0()) ->* true() obtained from narrowing requires [problem obtained from narrowing is proven infeasible using the symbol transition graph on false() ->* true() ,problem obtained from narrowing is proven infeasible since unification failed for lte(s(s(0())),0()) ~ true()]]]] where | is used as a fresh function symbol, since it is illegal in the input format.