from z3 import Solver, BitVec, sat
import itertools


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

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

foreach_idx = itertools.batched(conds, n=7)
foreach_idx = enumerate(foreach_idx)
flagbytes = []


for idx, constraints in foreach_idx:
    all_permutations = itertools.permutations(constraints, 6)
    for permutation in all_permutations:
        s = Solver()
        for cosntraint in permutation:
            s.add(permutation)
        if s.check() == sat:
            m = s.model()
            flagbyte = m[inp[idx]].as_long()  # pyright: ignore[reportAttributeAccessIssue, reportOptionalMemberAccess]
            flagbytes += [flagbyte]
            print("got 'er: %d" % idx)
            break

# __import__("ipdb").set_trace()

flagbytes = map(lambda x: x ^ 0xFF, flagbytes)
flagbytes = bytes(flagbytes)
flagbytes = flagbytes.decode()
print(flagbytes)