(VAR x y z)
(THEORY (AC union inter))
(RULES
if(true, x, y) -> x
if(false,x,y) -> y
eq(0,0) -> true
eq(0,s(x)) -> false
eq(s(x),s(y)) -> eq(x,y)
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)
)