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