#SAT 

#size = 20 # < 1 sec
size = 5
    
txt0 = "(declare-sort V 0)\n"
txt0 += "(declare-fun U (V) Bool)"
txt0 += "(assert \n"  



txt1 = """(U x)"""
    
   
   
for i in range(size):
  txt1 = "(exists ((x)) " + txt1 + ")"
    


txt = txt0 + txt1 + ")(check-sat)\n(get-model)\n"

print txt