#SAT
#size = 4 # 5 sec
size = 2
txt0 = "(declare-sort V 0)\n"
txt0 += "(declare-fun U (V) Bool)\n"
txt0 += "(declare-fun B (V V) Bool)\n"
for i in range(size*2+2):
txt0 += "(declare-fun U" + str(i) + " (V) Bool)\n"
txt0 += "(assert (and \n"
for i in range(size*2+2):
for j in range(size*2+2):
if (i != j):
txt0 += "(forall ((x V)) (=> (U" + str(i) + " x) (not (U" + str(j) + " x))))\n"
txt1 = "(forall ((x V)) (=> (U0 x) "
for i in range(size):
txt1 += "(exists ((y V)) (and (B x y) (U" + str(2*i+1) + " y) (forall ((x V)) (=> (B y x) (and (U" + str(2*i+2) + " x) "
txt1 += "(exists ((y V)) (and (B x y) (U" + str(2*size+1) + " y)))"
for i in range(size):
txt1 += ")))))"
txt1 += "))\n"
txt2 = "(exists ((x V)) (U0 x))\n"
txt3 = "(forall ((x V)) (exists ((y V)) (B x y)))"
txt4 = ""
for i in range(2*size+1):
txt4 += "(forall ((x V) (y V)) (=> (and (B x y) (U" + str(i) + " x)) (U" + str(i+1) + " y)))\n"
txt = txt0 + txt1 + txt2 + txt3 + txt4 + "))\n(check-sat)\n(get-model)\n"
print txt