from z3 import *

s = Solver()

inp = [BitVec(f"flag_{i}", 8) for i in range(0, 49)]

s.add((inp[13] >> 2) & 1 == 0)
s.add((inp[41] >> 4) & 0xf < 14)
s.add((inp[5] >> 4) & 0xf < 18)
s.add((inp[4] >> 3) & 1 == 1)
s.add((inp[32] >> 0) & 1 == 0)
s.add((inp[16] >> 1) & 1 == 0)
s.add((inp[19] >> 4) & 0xf == 31)
s.add((inp[14] >> 3) & 1 == 0)
s.add((inp[44] >> 3) & 1 == 1)
s.add((inp[16] >> 3) & 1 == 1)
s.add((inp[3] >> 4) & 0xf == 8)
s.add((inp[36] >> 0) & 1 == 1)
s.add((inp[7] >> 3) & 1 == 0)
s.add((inp[29] >> 0) & 1 == 1)
s.add((inp[38] >> 4) & 0xf < 12)
s.add((inp[44] >> 2) & 1 == 0)
s.add((inp[31] >> 1) & 1 == 0)
s.add((inp[19] >> 1) & 1 == 1)
s.add((inp[32] >> 4) & 0xf == 9)
s.add((inp[35] >> 4) & 0xf == 10)
s.add((inp[20] >> 1) & 1 == 0)
s.add((inp[30] >> 4) & 0xf < 11)
s.add((inp[48] >> 2) & 1 == 0)
s.add((inp[47] >> 4) & 0xf == 8)
s.add((inp[18] >> 2) & 1 == 0)
s.add((inp[5] >> 4) & 0xf == 72)
s.add((inp[24] >> 4) & 0xf < 15)
s.add((inp[30] >> 3) & 1 == 1)
s.add((inp[42] >> 0) & 1 == 0)
s.add((inp[2] >> 0) & 1 == 0)
s.add((inp[28] >> 1) & 1 == 0)
s.add((inp[22] >> 0) & 1 == 0)
s.add((inp[19] >> 4) & 0xf < 16)
s.add((inp[7] >> 4) & 0xf < 11)
s.add((inp[32] >> 4) & 0xf == 77)
s.add((inp[26] >> 4) & 0xf < 19)
s.add((inp[36] >> 4) & 0xf < 13)
s.add((inp[21] >> 0) & 1 == 0)
s.add((inp[29] >> 4) & 0xf < 13)
s.add((inp[34] >> 3) & 1 == 1)
s.add((inp[46] >> 4) & 0xf == 8)
s.add((inp[27] >> 4) & 0xf == 8)
s.add((inp[27] >> 2) & 1 == 1)
s.add((inp[15] >> 4) & 0xf < 15)
s.add((inp[11] >> 1) & 1 == 1)
s.add((inp[0] >> 4) & 0xf == 9)
s.add((inp[25] >> 1) & 1 == 1)
s.add((inp[38] >> 4) & 0xf == 87)
s.add((inp[48] >> 0) & 1 == 0)
s.add((inp[17] >> 2) & 1 == 0)
s.add((inp[18] >> 4) & 0xf < 10)
s.add((inp[3] >> 2) & 1 == 0)
s.add((inp[8] >> 3) & 1 == 0)
s.add((inp[47] >> 1) & 1 == 1)
s.add((inp[6] >> 1) & 1 == 1)
s.add((inp[41] >> 2) & 1 == 0)
s.add((inp[17] >> 0) & 1 == 0)
s.add((inp[42] >> 4) & 0xf == 47)
s.add((inp[10] >> 4) & 0xf == 10)
s.add((inp[0] >> 3) & 1 == 0)
s.add((inp[23] >> 3) & 1 == 0)
s.add((inp[31] >> 4) & 0xf == 9)
s.add((inp[21] >> 4) & 0xf < 20)
s.add((inp[23] >> 2) & 1 == 0)
s.add((inp[8] >> 4) & 0xf == 83)
s.add((inp[36] >> 3) & 1 == 1)
s.add((inp[28] >> 4) & 0xf == 25)
s.add((inp[37] >> 4) & 0xf == 96)
s.add((inp[35] >> 4) & 0xf < 14)
s.add((inp[36] >> 1) & 1 == 1)
s.add((inp[43] >> 4) & 0xf < 15)
s.add((inp[34] >> 4) & 0xf < 15)
s.add((inp[28] >> 4) & 0xf == 10)
s.add((inp[26] >> 1) & 1 == 1)
s.add((inp[28] >> 0) & 1 == 0)
s.add((inp[30] >> 2) & 1 == 0)
s.add((inp[9] >> 4) & 0xf == 21)
s.add((inp[4] >> 1) & 1 == 0)
s.add((inp[3] >> 4) & 0xf == 104)
s.add((inp[46] >> 0) & 1 == 1)
s.add((inp[14] >> 2) & 1 == 0)
s.add((inp[25] >> 3) & 1 == 1)
s.add((inp[14] >> 4) & 0xf < 11)
s.add((inp[35] >> 4) & 0xf == 105)
s.add((inp[9] >> 2) & 1 == 0)
s.add((inp[3] >> 4) & 0xf < 10)
s.add((inp[44] >> 0) & 1 == 0)
s.add((inp[2] >> 4) & 0xf == 36)
s.add((inp[5] >> 2) & 1 == 1)
s.add((inp[16] >> 2) & 1 == 1)
s.add((inp[9] >> 1) & 1 == 1)
s.add((inp[2] >> 3) & 1 == 1)
s.add((inp[22] >> 2) & 1 == 0)
s.add((inp[34] >> 0) & 1 == 0)
s.add((inp[29] >> 4) & 0xf == 9)
s.add((inp[32] >> 1) & 1 == 0)
s.add((inp[46] >> 2) & 1 == 0)
s.add((inp[39] >> 1) & 1 == 0)
s.add((inp[29] >> 3) & 1 == 1)
s.add((inp[4] >> 2) & 1 == 0)
s.add((inp[4] >> 4) & 0xf == 9)
s.add((inp[16] >> 4) & 0xf < 13)
s.add((inp[45] >> 2) & 1 == 1)
s.add((inp[30] >> 4) & 0xf == 9)
s.add((inp[13] >> 4) & 0xf == 8)
s.add((inp[8] >> 2) & 1 == 0)
s.add((inp[0] >> 4) & 0xf < 11)
s.add((inp[7] >> 1) & 1 == 1)
s.add((inp[41] >> 4) & 0xf == 9)
s.add((inp[42] >> 1) & 1 == 1)
s.add((inp[27] >> 0) & 1 == 0)
s.add((inp[27] >> 1) & 1 == 1)
s.add((inp[45] >> 4) & 0xf == 9)
s.add((inp[6] >> 4) & 0xf == 21)
s.add((inp[40] >> 2) & 1 == 1)
s.add((inp[8] >> 4) & 0xf < 13)
s.add((inp[40] >> 0) & 1 == 0)
s.add((inp[43] >> 2) & 1 == 1)
s.add((inp[5] >> 1) & 1 == 0)
s.add((inp[17] >> 4) & 0xf == 9)
s.add((inp[15] >> 2) & 1 == 1)
s.add((inp[36] >> 4) & 0xf == 107)
s.add((inp[15] >> 0) & 1 == 1)
s.add((inp[9] >> 3) & 1 == 1)
s.add((inp[41] >> 3) & 1 == 0)
s.add((inp[6] >> 4) & 0xf < 9)
s.add((inp[11] >> 2) & 1 == 1)
s.add((inp[23] >> 0) & 1 == 0)
s.add((inp[46] >> 3) & 1 == 1)
s.add((inp[41] >> 0) & 1 == 1)
s.add((inp[27] >> 4) & 0xf < 18)
s.add((inp[43] >> 1) & 1 == 1)
s.add((inp[16] >> 0) & 1 == 1)
s.add((inp[14] >> 1) & 1 == 0)
s.add((inp[5] >> 4) & 0xf == 8)
s.add((inp[42] >> 4) & 0xf < 18)
s.add((inp[48] >> 4) & 0xf < 14)
s.add((inp[11] >> 4) & 0xf == 72)
s.add((inp[21] >> 1) & 1 == 0)
s.add((inp[8] >> 0) & 1 == 0)
s.add((inp[43] >> 4) & 0xf == 26)
s.add((inp[30] >> 4) & 0xf == 48)
s.add((inp[26] >> 3) & 1 == 0)
s.add((inp[48] >> 1) & 1 == 1)
s.add((inp[18] >> 1) & 1 == 0)
s.add((inp[38] >> 2) & 1 == 0)
s.add((inp[43] >> 3) & 1 == 0)
s.add((inp[0] >> 2) & 1 == 1)
s.add((inp[19] >> 3) & 1 == 1)
s.add((inp[38] >> 0) & 1 == 0)
s.add((inp[21] >> 4) & 0xf == 53)
s.add((inp[6] >> 4) & 0xf == 8)
s.add((inp[8] >> 1) & 1 == 0)
s.add((inp[0] >> 0) & 1 == 0)
s.add((inp[40] >> 1) & 1 == 1)
s.add((inp[20] >> 4) & 0xf == 9)
s.add((inp[18] >> 0) & 1 == 1)
s.add((inp[17] >> 4) & 0xf < 13)
s.add((inp[2] >> 2) & 1 == 1)
s.add((inp[44] >> 4) & 0xf == 9)
s.add((inp[42] >> 3) & 1 == 0)
s.add((inp[25] >> 4) & 0xf == 55)
s.add((inp[10] >> 4) & 0xf < 19)
s.add((inp[45] >> 4) & 0xf < 15)
s.add((inp[44] >> 4) & 0xf < 13)
s.add((inp[14] >> 4) & 0xf == 40)
s.add((inp[47] >> 4) & 0xf < 12)
s.add((inp[0] >> 1) & 1 == 1)
s.add((inp[17] >> 4) & 0xf == 62)
s.add((inp[40] >> 4) & 0xf == 67)
s.add((inp[3] >> 1) & 1 == 1)
s.add((inp[37] >> 4) & 0xf == 9)
s.add((inp[34] >> 1) & 1 == 1)
s.add((inp[38] >> 4) & 0xf == 9)
s.add((inp[13] >> 1) & 1 == 1)
s.add((inp[33] >> 4) & 0xf == 8)
s.add((inp[0] >> 4) & 0xf == 22)
s.add((inp[28] >> 2) & 1 == 0)
s.add((inp[36] >> 2) & 1 == 0)
s.add((inp[33] >> 3) & 1 == 1)
s.add((inp[12] >> 4) & 0xf == 75)
s.add((inp[33] >> 2) & 1 == 1)
s.add((inp[29] >> 1) & 1 == 0)
s.add((inp[24] >> 0) & 1 == 1)
s.add((inp[31] >> 4) & 0xf < 11)
s.add((inp[23] >> 4) & 0xf == 34)
s.add((inp[20] >> 4) & 0xf < 15)
s.add((inp[18] >> 4) & 0xf == 8)
s.add((inp[44] >> 4) & 0xf == 23)
s.add((inp[33] >> 0) & 1 == 1)
s.add((inp[21] >> 4) & 0xf == 10)
s.add((inp[12] >> 2) & 1 == 1)
s.add((inp[35] >> 1) & 1 == 0)
s.add((inp[44] >> 1) & 1 == 0)
s.add((inp[40] >> 4) & 0xf == 9)
s.add((inp[9] >> 4) & 0xf == 8)
s.add((inp[9] >> 0) & 1 == 0)
s.add((inp[40] >> 3) & 1 == 1)
s.add((inp[35] >> 0) & 1 == 0)
s.add((inp[27] >> 4) & 0xf == 42)
s.add((inp[12] >> 4) & 0xf == 8)
s.add((inp[26] >> 2) & 1 == 1)
s.add((inp[46] >> 1) & 1 == 1)
s.add((inp[16] >> 4) & 0xf == 8)
s.add((inp[47] >> 2) & 1 == 1)
s.add((inp[39] >> 4) & 0xf < 14)
s.add((inp[26] >> 4) & 0xf == 9)
s.add((inp[47] >> 3) & 1 == 0)
s.add((inp[15] >> 3) & 1 == 1)
s.add((inp[41] >> 1) & 1 == 1)
s.add((inp[7] >> 0) & 1 == 1)
s.add((inp[45] >> 1) & 1 == 1)
s.add((inp[45] >> 3) & 1 == 0)
s.add((inp[48] >> 3) & 1 == 0)
s.add((inp[14] >> 4) & 0xf == 10)
s.add((inp[11] >> 4) & 0xf == 9)
s.add((inp[12] >> 4) & 0xf < 12)
s.add((inp[32] >> 2) & 1 == 0)
s.add((inp[20] >> 3) & 1 == 0)
s.add((inp[29] >> 4) & 0xf == 56)
s.add((inp[6] >> 3) & 1 == 1)
s.add((inp[19] >> 0) & 1 == 0)
s.add((inp[39] >> 0) & 1 == 0)
s.add((inp[10] >> 0) & 1 == 0)
s.add((inp[15] >> 4) & 0xf == 8)
s.add((inp[23] >> 4) & 0xf < 18)
s.add((inp[1] >> 4) & 0xf == 9)
s.add((inp[19] >> 2) & 1 == 0)
s.add((inp[7] >> 2) & 1 == 1)
s.add((inp[45] >> 4) & 0xf == 70)
s.add((inp[37] >> 2) & 1 == 1)
s.add((inp[22] >> 3) & 1 == 1)
s.add((inp[5] >> 0) & 1 == 0)
s.add((inp[28] >> 3) & 1 == 0)
s.add((inp[21] >> 2) & 1 == 0)
s.add((inp[33] >> 4) & 0xf == 38)
s.add((inp[46] >> 4) & 0xf < 13)
s.add((inp[39] >> 4) & 0xf == 10)
s.add((inp[48] >> 4) & 0xf == 8)
s.add((inp[3] >> 3) & 1 == 1)
s.add((inp[21] >> 3) & 1 == 0)
s.add((inp[16] >> 4) & 0xf == 37)
s.add((inp[30] >> 1) & 1 == 1)
s.add((inp[26] >> 0) & 1 == 1)
s.add((inp[37] >> 0) & 1 == 1)
s.add((inp[7] >> 4) & 0xf == 9)
s.add((inp[22] >> 4) & 0xf == 8)
s.add((inp[3] >> 0) & 1 == 1)
s.add((inp[2] >> 1) & 1 == 0)
s.add((inp[29] >> 2) & 1 == 1)
s.add((inp[12] >> 3) & 1 == 1)
s.add((inp[13] >> 3) & 1 == 1)
s.add((inp[35] >> 2) & 1 == 0)
s.add((inp[20] >> 0) & 1 == 1)
s.add((inp[38] >> 3) & 1 == 1)
s.add((inp[1] >> 1) & 1 == 0)
s.add((inp[17] >> 3) & 1 == 0)
s.add((inp[7] >> 4) & 0xf == 46)
s.add((inp[31] >> 2) & 1 == 0)
s.add((inp[41] >> 4) & 0xf == 100)
s.add((inp[1] >> 4) & 0xf < 14)
s.add((inp[2] >> 4) & 0xf == 9)
s.add((inp[33] >> 1) & 1 == 0)
s.add((inp[46] >> 4) & 0xf == 26)
s.add((inp[24] >> 3) & 1 == 1)
s.add((inp[43] >> 0) & 1 == 0)
s.add((inp[43] >> 4) & 0xf == 9)
s.add((inp[25] >> 4) & 0xf == 8)
s.add((inp[20] >> 2) & 1 == 0)
s.add((inp[20] >> 4) & 0xf == 63)
s.add((inp[48] >> 4) & 0xf == 45)
s.add((inp[17] >> 1) & 1 == 0)
s.add((inp[34] >> 2) & 1 == 0)
s.add((inp[40] >> 4) & 0xf < 17)
s.add((inp[39] >> 4) & 0xf == 40)
s.add((inp[32] >> 3) & 1 == 0)
s.add((inp[47] >> 4) & 0xf == 90)
s.add((inp[1] >> 2) & 1 == 0)
s.add((inp[47] >> 0) & 1 == 0)
s.add((inp[4] >> 4) & 0xf == 30)
s.add((inp[18] >> 4) & 0xf == 29)
s.add((inp[35] >> 3) & 1 == 0)
s.add((inp[1] >> 4) & 0xf == 50)
s.add((inp[2] >> 4) & 0xf < 13)
s.add((inp[10] >> 4) & 0xf == 45)
s.add((inp[37] >> 3) & 1 == 0)
s.add((inp[22] >> 1) & 1 == 0)
s.add((inp[39] >> 3) & 1 == 0)
s.add((inp[31] >> 4) & 0xf == 67)
s.add((inp[11] >> 3) & 1 == 1)
s.add((inp[4] >> 0) & 1 == 1)
s.add((inp[28] >> 4) & 0xf < 12)
s.add((inp[32] >> 4) & 0xf < 14)
s.add((inp[25] >> 2) & 1 == 0)
s.add((inp[1] >> 0) & 1 == 1)
s.add((inp[23] >> 1) & 1 == 0)
s.add((inp[26] >> 4) & 0xf == 65)
s.add((inp[25] >> 4) & 0xf < 17)
s.add((inp[45] >> 0) & 1 == 1)
s.add((inp[6] >> 2) & 1 == 0)
s.add((inp[10] >> 1) & 1 == 0)
s.add((inp[14] >> 0) & 1 == 0)
s.add((inp[34] >> 4) & 0xf == 64)
s.add((inp[13] >> 0) & 1 == 1)
s.add((inp[10] >> 3) & 1 == 0)
s.add((inp[19] >> 4) & 0xf == 9)
s.add((inp[22] >> 4) & 0xf == 76)
s.add((inp[23] >> 4) & 0xf == 9)
s.add((inp[37] >> 1) & 1 == 1)
s.add((inp[31] >> 3) & 1 == 1)
s.add((inp[12] >> 1) & 1 == 0)
s.add((inp[4] >> 4) & 0xf < 18)
s.add((inp[10] >> 2) & 1 == 0)
s.add((inp[30] >> 0) & 1 == 0)
s.add((inp[27] >> 3) & 1 == 0)
s.add((inp[13] >> 4) & 0xf == 53)
s.add((inp[11] >> 4) & 0xf < 18)
s.add((inp[38] >> 1) & 1 == 1)
s.add((inp[33] >> 4) & 0xf < 14)
s.add((inp[42] >> 2) & 1 == 0)
s.add((inp[22] >> 4) & 0xf < 9)
s.add((inp[13] >> 4) & 0xf < 18)
s.add((inp[39] >> 2) & 1 == 0)
s.add((inp[37] >> 4) & 0xf < 11)
s.add((inp[24] >> 4) & 0xf == 8)
s.add((inp[12] >> 0) & 1 == 1)
s.add((inp[8] >> 4) & 0xf == 9)
s.add((inp[9] >> 4) & 0xf < 18)
s.add((inp[15] >> 1) & 1 == 1)
s.add((inp[31] >> 0) & 1 == 1)
s.add((inp[24] >> 2) & 1 == 1)
s.add((inp[18] >> 3) & 1 == 1)
s.add((inp[42] >> 4) & 0xf == 9)
s.add((inp[1] >> 3) & 1 == 0)
s.add((inp[11] >> 0) & 1 == 0)
s.add((inp[24] >> 4) & 0xf == 28)
s.add((inp[24] >> 1) & 1 == 0)
s.add((inp[25] >> 0) & 1 == 1)
s.add((inp[5] >> 3) & 1 == 0)
s.add((inp[15] >> 4) & 0xf == 61)
s.add((inp[36] >> 4) & 0xf == 8)
s.add((inp[6] >> 0) & 1 == 1)
s.add((inp[34] >> 4) & 0xf == 9)

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