from z3 import *

b1 = Bool('b1')
b2 = Bool('b2')
b3 = Bool('b3')
b4 = Bool('b4')
b5 = Bool('b5')
b6 = Bool('b6')
b7 = Bool('b7')
b8 = Bool('b8')

s = Solver()
s.add((b1 + b2 + b5 + b7)%2 = 0)
s.add((b2 + b3 + b6)%2 = 1)
s.add((b1 + b3 + b4 + b7)%2 = 1)
s.add((b1 + b2 + b4 + b5)%2 = 1)
s.add((b1 + b2 + b3 + b5 + b6)%2 = 1)
s.add((b1 + b2 + b3 + b4 + b6 + b7)%2 = 1)
s.add((b1 + b2 + b3 + b4 + b5 + b7)%2 = 1)
s.add((b1 + b2 + b3 + b4 + b5 + b6)%2 = 1)
s.add((b1 + b2 + b3 + b4 + b5 + b6 + b7)%2 = 0)
s.add((b2 + b3 + b4 + b5 + b6 + b7)%2 = 0)

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