```
#>> bujk && fexor
from z3 import *
s = Solver()

x = [BitVec('input_%d' % i, 8) for i in range(22)]

for i in range(22):
s.add(x[i] > 0x20) # ascii (' ')
s.add(x[i] < 0x7f)

s.add(x[3] + x[15] + (x[15] ^ x[19]) == 296 );

s.add(x[19] - x[7] + x[0] + x[16] + x[11] + x[17] == 361 );

s.add(x[6] - x[14] + x[9] - x[2] + x[8] - x[15] + x[21] - x[11] == -109 );

s.add((x[5] ^ x[3]) + x[12] - x[11] + (x[6] ^ x[4]) == 29 );

s.add(x[6] - x[13] + (x[10] ^ x[15]) + x[21] - x[5] == -48 );

s.add((x[18] ^ x[19]) + x[6] - x[16] + (x[5] ^ x[16]) == 102 );

s.add(x[11] - x[21] + x[12] - x[10] == 36 );

s.add(x[3] - x[17] + x[19] + x[4] + (x[12] ^ x[17]) + x[10] - x[2] == 160 );

s.add(x[13] - x[8] + x[10] - x[20] + x[3] - x[17] == 85 );

s.add(x[0] - x[15] + x[20] + x[18] == 156 );

s.add(x[19] + x[10] + x[10] + x[19] + x[0] - x[20] + x[3] - x[18] == 297 );

s.add(x[16] - x[14] + (x[0] ^ x[11]) + (x[0] ^ x[14]) + x[13] - x[19] == 106 );

s.add(x[8] - x[3] + (x[14] ^ x[2]) + x[11] + x[0] + x[1] - x[19] == 283 );

s.add((x[10] ^ x[2]) + x[2] + x[7] + x[20] + x[13] + (x[3] ^ x[16]) + x[9] + x[6] == 621 );

s.add(x[21] - x[19] + x[7] - x[18] + x[16] - x[21] + (x[12] ^ x[18]) == 75 );

s.add(x[5] - x[18] + x[17] - x[4] + x[15] + x[2] + x[21] - x[18] + x[7] + x[6] == 250 );

s.add(x[4] - x[0] + x[2] - x[4] + x[15] - x[21] + x[17] + x[2] == 265 );

s.add(x[8] - x[17] + x[14] - x[3] + (x[8] ^ x[14]) + x[5] + x[1] + x[7] + x[10] == 384 );

s.add(x[4] - x[16] + (x[2] ^ x[7]) == 77 );

s.add((x[19] ^ x[13]) + x[6] - x[13] + x[17] - x[11] + (x[16] ^ x[12]) == 85 );

s.add(x[5] - x[16] + x[8] - x[12] + x[17] - x[13] + x[11] - x[2] + x[1] + x[21] == 98 );

s.add(x[14] + x[10] + x[18] - x[9] + x[5] + x[10] == 413 );

s.add(x[17] - x[1] + x[4] + x[11] + x[17] - x[9] == 166 );

s.add(x[10] - x[8] + x[2] - x[19] == 74 );

s.add(x[10] + x[3] + x[3] - x[19] + (x[19] ^ x[0]) == 328 );

s.add((x[5] ^ x[16]) + x[16] + x[3] + (x[0] ^ x[16]) == 232 );

s.add(x[10] + x[21] + (x[19] ^ x[2]) == 217 );

s.add(x[12] - x[17] + x[12] + x[8] == 153 );

print (s.check())
m = s.model()
res = ""
for i in range(22):
c = m[x[i]].as_long()
res = res + chr(c)

print("flag: ",res)
```