-
Notifications
You must be signed in to change notification settings - Fork 0
/
check_found_solutions.c
2179 lines (1899 loc) · 103 KB
/
check_found_solutions.c
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
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
#include <dirent.h>
#include <stdio.h>
#include <string.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <unistd.h>
#include <fcntl.h>
#include <stdlib.h>
// #include "sha256.h"
#include "eter172c.c"
#include "e2_info.c"
// #define RUN_FAST 1
#define CHECK_WITH_256
unsigned char ring[] =
{ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0,
0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 0,
0, 1, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 1, 0,
0, 1, 2, 3, 4, 4, 4, 4, 4, 4, 4, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 5, 5, 5, 5, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 6, 6, 6, 6, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 6, 7, 7, 6, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 6, 7, 7, 6, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 6, 6, 6, 6, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 5, 5, 5, 5, 5, 5, 4, 3, 2, 1, 0,
0, 1, 2, 3, 4, 4, 4, 4, 4, 4, 4, 4, 3, 2, 1, 0,
0, 1, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 1, 0,
0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 0,
0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 };
typedef enum
{
INFO_UNKNOWN_COMBINATION = 0,
INFO_PREVIOUSLY_USED_COMBINATION = 1,
INFO_FORBIDDEN_COMBINATION = 2,
INFO_FORBIDDEN_EASY_COMBINATION = 3
} enumInfoCombination;
unsigned char *forbiddenCombinations[1 + NR_OF_SAT_VARIABLES];
unsigned long fieldMin[NR_OF_FIELDS];
unsigned long fieldMax[NR_OF_FIELDS];
unsigned long nrOfForbiddenCombinations = 0;
unsigned long nrOfForbiddenEasyCombinations = 0;
unsigned long nrOfPreviouslyUsedCombinations = 0;
unsigned char *usedCombinationsCounter[1 + 130180];
unsigned long diffInvalid[NR_OF_FIELDS];
unsigned long totalSolutions = 0;
unsigned long totalInvalidSolutions = 0;
unsigned long usedIndizes[256];
unsigned long nrOfUsedIndizes = 0;
int checkSolutions(char *filename);
int checkAgainstCmsRedFile(char *filename);
int importUnsatFile(char *filename);
int GetRing(int index)
{
return(ring[combinations[index-1].Field]);
}
unsigned char string_starts_with(char *string, char *searchstring)
{
if(strncmp(string, searchstring, strlen(searchstring)) == 0)
{
return 1;
}
return 0;
}
unsigned char string_ends_with(char *string, char *searchstring)
{
if(strlen(searchstring) > strlen(string))
{
return 0;
}
if(strncmp(string+strlen(string)-strlen(searchstring), searchstring, strlen(searchstring)) == 0)
{
return 1;
}
return 0;
}
int main(void)
{
memset(usedCombinationsCounter, 0, sizeof(usedCombinationsCounter));
for(int i = 1; i <= NR_OF_SAT_VARIABLES; i++)
{
usedCombinationsCounter[i] = malloc((i + 1) * sizeof(usedCombinationsCounter[0][0]));
memset(&usedCombinationsCounter[i][0], 0, (i + 1) * sizeof(usedCombinationsCounter[0][0]));
}
memset(diffInvalid, 0, sizeof(diffInvalid));
memset(forbiddenCombinations, 0, sizeof(forbiddenCombinations));
for(int i = 1; i <= NR_OF_SAT_VARIABLES; i++)
{
forbiddenCombinations[i] = malloc((i + 1) * sizeof(forbiddenCombinations[0][0]));
memset(&forbiddenCombinations[i][0], 0, (i + 1) * sizeof(forbiddenCombinations[0][0]));
}
for(int i = 0; i < NR_OF_FIELDS; i++)
{
fieldMin[i] = NR_OF_SAT_VARIABLES + 1;
fieldMax[i] = 1 - 1;
}
for(int i = 1; i <= NR_OF_SAT_VARIABLES; i++)
{
if(i < fieldMin[combinations[i-1].Field]) fieldMin[combinations[i-1].Field] = i;
if(fieldMax[combinations[i-1].Field] < i) fieldMax[combinations[i-1].Field] = i;
}
for(int i = 0; i < 5; i++)
{
printf("c Field %d: min=%ld max=%ld\n", i, fieldMin[i], fieldMax[i]);
}
// Calculate easy forbidden combinations (e.g. same field, not suitable neighbour)
for(int i = 1; i <= NR_OF_SAT_VARIABLES; i++)
{
if((i % 1000) == 0) printf("c i=%d\n", i);
for(int j = i + 1; j <= NR_OF_SAT_VARIABLES; j++)
{
if(combinations[i-1].Field == combinations[j-1].Field);
else if(combinations[i-1].Card == combinations[j-1].Card);
else if((combinations[i-1].Field + 1) == combinations[j-1].Field && combinations[i-1].PatternEast != combinations[j-1].PatternWest);
else if((combinations[i-1].Field + 16) == combinations[j-1].Field && combinations[i-1].PatternSouth != combinations[j-1].PatternNorth);
else continue;
forbiddenCombinations[j][i] = INFO_FORBIDDEN_EASY_COMBINATION;
nrOfForbiddenEasyCombinations++;
}
}
printf("c Memory initialized\n");
setvbuf(stdout, (char*)NULL, _IONBF, 0);
#if 1
importUnsatFile("e2_found_invalid_clauses_round_1.cnf");
importUnsatFile("e2_found_invalid_clauses_round_2.cnf");
importUnsatFile("e2_found_invalid_clauses_round_3.cnf");
importUnsatFile("e2_found_invalid_clauses_round_4.cnf");
importUnsatFile("e2_found_invalid_clauses_round_5.cnf");
importUnsatFile("e2_found_invalid_clauses_round_6.cnf");
importUnsatFile("e2_found_invalid_clauses_round_7.cnf");
importUnsatFile("e2_found_invalid_clauses_round_8.cnf");
importUnsatFile("e2_found_invalid_clauses_round_9.cnf");
// importUnsatFile("e2_unsat_202104151313.cnf");
// importUnsatFile("e2_unsat_unred_202107050830_all_clauses.cnf");
// importUnsatFile("e2_found_invalid_clauses_round_55.cnf");
// importUnsatFile("e2_found_invalid_clauses_round_56.cnf");
// importUnsatFile("e2_found_invalid_clauses_round_57.cnf");
// importUnsatFile("e2_found_invalid_clauses_round_58.cnf");
// importUnsatFile("e2_found_invalid_clauses_round_59.cnf");
// importUnsatFile("e2_unsat_unred_202108011651.cnf");
// importUnsatFile("e2_unsat_unred_202108141059.cnf");
// importUnsatFile("e2_unsat_unred_202108141402.cnf");
// importUnsatFile("e2_unsat_unred_202108141949.cnf");
// importUnsatFile("e2_unsat_unred_202108150914.cnf");
// importUnsatFile("e2_unsat_unred_202108151542.cnf");
// importUnsatFile("e2_unsat_unred_202108152136.cnf");
// importUnsatFile("e2_unsat_unred_202108160716.cnf");
// importUnsatFile("e2_unsat_unred_202108162226.cnf");
// importUnsatFile("e2_unsat_unred_202108170716.cnf");
// importUnsatFile("e2_unsat_unred_202108180704.cnf");
// importUnsatFile("e2_unsat_unred_202108181212.cnf");
importUnsatFile("e2_unsat_unred_202108181919.cnf");
importUnsatFile("e2_unsat_unred_202108182112.cnf");
importUnsatFile("e2_unsat_unred_202108190440.cnf");
importUnsatFile("e2_unsat_unred_202108191034.cnf");
importUnsatFile("e2_unsat_unred_202108202148.cnf");
importUnsatFile("e2_unsat_unred_202108210702.cnf");
importUnsatFile("e2_unsat_unred_202108212214.cnf");
importUnsatFile("e2_unsat_manually_found_202108221228.cnf");
importUnsatFile("e2_unsat_unred_202108220834.cnf");
importUnsatFile("e2_unsat_unred_202108221248.cnf");
importUnsatFile("e2_unsat_unred_202108221942.cnf");
// Broken file!!! Thanks to Akos!!! Later files can be influenced!!!
// importUnsatFile("e2_unsat_from_earlier_directory_202107280724.cnf");
importUnsatFile("e2_unsat_unred_202108230600.cnf");
importUnsatFile("e2_unsat_unred_202108231055.cnf");
importUnsatFile("e2_unsat_unred_202108231928.cnf");
importUnsatFile("e2_unsat_unred_202108240701.cnf");
importUnsatFile("e2_unsat_unred_202108242129.cnf");
importUnsatFile("e2_unsat_unred_202108251024.cnf");
importUnsatFile("e2_unsat_unred_202108252255.cnf");
importUnsatFile("e2_found_invalid_clauses_202108251032.cnf");
importUnsatFile("e2_unsat_unred_202108260720.cnf");
importUnsatFile("e2_unsat_unred_202108260720.cnf");
importUnsatFile("e2_found_invalid_clauses_202108260727.cnf");
importUnsatFile("e2_unsat_unred_202108262325.cnf");
importUnsatFile("e2_unsat_unred_202108270833.cnf");
importUnsatFile("e2_unsat_unred_202108281649.cnf");
importUnsatFile("e2_unsat_unred_202108291127.cnf");
importUnsatFile("e2_unsat_unred_202108292108.cnf");
importUnsatFile("e2_unsat_unred_202108300628.cnf");
importUnsatFile("e2_found_invalid_clauses_202108300628.cnf");
importUnsatFile("e2_unsat_unred_202108302136.cnf");
importUnsatFile("e2_unsat_unred_202108310649.cnf");
importUnsatFile("e2_unsat_unred_202108312210.cnf");
importUnsatFile("e2_unsat_unred_202109010839.cnf");
importUnsatFile("e2_unsat_unred_202109012052.cnf");
importUnsatFile("e2_unsat_unred_202109020737.cnf");
importUnsatFile("e2_unsat_unred_202109022231.cnf");
importUnsatFile("e2_unsat_unred_202109031643.cnf");
importUnsatFile("e2_unsat_unred_202109041000.cnf");
importUnsatFile("e2_found_invalid_clauses_202109041000.cnf");
importUnsatFile("e2_unsat_unred_202109050650.cnf");
importUnsatFile("e2_unsat_unred_202109051857.cnf");
importUnsatFile("e2_unsat_unred_202109060748.cnf");
importUnsatFile("e2_unsat_unred_202109062247.cnf");
importUnsatFile("e2_unsat_unred_202109071430.cnf");
importUnsatFile("e2_unsat_unred_202109080711.cnf");
importUnsatFile("e2_unsat_unred_202109082200.cnf");
importUnsatFile("e2_unsat_unred_202109090809.cnf");
importUnsatFile("e2_unsat_unred_202109092258.cnf");
importUnsatFile("e2_unsat_unred_202109102140.cnf");
importUnsatFile("e2_unsat_unred_202109111208.cnf");
importUnsatFile("e2_unsat_unred_202109120716.cnf");
importUnsatFile("e2_unsat_unred_202109122155.cnf");
// Each clause of the following file is manually verified
importUnsatFile("e2_unsat_unred_duplicate_runs_202109122215.cnf");
importUnsatFile("e2_unsat_unred_202109132136.cnf");
importUnsatFile("e2_unsat_unred_202109150724.cnf");
#endif // 0
// UNSATUNSATUNSAT
printf("c Final %ld forbidden easy combinations (FILTERSTAT)\n", nrOfForbiddenEasyCombinations);
printf("c Final %ld forbidden combinations (FILTERSTAT)\n", nrOfForbiddenCombinations);
printf("c Final %ld previous used combinations (FILTERSTAT)\n", nrOfPreviouslyUsedCombinations);
totalSolutions = 0;
totalInvalidSolutions = 0;
// SEARCH36 (=9*4)
#if 0
{
#include "e2_partial_f0_f1_f2_f16_f17_f18_f32_f33_f34.c"
#include "e2_partial_f13_f14_f15_f29_f30_f31_f45_f46_f47.c"
#include "e2_partial_f208_f209_f210_f224_f225_f226_f240_f241_f242.c"
#include "e2_partial_f221_f222_f223_f237_f238_f239_f253_f254_f255.c"
for(int tl = 0; tl < 3084; tl++)
{
fprintf(stderr, "tl=%d\n", tl);
for(int tr = 0; tr < 3782; tr++)
{
// fprintf(stderr, "tl=%d,tr=%d\n", tl, tr);
fprintf(stderr, "tl=%d,tr=%d,totalSolutions=%ld\n", tl, tr, totalSolutions);
if(tr == 800) exit(1);
int abort = 0;
for(int i = 0; i < 9 && !abort; i++)
{
for(int j = 0; j < 9 && !abort; j++)
{
if(forbiddenCombinations[topright[tr][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
}
}
if(abort) continue;
for(int bl = 0; bl < 3195; bl++)
{
// fprintf(stderr, "tl=%d,tr=%d,bl=%d,totalSolutions=%ld\n", tl, tr, bl, totalSolutions);
int abort = 0;
for(int i = 0; i < 9 && !abort; i++)
{
for(int j = 0; j < 9 && !abort; j++)
{
if( forbiddenCombinations[topright[tr][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
else if(forbiddenCombinations[bottomleft[bl][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
}
}
if(abort) continue;
for(int br = 0; br < 2897; br++)
{
// fprintf(stderr, "tl=%d,tr=%d,bl=%d,br=%d\n", tl, tr, bl, br);
int abort = 0;
for(int i = 0; i < 9 && !abort; i++)
{
for(int j = 0; j < 9 && !abort; j++)
{
if( forbiddenCombinations[topright[tr][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
else if(forbiddenCombinations[bottomleft[bl][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
else if(forbiddenCombinations[bottomright[br][j]][topleft[tl][i]] != INFO_UNKNOWN_COMBINATION) abort = 1;
}
}
if(abort) continue;
#if 0
printf("SAT\n");
for(int i = 0; i < 9; i++)
{
printf("%ld ", topleft[tl][i]);
}
for(int i = 0; i < 9; i++)
{
printf("%ld ", topright[tr][i]);
}
for(int i = 0; i < 9; i++)
{
printf("%ld ", bottomleft[bl][i]);
}
for(int i = 0; i < 9; i++)
{
printf("%ld ", bottomright[br][i]);
}
printf("0\n");
#endif // 0
totalSolutions++;
// if(totalSolutions == 1000) exit(1);
}
}
}
}
}
#endif // 0
// checkSolutions("e2_new_2021_only_field_0_to_3_compressed.res");
// checkSolutions("e2_new_2021_only_field_0_to_4_compressed.res");
// checkSolutions("e2_new_2021_only_ring_0_with_e2_unsat_202102271051_only_sol_0.res");
// checkSolutions("e2_new_2021_only_ring_0_with_e2_unsat_202102271051.res");
// checkSolutions("e2_only_second_inside_set_8956_set_9009.res");
#if 0
checkSolutions("e2_only_second_inside_set_8956_set_9010.res");
checkSolutions("e2_only_second_inside_set_8956_set_9013.res");
checkSolutions("e2_only_second_inside_set_8956_set_9014.res");
checkSolutions("e2_only_second_inside_set_8956_set_9016.res");
checkSolutions("e2_only_second_inside_set_8956_set_9017.res");
checkSolutions("e2_only_second_inside_set_8956_set_9019.res");
checkSolutions("e2_only_second_inside_set_8956_set_9020.res");
checkSolutions("e2_only_second_inside_set_8956_set_9022.res");
checkSolutions("e2_only_second_inside_set_8956_set_9025.res");
checkSolutions("e2_only_second_inside_set_8956_set_9028.res");
checkSolutions("e2_only_second_inside_set_8956_set_9033.res");
checkSolutions("e2_only_second_inside_set_8956_set_9036.res");
checkSolutions("e2_only_second_inside_set_8956_set_9037.res");
checkSolutions("e2_only_second_inside_set_8956_set_9038.res");
checkSolutions("e2_only_second_inside_set_8956_set_9040.res");
checkSolutions("e2_only_second_inside_set_8956_set_9041.res");
checkSolutions("e2_only_second_inside_set_8956_set_9043.res");
checkSolutions("e2_only_second_inside_set_8956_set_9045.res");
checkSolutions("e2_only_second_inside_set_8956_set_9047.res");
checkSolutions("e2_only_second_inside_set_8956_set_9049.res");
checkSolutions("e2_only_second_inside_set_8956_set_9054.res");
#endif // 0
#if 0
checkSolutions("e2_new_2019_only_second_inside.res");
checkSolutions("e2_new_2019_only_second_inside_set_24830.res");
checkSolutions("e2_new_2019_only_second_inside_set_24831.res");
checkSolutions("e2_new_2019_only_second_inside_set_24832.res");
checkSolutions("e2_new_2019_only_second_inside_set_24833.res");
checkSolutions("e2_new_2019_only_second_inside_set_24834.res");
checkSolutions("e2_new_2019_only_second_inside_set_24835.res");
checkSolutions("e2_new_2019_only_second_inside_set_24836.res");
checkSolutions("e2_new_2019_only_second_inside_set_24837.res");
checkSolutions("e2_new_2019_only_second_inside_set_24838.res");
checkSolutions("e2_new_2019_only_second_inside_set_24839.res");
checkSolutions("e2_new_2019_only_second_inside_set_24840.res");
checkSolutions("e2_new_2019_only_second_inside_set_24841.res");
checkSolutions("e2_new_2019_only_second_inside_set_24842.res");
checkSolutions("e2_new_2019_only_second_inside_set_24843.res");
checkSolutions("e2_new_2019_only_second_inside_set_24844.res");
checkSolutions("e2_new_2019_only_second_inside_set_24845.res");
checkSolutions("e2_new_2019_only_second_inside_set_24846.res");
checkSolutions("e2_new_2019_only_second_inside_set_24847.res");
checkSolutions("e2_new_2019_only_second_inside_set_24848.res");
checkSolutions("e2_new_2019_only_second_inside_set_24849.res");
#endif // 0
#if 0
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101130728.res");
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101120924.res");
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101110932.res");
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101062023_transred_0_implicitmanip_0.res");
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101061118_transred_0_implicitmanip_0.res");
checkSolutions("e2_new_2019_only_second_inside_with_e2_unsat_202101042256_transred_0_implicitmanip_0.res");
checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202012170954.res");
checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202012170954.res");
#endif // 0
#if 0
checkSolutions("e2_test_partial_211_fields_set_1.res");
checkSolutions("e2_test_partial_211_fields_set_2.res");
checkSolutions("e2_test_partial_211_fields_set_3.res");
checkSolutions("e2_test_partial_211_fields_set_4.res");
#endif // 0
// checkSolutions("e2_partial_field_233_fields_filled_with_e2_unsat_202012120750.res");
// checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202012120750.res");
// checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202012120750.res");
#if 0
checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202012090857.res");
checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202012090857.res");
checkSolutions("e2_partial_field_233_fields_filled_with_e2_unsat_202012012203.res");
checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202012012203.res");
checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202012012203.res");
checkSolutions("e2_partial_field_235_fields_filled_with_e2_unsat_202011080724.res");
// exit(1);
checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202011221231.res");
checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202011221231.res");
// exit(1);
checkSolutions("e2_partial_field_233_fields_filled_with_e2_unsat_202011170001.res");
checkSolutions("e2_partial_field_231_fields_filled_with_e2_unsat_202011170001.res");
checkSolutions("e2_partial_field_229_fields_filled_with_e2_unsat_202011170001.res");
// exit(1);
checkSolutions("e2_partial_field_229_fields_filled_with_filter_4_unsat_5081_run1_set_9_run2.res");
checkSolutions("e2_partial_field_231_fields_filled_with_filter_4_unsat_5081_run1_set_9_run2.res");
checkSolutions("e2_partial_field_233_fields_filled_with_filter_4_unsat_5081_run1_set_9_run2.res");
checkSolutions("e2_partial_field_235_fields_filled_with_filter_4_unsat_5081_run1_set_9_run2.res");
#endif // 0
// checkSolutions("e2_test_partial_229_fields_5081_solutions.res");
#if 1
// checkSolutions("e2_partial_field_229_fields_filled_with_unsat_202008151148_and_202008151329.res");
// checkSolutions("e2_partial_field_229_fields_filled_with_unsat_202008231948_and_202008151329.res");
// checkSolutions("e2_partial_field_235_fields_filled_with_filter_4_unsat_5081_run1_set_22_run2.res");
// checkSolutions("e2_partial_field_235_fields_filled_with_filter_4_unsat_5081_run1_set_23_run2.res");
#endif // 0
// Invalidated!
// checkSolutions("e2_partial_field_lower_left_12_square_remaining_filled_edge_and_ring_2_and_ring_4_and_ring_6_completed_resextract_0_filter_4.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_202108020807.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_202108020807.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_202108020807.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_202108020807_resextract_0_ring_0_search_all_ring_0_ring_1.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_202108020807_resextract_11_ring_0_search_all_ring_0_ring_1.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_202108020807_resextract_21_ring_0_search_all_ring_0_ring_1.res");
// checkSolutions("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_202108020807_resextract_0_ring_0_search_all_ring_0_ring_1_ring_2_ring_3.res");
// checkSolutions("e2_new_2021_half_filled.res");
#if 0
for(int i = 0; i < NR_OF_SAT_VARIABLES; i++)
{
for(int j = i + 1; j < NR_OF_SAT_VARIABLES; j++)
{
if(usedCombinationsCounter[j][i] > 0)
{
printf("./runme_256_set_set_timeout.sh %6d %6d 180 OCCURANCE%03d\n", i, j, usedCombinationsCounter[j][i]);
}
}
}
#endif // 0
#if 0
// CMS 5.0.2
checkAgainstCmsRedFile("e2_red_202104051251.cnf");
checkAgainstCmsRedFile("e2_red_202104110748.cnf");
checkAgainstCmsRedFile("e2_red_202104151313.cnf");
checkAgainstCmsRedFile("e2_red_202104161001.cnf");
checkAgainstCmsRedFile("e2_red_202104170807.cnf");
checkAgainstCmsRedFile("e2_red_202104172221.cnf");
checkAgainstCmsRedFile("e2_red_202104180849.cnf");
// CMS 20210418
checkAgainstCmsRedFile("e2_red_current_cms_202104181055.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104190643.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104200653.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104202251.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104210937.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104220721.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104232109.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104242120.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104261432.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202104290815.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105011710.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105021926.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105061934.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105082148.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105112041.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105131322.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105150724.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105180805.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105210818.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105221238.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105250117.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105261906.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105272128.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105290828.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202105311113.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106011056.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106021058.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106022218.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106031030.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106032305.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106041132.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106051124.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106061216.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106062051.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106071055.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106081101.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106090009.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106090848.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106100711.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106101653.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106111141.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106112218.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106121132_marie_ubuntu.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106131108.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106131108_sls_16000.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106131108_transred_1_implicitmanip_1.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106140848.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106140848_sls_16000.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106140848_transred_1_implicitmanip_1.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106151227.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106151227_sls_16000.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106151227_transred_1_implicitmanip_1.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106170946.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106170946_transred_1_implicitmanip_1.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106181700.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106181700_transred_1_implicitmanip_1.cnf");
#endif // 0
// checkAgainstCmsRedFile("e2_red_current_cms_202106191557.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106191557_sls_16000.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106191557_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106202218_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106210628_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106210634_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106220755_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106220755_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106222139_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106222139_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106230800_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106230800_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106231633_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106231633_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106241029_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106241029_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106242033_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106242033_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106250706_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106250706_all_clauses_transred_1_implicitmanip_1.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106260830_all_clauses.cnf");
// checkAgainstCmsRedFile("e2_red_current_cms_202106260830_all_clauses_transred_1_implicitmanip_1.cnf");
#if 0
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_0_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_1_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_2_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_3_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_5_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_6_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_7_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_8_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_9_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_10_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_12_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_13_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_14_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_15_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_16_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_17_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_100_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_101_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_102_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_103_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_104_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_105_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_106_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_108_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_109_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_110_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_111_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_112_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_114_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_115_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_116_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106260921_r_117_all_clauses.cnf");
#endif // 0
#if 0
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_0_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_1_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_2_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_4_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_5_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_6_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_7_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_8_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_9_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_10_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_12_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_13_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_14_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_15_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_16_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_17_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_100_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_102_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_103_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_104_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_105_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_106_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_107_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_108_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_109_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_111_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_112_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_113_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_114_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_115_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_116_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106270841_r_117_all_clauses.cnf");
#endif // 0
#if 0
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_0_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_100_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_101_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_102_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_103_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_104_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_105_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_106_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_107_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_108_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_109_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_10_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_110_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_111_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_112_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_113_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_114_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_115_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_11_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_12_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_13_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_14_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_15_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_1_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_2_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_3_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_4_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_5_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_6_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_7_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_8_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106280938_r_9_all_clauses.cnf");
#endif // 0
#if 0
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_0_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_100_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_101_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_102_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_103_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_104_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_105_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_106_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_107_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_108_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_109_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_10_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_110_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_111_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_112_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_113_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_115_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_12_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_13_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_14_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_15_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_1_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_2_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_3_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_4_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_5_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_6_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_7_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_8_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_9_all_clauses.cnf");
#endif // 0
#if 0
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_0_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_100_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_101_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_102_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_103_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_104_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_105_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_106_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_107_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_108_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_109_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_10_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_110_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_111_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_112_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_113_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_115_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_12_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_13_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_14_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_15_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_1_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_2_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_3_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_4_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_5_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_6_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_7_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_8_all_clauses.cnf");
checkAgainstCmsRedFile("e2_red_current_cms_202106290838_r_9_all_clauses.cnf");
#endif // 0
// checkAgainstCmsRedFile("e2_test_202108011013_red.cnf");
// checkAgainstCmsRedFile("e2_unsat_unred_202105311102.cnf");
#if 0
checkAgainstCmsRedFile("e2_full_plus_arc_red_sky_concat.cnf");
checkAgainstCmsRedFile("e2_full_plus_arc_red_80_to_150_sky_concat.cnf");
checkAgainstCmsRedFile("e2_partial_0_to_4_red_0_to_1112_sky_concat.cnf");
checkAgainstCmsRedFile("e2_new_2019_with_e2_unsat_202101110932_red.cnf");
#endif // 0
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108141402_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108141402_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108141402_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108141949_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108141949_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108141949_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108150914_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108150914_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108150914_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108150914_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108151542_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108151542_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108151542_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108151542_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108152136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108152136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108152136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108152136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_holes_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_two_holes_left_right_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_two_holes_top_bottom_202108160716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108162226_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108162226_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108162226_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108170716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_epyc_202108170716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108170716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108170716_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108180704_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108180704_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108180704_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108180704_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108181212_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108181212_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108181212_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108181212_red.cnf");
// Ab hier Neustart der RED-Files, weil Problem mit allclauses!?!
// Wenn man nicht volles Feld mit allclauses nimmt, kommt es zu fehlerhaften Berechnungen!?!
// checkAgainstCmsRedFile("e2_new_2019_202108181919_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_holes_202108181919_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108181919_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108181919_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108181919_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108182112_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108182112_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108182112_red.cnf");
// This is old file with 1,4 million entries
// But it results only in 12000 new clauses
// Danger too big, to introduce new error
// we get same amount of new clauses by using CMS again and again
// checkAgainstCmsRedFile("e2_unsat_from_earlier_directory_202107280724_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108190440_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108190440_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108191034_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108191034_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108191034_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108191034_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108191749_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108191749_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108190440_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108191749_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108191749_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108192049_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108192049_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108192049_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108192049_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108192049_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108200653_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108200653_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108200653_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108200653_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108200653_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108201333_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108201333_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108201333_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108201333_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108201333_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108202148_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108202148_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108202148_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108202148_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108202148_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108210702_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108210702_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108210702_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108210702_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108210702_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108212214_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108212214_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108212214_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108212214_red.cnf");
// checkAgainstCmsRedFile("e2_unsat_manually_found_202108221228_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108220834_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108220834_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108220834_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108220834_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108220834_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108221248_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108221248_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108221248_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108221248_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108221248_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108221942_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108221942_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108221942_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108221942_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108221942_red.cnf");
// checkAgainstCmsRedFile("e2_unsat_found_earlier_202108231044_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108230600_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108230600_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108230600_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108230600_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108230600_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108231055_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108231055_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108231055_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108231055_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108231055_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108231928_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108231928_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108231928_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108231928_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108240701_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108240701_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108240701_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108240701_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108242129_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108242129_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108242129_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108242129_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108251024_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108252255_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108252255_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108252255_red.cnf");
// checkAgainstCmsRedFile("e2_found_invalid_clauses_202108251032_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108260720_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108260720_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108260720_red.cnf");
// checkAgainstCmsRedFile("e2_found_invalid_clauses_202108260727_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108262325_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108262325_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108262325_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108270833_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108270833_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108270833_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108281649_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108281649_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108281649_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108291127_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108291127_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108291127_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108291127_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108291127_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_and_ring_6_202108291127_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108292108_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108292108_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108292108_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108292108_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_and_ring_5_202108292108_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108300628_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108300628_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108300628_red.cnf");
// checkAgainstCmsRedFile("e2_found_invalid_clauses_202108300628_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108302136_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108302136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108302136_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108310649_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108310649_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108310649_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108310649_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108312210_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202108312210_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202108312210_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202108312210_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202109010839_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202109010839_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202109010839_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_only_ring_0_and_ring_1_and_ring_2_and_ring_3_and_ring_4_202109010839_red.cnf");
// checkAgainstCmsRedFile("e2_new_2019_202109012052_epyc_red.cnf");
// checkAgainstCmsRedFile("e2_new_2021_four_smaller_holes_202109012052_red.cnf");