/
part2solver.py
862 lines (854 loc) · 37.4 KB
/
part2solver.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
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
from z3 import *
s = Solver()
FLAG = [BitVec(f'FLAG_{i}', 32) for i in range(840)]
for i in range(len(FLAG)):
s.add(FLAG[i] >= 0)
s.add(FLAG[i] <= 0xFF)
s.add((FLAG[839] + 0) % 255 == 65)
s.add(((FLAG[838] ^ 65) + 1) % 255 == 98)
s.add(((FLAG[837] ^ 98) + 2) % 255 == 35)
s.add(((FLAG[836] ^ 35) + 3) % 255 == 69)
s.add(((FLAG[835] ^ 69) + 4) % 255 == 36)
s.add(((FLAG[834] ^ 36) + 5) % 255 == 92)
s.add(((FLAG[833] ^ 92) + 6) % 255 == 67)
s.add(((FLAG[832] ^ 67) + 7) % 255 == 56)
s.add(((FLAG[831] ^ 56) + 8) % 255 == 32)
s.add(((FLAG[830] ^ 32) + 9) % 255 == 76)
s.add(((FLAG[829] ^ 76) + 10) % 255 == 47)
s.add(((FLAG[828] ^ 47) + 11) % 255 == 106)
s.add(((FLAG[827] ^ 106) + 12) % 255 == 14)
s.add(((FLAG[826] ^ 14) + 13) % 255 == 120)
s.add(((FLAG[825] ^ 120) + 14) % 255 == 24)
s.add(((FLAG[824] ^ 24) + 15) % 255 == 67)
s.add(((FLAG[823] ^ 67) + 16) % 255 == 115)
s.add(((FLAG[822] ^ 115) + 17) % 255 == 35)
s.add(((FLAG[821] ^ 35) + 18) % 255 == 97)
s.add(((FLAG[820] ^ 97) + 19) % 255 == 37)
s.add(((FLAG[819] ^ 37) + 20) % 255 == 94)
s.add(((FLAG[818] ^ 94) + 21) % 255 == 147)
s.add(((FLAG[817] ^ 147) + 22) % 255 == 15)
s.add(((FLAG[816] ^ 15) + 23) % 255 == 120)
s.add(((FLAG[815] ^ 120) + 24) % 255 == 47)
s.add(((FLAG[814] ^ 47) + 25) % 255 == 113)
s.add(((FLAG[813] ^ 113) + 26) % 255 == 57)
s.add(((FLAG[812] ^ 57) + 27) % 255 == 52)
s.add(((FLAG[811] ^ 52) + 28) % 255 == 113)
s.add(((FLAG[810] ^ 113) + 29) % 255 == 31)
s.add(((FLAG[809] ^ 31) + 30) % 255 == 93)
s.add(((FLAG[808] ^ 93) + 31) % 255 == 61)
s.add(((FLAG[807] ^ 61) + 32) % 255 == 124)
s.add(((FLAG[806] ^ 124) + 33) % 255 == 58)
s.add(((FLAG[805] ^ 58) + 34) % 255 == 107)
s.add(((FLAG[804] ^ 107) + 35) % 255 == 45)
s.add(((FLAG[803] ^ 45) + 36) % 255 == 131)
s.add(((FLAG[802] ^ 131) + 37) % 255 == 201)
s.add(((FLAG[801] ^ 201) + 38) % 255 == 224)
s.add(((FLAG[800] ^ 224) + 39) % 255 == 231)
s.add(((FLAG[799] ^ 231) + 40) % 255 == 172)
s.add(((FLAG[798] ^ 172) + 41) % 255 == 238)
s.add(((FLAG[797] ^ 238) + 42) % 255 == 200)
s.add(((FLAG[796] ^ 200) + 43) % 255 == 203)
s.add(((FLAG[795] ^ 203) + 44) % 255 == 218)
s.add(((FLAG[794] ^ 218) + 45) % 255 == 213)
s.add(((FLAG[793] ^ 213) + 46) % 255 == 40)
s.add(((FLAG[792] ^ 40) + 47) % 255 == 55)
s.add(((FLAG[791] ^ 55) + 48) % 255 == 115)
s.add(((FLAG[790] ^ 115) + 49) % 255 == 76)
s.add(((FLAG[789] ^ 76) + 50) % 255 == 91)
s.add(((FLAG[788] ^ 91) + 51) % 255 == 174)
s.add(((FLAG[787] ^ 174) + 52) % 255 == 18)
s.add(((FLAG[786] ^ 18) + 53) % 255 == 175)
s.add(((FLAG[785] ^ 175) + 54) % 255 == 252)
s.add(((FLAG[784] ^ 252) + 55) % 255 == 209)
s.add(((FLAG[783] ^ 209) + 56) % 255 == 221)
s.add(((FLAG[782] ^ 221) + 57) % 255 == 55)
s.add(((FLAG[781] ^ 55) + 58) % 255 == 142)
s.add(((FLAG[780] ^ 142) + 59) % 255 == 35)
s.add(((FLAG[779] ^ 35) + 60) % 255 == 143)
s.add(((FLAG[778] ^ 143) + 61) % 255 == 37)
s.add(((FLAG[777] ^ 37) + 62) % 255 == 126)
s.add(((FLAG[776] ^ 126) + 63) % 255 == 75)
s.add(((FLAG[775] ^ 75) + 64) % 255 == 167)
s.add(((FLAG[774] ^ 167) + 65) % 255 == 200)
s.add(((FLAG[773] ^ 200) + 66) % 255 == 205)
s.add(((FLAG[772] ^ 205) + 67) % 255 == 239)
s.add(((FLAG[771] ^ 239) + 68) % 255 == 206)
s.add(((FLAG[770] ^ 206) + 69) % 255 == 3)
s.add(((FLAG[769] ^ 3) + 70) % 255 == 168)
s.add(((FLAG[768] ^ 168) + 71) % 255 == 34)
s.add(((FLAG[767] ^ 34) + 72) % 255 == 77)
s.add(((FLAG[766] ^ 77) + 73) % 255 == 135)
s.add(((FLAG[765] ^ 135) + 74) % 255 == 241)
s.add(((FLAG[764] ^ 241) + 75) % 255 == 221)
s.add(((FLAG[763] ^ 221) + 76) % 255 == 254)
s.add(((FLAG[762] ^ 254) + 77) % 255 == 231)
s.add(((FLAG[761] ^ 231) + 78) % 255 == 208)
s.add(((FLAG[760] ^ 208) + 79) % 255 == 76)
s.add(((FLAG[759] ^ 76) + 80) % 255 == 188)
s.add(((FLAG[758] ^ 188) + 81) % 255 == 8)
s.add(((FLAG[757] ^ 8) + 82) % 255 == 185)
s.add(((FLAG[756] ^ 185) + 83) % 255 == 31)
s.add(((FLAG[755] ^ 31) + 84) % 255 == 147)
s.add(((FLAG[754] ^ 147) + 85) % 255 == 38)
s.add(((FLAG[753] ^ 38) + 86) % 255 == 157)
s.add(((FLAG[752] ^ 157) + 87) % 255 == 80)
s.add(((FLAG[751] ^ 80) + 88) % 255 == 123)
s.add(((FLAG[750] ^ 123) + 89) % 255 == 115)
s.add(((FLAG[749] ^ 115) + 90) % 255 == 91)
s.add(((FLAG[748] ^ 91) + 91) % 255 == 214)
s.add(((FLAG[747] ^ 214) + 92) % 255 == 2)
s.add(((FLAG[746] ^ 2) + 93) % 255 == 199)
s.add(((FLAG[745] ^ 199) + 94) % 255 == 13)
s.add(((FLAG[744] ^ 13) + 95) % 255 == 202)
s.add(((FLAG[743] ^ 202) + 96) % 255 == 31)
s.add(((FLAG[742] ^ 31) + 97) % 255 == 148)
s.add(((FLAG[741] ^ 148) + 98) % 255 == 23)
s.add(((FLAG[740] ^ 23) + 99) % 255 == 225)
s.add(((FLAG[739] ^ 225) + 100) % 255 == 246)
s.add(((FLAG[738] ^ 246) + 101) % 255 == 60)
s.add(((FLAG[737] ^ 60) + 102) % 255 == 185)
s.add(((FLAG[736] ^ 185) + 103) % 255 == 63)
s.add(((FLAG[735] ^ 63) + 104) % 255 == 194)
s.add(((FLAG[734] ^ 194) + 105) % 255 == 76)
s.add(((FLAG[733] ^ 76) + 106) % 255 == 141)
s.add(((FLAG[732] ^ 141) + 107) % 255 == 87)
s.add(((FLAG[731] ^ 87) + 108) % 255 == 227)
s.add(((FLAG[730] ^ 227) + 109) % 255 == 5)
s.add(((FLAG[729] ^ 5) + 110) % 255 == 219)
s.add(((FLAG[728] ^ 219) + 111) % 255 == 46)
s.add(((FLAG[727] ^ 46) + 112) % 255 == 126)
s.add(((FLAG[726] ^ 126) + 113) % 255 == 126)
s.add(((FLAG[725] ^ 126) + 114) % 255 == 137)
s.add(((FLAG[724] ^ 137) + 115) % 255 == 88)
s.add(((FLAG[723] ^ 88) + 116) % 255 == 156)
s.add(((FLAG[722] ^ 156) + 117) % 255 == 102)
s.add(((FLAG[721] ^ 102) + 118) % 255 == 121)
s.add(((FLAG[720] ^ 121) + 119) % 255 == 129)
s.add(((FLAG[719] ^ 129) + 120) % 255 == 110)
s.add(((FLAG[718] ^ 110) + 121) % 255 == 199)
s.add(((FLAG[717] ^ 199) + 122) % 255 == 33)
s.add(((FLAG[716] ^ 33) + 123) % 255 == 202)
s.add(((FLAG[715] ^ 202) + 124) % 255 == 43)
s.add(((FLAG[714] ^ 43) + 125) % 255 == 136)
s.add(((FLAG[713] ^ 136) + 126) % 255 == 100)
s.add(((FLAG[712] ^ 100) + 127) % 255 == 138)
s.add(((FLAG[711] ^ 138) + 128) % 255 == 122)
s.add(((FLAG[710] ^ 122) + 129) % 255 == 143)
s.add(((FLAG[709] ^ 143) + 130) % 255 == 50)
s.add(((FLAG[708] ^ 50) + 131) % 255 == 200)
s.add(((FLAG[707] ^ 200) + 132) % 255 == 38)
s.add(((FLAG[706] ^ 38) + 133) % 255 == 199)
s.add(((FLAG[705] ^ 199) + 134) % 255 == 41)
s.add(((FLAG[704] ^ 41) + 135) % 255 == 204)
s.add(((FLAG[703] ^ 204) + 136) % 255 == 62)
s.add(((FLAG[702] ^ 62) + 137) % 255 == 167)
s.add(((FLAG[701] ^ 167) + 138) % 255 == 87)
s.add(((FLAG[700] ^ 87) + 139) % 255 == 196)
s.add(((FLAG[699] ^ 196) + 140) % 255 == 56)
s.add(((FLAG[698] ^ 56) + 141) % 255 == 220)
s.add(((FLAG[697] ^ 220) + 142) % 255 == 65)
s.add(((FLAG[696] ^ 65) + 143) % 255 == 240)
s.add(((FLAG[695] ^ 240) + 144) % 255 == 38)
s.add(((FLAG[694] ^ 38) + 145) % 255 == 217)
s.add(((FLAG[693] ^ 217) + 146) % 255 == 77)
s.add(((FLAG[692] ^ 77) + 147) % 255 == 210)
s.add(((FLAG[691] ^ 210) + 148) % 255 == 64)
s.add(((FLAG[690] ^ 64) + 149) % 255 == 197)
s.add(((FLAG[689] ^ 197) + 150) % 255 == 72)
s.add(((FLAG[688] ^ 72) + 151) % 255 == 184)
s.add(((FLAG[687] ^ 184) + 152) % 255 == 112)
s.add(((FLAG[686] ^ 112) + 153) % 255 == 183)
s.add(((FLAG[685] ^ 183) + 154) % 255 == 50)
s.add(((FLAG[684] ^ 50) + 155) % 255 == 225)
s.add(((FLAG[683] ^ 225) + 156) % 255 == 33)
s.add(((FLAG[682] ^ 33) + 157) % 255 == 223)
s.add(((FLAG[681] ^ 223) + 158) % 255 == 86)
s.add(((FLAG[680] ^ 86) + 159) % 255 == 215)
s.add(((FLAG[679] ^ 215) + 160) % 255 == 95)
s.add(((FLAG[678] ^ 95) + 161) % 255 == 207)
s.add(((FLAG[677] ^ 207) + 162) % 255 == 93)
s.add(((FLAG[676] ^ 93) + 163) % 255 == 219)
s.add(((FLAG[675] ^ 219) + 164) % 255 == 77)
s.add(((FLAG[674] ^ 77) + 165) % 255 == 9)
s.add(((FLAG[673] ^ 9) + 166) % 255 == 207)
s.add(((FLAG[672] ^ 207) + 167) % 255 == 46)
s.add(((FLAG[671] ^ 46) + 168) % 255 == 3)
s.add(((FLAG[670] ^ 3) + 169) % 255 == 204)
s.add(((FLAG[669] ^ 204) + 170) % 255 == 80)
s.add(((FLAG[668] ^ 80) + 171) % 255 == 206)
s.add(((FLAG[667] ^ 206) + 172) % 255 == 155)
s.add(((FLAG[666] ^ 155) + 173) % 255 == 168)
s.add(((FLAG[665] ^ 168) + 174) % 255 == 55)
s.add(((FLAG[664] ^ 55) + 175) % 255 == 242)
s.add(((FLAG[663] ^ 242) + 176) % 255 == 60)
s.add(((FLAG[662] ^ 60) + 177) % 255 == 253)
s.add(((FLAG[661] ^ 253) + 178) % 255 == 75)
s.add(((FLAG[660] ^ 75) + 179) % 255 == 31)
s.add(((FLAG[659] ^ 31) + 180) % 255 == 201)
s.add(((FLAG[658] ^ 201) + 181) % 255 == 92)
s.add(((FLAG[657] ^ 92) + 182) % 255 == 240)
s.add(((FLAG[656] ^ 240) + 183) % 255 == 136)
s.add(((FLAG[655] ^ 136) + 184) % 255 == 180)
s.add(((FLAG[654] ^ 180) + 185) % 255 == 123)
s.add(((FLAG[653] ^ 123) + 186) % 255 == 211)
s.add(((FLAG[652] ^ 211) + 187) % 255 == 92)
s.add(((FLAG[651] ^ 92) + 188) % 255 == 228)
s.add(((FLAG[650] ^ 228) + 189) % 255 == 75)
s.add(((FLAG[649] ^ 75) + 190) % 255 == 253)
s.add(((FLAG[648] ^ 253) + 191) % 255 == 72)
s.add(((FLAG[647] ^ 72) + 192) % 255 == 252)
s.add(((FLAG[646] ^ 252) + 193) % 255 == 87)
s.add(((FLAG[645] ^ 87) + 194) % 255 == 250)
s.add(((FLAG[644] ^ 250) + 195) % 255 == 88)
s.add(((FLAG[643] ^ 88) + 196) % 255 == 61)
s.add(((FLAG[642] ^ 61) + 197) % 255 == 36)
s.add(((FLAG[641] ^ 36) + 198) % 255 == 20)
s.add(((FLAG[640] ^ 20) + 199) % 255 == 44)
s.add(((FLAG[639] ^ 44) + 200) % 255 == 13)
s.add(((FLAG[638] ^ 13) + 201) % 255 == 50)
s.add(((FLAG[637] ^ 50) + 202) % 255 == 11)
s.add(((FLAG[636] ^ 11) + 203) % 255 == 246)
s.add(((FLAG[635] ^ 246) + 204) % 255 == 108)
s.add(((FLAG[634] ^ 108) + 205) % 255 == 207)
s.add(((FLAG[633] ^ 207) + 206) % 255 == 190)
s.add(((FLAG[632] ^ 190) + 207) % 255 == 153)
s.add(((FLAG[631] ^ 153) + 208) % 255 == 194)
s.add(((FLAG[630] ^ 194) + 209) % 255 == 125)
s.add(((FLAG[629] ^ 125) + 210) % 255 == 240)
s.add(((FLAG[628] ^ 240) + 211) % 255 == 108)
s.add(((FLAG[627] ^ 108) + 212) % 255 == 33)
s.add(((FLAG[626] ^ 33) + 213) % 255 == 26)
s.add(((FLAG[625] ^ 26) + 214) % 255 == 82)
s.add(((FLAG[624] ^ 82) + 215) % 255 == 9)
s.add(((FLAG[623] ^ 9) + 216) % 255 == 58)
s.add(((FLAG[622] ^ 58) + 217) % 255 == 243)
s.add(((FLAG[621] ^ 243) + 218) % 255 == 122)
s.add(((FLAG[620] ^ 122) + 219) % 255 == 250)
s.add(((FLAG[619] ^ 250) + 220) % 255 == 107)
s.add(((FLAG[618] ^ 107) + 221) % 255 == 252)
s.add(((FLAG[617] ^ 252) + 222) % 255 == 120)
s.add(((FLAG[616] ^ 120) + 223) % 255 == 233)
s.add(((FLAG[615] ^ 233) + 224) % 255 == 170)
s.add(((FLAG[614] ^ 170) + 225) % 255 == 165)
s.add(((FLAG[613] ^ 165) + 226) % 255 == 174)
s.add(((FLAG[612] ^ 174) + 227) % 255 == 114)
s.add(((FLAG[611] ^ 114) + 228) % 255 == 234)
s.add(((FLAG[610] ^ 234) + 229) % 255 == 104)
s.add(((FLAG[609] ^ 104) + 230) % 255 == 243)
s.add(((FLAG[608] ^ 243) + 231) % 255 == 187)
s.add(((FLAG[607] ^ 187) + 232) % 255 == 180)
s.add(((FLAG[606] ^ 180) + 233) % 255 == 194)
s.add(((FLAG[605] ^ 194) + 234) % 255 == 142)
s.add(((FLAG[604] ^ 142) + 235) % 255 == 211)
s.add(((FLAG[603] ^ 211) + 236) % 255 == 170)
s.add(((FLAG[602] ^ 170) + 237) % 255 == 204)
s.add(((FLAG[601] ^ 204) + 238) % 255 == 152)
s.add(((FLAG[600] ^ 152) + 239) % 255 == 208)
s.add(((FLAG[599] ^ 208) + 240) % 255 == 149)
s.add(((FLAG[598] ^ 149) + 241) % 255 == 167)
s.add(((FLAG[597] ^ 167) + 242) % 255 == 193)
s.add(((FLAG[596] ^ 193) + 243) % 255 == 166)
s.add(((FLAG[595] ^ 166) + 244) % 255 == 123)
s.add(((FLAG[594] ^ 123) + 245) % 255 == 254)
s.add(((FLAG[593] ^ 254) + 246) % 255 == 146)
s.add(((FLAG[592] ^ 146) + 247) % 255 == 218)
s.add(((FLAG[591] ^ 218) + 248) % 255 == 175)
s.add(((FLAG[590] ^ 175) + 249) % 255 == 200)
s.add(((FLAG[589] ^ 200) + 250) % 255 == 166)
s.add(((FLAG[588] ^ 166) + 251) % 255 == 191)
s.add(((FLAG[587] ^ 191) + 252) % 255 == 216)
s.add(((FLAG[586] ^ 216) + 253) % 255 == 246)
s.add(((FLAG[585] ^ 246) + 254) % 255 == 147)
s.add(((FLAG[584] ^ 147) + 0) % 255 == 234)
s.add(((FLAG[583] ^ 234) + 1) % 255 == 203)
s.add(((FLAG[582] ^ 203) + 2) % 255 == 172)
s.add(((FLAG[581] ^ 172) + 3) % 255 == 143)
s.add(((FLAG[580] ^ 143) + 4) % 255 == 231)
s.add(((FLAG[579] ^ 231) + 5) % 255 == 135)
s.add(((FLAG[578] ^ 135) + 6) % 255 == 249)
s.add(((FLAG[577] ^ 249) + 7) % 255 == 148)
s.add(((FLAG[576] ^ 148) + 8) % 255 == 249)
s.add(((FLAG[575] ^ 249) + 9) % 255 == 148)
s.add(((FLAG[574] ^ 148) + 10) % 255 == 190)
s.add(((FLAG[573] ^ 190) + 11) % 255 == 216)
s.add(((FLAG[572] ^ 216) + 12) % 255 == 195)
s.add(((FLAG[571] ^ 195) + 13) % 255 == 187)
s.add(((FLAG[570] ^ 187) + 14) % 255 == 236)
s.add(((FLAG[569] ^ 236) + 15) % 255 == 219)
s.add(((FLAG[568] ^ 219) + 16) % 255 == 205)
s.add(((FLAG[567] ^ 205) + 17) % 255 == 181)
s.add(((FLAG[566] ^ 181) + 18) % 255 == 223)
s.add(((FLAG[565] ^ 223) + 19) % 255 == 205)
s.add(((FLAG[564] ^ 205) + 20) % 255 == 189)
s.add(((FLAG[563] ^ 189) + 21) % 255 == 178)
s.add(((FLAG[562] ^ 178) + 22) % 255 == 242)
s.add(((FLAG[561] ^ 242) + 23) % 255 == 158)
s.add(((FLAG[560] ^ 158) + 24) % 255 == 12)
s.add(((FLAG[559] ^ 12) + 25) % 255 == 135)
s.add(((FLAG[558] ^ 135) + 26) % 255 == 252)
s.add(((FLAG[557] ^ 252) + 27) % 255 == 169)
s.add(((FLAG[556] ^ 169) + 28) % 255 == 165)
s.add(((FLAG[555] ^ 165) + 29) % 255 == 204)
s.add(((FLAG[554] ^ 204) + 30) % 255 == 193)
s.add(((FLAG[553] ^ 193) + 31) % 255 == 198)
s.add(((FLAG[552] ^ 198) + 32) % 255 == 7)
s.add(((FLAG[551] ^ 7) + 33) % 255 == 152)
s.add(((FLAG[550] ^ 152) + 34) % 255 == 26)
s.add(((FLAG[549] ^ 26) + 35) % 255 == 140)
s.add(((FLAG[548] ^ 140) + 36) % 255 == 10)
s.add(((FLAG[547] ^ 10) + 37) % 255 == 163)
s.add(((FLAG[546] ^ 163) + 38) % 255 == 240)
s.add(((FLAG[545] ^ 240) + 39) % 255 == 198)
s.add(((FLAG[544] ^ 198) + 40) % 255 == 208)
s.add(((FLAG[543] ^ 208) + 41) % 255 == 204)
s.add(((FLAG[542] ^ 204) + 42) % 255 == 23)
s.add(((FLAG[541] ^ 23) + 43) % 255 == 158)
s.add(((FLAG[540] ^ 158) + 44) % 255 == 30)
s.add(((FLAG[539] ^ 30) + 45) % 255 == 150)
s.add(((FLAG[538] ^ 150) + 46) % 255 == 39)
s.add(((FLAG[537] ^ 39) + 47) % 255 == 54)
s.add(((FLAG[536] ^ 54) + 48) % 255 == 114)
s.add(((FLAG[535] ^ 114) + 49) % 255 == 75)
s.add(((FLAG[534] ^ 75) + 50) % 255 == 96)
s.add(((FLAG[533] ^ 96) + 51) % 255 == 115)
s.add(((FLAG[532] ^ 115) + 52) % 255 == 70)
s.add(((FLAG[531] ^ 70) + 53) % 255 == 95)
s.add(((FLAG[530] ^ 95) + 54) % 255 == 101)
s.add(((FLAG[529] ^ 101) + 55) % 255 == 68)
s.add(((FLAG[528] ^ 68) + 56) % 255 == 93)
s.add(((FLAG[527] ^ 93) + 57) % 255 == 120)
s.add(((FLAG[526] ^ 120) + 58) % 255 == 87)
s.add(((FLAG[525] ^ 87) + 59) % 255 == 94)
s.add(((FLAG[524] ^ 94) + 60) % 255 == 172)
s.add(((FLAG[523] ^ 172) + 61) % 255 == 201)
s.add(((FLAG[522] ^ 201) + 62) % 255 == 205)
s.add(((FLAG[521] ^ 205) + 63) % 255 == 225)
s.add(((FLAG[461] ^ 225) + 64) % 255 == 211)
# s.add(((FLAG[540794265] ^ 211) + 65) % 255 == 53)
s.add(((FLAG[518] ^ 53) + 66) % 255 == 146)
s.add(((FLAG[517] ^ 146) + 67) % 255 == 46)
s.add(((FLAG[516] ^ 46) + 68) % 255 == 147)
s.add(((FLAG[515] ^ 147) + 69) % 255 == 68)
# s.add(((-1066059168 ^ 68) + 70) % 255 == 122)
s.add(((FLAG[513] ^ 122) + 71) % 255 == 93)
s.add(((FLAG[512] ^ 93) + 72) % 255 == 128)
s.add(((FLAG[511] ^ 128) + 73) % 255 == 245)
s.add(((FLAG[510] ^ 245) + 74) % 255 == 32)
s.add(((FLAG[509] ^ 32) + 75) % 255 == 162)
s.add(((FLAG[508] ^ 162) + 76) % 255 == 24)
s.add(((FLAG[507] ^ 24) + 77) % 255 == 185)
s.add(((FLAG[506] ^ 185) + 78) % 255 == 32)
s.add(((FLAG[505] ^ 32) + 79) % 255 == 79)
s.add(((FLAG[504] ^ 79) + 80) % 255 == 126)
s.add(((FLAG[503] ^ 126) + 81) % 255 == 175)
s.add(((FLAG[502] ^ 175) + 82) % 255 == 22)
s.add(((FLAG[501] ^ 22) + 83) % 255 == 198)
s.add(((FLAG[500] ^ 198) + 84) % 255 == 244)
s.add(((FLAG[499] ^ 244) + 85) % 255 == 213)
s.add(((FLAG[498] ^ 213) + 86) % 255 == 76)
s.add(((FLAG[497] ^ 76) + 87) % 255 == 150)
s.add(((FLAG[496] ^ 150) + 88) % 255 == 87)
s.add(((FLAG[495] ^ 87) + 89) % 255 == 151)
s.add(((FLAG[494] ^ 151) + 90) % 255 == 76)
s.add(((FLAG[493] ^ 76) + 91) % 255 == 147)
s.add(((FLAG[492] ^ 147) + 92) % 255 == 16)
s.add(((FLAG[491] ^ 16) + 93) % 255 == 220)
s.add(((FLAG[490] ^ 220) + 94) % 255 == 25)
s.add(((FLAG[489] ^ 25) + 95) % 255 == 152)
s.add(((FLAG[488] ^ 152) + 96) % 255 == 12)
s.add(((FLAG[487] ^ 12) + 97) % 255 == 129)
s.add(((FLAG[486] ^ 129) + 98) % 255 == 4)
s.add(((FLAG[485] ^ 4) + 99) % 255 == 163)
s.add(((FLAG[484] ^ 163) + 100) % 255 == 231)
s.add(((FLAG[483] ^ 231) + 101) % 255 == 245)
s.add(((FLAG[482] ^ 245) + 102) % 255 == 1)
s.add(((FLAG[481] ^ 1) + 103) % 255 == 219)
s.add(((FLAG[480] ^ 219) + 104) % 255 == 32)
s.add(((FLAG[479] ^ 32) + 105) % 255 == 173)
s.add(((FLAG[478] ^ 173) + 106) % 255 == 247)
s.add(((FLAG[477] ^ 247) + 107) % 255 == 1)
s.add(((FLAG[476] ^ 1) + 108) % 255 == 208)
s.add(((FLAG[475] ^ 208) + 109) % 255 == 94)
s.add(((FLAG[474] ^ 94) + 110) % 255 == 154)
s.add(((FLAG[473] ^ 154) + 111) % 255 == 111)
s.add(((FLAG[472] ^ 111) + 112) % 255 == 143)
s.add(((FLAG[471] ^ 143) + 113) % 255 == 85)
s.add(((FLAG[470] ^ 85) + 114) % 255 == 166)
s.add(((FLAG[469] ^ 166) + 115) % 255 == 57)
s.add(((FLAG[468] ^ 57) + 116) % 255 == 208)
s.add(((FLAG[467] ^ 208) + 117) % 255 == 42)
s.add(((FLAG[466] ^ 42) + 118) % 255 == 128)
s.add(((FLAG[465] ^ 128) + 119) % 255 == 90)
s.add(((FLAG[464] ^ 90) + 120) % 255 == 155)
s.add(((FLAG[463] ^ 155) + 121) % 255 == 53)
s.add(((FLAG[462] ^ 53) + 122) % 255 == 238)
# s.add(((FLAG[461] ^ 238) + 123) % 255 == 62)
s.add(((FLAG[460] ^ 62) + 124) % 255 == 154)
s.add(((FLAG[459] ^ 154) + 125) % 255 == 93)
s.add(((FLAG[458] ^ 93) + 126) % 255 == 251)
s.add(((FLAG[457] ^ 251) + 127) % 255 == 12)
s.add(((FLAG[456] ^ 12) + 128) % 255 == 227)
s.add(((FLAG[455] ^ 227) + 129) % 255 == 24)
s.add(((FLAG[454] ^ 24) + 130) % 255 == 246)
s.add(((FLAG[453] ^ 246) + 131) % 255 == 22)
s.add(((FLAG[452] ^ 22) + 132) % 255 == 186)
s.add(((FLAG[451] ^ 186) + 133) % 255 == 54)
s.add(((FLAG[450] ^ 54) + 134) % 255 == 218)
s.add(((FLAG[449] ^ 218) + 135) % 255 == 71)
s.add(((FLAG[448] ^ 71) + 136) % 255 == 172)
s.add(((FLAG[447] ^ 172) + 137) % 255 == 77)
s.add(((FLAG[446] ^ 77) + 138) % 255 == 170)
s.add(((FLAG[445] ^ 170) + 139) % 255 == 91)
s.add(((FLAG[444] ^ 91) + 140) % 255 == 8)
s.add(((FLAG[443] ^ 8) + 141) % 255 == 215)
s.add(((FLAG[442] ^ 215) + 142) % 255 == 138)
s.add(((FLAG[441] ^ 138) + 143) % 255 == 58)
s.add(((FLAG[440] ^ 58) + 144) % 255 == 235)
s.add(((FLAG[439] ^ 235) + 145) % 255 == 23)
s.add(((FLAG[438] ^ 23) + 146) % 255 == 6)
s.add(((FLAG[437] ^ 6) + 147) % 255 == 185)
s.add(((FLAG[436] ^ 185) + 148) % 255 == 95)
s.add(((FLAG[435] ^ 95) + 149) % 255 == 197)
s.add(((FLAG[434] ^ 197) + 150) % 255 == 124)
s.add(((FLAG[433] ^ 124) + 151) % 255 == 170)
s.add(((FLAG[432] ^ 170) + 152) % 255 == 93)
s.add(((FLAG[431] ^ 93) + 153) % 255 == 13)
s.add(((FLAG[430] ^ 13) + 154) % 255 == 199)
s.add(((FLAG[429] ^ 199) + 155) % 255 == 47)
s.add(((FLAG[428] ^ 47) + 156) % 255 == 227)
s.add(((FLAG[427] ^ 227) + 157) % 255 == 36)
s.add(((FLAG[426] ^ 36) + 158) % 255 == 162)
s.add(((FLAG[425] ^ 162) + 159) % 255 == 111)
s.add(((FLAG[424] ^ 111) + 160) % 255 == 170)
s.add(((FLAG[423] ^ 170) + 161) % 255 == 128)
s.add(((FLAG[422] ^ 128) + 162) % 255 == 139)
s.add(((FLAG[421] ^ 139) + 163) % 255 == 136)
s.add(((FLAG[420] ^ 136) + 164) % 255 == 145)
s.add(((FLAG[419] ^ 145) + 165) % 255 == 87)
s.add(((FLAG[418] ^ 87) + 166) % 255 == 228)
s.add(((FLAG[417] ^ 228) + 167) % 255 == 63)
s.add(((FLAG[416] ^ 63) + 168) % 255 == 199)
s.add(((FLAG[415] ^ 199) + 169) % 255 == 83)
s.add(((FLAG[414] ^ 83) + 170) % 255 == 220)
s.add(((FLAG[413] ^ 220) + 171) % 255 == 93)
s.add(((FLAG[412] ^ 93) + 172) % 255 == 228)
s.add(((FLAG[411] ^ 228) + 173) % 255 == 46)
s.add(((FLAG[410] ^ 46) + 174) % 255 == 188)
s.add(((FLAG[409] ^ 188) + 175) % 255 == 141)
s.add(((FLAG[408] ^ 141) + 176) % 255 == 156)
s.add(((FLAG[407] ^ 156) + 177) % 255 == 154)
s.add(((FLAG[406] ^ 154) + 178) % 255 == 178)
s.add(((FLAG[405] ^ 178) + 179) % 255 == 116)
s.add(((FLAG[404] ^ 116) + 180) % 255 == 9)
s.add(((FLAG[403] ^ 9) + 181) % 255 == 248)
s.add(((FLAG[402] ^ 248) + 182) % 255 == 68)
s.add(((FLAG[401] ^ 68) + 183) % 255 == 223)
s.add(((FLAG[400] ^ 223) + 184) % 255 == 111)
s.add(((FLAG[399] ^ 111) + 185) % 255 == 211)
s.add(((FLAG[398] ^ 211) + 186) % 255 == 91)
s.add(((FLAG[397] ^ 91) + 187) % 255 == 55)
s.add(((FLAG[396] ^ 55) + 188) % 255 == 49)
s.add(((FLAG[395] ^ 49) + 189) % 255 == 14)
s.add(((FLAG[394] ^ 14) + 190) % 255 == 42)
s.add(((FLAG[393] ^ 42) + 191) % 255 == 25)
s.add(((FLAG[392] ^ 25) + 192) % 255 == 57)
s.add(((FLAG[391] ^ 57) + 193) % 255 == 13)
s.add(((FLAG[390] ^ 13) + 194) % 255 == 227)
s.add(((FLAG[389] ^ 227) + 195) % 255 == 135)
s.add(((FLAG[388] ^ 135) + 196) % 255 == 181)
s.add(((FLAG[387] ^ 181) + 197) % 255 == 163)
s.add(((FLAG[386] ^ 163) + 198) % 255 == 147)
s.add(((FLAG[385] ^ 147) + 199) % 255 == 123)
s.add(((FLAG[384] ^ 123) + 200) % 255 == 214)
s.add(((FLAG[383] ^ 214) + 201) % 255 == 111)
s.add(((FLAG[382] ^ 111) + 202) % 255 == 212)
s.add(((FLAG[381] ^ 212) + 203) % 255 == 124)
s.add(((FLAG[380] ^ 124) + 204) % 255 == 41)
s.add(((FLAG[379] ^ 41) + 205) % 255 == 14)
s.add(((FLAG[378] ^ 14) + 206) % 255 == 73)
s.add(((FLAG[377] ^ 73) + 207) % 255 == 57)
s.add(((FLAG[376] ^ 57) + 208) % 255 == 33)
s.add(((FLAG[375] ^ 33) + 209) % 255 == 33)
s.add(((FLAG[374] ^ 33) + 210) % 255 == 211)
s.add(((FLAG[373] ^ 211) + 211) % 255 == 143)
s.add(((FLAG[372] ^ 143) + 212) % 255 == 187)
s.add(((FLAG[371] ^ 187) + 213) % 255 == 158)
s.add(((FLAG[370] ^ 158) + 214) % 255 == 149)
s.add(((FLAG[369] ^ 149) + 215) % 255 == 189)
s.add(((FLAG[368] ^ 189) + 216) % 255 == 168)
s.add(((FLAG[367] ^ 168) + 217) % 255 == 155)
s.add(((FLAG[366] ^ 155) + 218) % 255 == 200)
s.add(((FLAG[365] ^ 200) + 219) % 255 == 133)
s.add(((FLAG[364] ^ 133) + 220) % 255 == 206)
s.add(((FLAG[363] ^ 206) + 221) % 255 == 137)
s.add(((FLAG[362] ^ 137) + 222) % 255 == 136)
s.add(((FLAG[361] ^ 136) + 223) % 255 == 203)
s.add(((FLAG[360] ^ 203) + 224) % 255 == 133)
s.add(((FLAG[359] ^ 133) + 225) % 255 == 217)
s.add(((FLAG[358] ^ 217) + 226) % 255 == 142)
s.add(((FLAG[357] ^ 142) + 227) % 255 == 207)
s.add(((FLAG[356] ^ 207) + 228) % 255 == 161)
s.add(((FLAG[355] ^ 161) + 229) % 255 == 183)
s.add(((FLAG[354] ^ 183) + 230) % 255 == 191)
s.add(((FLAG[353] ^ 191) + 231) % 255 == 185)
s.add(((FLAG[352] ^ 185) + 232) % 255 == 198)
s.add(((FLAG[351] ^ 198) + 233) % 255 == 141)
s.add(((FLAG[350] ^ 141) + 234) % 255 == 206)
s.add(((FLAG[349] ^ 206) + 235) % 255 == 153)
s.add(((FLAG[348] ^ 153) + 236) % 255 == 233)
s.add(((FLAG[347] ^ 233) + 237) % 255 == 181)
s.add(((FLAG[346] ^ 181) + 238) % 255 == 174)
s.add(((FLAG[345] ^ 174) + 239) % 255 == 206)
s.add(((FLAG[344] ^ 206) + 240) % 255 == 158)
s.add(((FLAG[343] ^ 158) + 241) % 255 == 220)
s.add(((FLAG[342] ^ 220) + 242) % 255 == 173)
s.add(((FLAG[341] ^ 173) + 243) % 255 == 202)
s.add(((FLAG[340] ^ 202) + 244) % 255 == 177)
s.add(((FLAG[339] ^ 177) + 245) % 255 == 242)
s.add(((FLAG[338] ^ 242) + 246) % 255 == 164)
s.add(((FLAG[337] ^ 164) + 247) % 255 == 206)
s.add(((FLAG[336] ^ 206) + 248) % 255 == 246)
s.add(((FLAG[335] ^ 246) + 249) % 255 == 122)
s.add(((FLAG[334] ^ 122) + 250) % 255 == 68)
s.add(((FLAG[333] ^ 68) + 251) % 255 == 50)
s.add(((FLAG[332] ^ 50) + 252) % 255 == 62)
s.add(((FLAG[331] ^ 62) + 253) % 255 == 13)
s.add(((FLAG[330] ^ 13) + 254) % 255 == 98)
s.add(((FLAG[329] ^ 98) + 0) % 255 == 5)
s.add(((FLAG[328] ^ 5) + 1) % 255 == 91)
s.add(((FLAG[327] ^ 91) + 2) % 255 == 62)
s.add(((FLAG[326] ^ 62) + 3) % 255 == 17)
s.add(((FLAG[325] ^ 17) + 4) % 255 == 105)
s.add(((FLAG[324] ^ 105) + 5) % 255 == 59)
s.add(((FLAG[323] ^ 59) + 6) % 255 == 96)
s.add(((FLAG[322] ^ 96) + 7) % 255 == 70)
s.add(((FLAG[321] ^ 70) + 8) % 255 == 50)
s.add(((FLAG[320] ^ 50) + 9) % 255 == 12)
s.add(((FLAG[319] ^ 12) + 10) % 255 == 130)
s.add(((FLAG[318] ^ 130) + 11) % 255 == 2)
s.add(((FLAG[317] ^ 2) + 12) % 255 == 122)
s.add(((FLAG[316] ^ 122) + 13) % 255 == 86)
s.add(((FLAG[315] ^ 86) + 14) % 255 == 23)
s.add(((FLAG[314] ^ 23) + 15) % 255 == 142)
s.add(((FLAG[313] ^ 142) + 16) % 255 == 0)
s.add(((FLAG[312] ^ 0) + 17) % 255 == 131)
s.add(((FLAG[311] ^ 131) + 18) % 255 == 249)
s.add(((FLAG[310] ^ 249) + 19) % 255 == 175)
s.add(((FLAG[309] ^ 175) + 20) % 255 == 241)
s.add(((FLAG[308] ^ 241) + 21) % 255 == 161)
s.add(((FLAG[307] ^ 161) + 22) % 255 == 193)
s.add(((FLAG[306] ^ 193) + 23) % 255 == 172)
s.add(((FLAG[305] ^ 172) + 24) % 255 == 220)
s.add(((FLAG[304] ^ 220) + 25) % 255 == 210)
s.add(((FLAG[303] ^ 210) + 26) % 255 == 13)
s.add(((FLAG[302] ^ 13) + 27) % 255 == 118)
s.add(((FLAG[301] ^ 118) + 28) % 255 == 59)
s.add(((FLAG[300] ^ 59) + 29) % 255 == 121)
s.add(((FLAG[299] ^ 121) + 30) % 255 == 58)
s.add(((FLAG[298] ^ 58) + 31) % 255 == 115)
s.add(((FLAG[297] ^ 115) + 32) % 255 == 54)
s.add(((FLAG[296] ^ 54) + 33) % 255 == 101)
s.add(((FLAG[295] ^ 101) + 34) % 255 == 34)
s.add(((FLAG[294] ^ 34) + 35) % 255 == 37)
s.add(((FLAG[293] ^ 37) + 36) % 255 == 106)
s.add(((FLAG[292] ^ 106) + 37) % 255 == 40)
s.add(((FLAG[291] ^ 40) + 38) % 255 == 126)
s.add(((FLAG[290] ^ 126) + 39) % 255 == 61)
s.add(((FLAG[289] ^ 61) + 40) % 255 == 128)
s.add(((FLAG[288] ^ 128) + 41) % 255 == 28)
s.add(((FLAG[287] ^ 28) + 42) % 255 == 102)
s.add(((FLAG[286] ^ 102) + 43) % 255 == 58)
s.add(((FLAG[285] ^ 58) + 44) % 255 == 117)
s.add(((FLAG[284] ^ 117) + 45) % 255 == 130)
s.add(((FLAG[283] ^ 130) + 46) % 255 == 18)
s.add(((FLAG[282] ^ 18) + 47) % 255 == 97)
s.add(((FLAG[281] ^ 97) + 48) % 255 == 60)
s.add(((FLAG[280] ^ 60) + 49) % 255 == 138)
s.add(((FLAG[279] ^ 138) + 50) % 255 == 49)
s.add(((FLAG[278] ^ 49) + 51) % 255 == 140)
s.add(((FLAG[277] ^ 140) + 52) % 255 == 24)
s.add(((FLAG[276] ^ 24) + 53) % 255 == 177)
s.add(((FLAG[275] ^ 177) + 54) % 255 == 199)
s.add(((FLAG[274] ^ 199) + 55) % 255 == 223)
s.add(((FLAG[273] ^ 223) + 56) % 255 == 241)
s.add(((FLAG[272] ^ 241) + 57) % 255 == 11)
s.add(((FLAG[271] ^ 11) + 58) % 255 == 168)
# s.add(((FLAG[270] ^ 168) + 59) % 255 == 2)
# s.add(((FLAG[269] ^ 2) + 60) % 255 == 157)
# s.add(((FLAG[268] ^ 157) + 61) % 255 == 45)
# s.add(((FLAG[267] ^ 45) + 62) % 255 == 146)
# s.add(((FLAG[266] ^ 146) + 63) % 255 == 34)
# s.add(((FLAG[265] ^ 34) + 64) % 255 == 150)
# s.add(((FLAG[264] ^ 150) + 65) % 255 == 65)
# s.add(((FLAG[263] ^ 65) + 66) % 255 == 113)
# s.add(((FLAG[262] ^ 113) + 67) % 255 == 89)
# s.add(((FLAG[261] ^ 89) + 68) % 255 == 189)
# s.add(((FLAG[260] ^ 189) + 69) % 255 == 34)
# s.add(((FLAG[259] ^ 34) + 70) % 255 == 148)
# s.add(((FLAG[258] ^ 148) + 71) % 255 == 44)
# s.add(((FLAG[257] ^ 44) + 72) % 255 == 140)
# s.add(((FLAG[256] ^ 140) + 73) % 255 == 55)
# s.add(((FLAG[255] ^ 55) + 74) % 255 == 159)
# s.add(((FLAG[254] ^ 159) + 75) % 255 == 70)
# s.add(((FLAG[253] ^ 70) + 76) % 255 == 126)
# s.add(((FLAG[252] ^ 126) + 77) % 255 == 100)
# s.add(((FLAG[251] ^ 100) + 78) % 255 == 85)
# s.add(((FLAG[250] ^ 85) + 79) % 255 == 196)
# s.add(((FLAG[249] ^ 196) + 80) % 255 == 1)
# s.add(((FLAG[248] ^ 1) + 81) % 255 == 181)
# s.add(((FLAG[247] ^ 181) + 82) % 255 == 32)
# s.add(((FLAG[246] ^ 32) + 83) % 255 == 167)
# s.add(((FLAG[245] ^ 167) + 84) % 255 == 219)
# s.add(((FLAG[244] ^ 219) + 85) % 255 == 2)
# s.add(((FLAG[243] ^ 2) + 86) % 255 == 192)
# s.add(((FLAG[242] ^ 192) + 87) % 255 == 252)
# s.add(((FLAG[241] ^ 252) + 88) % 255 == 230)
# s.add(((FLAG[240] ^ 230) + 89) % 255 == 220)
# s.add(((FLAG[239] ^ 220) + 90) % 255 == 87)
# s.add(((FLAG[238] ^ 87) + 91) % 255 == 141)
# s.add(((FLAG[237] ^ 141) + 92) % 255 == 73)
# s.add(((FLAG[236] ^ 73) + 93) % 255 == 135)
# s.add(((FLAG[235] ^ 135) + 94) % 255 == 78)
# s.add(((FLAG[234] ^ 78) + 95) % 255 == 205)
# s.add(((FLAG[233] ^ 205) + 96) % 255 == 2)
# s.add(((FLAG[232] ^ 2) + 97) % 255 == 200)
# s.add(((FLAG[231] ^ 200) + 98) % 255 == 31)
# s.add(((FLAG[230] ^ 31) + 99) % 255 == 206)
# s.add(((FLAG[229] ^ 206) + 100) % 255 == 16)
# s.add(((FLAG[228] ^ 16) + 101) % 255 == 199)
# s.add(((FLAG[227] ^ 199) + 102) % 255 == 78)
# s.add(((FLAG[226] ^ 78) + 103) % 255 == 136)
# s.add(((FLAG[225] ^ 136) + 104) % 255 == 87)
# s.add(((FLAG[224] ^ 87) + 105) % 255 == 224)
# s.add(((FLAG[223] ^ 224) + 106) % 255 == 254)
# s.add(((FLAG[222] ^ 254) + 107) % 255 == 2)
# s.add(((FLAG[221] ^ 2) + 108) % 255 == 211)
# s.add(((FLAG[220] ^ 211) + 109) % 255 == 97)
# s.add(((FLAG[219] ^ 97) + 110) % 255 == 127)
# s.add(((FLAG[218] ^ 127) + 111) % 255 == 130)
# s.add(((FLAG[217] ^ 130) + 112) % 255 == 84)
# s.add(((FLAG[216] ^ 84) + 113) % 255 == 174)
# s.add(((FLAG[215] ^ 174) + 114) % 255 == 51)
# s.add(((FLAG[214] ^ 51) + 115) % 255 == 186)
# s.add(((FLAG[213] ^ 186) + 116) % 255 == 84)
# s.add(((FLAG[212] ^ 84) + 117) % 255 == 161)
# s.add(((FLAG[211] ^ 161) + 118) % 255 == 76)
# s.add(((FLAG[210] ^ 76) + 119) % 255 == 227)
# s.add(((FLAG[209] ^ 227) + 120) % 255 == 98)
# s.add(((FLAG[208] ^ 98) + 121) % 255 == 132)
# s.add(((FLAG[207] ^ 132) + 122) % 255 == 114)
# s.add(((FLAG[206] ^ 114) + 123) % 255 == 205)
# s.add(((FLAG[205] ^ 205) + 124) % 255 == 37)
# s.add(((FLAG[204] ^ 37) + 125) % 255 == 200)
# s.add(((FLAG[203] ^ 200) + 126) % 255 == 42)
# s.add(((FLAG[202] ^ 42) + 127) % 255 == 196)
# s.add(((FLAG[201] ^ 196) + 128) % 255 == 33)
# s.add(((FLAG[200] ^ 33) + 129) % 255 == 197)
# s.add(((FLAG[199] ^ 197) + 130) % 255 == 36)
# s.add(((FLAG[198] ^ 36) + 131) % 255 == 135)
# s.add(((FLAG[197] ^ 135) + 132) % 255 == 117)
# s.add(((FLAG[196] ^ 117) + 133) % 255 == 161)
# s.add(((FLAG[195] ^ 161) + 134) % 255 == 92)
# s.add(((FLAG[194] ^ 92) + 135) % 255 == 187)
# s.add(((FLAG[193] ^ 187) + 136) % 255 == 36)
# s.add(((FLAG[192] ^ 36) + 137) % 255 == 206)
# s.add(((FLAG[191] ^ 206) + 138) % 255 == 121)
# s.add(((FLAG[190] ^ 121) + 139) % 255 == 168)
# s.add(((FLAG[189] ^ 168) + 140) % 255 == 78)
# s.add(((FLAG[188] ^ 78) + 141) % 255 == 181)
# s.add(((FLAG[187] ^ 181) + 142) % 255 == 98)
# s.add(((FLAG[186] ^ 98) + 143) % 255 == 150)
# s.add(((FLAG[185] ^ 150) + 144) % 255 == 117)
# s.add(((FLAG[184] ^ 117) + 145) % 255 == 161)
# s.add(((FLAG[183] ^ 161) + 146) % 255 == 98)
# s.add(((FLAG[182] ^ 98) + 147) % 255 == 169)
# s.add(((FLAG[181] ^ 169) + 148) % 255 == 30)
# s.add(((FLAG[180] ^ 30) + 149) % 255 == 242)
# s.add(((FLAG[179] ^ 242) + 150) % 255 == 42)
# s.add(((FLAG[178] ^ 42) + 151) % 255 == 230)
# s.add(((FLAG[177] ^ 230) + 152) % 255 == 46)
# s.add(((FLAG[176] ^ 46) + 153) % 255 == 232)
# s.add(((FLAG[175] ^ 232) + 154) % 255 == 53)
# s.add(((FLAG[174] ^ 53) + 155) % 255 == 176)
# s.add(((FLAG[173] ^ 176) + 156) % 255 == 112)
# s.add(((FLAG[172] ^ 112) + 157) % 255 == 182)
# s.add(((FLAG[171] ^ 182) + 158) % 255 == 101)
# s.add(((FLAG[170] ^ 101) + 159) % 255 == 172)
# s.add(((FLAG[169] ^ 172) + 160) % 255 == 106)
# s.add(((FLAG[168] ^ 106) + 161) % 255 == 185)
# s.add(((FLAG[167] ^ 185) + 162) % 255 == 56)
# s.add(((FLAG[166] ^ 56) + 163) % 255 == 187)
# s.add(((FLAG[165] ^ 187) + 164) % 255 == 113)
# s.add(((FLAG[164] ^ 113) + 165) % 255 == 190)
# s.add(((FLAG[163] ^ 190) + 166) % 255 == 120)
# s.add(((FLAG[162] ^ 120) + 167) % 255 == 178)
# s.add(((FLAG[161] ^ 178) + 168) % 255 == 128)
# s.add(((FLAG[160] ^ 128) + 169) % 255 == 74)
# s.add(((FLAG[159] ^ 74) + 170) % 255 == 205)
# s.add(((FLAG[158] ^ 205) + 171) % 255 == 79)
# s.add(((FLAG[157] ^ 79) + 172) % 255 == 216)
# s.add(((FLAG[156] ^ 216) + 173) % 255 == 88)
# s.add(((FLAG[155] ^ 88) + 174) % 255 == 235)
# s.add(((FLAG[154] ^ 235) + 175) % 255 == 54)
# s.add(((FLAG[153] ^ 54) + 176) % 255 == 4)
# s.add(((FLAG[152] ^ 4) + 177) % 255 == 28)
# s.add(((FLAG[151] ^ 28) + 178) % 255 == 27)
# s.add(((FLAG[150] ^ 27) + 179) % 255 == 238)
# s.add(((FLAG[149] ^ 238) + 180) % 255 == 60)
# s.add(((FLAG[148] ^ 60) + 181) % 255 == 5)
# s.add(((FLAG[147] ^ 5) + 182) % 255 == 219)
# s.add(((FLAG[146] ^ 219) + 183) % 255 == 119)
# s.add(((FLAG[145] ^ 119) + 184) % 255 == 202)
# s.add(((FLAG[144] ^ 202) + 185) % 255 == 120)
# s.add(((FLAG[143] ^ 120) + 186) % 255 == 215)
# s.add(((FLAG[142] ^ 215) + 187) % 255 == 97)
# s.add(((FLAG[141] ^ 97) + 188) % 255 == 200)
# s.add(((FLAG[140] ^ 200) + 189) % 255 == 95)
# s.add(((FLAG[139] ^ 95) + 190) % 255 == 239)
# s.add(((FLAG[138] ^ 239) + 191) % 255 == 74)
# s.add(((FLAG[137] ^ 74) + 192) % 255 == 238)
# s.add(((FLAG[136] ^ 238) + 193) % 255 == 144)
# s.add(((FLAG[135] ^ 144) + 194) % 255 == 181)
# s.add(((FLAG[134] ^ 181) + 195) % 255 == 144)
# s.add(((FLAG[133] ^ 144) + 196) % 255 == 117)
# s.add(((FLAG[132] ^ 117) + 197) % 255 == 198)
# s.add(((FLAG[131] ^ 198) + 198) % 255 == 117)
# s.add(((FLAG[130] ^ 117) + 199) % 255 == 215)
# s.add(((FLAG[129] ^ 215) + 200) % 255 == 192)
# s.add(((FLAG[128] ^ 192) + 201) % 255 == 109)
# s.add(((FLAG[127] ^ 109) + 202) % 255 == 204)
# s.add(((FLAG[126] ^ 204) + 203) % 255 == 138)
# s.add(((FLAG[125] ^ 138) + 204) % 255 == 197)
# s.add(((FLAG[124] ^ 197) + 205) % 255 == 110)
# s.add(((FLAG[123] ^ 110) + 206) % 255 == 235)
# s.add(((FLAG[122] ^ 235) + 207) % 255 == 107)
# s.add(((FLAG[121] ^ 107) + 208) % 255 == 212)
# s.add(((FLAG[120] ^ 212) + 209) % 255 == 140)
# s.add(((FLAG[119] ^ 140) + 210) % 255 == 187)
# s.add(((FLAG[118] ^ 187) + 211) % 255 == 166)
# s.add(((FLAG[117] ^ 166) + 212) % 255 == 157)
# s.add(((FLAG[116] ^ 157) + 213) % 255 == 208)
# s.add(((FLAG[115] ^ 208) + 214) % 255 == 199)
# s.add(((FLAG[114] ^ 199) + 215) % 255 == 165)
# s.add(((FLAG[113] ^ 165) + 216) % 255 == 162)
# s.add(((FLAG[112] ^ 162) + 217) % 255 == 161)
# s.add(((FLAG[111] ^ 161) + 218) % 255 == 176)
# s.add(((FLAG[110] ^ 176) + 219) % 255 == 160)
# s.add(((FLAG[109] ^ 160) + 220) % 255 == 162)
# s.add(((FLAG[108] ^ 162) + 221) % 255 == 174)
# s.add(((FLAG[107] ^ 174) + 222) % 255 == 109)
# s.add(((FLAG[106] ^ 109) + 223) % 255 == 225)
# s.add(((FLAG[105] ^ 225) + 224) % 255 == 104)
# s.add(((FLAG[104] ^ 104) + 225) % 255 == 42)
# s.add(((FLAG[103] ^ 42) + 226) % 255 == 46)
# s.add(((FLAG[102] ^ 46) + 227) % 255 == 36)
# s.add(((FLAG[101] ^ 36) + 228) % 255 == 48)
# s.add(((FLAG[100] ^ 48) + 229) % 255 == 42)
# s.add(((FLAG[99] ^ 42) + 230) % 255 == 41)
# s.add(((FLAG[98] ^ 41) + 231) % 255 == 52)
# s.add(((FLAG[97] ^ 52) + 232) % 255 == 47)
# s.add(((FLAG[96] ^ 47) + 233) % 255 == 248)
# s.add(((FLAG[95] ^ 248) + 234) % 255 == 119)
# s.add(((FLAG[94] ^ 119) + 235) % 255 == 253)
# s.add(((FLAG[93] ^ 253) + 236) % 255 == 114)
# s.add(((FLAG[92] ^ 114) + 237) % 255 == 243)
# s.add(((FLAG[91] ^ 243) + 238) % 255 == 206)
# s.add(((FLAG[90] ^ 206) + 239) % 255 == 222)
# s.add(((FLAG[89] ^ 222) + 240) % 255 == 155)
# s.add(((FLAG[88] ^ 155) + 241) % 255 == 229)
# s.add(((FLAG[87] ^ 229) + 242) % 255 == 115)
# s.add(((FLAG[86] ^ 115) + 243) % 255 == 71)
# s.add(((FLAG[85] ^ 71) + 244) % 255 == 33)
# s.add(((FLAG[84] ^ 33) + 245) % 255 == 58)
# s.add(((FLAG[83] ^ 58) + 246) % 255 == 58)
# s.add(((FLAG[82] ^ 58) + 247) % 255 == 12)
# s.add(((FLAG[81] ^ 12) + 248) % 255 == 254)
# s.add(((FLAG[80] ^ 254) + 249) % 255 == 164)
# s.add(((FLAG[79] ^ 164) + 250) % 255 == 199)
# s.add(((FLAG[78] ^ 199) + 251) % 255 == 158)
# s.add(((FLAG[77] ^ 158) + 252) % 255 == 187)
# s.add(((FLAG[76] ^ 187) + 253) % 255 == 235)
# s.add(((FLAG[75] ^ 235) + 254) % 255 == 129)
# s.add(((FLAG[74] ^ 129) + 0) % 255 == 230)
# s.add(((FLAG[73] ^ 230) + 1) % 255 == 132)
# s.add(((FLAG[72] ^ 132) + 2) % 255 == 236)
# s.add(((FLAG[71] ^ 236) + 3) % 255 == 140)
# s.add(((FLAG[70] ^ 140) + 4) % 255 == 3)
# s.add(((FLAG[69] ^ 3) + 5) % 255 == 107)
# s.add(((FLAG[68] ^ 107) + 6) % 255 == 81)
# s.add(((FLAG[67] ^ 81) + 7) % 255 == 57)
# s.add(((FLAG[66] ^ 57) + 8) % 255 == 88)
# s.add(((FLAG[65] ^ 88) + 9) % 255 == 49)
# s.add(((FLAG[64] ^ 49) + 10) % 255 == 99)
# s.add(((FLAG[63] ^ 99) + 11) % 255 == 17)
# s.add(((FLAG[62] ^ 17) + 12) % 255 == 111)
# s.add(((FLAG[61] ^ 111) + 13) % 255 == 92)
# s.add(((FLAG[60] ^ 92) + 14) % 255 == 67)
# s.add(((FLAG[59] ^ 67) + 15) % 255 == 63)
# s.add(((FLAG[58] ^ 63) + 16) % 255 == 47)
# s.add(((FLAG[57] ^ 47) + 17) % 255 == 108)
# s.add(((FLAG[56] ^ 108) + 18) % 255 == 22)
# s.add(((FLAG[55] ^ 22) + 19) % 255 == 134)
# s.add(((FLAG[54] ^ 134) + 20) % 255 == 9)
# s.add(((FLAG[53] ^ 9) + 21) % 255 == 129)
# s.add(((FLAG[52] ^ 129) + 22) % 255 == 253)
# s.add(((FLAG[51] ^ 253) + 23) % 255 == 169)
# s.add(((FLAG[50] ^ 169) + 24) % 255 == 243)
# s.add(((FLAG[49] ^ 243) + 25) % 255 == 175)
# s.add(((FLAG[48] ^ 175) + 26) % 255 == 169)
# s.add(((FLAG[47] ^ 169) + 27) % 255 == 227)
# s.add(((FLAG[46] ^ 227) + 28) % 255 == 223)
# s.add(((FLAG[45] ^ 223) + 29) % 255 == 201)
# s.add(((FLAG[44] ^ 201) + 30) % 255 == 215)
# s.add(((FLAG[43] ^ 215) + 31) % 255 == 209)
# s.add(((FLAG[42] ^ 209) + 32) % 255 == 210)
# s.add(((FLAG[41] ^ 210) + 33) % 255 == 220)
# s.add(((FLAG[40] ^ 220) + 34) % 255 == 223)
# s.add(((FLAG[39] ^ 223) + 35) % 255 == 214)
# s.add(((FLAG[38] ^ 214) + 36) % 255 == 27)
# s.add(((FLAG[37] ^ 27) + 37) % 255 == 157)
# s.add(((FLAG[36] ^ 157) + 38) % 255 == 35)
# s.add(((FLAG[35] ^ 35) + 39) % 255 == 119)
# s.add(((FLAG[34] ^ 119) + 40) % 255 == 58)
# s.add(((FLAG[33] ^ 58) + 41) % 255 == 67)
# s.add(((FLAG[32] ^ 67) + 42) % 255 == 86)
# s.add(((FLAG[31] ^ 86) + 43) % 255 == 91)
# s.add(((FLAG[30] ^ 91) + 44) % 255 == 167)
# s.add(((FLAG[29] ^ 167) + 45) % 255 == 243)
# s.add(((FLAG[28] ^ 243) + 46) % 255 == 2)
# s.add(((FLAG[27] ^ 2) + 47) % 255 == 161)
# s.add(((FLAG[26] ^ 161) + 48) % 255 == 254)
# s.add(((FLAG[25] ^ 254) + 49) % 255 == 195)
# s.add(((FLAG[24] ^ 195) + 50) % 255 == 236)
# s.add(((FLAG[23] ^ 236) + 51) % 255 == 192)
# s.add(((FLAG[22] ^ 192) + 52) % 255 == 224)
# s.add(((FLAG[21] ^ 224) + 53) % 255 == 197)
# s.add(((FLAG[20] ^ 197) + 54) % 255 == 227)
# s.add(((FLAG[19] ^ 227) + 55) % 255 == 185)
# s.add(((FLAG[18] ^ 185) + 56) % 255 == 20)
# s.add(((FLAG[17] ^ 20) + 57) % 255 == 170)
# s.add(((FLAG[16] ^ 170) + 58) % 255 == 25)
# s.add(((FLAG[15] ^ 25) + 59) % 255 == 171)
# s.add(((FLAG[14] ^ 171) + 60) % 255 == 5)
# s.add(((FLAG[13] ^ 5) + 61) % 255 == 98)
# s.add(((FLAG[12] ^ 98) + 62) % 255 == 79)
# s.add(((FLAG[11] ^ 79) + 63) % 255 == 121)
# s.add(((FLAG[10] ^ 121) + 64) % 255 == 91)
# s.add(((FLAG[9] ^ 91) + 65) % 255 == 105)
# s.add(((FLAG[8] ^ 105) + 66) % 255 == 95)
# s.add(((FLAG[7] ^ 95) + 67) % 255 == 121)
# s.add(((FLAG[6] ^ 121) + 68) % 255 == 81)
# s.add(((FLAG[5] ^ 81) + 69) % 255 == 105)
# s.add(((FLAG[4] ^ 105) + 70) % 255 == 99)
# s.add(((FLAG[3] ^ 99) + 71) % 255 == 81)
# s.add(((FLAG[2] ^ 81) + 72) % 255 == 134)
# s.add(((FLAG[1] ^ 134) + 73) % 255 == 50)
# s.add(((FLAG[0] ^ 50) + 74) % 255 == 102)
if s.check() == unsat:
print('unsat')
exit(-1)
model = s.model()
print('flag:')
for x in reversed(FLAG):
print(chr(model[x].as_long()), end='')
print()