from z3 import *
flag = [Int("flag_%d" % i) for i in range(16)]
s = Solver()
s.add(flag[1] == 3)
s.add(flag[2] == 1)
s.add(flag[4] == 1)
s.add(flag[7] == 3)
s.add(flag[8] == 2)
s.add(flag[10] == 3)
s.add(flag[11] == 4)
s.add(flag[13] == 4)
s.add(flag[14] == 2)
s.add(flag[3] + flag[2] + flag[1] + flag[0] == 10)
s.add(flag[7] + flag[6] + flag[5] + flag[4] == 10)
s.add(flag[11] + flag[10] + flag[9] + flag[8] == 10)
s.add(flag[15] + flag[14] + flag[13] + flag[12] == 10)
s.add(flag[12] + flag[8] + flag[4] + flag[0] == 10)
s.add(flag[13] + flag[9] + flag[5] + flag[1] == 10)
s.add(flag[14] + flag[10] + flag[6] + flag[2] == 10)
s.add(flag[15] + flag[11] + flag[7] + flag[3] == 10)
s.add(flag[5] + flag[1] + flag[0] + flag[4] == 10)
s.add(flag[7] + flag[6] + flag[2] + flag[3] == 10)
s.add(flag[13] + flag[12] + flag[9] + flag[8] == 10)
s.add(flag[15] + flag[14] + flag[11] + flag[10] == 10)
assert s.check() == sat
print("OK")
m = s.model()
c = [m[flag[i]].as_long() for i in range(16)]
for i in [0, 3, 5, 6, 9, 12, 15]:
print(c[i], end="")
