(VAR x y z)
(THEORY (AC union inter eq))
(RULES
if(true, x, y) -> x
if(false,x,y) -> y
eq(0,0) -> true
eq(0,1) -> false
eq(1,1) -> true
union(empty,x) -> x
inter(x,empty) -> empty
inter(x,union(y,z)) -> union(inter(x,y), inter(x,z))
inter(single(x),single(y)) -> if(eq(x,y),single(x),empty)
)