(COMMENT 

Full theory of booleans.
(Hsiang, 82), (Ben Cherifa & Lescanne, 87, p. 152), (Hsiang &
Dershowitz, 83), (Dershowitz 87, p. 102), (Steinbach 91, Example 8.5)

)

(VAR z  y  x)
(THEORY (AC or xor and))

(RULES

xor(F,x) -> x 
xor(neg(x),x) -> F 
and(T,x) -> x 
and(F,x) -> 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(T,x)) 
or(x,y) -> xor(and(x,y),xor(x,y)) 
equiv(x,y) -> xor(xor(T,y),x) 
neg(x) -> xor(T,x) 

)