(VAR x y z)
(RULES
not(x) -> xor(x,true)
implies(x,y) -> xor(and(x,y),xor(x,true))
or(x,y) -> xor(and(x,y),xor(x,y))
=(x,y) -> xor(x,xor(y,true))
)

(COMMENT Example 2.30 (Boolean Ring) in \cite{SK90})