Rev Adulthood

Ishmael42 61 min read (12889 words)

Interesting Z3 rev challenge. Solved it with power of unix tools, vim and ofc, some Z3. (Possible Unintended Solution :))))

Challenge Files:

Problem Statement

Given a singular python file with a bunch of checks on a xor(userinput, 0xff). Userinput has to be a flag, of max 49 chars.

PY 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360

inpu = input("Enter the Flag: ")
inp = [ord(i)^0xff for i in inpu]

if len(inp) != 49:
    print("Thou hast failed the trial.")
    exit(0)

correct = 0

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




if correct == 294:
    print("Thou has passed the trial!")
else:
    print("Thou hast failed the trial.")

Looks simple enough, so I just use some vim-fu to turn the if conditions to z3 solver.add statements expecting a quick win

PY 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353

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)

Unfortunately, it didn’t work.

The twist

There is a total of 343 constraints being checked, each adds 1 to the variable correct if it passes. But at the end, the value of correct must be 294. It’s enforced by this check at the end of the file:

PY 
1
2
3
4

if correct == 294:
    print("Thou has passed the trial!")
else:
    print("Thou hast failed the trial.")

294 looks like an oddly specific number. heck, it’s even a multiple of 49 (49 * 6 == 294). Oddly enough, there’s another multiple of 49, which is 343, the number of constraint checks (49 * 7 == 343).

Out of the 343 constraint checks, only 294 must pass.

(Neo)Vim-Fu

The constraint checks were all jumbled, so I decied to group them. For this, I used this vimscript.

VIM 
1
2
3
4
5
6
7

" Clear the register A
:norm qaq
" Find all lines that have <number>] and delete it into the register A
for i in range(49)
  execute 'g/inp.' . i . '\]/norm "Add'
endfor
:norm "Ap

This gives the result. From this, it’s clear that each index has 7 checks. From this, I deduced that each index has a decoy check and I should get rid of it.

PY 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343

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

After further vim-fu, I come up with this solve script that bruteforces the odd-one-out check and finds the correct flag charecter for each index.

PY 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376

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)

Flag

TEXT 
1

inctf{thou_art_proven_worthy_before_the_almighty}