# SAT on even sizes
# UNSAT on odd sizes
size = 2
txt0 = "(declare-sort V 0)\n"
txt0 += "(declare-fun B (V V) Bool)\n"
txt0 += "(declare-fun A (V) Bool)\n"
for i in range(size):
txt0 += "(declare-fun U" + str(i) + " (V) Bool)\n"
txt0 += "\n"
txt0 += "(assert \n"
txt1 = ""
for i in range(size):
for j in range(size):
if (i != j):
txt1 += "(forall ((x V)) (=> (U" + str(i) + " x) (not (U" + str(j) + " x))))\n"
txt2 = ""
for i in range(size):
txt2 += "(exists ((x V)) (U" + str(i) + " x))\n "
txt2p5 = ""
#for i in range(size):
#txt2p5 += "(forall ((x V) (y V)) (=> (not (= x y)) (not (and (U" + str(i) + " x) (U" + str(i) + " y)))))\n"
txt3 = ""
#txt3 = "(and "
#for i in range(size-1):
#txt3 += "(forall ((x V) (y V)) (=> (and (U" + str(i) + " x) (U" + str(i+1) + " y)) (B x y)))\n"
#txt3 += "(forall ((x V) (y V)) (=> (and (U" + str(size-1) + " x) (U0 y)) (B x y)))"
#txt3 += ")\n"
txt4 = "(and "
for i in range(size):
for j in range(size):
if ((j != i+1) and (j != 0 or i != size-1)):
txt4 += "(forall ((x V) (y V)) (=> (and (U" + str(i) + " x) (U" + str(j) + " y)) (not (B x y))))\n"
txt4 += ")\n"
txt4p5 = "(forall ((x V)) (exists ((y V)) (and (B x y) (or "
for i in range(size):
txt4p5 += "(U" + str(i) + " y) "
txt4p5 += ")\n"
txt5 = "(forall ((x V)) (=> (U0 x) (A x)))\n"
txt6 = "(forall ((x V) (y V)) (=> (B x y) (and (=> (A x) (not (A y))) (=> (not (A x)) (A y)))))\n"
txt = txt0 + "(and \n" + txt1 + txt2 + txt2p5 + txt3 + txt4 + txt4p5 + txt5 + txt6 + "))\n\n(check-sat)\n(get-model)\n"
print txt