forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
S5-plot_data_x150.txt
96 lines (72 loc) · 21.7 KB
/
S5-plot_data_x150.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
1: Average symbolic conclusion length is 51/6 ≈ 8.50. (Median: 9.50)
There are 3 minimal D-proofs with conclusions of even symbolic length, and there are 3 minimal D-proofs with conclusions of odd symbolic length. [3/6 ≈ 50.00% even]
1 0 2 0 3 0 4 1 5 1 6 0 7 0 8 0 9 1 10 2 11 0 12 0 13 1
2: Average symbolic conclusion length is 57/6 ≈ 9.50. (Median: 10.50)
There are 3 minimal D-proofs with conclusions of even symbolic length, and there are 3 minimal D-proofs with conclusions of odd symbolic length. [3/6 ≈ 50.00% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 0 8 0 9 0 10 1 11 2 12 0 13 0 14 1
3: Average symbolic conclusion length is 195/17 ≈ 11.47. (Median: 12)
There are 6 minimal D-proofs with conclusions of even symbolic length, and there are 11 minimal D-proofs with conclusions of odd symbolic length. [6/17 ≈ 35.29% even]
1 0 2 0 3 0 4 0 5 0 6 2 7 3 8 0 9 0 10 0 11 2 12 4 13 1 14 0 15 4 16 0 17 0 18 0 19 1
4: Average symbolic conclusion length is 338/28 ≈ 12.07. (Median: 12.50)
There are 16 minimal D-proofs with conclusions of even symbolic length, and there are 12 minimal D-proofs with conclusions of odd symbolic length. [16/28 ≈ 57.14% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 4 8 4 9 0 10 0 11 1 12 5 13 6 14 1 15 1 16 5 17 0 18 0 19 0 20 1
5: Average symbolic conclusion length is 768/56 ≈ 13.71. (Median: 14)
There are 22 minimal D-proofs with conclusions of even symbolic length, and there are 34 minimal D-proofs with conclusions of odd symbolic length. [22/56 ≈ 39.29% even]
1 0 2 0 3 1 4 0 5 0 6 0 7 0 8 7 9 8 10 0 11 0 12 1 13 8 14 12 15 2 16 1 17 10 18 0 19 0 20 1 21 2 22 0 23 2 24 0 25 0 26 0 27 0 28 0 29 1
6: Average symbolic conclusion length is 1297/89 ≈ 14.57. (Median: 15)
There are 50 minimal D-proofs with conclusions of even symbolic length, and there are 39 minimal D-proofs with conclusions of odd symbolic length. [50/89 ≈ 56.18% even]
1 0 2 0 3 0 4 1 5 0 6 0 7 0 8 0 9 12 10 12 11 0 12 0 13 2 14 13 15 19 16 3 17 4 18 15 19 0 20 0 21 2 22 3 23 0 24 2 25 0 26 0 27 0 28 0 29 0 30 1
7: Average symbolic conclusion length is 3190/203 ≈ 15.71. (Median: 16)
There are 77 minimal D-proofs with conclusions of even symbolic length, and there are 126 minimal D-proofs with conclusions of odd symbolic length. [77/203 ≈ 37.93% even]
1 0 2 0 3 0 4 0 5 3 6 2 7 1 8 0 9 3 10 22 11 30 12 2 13 3 14 7 15 26 16 33 17 8 18 6 19 32 20 0 21 4 22 3 23 7 24 0 25 5 26 0 27 0 28 0 29 0 30 0 31 2 32 1 33 0 34 0 35 0 36 1 37 1 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 1
8: Average symbolic conclusion length is 5402/325 ≈ 16.62. (Median: 17)
There are 191 minimal D-proofs with conclusions of even symbolic length, and there are 134 minimal D-proofs with conclusions of odd symbolic length. [191/325 ≈ 58.77% even]
1 0 2 0 3 0 4 0 5 0 6 4 7 2 8 1 9 0 10 6 11 39 12 43 13 2 14 3 15 13 16 48 17 54 18 11 19 14 20 48 21 0 22 5 23 5 24 10 25 2 26 7 27 0 28 0 29 0 30 0 31 1 32 3 33 1 34 0 35 0 36 0 37 1 38 1 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 1
9: Average symbolic conclusion length is 12383/666 ≈ 18.59. (Median: 18)
There are 257 minimal D-proofs with conclusions of even symbolic length, and there are 409 minimal D-proofs with conclusions of odd symbolic length. [257/666 ≈ 38.59% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 7 8 5 9 4 10 1 11 12 12 69 13 79 14 6 15 13 16 25 17 93 18 97 19 25 20 27 21 90 22 1 23 13 24 11 25 22 26 5 27 17 28 0 29 3 30 3 31 2 32 3 33 10 34 2 35 6 36 0 37 2 38 2 39 3 40 0 41 1 42 0 43 1 44 0 45 0 46 0 47 2 48 0 49 0 50 0 51 1 52 0 53 0 54 0 55 0 56 0 57 1 58 0 59 1 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 1
10: Average symbolic conclusion length is 22606/1174 ≈ 19.26. (Median: 19)
There are 680 minimal D-proofs with conclusions of even symbolic length, and there are 494 minimal D-proofs with conclusions of odd symbolic length. [680/1174 ≈ 57.92% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 13 9 9 10 6 11 5 12 31 13 131 14 133 15 11 16 23 17 52 18 159 19 165 20 40 21 60 22 150 23 5 24 23 25 22 26 34 27 10 28 26 29 1 30 4 31 3 32 2 33 4 34 14 35 4 36 6 37 3 38 3 39 6 40 4 41 0 42 1 43 1 44 1 45 1 46 0 47 1 48 3 49 0 50 0 51 0 52 1 53 0 54 0 55 0 56 0 57 0 58 1 59 0 60 1 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 1
11: Average symbolic conclusion length is 49704/2340 ≈ 21.24. (Median: 20)
There are 934 minimal D-proofs with conclusions of even symbolic length, and there are 1406 minimal D-proofs with conclusions of odd symbolic length. [934/2340 ≈ 39.91% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 2 9 26 10 24 11 16 12 11 13 66 14 232 15 248 16 29 17 51 18 107 19 299 20 288 21 85 22 109 23 271 24 14 25 53 26 39 27 74 28 19 29 56 30 2 31 16 32 9 33 9 34 9 35 32 36 8 37 16 38 7 39 16 40 11 41 18 42 1 43 6 44 1 45 9 46 3 47 4 48 2 49 11 50 3 51 1 52 0 53 9 54 0 55 2 56 2 57 1 58 0 59 2 60 0 61 3 62 1 63 0 64 0 65 1 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 2 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 1 83 0 84 0 85 0 86 0 87 0 88 0 89 0 90 0 91 1 92 0 93 0 94 0 95 1 96 0 97 0 98 0 99 0 100 0 101 0 102 0 103 0 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 1
12: Average symbolic conclusion length is 91359/4106 ≈ 22.25. (Median: 21)
There are 2325 minimal D-proofs with conclusions of even symbolic length, and there are 1781 minimal D-proofs with conclusions of odd symbolic length. [2325/4106 ≈ 56.62% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 5 10 43 11 37 12 24 13 19 14 128 15 414 16 407 17 52 18 86 19 212 20 529 21 496 22 146 23 217 24 446 25 28 26 83 27 74 28 117 29 45 30 87 31 14 32 27 33 20 34 17 35 24 36 49 37 22 38 24 39 20 40 20 41 32 42 23 43 9 44 9 45 5 46 10 47 10 48 4 49 9 50 14 51 3 52 1 53 2 54 10 55 1 56 5 57 3 58 1 59 3 60 3 61 1 62 4 63 1 64 0 65 1 66 1 67 0 68 1 69 0 70 0 71 0 72 0 73 1 74 3 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 1 84 0 85 0 86 0 87 0 88 0 89 0 90 0 91 0 92 1 93 0 94 0 95 0 96 1 97 0 98 0 99 0 100 0 101 0 102 0 103 0 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 0 114 1
13: Average symbolic conclusion length is 203264/8396 ≈ 24.21. (Median: 22)
There are 3444 minimal D-proofs with conclusions of even symbolic length, and there are 4952 minimal D-proofs with conclusions of odd symbolic length. [3444/8396 ≈ 41.02% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 5 8 6 9 4 10 18 11 92 12 87 13 77 14 59 15 282 16 765 17 748 18 118 19 195 20 420 21 1010 22 883 23 334 24 424 25 833 26 90 27 188 28 143 29 243 30 87 31 173 32 23 33 84 34 40 35 56 36 48 37 114 38 40 39 70 40 33 41 71 42 53 43 80 44 17 45 36 46 7 47 39 48 14 49 27 50 15 51 41 52 7 53 9 54 3 55 24 56 5 57 15 58 5 59 16 60 6 61 12 62 8 63 15 64 2 65 2 66 2 67 6 68 5 69 4 70 0 71 9 72 0 73 1 74 1 75 10 76 0 77 3 78 0 79 1 80 1 81 4 82 1 83 1 84 2 85 2 86 0 87 6 88 0 89 0 90 0 91 0 92 2 93 2 94 0 95 0 96 0 97 2 98 0 99 1 100 0 101 0 102 1 103 0 104 0 105 0 106 0 107 1 108 0 109 0 110 0 111 0 112 0 113 0 114 0 115 2 116 0 117 0 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 0 132 1 133 0 134 0 135 0 136 0 137 0 138 0 139 0 140 0 141 0 142 0 143 0 144 0 145 0 146 1 147 0 148 0 149 0 150 0
14: Average symbolic conclusion length is 382728/15153 ≈ 25.26. (Median: 23)
There are 8395 minimal D-proofs with conclusions of even symbolic length, and there are 6758 minimal D-proofs with conclusions of odd symbolic length. [8395/15153 ≈ 55.40% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 7 9 7 10 6 11 40 12 172 13 154 14 117 15 118 16 541 17 1408 18 1289 19 219 20 364 21 826 22 1785 23 1543 24 571 25 820 26 1408 27 209 28 316 29 285 30 414 31 178 32 281 33 70 34 125 35 102 36 80 37 114 38 174 39 82 40 102 41 76 42 102 43 129 44 112 45 78 46 46 47 52 48 54 49 38 50 43 51 54 52 63 53 30 54 12 55 13 56 37 57 13 58 24 59 22 60 19 61 12 62 29 63 12 64 20 65 12 66 2 67 6 68 9 69 6 70 5 71 7 72 10 73 0 74 7 75 3 76 13 77 1 78 3 79 0 80 1 81 1 82 4 83 2 84 2 85 3 86 3 87 1 88 6 89 0 90 0 91 0 92 3 93 3 94 3 95 0 96 0 97 3 98 3 99 0 100 1 101 0 102 0 103 1 104 0 105 0 106 0 107 1 108 1 109 0 110 0 111 0 112 1 113 0 114 0 115 1 116 3 117 0 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 0 132 0 133 1 134 0 135 0 136 0 137 0 138 0 139 0 140 0 141 0 142 0 143 0 144 0 145 0 146 0 147 1 148 0 149 0 150 0
15: Average symbolic conclusion length is 836591/30340 ≈ 27.57. (Median: 24)
There are 12777 minimal D-proofs with conclusions of even symbolic length, and there are 17563 minimal D-proofs with conclusions of odd symbolic length. [12777/30340 ≈ 42.11% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 1 8 4 9 18 10 23 11 27 12 86 13 328 14 318 15 250 16 256 17 1083 18 2538 19 2368 20 469 21 755 22 1640 23 3312 24 2734 25 1161 26 1551 27 2567 28 471 29 693 30 542 31 892 32 374 33 572 34 153 35 370 36 188 37 292 38 210 39 444 40 144 41 269 42 130 43 270 44 208 45 313 46 112 47 217 48 72 49 171 50 83 51 132 52 86 53 202 54 49 55 94 56 35 57 103 58 32 59 92 60 38 61 67 62 39 63 69 64 23 65 88 66 21 67 22 68 24 69 24 70 13 71 25 72 15 73 23 74 13 75 18 76 6 77 45 78 1 79 13 80 5 81 6 82 5 83 14 84 5 85 4 86 10 87 10 88 4 89 20 90 3 91 5 92 4 93 7 94 8 95 12 96 1 97 12 98 3 99 10 100 1 101 5 102 6 103 1 104 2 105 5 106 0 107 8 108 1 109 4 110 1 111 2 112 7 113 2 114 0 115 3 116 1 117 12 118 0 119 2 120 0 121 0 122 0 123 2 124 1 125 0 126 0 127 2 128 0 129 1 130 2 131 3 132 1 133 0 134 2 135 0 136 0 137 2 138 0 139 4 140 0 141 2 142 0 143 0 144 0 145 0 146 0 147 2 148 2 149 0 150 0
16: Average symbolic conclusion length is 1629454/56725 ≈ 28.73. (Median: 25)
There are 30657 minimal D-proofs with conclusions of even symbolic length, and there are 26068 minimal D-proofs with conclusions of odd symbolic length. [30657/56725 ≈ 54.04% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 2 9 12 10 38 11 43 12 44 13 193 14 629 15 621 16 466 17 540 18 2099 19 4636 20 4106 21 931 22 1448 23 3260 24 6017 25 4888 26 2178 27 3040 28 4508 29 1035 30 1224 31 1136 32 1578 33 781 34 931 35 362 36 599 37 446 38 445 39 564 40 690 41 425 42 411 43 332 44 424 45 483 46 463 47 367 48 290 49 326 50 257 51 244 52 187 53 256 54 288 55 172 56 133 57 139 58 157 59 95 60 130 61 102 62 109 63 94 64 112 65 96 66 116 67 54 68 67 69 50 70 40 71 52 72 38 73 35 74 45 75 17 76 28 77 48 78 62 79 11 80 35 81 11 82 14 83 11 84 19 85 8 86 11 87 19 88 14 89 18 90 27 91 5 92 12 93 6 94 15 95 16 96 16 97 7 98 14 99 9 100 13 101 3 102 18 103 6 104 2 105 3 106 5 107 13 108 9 109 4 110 5 111 1 112 5 113 9 114 3 115 1 116 4 117 9 118 15 119 0 120 3 121 0 122 5 123 0 124 2 125 2 126 0 127 0 128 2 129 0 130 1 131 2 132 3 133 1 134 1 135 3 136 0 137 1 138 2 139 1 140 4 141 0 142 3 143 0 144 0 145 0 146 0 147 3 148 3 149 3 150 0
17: Average symbolic conclusion length is 3528874/113539 ≈ 31.08. (Median: 26)
There are 49231 minimal D-proofs with conclusions of even symbolic length, and there are 64308 minimal D-proofs with conclusions of odd symbolic length. [49231/113539 ≈ 43.36% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 0 8 3 9 9 10 31 11 99 12 121 13 126 14 432 15 1243 16 1250 17 1023 18 1169 19 4190 20 8517 21 7487 22 1942 23 2994 24 6379 25 11228 26 8749 27 4327 28 5784 29 8323 30 2215 31 2597 32 2194 33 3322 34 1580 35 1889 36 744 37 1370 38 771 39 1147 40 966 41 1701 42 713 43 1125 44 591 45 1048 46 813 47 1152 48 565 49 948 50 463 51 916 52 413 53 675 54 425 55 747 56 345 57 498 58 219 59 562 60 167 61 379 62 204 63 340 64 174 65 345 66 159 67 342 68 151 69 184 70 91 71 217 72 90 73 126 74 112 75 139 76 41 77 128 78 74 79 146 80 61 81 97 82 38 83 113 84 25 85 67 86 35 87 63 88 40 89 65 90 32 91 85 92 33 93 47 94 17 95 63 96 32 97 50 98 27 99 40 100 19 101 44 102 16 103 35 104 15 105 15 106 8 107 52 108 21 109 24 110 6 111 22 112 16 113 16 114 18 115 18 116 5 117 13 118 13 119 41 120 1 121 10 122 14 123 18 124 1 125 9 126 4 127 14 128 1 129 7 130 1 131 14 132 5 133 9 134 8 135 4 136 8 137 3 138 2 139 9 140 5 141 10 142 3 143 8 144 1 145 3 146 0 147 8 148 4 149 6 150 7
18: Average symbolic conclusion length is 6969323/214468 ≈ 32.50. (Median: 28)
There are 113173 minimal D-proofs with conclusions of even symbolic length, and there are 101295 minimal D-proofs with conclusions of odd symbolic length. [113173/214468 ≈ 52.77% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 2 8 1 9 4 10 18 11 61 12 178 13 209 14 213 15 855 16 2346 17 2351 18 1824 19 2348 20 7961 21 15617 22 13229 23 3779 24 5780 25 12432 26 20365 27 15683 28 8040 29 11066 30 14739 31 4643 32 4691 33 4608 34 6081 35 3387 36 3284 37 1824 38 2401 39 1735 40 1883 41 2365 42 2691 43 1940 44 1761 45 1589 46 1669 47 1868 48 1755 49 1475 50 1361 51 1502 52 1289 53 1409 54 983 55 1201 56 1209 57 918 58 702 59 935 60 820 61 656 62 670 63 564 64 534 65 535 66 532 67 471 68 585 69 422 70 291 71 398 72 309 73 219 74 354 75 223 76 214 77 220 78 187 79 177 80 270 81 115 82 156 83 172 84 142 85 78 86 166 87 90 88 92 89 117 90 87 91 69 92 167 93 65 94 66 95 68 96 93 97 79 98 100 99 57 100 60 101 68 102 66 103 35 104 71 105 36 106 20 107 47 108 62 109 44 110 37 111 26 112 68 113 35 114 29 115 36 116 26 117 35 118 20 119 45 120 61 121 6 122 26 123 24 124 25 125 10 126 15 127 25 128 18 129 8 130 9 131 10 132 34 133 12 134 16 135 10 136 5 137 22 138 3 139 7 140 13 141 11 142 17 143 7 144 13 145 1 146 4 147 7 148 9 149 12 150 9
19: Average symbolic conclusion length is 15084320/431896 ≈ 34.93. (Median: 29)
There are 191506 minimal D-proofs with conclusions of even symbolic length, and there are 240390 minimal D-proofs with conclusions of odd symbolic length. [191506/431896 ≈ 44.34% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 3 8 12 9 14 10 28 11 65 12 168 13 435 14 496 15 624 16 1857 17 4677 18 4736 19 3824 20 4986 21 15667 22 28684 23 24297 24 7765 25 12042 26 24417 27 38235 28 28616 29 16096 30 21322 31 27394 32 9649 33 9719 34 9027 35 12664 36 6730 37 6984 38 3724 39 5579 40 3245 41 4476 42 4156 43 6300 44 3328 45 4816 46 2673 47 4501 48 3173 49 4174 50 2452 51 3641 52 2306 53 3909 54 2071 55 3348 56 1941 57 3125 58 1484 59 2300 60 1406 61 2471 62 1291 63 2053 64 956 65 1742 66 881 67 1525 68 904 69 1516 70 696 71 1233 72 659 73 985 74 632 75 780 76 433 77 952 78 356 79 614 80 504 81 647 82 236 83 552 84 285 85 441 86 309 87 472 88 171 89 471 90 194 91 273 92 279 93 391 94 133 95 297 96 134 97 312 98 206 99 251 100 95 101 285 102 139 103 193 104 141 105 182 106 80 107 155 108 81 109 169 110 107 111 121 112 92 113 192 114 68 115 95 116 91 117 182 118 63 119 104 120 73 121 153 122 74 123 95 124 47 125 103 126 17 127 66 128 51 129 51 130 12 131 75 132 65 133 78 134 32 135 55 136 31 137 89 138 39 139 42 140 19 141 46 142 34 143 65 144 17 145 43 146 5 147 57 148 15 149 34 150 22
20: Average symbolic conclusion length is 30243983/829754 ≈ 36.45. (Median: 31)
There are 429831 minimal D-proofs with conclusions of even symbolic length, and there are 399923 minimal D-proofs with conclusions of odd symbolic length. [429831/829754 ≈ 51.80% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 2 8 5 9 19 10 19 11 36 12 120 13 372 14 861 15 939 16 1179 17 3805 18 8954 19 9216 20 7257 21 10182 22 30136 23 52828 24 43511 25 15325 26 23470 27 47628 28 70102 29 52168 30 30565 31 41131 32 49882 33 19789 34 18242 35 18575 36 23702 37 14179 38 12264 39 8710 40 9952 41 7097 42 7694 43 8987 44 10307 45 8134 46 7590 47 7408 48 7215 49 7771 50 6822 51 5916 52 5634 53 6177 54 5788 55 6311 56 4872 57 6108 58 4882 59 4320 60 3392 61 4033 62 3966 63 3789 64 3081 65 3556 66 2636 67 2538 68 2624 69 2403 70 2409 71 2180 72 1803 73 2097 74 1766 75 1620 76 1321 77 1534 78 1356 79 997 80 1501 81 1157 82 1084 83 919 84 846 85 736 86 883 87 707 88 730 89 818 90 649 91 507 92 767 93 579 94 634 95 488 96 435 97 483 98 616 99 450 100 406 101 406 102 481 103 319 104 464 105 264 106 306 107 334 108 231 109 239 110 315 111 229 112 211 113 253 114 295 115 180 116 201 117 292 118 248 119 172 120 143 121 172 122 392 123 155 124 150 125 171 126 151 127 125 128 121 129 111 130 85 131 84 132 122 133 108 134 137 135 66 136 80 137 152 138 114 139 105 140 61 141 65 142 137 143 73 144 90 145 35 146 69 147 66 148 67 149 61 150 47
21: Average symbolic conclusion length is 65021170/1666562 ≈ 39.02. (Median: 32)
There are 752506 minimal D-proofs with conclusions of even symbolic length, and there are 914056 minimal D-proofs with conclusions of odd symbolic length. [752506/1666562 ≈ 45.15% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 5 8 5 9 12 10 53 11 61 12 128 13 324 14 836 15 1858 16 2044 17 2680 18 7875 19 17487 20 18043 21 14860 22 20930 23 58684 24 97662 25 79815 26 30879 27 47490 28 92498 29 131130 30 95665 31 60534 32 79138 33 93760 34 40447 35 37324 36 36940 37 48381 38 28088 39 26133 40 17536 41 22853 42 13575 43 17845 44 16389 45 22084 46 14100 47 18549 48 12284 49 18856 50 13296 51 16891 52 9943 53 14182 54 10002 55 14962 56 9949 57 14531 58 9415 59 14729 60 6923 61 10186 62 6602 63 10574 64 6119 65 10003 66 5519 67 8409 68 5096 69 7185 70 4065 71 7079 72 3574 73 5442 74 3724 75 5420 76 2780 77 4632 78 2539 79 3701 80 2555 81 3473 82 2106 83 4194 84 1541 85 2286 86 1918 87 2279 88 1299 89 2536 90 1284 91 1947 92 1584 93 1730 94 1081 95 2324 96 816 97 1368 98 1144 99 1598 100 838 101 1537 102 857 103 1224 104 887 105 1010 106 527 107 1464 108 556 109 730 110 660 111 886 112 514 113 811 114 480 115 813 116 470 117 643 118 501 119 893 120 320 121 422 122 583 123 826 124 299 125 521 126 295 127 738 128 297 129 390 130 207 131 478 132 290 133 365 134 280 135 414 136 138 137 414 138 234 139 360 140 230 141 218 142 278 143 396 144 147 145 231 146 134 147 430 148 97 149 263 150 103
22: Average symbolic conclusion length is 132289739/3250922 ≈ 40.69. (Median: 33)
There are 1656199 minimal D-proofs with conclusions of even symbolic length, and there are 1594723 minimal D-proofs with conclusions of odd symbolic length. [1656199/3250922 ≈ 50.95% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 3 8 8 9 7 10 29 11 112 12 138 13 230 14 654 15 1816 16 3718 17 4094 18 5454 19 15996 20 33729 21 34869 22 28509 23 42466 24 112604 25 180968 26 145167 27 61624 28 94220 29 180161 30 242710 31 176759 32 116456 33 153467 34 173593 35 82524 36 71790 37 75620 38 92575 39 58114 40 47919 41 40021 42 42336 43 31474 44 32113 45 35752 46 38458 47 31333 48 30605 49 30794 50 30863 51 33492 52 27444 53 26057 54 22976 55 24356 56 24011 57 25237 58 21892 59 27406 60 21880 61 22359 62 15633 63 18648 64 16603 65 17242 66 14884 67 16985 68 13769 69 14948 70 11353 71 13223 72 10961 73 10188 74 9467 75 10165 76 8462 77 9659 78 7159 79 7554 80 6947 81 5934 82 5910 83 7327 84 6140 85 4592 86 5758 87 4345 88 3805 89 4571 90 3874 91 3577 92 3952 93 3428 94 2977 95 3923 96 3410 97 2172 98 3248 99 2585 100 2563 101 2863 102 2465 103 2147 104 2573 105 1943 106 1755 107 2291 108 2059 109 1443 110 1816 111 1455 112 1682 113 1773 114 1250 115 1171 116 1547 117 1236 118 1075 119 1551 120 1317 121 898 122 1094 123 1183 124 1413 125 882 126 781 127 1096 128 1150 129 737 130 613 131 818 132 1168 133 630 134 731 135 658 136 653 137 835 138 606 139 595 140 653 141 550 142 491 143 657 144 593 145 354 146 468 147 657 148 574 149 429 150 377
23: Average symbolic conclusion length is 283443336/6547739 ≈ 43.29. (Median: 35)
There are 3001625 minimal D-proofs with conclusions of even symbolic length, and there are 3546114 minimal D-proofs with conclusions of odd symbolic length. [3001625/6547739 ≈ 45.84% even]
1 0 2 0 3 0 4 0 5 0 6 2 7 1 8 7 9 21 10 28 11 84 12 289 13 410 14 683 15 1677 16 4132 17 7949 18 8711 19 12389 20 33003 21 66400 22 68516 23 57887 24 87010 25 218686 26 336205 27 268900 28 123789 29 190527 30 350105 31 455893 32 328338 33 230840 34 297159 35 330844 36 167327 37 146701 38 151878 39 186739 40 115009 41 99791 42 79635 43 93586 44 60819 45 73658 46 66528 47 82580 48 56878 49 68451 50 52541 51 74679 52 56778 53 69424 54 43878 55 58825 56 41938 57 57360 58 40970 59 57347 60 42768 61 60578 62 34765 63 48973 64 29919 65 45287 66 27525 67 40837 68 27141 69 39545 70 23798 71 36879 72 21185 73 30484 74 19583 75 25735 76 16613 77 26236 78 15118 79 22893 80 13904 81 19118 82 10700 83 17660 84 11837 85 16644 86 11086 87 14383 88 7884 89 14703 90 7404 91 10780 92 8701 93 10242 94 6299 95 10314 96 6452 97 8981 98 6612 99 7701 100 4637 101 9124 102 4725 103 6690 104 5360 105 6375 106 3597 107 6581 108 3680 109 5440 110 3815 111 4402 112 3388 113 5901 114 2950 115 3558 116 3261 117 4383 118 2241 119 3865 120 2536 121 3725 122 2427 123 2965 124 2343 125 4135 126 1665 127 2551 128 2192 129 2959 130 1380 131 2332 132 2075 133 2534 134 1609 135 1942 136 1267 137 3332 138 1305 139 1838 140 1304 141 1855 142 1517 143 1935 144 1184 145 1595 146 863 147 1732 148 1020 149 1925 150 681
24: Average symbolic conclusion length is 581780034/12887201 ≈ 45.14. (Median: 36)
There are 6477643 minimal D-proofs with conclusions of even symbolic length, and there are 6409558 minimal D-proofs with conclusions of odd symbolic length. [6477643/12887201 ≈ 50.26% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 2 8 2 9 17 10 37 11 47 12 171 13 562 14 792 15 1271 16 3330 17 8591 18 15817 19 17120 20 24967 21 66367 22 128108 23 132921 24 112387 25 175141 26 419993 27 624814 28 493661 29 245997 30 377226 31 679438 32 848228 33 612269 34 446904 35 577647 36 621659 37 340137 38 287506 39 310610 40 362765 41 234964 42 189267 43 172874 44 177227 45 136853 46 135745 47 145872 48 147761 49 124572 50 117866 51 118484 52 126420 53 134238 54 113550 55 114901 56 96522 57 105549 58 94883 59 99696 60 91249 61 108226 62 95229 63 100633 64 73528 65 93401 66 70987 67 76999 68 64473 69 73832 70 61488 71 72279 72 55795 73 65032 74 52420 75 53463 76 41021 77 52048 78 40531 79 44349 80 38688 81 42105 82 31086 83 34196 84 28454 85 30681 86 30712 87 27649 88 23649 89 29219 90 21956 91 20249 92 25028 93 20319 94 17029 95 21165 96 16050 97 17368 98 18341 99 14464 100 12909 101 17088 102 14103 103 12067 104 15648 105 12165 106 10492 107 12846 108 10070 109 9908 110 11314 111 8450 112 8195 113 10752 114 9023 115 7386 116 8883 117 8459 118 7119 119 8077 120 5890 121 6623 122 7976 123 5726 124 5072 125 7192 126 6671 127 4646 128 5539 129 5266 130 4899 131 4624 132 4148 133 4741 134 5126 135 3615 136 3196 137 5561 138 4685 139 3439 140 3500 141 3393 142 4788 143 3896 144 2961 145 2933 146 3016 147 3382 148 2663 149 3514 150 2883