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