(VAR x y z)
(THEORY (AC join) (AC meet))
(RULES
join(x,meet(x,y)) -> x
meet(x,join(x,y)) -> x
join(x,meet(y,z)) -> meet(join(x,y),join(x,z))
)