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