(VAR x y z)
(THEORY (AC and or))
(RULES
and(x,0) -> 0
and(x,1) -> x
and(x,x) -> x
or(x,0) -> x
or(x,1) -> 1
or(x,x) -> x
)