```
from z3 import *

s = []
for i in range(42):
byte = BitVec(f"{i}", 8)
s.append(byte)

solver = Solver()

solver.add( s[7] + s[13] + s[8] == 269)
solver.add(s[0] - s[1] + s[14] + s[0] == 165)
solver.add(s[34] + s[16] * s[21] + s[38] == 9482)
solver.add(s[41] + s[8] * s[6] + s[23] == 5500)
solver.add(s[11] * s[4] * s[18] + s[19] == 639710)
solver.add(s[23] + s[33] * s[34] == 6403)
solver.add(s[18] * s[14] - s[33] == 5072)
solver.add(s[24] - s[39] - s[30] - s[22] == -110)
solver.add(s[10] + s[30] - s[19] + s[1] == 110)
solver.add(s[15] - s[20] - s[41] == -169)
solver.add(s[15] * s[35] - s[41] * s[8] == -10231)
solver.add(s[36] + s[31] * s[11] - s[32] == 8428)
solver.add( s[29] + s[25] + s[40] == 289)
solver.add(s[7] - s[12] + s[24] == 100)
solver.add(s[21] * s[30] - s[6] == 9262)
solver.add(s[38] * s[33] * s[3] == 480244)
solver.add(s[20] - s[31] * s[0] - s[2] == -5954)
solver.add(s[27] + s[12] * s[21] == 5095)
solver.add(s[6] + s[11] * s[8] - s[8] == 10938)
solver.add(s[34] - s[5] + s[7] * s[24] == 5014)
solver.add(s[40] - s[18] - s[2] == -83)
solver.add(s[11] - s[31] + s[9] * s[24] == 10114 )
solver.add(s[41] == 125)
solver.add(s[28] + s[30] - s[3] * s[16] == -6543)
solver.add(s[18] * s[25] - s[11] == 5828 )
solver.add( s[8] * s[9] * s[11] == 1089000 )
solver.add( s[3] * s[25] - s[29] * s[6] == 2286 )
solver.add( s[36] - s[7] * s[33] == -3642 )
solver.add( s[32] - s[1] + s[20] == 73 )
solver.add( s[39] + s[5] * s[4] == 8307 )
solver.add( s[0] * s[39] * s[8] == 515460 )
solver.add( s[12] - s[13] + s[31] == 25 )
solver.add( s[18] + s[10] + s[41] + s[41] == 351 )
solver.add( s[7] + s[14] * s[1] + s[22] == 7624 )
solver.add( s[27] + s[24] * s[18] + s[14] == 5500 )
solver.add( s[20] - s[41] * s[6] + s[18] == -5853 )
solver.add( s[33] - s[2] - s[25] * s[31] == -9585 )
solver.add( s[18] * s[11] * s[37] == 353600 )
solver.add( s[17] + s[8] + s[7] - s[39] == 192 )
solver.add( s[11] - s[35] - s[9] * s[31] == -8285 )
solver.add( s[23] - s[29] + s[39] == 40 )
solver.add( s[28] + s[10] * s[25] * s[20] == 530777 )
solver.add( s[32] * s[29] * s[3] == 463914 )
solver.add( s[32] - s[22] + s[30] == 98 )
solver.add( s[0] - s[13] + s[40] - s[38] == -74 )
solver.add( s[17] + s[21] - s[38] == 108 )
solver.add( s[0] - s[41] * s[23] == -11804 )
solver.add( s[2] * s[29] * s[27] == 997645 )
solver.add( s[25] - s[19] * s[35] == -7476 )
solver.add( s[16] - s[19] * s[7] == -5295 )
solver.add( s[33] + s[12] * s[26] + s[22] == 2728 )
solver.add( s[41] + s[24] + s[32] == 281 )
solver.add( s[23] * s[31] * s[14] == 790020 )
solver.add( s[35] - s[35] * s[6] - s[14] == -3342 )
solver.add( s[31] + s[40] - s[17] * s[25] == -11148 )
solver.add( s[36] * s[18] + s[13] * s[19] == 16364 )
solver.add( s[40] - s[5] + s[2] * s[18] == 4407 )
solver.add( s[21] - s[25] + s[3] == 55 )
solver.add( s[14] + s[14] + s[13] - s[2] == 223 )
solver.add( s[36] * s[35] - s[5] * s[29] == -2449 )
solver.add( s[41] - s[39] + s[1] == 135 )
solver.add( s[35] - s[0] * s[35] + s[0] == -4759 )
solver.add( s[8] - s[10] * s[21] - s[31] == -4776 )
solver.add( s[29] - s[24] + s[28] == 126 )
solver.add( s[0] * s[10] - s[32] - s[8] == 3315 )
solver.add( s[28] * s[32] + s[41] == 5903 )
solver.add( s[37] - s[24] + s[32] == 20 )
solver.add( s[20] * s[10] - s[15] + s[31] == 4688 )
solver.add( s[36] - s[9] - s[18] * s[18] == -2721 )
solver.add( s[9] * s[7] + s[16] * s[30] == 13876 )
solver.add( s[18] + s[34] + s[24] - s[7] == 188 )
solver.add( s[16] * s[27] + s[20] == 9310 )
solver.add( s[22] - s[30] - s[37] - s[9] == -211 )
solver.add( s[4] * s[41] * s[27] - s[38] == 1491286 )
solver.add( s[35] - s[29] * s[8] + s[13] == -13131 )
solver.add( s[23] - s[7] - s[24] - s[22] == -107 )
solver.add( s[37] * s[4] * s[5] == 560388 )
solver.add( s[17] * s[32] - s[15] == 5295 )
solver.add( s[32] + s[23] * s[18] - s[5] == 4927 )
solver.add( s[3] + s[8] * s[39] + s[39] == 7397 )
solver.add( s[7] * s[25] - s[3] + s[36] == 5597 )
solver.add( s[9] - s[24] - s[33] == -79 )
solver.add( s[30] + s[14] * s[36] == 8213 )

if solver.check() == sat:
solution = solver.model()
flag = []
for i in range(42):
flag.append(chr(int(str(solution[s[i]]))))
print("".join(flag))
else:
print("not found")

```