(VAR u x y z )
(STRATEGY INNERMOST)
(RULES 
        -(x,0) -> x
        -(s(x),s(y)) -> -(x,y)
        <=(0,y) -> true
        <=(s(x),0) -> false
        <=(s(x),s(y)) -> <=(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,-(z,s(x)),u)
        f(s(x),s(y),z,u) -> if(<=(x,y),f(s(x),-(y,x),z,u),f(x,u,z,u))
        
)