# UNSAT

size = 2 # 2 min

txt0 = "(declare-sort V 0)\n"
txt0 += "(declare-fun B (V V) Bool)"
txt0 += "(declare-fun A (V) Bool)"

for i in range(size):
  txt0 += "(declare-fun U" + str(i) + " (V) Bool)\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)) (=> (U" + str(size-1) +" x) (not (A x))))\n"

txt7 = "(forall ((x V) (y V)) (=> (B x y) (=> (A x) (A y))))\n" 



txt = txt0 + "(and \n" + txt1 + txt2 + txt2p5 + txt3 + txt4 + txt4p5 + txt5 + txt6 + txt7 + "))\n(check-sat)\n(get-model)\n"



print txt