(declare-sort V 0) (declare-fun U (V) Bool)(assert (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (and (U x) (not (U x))))))))))))))(check-sat) (get-model)