#!/usr/bin/python3

from z3 import *

s=Solver()

TOTAL=10

# not booleans, beacause we will sum them:
vals=[Int("sentence_%d_is_false" % i) for i in range(TOTAL)]

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

for i in range(TOTAL):
    s.add(vals[i]==If(Sum(vals)==i+1,  0, 1))

print (s.check())
print (s.model())