(VAR u x y z )
(STRATEGY INNERMOST)
(RULES 
        minus(0,y) -> 0
        minus(s(x),0) -> s(x)
        minus(s(x),s(y)) -> minus(x,y)
        le(0,y) -> true
        le(s(x),0) -> false
        le(s(x),s(y)) -> le(x,y)
        if(true,x,y) -> x
        if(false,x,y) -> y
        perfectp(0) -> false
        perfectp(s(x)) -> f(x,s(0),s(x),s(x))
        f(0,y,0,u) -> true
        f(0,y,s(z),u) -> false
        f(s(x),0,z,u) -> f(x,u,minus(z,s(x)),u)
        f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
)