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