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)

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

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