from z3 import *

b1 = BitVec('b1', 1)
b2 = BitVec('b2', 1)
b3 = BitVec('b3', 1)
b4 = BitVec('b4', 1)
b5 = BitVec('b5', 1)
b6 = BitVec('b6', 1)
b7 = BitVec('b7', 1)
b8 = BitVec('b8', 1)
b9 = BitVec('b9', 1)

s = Solver()
s.add(b1 ^ b2 ^ b5 ^ b7 ^ b9 == 1)
s.add(b1 ^ b2 ^ b3 ^ b6 ^ b8 == 1)
s.add(b1 ^ b2 ^ b3 ^ b4 ^ b7 ^ b9 == 1)
s.add(b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b8 == 1)
s.add(b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b9 == 1)
s.add(b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 == 1)
s.add(b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 == 0)
s.add(b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9 == 0)
s.add(b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9 == 1)
s.add(b1 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9 == 1)

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