(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)) (U x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))(check-sat)
(get-model)