(set-logic QF_UFLIAFS) (set-info :status unsat) (declare-sort E 0) (declare-fun A () (Set E)) (declare-fun B () (Set E)) (declare-fun C () (Set E)) (assert (and (= (as emptyset (Set E)) (intersection A B)) (subset C (union A B)) (>= (card C) 5) (<= (card A) 2) (<= (card B) 2) ) ) (check-sat)