#!/usr/bin/python3

from z3 import *

s=Solver()

vals=[Int("sentence_%d_is_false" % i) for i in range(10)]

for val in vals:
    s.add(Or(val==0, val==1))

s.add(vals[0]==If(Sum(vals)==1,  0, 1))
s.add(vals[1]==If(Sum(vals)==2,  0, 1))
s.add(vals[2]==If(Sum(vals)==3,  0, 1))
s.add(vals[3]==If(Sum(vals)==4,  0, 1))
s.add(vals[4]==If(Sum(vals)==5,  0, 1))
s.add(vals[5]==If(Sum(vals)==6,  0, 1))
s.add(vals[6]==If(Sum(vals)==7,  0, 1))
s.add(vals[7]==If(Sum(vals)==8,  0, 1))
s.add(vals[8]==If(Sum(vals)==9,  0, 1))
s.add(vals[9]==If(Sum(vals)==10, 0, 1))

result=s.check()
print (result)
print (s.model())