(VAR x y)
(THEORY (AC or and))
(RULES
not(not(x)) -> x
or(not(x),not(y)) -> not(and(x,y))
)