(declare-sort V 0)
(declare-fun U (V) Bool)
(declare-fun B (V V) Bool)
(declare-fun U0 (V) Bool)
(declare-fun U1 (V) Bool)
(declare-fun U2 (V) Bool)
(declare-fun U3 (V) Bool)
(declare-fun U4 (V) Bool)
(declare-fun U5 (V) Bool)
(declare-fun U6 (V) Bool)
(declare-fun U7 (V) Bool)
(declare-fun U8 (V) Bool)
(declare-fun U9 (V) Bool)
(declare-fun U10 (V) Bool)
(declare-fun U11 (V) Bool)
(declare-fun U12 (V) Bool)
(declare-fun U13 (V) Bool)
(declare-fun U14 (V) Bool)
(declare-fun U15 (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)) (=> (U0 x) (not (U4 x))))
(forall ((x V)) (=> (U0 x) (not (U5 x))))
(forall ((x V)) (=> (U0 x) (not (U6 x))))
(forall ((x V)) (=> (U0 x) (not (U7 x))))
(forall ((x V)) (=> (U0 x) (not (U8 x))))
(forall ((x V)) (=> (U0 x) (not (U9 x))))
(forall ((x V)) (=> (U0 x) (not (U10 x))))
(forall ((x V)) (=> (U0 x) (not (U11 x))))
(forall ((x V)) (=> (U0 x) (not (U12 x))))
(forall ((x V)) (=> (U0 x) (not (U13 x))))
(forall ((x V)) (=> (U0 x) (not (U14 x))))
(forall ((x V)) (=> (U0 x) (not (U15 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)) (=> (U1 x) (not (U4 x))))
(forall ((x V)) (=> (U1 x) (not (U5 x))))
(forall ((x V)) (=> (U1 x) (not (U6 x))))
(forall ((x V)) (=> (U1 x) (not (U7 x))))
(forall ((x V)) (=> (U1 x) (not (U8 x))))
(forall ((x V)) (=> (U1 x) (not (U9 x))))
(forall ((x V)) (=> (U1 x) (not (U10 x))))
(forall ((x V)) (=> (U1 x) (not (U11 x))))
(forall ((x V)) (=> (U1 x) (not (U12 x))))
(forall ((x V)) (=> (U1 x) (not (U13 x))))
(forall ((x V)) (=> (U1 x) (not (U14 x))))
(forall ((x V)) (=> (U1 x) (not (U15 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)) (=> (U2 x) (not (U4 x))))
(forall ((x V)) (=> (U2 x) (not (U5 x))))
(forall ((x V)) (=> (U2 x) (not (U6 x))))
(forall ((x V)) (=> (U2 x) (not (U7 x))))
(forall ((x V)) (=> (U2 x) (not (U8 x))))
(forall ((x V)) (=> (U2 x) (not (U9 x))))
(forall ((x V)) (=> (U2 x) (not (U10 x))))
(forall ((x V)) (=> (U2 x) (not (U11 x))))
(forall ((x V)) (=> (U2 x) (not (U12 x))))
(forall ((x V)) (=> (U2 x) (not (U13 x))))
(forall ((x V)) (=> (U2 x) (not (U14 x))))
(forall ((x V)) (=> (U2 x) (not (U15 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))))
(forall ((x V)) (=> (U3 x) (not (U4 x))))
(forall ((x V)) (=> (U3 x) (not (U5 x))))
(forall ((x V)) (=> (U3 x) (not (U6 x))))
(forall ((x V)) (=> (U3 x) (not (U7 x))))
(forall ((x V)) (=> (U3 x) (not (U8 x))))
(forall ((x V)) (=> (U3 x) (not (U9 x))))
(forall ((x V)) (=> (U3 x) (not (U10 x))))
(forall ((x V)) (=> (U3 x) (not (U11 x))))
(forall ((x V)) (=> (U3 x) (not (U12 x))))
(forall ((x V)) (=> (U3 x) (not (U13 x))))
(forall ((x V)) (=> (U3 x) (not (U14 x))))
(forall ((x V)) (=> (U3 x) (not (U15 x))))
(forall ((x V)) (=> (U4 x) (not (U0 x))))
(forall ((x V)) (=> (U4 x) (not (U1 x))))
(forall ((x V)) (=> (U4 x) (not (U2 x))))
(forall ((x V)) (=> (U4 x) (not (U3 x))))
(forall ((x V)) (=> (U4 x) (not (U5 x))))
(forall ((x V)) (=> (U4 x) (not (U6 x))))
(forall ((x V)) (=> (U4 x) (not (U7 x))))
(forall ((x V)) (=> (U4 x) (not (U8 x))))
(forall ((x V)) (=> (U4 x) (not (U9 x))))
(forall ((x V)) (=> (U4 x) (not (U10 x))))
(forall ((x V)) (=> (U4 x) (not (U11 x))))
(forall ((x V)) (=> (U4 x) (not (U12 x))))
(forall ((x V)) (=> (U4 x) (not (U13 x))))
(forall ((x V)) (=> (U4 x) (not (U14 x))))
(forall ((x V)) (=> (U4 x) (not (U15 x))))
(forall ((x V)) (=> (U5 x) (not (U0 x))))
(forall ((x V)) (=> (U5 x) (not (U1 x))))
(forall ((x V)) (=> (U5 x) (not (U2 x))))
(forall ((x V)) (=> (U5 x) (not (U3 x))))
(forall ((x V)) (=> (U5 x) (not (U4 x))))
(forall ((x V)) (=> (U5 x) (not (U6 x))))
(forall ((x V)) (=> (U5 x) (not (U7 x))))
(forall ((x V)) (=> (U5 x) (not (U8 x))))
(forall ((x V)) (=> (U5 x) (not (U9 x))))
(forall ((x V)) (=> (U5 x) (not (U10 x))))
(forall ((x V)) (=> (U5 x) (not (U11 x))))
(forall ((x V)) (=> (U5 x) (not (U12 x))))
(forall ((x V)) (=> (U5 x) (not (U13 x))))
(forall ((x V)) (=> (U5 x) (not (U14 x))))
(forall ((x V)) (=> (U5 x) (not (U15 x))))
(forall ((x V)) (=> (U6 x) (not (U0 x))))
(forall ((x V)) (=> (U6 x) (not (U1 x))))
(forall ((x V)) (=> (U6 x) (not (U2 x))))
(forall ((x V)) (=> (U6 x) (not (U3 x))))
(forall ((x V)) (=> (U6 x) (not (U4 x))))
(forall ((x V)) (=> (U6 x) (not (U5 x))))
(forall ((x V)) (=> (U6 x) (not (U7 x))))
(forall ((x V)) (=> (U6 x) (not (U8 x))))
(forall ((x V)) (=> (U6 x) (not (U9 x))))
(forall ((x V)) (=> (U6 x) (not (U10 x))))
(forall ((x V)) (=> (U6 x) (not (U11 x))))
(forall ((x V)) (=> (U6 x) (not (U12 x))))
(forall ((x V)) (=> (U6 x) (not (U13 x))))
(forall ((x V)) (=> (U6 x) (not (U14 x))))
(forall ((x V)) (=> (U6 x) (not (U15 x))))
(forall ((x V)) (=> (U7 x) (not (U0 x))))
(forall ((x V)) (=> (U7 x) (not (U1 x))))
(forall ((x V)) (=> (U7 x) (not (U2 x))))
(forall ((x V)) (=> (U7 x) (not (U3 x))))
(forall ((x V)) (=> (U7 x) (not (U4 x))))
(forall ((x V)) (=> (U7 x) (not (U5 x))))
(forall ((x V)) (=> (U7 x) (not (U6 x))))
(forall ((x V)) (=> (U7 x) (not (U8 x))))
(forall ((x V)) (=> (U7 x) (not (U9 x))))
(forall ((x V)) (=> (U7 x) (not (U10 x))))
(forall ((x V)) (=> (U7 x) (not (U11 x))))
(forall ((x V)) (=> (U7 x) (not (U12 x))))
(forall ((x V)) (=> (U7 x) (not (U13 x))))
(forall ((x V)) (=> (U7 x) (not (U14 x))))
(forall ((x V)) (=> (U7 x) (not (U15 x))))
(forall ((x V)) (=> (U8 x) (not (U0 x))))
(forall ((x V)) (=> (U8 x) (not (U1 x))))
(forall ((x V)) (=> (U8 x) (not (U2 x))))
(forall ((x V)) (=> (U8 x) (not (U3 x))))
(forall ((x V)) (=> (U8 x) (not (U4 x))))
(forall ((x V)) (=> (U8 x) (not (U5 x))))
(forall ((x V)) (=> (U8 x) (not (U6 x))))
(forall ((x V)) (=> (U8 x) (not (U7 x))))
(forall ((x V)) (=> (U8 x) (not (U9 x))))
(forall ((x V)) (=> (U8 x) (not (U10 x))))
(forall ((x V)) (=> (U8 x) (not (U11 x))))
(forall ((x V)) (=> (U8 x) (not (U12 x))))
(forall ((x V)) (=> (U8 x) (not (U13 x))))
(forall ((x V)) (=> (U8 x) (not (U14 x))))
(forall ((x V)) (=> (U8 x) (not (U15 x))))
(forall ((x V)) (=> (U9 x) (not (U0 x))))
(forall ((x V)) (=> (U9 x) (not (U1 x))))
(forall ((x V)) (=> (U9 x) (not (U2 x))))
(forall ((x V)) (=> (U9 x) (not (U3 x))))
(forall ((x V)) (=> (U9 x) (not (U4 x))))
(forall ((x V)) (=> (U9 x) (not (U5 x))))
(forall ((x V)) (=> (U9 x) (not (U6 x))))
(forall ((x V)) (=> (U9 x) (not (U7 x))))
(forall ((x V)) (=> (U9 x) (not (U8 x))))
(forall ((x V)) (=> (U9 x) (not (U10 x))))
(forall ((x V)) (=> (U9 x) (not (U11 x))))
(forall ((x V)) (=> (U9 x) (not (U12 x))))
(forall ((x V)) (=> (U9 x) (not (U13 x))))
(forall ((x V)) (=> (U9 x) (not (U14 x))))
(forall ((x V)) (=> (U9 x) (not (U15 x))))
(forall ((x V)) (=> (U10 x) (not (U0 x))))
(forall ((x V)) (=> (U10 x) (not (U1 x))))
(forall ((x V)) (=> (U10 x) (not (U2 x))))
(forall ((x V)) (=> (U10 x) (not (U3 x))))
(forall ((x V)) (=> (U10 x) (not (U4 x))))
(forall ((x V)) (=> (U10 x) (not (U5 x))))
(forall ((x V)) (=> (U10 x) (not (U6 x))))
(forall ((x V)) (=> (U10 x) (not (U7 x))))
(forall ((x V)) (=> (U10 x) (not (U8 x))))
(forall ((x V)) (=> (U10 x) (not (U9 x))))
(forall ((x V)) (=> (U10 x) (not (U11 x))))
(forall ((x V)) (=> (U10 x) (not (U12 x))))
(forall ((x V)) (=> (U10 x) (not (U13 x))))
(forall ((x V)) (=> (U10 x) (not (U14 x))))
(forall ((x V)) (=> (U10 x) (not (U15 x))))
(forall ((x V)) (=> (U11 x) (not (U0 x))))
(forall ((x V)) (=> (U11 x) (not (U1 x))))
(forall ((x V)) (=> (U11 x) (not (U2 x))))
(forall ((x V)) (=> (U11 x) (not (U3 x))))
(forall ((x V)) (=> (U11 x) (not (U4 x))))
(forall ((x V)) (=> (U11 x) (not (U5 x))))
(forall ((x V)) (=> (U11 x) (not (U6 x))))
(forall ((x V)) (=> (U11 x) (not (U7 x))))
(forall ((x V)) (=> (U11 x) (not (U8 x))))
(forall ((x V)) (=> (U11 x) (not (U9 x))))
(forall ((x V)) (=> (U11 x) (not (U10 x))))
(forall ((x V)) (=> (U11 x) (not (U12 x))))
(forall ((x V)) (=> (U11 x) (not (U13 x))))
(forall ((x V)) (=> (U11 x) (not (U14 x))))
(forall ((x V)) (=> (U11 x) (not (U15 x))))
(forall ((x V)) (=> (U12 x) (not (U0 x))))
(forall ((x V)) (=> (U12 x) (not (U1 x))))
(forall ((x V)) (=> (U12 x) (not (U2 x))))
(forall ((x V)) (=> (U12 x) (not (U3 x))))
(forall ((x V)) (=> (U12 x) (not (U4 x))))
(forall ((x V)) (=> (U12 x) (not (U5 x))))
(forall ((x V)) (=> (U12 x) (not (U6 x))))
(forall ((x V)) (=> (U12 x) (not (U7 x))))
(forall ((x V)) (=> (U12 x) (not (U8 x))))
(forall ((x V)) (=> (U12 x) (not (U9 x))))
(forall ((x V)) (=> (U12 x) (not (U10 x))))
(forall ((x V)) (=> (U12 x) (not (U11 x))))
(forall ((x V)) (=> (U12 x) (not (U13 x))))
(forall ((x V)) (=> (U12 x) (not (U14 x))))
(forall ((x V)) (=> (U12 x) (not (U15 x))))
(forall ((x V)) (=> (U13 x) (not (U0 x))))
(forall ((x V)) (=> (U13 x) (not (U1 x))))
(forall ((x V)) (=> (U13 x) (not (U2 x))))
(forall ((x V)) (=> (U13 x) (not (U3 x))))
(forall ((x V)) (=> (U13 x) (not (U4 x))))
(forall ((x V)) (=> (U13 x) (not (U5 x))))
(forall ((x V)) (=> (U13 x) (not (U6 x))))
(forall ((x V)) (=> (U13 x) (not (U7 x))))
(forall ((x V)) (=> (U13 x) (not (U8 x))))
(forall ((x V)) (=> (U13 x) (not (U9 x))))
(forall ((x V)) (=> (U13 x) (not (U10 x))))
(forall ((x V)) (=> (U13 x) (not (U11 x))))
(forall ((x V)) (=> (U13 x) (not (U12 x))))
(forall ((x V)) (=> (U13 x) (not (U14 x))))
(forall ((x V)) (=> (U13 x) (not (U15 x))))
(forall ((x V)) (=> (U14 x) (not (U0 x))))
(forall ((x V)) (=> (U14 x) (not (U1 x))))
(forall ((x V)) (=> (U14 x) (not (U2 x))))
(forall ((x V)) (=> (U14 x) (not (U3 x))))
(forall ((x V)) (=> (U14 x) (not (U4 x))))
(forall ((x V)) (=> (U14 x) (not (U5 x))))
(forall ((x V)) (=> (U14 x) (not (U6 x))))
(forall ((x V)) (=> (U14 x) (not (U7 x))))
(forall ((x V)) (=> (U14 x) (not (U8 x))))
(forall ((x V)) (=> (U14 x) (not (U9 x))))
(forall ((x V)) (=> (U14 x) (not (U10 x))))
(forall ((x V)) (=> (U14 x) (not (U11 x))))
(forall ((x V)) (=> (U14 x) (not (U12 x))))
(forall ((x V)) (=> (U14 x) (not (U13 x))))
(forall ((x V)) (=> (U14 x) (not (U15 x))))
(forall ((x V)) (=> (U15 x) (not (U0 x))))
(forall ((x V)) (=> (U15 x) (not (U1 x))))
(forall ((x V)) (=> (U15 x) (not (U2 x))))
(forall ((x V)) (=> (U15 x) (not (U3 x))))
(forall ((x V)) (=> (U15 x) (not (U4 x))))
(forall ((x V)) (=> (U15 x) (not (U5 x))))
(forall ((x V)) (=> (U15 x) (not (U6 x))))
(forall ((x V)) (=> (U15 x) (not (U7 x))))
(forall ((x V)) (=> (U15 x) (not (U8 x))))
(forall ((x V)) (=> (U15 x) (not (U9 x))))
(forall ((x V)) (=> (U15 x) (not (U10 x))))
(forall ((x V)) (=> (U15 x) (not (U11 x))))
(forall ((x V)) (=> (U15 x) (not (U12 x))))
(forall ((x V)) (=> (U15 x) (not (U13 x))))
(forall ((x V)) (=> (U15 x) (not (U14 x))))
(forall ((x V)) (=> (U0 x) (exists ((y V)) (and (B x y) (U1 y) (forall ((x V)) (=> (B y x) (U2 x) (exists ((y V)) (and (B x y) (U3 y) (forall ((x V)) (=> (B y x) (U4 x) (exists ((y V)) (and (B x y) (U5 y) (forall ((x V)) (=> (B y x) (U6 x) (exists ((y V)) (and (B x y) (U7 y) (forall ((x V)) (=> (B y x) (U8 x) (exists ((y V)) (and (B x y) (U9 y) (forall ((x V)) (=> (B y x) (U10 x) (exists ((y V)) (and (B x y) (U11 y) (forall ((x V)) (=> (B y x) (U12 x) (exists ((y V)) (and (B x y) (U13 y) (forall ((x V)) (=> (B y x) (U14 x) (exists ((y V)) (and (B x y) (U15 y)))))))))))))))))))))))))))))))))
(exists ((x V)) (U0 x))
(forall ((x V)) (exists ((y V)) (B x y)))(forall ((x V) (y V)) (=> (and (B x y) (U0 x)) (U1 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U1 x)) (U2 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U2 x)) (U3 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U3 x)) (U4 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U4 x)) (U5 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U5 x)) (U6 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U6 x)) (U7 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U7 x)) (U8 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U8 x)) (U9 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U9 x)) (U10 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U10 x)) (U11 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U11 x)) (U12 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U12 x)) (U13 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U13 x)) (U14 y)))
(forall ((x V) (y V)) (=> (and (B x y) (U14 x)) (U15 y)))
))
(check-sat)
(get-model)