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