(declare-sort V 0)
(declare-fun B (V V) Bool)(declare-fun A (V) Bool)(declare-fun U0 (V) Bool)
(declare-fun U1 (V) Bool)
(declare-fun U2 (V) Bool)
(declare-fun U3 (V) Bool)
(assert
(and
(forall ((x V)) (=> (U0 x) (not (U1 x))))
(forall ((x V)) (=> (U0 x) (not (U2 x))))
(forall ((x V)) (=> (U0 x) (not (U3 x))))
(forall ((x V)) (=> (U1 x) (not (U0 x))))
(forall ((x V)) (=> (U1 x) (not (U2 x))))
(forall ((x V)) (=> (U1 x) (not (U3 x))))
(forall ((x V)) (=> (U2 x) (not (U0 x))))
(forall ((x V)) (=> (U2 x) (not (U1 x))))
(forall ((x V)) (=> (U2 x) (not (U3 x))))
(forall ((x V)) (=> (U3 x) (not (U0 x))))
(forall ((x V)) (=> (U3 x) (not (U1 x))))
(forall ((x V)) (=> (U3 x) (not (U2 x))))
(exists ((x V)) (U0 x))
(exists ((x V)) (U1 x))
(exists ((x V)) (U2 x))
(exists ((x V)) (U3 x))
(and (forall ((x V) (y V)) (=> (and (U0 x) (U0 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U0 x) (U2 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U0 x) (U3 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U1 x) (U0 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U1 x) (U1 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U1 x) (U3 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U2 x) (U0 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U2 x) (U1 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U2 x) (U2 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U3 x) (U1 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U3 x) (U2 y)) (not (B x y))))
(forall ((x V) (y V)) (=> (and (U3 x) (U3 y)) (not (B x y))))
)
(forall ((x V)) (exists ((y V)) (and (B x y) (or (U0 y) (U1 y) (U2 y) (U3 y) ))))
(forall ((x V)) (=> (U0 x) (A x)))
(forall ((x V) (y V)) (=> (B x y) (and (=> (A x) (not (A y))) (=> (not (A x)) (A y)))))
))(check-sat)
(get-model)