(VAR x y )
(RULES 
        minus(minus(x)) -> x
        minux(+(x,y)) -> +(minus(y),minus(x))
        +(minus(x),+(x,y)) -> y
        +(+(x,y),minus(y)) -> x
        
)