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