MAYBE 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.