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