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