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