#SAT
#size = 2 < 1 sec
size = 10 # 9 sec
txt0 = "(declare-sort V 0)\n"
txt0 += "(declare-fun U (V) Bool)\n"
txt0 += "(declare-fun B (V V) Bool)\n"
txt0 += "(assert (and \n"
txt1 = "(forall ((x V)) (=> (U x) "
for i in range(size):
txt1 += "(exists ((y V)) (and (B x y) (not (U y)) (forall ((x V)) (=> (B y x) (and (not (U x)) "
txt1 += "(exists ((y V)) (and (B x y) (U y)))"
for i in range(size):
txt1 += ")))))"
txt1 += "))\n"
txt2 = "(exists ((x V)) (U x))\n"
txt3 = "(forall ((x V)) (exists ((y V)) (B x y)))"
txt = txt0 + txt1 + txt2 + txt3 + "))\n(check-sat)\n(get-model)\n"
print txt