solve.py

#!/usr/bin/env python3

from z3 import Int, Solver

a = [Int(f'a{i}') for i in range(40)]
s = Solver()

s.add(a[2] * a[8] == 2600)
s.add(a[35] - a[39] == -1)
s.add(a[19] + a[37] == 149)
s.add(a[20] + a[25] == 200)
s.add(a[4] - a[7] == -49)
s.add(a[15] + a[24] - a[27] == 54)
s.add(a[18] + a[21] + a[24] - a[27] == 106)
s.add(a[30] + a[31] - a[32] + a[33] - a[34] == 48)
s.add(a[0] + a[28] == 153)
s.add(a[0] - a[6] == -3)
s.add(a[3] + a[9] == 99)
s.add(a[3] * a[9] * a[12] == 134640)
s.add(a[5] - a[23] == 47)
s.add(a[29] + a[36] == 148)
s.add(a[10] - a[38] == 50)
s.add(a[11] + a[26] == 147)
s.add(a[0] + a[22] == 99)
s.add(a[4] + a[39] == 103)
s.add(a[7] + a[25] == 199)
s.add(a[28] - a[37] == 1)
s.add(a[11] + a[29] == 146)
s.add(a[5] - a[20] == 2)
s.add(a[8] + a[38] == 102)
s.add(a[19] - a[35] == -5)
s.add(a[19] + a[35] == 101)
s.add(a[23] + a[36] == 105)
s.add(a[22] - a[26] == -50)
s.add(a[13] + a[19] == 98)
s.add(a[5] - a[30] == 4)
s.add(a[17] - a[26] == -50)
s.add(a[1] - a[35] == -2)
s.add(a[11] - a[27] == -3)
s.add(a[32] + a[39] == 156)
s.add(a[8] + a[14] == 99)
s.add(a[10] - a[16] == 2)
s.add(a[7] + a[31] == 150)
s.add(a[4] - a[33] == -5)
s.add(a[2] - a[34] == -1)
s.add(a[15] + a[20] == 154)
s.add(a[18] - a[37] == -45)
s.add(a[1] + a[13] + a[14] + a[16] + a[17] == 298)
s.add(a[21] - a[38] == -1)
s.add(a[0] - a[24] == 0)
s.add(a[19] + a[25] - a[36] == 98)
s.add(-a[0] + a[28] + a[29] == 148)
s.add(-a[4] + a[22] + a[23] == 53)
s.add(a[2] + a[5] - a[35] == 100)
s.add(a[7] + a[20] - a[29] == 100)
s.add(a[10] + a[11] - a[26] == 53)
s.add(a[8] + a[23] - a[38] == 52)
s.add(a[22] + a[37] - a[39] == 95)
s.add(a[25] + a[28] - a[36] == 152)

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

flag = ''

for i in a:
    flag += chr(model[i].as_long())

print(flag)