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