(set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) (declare-fun x () Int) (declare-fun y () Int) (assert (member y S)) (assert (not (member x (union S T)))) (assert (= x y)) (check-sat)