L proof_size
1 4131
2 4229
3 4335
4 4335
5 4433
6 4437
7 4433
8 4433
9 4535
10 4535
11 4535
12 4535
13 4539
14 4535
15 4535
16 4535
17 4637
18 4641
19 4641
20 4641
21 4641
22 4641
23 4637
24 4641
25 4641
26 4637
27 4637
28 4641
29 4637
30 4641
31 4637
32 4637
33 4739
34 4743
35 4739
36 4739
37 4743
38 4739
39 4739
40 4739
41 4743
42 4743
43 4743
44 4739
45 4743
46 4739
47 4739
48 4739
49 4739
50 4743
51 4739
52 4739
53 4739
54 4743
55 4739
56 4743
57 4743
58 4743
59 4743
60 4739
61 4743
62 4743
63 4743
64 4743
65 4841
66 4845
67 4841
68 4845
69 4845
70 4845
71 4841
72 4841
73 4841
74 4841
75 4841
76 4841
77 4841
78 4845
79 4845
80 4841
81 4841
82 4841
83 4845
84 4841
85 4845
86 4841
87 4841
88 4841
89 4845
90 4845
91 4841
92 4841
93 4845
94 4841
95 4845
96 4845
97 4845
98 4841
99 4841
100 4841
101 4841
102 4845
103 4841
104 4841
105 4845
106 4841
107 4845
108 4841
109 4841
110 4845
111 4841
112 4841
113 4845
114 4841
115 4841
116 4845
117 4841
118 4845
119 4841
120 4845
121 4841
122 4845
123 4845
124 4841
125 4845
126 4841
127 4845
128 4845
129 4943
130 4947
131 4947
132 4943
133 4947
134 4947
135 4947
136 4947
137 4947
138 4947
139 4943
140 4943
141 4947
142 4947
143 4947
144 4947
145 4947
146 4943
147 4943
148 4943
149 4943
150 4947
151 4943
152 4943
153 4947
154 4947
155 4947
156 4947
157 4943
158 4947
159 4947
160 4947
161 4947
162 4947
163 4943
164 4947
165 4947
166 4943
167 4943
168 4943
169 4947
170 4947
171 4947
172 4947
173 4947
174 4943
175 4947
176 4947
177 4943
178 4947
179 4943
180 4947
181 4947
182 4947
183 4947
184 4947
185 4947
186 4943
187 4943
188 4943
189 4947
190 4947
191 4943
192 4947
193 4943
194 4943
195 4943
196 4947
197 4947
198 4943
199 4943
200 4947
201 4943
202 4943
203 4943
204 4943
205 4947
206 4943
207 4947
208 4947
209 4943
210 4943
211 4943
212 4947
213 4943
214 4947
215 4947
216 4947
217 4943
218 4947
219 4947
220 4943
221 4943
222 4943
223 4947
224 4947
225 4947
226 4943
227 4943
228 4947
229 4943
230 4947
231 4947
232 4943
233 4947
234 4943
235 4947
236 4947
237 4943
238 4943
239 4943
240 4947
241 4943
242 4947
243 4943
244 4943
245 4943
246 4947
247 4947
248 4943
249 4943
250 4943
251 4947
252 4943
253 4943
254 4947
255 4943
256 4943
257 5046
258 5046
259 5050
260 5050
261 5046
262 5050
263 5050
264 5046
265 5050
266 5046
267 5046
268 5050
269 5046
270 5046
271 5046
272 5050
273 5050
274 5046
275 5050
276 5050
277 5050
278 5050
279 5046
280 5046
281 5046
282 5050
283 5050
284 5046
285 5046
286 5046
287 5046
288 5050
289 5046
290 5046
291 5050
292 5046
293 5050
294 5050
295 5050
296 5046
297 5050
298 5050
299 5046
300 5046
301 5046
302 5050
303 5050
304 5046
305 5046
306 5046
307 5046
308 5050
309 5050
310 5046
311 5050
312 5046
313 5046
314 5050
315 5046
316 5050
317 5046
318 5046
319 5050
320 5050
321 5050
322 5046
323 5046
324 5046
325 5046
326 5050
327 5046
328 5050
329 5046
330 5046
331 5046
332 5050
333 5050
334 5050
335 5046
336 5050
337 5050
338 5046
339 5050
340 5046
341 5050
342 5050
343 5046
344 5046
345 5046
346 5050
347 5046
348 5050
349 5050
350 5046
351 5046
352 5050
353 5046
354 5050
355 5046
356 5050
357 5046
358 5050
359 5046
360 5050
361 5050
362 5050
363 5046
364 5046
365 5050
366 5050
367 5046
368 5050
369 5046
370 5046
371 5050
372 5046
373 5046
374 5046
375 5046
376 5046
377 5050
378 5050
379 5046
380 5046
381 5046
382 5050
383 5046
384 5050
385 5050
386 5046
387 5046
388 5050
389 5050
390 5050
391 5046
392 5046
393 5046
394 5046
395 5046
396 5050
397 5046
398 5050
399 5046
400 5050
401 5050
402 5046
403 5046
404 5046
405 5046
406 5050
407 5046
408 5046
409 5046
410 5050
411 5046
412 5046
413 5050
414 5046
415 5046
416 5050
417 5046
418 5046
419 5050
420 5050
421 5050
422 5050
423 5050
424 5050
425 5046
426 5050
427 5050
428 5046
429 5046
430 5046
431 5046
432 5050
433 5050
434 5046
435 5050
436 5046
437 5050
438 5050
439 5050
440 5050
441 5050
442 5046
443 5046
444 5046
445 5046
446 5050
447 5050
448 5050
449 5050
450 5050
451 5046
452 5046
453 5050
454 5046
455 5046
456 5050
457 5046
458 5050
459 5046
460 5046
461 5046
462 5046
463 5046
464 5046
465 5050
466 5050
467 5046
468 5046
469 5046
470 5050
471 5050
472 5050
473 5050
474 5046
475 5046
476 5050
477 5050
478 5046
479 5046
480 5050
481 5046
482 5046
483 5050
484 5046
485 5050
486 5050
487 5050
488 5050
489 5046
490 5046
491 5046
492 5050
493 5046
494 5046
495 5046
496 5050
497 5046
498 5050
499 5050
500 5046
501 5050
502 5046
503 5050
504 5050
505 5050
506 5046
507 5050
508 5050
509 5050
510 5050
511 5050
512 5046
513 5153
514 5149
515 5149
516 5149
517 5153
518 5153
519 5149
520 5153
521 5149
522 5149
523 5149
524 5153
525 5153
526 5149
527 5149
528 5149
529 5149
530 5153
531 5149
532 5149
533 5153
534 5153
535 5153
536 5153
537 5149
538 5149
539 5149
540 5153
541 5153
542 5153
543 5149
544 5153
545 5153
546 5153
547 5153
548 5153
549 5149
550 5149
551 5153
552 5153
553 5153
554 5149
555 5153
556 5149
557 5153
558 5149
559 5149
560 5153
561 5153
562 5153
563 5149
564 5153
565 5149
566 5153
567 5153
568 5149
569 5149
570 5153
571 5153
572 5149
573 5149
574 5153
575 5153
576 5149
577 5149
578 5153
579 5149
580 5149
581 5149
582 5153
583 5153
584 5149
585 5149
586 5149
587 5149
588 5149
589 5153
590 5153
591 5149
592 5149
593 5153
594 5153
595 5153
596 5149
597 5149
598 5153
599 5153
600 5153
601 5153
602 5149
603 5149
604 5153
605 5149
606 5153
607 5153
608 5153
609 5149
610 5153
611 5149
612 5153
613 5149
614 5149
615 5149
616 5149
617 5149
618 5153
619 5149
620 5153
621 5149
622 5149
623 5153
624 5149
625 5149
626 5149
627 5149
628 5153
629 5149
630 5149
631 5149
632 5149
633 5153
634 5149
635 5149
636 5153
637 5153
638 5149
639 5153
640 5153
641 5149
642 5149
643 5153
644 5153
645 5153
646 5153
647 5149
648 5153
649 5153
650 5149
651 5149
652 5153
653 5153
654 5153
655 5149
656 5149
657 5149
658 5149
659 5153
660 5149
661 5153
662 5153
663 5149
664 5149
665 5149
666 5153
667 5149
668 5153
669 5153
670 5149
671 5149
672 5149
673 5149
674 5153
675 5153
676 5149
677 5153
678 5149
679 5153
680 5149
681 5153
682 5149
683 5153
684 5153
685 5153
686 5149
687 5149
688 5153
689 5153
690 5149
691 5153
692 5153
693 5153
694 5153
695 5153
696 5149
697 5153
698 5149
699 5153
700 5153
701 5153
702 5153
703 5153
704 5153
705 5153
706 5153
707 5149
708 5153
709 5153
710 5149
711 5153
712 5153
713 5149
714 5153
715 5149
716 5149
717 5149
718 5153
719 5153
720 5149
721 5149
722 5153
723 5149
724 5149
725 5149
726 5153
727 5149
728 5153
729 5153
730 5149
731 5149
732 5149
733 5149
734 5153
735 5153
736 5149
737 5149
738 5153
739 5153
740 5149
741 5153
742 5149
743 5149
744 5153
745 5149
746 5149
747 5149
748 5149
749 5153
750 5153
751 5149
752 5149
753 5153
754 5149
755 5149
756 5149
757 5153
758 5153
759 5153
760 5149
761 5149
762 5153
763 5149
764 5153
765 5153
766 5153
767 5153
768 5153
769 5149
770 5153
771 5153
772 5149
773 5153
774 5153
775 5149
776 5153
777 5153
778 5149
779 5149
780 5149
781 5153
782 5153
783 5149
784 5149
785 5153
786 5149
787 5149
788 5153
789 5149
790 5153
791 5149
792 5149
793 5153
794 5153
795 5149
796 5149
797 5149
798 5149
799 5149
800 5153
801 5153
802 5153
803 5153
804 5153
805 5149
806 5149
807 5153
808 5149
809 5149
810 5149
811 5149
812 5153
813 5153
814 5153
815 5149
816 5153
817 5153
818 5153
819 5149
820 5149
821 5153
822 5153
823 5149
824 5153
825 5149
826 5149
827 5149
828 5153
829 5149
830 5149
831 5149
832 5149
833 5149
834 5149
835 5153
836 5149
837 5153
838 5153
839 5153
840 5153
841 5149
842 5149
843 5149
844 5153
845 5153
846 5149
847 5153
848 5153
849 5149
850 5149
851 5153
852 5149
853 5149
854 5153
855 5149
856 5149
857 5149
858 5153
859 5153
860 5149
861 5149
862 5149
863 5153
864 5149
865 5153
866 5149
867 5149
868 5149
869 5153
870 5153
871 5153
872 5153
873 5153
874 5153
875 5149
876 5153
877 5149
878 5149
879 5149
880 5149
881 5153
882 5149
883 5149
884 5153
885 5153
886 5153
887 5149
888 5153
889 5149
890 5149
891 5149
892 5149
893 5153
894 5149
895 5153
896 5149
897 5149
898 5149
899 5153
900 5149
901 5149
902 5149
903 5153
904 5153
905 5153
906 5149
907 5153
908 5149
909 5149
910 5149
911 5153
912 5153
913 5149
914 5153
915 5153
916 5153
917 5149
918 5149
919 5153
920 5149
921 5149
922 5153
923 5153
924 5149
925 5153
926 5149
927 5153
928 5149
929 5149
930 5149
931 5153
932 5149
933 5149
934 5149
935 5149
936 5149
937 5149
938 5153
939 5153
940 5153
941 5153
942 5149
943 5153
944 5153
945 5149
946 5149
947 5149
948 5149
949 5153
950 5153
951 5149
952 5149
953 5153
954 5149
955 5153
956 5149
957 5149
958 5149
959 5153
960 5153
961 5149
962 5153
963 5153
964 5149
965 5153
966 5149
967 5153
968 5149
969 5153
970 5149
971 5153
972 5153
973 5153
974 5149
975 5149
976 5149
977 5153
978 5153
979 5153
980 5153
981 5149
982 5149
983 5149
984 5153
985 5153
986 5153
987 5149
988 5153
989 5149
990 5153
991 5153
992 5153
993 5149
994 5149
995 5153
996 5153
997 5153
998 5149
999 5149
1000 5149
1001 5153
1002 5149
1003 5149
1004 5153
1005 5153
1006 5153
1007 5153
1008 5149
1009 5149
1010 5153
1011 5149
1012 5153
1013 5153
1014 5149
1015 5149
1016 5153
1017 5149
1018 5153
1019 5149
1020 5149
1021 5149
1022 5149
1023 5149
1024 5153
