(VAR x y z )
(RULES 
        xor(x,F) -> x
        xor(x,neg(x)) -> F
        and(x,T) -> x
        and(x,F) -> F
        and(x,x) -> x
        and(xor(x,y),z) -> xor(and(x,z),and(y,z))
        xor(x,x) -> F
        impl(x,y) -> xor(and(x,y),xor(x,T))
        or(x,y) -> xor(and(x,y),xor(x,y))
        equiv(x,y) -> xor(x,xor(y,T))
        neg(x) -> xor(x,T)
        
)