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