(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)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (forall ((x)) (exists ((x)) (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)