-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathw6-plot_data_x800.txt
164 lines (123 loc) · 143 KB
/
w6-plot_data_x800.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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
1: Average symbolic conclusion length is 21/1 ≈ 21.00. (Median: 21)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there is 1 minimal D-proof with a conclusion of odd symbolic length. [0/1 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 1
3: Average symbolic conclusion length is 13/1 ≈ 13.00. (Median: 13)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there is 1 minimal D-proof with a conclusion of odd symbolic length. [0/1 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 1
5: Average symbolic conclusion length is 40/2 ≈ 20.00. (Median: 20.00)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 2 minimal D-proofs with conclusions of odd symbolic length. [0/2 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 1 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 0 22 0 23 0 24 0 25 0 26 0 27 1
7: Average symbolic conclusion length is 43/3 ≈ 14.33. (Median: 9)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 3 minimal D-proofs with conclusions of odd symbolic length. [0/3 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 0 22 0 23 0 24 0 25 1
9: Average symbolic conclusion length is 86/6 ≈ 14.33. (Median: 8.00)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 6 minimal D-proofs with conclusions of odd symbolic length. [0/6 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 3 8 0 9 1 10 0 11 0 12 0 13 1 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 0 22 0 23 0 24 0 25 0 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 0 37 0 38 0 39 0 40 0 41 0 42 0 43 1
11: Average symbolic conclusion length is 179/7 ≈ 25.57. (Median: 21)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 7 minimal D-proofs with conclusions of odd symbolic length. [0/7 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 0 15 1 16 0 17 0 18 0 19 1 20 0 21 1 22 0 23 0 24 0 25 0 26 0 27 1 28 0 29 0 30 0 31 1 32 0 33 0 34 0 35 0 36 0 37 0 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 0 48 0 49 0 50 0 51 0 52 0 53 0 54 0 55 0 56 0 57 0 58 0 59 0 60 0 61 1
13: Average symbolic conclusion length is 339/12 ≈ 28.25. (Median: 22.00)
There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 11 minimal D-proofs with conclusions of odd symbolic length. [1/12 ≈ 8.33% even]
1 0 2 0 3 1 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 1 12 0 13 0 14 0 15 2 16 0 17 0 18 0 19 1 20 0 21 0 22 0 23 0 24 0 25 2 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 2 34 0 35 0 36 0 37 0 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 0 48 0 49 0 50 0 51 0 52 0 53 0 54 0 55 0 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 1 74 0 75 0 76 0 77 0 78 0 79 1
15: Average symbolic conclusion length is 678/15 ≈ 45.20. (Median: 43)
There are 3 minimal D-proofs with conclusions of even symbolic length, and there are 12 minimal D-proofs with conclusions of odd symbolic length. [3/15 ≈ 20.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 1 13 0 14 0 15 0 16 0 17 1 18 0 19 1 20 0 21 0 22 1 23 1 24 0 25 0 26 1 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 0 37 0 38 0 39 0 40 0 41 0 42 0 43 1 44 0 45 0 46 0 47 0 48 0 49 1 50 0 51 1 52 0 53 0 54 0 55 1 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 1 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 0 84 0 85 0 86 0 87 0 88 0 89 0 90 0 91 2 92 0 93 0 94 0 95 0 96 0 97 1
17: Average symbolic conclusion length is 1058/23 ≈ 46.00. (Median: 37)
There are 5 minimal D-proofs with conclusions of even symbolic length, and there are 18 minimal D-proofs with conclusions of odd symbolic length. [5/23 ≈ 21.74% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 0 13 0 14 1 15 1 16 0 17 1 18 1 19 0 20 1 21 0 22 0 23 1 24 1 25 0 26 0 27 1 28 0 29 0 30 0 31 1 32 0 33 0 34 0 35 0 36 0 37 2 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 0 48 0 49 3 50 0 51 1 52 0 53 0 54 0 55 0 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 2 68 0 69 2 70 0 71 0 72 0 73 0 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 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 0 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 1 110 0 111 0 112 0 113 0 114 0 115 1
19: Average symbolic conclusion length is 1896/36 ≈ 52.67. (Median: 35.50)
There are 10 minimal D-proofs with conclusions of even symbolic length, and there are 26 minimal D-proofs with conclusions of odd symbolic length. [10/36 ≈ 27.78% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 1 9 0 10 0 11 0 12 0 13 2 14 0 15 0 16 1 17 0 18 3 19 1 20 0 21 1 22 0 23 0 24 1 25 0 26 0 27 0 28 0 29 2 30 0 31 1 32 2 33 1 34 1 35 0 36 0 37 2 38 1 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 0 48 0 49 1 50 0 51 0 52 0 53 0 54 0 55 0 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 3 68 0 69 0 70 0 71 0 72 0 73 0 74 0 75 0 76 0 77 0 78 0 79 1 80 0 81 0 82 0 83 0 84 0 85 2 86 0 87 1 88 0 89 0 90 0 91 1 92 0 93 0 94 0 95 0 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 3 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 2 128 0 129 0 130 0 131 0 132 0 133 1
21: Average symbolic conclusion length is 3038/61 ≈ 49.80. (Median: 36)
There are 15 minimal D-proofs with conclusions of even symbolic length, and there are 46 minimal D-proofs with conclusions of odd symbolic length. [15/61 ≈ 24.59% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 1 12 0 13 0 14 2 15 1 16 3 17 0 18 0 19 1 20 0 21 1 22 1 23 2 24 1 25 1 26 2 27 1 28 0 29 2 30 4 31 3 32 1 33 1 34 0 35 1 36 1 37 3 38 0 39 1 40 0 41 2 42 0 43 2 44 0 45 0 46 0 47 0 48 0 49 3 50 0 51 0 52 0 53 0 54 0 55 4 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 1 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 0 84 0 85 3 86 0 87 1 88 0 89 0 90 0 91 0 92 0 93 0 94 0 95 0 96 0 97 0 98 0 99 0 100 0 101 0 102 0 103 4 104 0 105 2 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 1 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 1 140 0 141 0 142 0 143 0 144 0 145 1 146 0 147 0 148 0 149 0 150 0 151 1
23: Average symbolic conclusion length is 5286/99 ≈ 53.39. (Median: 39)
There are 29 minimal D-proofs with conclusions of even symbolic length, and there are 70 minimal D-proofs with conclusions of odd symbolic length. [29/99 ≈ 29.29% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 1 10 1 11 2 12 5 13 1 14 3 15 3 16 1 17 2 18 2 19 1 20 1 21 2 22 1 23 0 24 2 25 4 26 0 27 0 28 2 29 0 30 4 31 6 32 0 33 1 34 0 35 0 36 1 37 1 38 1 39 3 40 0 41 3 42 0 43 1 44 2 45 1 46 1 47 0 48 1 49 7 50 1 51 0 52 0 53 0 54 0 55 3 56 0 57 0 58 0 59 0 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 3 68 0 69 0 70 0 71 0 72 0 73 3 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 0 84 0 85 1 86 0 87 0 88 0 89 0 90 0 91 2 92 0 93 0 94 0 95 0 96 0 97 0 98 0 99 0 100 0 101 0 102 0 103 4 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 0 120 0 121 2 122 0 123 1 124 0 125 0 126 0 127 1 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 1 140 0 141 0 142 0 143 0 144 0 145 3 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 2 158 0 159 0 160 0 161 0 162 0 163 2 164 0 165 0 166 0 167 0 168 0 169 1 170 0 171 0 172 0 173 0 174 0 175 0 176 0 177 0 178 0 179 0 180 0 181 0 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 1
25: Average symbolic conclusion length is 8904/152 ≈ 58.58. (Median: 42)
There are 46 minimal D-proofs with conclusions of even symbolic length, and there are 106 minimal D-proofs with conclusions of odd symbolic length. [46/152 ≈ 30.26% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 5 11 1 12 3 13 3 14 1 15 6 16 2 17 0 18 1 19 2 20 3 21 4 22 3 23 4 24 2 25 2 26 3 27 0 28 3 29 3 30 0 31 1 32 3 33 0 34 2 35 2 36 4 37 4 38 2 39 2 40 0 41 1 42 4 43 3 44 1 45 1 46 1 47 1 48 1 49 1 50 0 51 1 52 0 53 2 54 0 55 6 56 0 57 1 58 0 59 1 60 0 61 2 62 0 63 0 64 0 65 3 66 1 67 5 68 0 69 0 70 0 71 0 72 0 73 6 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 0 84 0 85 5 86 0 87 0 88 0 89 0 90 0 91 7 92 0 93 0 94 0 95 0 96 0 97 1 98 0 99 0 100 0 101 0 102 0 103 1 104 0 105 0 106 0 107 0 108 0 109 4 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 0 120 0 121 5 122 0 123 1 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 4 140 0 141 2 142 0 143 0 144 0 145 0 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 0 158 0 159 0 160 0 161 0 162 0 163 1 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 1 176 0 177 0 178 0 179 0 180 0 181 1 182 0 183 0 184 0 185 0 186 0 187 1 188 0 189 0 190 0 191 0 192 0 193 1 194 0 195 0 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 0 210 0 211 2 212 0 213 0 214 0 215 0 216 0 217 0 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 0 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 1
27: Average symbolic conclusion length is 13871/214 ≈ 64.82. (Median: 44.00)
There are 75 minimal D-proofs with conclusions of even symbolic length, and there are 139 minimal D-proofs with conclusions of odd symbolic length. [75/214 ≈ 35.05% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 2 9 1 10 0 11 2 12 1 13 3 14 2 15 0 16 3 17 1 18 6 19 6 20 4 21 5 22 4 23 2 24 10 25 2 26 3 27 4 28 1 29 3 30 5 31 2 32 1 33 2 34 4 35 3 36 3 37 6 38 2 39 1 40 3 41 0 42 5 43 4 44 0 45 1 46 1 47 1 48 1 49 0 50 1 51 1 52 2 53 3 54 1 55 5 56 2 57 4 58 1 59 0 60 1 61 4 62 1 63 0 64 1 65 0 66 0 67 6 68 0 69 0 70 0 71 0 72 0 73 5 74 0 75 2 76 1 77 1 78 0 79 1 80 0 81 0 82 0 83 0 84 1 85 11 86 0 87 0 88 1 89 0 90 0 91 3 92 0 93 0 94 0 95 0 96 0 97 0 98 0 99 0 100 0 101 0 102 0 103 7 104 0 105 0 106 0 107 0 108 0 109 5 110 0 111 0 112 0 113 0 114 0 115 1 116 0 117 0 118 0 119 0 120 0 121 1 122 0 123 0 124 0 125 0 126 0 127 6 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 4 140 0 141 0 142 0 143 0 144 0 145 0 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 2 158 0 159 1 160 0 161 0 162 0 163 2 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 2 176 0 177 0 178 0 179 0 180 0 181 3 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 2 194 0 195 0 196 0 197 0 198 0 199 2 200 0 201 0 202 0 203 0 204 0 205 1 206 0 207 0 208 0 209 0 210 0 211 0 212 0 213 0 214 0 215 0 216 0 217 0 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 1 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 1 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 2 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 0 284 0 285 0 286 0 287 0 288 0 289 0 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 1
29: Average symbolic conclusion length is 21182/299 ≈ 70.84. (Median: 48)
There are 111 minimal D-proofs with conclusions of even symbolic length, and there are 188 minimal D-proofs with conclusions of odd symbolic length. [111/299 ≈ 37.12% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 2 11 4 12 1 13 3 14 5 15 2 16 5 17 5 18 6 19 0 20 3 21 5 22 9 23 1 24 6 25 4 26 2 27 10 28 7 29 1 30 2 31 7 32 6 33 5 34 4 35 6 36 3 37 2 38 5 39 3 40 4 41 5 42 1 43 2 44 3 45 1 46 2 47 2 48 6 49 4 50 2 51 1 52 2 53 1 54 4 55 4 56 2 57 1 58 1 59 1 60 2 61 4 62 0 63 1 64 3 65 0 66 0 67 3 68 0 69 0 70 2 71 1 72 1 73 5 74 0 75 1 76 1 77 3 78 1 79 7 80 0 81 0 82 2 83 0 84 0 85 3 86 0 87 0 88 1 89 4 90 0 91 3 92 0 93 1 94 2 95 1 96 0 97 2 98 0 99 0 100 0 101 0 102 1 103 6 104 0 105 0 106 2 107 0 108 0 109 6 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 0 120 0 121 7 122 0 123 0 124 0 125 0 126 0 127 7 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 2 140 0 141 0 142 0 143 0 144 0 145 4 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 8 158 0 159 1 160 0 161 0 162 0 163 2 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 5 176 0 177 2 178 0 179 0 180 0 181 2 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 2 194 0 195 0 196 0 197 0 198 0 199 1 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 0 210 0 211 1 212 0 213 0 214 0 215 0 216 0 217 3 218 0 219 0 220 0 221 0 222 0 223 1 224 0 225 0 226 0 227 0 228 0 229 1 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 2 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 0 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 1 284 0 285 0 286 0 287 0 288 0 289 0 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 1 302 0 303 0 304 0 305 0 306 0 307 0 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 0 318 0 319 2 320 0 321 0 322 0 323 0 324 0 325 0 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 0 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 1
31: Average symbolic conclusion length is 31424/400 ≈ 78.56. (Median: 54)
There are 168 minimal D-proofs with conclusions of even symbolic length, and there are 232 minimal D-proofs with conclusions of odd symbolic length. [168/400 ≈ 42.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 1 11 3 12 2 13 0 14 2 15 3 16 0 17 2 18 4 19 2 20 7 21 3 22 4 23 8 24 3 25 8 26 8 27 3 28 8 29 5 30 9 31 6 32 7 33 9 34 6 35 3 36 16 37 4 38 5 39 6 40 3 41 2 42 7 43 1 44 3 45 4 46 6 47 3 48 5 49 8 50 2 51 0 52 5 53 1 54 8 55 4 56 1 57 2 58 4 59 5 60 1 61 2 62 1 63 2 64 4 65 3 66 2 67 3 68 2 69 1 70 6 71 1 72 1 73 4 74 3 75 1 76 1 77 0 78 0 79 5 80 0 81 0 82 5 83 0 84 0 85 0 86 0 87 0 88 4 89 1 90 1 91 4 92 0 93 3 94 0 95 0 96 1 97 7 98 0 99 0 100 3 101 0 102 0 103 8 104 0 105 0 106 2 107 0 108 0 109 5 110 0 111 2 112 2 113 1 114 0 115 1 116 0 117 0 118 0 119 0 120 1 121 14 122 0 123 0 124 2 125 0 126 0 127 3 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 0 138 0 139 10 140 0 141 0 142 0 143 0 144 0 145 5 146 0 147 0 148 0 149 0 150 0 151 1 152 0 153 0 154 0 155 0 156 0 157 2 158 0 159 0 160 0 161 0 162 0 163 6 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 6 176 0 177 0 178 0 179 0 180 0 181 2 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 2 194 0 195 1 196 0 197 0 198 0 199 2 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 0 210 0 211 3 212 0 213 0 214 0 215 0 216 0 217 5 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 2 230 0 231 0 232 0 233 0 234 0 235 6 236 0 237 0 238 0 239 0 240 0 241 1 242 0 243 0 244 0 245 0 246 0 247 1 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 1 266 0 267 0 268 0 269 0 270 0 271 1 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 1 284 0 285 0 286 0 287 0 288 0 289 0 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 2 302 0 303 0 304 0 305 0 306 0 307 0 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 0 318 0 319 0 320 0 321 0 322 0 323 0 324 0 325 0 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 1 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 1 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 2 374 0 375 0 376 0 377 0 378 0 379 0 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 0 392 0 393 0 394 0 395 0 396 0 397 0 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 1
33: Average symbolic conclusion length is 45863/560 ≈ 81.90. (Median: 54.50)
There are 245 minimal D-proofs with conclusions of even symbolic length, and there are 315 minimal D-proofs with conclusions of odd symbolic length. [245/560 ≈ 43.75% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 1 11 0 12 0 13 3 14 0 15 3 16 7 17 5 18 5 19 5 20 6 21 11 22 4 23 10 24 10 25 6 26 10 27 6 28 9 29 8 30 11 31 2 32 4 33 7 34 18 35 2 36 8 37 9 38 6 39 14 40 11 41 0 42 4 43 12 44 9 45 5 46 5 47 7 48 4 49 3 50 5 51 5 52 8 53 6 54 4 55 5 56 3 57 3 58 5 59 2 60 6 61 4 62 3 63 2 64 4 65 2 66 7 67 6 68 2 69 1 70 1 71 1 72 5 73 4 74 0 75 4 76 4 77 0 78 0 79 3 80 0 81 1 82 9 83 1 84 3 85 5 86 0 87 0 88 4 89 0 90 1 91 7 92 1 93 0 94 1 95 0 96 0 97 6 98 0 99 0 100 9 101 4 102 0 103 2 104 0 105 0 106 6 107 1 108 1 109 3 110 0 111 1 112 2 113 5 114 1 115 10 116 0 117 0 118 3 119 0 120 0 121 5 122 0 123 0 124 6 125 0 126 0 127 3 128 0 129 1 130 4 131 1 132 0 133 4 134 0 135 0 136 0 137 0 138 1 139 7 140 0 141 0 142 4 143 0 144 0 145 7 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 7 158 0 159 0 160 0 161 0 162 0 163 7 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 2 176 0 177 0 178 0 179 0 180 0 181 4 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 8 194 0 195 1 196 0 197 0 198 0 199 2 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 0 210 0 211 6 212 0 213 2 214 0 215 0 216 0 217 2 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 5 230 0 231 0 232 0 233 0 234 0 235 1 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 2 248 0 249 0 250 0 251 0 252 0 253 3 254 0 255 0 256 0 257 0 258 0 259 1 260 0 261 0 262 0 263 0 264 0 265 3 266 0 267 0 268 0 269 0 270 0 271 2 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 2 284 0 285 0 286 0 287 0 288 0 289 2 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 0 302 0 303 0 304 0 305 0 306 0 307 0 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 0 318 0 319 1 320 0 321 0 322 0 323 0 324 0 325 2 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 1 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 2 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 0 374 0 375 0 376 0 377 0 378 0 379 0 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 1 392 0 393 0 394 0 395 0 396 0 397 0 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 1 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 2 428 0 429 0 430 0 431 0 432 0 433 0 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 0 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 1
35: Average symbolic conclusion length is 69276/797 ≈ 86.92. (Median: 59)
There are 377 minimal D-proofs with conclusions of even symbolic length, and there are 420 minimal D-proofs with conclusions of odd symbolic length. [377/797 ≈ 47.30% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 2 9 0 10 0 11 2 12 0 13 3 14 5 15 0 16 3 17 4 18 1 19 10 20 6 21 12 22 5 23 4 24 9 25 4 26 10 27 12 28 7 29 8 30 10 31 8 32 16 33 7 34 12 35 21 36 6 37 13 38 14 39 7 40 14 41 10 42 12 43 12 44 11 45 12 46 13 47 4 48 22 49 7 50 7 51 6 52 9 53 2 54 9 55 4 56 3 57 7 58 12 59 1 60 8 61 12 62 4 63 1 64 8 65 0 66 10 67 3 68 1 69 3 70 8 71 5 72 2 73 7 74 1 75 2 76 9 77 4 78 3 79 4 80 4 81 3 82 7 83 6 84 4 85 3 86 3 87 1 88 4 89 0 90 1 91 5 92 1 93 1 94 7 95 1 96 0 97 4 98 0 99 1 100 14 101 1 102 2 103 3 104 0 105 0 106 11 107 0 108 1 109 7 110 2 111 1 112 1 113 0 114 0 115 9 116 0 117 0 118 15 119 0 120 0 121 0 122 0 123 0 124 9 125 1 126 1 127 6 128 0 129 3 130 0 131 0 132 1 133 13 134 0 135 0 136 5 137 0 138 0 139 10 140 0 141 0 142 4 143 0 144 0 145 5 146 0 147 2 148 3 149 1 150 0 151 5 152 0 153 0 154 1 155 0 156 1 157 17 158 0 159 0 160 3 161 0 162 0 163 4 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 12 176 0 177 0 178 0 179 0 180 0 181 5 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 2 194 0 195 0 196 0 197 0 198 0 199 6 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 0 210 0 211 6 212 0 213 0 214 0 215 0 216 0 217 2 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 3 230 0 231 1 232 0 233 0 234 0 235 2 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 5 248 0 249 0 250 0 251 0 252 0 253 5 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 2 266 0 267 0 268 0 269 0 270 0 271 7 272 0 273 0 274 0 275 0 276 0 277 1 278 0 279 0 280 0 281 0 282 0 283 2 284 0 285 0 286 0 287 0 288 0 289 2 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 1 302 0 303 0 304 0 305 0 306 0 307 1 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 0 318 0 319 2 320 0 321 0 322 0 323 0 324 0 325 2 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 2 338 0 339 0 340 0 341 0 342 0 343 4 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 0 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 1 374 0 375 0 376 0 377 0 378 0 379 1 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 1 392 0 393 0 394 0 395 0 396 0 397 0 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 2 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 0 428 0 429 0 430 0 431 0 432 0 433 0 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 1 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 1 464 0 465 0 466 0 467 0 468 0 469 0 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 2 482 0 483 0 484 0 485 0 486 0 487 0 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 0 500 0 501 0 502 0 503 0 504 0 505 0 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 1
37: Average symbolic conclusion length is 100819/1162 ≈ 86.76. (Median: 58)
There are 573 minimal D-proofs with conclusions of even symbolic length, and there are 589 minimal D-proofs with conclusions of odd symbolic length. [573/1162 ≈ 49.31% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 1 9 0 10 0 11 1 12 3 13 0 14 3 15 7 16 6 17 14 18 8 19 12 20 7 21 11 22 12 23 6 24 7 25 17 26 9 27 14 28 13 29 15 30 18 31 12 32 16 33 25 34 10 35 23 36 21 37 9 38 17 39 11 40 21 41 14 42 18 43 11 44 12 45 12 46 35 47 6 48 11 49 15 50 12 51 18 52 19 53 2 54 6 55 17 56 12 57 10 58 12 59 9 60 4 61 8 62 5 63 6 64 17 65 7 66 5 67 6 68 3 69 2 70 12 71 3 72 6 73 9 74 3 75 3 76 8 77 2 78 8 79 12 80 3 81 1 82 11 83 1 84 10 85 3 86 0 87 4 88 9 89 1 90 3 91 9 92 0 93 4 94 11 95 1 96 4 97 5 98 1 99 1 100 14 101 0 102 7 103 6 104 1 105 0 106 4 107 0 108 3 109 6 110 0 111 4 112 9 113 0 114 0 115 2 116 0 117 1 118 22 119 1 120 2 121 5 122 0 123 0 124 9 125 5 126 1 127 13 128 1 129 0 130 1 131 0 132 0 133 7 134 0 135 0 136 15 137 6 138 0 139 3 140 0 141 0 142 13 143 1 144 1 145 7 146 0 147 1 148 4 149 0 150 1 151 13 152 0 153 0 154 5 155 0 156 0 157 7 158 0 159 0 160 11 161 0 162 0 163 3 164 0 165 1 166 6 167 1 168 0 169 7 170 0 171 0 172 2 173 0 174 1 175 9 176 0 177 0 178 6 179 0 180 0 181 7 182 0 183 0 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 8 194 0 195 0 196 0 197 0 198 0 199 7 200 0 201 0 202 0 203 0 204 0 205 3 206 0 207 0 208 1 209 0 210 0 211 2 212 0 213 0 214 0 215 0 216 0 217 4 218 0 219 0 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 8 230 0 231 1 232 0 233 0 234 0 235 2 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 6 248 0 249 2 250 0 251 0 252 0 253 2 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 5 266 0 267 0 268 0 269 0 270 0 271 1 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 3 284 0 285 0 286 0 287 0 288 0 289 3 290 0 291 0 292 0 293 0 294 0 295 1 296 0 297 0 298 0 299 0 300 0 301 6 302 0 303 0 304 0 305 0 306 0 307 2 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 0 318 0 319 3 320 0 321 0 322 0 323 0 324 0 325 2 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 2 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 1 356 0 357 0 358 0 359 0 360 0 361 2 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 1 374 0 375 0 376 0 377 0 378 0 379 2 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 2 392 0 393 0 394 0 395 0 396 0 397 2 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 0 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 1 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 1 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 2 464 0 465 0 466 0 467 0 468 0 469 0 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 0 482 0 483 0 484 0 485 0 486 0 487 0 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 1 500 0 501 0 502 0 503 0 504 0 505 0 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 1 518 0 519 0 520 0 521 0 522 0 523 0 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 2 536 0 537 0 538 0 539 0 540 0 541 0 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 0 554 0 555 0 556 0 557 0 558 0 559 0 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 1
39: Average symbolic conclusion length is 154946/1706 ≈ 90.82. (Median: 60)
There are 894 minimal D-proofs with conclusions of even symbolic length, and there are 812 minimal D-proofs with conclusions of odd symbolic length. [894/1706 ≈ 52.40% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 0 10 1 11 0 12 4 13 8 14 5 15 15 16 6 17 11 18 8 19 13 20 18 21 8 22 8 23 17 24 6 25 15 26 22 27 24 28 17 29 16 30 16 31 17 32 20 33 27 34 26 35 12 36 22 37 18 38 22 39 25 40 23 41 22 42 24 43 17 44 30 45 16 46 24 47 35 48 13 49 24 50 20 51 14 52 27 53 16 54 17 55 21 56 15 57 15 58 26 59 6 60 29 61 8 62 10 63 7 64 19 65 3 66 12 67 4 68 4 69 6 70 24 71 2 72 11 73 21 74 5 75 2 76 20 77 0 78 10 79 9 80 1 81 4 82 22 83 2 84 4 85 4 86 1 87 2 88 18 89 3 90 3 91 11 92 4 93 5 94 18 95 6 96 2 97 12 98 5 99 1 100 15 101 1 102 5 103 2 104 1 105 2 106 17 107 7 108 1 109 8 110 0 111 1 112 19 113 1 114 2 115 6 116 2 117 2 118 15 119 1 120 7 121 2 122 2 123 1 124 16 125 0 126 1 127 8 128 1 129 1 130 12 131 0 132 0 133 7 134 0 135 1 136 31 137 1 138 2 139 3 140 0 141 0 142 22 143 0 144 1 145 12 146 2 147 1 148 2 149 0 150 0 151 12 152 0 153 0 154 25 155 0 156 0 157 0 158 0 159 0 160 16 161 1 162 1 163 6 164 0 165 3 166 2 167 0 168 1 169 19 170 0 171 0 172 8 173 0 174 0 175 13 176 0 177 0 178 6 179 0 180 0 181 9 182 0 183 2 184 4 185 1 186 0 187 10 188 0 189 0 190 2 191 0 192 1 193 22 194 0 195 0 196 4 197 0 198 0 199 6 200 0 201 0 202 1 203 0 204 0 205 3 206 0 207 0 208 1 209 0 210 0 211 13 212 0 213 0 214 0 215 0 216 0 217 5 218 0 219 0 220 0 221 0 222 0 223 6 224 0 225 0 226 2 227 0 228 0 229 2 230 0 231 0 232 0 233 0 234 0 235 8 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 6 248 0 249 0 250 0 251 0 252 0 253 2 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 1 263 0 264 0 265 3 266 0 267 1 268 0 269 0 270 0 271 2 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 5 284 0 285 0 286 0 287 0 288 0 289 5 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 3 302 0 303 0 304 0 305 0 306 0 307 7 308 0 309 0 310 0 311 0 312 0 313 1 314 0 315 0 316 0 317 0 318 0 319 4 320 0 321 0 322 0 323 0 324 0 325 2 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 1 338 0 339 0 340 0 341 0 342 0 343 1 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 3 356 0 357 0 358 0 359 0 360 0 361 2 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 2 374 0 375 0 376 0 377 0 378 0 379 5 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 1 392 0 393 0 394 0 395 0 396 0 397 2 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 1 410 0 411 0 412 0 413 0 414 0 415 1 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 1 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 2 446 0 447 0 448 0 449 0 450 0 451 4 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 0 464 0 465 0 466 0 467 0 468 0 469 0 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 1 482 0 483 0 484 0 485 0 486 0 487 1 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 1 500 0 501 0 502 0 503 0 504 0 505 0 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 2 518 0 519 0 520 0 521 0 522 0 523 0 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 0 536 0 537 0 538 0 539 0 540 0 541 0 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 1 554 0 555 0 556 0 557 0 558 0 559 0 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 1 572 0 573 0 574 0 575 0 576 0 577 0 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 2 590 0 591 0 592 0 593 0 594 0 595 0 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 0 608 0 609 0 610 0 611 0 612 0 613 0 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 1
41: Average symbolic conclusion length is 227308/2502 ≈ 90.85. (Median: 63)
There are 1322 minimal D-proofs with conclusions of even symbolic length, and there are 1180 minimal D-proofs with conclusions of odd symbolic length. [1322/2502 ≈ 52.84% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 2 11 3 12 0 13 8 14 7 15 6 16 9 17 11 18 17 19 9 20 7 21 16 22 15 23 23 24 26 25 21 26 23 27 28 28 29 29 38 30 24 31 41 32 26 33 25 34 30 35 27 36 24 37 42 38 28 39 37 40 29 41 39 42 35 43 32 44 31 45 43 46 22 47 40 48 38 49 23 50 30 51 20 52 36 53 18 54 28 55 17 56 19 57 19 58 45 59 14 60 19 61 20 62 22 63 30 64 36 65 8 66 12 67 22 68 18 69 21 70 24 71 15 72 5 73 9 74 6 75 9 76 29 77 10 78 6 79 12 80 5 81 5 82 39 83 5 84 8 85 11 86 4 87 2 88 23 89 3 90 9 91 18 92 4 93 1 94 22 95 5 96 6 97 17 98 0 99 4 100 43 101 1 102 7 103 9 104 0 105 2 106 23 107 1 108 4 109 13 110 1 111 2 112 16 113 1 114 4 115 19 116 2 117 0 118 34 119 0 120 16 121 5 122 0 123 3 124 18 125 0 126 2 127 11 128 0 129 5 130 23 131 1 132 3 133 7 134 1 135 1 136 32 137 0 138 13 139 6 140 1 141 0 142 12 143 0 144 2 145 11 146 0 147 5 148 16 149 6 150 0 151 3 152 0 153 1 154 39 155 1 156 2 157 5 158 0 159 0 160 16 161 7 162 1 163 16 164 1 165 0 166 2 167 0 168 0 169 8 170 0 171 0 172 23 173 0 174 0 175 4 176 0 177 0 178 22 179 1 180 1 181 10 182 0 183 1 184 6 185 0 186 1 187 16 188 0 189 0 190 10 191 0 192 0 193 10 194 0 195 0 196 16 197 0 198 0 199 9 200 0 201 1 202 9 203 1 204 0 205 6 206 0 207 0 208 4 209 0 210 1 211 10 212 0 213 0 214 8 215 0 216 0 217 7 218 0 219 0 220 2 221 0 222 0 223 0 224 0 225 0 226 1 227 0 228 0 229 9 230 0 231 0 232 0 233 0 234 0 235 10 236 0 237 0 238 0 239 0 240 0 241 6 242 0 243 0 244 2 245 0 246 0 247 2 248 0 249 0 250 0 251 0 252 0 253 8 254 0 255 0 256 1 257 0 258 0 259 0 260 0 261 0 262 1 263 0 264 0 265 8 266 0 267 1 268 0 269 0 270 0 271 2 272 0 273 0 274 0 275 0 276 0 277 4 278 0 279 0 280 2 281 0 282 0 283 6 284 0 285 2 286 0 287 0 288 0 289 3 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 5 302 0 303 0 304 0 305 0 306 0 307 1 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 1 317 0 318 0 319 3 320 0 321 0 322 0 323 0 324 0 325 3 326 0 327 0 328 0 329 0 330 0 331 1 332 0 333 0 334 0 335 0 336 0 337 6 338 0 339 0 340 0 341 0 342 0 343 2 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 4 356 0 357 0 358 0 359 0 360 0 361 2 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 0 371 0 372 0 373 5 374 0 375 0 376 0 377 0 378 0 379 0 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 2 392 0 393 0 394 0 395 0 396 0 397 2 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 3 410 0 411 0 412 0 413 0 414 0 415 2 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 2 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 0 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 1 464 0 465 0 466 0 467 0 468 0 469 2 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 1 482 0 483 0 484 0 485 0 486 0 487 2 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 2 500 0 501 0 502 0 503 0 504 0 505 2 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 0 518 0 519 0 520 0 521 0 522 0 523 0 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 1 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 1 554 0 555 0 556 0 557 0 558 0 559 0 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 2 572 0 573 0 574 0 575 0 576 0 577 0 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 0 590 0 591 0 592 0 593 0 594 0 595 0 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 1 608 0 609 0 610 0 611 0 612 0 613 0 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 1 626 0 627 0 628 0 629 0 630 0 631 0 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 2 644 0 645 0 646 0 647 0 648 0 649 0 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 0 662 0 663 0 664 0 665 0 666 0 667 0 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 1
43: Average symbolic conclusion length is 346281/3673 ≈ 94.28. (Median: 64)
There are 1984 minimal D-proofs with conclusions of even symbolic length, and there are 1689 minimal D-proofs with conclusions of odd symbolic length. [1984/3673 ≈ 54.02% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 0 11 3 12 6 13 3 14 6 15 11 16 13 17 9 18 17 19 19 20 19 21 28 22 26 23 36 24 26 25 36 26 35 27 57 28 24 29 50 30 29 31 40 32 50 33 47 34 27 35 49 36 35 37 41 38 46 39 57 40 45 41 43 42 35 43 41 44 43 45 62 46 46 47 35 48 44 49 37 50 47 51 50 52 37 53 39 54 41 55 34 56 48 57 38 58 42 59 51 60 15 61 49 62 28 63 30 64 46 65 26 66 32 67 32 68 22 69 18 70 36 71 7 72 37 73 16 74 12 75 8 76 39 77 8 78 19 79 11 80 7 81 9 82 48 83 3 84 21 85 15 86 6 87 5 88 37 89 0 90 13 91 26 92 1 93 6 94 52 95 3 96 6 97 11 98 2 99 2 100 41 101 4 102 4 103 8 104 5 105 4 106 35 107 3 108 5 109 33 110 6 111 2 112 37 113 0 114 2 115 9 116 1 117 2 118 49 119 7 120 1 121 5 122 0 123 1 124 37 125 2 126 3 127 15 128 2 129 4 130 29 131 8 132 2 133 15 134 4 135 1 136 36 137 0 138 7 139 2 140 1 141 2 142 35 143 1 144 1 145 9 146 0 147 1 148 32 149 1 150 2 151 9 152 2 153 2 154 33 155 0 156 11 157 2 158 2 159 1 160 32 161 0 162 1 163 9 164 1 165 1 166 19 167 0 168 0 169 11 170 0 171 1 172 56 173 1 174 2 175 3 176 0 177 0 178 40 179 0 180 1 181 16 182 2 183 1 184 6 185 0 186 0 187 18 188 0 189 0 190 38 191 0 192 0 193 0 194 0 195 0 196 27 197 1 198 1 199 7 200 0 201 3 202 4 203 0 204 1 205 23 206 0 207 0 208 14 209 0 210 0 211 16 212 0 213 0 214 8 215 0 216 0 217 9 218 0 219 2 220 6 221 1 222 0 223 10 224 0 225 0 226 5 227 0 228 1 229 25 230 0 231 0 232 7 233 0 234 0 235 7 236 0 237 0 238 2 239 0 240 0 241 6 242 0 243 0 244 4 245 0 246 0 247 15 248 0 249 0 250 0 251 0 252 0 253 7 254 0 255 0 256 1 257 0 258 0 259 12 260 0 261 0 262 4 263 0 264 0 265 2 266 0 267 0 268 0 269 0 270 0 271 8 272 0 273 0 274 2 275 0 276 0 277 4 278 0 279 0 280 1 281 0 282 0 283 6 284 0 285 0 286 0 287 0 288 0 289 6 290 0 291 0 292 0 293 0 294 0 295 8 296 0 297 0 298 2 299 0 300 0 301 3 302 0 303 1 304 0 305 0 306 0 307 4 308 0 309 0 310 1 311 0 312 0 313 0 314 0 315 0 316 1 317 0 318 0 319 5 320 0 321 0 322 0 323 0 324 0 325 5 326 0 327 0 328 0 329 0 330 0 331 0 332 0 333 0 334 2 335 0 336 0 337 3 338 0 339 0 340 0 341 0 342 0 343 9 344 0 345 0 346 0 347 0 348 0 349 1 350 0 351 0 352 0 353 0 354 0 355 4 356 0 357 0 358 0 359 0 360 0 361 2 362 0 363 0 364 0 365 0 366 0 367 0 368 0 369 0 370 1 371 0 372 0 373 2 374 0 375 0 376 0 377 0 378 0 379 1 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 5 392 0 393 0 394 0 395 0 396 0 397 2 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 2 410 0 411 0 412 0 413 0 414 0 415 5 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 2 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 1 446 0 447 0 448 0 449 0 450 0 451 1 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 2 464 0 465 0 466 0 467 0 468 0 469 2 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 2 482 0 483 0 484 0 485 0 486 0 487 5 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 0 500 0 501 0 502 0 503 0 504 0 505 2 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 1 518 0 519 0 520 0 521 0 522 0 523 1 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 1 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 2 554 0 555 0 556 0 557 0 558 0 559 4 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 0 572 0 573 0 574 0 575 0 576 0 577 0 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 1 590 0 591 0 592 0 593 0 594 0 595 1 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 1 608 0 609 0 610 0 611 0 612 0 613 0 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 2 626 0 627 0 628 0 629 0 630 0 631 0 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 0 644 0 645 0 646 0 647 0 648 0 649 0 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 1 662 0 663 0 664 0 665 0 666 0 667 0 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 1 680 0 681 0 682 0 683 0 684 0 685 0 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 2 698 0 699 0 700 0 701 0 702 0 703 0 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 0 716 0 717 0 718 0 719 0 720 0 721 0 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 1
45: Average symbolic conclusion length is 513077/5333 ≈ 96.21. (Median: 66)
There are 2812 minimal D-proofs with conclusions of even symbolic length, and there are 2521 minimal D-proofs with conclusions of odd symbolic length. [2812/5333 ≈ 52.73% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 2 11 1 12 3 13 6 14 7 15 8 16 15 17 18 18 6 19 25 20 22 21 24 22 20 23 28 24 32 25 48 26 36 27 42 28 39 29 51 30 54 31 59 32 36 33 60 34 65 35 71 36 55 37 78 38 64 39 70 40 66 41 100 42 52 43 107 44 61 45 69 46 53 47 64 48 49 49 96 50 55 51 77 52 51 53 77 54 59 55 64 56 48 57 72 58 37 59 65 60 58 61 36 62 45 63 36 64 55 65 29 66 43 67 39 68 31 69 25 70 70 71 24 72 30 73 35 74 35 75 48 76 39 77 17 78 10 79 35 80 28 81 34 82 33 83 25 84 13 85 30 86 10 87 22 88 49 89 11 90 10 91 12 92 9 93 14 94 35 95 11 96 9 97 17 98 9 99 4 100 50 101 5 102 22 103 24 104 5 105 8 106 57 107 5 108 7 109 17 110 0 111 5 112 58 113 3 114 5 115 23 116 2 117 2 118 85 119 12 120 10 121 17 122 2 123 1 124 52 125 2 126 6 127 32 128 3 129 0 130 44 131 0 132 5 133 25 134 0 135 3 136 90 137 1 138 9 139 7 140 0 141 2 142 43 143 2 144 4 145 15 146 1 147 2 148 31 149 0 150 3 151 26 152 2 153 0 154 71 155 0 156 25 157 5 158 0 159 3 160 32 161 0 162 2 163 17 164 0 165 6 166 43 167 1 168 2 169 12 170 1 171 1 172 64 173 7 174 21 175 6 176 1 177 0 178 22 179 0 180 2 181 15 182 0 183 6 184 26 185 8 186 0 187 9 188 0 189 1 190 63 191 1 192 2 193 5 194 0 195 0 196 28 197 0 198 1 199 19 200 1 201 0 202 5 203 0 204 0 205 15 206 0 207 0 208 36 209 0 210 0 211 5 212 0 213 0 214 32 215 1 216 1 217 11 218 0 219 1 220 9 221 0 222 1 223 19 224 0 225 0 226 21 227 0 228 0 229 11 230 0 231 0 232 23 233 0 234 0 235 12 236 0 237 1 238 14 239 1 240 0 241 6 242 0 243 0 244 8 245 0 246 1 247 11 248 0 249 0 250 14 251 0 252 0 253 10 254 0 255 0 256 4 257 0 258 0 259 0 260 0 261 0 262 4 263 0 264 0 265 10 266 0 267 0 268 0 269 0 270 0 271 10 272 0 273 0 274 1 275 0 276 0 277 6 278 0 279 0 280 5 281 0 282 0 283 2 284 0 285 0 286 1 287 0 288 0 289 11 290 0 291 0 292 2 293 0 294 0 295 0 296 0 297 0 298 4 299 0 300 0 301 8 302 0 303 1 304 0 305 0 306 0 307 8 308 0 309 0 310 1 311 0 312 0 313 8 314 0 315 0 316 4 317 0 318 0 319 6 320 0 321 2 322 0 323 0 324 0 325 3 326 0 327 0 328 2 329 0 330 0 331 0 332 0 333 0 334 1 335 0 336 0 337 5 338 0 339 0 340 0 341 0 342 0 343 4 344 0 345 0 346 0 347 0 348 0 349 5 350 0 351 0 352 2 353 0 354 0 355 3 356 0 357 0 358 0 359 0 360 0 361 7 362 0 363 0 364 1 365 0 366 0 367 1 368 0 369 0 370 1 371 0 372 0 373 6 374 0 375 0 376 0 377 0 378 0 379 2 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 0 388 2 389 0 390 0 391 4 392 0 393 0 394 0 395 0 396 0 397 3 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 5 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 1 425 0 426 0 427 3 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 6 446 0 447 0 448 0 449 0 450 0 451 2 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 3 464 0 465 0 466 0 467 0 468 0 469 2 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 2 482 0 483 0 484 0 485 0 486 0 487 0 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 1 500 0 501 0 502 0 503 0 504 0 505 2 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 1 518 0 519 0 520 0 521 0 522 0 523 2 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 2 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 0 554 0 555 0 556 0 557 0 558 0 559 0 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 1 572 0 573 0 574 0 575 0 576 0 577 2 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 1 590 0 591 0 592 0 593 0 594 0 595 2 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 2 608 0 609 0 610 0 611 0 612 0 613 2 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 0 626 0 627 0 628 0 629 0 630 0 631 0 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 1 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 1 662 0 663 0 664 0 665 0 666 0 667 0 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 2 680 0 681 0 682 0 683 0 684 0 685 0 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 0 698 0 699 0 700 0 701 0 702 0 703 0 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 1 716 0 717 0 718 0 719 0 720 0 721 0 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 1 734 0 735 0 736 0 737 0 738 0 739 0 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 2 752 0 753 0 754 0 755 0 756 0 757 0 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 0 770 0 771 0 772 0 773 0 774 0 775 0 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 1
47: Average symbolic conclusion length is 774113/7756 ≈ 99.81. (Median: 68)
There are 4063 minimal D-proofs with conclusions of even symbolic length, and there are 3693 minimal D-proofs with conclusions of odd symbolic length. [4063/7756 ≈ 52.39% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 1 12 1 13 3 14 10 15 9 16 5 17 14 18 19 19 11 20 13 21 30 22 31 23 33 24 44 25 61 26 46 27 60 28 65 29 78 30 57 31 82 32 72 33 102 34 71 35 122 36 66 37 106 38 88 39 150 40 63 41 131 42 81 43 101 44 95 45 110 46 56 47 116 48 83 49 95 50 81 51 123 52 84 53 102 54 61 55 76 56 76 57 115 58 78 59 77 60 73 61 68 62 85 63 96 64 54 65 65 66 64 67 78 68 70 69 76 70 59 71 76 72 25 73 83 74 39 75 55 76 61 77 42 78 36 79 56 80 33 81 30 82 48 83 11 84 50 85 38 86 20 87 10 88 55 89 16 90 33 91 22 92 13 93 15 94 62 95 5 96 18 97 45 98 9 99 17 100 76 101 6 102 31 103 38 104 2 105 7 106 74 107 3 108 13 109 28 110 2 111 3 112 75 113 6 114 8 115 34 116 8 117 9 118 86 119 4 120 20 121 23 122 7 123 4 124 65 125 0 126 3 127 49 128 1 129 4 130 97 131 3 132 4 133 18 134 1 135 1 136 81 137 2 138 6 139 18 140 3 141 2 142 67 143 9 144 3 145 58 146 5 147 2 148 69 149 1 150 2 151 13 152 1 153 2 154 88 155 9 156 1 157 9 158 0 159 1 160 71 161 1 162 2 163 21 164 2 165 4 166 46 167 1 168 2 169 20 170 4 171 1 172 69 173 0 174 11 175 2 176 1 177 2 178 57 179 0 180 1 181 16 182 0 183 1 184 49 185 1 186 2 187 10 188 2 189 2 190 63 191 0 192 16 193 2 194 2 195 1 196 56 197 0 198 1 199 12 200 1 201 1 202 28 203 0 204 0 205 14 206 0 207 1 208 90 209 1 210 2 211 3 212 0 213 0 214 65 215 0 216 1 217 20 218 2 219 1 220 11 221 0 222 0 223 24 224 0 225 0 226 63 227 0 228 0 229 0 230 0 231 0 232 40 233 1 234 1 235 10 236 0 237 3 238 6 239 0 240 1 241 28 242 0 243 0 244 28 245 0 246 0 247 18 248 0 249 0 250 12 251 0 252 0 253 11 254 0 255 2 256 9 257 1 258 0 259 13 260 0 261 0 262 14 263 0 264 1 265 28 266 0 267 0 268 10 269 0 270 0 271 7 272 0 273 0 274 4 275 0 276 0 277 6 278 0 279 0 280 13 281 0 282 0 283 17 284 0 285 0 286 2 287 0 288 0 289 8 290 0 291 0 292 4 293 0 294 0 295 12 296 0 297 0 298 8 299 0 300 0 301 2 302 0 303 0 304 2 305 0 306 0 307 9 308 0 309 0 310 4 311 0 312 0 313 8 314 0 315 0 316 3 317 0 318 0 319 6 320 0 321 0 322 0 323 0 324 0 325 6 326 0 327 0 328 1 329 0 330 0 331 16 332 0 333 0 334 5 335 0 336 0 337 3 338 0 339 1 340 2 341 0 342 0 343 6 344 0 345 0 346 2 347 0 348 0 349 5 350 0 351 0 352 4 353 0 354 0 355 5 356 0 357 0 358 0 359 0 360 0 361 7 362 0 363 0 364 1 365 0 366 0 367 10 368 0 369 0 370 4 371 0 372 0 373 3 374 0 375 0 376 0 377 0 378 0 379 9 380 0 381 0 382 2 383 0 384 0 385 1 386 0 387 0 388 1 389 0 390 0 391 4 392 0 393 0 394 0 395 0 396 0 397 6 398 0 399 0 400 0 401 0 402 0 403 0 404 0 405 0 406 2 407 0 408 0 409 2 410 0 411 0 412 0 413 0 414 0 415 3 416 0 417 0 418 1 419 0 420 0 421 0 422 0 423 0 424 1 425 0 426 0 427 5 428 0 429 0 430 0 431 0 432 0 433 2 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 2 443 0 444 0 445 3 446 0 447 0 448 0 449 0 450 0 451 7 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 4 464 0 465 0 466 0 467 0 468 0 469 2 470 0 471 0 472 0 473 0 474 0 475 0 476 0 477 0 478 1 479 0 480 0 481 1 482 0 483 0 484 0 485 0 486 0 487 1 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 3 500 0 501 0 502 0 503 0 504 0 505 2 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 2 518 0 519 0 520 0 521 0 522 0 523 5 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 0 534 0 535 1 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 1 554 0 555 0 556 0 557 0 558 0 559 1 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 1 572 0 573 0 574 0 575 0 576 0 577 2 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 2 590 0 591 0 592 0 593 0 594 0 595 5 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 0 608 0 609 0 610 0 611 0 612 0 613 2 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 1 626 0 627 0 628 0 629 0 630 0 631 1 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 1 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 2 662 0 663 0 664 0 665 0 666 0 667 4 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 0 680 0 681 0 682 0 683 0 684 0 685 0 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 1 698 0 699 0 700 0 701 0 702 0 703 1 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 1 716 0 717 0 718 0 719 0 720 0 721 0 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 2 734 0 735 0 736 0 737 0 738 0 739 0 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 0 752 0 753 0 754 0 755 0 756 0 757 0 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 1 770 0 771 0 772 0 773 0 774 0 775 0 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 1 788 0 789 0 790 0 791 0 792 0 793 0 794 0 795 0 796 0 797 0 798 0 799 0 800 0
49: Average symbolic conclusion length is 1155663/11285 ≈ 102.41. (Median: 69)
There are 5670 minimal D-proofs with conclusions of even symbolic length, and there are 5615 minimal D-proofs with conclusions of odd symbolic length. [5670/11285 ≈ 50.24% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 3 12 7 13 4 14 4 15 12 16 10 17 8 18 13 19 26 20 22 21 40 22 40 23 54 24 39 25 57 26 63 27 71 28 55 29 92 30 56 31 103 32 94 33 120 34 69 35 110 36 98 37 158 38 99 39 138 40 125 41 129 42 118 43 165 44 99 45 165 46 149 47 175 48 106 49 185 50 128 51 172 52 122 53 199 54 93 55 215 56 106 57 155 58 94 59 131 60 90 61 191 62 93 63 141 64 78 65 144 66 90 67 122 68 75 69 127 70 62 71 110 72 81 73 71 74 62 75 60 76 80 77 48 78 65 79 72 80 42 81 42 82 85 83 40 84 43 85 75 86 51 87 68 88 78 89 35 90 16 91 82 92 36 93 42 94 52 95 37 96 15 97 48 98 19 99 39 100 50 101 15 102 12 103 43 104 20 105 23 106 78 107 23 108 19 109 49 110 15 111 31 112 57 113 7 114 14 115 59 116 14 117 28 118 61 119 8 120 18 121 62 122 3 123 8 124 110 125 3 126 13 127 34 128 2 129 7 130 78 131 15 132 7 133 50 134 6 135 2 136 103 137 4 138 27 139 49 140 4 141 3 142 122 143 16 144 6 145 35 146 0 147 4 148 105 149 3 150 5 151 37 152 2 153 2 154 155 155 4 156 16 157 28 158 2 159 1 160 96 161 2 162 5 163 47 164 3 165 0 166 77 167 3 168 5 169 35 170 0 171 3 172 155 173 0 174 12 175 11 176 0 177 2 178 71 179 1 180 3 181 25 182 1 183 2 184 54 185 0 186 3 187 33 188 2 189 0 190 125 191 1 192 37 193 5 194 0 195 3 196 51 197 8 198 2 199 29 200 0 201 7 202 69 203 1 204 2 205 13 206 1 207 1 208 110 209 9 210 31 211 6 212 1 213 0 214 39 215 0 216 2 217 19 218 0 219 7 220 41 221 0 222 0 223 15 224 0 225 1 226 95 227 1 228 2 229 5 230 0 231 0 232 42 233 0 234 1 235 24 236 1 237 0 238 11 239 0 240 0 241 24 242 0 243 0 244 55 245 0 246 0 247 6 248 0 249 0 250 48 251 1 252 1 253 10 254 0 255 1 256 13 257 0 258 1 259 28 260 0 261 0 262 45 263 0 264 0 265 13 266 0 267 0 268 34 269 0 270 0 271 13 272 0 273 1 274 21 275 1 276 0 277 14 278 0 279 0 280 24 281 0 282 1 283 12 284 0 285 0 286 21 287 0 288 0 289 13 290 0 291 0 292 6 293 0 294 0 295 0 296 0 297 0 298 11 299 0 300 0 301 11 302 0 303 0 304 3 305 0 306 0 307 10 308 0 309 0 310 2 311 0 312 0 313 6 314 0 315 0 316 16 317 0 318 0 319 2 320 0 321 0 322 2 323 0 324 0 325 11 326 0 327 0 328 4 329 0 330 0 331 0 332 0 333 0 334 13 335 0 336 0 337 8 338 0 339 1 340 2 341 0 342 0 343 12 344 0 345 0 346 4 347 0 348 0 349 8 350 0 351 0 352 8 353 0 354 0 355 6 356 0 357 2 358 4 359 0 360 0 361 6 362 0 363 0 364 4 365 0 366 0 367 0 368 0 369 0 370 3 371 0 372 0 373 5 374 0 375 0 376 0 377 0 378 0 379 4 380 0 381 0 382 1 383 0 384 0 385 10 386 0 387 0 388 5 389 0 390 0 391 3 392 0 393 0 394 1 395 0 396 0 397 10 398 0 399 0 400 2 401 0 402 0 403 1 404 0 405 0 406 4 407 0 408 0 409 6 410 0 411 0 412 0 413 0 414 0 415 8 416 0 417 0 418 1 419 0 420 0 421 6 422 0 423 0 424 4 425 0 426 0 427 4 428 0 429 0 430 0 431 0 432 0 433 3 434 0 435 0 436 2 437 0 438 0 439 0 440 0 441 0 442 1 443 0 444 0 445 5 446 0 447 0 448 0 449 0 450 0 451 3 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 2 461 0 462 0 463 3 464 0 465 0 466 0 467 0 468 0 469 6 470 0 471 0 472 1 473 0 474 0 475 0 476 0 477 0 478 1 479 0 480 0 481 6 482 0 483 0 484 0 485 0 486 0 487 2 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 2 497 0 498 0 499 4 500 0 501 0 502 0 503 0 504 0 505 3 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 0 515 0 516 0 517 5 518 0 519 0 520 0 521 0 522 0 523 0 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 1 533 0 534 0 535 2 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 0 551 0 552 0 553 3 554 0 555 0 556 0 557 0 558 0 559 2 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 2 572 0 573 0 574 0 575 0 576 0 577 2 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 0 587 0 588 0 589 0 590 0 591 0 592 0 593 0 594 0 595 0 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 1 608 0 609 0 610 0 611 0 612 0 613 2 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 1 626 0 627 0 628 0 629 0 630 0 631 2 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 2 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 0 662 0 663 0 664 0 665 0 666 0 667 0 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 1 680 0 681 0 682 0 683 0 684 0 685 2 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 1 698 0 699 0 700 0 701 0 702 0 703 2 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 2 716 0 717 0 718 0 719 0 720 0 721 2 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 0 734 0 735 0 736 0 737 0 738 0 739 0 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 1 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 1 770 0 771 0 772 0 773 0 774 0 775 0 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 2 788 0 789 0 790 0 791 0 792 0 793 0 794 0 795 0 796 0 797 0 798 0 799 0 800 0
51: Average symbolic conclusion length is 1739492/16457 ≈ 105.70. (Median: 73)
There are 8093 minimal D-proofs with conclusions of even symbolic length, and there are 8364 minimal D-proofs with conclusions of odd symbolic length. [8093/16457 ≈ 49.18% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 3 11 4 12 2 13 9 14 5 15 4 16 8 17 13 18 3 19 30 20 32 21 37 22 37 23 44 24 49 25 48 26 59 27 81 28 64 29 89 30 97 31 125 32 88 33 144 34 127 35 163 36 128 37 218 38 156 39 179 40 163 41 240 42 147 43 234 44 174 45 250 46 161 47 305 48 150 49 275 50 173 51 318 52 128 53 273 54 165 55 244 56 159 57 223 58 116 59 228 60 156 61 202 62 134 63 224 64 150 65 205 66 105 67 152 68 130 69 202 70 123 71 146 72 113 73 138 74 129 75 165 76 101 77 111 78 90 79 149 80 99 81 140 82 90 83 123 84 42 85 157 86 60 87 105 88 81 89 76 90 49 91 101 92 44 93 44 94 72 95 23 96 61 97 72 98 36 99 30 100 67 101 24 102 43 103 81 104 21 105 34 106 91 107 16 108 31 109 93 110 12 111 26 112 100 113 21 114 28 115 102 116 10 117 15 118 98 119 6 120 21 121 80 122 8 123 5 124 114 125 15 126 31 127 73 128 12 129 14 130 116 131 6 132 11 133 102 134 10 135 18 136 142 137 2 138 26 139 76 140 2 141 7 142 143 143 3 144 18 145 62 146 1 147 1 148 138 149 4 150 7 151 67 152 6 153 8 154 160 155 4 156 25 157 56 158 6 159 4 160 123 161 0 162 3 163 88 164 1 165 3 166 166 167 10 168 2 169 31 170 1 171 1 172 139 173 3 174 9 175 41 176 3 177 2 178 122 179 11 180 3 181 90 182 5 183 2 184 113 185 0 186 1 187 22 188 1 189 2 190 140 191 1 192 1 193 14 194 0 195 1 196 121 197 1 198 2 199 35 200 2 201 4 202 69 203 0 204 2 205 29 206 4 207 1 208 115 209 0 210 16 211 2 212 1 213 2 214 86 215 0 216 1 217 23 218 0 219 1 220 71 221 1 222 2 223 14 224 2 225 2 226 101 227 0 228 22 229 3 230 2 231 1 232 86 233 0 234 1 235 15 236 1 237 1 238 40 239 0 240 0 241 19 242 0 243 1 244 130 245 1 246 2 247 3 248 0 249 0 250 98 251 0 252 1 253 26 254 2 255 1 256 18 257 0 258 0 259 30 260 0 261 0 262 99 263 0 264 0 265 0 266 0 267 0 268 61 269 1 270 1 271 11 272 0 273 3 274 9 275 0 276 1 277 34 278 0 279 0 280 57 281 0 282 0 283 19 284 0 285 0 286 16 287 0 288 0 289 15 290 0 291 2 292 13 293 1 294 0 295 17 296 0 297 0 298 30 299 0 300 1 301 31 302 0 303 0 304 17 305 0 306 0 307 11 308 0 309 0 310 6 311 0 312 0 313 7 314 0 315 0 316 37 317 0 318 0 319 19 320 0 321 0 322 6 323 0 324 0 325 9 326 0 327 0 328 8 329 0 330 0 331 17 332 0 333 0 334 30 335 0 336 0 337 2 338 0 339 0 340 4 341 0 342 0 343 12 344 0 345 0 346 6 347 0 348 0 349 8 350 0 351 0 352 12 353 0 354 0 355 6 356 0 357 0 358 2 359 0 360 0 361 10 362 0 363 0 364 2 365 0 366 0 367 16 368 0 369 0 370 16 371 0 372 0 373 3 374 0 375 1 376 4 377 0 378 0 379 6 380 0 381 0 382 4 383 0 384 0 385 10 386 0 387 0 388 11 389 0 390 0 391 5 392 0 393 0 394 2 395 0 396 0 397 8 398 0 399 0 400 4 401 0 402 0 403 20 404 0 405 0 406 8 407 0 408 0 409 3 410 0 411 0 412 2 413 0 414 0 415 10 416 0 417 0 418 4 419 0 420 0 421 7 422 0 423 0 424 3 425 0 426 0 427 4 428 0 429 0 430 0 431 0 432 0 433 6 434 0 435 0 436 1 437 0 438 0 439 12 440 0 441 0 442 5 443 0 444 0 445 2 446 0 447 0 448 2 449 0 450 0 451 5 452 0 453 0 454 2 455 0 456 0 457 0 458 0 459 0 460 4 461 0 462 0 463 5 464 0 465 0 466 0 467 0 468 0 469 4 470 0 471 0 472 1 473 0 474 0 475 0 476 0 477 0 478 4 479 0 480 0 481 3 482 0 483 0 484 0 485 0 486 0 487 7 488 0 489 0 490 2 491 0 492 0 493 0 494 0 495 0 496 1 497 0 498 0 499 4 500 0 501 0 502 0 503 0 504 0 505 6 506 0 507 0 508 0 509 0 510 0 511 0 512 0 513 0 514 2 515 0 516 0 517 2 518 0 519 0 520 0 521 0 522 0 523 3 524 0 525 0 526 1 527 0 528 0 529 0 530 0 531 0 532 1 533 0 534 0 535 5 536 0 537 0 538 0 539 0 540 0 541 2 542 0 543 0 544 0 545 0 546 0 547 0 548 0 549 0 550 2 551 0 552 0 553 2 554 0 555 0 556 0 557 0 558 0 559 7 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 0 569 0 570 0 571 2 572 0 573 0 574 0 575 0 576 0 577 2 578 0 579 0 580 0 581 0 582 0 583 0 584 0 585 0 586 1 587 0 588 0 589 1 590 0 591 0 592 0 593 0 594 0 595 1 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 0 606 0 607 2 608 0 609 0 610 0 611 0 612 0 613 2 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 2 626 0 627 0 628 0 629 0 630 0 631 5 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 0 641 0 642 0 643 0 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 1 662 0 663 0 664 0 665 0 666 0 667 1 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 1 680 0 681 0 682 0 683 0 684 0 685 2 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 2 698 0 699 0 700 0 701 0 702 0 703 5 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 0 716 0 717 0 718 0 719 0 720 0 721 2 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 1 734 0 735 0 736 0 737 0 738 0 739 1 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 1 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 2 770 0 771 0 772 0 773 0 774 0 775 4 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 0 788 0 789 0 790 0 791 0 792 0 793 0 794 0 795 0 796 0 797 0 798 0 799 0 800 0
53: Average symbolic conclusion length is 2612804/24156 ≈ 108.16. (Median: 74)
There are 11344 minimal D-proofs with conclusions of even symbolic length, and there are 12812 minimal D-proofs with conclusions of odd symbolic length. [11344/24156 ≈ 46.96% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 4 12 3 13 3 14 5 15 9 16 3 17 19 18 38 19 28 20 47 21 45 22 46 23 54 24 83 25 82 26 70 27 123 28 95 29 110 30 102 31 179 32 149 33 193 34 147 35 234 36 144 37 227 38 214 39 267 40 166 41 300 42 173 43 300 44 235 45 343 46 206 47 294 48 220 49 411 50 229 51 352 52 285 53 306 54 233 55 377 56 221 57 362 58 282 59 345 60 202 61 374 62 217 63 365 64 202 65 343 66 156 67 406 68 165 69 303 70 156 71 246 72 145 73 339 74 140 75 244 76 131 77 243 78 129 79 216 80 105 81 209 82 94 83 178 84 113 85 153 86 89 87 112 88 136 89 90 90 102 91 146 92 58 93 71 94 145 95 79 96 70 97 168 98 68 99 111 100 95 101 70 102 24 103 161 104 49 105 76 106 104 107 60 108 30 109 129 110 30 111 43 112 87 113 23 114 20 115 116 116 27 117 30 118 76 119 29 120 21 121 120 122 29 123 65 124 141 125 18 126 20 127 153 128 24 129 46 130 115 131 31 132 17 133 131 134 8 135 49 136 95 137 6 138 13 139 123 140 14 141 30 142 173 143 16 144 22 145 130 146 11 147 10 148 139 149 6 150 11 151 147 152 8 153 15 154 126 155 19 156 22 157 136 158 2 159 6 160 214 161 3 162 16 163 81 164 2 165 2 166 149 167 31 168 7 169 107 170 6 171 2 172 193 173 4 174 39 175 104 176 4 177 4 178 212 179 3 180 6 181 68 182 0 183 4 184 174 185 3 186 4 187 64 188 2 189 2 190 250 191 9 192 24 193 54 194 2 195 1 196 162 197 1 198 4 199 74 200 3 201 0 202 120 203 1 204 4 205 50 206 0 207 3 208 245 209 0 210 17 211 15 212 0 213 2 214 115 215 4 216 2 217 41 218 1 219 2 220 86 221 9 222 3 223 43 224 2 225 0 226 199 227 0 228 53 229 10 230 0 231 3 232 79 233 10 234 2 235 39 236 0 237 8 238 107 239 2 240 2 241 16 242 1 243 1 244 169 245 0 246 43 247 8 248 1 249 0 250 63 251 0 252 2 253 26 254 0 255 8 256 61 257 0 258 0 259 18 260 0 261 1 262 139 263 1 264 2 265 6 266 0 267 0 268 61 269 0 270 1 271 29 272 1 273 0 274 18 275 0 276 0 277 25 278 0 279 0 280 81 281 0 282 0 283 7 284 0 285 0 286 68 287 1 288 1 289 13 290 0 291 1 292 20 293 0 294 1 295 39 296 0 297 0 298 68 299 0 300 0 301 15 302 0 303 0 304 49 305 0 306 0 307 19 308 0 309 1 310 31 311 1 312 0 313 24 314 0 315 0 316 46 317 0 318 1 319 13 320 0 321 0 322 34 323 0 324 0 325 14 326 0 327 0 328 9 329 0 330 0 331 8 332 0 333 0 334 28 335 0 336 0 337 12 338 0 339 0 340 6 341 0 342 0 343 11 344 0 345 0 346 5 347 0 348 0 349 16 350 0 351 0 352 28 353 0 354 0 355 2 356 0 357 0 358 8 359 0 360 0 361 11 362 0 363 0 364 6 365 0 366 0 367 0 368 0 369 0 370 44 371 0 372 0 373 8 374 0 375 1 376 8 377 0 378 0 379 13 380 0 381 0 382 7 383 0 384 0 385 8 386 0 387 0 388 29 389 0 390 0 391 6 392 0 393 2 394 9 395 0 396 0 397 10 398 0 399 0 400 6 401 0 402 0 403 0 404 0 405 0 406 9 407 0 408 0 409 5 410 0 411 0 412 3 413 0 414 0 415 4 416 0 417 0 418 2 419 0 420 0 421 10 422 0 423 0 424 22 425 0 426 0 427 3 428 0 429 0 430 2 431 0 432 0 433 10 434 0 435 0 436 4 437 0 438 0 439 1 440 0 441 0 442 12 443 0 444 0 445 6 446 0 447 0 448 2 449 0 450 0 451 13 452 0 453 0 454 4 455 0 456 0 457 12 458 0 459 0 460 8 461 0 462 0 463 4 464 0 465 0 466 4 467 0 468 0 469 6 470 0 471 0 472 4 473 0 474 0 475 0 476 0 477 0 478 3 479 0 480 0 481 5 482 0 483 0 484 0 485 0 486 0 487 3 488 0 489 0 490 1 491 0 492 0 493 7 494 0 495 0 496 5 497 0 498 0 499 3 500 0 501 0 502 1 503 0 504 0 505 9 506 0 507 0 508 2 509 0 510 0 511 0 512 0 513 0 514 4 515 0 516 0 517 6 518 0 519 0 520 0 521 0 522 0 523 8 524 0 525 0 526 1 527 0 528 0 529 0 530 0 531 0 532 4 533 0 534 0 535 4 536 0 537 0 538 0 539 0 540 0 541 3 542 0 543 0 544 2 545 0 546 0 547 0 548 0 549 0 550 1 551 0 552 0 553 5 554 0 555 0 556 0 557 0 558 0 559 3 560 0 561 0 562 0 563 0 564 0 565 0 566 0 567 0 568 2 569 0 570 0 571 3 572 0 573 0 574 0 575 0 576 0 577 6 578 0 579 0 580 1 581 0 582 0 583 0 584 0 585 0 586 1 587 0 588 0 589 6 590 0 591 0 592 0 593 0 594 0 595 2 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 2 605 0 606 0 607 3 608 0 609 0 610 0 611 0 612 0 613 3 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 0 625 2 626 0 627 0 628 0 629 0 630 0 631 0 632 0 633 0 634 0 635 0 636 0 637 0 638 0 639 0 640 1 641 0 642 0 643 1 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 0 661 1 662 0 663 0 664 0 665 0 666 0 667 2 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 2 680 0 681 0 682 0 683 0 684 0 685 2 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 0 695 0 696 0 697 0 698 0 699 0 700 0 701 0 702 0 703 0 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 1 716 0 717 0 718 0 719 0 720 0 721 2 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 1 734 0 735 0 736 0 737 0 738 0 739 2 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 2 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 0 770 0 771 0 772 0 773 0 774 0 775 0 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 1 788 0 789 0 790 0 791 0 792 0 793 2 794 0 795 0 796 0 797 0 798 0 799 0 800 0
55: Average symbolic conclusion length is 3960911/35569 ≈ 111.36. (Median: 77)
There are 16340 minimal D-proofs with conclusions of even symbolic length, and there are 19229 minimal D-proofs with conclusions of odd symbolic length. [16340/35569 ≈ 45.94% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 1 11 2 12 1 13 6 14 4 15 8 16 23 17 13 18 37 19 35 20 37 21 42 22 67 23 68 24 49 25 98 26 81 27 108 28 137 29 151 30 126 31 174 32 174 33 222 34 192 35 244 36 222 37 267 38 241 39 324 40 264 41 353 42 295 43 436 44 313 45 456 46 361 47 464 48 336 49 553 50 383 51 466 52 365 53 550 54 344 55 565 56 353 57 537 58 301 59 618 60 292 61 590 62 303 63 599 64 246 65 503 66 288 67 482 68 272 69 432 70 227 71 425 72 251 73 387 74 220 75 384 76 248 77 358 78 172 79 297 80 198 81 330 82 210 83 248 84 160 85 277 86 188 87 262 88 166 89 183 90 135 91 301 92 137 93 241 94 162 95 190 96 75 97 301 98 80 99 189 100 137 101 123 102 64 103 235 104 66 105 87 106 116 107 53 108 96 109 193 110 55 111 64 112 136 113 54 114 60 115 203 116 31 117 74 118 126 119 44 120 37 121 239 122 25 123 71 124 136 125 53 126 48 127 201 128 18 129 31 130 146 131 15 132 23 133 207 134 20 135 14 136 142 137 27 138 30 139 226 140 20 141 27 142 189 143 23 144 33 145 218 146 13 147 29 148 193 149 20 150 18 151 254 152 9 153 18 154 190 155 6 156 24 157 196 158 7 159 3 160 226 161 8 162 46 163 171 164 10 165 13 166 219 167 6 168 11 169 214 170 9 171 19 172 263 173 2 174 31 175 162 176 2 177 5 178 253 179 3 180 25 181 133 182 1 183 2 184 228 185 4 186 7 187 123 188 6 189 8 190 275 191 12 192 30 193 125 194 6 195 4 196 208 197 1 198 3 199 159 200 1 201 3 202 254 203 12 204 2 205 67 206 1 207 1 208 234 209 2 210 12 211 79 212 3 213 3 214 213 215 2 216 3 217 150 218 5 219 2 220 167 221 0 222 1 223 43 224 1 225 2 226 219 227 0 228 1 229 26 230 0 231 1 232 195 233 1 234 2 235 66 236 2 237 4 238 100 239 0 240 2 241 44 242 4 243 1 244 173 245 0 246 22 247 10 248 1 249 2 250 127 251 0 252 1 253 33 254 0 255 1 256 99 257 1 258 2 259 19 260 2 261 2 262 156 263 0 264 29 265 3 266 2 267 1 268 129 269 0 270 1 271 19 272 1 273 1 274 57 275 0 276 0 277 25 278 0 279 1 280 184 281 1 282 2 283 7 284 0 285 0 286 145 287 0 288 1 289 31 290 2 291 1 292 29 293 0 294 0 295 41 296 0 297 0 298 136 299 0 300 0 301 1 302 0 303 0 304 92 305 1 306 1 307 11 308 0 309 3 310 14 311 0 312 1 313 49 314 0 315 0 316 88 317 0 318 0 319 21 320 0 321 0 322 24 323 0 324 0 325 15 326 0 327 2 328 19 329 1 330 0 331 19 332 0 333 0 334 58 335 0 336 1 337 34 338 0 339 0 340 26 341 0 342 0 343 13 344 0 345 0 346 9 347 0 348 0 349 7 350 0 351 0 352 59 353 0 354 0 355 21 356 0 357 0 358 13 359 0 360 0 361 12 362 0 363 0 364 13 365 0 366 0 367 24 368 0 369 0 370 61 371 0 372 0 373 2 374 0 375 0 376 12 377 0 378 0 379 13 380 0 381 0 382 8 383 0 384 0 385 11 386 0 387 0 388 51 389 0 390 0 391 6 392 0 393 0 394 4 395 0 396 0 397 15 398 0 399 0 400 4 401 0 402 0 403 22 404 0 405 0 406 29 407 0 408 0 409 3 410 0 411 1 412 10 413 0 414 0 415 12 416 0 417 0 418 6 419 0 420 0 421 10 422 0 423 0 424 41 425 0 426 0 427 5 428 0 429 0 430 6 431 0 432 0 433 9 434 0 435 0 436 7 437 0 438 0 439 20 440 0 441 0 442 41 443 0 444 0 445 3 446 0 447 0 448 4 449 0 450 0 451 14 452 0 453 0 454 6 455 0 456 0 457 13 458 0 459 0 460 10 461 0 462 0 463 4 464 0 465 0 466 2 467 0 468 0 469 12 470 0 471 0 472 2 473 0 474 0 475 24 476 0 477 0 478 20 479 0 480 0 481 2 482 0 483 0 484 4 485 0 486 0 487 5 488 0 489 0 490 4 491 0 492 0 493 7 494 0 495 0 496 11 497 0 498 0 499 5 500 0 501 0 502 2 503 0 504 0 505 5 506 0 507 0 508 4 509 0 510 0 511 14 512 0 513 0 514 8 515 0 516 0 517 3 518 0 519 0 520 2 521 0 522 0 523 8 524 0 525 0 526 4 527 0 528 0 529 0 530 0 531 0 532 3 533 0 534 0 535 4 536 0 537 0 538 0 539 0 540 0 541 6 542 0 543 0 544 1 545 0 546 0 547 0 548 0 549 0 550 5 551 0 552 0 553 2 554 0 555 0 556 2 557 0 558 0 559 5 560 0 561 0 562 2 563 0 564 0 565 0 566 0 567 0 568 4 569 0 570 0 571 5 572 0 573 0 574 0 575 0 576 0 577 4 578 0 579 0 580 1 581 0 582 0 583 0 584 0 585 0 586 4 587 0 588 0 589 3 590 0 591 0 592 0 593 0 594 0 595 7 596 0 597 0 598 2 599 0 600 0 601 0 602 0 603 0 604 1 605 0 606 0 607 4 608 0 609 0 610 0 611 0 612 0 613 6 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 2 623 0 624 0 625 1 626 0 627 0 628 0 629 0 630 0 631 3 632 0 633 0 634 1 635 0 636 0 637 0 638 0 639 0 640 1 641 0 642 0 643 3 644 0 645 0 646 0 647 0 648 0 649 2 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 2 659 0 660 0 661 2 662 0 663 0 664 0 665 0 666 0 667 7 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 0 679 1 680 0 681 0 682 0 683 0 684 0 685 2 686 0 687 0 688 0 689 0 690 0 691 0 692 0 693 0 694 1 695 0 696 0 697 1 698 0 699 0 700 0 701 0 702 0 703 1 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 0 714 0 715 1 716 0 717 0 718 0 719 0 720 0 721 2 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 2 734 0 735 0 736 0 737 0 738 0 739 5 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 0 749 0 750 0 751 0 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 1 770 0 771 0 772 0 773 0 774 0 775 1 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 1 788 0 789 0 790 0 791 0 792 0 793 2 794 0 795 0 796 0 797 0 798 0 799 0 800 0
57: Average symbolic conclusion length is 5991679/52769 ≈ 113.55. (Median: 79)
There are 23296 minimal D-proofs with conclusions of even symbolic length, and there are 29473 minimal D-proofs with conclusions of odd symbolic length. [23296/52769 ≈ 44.15% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 2 11 3 12 3 13 3 14 6 15 3 16 20 17 27 18 22 19 28 20 46 21 65 22 46 23 85 24 109 25 102 26 153 27 149 28 163 29 178 30 259 31 254 32 286 33 287 34 292 35 298 36 346 37 395 38 350 39 482 40 375 41 455 42 364 43 599 44 479 45 599 46 445 47 668 48 404 49 652 50 556 51 675 52 479 53 751 54 412 55 748 56 509 57 782 58 480 59 689 60 441 61 852 62 510 63 733 64 555 65 622 66 469 67 754 68 443 69 713 70 490 71 607 72 356 73 707 74 349 75 684 76 324 77 567 78 243 79 692 80 242 81 537 82 266 83 419 84 215 85 627 86 201 87 415 88 235 89 399 90 176 91 439 92 154 93 342 94 166 95 292 96 156 97 330 98 129 99 206 100 201 101 160 102 141 103 358 104 80 105 129 106 261 107 149 108 113 109 374 110 90 111 181 112 202 113 139 114 43 115 357 116 65 117 148 118 126 119 103 120 43 121 310 122 43 123 84 124 206 125 45 126 64 127 293 128 36 129 50 130 176 131 49 132 42 133 353 134 46 135 97 136 129 137 40 138 24 139 328 140 35 141 66 142 224 143 53 144 49 145 339 146 21 147 99 148 169 149 13 150 19 151 328 152 26 153 55 154 155 155 44 156 19 157 308 158 20 159 80 160 317 161 21 162 20 163 357 164 19 165 60 166 241 167 21 168 16 169 327 170 6 171 13 172 181 173 6 174 14 175 289 176 8 177 12 178 332 179 38 180 30 181 303 182 10 183 11 184 269 185 6 186 10 187 311 188 8 189 12 190 221 191 38 192 28 193 279 194 2 195 6 196 365 197 3 198 21 199 207 200 2 201 4 202 258 203 13 204 7 205 212 206 6 207 2 208 316 209 4 210 53 211 210 212 4 213 3 214 336 215 10 216 6 217 128 218 0 219 4 220 269 221 2 222 3 223 118 224 2 225 2 226 390 227 6 228 33 229 98 230 2 231 1 232 259 233 1 234 4 235 120 236 3 237 0 238 178 239 6 240 3 241 77 242 0 243 3 244 355 245 10 246 23 247 28 248 0 249 3 250 176 251 2 252 2 253 69 254 1 255 2 256 133 257 11 258 3 259 64 260 2 261 0 262 308 263 3 264 72 265 21 266 0 267 3 268 121 269 0 270 2 271 63 272 0 273 9 274 158 275 1 276 2 277 21 278 1 279 1 280 265 281 0 282 57 283 11 284 1 285 0 286 96 287 1 288 2 289 42 290 0 291 9 292 91 293 0 294 0 295 22 296 0 297 1 298 195 299 1 300 2 301 13 302 0 303 0 304 89 305 0 306 1 307 34 308 1 309 0 310 34 311 0 312 0 313 28 314 0 315 0 316 128 317 0 318 0 319 10 320 0 321 0 322 97 323 1 324 1 325 17 326 0 327 1 328 31 329 0 330 1 331 47 332 0 333 0 334 104 335 0 336 0 337 20 338 0 339 0 340 71 341 0 342 0 343 23 344 0 345 1 346 42 347 1 348 0 349 27 350 0 351 0 352 70 353 0 354 1 355 14 356 0 357 0 358 53 359 0 360 0 361 18 362 0 363 0 364 15 365 0 366 0 367 23 368 0 369 0 370 50 371 0 372 0 373 13 374 0 375 0 376 12 377 0 378 0 379 12 380 0 381 0 382 11 383 0 384 0 385 28 386 0 387 0 388 44 389 0 390 0 391 2 392 0 393 0 394 17 395 0 396 0 397 13 398 0 399 0 400 9 401 0 402 0 403 8 404 0 405 0 406 64 407 0 408 0 409 8 410 0 411 1 412 18 413 0 414 0 415 18 416 0 417 0 418 12 419 0 420 0 421 21 422 0 423 0 424 55 425 0 426 0 427 6 428 0 429 2 430 20 431 0 432 0 433 11 434 0 435 0 436 8 437 0 438 0 439 2 440 0 441 0 442 30 443 0 444 0 445 5 446 0 447 0 448 6 449 0 450 0 451 5 452 0 453 0 454 3 455 0 456 0 457 10 458 0 459 0 460 33 461 0 462 0 463 3 464 0 465 0 466 8 467 0 468 0 469 10 470 0 471 0 472 6 473 0 474 0 475 1 476 0 477 0 478 56 479 0 480 0 481 6 482 0 483 0 484 8 485 0 486 0 487 14 488 0 489 0 490 7 491 0 492 0 493 12 494 0 495 0 496 37 497 0 498 0 499 4 500 0 501 0 502 9 503 0 504 0 505 11 506 0 507 0 508 6 509 0 510 0 511 0 512 0 513 0 514 8 515 0 516 0 517 5 518 0 519 0 520 3 521 0 522 0 523 3 524 0 525 0 526 2 527 0 528 0 529 14 530 0 531 0 532 30 533 0 534 0 535 3 536 0 537 0 538 2 539 0 540 0 541 9 542 0 543 0 544 4 545 0 546 0 547 0 548 0 549 0 550 12 551 0 552 0 553 6 554 0 555 0 556 2 557 0 558 0 559 14 560 0 561 0 562 4 563 0 564 0 565 8 566 0 567 0 568 8 569 0 570 0 571 4 572 0 573 0 574 4 575 0 576 0 577 6 578 0 579 0 580 4 581 0 582 0 583 0 584 0 585 0 586 3 587 0 588 0 589 5 590 0 591 0 592 0 593 0 594 0 595 3 596 0 597 0 598 1 599 0 600 0 601 0 602 0 603 0 604 5 605 0 606 0 607 3 608 0 609 0 610 1 611 0 612 0 613 9 614 0 615 0 616 2 617 0 618 0 619 0 620 0 621 0 622 4 623 0 624 0 625 6 626 0 627 0 628 0 629 0 630 0 631 8 632 0 633 0 634 1 635 0 636 0 637 0 638 0 639 0 640 4 641 0 642 0 643 4 644 0 645 0 646 0 647 0 648 0 649 3 650 0 651 0 652 2 653 0 654 0 655 0 656 0 657 0 658 1 659 0 660 0 661 5 662 0 663 0 664 0 665 0 666 0 667 3 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 2 677 0 678 0 679 2 680 0 681 0 682 0 683 0 684 0 685 6 686 0 687 0 688 1 689 0 690 0 691 0 692 0 693 0 694 1 695 0 696 0 697 3 698 0 699 0 700 0 701 0 702 0 703 2 704 0 705 0 706 0 707 0 708 0 709 0 710 0 711 0 712 2 713 0 714 0 715 2 716 0 717 0 718 0 719 0 720 0 721 3 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 0 731 0 732 0 733 0 734 0 735 0 736 0 737 0 738 0 739 0 740 0 741 0 742 0 743 0 744 0 745 0 746 0 747 0 748 1 749 0 750 0 751 1 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 0 769 1 770 0 771 0 772 0 773 0 774 0 775 2 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 2 788 0 789 0 790 0 791 0 792 0 793 2 794 0 795 0 796 0 797 0 798 0 799 0 800 0
59: Average symbolic conclusion length is 9167435/78319 ≈ 117.05. (Median: 81)
There are 34174 minimal D-proofs with conclusions of even symbolic length, and there are 44145 minimal D-proofs with conclusions of odd symbolic length. [34174/78319 ≈ 43.63% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 4 13 2 14 12 15 16 16 9 17 22 18 30 19 33 20 45 21 83 22 97 23 78 24 144 25 129 26 169 27 151 28 227 29 232 30 288 31 276 32 305 33 295 34 426 35 393 36 379 37 490 38 421 39 542 40 571 41 616 42 541 43 704 44 613 45 735 46 680 47 805 48 733 49 831 50 773 51 920 52 749 53 981 54 783 55 1070 56 811 57 1142 58 847 59 1034 60 799 61 1167 62 807 63 1023 64 730 65 1095 66 693 67 1146 68 666 69 1016 70 538 71 1130 72 532 73 1139 74 499 75 1082 76 441 77 885 78 468 79 893 80 465 81 784 82 411 83 714 84 410 85 730 86 357 87 667 88 412 89 589 90 277 91 550 92 299 93 545 94 332 95 424 96 217 97 543 98 268 99 401 100 326 101 290 102 183 103 573 104 194 105 397 106 289 107 303 108 110 109 555 110 114 111 300 112 251 113 191 114 101 115 508 116 94 117 184 118 224 119 96 120 122 121 478 122 83 123 137 124 234 125 109 126 100 127 508 128 44 129 133 130 283 131 101 132 73 133 584 134 42 135 160 136 204 137 93 138 54 139 535 140 36 141 66 142 251 143 44 144 65 145 480 146 32 147 52 148 291 149 58 150 48 151 577 152 31 153 96 154 235 155 51 156 29 157 595 158 24 159 62 160 280 161 69 162 53 163 504 164 17 165 28 166 298 167 15 168 24 169 553 170 20 171 12 172 264 173 21 174 32 175 562 176 16 177 27 178 373 179 31 180 47 181 491 182 12 183 33 184 366 185 16 186 19 187 569 188 10 189 16 190 316 191 6 192 28 193 430 194 7 195 2 196 406 197 8 198 66 199 374 200 10 201 13 202 384 203 6 204 10 205 408 206 9 207 21 208 436 209 2 210 37 211 314 212 2 213 4 214 418 215 12 216 33 217 271 218 1 219 6 220 360 221 5 222 7 223 231 224 6 225 12 226 441 227 14 228 38 229 244 230 6 231 4 232 334 233 0 234 2 235 271 236 1 237 3 238 371 239 2 240 2 241 150 242 1 243 1 244 346 245 2 246 17 247 147 248 3 249 2 250 353 251 1 252 3 253 266 254 5 255 3 256 239 257 0 258 1 259 93 260 1 261 2 262 313 263 0 264 1 265 68 266 0 267 1 268 307 269 1 270 2 271 131 272 2 273 4 274 139 275 0 276 2 277 76 278 4 279 1 280 265 281 0 282 29 283 32 284 1 285 3 286 195 287 0 288 1 289 77 290 0 291 1 292 131 293 1 294 2 295 28 296 2 297 2 298 217 299 0 300 37 301 10 302 2 303 1 304 193 305 0 306 1 307 44 308 1 309 1 310 81 311 0 312 0 313 36 314 0 315 1 316 271 317 1 318 2 319 16 320 0 321 0 322 214 323 0 324 1 325 38 326 2 327 1 328 47 329 0 330 0 331 53 332 0 333 0 334 211 335 0 336 0 337 4 338 0 339 0 340 134 341 1 342 1 343 17 344 0 345 3 346 23 347 0 348 1 349 66 350 0 351 0 352 123 353 0 354 0 355 29 356 0 357 0 358 39 359 0 360 0 361 18 362 0 363 2 364 30 365 1 366 0 367 31 368 0 369 0 370 103 371 0 372 1 373 38 374 0 375 0 376 44 377 0 378 0 379 15 380 0 381 0 382 16 383 0 384 0 385 26 386 0 387 0 388 100 389 0 390 0 391 26 392 0 393 0 394 29 395 0 396 0 397 13 398 0 399 0 400 20 401 0 402 0 403 28 404 0 405 0 406 88 407 0 408 0 409 2 410 0 411 0 412 28 413 0 414 0 415 14 416 0 417 0 418 11 419 0 420 0 421 14 422 0 423 0 424 82 425 0 426 0 427 6 428 0 429 0 430 10 431 0 432 0 433 15 434 0 435 0 436 7 437 0 438 0 439 31 440 0 441 0 442 59 443 0 444 0 445 3 446 0 447 1 448 18 449 0 450 0 451 14 452 0 453 0 454 8 455 0 456 0 457 13 458 0 459 0 460 61 461 0 462 0 463 5 464 0 465 0 466 13 467 0 468 0 469 12 470 0 471 0 472 11 473 0 474 0 475 29 476 0 477 0 478 79 479 0 480 0 481 3 482 0 483 0 484 12 485 0 486 0 487 15 488 0 489 0 490 8 491 0 492 0 493 15 494 0 495 0 496 66 497 0 498 0 499 4 500 0 501 0 502 4 503 0 504 0 505 18 506 0 507 0 508 3 509 0 510 0 511 24 512 0 513 0 514 32 515 0 516 0 517 2 518 0 519 0 520 10 521 0 522 0 523 13 524 0 525 0 526 6 527 0 528 0 529 14 530 0 531 0 532 51 533 0 534 0 535 5 536 0 537 0 538 6 539 0 540 0 541 6 542 0 543 0 544 7 545 0 546 0 547 28 548 0 549 0 550 57 551 0 552 0 553 3 554 0 555 0 556 4 557 0 558 0 559 13 560 0 561 0 562 6 563 0 564 0 565 8 566 0 567 0 568 10 569 0 570 0 571 4 572 0 573 0 574 2 575 0 576 0 577 14 578 0 579 0 580 2 581 0 582 0 583 16 584 0 585 0 586 25 587 0 588 0 589 2 590 0 591 0 592 4 593 0 594 0 595 5 596 0 597 0 598 4 599 0 600 0 601 0 602 0 603 0 604 11 605 0 606 0 607 5 608 0 609 0 610 2 611 0 612 0 613 5 614 0 615 0 616 4 617 0 618 0 619 0 620 0 621 0 622 8 623 0 624 0 625 3 626 0 627 0 628 2 629 0 630 0 631 8 632 0 633 0 634 4 635 0 636 0 637 0 638 0 639 0 640 3 641 0 642 0 643 4 644 0 645 0 646 0 647 0 648 0 649 6 650 0 651 0 652 1 653 0 654 0 655 0 656 0 657 0 658 5 659 0 660 0 661 2 662 0 663 0 664 2 665 0 666 0 667 5 668 0 669 0 670 2 671 0 672 0 673 0 674 0 675 0 676 4 677 0 678 0 679 5 680 0 681 0 682 0 683 0 684 0 685 4 686 0 687 0 688 1 689 0 690 0 691 0 692 0 693 0 694 4 695 0 696 0 697 2 698 0 699 0 700 0 701 0 702 0 703 7 704 0 705 0 706 2 707 0 708 0 709 0 710 0 711 0 712 1 713 0 714 0 715 2 716 0 717 0 718 0 719 0 720 0 721 6 722 0 723 0 724 0 725 0 726 0 727 0 728 0 729 0 730 2 731 0 732 0 733 1 734 0 735 0 736 0 737 0 738 0 739 3 740 0 741 0 742 1 743 0 744 0 745 0 746 0 747 0 748 1 749 0 750 0 751 2 752 0 753 0 754 0 755 0 756 0 757 2 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 2 767 0 768 0 769 2 770 0 771 0 772 0 773 0 774 0 775 7 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 0 785 0 786 0 787 0 788 0 789 0 790 0 791 0 792 0 793 2 794 0 795 0 796 0 797 0 798 0 799 0 800 0
61: Average symbolic conclusion length is 13939505/116867 ≈ 119.28. (Median: 84)
There are 49814 minimal D-proofs with conclusions of even symbolic length, and there are 67053 minimal D-proofs with conclusions of odd symbolic length. [49814/116867 ≈ 42.62% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 3 13 3 14 4 15 7 16 19 17 19 18 34 19 67 20 48 21 44 22 96 23 106 24 119 25 130 26 167 27 222 28 227 29 275 30 364 31 298 32 441 33 461 34 472 35 494 36 620 37 643 38 783 39 704 40 820 41 766 42 971 43 948 44 1095 45 1009 46 1084 47 1022 48 1137 49 1170 50 1068 51 1365 52 1136 53 1260 54 1042 55 1520 56 1228 57 1474 58 1187 59 1535 60 988 61 1534 62 1205 63 1445 64 1106 65 1600 66 864 67 1537 68 1080 69 1536 70 955 71 1388 72 834 73 1659 74 1054 75 1377 76 1010 77 1137 78 876 79 1397 80 828 81 1241 82 858 83 1015 84 584 85 1175 86 561 87 1176 88 507 89 922 90 388 91 1243 92 349 93 973 94 446 95 696 96 327 97 1068 98 308 99 689 100 397 101 633 102 264 103 809 104 241 105 571 106 312 107 478 108 239 109 728 110 188 111 376 112 381 113 276 114 191 115 705 116 117 117 231 118 430 119 269 120 141 121 808 122 135 123 314 124 428 125 279 126 74 127 819 128 96 129 249 130 341 131 175 132 68 133 776 134 65 135 202 136 298 137 98 138 71 139 774 140 53 141 109 142 441 143 110 144 98 145 817 146 61 147 133 148 368 149 90 150 45 151 899 152 46 153 179 154 238 155 75 156 48 157 772 158 39 159 104 160 421 161 32 162 105 163 765 164 35 165 56 166 336 167 71 168 42 169 922 170 39 171 229 172 254 173 45 174 19 175 758 176 36 177 104 178 461 179 80 180 82 181 805 182 13 183 126 184 319 185 13 186 20 187 812 188 21 189 71 190 286 191 27 192 19 193 698 194 18 195 27 196 609 197 26 198 24 199 758 200 12 201 54 202 424 203 57 204 17 205 717 206 5 207 12 208 313 209 6 210 14 211 610 212 8 213 5 214 577 215 60 216 40 217 663 218 10 219 15 220 456 221 6 222 10 223 597 224 8 225 9 226 362 227 15 228 35 229 538 230 2 231 6 232 569 233 3 234 26 235 459 236 2 237 10 238 408 239 21 240 7 241 402 242 6 243 2 244 478 245 3 246 70 247 396 248 4 249 3 250 502 251 7 252 5 253 257 254 0 255 6 256 391 257 2 258 3 259 227 260 2 261 5 262 553 263 13 264 44 265 172 266 2 267 1 268 395 269 12 270 4 271 205 272 3 273 2 274 259 275 3 276 3 277 137 278 0 279 3 280 504 281 12 282 30 283 61 284 0 285 2 286 263 287 7 288 2 289 112 290 1 291 2 292 198 293 0 294 3 295 111 296 2 297 0 298 441 299 1 300 94 301 48 302 0 303 3 304 190 305 0 306 2 307 123 308 0 309 10 310 228 311 4 312 2 313 38 314 1 315 1 316 378 317 0 318 73 319 31 320 1 321 1 322 148 323 0 324 2 325 77 326 0 327 10 328 140 329 0 330 0 331 38 332 0 333 1 334 306 335 2 336 2 337 31 338 0 339 0 340 130 341 0 342 1 343 66 344 1 345 0 346 61 347 0 348 0 349 36 350 0 351 0 352 186 353 0 354 0 355 18 356 0 357 0 358 140 359 1 360 1 361 39 362 0 363 1 364 48 365 0 366 1 367 58 368 0 369 0 370 174 371 0 372 0 373 31 374 0 375 0 376 105 377 0 378 0 379 32 380 0 381 1 382 66 383 1 384 0 385 32 386 0 387 0 388 138 389 0 390 1 391 20 392 0 393 0 394 76 395 0 396 0 397 25 398 0 399 0 400 28 401 0 402 0 403 35 404 0 405 0 406 76 407 0 408 0 409 20 410 0 411 0 412 24 413 0 414 0 415 14 416 0 417 0 418 18 419 0 420 0 421 30 422 0 423 0 424 90 425 0 426 0 427 2 428 0 429 0 430 34 431 0 432 0 433 16 434 0 435 0 436 16 437 0 438 0 439 31 440 0 441 0 442 96 443 0 444 0 445 11 446 0 447 1 448 35 449 0 450 0 451 21 452 0 453 0 454 20 455 0 456 0 457 37 458 0 459 0 460 74 461 0 462 0 463 6 464 0 465 2 466 37 467 0 468 0 469 14 470 0 471 0 472 11 473 0 474 0 475 13 476 0 477 0 478 56 479 0 480 0 481 5 482 0 483 0 484 12 485 0 486 0 487 5 488 0 489 0 490 6 491 0 492 0 493 25 494 0 495 0 496 47 497 0 498 0 499 3 500 0 501 0 502 17 503 0 504 0 505 12 506 0 507 0 508 8 509 0 510 0 511 4 512 0 513 0 514 74 515 0 516 0 517 6 518 0 519 0 520 18 521 0 522 0 523 19 524 0 525 0 526 10 527 0 528 0 529 13 530 0 531 0 532 70 533 0 534 0 535 4 536 0 537 0 538 20 539 0 540 0 541 12 542 0 543 0 544 8 545 0 546 0 547 1 548 0 549 0 550 36 551 0 552 0 553 5 554 0 555 0 556 6 557 0 558 0 559 4 560 0 561 0 562 3 563 0 564 0 565 14 566 0 567 0 568 41 569 0 570 0 571 3 572 0 573 0 574 8 575 0 576 0 577 9 578 0 579 0 580 6 581 0 582 0 583 1 584 0 585 0 586 73 587 0 588 0 589 6 590 0 591 0 592 8 593 0 594 0 595 15 596 0 597 0 598 7 599 0 600 0 601 16 602 0 603 0 604 47 605 0 606 0 607 4 608 0 609 0 610 9 611 0 612 0 613 12 614 0 615 0 616 6 617 0 618 0 619 0 620 0 621 0 622 8 623 0 624 0 625 5 626 0 627 0 628 3 629 0 630 0 631 3 632 0 633 0 634 2 635 0 636 0 637 9 638 0 639 0 640 40 641 0 642 0 643 3 644 0 645 0 646 2 647 0 648 0 649 9 650 0 651 0 652 4 653 0 654 0 655 0 656 0 657 0 658 12 659 0 660 0 661 6 662 0 663 0 664 2 665 0 666 0 667 15 668 0 669 0 670 4 671 0 672 0 673 0 674 0 675 0 676 8 677 0 678 0 679 4 680 0 681 0 682 4 683 0 684 0 685 6 686 0 687 0 688 4 689 0 690 0 691 0 692 0 693 0 694 3 695 0 696 0 697 5 698 0 699 0 700 0 701 0 702 0 703 3 704 0 705 0 706 1 707 0 708 0 709 0 710 0 711 0 712 5 713 0 714 0 715 3 716 0 717 0 718 1 719 0 720 0 721 9 722 0 723 0 724 2 725 0 726 0 727 0 728 0 729 0 730 4 731 0 732 0 733 6 734 0 735 0 736 0 737 0 738 0 739 8 740 0 741 0 742 1 743 0 744 0 745 0 746 0 747 0 748 4 749 0 750 0 751 3 752 0 753 0 754 0 755 0 756 0 757 3 758 0 759 0 760 2 761 0 762 0 763 0 764 0 765 0 766 1 767 0 768 0 769 2 770 0 771 0 772 0 773 0 774 0 775 3 776 0 777 0 778 0 779 0 780 0 781 0 782 0 783 0 784 2 785 0 786 0 787 1 788 0 789 0 790 0 791 0 792 0 793 6 794 0 795 0 796 1 797 0 798 0 799 0 800 0
63: Average symbolic conclusion length is 21439177/174207 ≈ 123.07. (Median: 86)
There are 74472 minimal D-proofs with conclusions of even symbolic length, and there are 99735 minimal D-proofs with conclusions of odd symbolic length. [74472/174207 ≈ 42.75% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 1 12 2 13 6 14 8 15 5 16 20 17 33 18 26 19 40 20 83 21 82 22 76 23 114 24 141 25 168 26 233 27 292 28 374 29 318 30 450 31 439 32 517 33 584 34 695 35 613 36 881 37 770 38 984 39 753 40 1122 41 1010 42 1273 43 1133 44 1275 45 1186 46 1532 47 1369 48 1341 49 1630 50 1485 51 1652 52 1794 53 1774 54 1654 55 1996 56 1868 57 1846 58 1833 59 2036 60 1910 61 2006 62 1988 63 2105 64 1719 65 2169 66 1850 67 2274 68 1790 69 2377 70 1759 71 2018 72 1672 73 2230 74 1606 75 1980 76 1441 77 1997 78 1297 79 2087 80 1159 81 1816 82 968 83 1960 84 904 85 2011 86 827 87 1823 88 780 89 1491 90 755 91 1639 92 773 93 1369 94 746 95 1160 96 709 97 1250 98 568 99 1139 100 695 101 949 102 435 103 1023 104 465 105 894 106 575 107 694 108 322 109 1090 110 379 111 693 112 556 113 501 114 266 115 1028 116 313 117 677 118 519 119 480 120 167 121 1159 122 189 123 515 124 534 125 302 126 181 127 995 128 141 129 336 130 456 131 197 132 163 133 970 134 119 135 224 136 547 137 184 138 120 139 1127 140 77 141 294 142 545 143 200 144 127 145 1129 146 71 147 273 148 513 149 158 150 83 151 1229 152 54 153 174 154 441 155 88 156 67 157 1218 158 63 159 135 160 511 161 121 162 107 163 1251 164 43 165 129 166 580 167 117 168 65 169 1420 170 35 171 202 172 374 173 105 174 46 175 1316 176 37 177 80 178 518 179 46 180 93 181 1187 182 29 183 29 184 565 185 66 186 55 187 1367 188 27 189 121 190 435 191 61 192 33 193 1372 194 24 195 64 196 540 197 81 198 79 199 1143 200 16 201 31 202 556 203 15 204 26 205 1271 206 21 207 11 208 448 209 14 210 34 211 1227 212 16 213 26 214 666 215 41 216 65 217 1017 218 12 219 43 220 645 221 18 222 20 223 1161 224 11 225 18 226 488 227 6 228 31 229 848 230 7 231 5 232 663 233 8 234 92 235 769 236 10 237 21 238 643 239 16 240 8 241 754 242 9 243 23 244 664 245 3 246 43 247 576 248 2 249 4 250 636 251 14 252 45 253 533 254 1 255 11 256 546 257 4 258 6 259 436 260 6 261 10 262 662 263 3 264 47 265 459 266 6 267 4 268 509 269 0 270 2 271 476 272 1 273 4 274 536 275 1 276 2 277 319 278 1 279 1 280 484 281 2 282 23 283 284 284 3 285 2 286 540 287 1 288 3 289 438 290 5 291 7 292 349 293 0 294 1 295 206 296 1 297 5 298 425 299 0 300 1 301 163 302 0 303 1 304 466 305 1 306 2 307 242 308 2 309 4 310 195 311 0 312 2 313 144 314 4 315 1 316 364 317 0 318 37 319 85 320 1 321 2 322 304 323 0 324 1 325 179 326 0 327 2 328 176 329 1 330 2 331 66 332 2 333 2 334 302 335 0 336 46 337 38 338 2 339 1 340 291 341 0 342 1 343 114 344 1 345 1 346 114 347 0 348 0 349 78 350 0 351 1 352 364 353 1 354 2 355 41 356 0 357 1 358 320 359 0 360 1 361 121 362 2 363 1 364 69 365 0 366 0 367 73 368 0 369 0 370 287 371 0 372 0 373 26 374 0 375 0 376 209 377 1 378 1 379 55 380 0 381 3 382 39 383 0 384 1 385 83 386 0 387 0 388 209 389 0 390 0 391 47 392 0 393 0 394 70 395 0 396 0 397 26 398 0 399 2 400 49 401 1 402 0 403 48 404 0 405 0 406 149 407 0 408 1 409 47 410 0 411 0 412 70 413 0 414 0 415 28 416 0 417 0 418 27 419 0 420 0 421 52 422 0 423 0 424 179 425 0 426 0 427 35 428 0 429 0 430 60 431 0 432 0 433 18 434 0 435 0 436 35 437 0 438 0 439 50 440 0 441 0 442 174 443 0 444 0 445 6 446 0 447 0 448 53 449 0 450 0 451 19 452 0 453 0 454 18 455 0 456 0 457 51 458 0 459 0 460 110 461 0 462 0 463 12 464 0 465 0 466 23 467 0 468 0 469 19 470 0 471 0 472 12 473 0 474 0 475 35 476 0 477 0 478 114 479 0 480 0 481 3 482 0 483 1 484 35 485 0 486 0 487 16 488 0 489 0 490 13 491 0 492 0 493 16 494 0 495 0 496 111 497 0 498 0 499 8 500 0 501 0 502 29 503 0 504 0 505 13 506 0 507 0 508 16 509 0 510 0 511 43 512 0 513 0 514 102 515 0 516 0 517 3 518 0 519 0 520 28 521 0 522 0 523 16 524 0 525 0 526 10 527 0 528 0 529 25 530 0 531 0 532 102 533 0 534 0 535 4 536 0 537 0 538 10 539 0 540 0 541 18 542 0 543 0 544 5 545 0 546 0 547 34 548 0 549 0 550 67 551 0 552 0 553 2 554 0 555 0 556 18 557 0 558 0 559 15 560 0 561 0 562 8 563 0 564 0 565 14 566 0 567 0 568 68 569 0 570 0 571 5 572 0 573 0 574 13 575 0 576 0 577 9 578 0 579 0 580 10 581 0 582 0 583 31 584 0 585 0 586 107 587 0 588 0 589 3 590 0 591 0 592 12 593 0 594 0 595 14 596 0 597 0 598 8 599 0 600 0 601 20 602 0 603 0 604 90 605 0 606 0 607 4 608 0 609 0 610 4 611 0 612 0 613 21 614 0 615 0 616 3 617 0 618 0 619 32 620 0 621 0 622 37 623 0 624 0 625 2 626 0 627 0 628 10 629 0 630 0 631 15 632 0 633 0 634 6 635 0 636 0 637 9 638 0 639 0 640 66 641 0 642 0 643 5 644 0 645 0 646 6 647 0 648 0 649 6 650 0 651 0 652 7 653 0 654 0 655 18 656 0 657 0 658 77 659 0 660 0 661 3 662 0 663 0 664 4 665 0 666 0 667 14 668 0 669 0 670 6 671 0 672 0 673 0 674 0 675 0 676 10 677 0 678 0 679 4 680 0 681 0 682 2 683 0 684 0 685 16 686 0 687 0 688 2 689 0 690 0 691 0 692 0 693 0 694 31 695 0 696 0 697 2 698 0 699 0 700 4 701 0 702 0 703 5 704 0 705 0 706 4 707 0 708 0 709 0 710 0 711 0 712 11 713 0 714 0 715 5 716 0 717 0 718 2 719 0 720 0 721 5 722 0 723 0 724 4 725 0 726 0 727 0 728 0 729 0 730 8 731 0 732 0 733 3 734 0 735 0 736 2 737 0 738 0 739 8 740 0 741 0 742 4 743 0 744 0 745 0 746 0 747 0 748 3 749 0 750 0 751 4 752 0 753 0 754 0 755 0 756 0 757 6 758 0 759 0 760 1 761 0 762 0 763 0 764 0 765 0 766 5 767 0 768 0 769 1 770 0 771 0 772 2 773 0 774 0 775 5 776 0 777 0 778 2 779 0 780 0 781 0 782 0 783 0 784 4 785 0 786 0 787 3 788 0 789 0 790 0 791 0 792 0 793 4 794 0 795 0 796 1 797 0 798 0 799 0 800 0
65: Average symbolic conclusion length is 32707416/260535 ≈ 125.54. (Median: 88)
There are 110827 minimal D-proofs with conclusions of even symbolic length, and there are 149708 minimal D-proofs with conclusions of odd symbolic length. [110827/260535 ≈ 42.54% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 4 12 7 13 2 14 7 15 16 16 20 17 39 18 48 19 46 20 55 21 72 22 112 23 104 24 195 25 230 26 277 27 247 28 358 29 360 30 439 31 533 32 577 33 596 34 759 35 751 36 1044 37 855 38 1145 39 1217 40 1380 41 1244 42 1721 43 1459 44 1831 45 1789 46 1990 47 1852 48 2280 49 2182 50 2690 51 2257 52 2714 53 2371 54 3035 55 2548 56 3083 57 2649 58 2983 59 2668 60 3071 61 2791 62 2675 63 3148 64 2855 65 2902 66 2515 67 3357 68 2724 69 3078 70 2743 71 3079 72 2166 73 3153 74 2469 75 2798 76 2279 77 3036 78 1680 79 2898 80 2121 81 2862 82 1874 83 2527 84 1566 85 2976 86 2010 87 2405 88 1856 89 1951 90 1520 91 2451 92 1519 93 2027 94 1473 95 1665 96 966 97 1994 98 901 99 1955 100 924 101 1473 102 629 103 2058 104 553 105 1618 106 699 107 1133 108 495 109 1876 110 510 111 1131 112 701 113 1026 114 491 115 1540 116 384 117 1011 118 676 119 761 120 370 121 1343 122 284 123 634 124 631 125 486 126 276 127 1413 128 188 129 457 130 841 131 506 132 220 133 1561 134 223 135 582 136 762 137 452 138 120 139 1574 140 161 141 477 142 719 143 325 144 142 145 1624 146 131 147 368 148 787 149 232 150 101 151 1671 152 90 153 231 154 783 155 198 156 97 157 1821 158 93 159 297 160 908 161 221 162 94 163 1942 164 74 165 251 166 763 167 139 168 72 169 1987 170 60 171 253 172 618 173 78 174 78 175 1894 176 49 177 107 178 933 179 120 180 135 181 1944 182 59 183 186 184 732 185 98 186 43 187 2110 188 47 189 311 190 493 191 112 192 54 193 1778 194 34 195 250 196 820 197 33 198 175 199 1752 200 37 201 111 202 617 203 100 204 47 205 2043 206 30 207 329 208 481 209 52 210 19 211 1631 212 30 213 137 214 878 215 65 216 135 217 1700 218 11 219 67 220 565 221 13 222 21 223 1760 224 13 225 45 226 486 227 75 228 20 229 1438 230 17 231 23 232 1057 233 32 234 28 235 1498 236 12 237 66 238 683 239 84 240 18 241 1424 242 5 243 12 244 499 245 6 246 15 247 1189 248 8 249 5 250 920 251 31 252 52 253 1320 254 10 255 28 256 710 257 6 258 9 259 1093 260 8 261 10 262 551 263 24 264 43 265 1001 266 2 267 9 268 854 269 2 270 32 271 950 272 2 273 29 274 604 275 19 276 6 277 752 278 6 279 2 280 691 281 3 282 91 283 718 284 4 285 3 286 730 287 15 288 4 289 520 290 0 291 10 292 552 293 14 294 3 295 445 296 2 297 2 298 746 299 10 300 58 301 323 302 2 303 1 304 574 305 14 306 4 307 375 308 3 309 8 310 365 311 10 312 3 313 269 314 0 315 3 316 670 317 0 318 38 319 150 320 0 321 2 322 396 323 4 324 2 325 242 326 1 327 4 328 283 329 0 330 3 331 216 332 2 333 3 334 605 335 6 336 119 337 116 338 0 339 3 340 292 341 0 342 2 343 236 344 0 345 13 346 329 347 2 348 2 349 100 350 1 351 1 352 522 353 0 354 91 355 87 356 1 357 0 358 223 359 3 360 2 361 141 362 0 363 11 364 211 365 0 366 0 367 88 368 0 369 1 370 415 371 1 372 2 373 70 374 0 375 0 376 203 377 0 378 1 379 144 380 1 381 0 382 102 383 1 384 0 385 69 386 0 387 0 388 286 389 0 390 0 391 38 392 0 393 1 394 207 395 1 396 1 397 85 398 0 399 1 400 83 401 0 402 1 403 100 404 0 405 0 406 277 407 0 408 0 409 55 410 0 411 0 412 157 413 0 414 0 415 101 416 0 417 1 418 106 419 1 420 0 421 48 422 0 423 0 424 210 425 0 426 1 427 40 428 0 429 0 430 118 431 0 432 0 433 69 434 0 435 0 436 52 437 0 438 0 439 46 440 0 441 0 442 178 443 0 444 0 445 37 446 0 447 0 448 46 449 0 450 0 451 25 452 0 453 0 454 41 455 0 456 0 457 37 458 0 459 0 460 147 461 0 462 0 463 11 464 0 465 0 466 59 467 0 468 0 469 29 470 0 471 0 472 27 473 0 474 0 475 56 476 0 477 0 478 167 479 0 480 0 481 18 482 0 483 1 484 63 485 0 486 0 487 34 488 0 489 0 490 31 491 0 492 0 493 42 494 0 495 0 496 151 497 0 498 0 499 9 500 0 501 2 502 58 503 0 504 0 505 20 506 0 507 0 508 21 509 0 510 0 511 48 512 0 513 0 514 75 515 0 516 0 517 11 518 0 519 0 520 24 521 0 522 0 523 6 524 0 525 0 526 12 527 0 528 0 529 42 530 0 531 0 532 103 533 0 534 0 535 3 536 0 537 0 538 34 539 0 540 0 541 15 542 0 543 0 544 12 545 0 546 0 547 18 548 0 549 0 550 110 551 0 552 0 553 9 554 0 555 0 556 35 557 0 558 0 559 21 560 0 561 0 562 15 563 0 564 0 565 32 566 0 567 0 568 87 569 0 570 0 571 4 572 0 573 0 574 37 575 0 576 0 577 16 578 0 579 0 580 10 581 0 582 0 583 8 584 0 585 0 586 68 587 0 588 0 589 5 590 0 591 0 592 12 593 0 594 0 595 4 596 0 597 0 598 4 599 0 600 0 601 15 602 0 603 0 604 54 605 0 606 0 607 3 608 0 609 0 610 17 611 0 612 0 613 11 614 0 615 0 616 8 617 0 618 0 619 2 620 0 621 0 622 90 623 0 624 0 625 6 626 0 627 0 628 18 629 0 630 0 631 20 632 0 633 0 634 10 635 0 636 0 637 17 638 0 639 0 640 90 641 0 642 0 643 4 644 0 645 0 646 20 647 0 648 0 649 13 650 0 651 0 652 8 653 0 654 0 655 4 656 0 657 0 658 45 659 0 660 0 661 5 662 0 663 0 664 6 665 0 666 0 667 4 668 0 669 0 670 3 671 0 672 0 673 18 674 0 675 0 676 51 677 0 678 0 679 3 680 0 681 0 682 8 683 0 684 0 685 9 686 0 687 0 688 6 689 0 690 0 691 0 692 0 693 0 694 95 695 0 696 0 697 6 698 0 699 0 700 8 701 0 702 0 703 16 704 0 705 0 706 7 707 0 708 0 709 10 710 0 711 0 712 59 713 0 714 0 715 4 716 0 717 0 718 9 719 0 720 0 721 13 722 0 723 0 724 6 725 0 726 0 727 1 728 0 729 0 730 8 731 0 732 0 733 5 734 0 735 0 736 3 737 0 738 0 739 3 740 0 741 0 742 2 743 0 744 0 745 0 746 0 747 0 748 52 749 0 750 0 751 3 752 0 753 0 754 2 755 0 756 0 757 9 758 0 759 0 760 4 761 0 762 0 763 0 764 0 765 0 766 12 767 0 768 0 769 6 770 0 771 0 772 2 773 0 774 0 775 16 776 0 777 0 778 4 779 0 780 0 781 0 782 0 783 0 784 8 785 0 786 0 787 4 788 0 789 0 790 4 791 0 792 0 793 6 794 0 795 0 796 4 797 0 798 0 799 0 800 0
67: Average symbolic conclusion length is 50391036/389264 ≈ 129.45. (Median: 91)
There are 168296 minimal D-proofs with conclusions of even symbolic length, and there are 220968 minimal D-proofs with conclusions of odd symbolic length. [168296/389264 ≈ 43.23% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 1 11 3 12 0 13 8 14 7 15 17 16 27 17 16 18 34 19 52 20 74 21 41 22 132 23 186 24 196 25 222 26 283 27 330 28 339 29 534 30 548 31 569 32 853 33 810 34 1029 35 1021 36 1338 37 1266 38 1558 39 1563 40 2093 41 1668 42 2241 43 2042 44 2464 45 2248 46 2908 47 2358 48 3326 49 2737 50 3530 51 2655 52 3749 53 3065 54 3970 55 3355 56 3954 57 3404 58 4406 59 3664 60 3711 61 4205 62 4199 63 4030 64 4577 65 4230 66 4087 67 4547 68 4749 69 3946 70 4184 71 4364 72 4300 73 4254 74 4444 75 4188 76 3637 77 4207 78 3874 79 4327 80 3668 81 4448 82 3499 83 3619 84 3218 85 3978 86 3020 87 3523 88 2684 89 3426 90 2359 91 3714 92 2029 93 3063 94 1798 95 3275 96 1510 97 3396 98 1376 99 3016 100 1478 101 2471 102 1288 103 2848 104 1281 105 2308 106 1399 107 1889 108 1221 109 2329 110 968 111 1828 112 1337 113 1525 114 745 115 1826 116 710 117 1485 118 1070 119 1155 120 486 121 1948 122 587 123 1161 124 1078 125 852 126 420 127 2076 128 547 129 1137 130 1074 131 760 132 363 133 2069 134 326 135 995 136 1009 137 516 138 278 139 1996 140 258 141 621 142 1105 143 399 144 263 145 2208 146 191 147 450 148 1134 149 364 150 214 151 2086 152 149 153 561 154 1063 155 339 156 167 157 2523 158 128 159 480 160 1279 161 258 162 176 163 2446 164 99 165 403 166 1084 167 193 168 107 169 2320 170 98 171 280 172 1185 173 200 174 96 175 2783 176 72 177 318 178 1260 179 237 180 144 181 2673 182 67 183 309 184 1107 185 175 186 74 187 2859 188 54 189 203 190 920 191 86 192 62 193 2869 194 58 195 123 196 1104 197 134 198 147 199 2855 200 40 201 144 202 1130 203 141 204 79 205 3071 206 32 207 259 208 714 209 126 210 54 211 2876 212 37 213 62 214 982 215 51 216 136 217 2663 218 30 219 31 220 999 221 70 222 65 223 2861 224 25 225 190 226 736 227 73 228 38 229 2848 230 25 231 75 232 960 233 93 234 114 235 2345 236 17 237 48 238 940 239 15 240 28 241 2587 242 22 243 17 244 729 245 14 246 36 247 2426 248 16 249 37 250 1097 251 53 252 86 253 1950 254 12 255 58 256 1046 257 20 258 22 259 2179 260 12 261 16 262 733 263 17 264 33 265 1589 266 7 267 2 268 1018 269 9 270 123 271 1481 272 10 273 24 274 1008 275 18 276 8 277 1364 278 9 279 25 280 977 281 2 282 48 283 1043 284 2 285 4 286 930 287 2 288 59 289 1030 290 1 291 22 292 796 293 4 294 6 295 829 296 6 297 12 298 960 299 2 300 57 301 846 302 6 303 7 304 739 305 0 306 2 307 855 308 1 309 13 310 770 311 1 312 2 313 650 314 1 315 1 316 658 317 2 318 30 319 574 320 3 321 2 322 789 323 1 324 3 325 765 326 5 327 12 328 516 329 0 330 1 331 447 332 1 333 2 334 571 335 0 336 1 337 364 338 0 339 1 340 683 341 1 342 2 343 453 344 2 345 5 346 294 347 0 348 2 349 293 350 4 351 1 352 477 353 0 354 46 355 210 356 1 357 2 358 455 359 0 360 1 361 334 362 0 363 6 364 258 365 1 366 2 367 156 368 2 369 5 370 394 371 0 372 56 373 127 374 2 375 1 376 431 377 0 378 1 379 263 380 1 381 1 382 170 383 0 384 0 385 180 386 0 387 1 388 470 389 1 390 2 391 121 392 0 393 0 394 475 395 0 396 1 397 308 398 2 399 2 400 107 401 0 402 0 403 147 404 0 405 0 406 371 407 0 408 0 409 92 410 0 411 0 412 328 413 1 414 1 415 180 416 0 417 3 418 62 419 0 420 1 421 149 422 0 423 0 424 284 425 0 426 0 427 87 428 0 429 1 430 132 431 0 432 0 433 144 434 0 435 2 436 71 437 1 438 0 439 86 440 0 441 0 442 227 443 0 444 1 445 67 446 0 447 0 448 127 449 0 450 0 451 90 452 0 453 0 454 48 455 0 456 0 457 84 458 0 459 0 460 261 461 0 462 0 463 57 464 0 465 0 466 115 467 0 468 0 469 51 470 0 471 0 472 61 473 0 474 0 475 84 476 0 477 0 478 246 479 0 480 0 481 27 482 0 483 0 484 98 485 0 486 0 487 36 488 0 489 0 490 29 491 0 492 0 493 98 494 0 495 0 496 218 497 0 498 0 499 26 500 0 501 0 502 50 503 0 504 0 505 30 506 0 507 0 508 26 509 0 510 0 511 68 512 0 513 0 514 163 515 0 516 0 517 10 518 0 519 1 520 60 521 0 522 0 523 30 524 0 525 0 526 22 527 0 528 0 529 74 530 0 531 0 532 203 533 0 534 0 535 15 536 0 537 0 538 60 539 0 540 0 541 18 542 0 543 0 544 25 545 0 546 0 547 52 548 0 549 0 550 218 551 0 552 0 553 6 554 0 555 0 556 53 557 0 558 0 559 24 560 0 561 0 562 15 563 0 564 0 565 36 566 0 567 0 568 127 569 0 570 0 571 10 572 0 573 0 574 23 575 0 576 0 577 23 578 0 579 0 580 8 581 0 582 0 583 51 584 0 585 0 586 133 587 0 588 0 589 2 590 0 591 0 592 35 593 0 594 0 595 19 596 0 597 0 598 12 599 0 600 0 601 28 602 0 603 0 604 132 605 0 606 0 607 8 608 0 609 0 610 29 611 0 612 0 613 10 614 0 615 0 616 14 617 0 618 0 619 45 620 0 621 0 622 127 623 0 624 0 625 3 626 0 627 0 628 28 629 0 630 0 631 15 632 0 633 0 634 10 635 0 636 0 637 25 638 0 639 0 640 132 641 0 642 0 643 4 644 0 645 0 646 10 647 0 648 0 649 22 650 0 651 0 652 4 653 0 654 0 655 37 656 0 657 0 658 81 659 0 660 0 661 2 662 0 663 0 664 18 665 0 666 0 667 17 668 0 669 0 670 8 671 0 672 0 673 24 674 0 675 0 676 81 677 0 678 0 679 5 680 0 681 0 682 13 683 0 684 0 685 10 686 0 687 0 688 10 689 0 690 0 691 38 692 0 693 0 694 143 695 0 696 0 697 3 698 0 699 0 700 12 701 0 702 0 703 15 704 0 705 0 706 8 707 0 708 0 709 12 710 0 711 0 712 122 713 0 714 0 715 4 716 0 717 0 718 4 719 0 720 0 721 24 722 0 723 0 724 3 725 0 726 0 727 21 728 0 729 0 730 43 731 0 732 0 733 2 734 0 735 0 736 10 737 0 738 0 739 17 740 0 741 0 742 6 743 0 744 0 745 2 746 0 747 0 748 84 749 0 750 0 751 5 752 0 753 0 754 6 755 0 756 0 757 6 758 0 759 0 760 7 761 0 762 0 763 0 764 0 765 0 766 101 767 0 768 0 769 3 770 0 771 0 772 4 773 0 774 0 775 15 776 0 777 0 778 6 779 0 780 0 781 0 782 0 783 0 784 10 785 0 786 0 787 4 788 0 789 0 790 2 791 0 792 0 793 18 794 0 795 0 796 2 797 0 798 0 799 0 800 0
69: Average symbolic conclusion length is 77066721/582969 ≈ 132.20. (Median: 93)
There are 254576 minimal D-proofs with conclusions of even symbolic length, and there are 328393 minimal D-proofs with conclusions of odd symbolic length. [254576/582969 ≈ 43.67% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 1 11 1 12 3 13 5 14 15 15 11 16 24 17 36 18 56 19 36 20 77 21 123 22 128 23 216 24 209 25 264 26 318 27 422 28 483 29 524 30 775 31 678 32 978 33 960 34 1240 35 1161 36 1539 37 1528 38 1996 39 1734 40 2284 41 2041 42 2641 43 2559 44 3094 45 2827 46 3571 47 3103 48 4363 49 3566 50 4454 51 4169 52 5025 53 4145 54 5708 55 4636 56 5880 57 5197 58 6027 59 5291 60 6715 61 5653 62 7297 63 5687 64 7067 65 5814 66 7883 67 5754 68 7274 69 5840 70 6954 71 5954 72 7055 73 5895 74 5994 75 6331 76 6383 77 5906 78 5399 79 6624 80 5581 81 5828 82 5600 83 5713 84 4315 85 5934 86 4716 87 5051 88 4438 89 5353 90 3258 91 5152 92 3933 93 5035 94 3629 95 4308 96 2861 97 5117 98 3684 99 4097 100 3464 101 3266 102 2602 103 4225 104 2726 105 3255 106 2769 107 2699 108 1682 109 3376 110 1544 111 3162 112 1761 113 2391 114 1034 115 3350 116 978 117 2683 118 1550 119 1847 120 885 121 3261 122 906 123 1870 124 1504 125 1629 126 900 127 2899 128 699 129 1622 130 1460 131 1260 132 636 133 2501 134 481 135 1143 136 1567 137 898 138 473 139 2848 140 323 141 890 142 1495 143 860 144 346 145 2966 146 375 147 886 148 1680 149 766 150 297 151 2945 152 298 153 967 154 1680 155 582 156 235 157 3190 158 229 159 629 160 1563 161 428 162 169 163 3158 164 159 165 508 166 1964 167 429 168 172 169 3572 170 206 171 721 172 1770 173 398 174 124 175 3865 176 139 177 448 178 1768 179 272 180 177 181 3871 182 118 183 435 184 1831 185 214 186 110 187 4093 188 93 189 335 190 1702 191 208 192 102 193 4237 194 92 195 323 196 1969 197 251 198 123 199 4275 200 73 201 305 202 1597 203 145 204 75 205 4510 206 60 207 450 208 1285 209 76 210 90 211 4157 212 51 213 125 214 1848 215 177 216 195 217 4121 218 56 219 416 220 1396 221 115 222 47 223 4422 224 49 225 618 226 965 227 151 228 65 229 3705 230 24 231 267 232 1542 233 32 234 280 235 3665 236 30 237 151 238 1124 239 75 240 54 241 4110 242 29 243 350 244 835 245 61 246 19 247 3228 248 21 249 98 250 1550 251 139 252 213 253 3303 254 10 255 115 256 959 257 13 258 21 259 3415 260 13 261 46 262 787 263 103 264 21 265 2752 266 17 267 28 268 1695 269 39 270 34 271 2759 272 12 273 111 274 1047 275 50 276 19 277 2620 278 5 279 18 280 761 281 6 282 15 283 2215 284 8 285 16 286 1390 287 41 288 66 289 2439 290 10 291 52 292 1067 293 5 294 8 295 1961 296 8 297 11 298 824 299 23 300 51 301 1792 302 2 303 6 304 1243 305 2 306 40 307 1855 308 2 309 49 310 864 311 28 312 5 313 1371 314 6 315 2 316 967 317 16 318 115 319 1304 320 4 321 3 322 1036 323 13 324 4 325 1062 326 0 327 23 328 765 329 16 330 3 331 851 332 2 333 3 334 995 335 18 336 74 337 656 338 2 339 4 340 815 341 1 342 4 343 732 344 3 345 27 346 501 347 7 348 3 349 561 350 0 351 3 352 881 353 0 354 47 355 356 356 0 357 2 358 584 359 11 360 2 361 546 362 1 363 8 364 397 365 0 366 3 367 449 368 2 369 0 370 779 371 3 372 147 373 305 374 0 375 3 376 444 377 0 378 2 379 517 380 0 381 20 382 469 383 7 384 2 385 276 386 1 387 1 388 709 389 0 390 111 391 234 392 1 393 0 394 339 395 1 396 2 397 316 398 0 399 14 400 311 401 0 402 0 403 233 404 0 405 4 406 550 407 4 408 2 409 169 410 0 411 0 412 313 413 0 414 1 415 294 416 1 417 2 418 169 419 0 420 0 421 156 422 0 423 0 424 377 425 0 426 0 427 107 428 0 429 0 430 314 431 2 432 1 433 185 434 0 435 1 436 140 437 0 438 1 439 204 440 0 441 0 442 408 443 0 444 0 445 115 446 0 447 0 448 243 449 0 450 0 451 258 452 0 453 1 454 167 455 1 456 0 457 124 458 0 459 0 460 322 461 0 462 1 463 89 464 0 465 1 466 186 467 0 468 0 469 165 470 0 471 0 472 101 473 0 474 0 475 109 476 0 477 0 478 263 479 0 480 0 481 74 482 0 483 0 484 91 485 0 486 0 487 124 488 0 489 0 490 80 491 0 492 0 493 73 494 0 495 0 496 259 497 0 498 0 499 29 500 0 501 0 502 108 503 0 504 0 505 90 506 0 507 0 508 48 509 0 510 0 511 89 512 0 513 0 514 292 515 0 516 0 517 40 518 0 519 1 520 108 521 0 522 0 523 76 524 0 525 0 526 63 527 0 528 0 529 58 530 0 531 0 532 222 533 0 534 0 535 30 536 0 537 2 538 92 539 0 540 0 541 52 542 0 543 0 544 39 545 0 546 0 547 87 548 0 549 0 550 196 551 0 552 0 553 25 554 0 555 0 556 45 557 0 558 0 559 20 560 0 561 0 562 22 563 0 564 0 565 49 566 0 567 0 568 169 569 0 570 0 571 10 572 0 573 0 574 59 575 0 576 0 577 32 578 0 579 0 580 20 581 0 582 0 583 70 584 0 585 0 586 187 587 0 588 0 589 16 590 0 591 0 592 63 593 0 594 0 595 34 596 0 597 0 598 25 599 0 600 0 601 54 602 0 603 0 604 178 605 0 606 0 607 7 608 0 609 0 610 58 611 0 612 0 613 26 614 0 615 0 616 17 617 0 618 0 619 29 620 0 621 0 622 85 623 0 624 0 625 11 626 0 627 0 628 24 629 0 630 0 631 4 632 0 633 0 634 7 635 0 636 0 637 35 638 0 639 0 640 127 641 0 642 0 643 3 644 0 645 0 646 34 647 0 648 0 649 15 650 0 651 0 652 11 653 0 654 0 655 13 656 0 657 0 658 132 659 0 660 0 661 9 662 0 663 0 664 35 665 0 666 0 667 24 668 0 669 0 670 13 671 0 672 0 673 20 674 0 675 0 676 106 677 0 678 0 679 4 680 0 681 0 682 37 683 0 684 0 685 17 686 0 687 0 688 10 689 0 690 0 691 8 692 0 693 0 694 86 695 0 696 0 697 5 698 0 699 0 700 12 701 0 702 0 703 6 704 0 705 0 706 4 707 0 708 0 709 19 710 0 711 0 712 64 713 0 714 0 715 3 716 0 717 0 718 17 719 0 720 0 721 11 722 0 723 0 724 8 725 0 726 0 727 6 728 0 729 0 730 111 731 0 732 0 733 6 734 0 735 0 736 18 737 0 738 0 739 21 740 0 741 0 742 10 743 0 744 0 745 21 746 0 747 0 748 114 749 0 750 0 751 4 752 0 753 0 754 20 755 0 756 0 757 15 758 0 759 0 760 8 761 0 762 0 763 3 764 0 765 0 766 57 767 0 768 0 769 5 770 0 771 0 772 6 773 0 774 0 775 4 776 0 777 0 778 3 779 0 780 0 781 11 782 0 783 0 784 63 785 0 786 0 787 3 788 0 789 0 790 8 791 0 792 0 793 10 794 0 795 0 796 6 797 0 798 0 799 3 800 0
71: Average symbolic conclusion length is 118746607/872258 ≈ 136.14. (Median: 95)
There are 390355 minimal D-proofs with conclusions of even symbolic length, and there are 481903 minimal D-proofs with conclusions of odd symbolic length. [390355/872258 ≈ 44.75% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 2 10 1 11 1 12 5 13 6 14 16 15 14 16 26 17 38 18 37 19 72 20 51 21 128 22 165 23 163 24 182 25 308 26 362 27 351 28 582 29 609 30 779 31 937 32 992 33 1076 34 1335 35 1680 36 1995 37 1887 38 2371 39 2372 40 2685 41 3070 42 3620 43 3311 44 4399 45 3808 46 5073 47 4460 48 5967 49 5034 50 6231 51 5497 52 7574 53 5823 54 7746 55 6574 56 8011 57 6892 58 9117 59 6751 60 9745 61 7487 62 9927 63 7252 64 10313 65 7621 66 10155 67 8280 68 10004 69 8079 70 10650 71 8515 72 8869 73 9229 74 10134 75 8574 76 10051 77 8881 78 8895 79 9176 80 10481 81 7705 82 8642 83 8369 84 8726 85 8147 86 9010 87 7614 88 7255 89 7539 90 7514 91 7781 92 7127 93 7709 94 6574 95 6164 96 5974 97 6937 98 5556 99 6086 100 5173 101 5709 102 4195 103 6305 104 3564 105 4958 106 3594 107 5279 108 2664 109 5815 110 2373 111 4867 112 3013 113 4044 114 2327 115 4867 116 2235 117 3897 118 3117 119 3065 120 2120 121 4033 122 1710 123 2888 124 2758 125 2480 126 1340 127 3579 128 1206 129 2455 130 2349 131 2029 132 858 133 3383 134 985 135 2054 136 2393 137 1478 138 760 139 3796 140 962 141 1866 142 2380 143 1249 144 709 145 4049 146 662 147 1595 148 2564 149 932 150 578 151 3605 152 516 153 1268 154 2478 155 748 156 377 157 4102 158 354 159 912 160 2724 161 670 162 352 163 4395 164 350 165 917 166 2743 167 643 168 423 169 4700 170 269 171 1056 172 2562 173 450 174 258 175 4826 176 179 177 684 178 2891 179 377 180 229 181 5232 182 153 183 515 184 2908 185 397 186 223 187 5041 188 146 189 823 190 2512 191 368 192 152 193 5766 194 127 195 589 196 3020 197 286 198 185 199 5717 200 98 201 454 202 2563 203 213 204 100 205 5312 206 101 207 343 208 2543 209 214 210 105 211 6186 212 72 213 336 214 2860 215 278 216 199 217 5771 218 56 219 332 220 2313 221 197 222 84 223 6022 224 55 225 272 226 1938 227 92 228 72 229 6101 230 60 231 103 232 2215 233 161 234 204 235 5925 236 38 237 136 238 2067 239 170 240 97 241 6009 242 33 243 422 244 1320 245 141 246 65 247 5719 248 37 249 86 250 1755 251 58 252 189 253 5372 254 32 255 51 256 1689 257 73 258 77 259 5418 260 25 261 323 262 1180 263 87 264 44 265 5423 266 27 267 78 268 1622 269 116 270 159 271 4493 272 18 273 64 274 1516 275 15 276 30 277 4821 278 23 279 13 280 1118 281 14 282 39 283 4497 284 16 285 32 286 1728 287 79 288 111 289 3593 290 12 291 83 292 1619 293 23 294 24 295 3914 296 13 297 20 298 1044 299 19 300 37 301 2885 302 7 303 6 304 1516 305 8 306 158 307 2721 308 10 309 38 310 1506 311 5 312 8 313 2424 314 9 315 34 316 1384 317 2 318 54 319 1882 320 2 321 16 322 1334 323 1 324 75 325 1947 326 1 327 37 328 1120 329 4 330 6 331 1561 332 6 333 12 334 1345 335 2 336 68 337 1585 338 6 339 4 340 1049 341 0 342 2 343 1540 344 1 345 15 346 1095 347 1 348 2 349 1300 350 1 351 1 352 903 353 2 354 38 355 1128 356 3 357 2 358 1118 359 1 360 3 361 1397 362 5 363 23 364 752 365 0 366 1 367 936 368 1 369 3 370 747 371 0 372 1 373 779 374 0 375 4 376 977 377 1 378 2 379 917 380 2 381 14 382 460 383 0 384 2 385 601 386 4 387 1 388 647 389 0 390 56 391 513 392 1 393 2 394 654 395 0 396 1 397 657 398 0 399 11 400 400 401 1 402 2 403 378 404 2 405 2 406 552 407 0 408 67 409 349 410 2 411 1 412 620 413 0 414 1 415 564 416 1 417 2 418 280 419 0 420 0 421 390 422 0 423 1 424 583 425 1 426 2 427 339 428 0 429 0 430 693 431 0 432 1 433 611 434 2 435 6 436 195 437 0 438 0 439 324 440 0 441 3 442 506 443 0 444 0 445 254 446 0 447 0 448 497 449 1 450 1 451 430 452 0 453 3 454 113 455 0 456 1 457 302 458 0 459 0 460 389 461 0 462 0 463 191 464 0 465 0 466 243 467 0 468 0 469 456 470 0 471 3 472 109 473 1 474 0 475 193 476 0 477 0 478 292 479 0 480 1 481 144 482 0 483 0 484 226 485 0 486 0 487 298 488 0 489 0 490 82 491 0 492 0 493 223 494 0 495 0 496 363 497 0 498 0 499 126 500 0 501 1 502 205 503 0 504 0 505 273 506 0 507 0 508 93 509 0 510 0 511 157 512 0 513 0 514 323 515 0 516 0 517 82 518 0 519 0 520 187 521 0 522 0 523 148 524 0 525 0 526 49 527 0 528 0 529 147 530 0 531 0 532 290 533 0 534 0 535 63 536 0 537 0 538 98 539 0 540 0 541 68 542 0 543 0 544 51 545 0 546 0 547 142 548 0 549 0 550 260 551 0 552 0 553 26 554 0 555 1 556 103 557 0 558 0 559 68 560 0 561 0 562 37 563 0 564 0 565 164 566 0 567 0 568 297 569 0 570 0 571 33 572 0 573 0 574 114 575 0 576 0 577 60 578 0 579 0 580 46 581 0 582 0 583 105 584 0 585 0 586 295 587 0 588 0 589 29 590 0 591 0 592 98 593 0 594 0 595 46 596 0 597 0 598 24 599 0 600 0 601 121 602 0 603 0 604 268 605 0 606 0 607 24 608 0 609 0 610 50 611 0 612 0 613 39 614 0 615 0 616 15 617 0 618 0 619 66 620 0 621 0 622 190 623 0 624 0 625 9 626 0 627 0 628 60 629 0 630 0 631 45 632 0 633 0 634 19 635 0 636 0 637 50 638 0 639 0 640 242 641 0 642 0 643 15 644 0 645 0 646 60 647 0 648 0 649 14 650 0 651 0 652 21 653 0 654 0 655 70 656 0 657 0 658 279 659 0 660 0 661 6 662 0 663 0 664 53 665 0 666 0 667 27 668 0 669 0 670 14 671 0 672 0 673 51 674 0 675 0 676 155 677 0 678 0 679 10 680 0 681 0 682 23 683 0 684 0 685 30 686 0 687 0 688 6 689 0 690 0 691 53 692 0 693 0 694 162 695 0 696 0 697 2 698 0 699 0 700 35 701 0 702 0 703 20 704 0 705 0 706 12 707 0 708 0 709 31 710 0 711 0 712 162 713 0 714 0 715 8 716 0 717 0 718 29 719 0 720 0 721 14 722 0 723 0 724 13 725 0 726 0 727 48 728 0 729 0 730 162 731 0 732 0 733 3 734 0 735 0 736 28 737 0 738 0 739 16 740 0 741 0 742 10 743 0 744 0 745 37 746 0 747 0 748 173 749 0 750 0 751 4 752 0 753 0 754 10 755 0 756 0 757 26 758 0 759 0 760 4 761 0 762 0 763 44 764 0 765 0 766 99 767 0 768 0 769 2 770 0 771 0 772 18 773 0 774 0 775 22 776 0 777 0 778 8 779 0 780 0 781 15 782 0 783 0 784 99 785 0 786 0 787 5 788 0 789 0 790 13 791 0 792 0 793 10 794 0 795 0 796 10 797 0 798 0 799 27 800 0
73: Average symbolic conclusion length is 181901765/1307863 ≈ 139.08. (Median: 98)
There are 595876 minimal D-proofs with conclusions of even symbolic length, and there are 711987 minimal D-proofs with conclusions of odd symbolic length. [595876/1307863 ≈ 45.56% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 2 9 0 10 1 11 1 12 9 13 5 14 4 15 21 16 16 17 33 18 24 19 66 20 116 21 99 22 141 23 224 24 262 25 294 26 472 27 547 28 597 29 928 30 865 31 1107 32 1267 33 1595 34 1840 35 2127 36 2260 37 2470 38 2896 39 3266 40 3623 41 3605 42 4747 43 3998 44 5513 45 5043 46 6429 47 5491 48 7187 49 6394 50 8326 51 7183 52 9114 53 7722 54 9838 55 9101 56 11092 57 9246 58 11893 59 9634 60 13334 61 10726 62 13567 63 11307 64 14000 65 11361 66 15221 67 11868 68 15485 69 12625 70 14994 71 12611 72 16647 73 12687 74 16868 75 12367 76 15839 77 12342 78 17691 79 11704 80 15553 81 11531 82 14715 83 11860 84 14586 85 11438 86 12292 87 11708 88 12942 89 11109 90 10680 91 12184 92 10819 93 10286 94 10811 95 10073 96 8250 97 10524 98 8686 99 8715 100 8471 101 9064 102 6179 103 8874 104 7027 105 8478 106 6919 107 7165 108 5185 109 8682 110 6625 111 6770 112 6641 113 5369 114 4595 115 7095 116 4878 117 5315 118 5265 119 4445 120 2972 121 5851 122 2777 123 5064 124 3747 125 3885 126 1903 127 5756 128 1875 129 4440 130 3638 131 3046 132 1759 133 5412 134 1727 135 3173 136 3734 137 2696 138 1688 139 5231 140 1423 141 2565 142 3736 143 2080 144 1207 145 4869 146 945 147 2005 148 3783 149 1640 150 934 151 4925 152 634 153 1821 154 4045 155 1472 156 687 157 5809 158 737 159 1571 160 3961 161 1313 162 667 163 5936 164 599 165 1496 166 4156 167 1060 168 520 169 5554 170 406 171 1140 172 4391 173 806 174 290 175 6301 176 306 177 1034 178 4173 179 772 180 262 181 6641 182 386 183 925 184 4529 185 716 186 326 187 6937 188 270 189 1293 190 4501 191 518 192 254 193 7687 194 240 195 794 196 4175 197 440 198 206 199 7475 200 176 201 467 202 4794 203 460 204 205 205 8193 206 197 207 1110 208 4216 209 417 210 126 211 8640 212 137 213 547 214 4124 215 287 216 227 217 8350 218 130 219 490 220 3984 221 236 222 121 223 8860 224 110 225 526 226 3566 227 224 228 105 229 8905 230 98 231 458 232 4056 233 286 234 174 235 8573 236 76 237 427 238 3166 239 209 240 82 241 9151 242 60 243 941 244 2586 245 84 246 109 247 8365 248 54 249 195 250 3468 251 232 252 286 253 8087 254 44 255 453 256 2623 257 131 258 56 259 8508 260 42 261 1027 262 1830 263 123 264 82 265 7165 266 24 267 136 268 2816 269 36 270 424 271 7072 272 20 273 161 274 2004 275 163 276 62 277 7605 278 27 279 592 280 1457 281 69 282 18 283 6022 284 21 285 107 286 2596 287 181 288 316 289 6122 290 12 291 203 292 1575 293 14 294 22 295 6186 296 13 297 69 298 1241 299 60 300 22 301 5023 302 18 303 30 304 2604 305 47 306 40 307 4869 308 12 309 180 310 1578 311 63 312 21 313 4631 314 5 315 14 316 1124 317 5 318 15 319 4011 320 8 321 8 322 2045 323 41 324 82 325 4298 326 10 327 99 328 1577 329 5 330 8 331 3434 332 8 333 13 334 1207 335 33 336 60 337 3160 338 2 339 11 340 1770 341 16 342 49 343 3405 344 2 345 94 346 1233 347 27 348 5 349 2437 350 6 351 8 352 1325 353 18 354 142 355 2336 356 4 357 14 358 1442 359 22 360 4 361 2065 362 0 363 47 364 1067 365 2 366 3 367 1592 368 2 369 4 370 1299 371 16 372 92 373 1313 374 2 375 1 376 1143 377 1 378 4 379 1515 380 3 381 47 382 690 383 15 384 3 385 1162 386 0 387 3 388 1150 389 0 390 57 391 866 392 0 393 2 394 851 395 8 396 2 397 1177 398 1 399 21 400 569 401 0 402 3 403 957 404 2 405 1 406 1029 407 10 408 178 409 749 410 0 411 6 412 666 413 0 414 2 415 1132 416 0 417 40 418 652 419 4 420 2 421 679 422 1 423 1 424 919 425 0 426 133 427 588 428 1 429 0 430 525 431 6 432 2 433 750 434 0 435 19 436 452 437 0 438 0 439 536 440 0 441 1 442 744 443 2 444 2 445 435 446 0 447 0 448 470 449 0 450 1 451 587 452 1 453 8 454 272 455 3 456 0 457 398 458 0 459 0 460 527 461 0 462 0 463 290 464 0 465 0 466 463 467 1 468 1 469 538 470 0 471 3 472 223 473 0 474 1 475 432 476 0 477 3 478 512 479 1 480 0 481 296 482 0 483 0 484 385 485 0 486 0 487 594 488 0 489 3 490 269 491 1 492 0 493 322 494 0 495 0 496 499 497 0 498 1 499 224 500 0 501 0 502 292 503 0 504 0 505 333 506 0 507 0 508 185 509 0 510 0 511 296 512 0 513 0 514 392 515 0 516 0 517 169 518 0 519 0 520 174 521 0 522 0 523 402 524 0 525 0 526 138 527 0 528 0 529 164 530 0 531 0 532 338 533 0 534 0 535 92 536 0 537 1 538 202 539 0 540 0 541 234 542 0 543 0 544 96 545 0 546 0 547 220 548 0 549 0 550 461 551 0 552 0 553 101 554 0 555 1 556 177 557 0 558 0 559 278 560 0 561 0 562 118 563 0 564 0 565 152 566 0 567 0 568 355 569 0 570 0 571 77 572 0 573 2 574 154 575 0 576 0 577 171 578 0 579 0 580 72 581 0 582 0 583 141 584 0 585 0 586 280 587 0 588 0 589 61 590 0 591 0 592 90 593 0 594 0 595 70 596 0 597 0 598 53 599 0 600 0 601 90 602 0 603 0 604 306 605 0 606 0 607 32 608 0 609 0 610 101 611 0 612 0 613 87 614 0 615 0 616 34 617 0 618 0 619 146 620 0 621 0 622 346 623 0 624 0 625 36 626 0 627 0 628 107 629 0 630 0 631 79 632 0 633 0 634 42 635 0 636 0 637 70 638 0 639 0 640 249 641 0 642 0 643 28 644 0 645 0 646 92 647 0 648 0 649 66 650 0 651 0 652 32 653 0 654 0 655 99 656 0 657 0 658 231 659 0 660 0 661 25 662 0 663 0 664 45 665 0 666 0 667 24 668 0 669 0 670 16 671 0 672 0 673 61 674 0 675 0 676 208 677 0 678 0 679 10 680 0 681 0 682 59 683 0 684 0 685 43 686 0 687 0 688 16 689 0 690 0 691 46 692 0 693 0 694 222 695 0 696 0 697 18 698 0 699 0 700 63 701 0 702 0 703 44 704 0 705 0 706 20 707 0 708 0 709 45 710 0 711 0 712 217 713 0 714 0 715 7 716 0 717 0 718 58 719 0 720 0 721 36 722 0 723 0 724 16 725 0 726 0 727 26 728 0 729 0 730 101 731 0 732 0 733 13 734 0 735 0 736 24 737 0 738 0 739 12 740 0 741 0 742 5 743 0 744 0 745 21 746 0 747 0 748 159 749 0 750 0 751 3 752 0 753 0 754 34 755 0 756 0 757 14 758 0 759 0 760 11 761 0 762 0 763 14 764 0 765 0 766 162 767 0 768 0 769 9 770 0 771 0 772 35 773 0 774 0 775 28 776 0 777 0 778 13 779 0 780 0 781 24 782 0 783 0 784 130 785 0 786 0 787 4 788 0 789 0 790 37 791 0 792 0 793 23 794 0 795 0 796 10 797 0 798 0 799 14 800 0
75: Average symbolic conclusion length is 280184638/1959086 ≈ 143.02. (Median: 100)
There are 916400 minimal D-proofs with conclusions of even symbolic length, and there are 1042686 minimal D-proofs with conclusions of odd symbolic length. [916400/1959086 ≈ 46.78% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 1 11 1 12 1 13 6 14 9 15 25 16 14 17 29 18 62 19 52 20 95 21 124 22 145 23 223 24 362 25 385 26 394 27 658 28 702 29 919 30 953 31 1236 32 1501 33 1731 34 1965 35 2397 36 2455 37 3242 38 3376 39 3633 40 4261 41 4533 42 5700 43 5944 44 6362 45 6591 46 7593 47 8127 48 9641 49 9202 50 10784 51 10255 52 11637 53 11876 54 14219 55 12131 56 15808 57 13075 58 16903 59 14515 60 19079 61 15166 62 18764 63 15943 64 21442 65 16215 66 21552 67 17008 68 21225 69 17427 70 23732 71 16443 72 23933 73 17664 74 23713 75 16682 76 24273 77 16827 78 22966 79 18214 80 22426 81 17068 82 22866 83 17736 84 19043 85 18318 86 21564 87 16844 88 20281 89 16954 90 17789 91 17150 92 20897 93 14163 94 16765 95 15036 96 16691 97 14724 98 17275 99 13178 100 13742 101 12903 102 13921 103 13349 104 13271 105 12863 106 12250 107 10276 108 10888 109 11856 110 10141 111 10082 112 9513 113 9335 114 7580 115 10742 116 6402 117 7984 118 7127 119 8388 120 4956 121 9943 122 4235 123 7812 124 6725 125 6568 126 4308 127 8649 128 4097 129 6227 130 6553 131 4971 132 3885 133 7180 134 3227 135 4771 136 6488 137 4158 138 2553 139 6576 140 2205 141 4124 142 5985 143 3431 144 1650 145 6582 146 1761 147 3426 148 5785 149 2671 150 1635 151 6641 152 1784 153 3317 154 6485 155 2218 156 1478 157 7203 158 1436 159 2685 160 6385 161 1644 162 1110 163 7236 164 1032 165 2131 166 6544 167 1501 168 769 169 6829 170 722 171 1867 172 6886 173 1244 174 658 175 8262 176 869 177 1792 178 6659 179 1096 180 736 181 9134 182 618 183 1591 184 7259 185 895 186 646 187 8523 188 446 189 1395 190 6995 191 809 192 325 193 9763 194 328 195 1071 196 7316 197 688 198 353 199 10128 200 298 201 1075 202 7179 203 653 204 514 205 10756 206 261 207 1435 208 6594 209 482 210 240 211 11057 212 188 213 982 214 7069 215 394 216 257 217 11439 218 168 219 637 220 6852 221 449 222 291 223 11138 224 145 225 1084 226 5798 227 418 228 160 229 12132 230 119 231 684 232 6887 233 318 234 239 235 11882 236 102 237 488 238 5621 239 239 240 113 241 11068 242 100 243 449 244 5290 245 234 246 118 247 12558 248 76 249 430 250 6127 251 335 252 285 253 11385 254 53 255 373 256 4609 257 228 258 94 259 11611 260 58 261 364 262 3919 263 98 264 78 265 11852 266 71 267 151 268 4285 269 183 270 280 271 11215 272 38 273 192 274 3731 275 208 276 117 277 10951 278 40 279 653 280 2424 281 156 282 80 283 10621 284 39 285 108 286 3036 287 64 288 259 289 10055 290 33 291 62 292 2835 293 89 294 93 295 9654 296 25 297 483 298 1943 299 104 300 54 301 9800 302 27 303 98 304 2613 305 142 306 216 307 8242 308 19 309 105 310 2432 311 28 312 30 313 8479 314 24 315 21 316 1722 317 15 318 42 319 8009 320 16 321 43 322 2689 323 97 324 140 325 6343 326 13 327 132 328 2460 329 24 330 25 331 6740 332 14 333 41 334 1523 335 5 336 41 337 5173 338 8 339 3 340 2221 341 8 342 199 343 4931 344 10 345 59 346 2210 347 4 348 9 349 4282 350 9 351 31 352 1932 353 2 354 60 355 3405 356 2 357 9 358 1902 359 1 360 94 361 3630 362 1 363 62 364 1569 365 4 366 6 367 2895 368 6 369 16 370 1810 371 2 372 80 373 2939 374 6 375 8 376 1496 377 0 378 2 379 2811 380 1 381 30 382 1531 383 1 384 2 385 2515 386 1 387 8 388 1214 389 2 390 47 391 2195 392 3 393 13 394 1575 395 1 396 3 397 2561 398 5 399 38 400 1091 401 0 402 1 403 1915 404 1 405 2 406 970 407 0 408 1 409 1611 410 0 411 1 412 1385 413 1 414 2 415 1805 416 2 417 16 418 728 419 0 420 2 421 1227 422 4 423 1 424 830 425 0 426 67 427 1143 428 1 429 2 430 939 431 0 432 1 433 1442 434 0 435 22 436 614 437 1 438 2 439 893 440 2 441 3 442 758 443 0 444 79 445 877 446 2 447 4 448 882 449 0 450 1 451 1136 452 1 453 11 454 489 455 0 456 0 457 871 458 0 459 1 460 785 461 1 462 2 463 817 464 0 465 0 466 978 467 0 468 1 469 1224 470 2 471 11 472 361 473 0 474 0 475 707 476 0 477 0 478 641 479 0 480 0 481 627 482 0 483 0 484 746 485 1 486 1 487 998 488 0 489 4 490 221 491 0 492 1 493 587 494 0 495 0 496 574 497 0 498 0 499 465 500 0 501 0 502 410 503 0 504 0 505 817 506 0 507 7 508 203 509 1 510 0 511 451 512 0 513 3 514 485 515 0 516 1 517 354 518 0 519 0 520 367 521 0 522 0 523 783 524 0 525 0 526 155 527 0 528 0 529 488 530 0 531 0 532 452 533 0 534 0 535 345 536 0 537 0 538 365 539 0 540 0 541 884 542 0 543 1 544 151 545 0 546 0 547 369 548 0 549 0 550 492 551 0 552 0 553 237 554 0 555 0 556 328 557 0 558 0 559 482 560 0 561 0 562 85 563 0 564 0 565 350 566 0 567 0 568 443 569 0 570 0 571 160 572 0 573 1 574 184 575 0 576 0 577 476 578 0 579 0 580 80 581 0 582 0 583 246 584 0 585 0 586 322 587 0 588 0 589 89 590 0 591 1 592 190 593 0 594 0 595 246 596 0 597 0 598 68 599 0 600 0 601 298 602 0 603 0 604 420 605 0 606 0 607 99 608 0 609 0 610 192 611 0 612 0 613 185 614 0 615 0 616 82 617 0 618 0 619 231 620 0 621 0 622 377 623 0 624 0 625 85 626 0 627 0 628 173 629 0 630 0 631 155 632 0 633 0 634 37 635 0 636 0 637 256 638 0 639 0 640 340 641 0 642 0 643 57 644 0 645 0 646 96 647 0 648 0 649 87 650 0 651 0 652 34 653 0 654 0 655 172 656 0 657 0 658 312 659 0 660 0 661 29 662 0 663 0 664 103 665 0 666 0 667 109 668 0 669 0 670 32 671 0 672 0 673 186 674 0 675 0 676 353 677 0 678 0 679 34 680 0 681 0 682 115 683 0 684 0 685 64 686 0 687 0 688 34 689 0 690 0 691 100 692 0 693 0 694 365 695 0 696 0 697 30 698 0 699 0 700 98 701 0 702 0 703 52 704 0 705 0 706 21 707 0 708 0 709 90 710 0 711 0 712 339 713 0 714 0 715 28 716 0 717 0 718 50 719 0 720 0 721 57 722 0 723 0 724 11 725 0 726 0 727 86 728 0 729 0 730 227 731 0 732 0 733 10 734 0 735 0 736 60 737 0 738 0 739 59 740 0 741 0 742 18 743 0 744 0 745 70 746 0 747 0 748 294 749 0 750 0 751 19 752 0 753 0 754 60 755 0 756 0 757 23 758 0 759 0 760 19 761 0 762 0 763 72 764 0 765 0 766 359 767 0 768 0 769 6 770 0 771 0 772 53 773 0 774 0 775 34 776 0 777 0 778 14 779 0 780 0 781 56 782 0 783 0 784 193 785 0 786 0 787 10 788 0 789 0 790 23 791 0 792 0 793 42 794 0 795 0 796 5 797 0 798 0 799 57 800 0
77: Average symbolic conclusion length is 429475009/2940441 ≈ 146.06. (Median: 102)
There are 1401718 minimal D-proofs with conclusions of even symbolic length, and there are 1538723 minimal D-proofs with conclusions of odd symbolic length. [1401718/2940441 ≈ 47.67% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 1 8 0 9 0 10 0 11 2 12 4 13 3 14 6 15 18 16 16 17 23 18 59 19 75 20 65 21 133 22 237 23 205 24 285 25 463 26 555 27 593 28 768 29 990 30 1204 31 1503 32 1921 33 2407 34 2251 35 3352 36 3247 37 3904 38 4449 39 5046 40 5625 41 7001 42 6608 43 7910 44 8176 45 9507 46 10347 47 11315 48 11752 49 12176 50 13894 51 14298 52 15836 53 14741 54 18954 55 15878 56 20167 57 18561 58 22611 59 18856 60 24125 61 21232 62 25947 63 22452 64 27873 65 22627 66 28430 67 25701 68 31345 69 24657 70 31602 71 25316 72 33757 73 26712 74 34388 75 26713 76 33091 77 26955 78 35161 79 26787 80 35267 81 27226 82 32936 83 26583 84 36121 85 25797 86 35285 87 24354 88 32448 89 23974 90 35843 91 22247 92 30770 93 21229 94 28866 95 21964 96 28324 97 21085 98 23832 99 20521 100 24833 101 19864 102 20111 103 21357 104 20222 105 17540 106 20250 107 17230 108 15428 109 18343 110 15575 111 14653 112 15701 113 14966 114 11641 115 15276 116 12473 117 13799 118 13639 119 11762 120 9449 121 14688 122 11813 123 11060 124 12650 125 8943 126 8170 127 12427 128 8843 129 8598 130 10380 131 7448 132 5619 133 10338 134 5221 135 8176 136 8761 137 6380 138 3855 139 10204 140 3643 141 7487 142 8246 143 5123 144 3406 145 9887 146 3536 147 5256 148 9140 149 4522 150 3388 151 9171 152 3014 153 4262 154 9205 155 3598 156 2452 157 9179 158 1936 159 3569 160 9186 161 2922 162 1756 163 9218 164 1449 165 3218 166 10208 167 2568 168 1666 169 10032 170 1530 171 2879 172 10405 173 2304 174 1599 175 11407 176 1305 177 2764 178 10749 179 1834 180 1104 181 10890 182 879 183 2052 184 11334 185 1611 186 857 187 10812 188 625 189 1998 190 11589 191 1361 192 613 193 12904 194 763 195 1622 196 11316 197 1221 198 641 199 13028 200 614 201 1868 202 11595 203 1044 204 594 205 12787 206 481 207 1466 208 11966 209 848 210 333 211 14593 212 302 213 1392 214 11341 215 807 216 290 217 14920 218 405 219 1201 220 11408 221 794 222 384 223 15231 224 284 225 1628 226 11307 227 531 228 282 229 16782 230 230 231 1029 232 10228 233 459 234 254 235 15936 236 213 237 591 238 10764 239 513 240 243 241 16894 242 232 243 1680 244 9407 245 448 246 132 247 17452 248 150 249 666 250 9053 251 313 252 299 253 16549 254 155 255 655 256 8224 257 280 258 151 259 17494 260 131 261 902 262 7180 263 319 264 122 265 17156 266 98 267 857 268 7985 269 344 270 256 271 16021 272 80 273 589 274 6119 275 260 276 105 277 17181 278 47 279 1323 280 5028 281 79 282 132 283 15637 284 44 285 262 286 6384 287 209 288 404 289 14724 290 45 291 343 292 4855 293 159 294 62 295 15286 296 37 297 1601 298 3487 299 237 300 95 301 13052 302 26 303 194 304 5009 305 34 306 612 307 12898 308 22 309 254 310 3546 311 205 312 70 313 13279 314 34 315 931 316 2656 317 82 318 20 319 10727 320 21 321 126 322 4279 323 141 324 454 325 10859 326 11 327 318 328 2625 329 15 330 24 331 10679 332 14 333 71 334 2011 335 71 336 27 337 8936 338 18 339 43 340 3980 341 56 342 47 343 8371 344 12 345 292 346 2401 347 66 348 21 349 7967 350 5 351 24 352 1746 353 5 354 16 355 7148 356 8 357 14 358 3001 359 53 360 98 361 7500 362 11 363 187 364 2357 365 20 366 8 367 5956 368 8 369 29 370 1774 371 33 372 71 373 5538 374 3 375 12 376 2597 377 18 378 59 379 6039 380 2 381 162 382 1798 383 37 384 6 385 4280 386 6 387 4 388 1837 389 3 390 172 391 4206 392 4 393 6 394 2026 395 21 396 5 397 3952 398 0 399 94 400 1529 401 2 402 3 403 2964 404 2 405 6 406 1732 407 25 408 112 409 2613 410 2 411 6 412 1590 413 1 414 4 415 2993 416 3 417 92 418 1003 419 13 420 3 421 2263 422 0 423 9 424 1461 425 0 426 68 427 1917 428 0 429 13 430 1232 431 16 432 2 433 2424 434 1 435 45 436 849 437 0 438 3 439 1955 440 2 441 2 442 1357 443 7 444 212 445 1663 446 0 447 3 448 1009 449 0 450 2 451 2389 452 0 453 61 454 924 455 11 456 2 457 1527 458 1 459 1 460 1224 461 0 462 157 463 1361 464 1 465 0 466 801 467 3 468 2 469 1665 470 0 471 33 472 679 473 0 474 0 475 1125 476 0 477 2 478 934 479 7 480 2 481 1046 482 0 483 3 484 690 485 0 486 1 487 1347 488 1 489 27 490 417 491 1 492 0 493 951 494 0 495 0 496 729 497 0 498 0 499 765 500 0 501 0 502 691 503 4 504 1 505 1162 506 0 507 7 508 349 509 0 510 1 511 960 512 0 513 0 514 723 515 0 516 0 517 709 518 0 519 0 520 596 521 0 522 0 523 1300 524 0 525 9 526 424 527 2 528 0 529 769 530 0 531 0 532 641 533 0 534 1 535 578 536 0 537 0 538 462 539 0 540 0 541 881 542 0 543 2 544 316 545 0 546 0 547 640 548 0 549 3 550 608 551 0 552 0 553 442 554 0 555 0 556 309 557 0 558 0 559 764 560 0 561 2 562 238 563 0 564 0 565 433 566 0 567 0 568 522 569 0 570 0 571 266 572 0 573 0 574 333 575 0 576 0 577 728 578 0 579 0 580 177 581 0 582 0 583 501 584 0 585 0 586 556 587 0 588 0 589 289 590 0 591 1 592 307 593 0 594 0 595 834 596 0 597 0 598 206 599 0 600 0 601 386 602 0 603 0 604 603 605 0 606 0 607 209 608 0 609 3 610 261 611 0 612 0 613 402 614 0 615 0 616 147 617 0 618 0 619 385 620 0 621 0 622 447 623 0 624 0 625 164 626 0 627 0 628 163 629 0 630 0 631 462 632 0 633 0 634 105 635 0 636 0 637 188 638 0 639 0 640 380 641 0 642 0 643 101 644 0 645 0 646 191 647 0 648 0 649 252 650 0 651 0 652 63 653 0 654 0 655 277 656 0 657 0 658 573 659 0 660 0 661 98 662 0 663 0 664 174 665 0 666 0 667 235 668 0 669 0 670 87 671 0 672 0 673 186 674 0 675 0 676 413 677 0 678 0 679 84 680 0 681 0 682 147 683 0 684 0 685 193 686 0 687 0 688 57 689 0 690 0 691 213 692 0 693 0 694 315 695 0 696 0 697 59 698 0 699 0 700 91 701 0 702 0 703 75 704 0 705 0 706 30 707 0 708 0 709 108 710 0 711 0 712 377 713 0 714 0 715 32 716 0 717 0 718 101 719 0 720 0 721 140 722 0 723 0 724 27 725 0 726 0 727 159 728 0 729 0 730 427 731 0 732 0 733 42 734 0 735 0 736 107 737 0 738 0 739 111 740 0 741 0 742 36 743 0 744 0 745 82 746 0 747 0 748 290 749 0 750 0 751 28 752 0 753 0 754 92 755 0 756 0 757 88 758 0 759 0 760 28 761 0 762 0 763 71 764 0 765 0 766 281 767 0 768 0 769 33 770 0 771 0 772 45 773 0 774 0 775 61 776 0 777 0 778 11 779 0 780 0 781 50 782 0 783 0 784 262 785 0 786 0 787 10 788 0 789 0 790 59 791 0 792 0 793 53 794 0 795 0 796 15 797 0 798 0 799 44 800 0
79: Average symbolic conclusion length is 661304003/4409199 ≈ 149.98. (Median: 105)
There are 2150194 minimal D-proofs with conclusions of even symbolic length, and there are 2259005 minimal D-proofs with conclusions of odd symbolic length. [2150194/4409199 ≈ 48.77% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 2 12 2 13 7 14 12 15 8 16 26 17 42 18 34 19 71 20 122 21 138 22 226 23 296 24 382 25 417 26 588 27 777 28 932 29 1270 30 1552 31 2030 32 2011 33 2713 34 2815 35 3535 36 4143 37 4657 38 5084 39 6389 40 6187 41 8250 42 7760 43 9540 44 10395 45 12050 46 11745 47 13835 48 14698 49 16607 50 17170 51 18274 52 20009 53 20407 54 24050 55 25010 56 25694 57 26066 58 29001 59 29671 60 32719 61 31761 62 35792 63 33231 64 36833 65 36325 66 42006 67 35203 68 44791 69 36933 70 45553 71 39038 72 49962 73 38430 74 47100 75 39480 76 51715 77 39232 78 51281 79 38864 80 49045 81 38706 82 53865 83 35926 84 52243 85 37774 86 51122 87 34863 88 51137 89 34450 90 47296 91 36585 92 45816 93 33576 94 45273 95 34204 96 37877 97 34468 98 42109 99 31295 100 38711 101 30477 102 33715 103 30728 104 39290 105 25046 106 31359 107 25963 108 30531 109 25511 110 31581 111 22032 112 25331 113 21431 114 25247 115 22927 116 24236 117 21089 118 22517 119 17220 120 19789 121 19777 122 18493 123 16733 124 17958 125 15213 126 13939 127 18380 128 11605 129 12992 130 14274 131 13252 132 9680 133 17323 134 8017 135 12402 136 14190 137 10706 138 8295 139 15376 140 7772 141 9985 142 14105 143 8185 144 7262 145 14118 146 6310 147 7859 148 13691 149 7037 150 5184 151 12362 152 4266 153 6793 154 13716 155 5859 156 3558 157 12800 158 3338 159 5949 160 14426 161 4745 162 3356 163 13504 164 3565 165 5548 166 15096 167 3883 168 3274 169 12970 170 2986 171 4586 172 16666 173 3139 174 2379 175 13641 176 2076 177 3953 178 17189 179 2799 180 1542 181 13903 182 1567 183 3284 184 17319 185 2370 186 1693 187 13917 188 1786 189 3243 190 18728 191 2003 192 1577 193 16102 194 1575 195 2963 196 18220 197 1603 198 1174 199 16900 200 1139 201 2457 202 18960 203 1656 204 796 205 15856 206 705 207 2121 208 19265 209 1272 210 637 211 18970 212 907 213 2124 214 17963 215 1219 216 802 217 20370 218 661 219 1774 220 19031 221 991 222 778 223 19115 224 427 225 1828 226 17934 227 811 228 344 229 21754 230 344 231 1529 232 17959 233 756 234 421 235 21530 236 305 237 1435 238 17193 239 718 240 701 241 22388 242 280 243 2035 244 15539 245 537 246 273 247 23103 248 190 249 1208 250 16127 251 436 252 325 253 22904 254 174 255 774 256 14947 257 501 258 408 259 22250 260 158 261 1470 262 12533 263 475 264 172 265 23541 266 106 267 827 268 14817 269 348 270 292 271 22720 272 120 273 645 274 11737 275 272 276 135 277 21163 278 127 279 636 280 10664 281 271 282 130 283 23669 284 90 285 568 286 12485 287 403 288 399 289 20806 290 67 291 451 292 9057 293 255 294 117 295 20964 296 65 297 528 298 7683 299 111 300 95 301 21554 302 80 303 205 304 8168 305 211 306 386 307 19875 308 36 309 227 310 6739 311 251 312 153 313 19008 314 45 315 1018 316 4599 317 184 318 97 319 18723 320 41 321 183 322 5314 323 75 324 340 325 17799 326 33 327 101 328 4794 329 104 330 109 331 16438 332 28 333 724 334 3410 335 135 336 57 337 17017 338 32 339 144 340 4339 341 172 342 285 343 14331 344 22 345 181 346 3953 347 31 348 31 349 14347 350 31 351 18 352 2853 353 14 354 46 355 13974 356 16 357 66 358 4236 359 100 360 177 361 10947 362 13 363 177 364 3795 365 28 366 29 367 11348 368 15 369 28 370 2443 371 4 372 49 373 9225 374 7 375 14 376 3313 377 8 378 245 379 8713 380 10 381 100 382 3329 383 4 384 9 385 7449 386 9 387 42 388 2781 389 2 390 66 391 6196 392 2 393 24 394 2785 395 1 396 113 397 6483 398 2 399 110 400 2290 401 4 402 6 403 5314 404 6 405 34 406 2495 407 2 408 93 409 5439 410 7 411 5 412 2183 413 0 414 2 415 5333 416 1 417 51 418 2212 419 1 420 3 421 4748 422 1 423 3 424 1650 425 2 426 57 427 4238 428 3 429 7 430 2302 431 1 432 4 433 4797 434 5 435 63 436 1610 437 0 438 1 439 3698 440 1 441 4 442 1320 443 0 444 1 445 3240 446 0 447 5 448 1986 449 1 450 2 451 3584 452 2 453 31 454 1139 455 0 456 2 457 2535 458 4 459 8 460 1119 461 0 462 79 463 2397 464 1 465 13 466 1383 467 0 468 1 469 2962 470 0 471 37 472 951 473 1 474 2 475 1935 476 2 477 2 478 960 479 0 480 92 481 1972 482 2 483 1 484 1259 485 0 486 1 487 2329 488 1 489 13 490 835 491 0 492 0 493 1847 494 0 495 1 496 1022 497 1 498 2 499 1803 500 0 501 0 502 1367 503 0 504 1 505 2468 506 2 507 22 508 639 509 0 510 0 511 1596 512 0 513 1 514 844 515 0 516 0 517 1409 518 0 519 3 520 1117 521 1 522 1 523 2019 524 0 525 13 526 449 527 0 528 1 529 1177 530 0 531 0 532 709 533 0 534 0 535 1069 536 0 537 0 538 664 539 0 540 0 541 1735 542 0 543 12 544 389 545 1 546 0 547 1000 548 0 549 0 550 720 551 0 552 1 553 893 554 0 555 0 556 582 557 0 558 0 559 1439 560 0 561 1 562 317 563 0 564 0 565 1030 566 0 567 0 568 692 569 0 570 0 571 836 572 0 573 0 574 604 575 0 576 0 577 1748 578 0 579 5 580 281 581 0 582 0 583 819 584 0 585 3 586 609 587 0 588 0 589 622 590 0 591 0 592 554 593 0 594 0 595 1452 596 0 597 0 598 162 599 0 600 0 601 718 602 0 603 0 604 715 605 0 606 0 607 450 608 0 609 0 610 342 611 0 612 0 613 1204 614 0 615 1 616 137 617 0 618 0 619 558 620 0 621 0 622 625 623 0 624 0 625 287 626 0 627 1 628 324 629 0 630 0 631 993 632 0 633 0 634 123 635 0 636 0 637 637 638 0 639 0 640 508 641 0 642 0 643 316 644 0 645 1 646 328 647 0 648 0 649 1015 650 0 651 0 652 130 653 0 654 0 655 452 656 0 657 0 658 619 659 0 660 0 661 232 662 0 663 0 664 301 665 0 666 0 667 494 668 0 669 0 670 71 671 0 672 0 673 448 674 0 675 0 676 575 677 0 678 0 679 156 680 0 681 0 682 168 683 0 684 0 685 448 686 0 687 0 688 67 689 0 690 0 691 344 692 0 693 0 694 373 695 0 696 0 697 97 698 0 699 0 700 174 701 0 702 0 703 273 704 0 705 0 706 54 707 0 708 0 709 458 710 0 711 0 712 507 713 0 714 0 715 94 716 0 717 0 718 192 719 0 720 0 721 223 722 0 723 0 724 63 725 0 726 0 727 265 728 0 729 0 730 454 731 0 732 0 733 97 734 0 735 0 736 174 737 0 738 0 739 216 740 0 741 0 742 33 743 0 744 0 745 279 746 0 747 0 748 412 749 0 750 0 751 74 752 0 753 0 754 96 755 0 756 0 757 108 758 0 759 0 760 21 761 0 762 0 763 175 764 0 765 0 766 383 767 0 768 0 769 38 770 0 771 0 772 103 773 0 774 0 775 151 776 0 777 0 778 29 779 0 780 0 781 150 782 0 783 0 784 428 785 0 786 0 787 49 788 0 789 0 790 116 791 0 792 0 793 106 794 0 795 0 796 30 797 0 798 0 799 122 800 0
81: Average symbolic conclusion length is 1013666693/6623647 ≈ 153.04. (Median: 107)
There are 3279114 minimal D-proofs with conclusions of even symbolic length, and there are 3344533 minimal D-proofs with conclusions of odd symbolic length. [3279114/6623647 ≈ 49.51% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 1 12 6 13 3 14 11 15 17 16 12 17 28 18 72 19 63 20 131 21 193 22 181 23 293 24 409 25 552 26 534 27 926 28 1163 29 1421 30 1583 31 2047 32 2393 33 2715 34 3674 35 4075 36 4593 37 5816 38 6393 39 8086 40 7976 41 10394 42 10623 43 12717 44 13420 45 16469 46 15629 47 20107 48 19119 49 22591 50 22830 51 25844 52 26946 53 32135 54 29477 55 34241 56 34128 57 38076 58 38794 59 42009 60 42555 61 43307 62 47389 63 48095 64 50862 65 46774 66 58137 67 49957 68 58386 69 54614 70 63955 71 52682 72 65213 73 58523 74 67172 75 58579 76 70975 77 57030 78 69794 79 62653 80 75215 81 58023 82 72472 83 58626 84 75518 85 59898 86 76255 87 57590 88 70264 89 57609 90 73307 91 55596 92 72586 93 54239 94 66050 95 52088 96 71579 97 49196 98 68714 99 45225 100 62097 101 43901 102 68045 103 40462 104 57902 105 37681 106 54162 107 39147 108 52378 109 37539 110 44322 111 35111 112 45892 113 34682 114 36925 115 36923 116 36646 117 29516 118 37370 119 29020 120 28508 121 31566 122 27779 123 24283 124 29854 125 24503 126 21673 127 26312 128 22169 129 22004 130 26073 131 19311 132 17549 133 25574 134 21158 135 17965 136 24759 137 15169 138 14973 139 22165 140 16279 141 14217 142 21155 143 12608 144 10958 145 19505 146 9953 147 13386 148 18609 149 10676 150 7985 151 19246 152 7320 153 12186 154 20064 155 8888 156 6998 157 19286 158 7328 159 9032 160 20635 161 7660 162 6637 163 18543 164 6208 165 7276 166 21562 167 6331 168 5200 169 17400 170 4172 171 6082 172 23475 173 5324 174 3720 175 18515 176 3293 177 6068 178 23368 179 4541 180 3328 181 19665 182 3363 183 4768 184 25871 185 4078 186 3824 187 19009 188 3020 189 4641 190 26612 191 3365 192 2508 193 22115 194 1936 195 4138 196 26980 197 2892 198 1820 199 21328 200 1392 201 3763 202 29387 203 2462 204 2005 205 21693 206 1627 207 3197 208 28903 209 2305 210 1710 211 26244 212 1473 213 3322 214 29692 215 1828 216 1333 217 23685 218 952 219 2311 220 30643 221 1670 222 1084 223 23657 224 657 225 2972 226 30346 227 1436 228 659 229 28796 230 906 231 2152 232 29723 233 1351 234 768 235 27742 236 621 237 2367 238 28842 239 1110 240 734 241 27547 242 540 243 2109 244 29230 245 937 246 375 247 31087 248 365 249 1494 250 27703 251 856 252 340 253 30543 254 427 255 1483 256 26066 257 831 258 477 259 30534 260 329 261 2522 262 25678 263 588 264 317 265 33353 266 284 267 1188 268 23093 269 540 270 367 271 31090 272 267 273 667 274 22632 275 600 276 336 277 32181 278 270 279 2742 280 19796 281 520 282 170 283 32666 284 151 285 847 286 18810 287 423 288 425 289 30518 290 166 291 1234 292 16420 293 303 294 203 295 32006 296 158 297 1576 298 14095 299 393 300 137 301 31104 302 88 303 940 304 15306 305 408 306 354 307 28311 308 81 309 799 310 11733 311 213 312 124 313 30226 314 63 315 1683 316 9646 317 95 318 154 319 27670 320 43 321 261 322 11638 323 365 324 553 325 25599 326 55 327 472 328 9023 329 176 330 83 331 26290 332 44 333 2531 334 6879 335 291 336 120 337 22744 338 32 339 266 340 8913 341 47 342 861 343 22412 344 22 345 363 346 6455 347 153 348 91 349 22441 350 32 351 1437 352 5096 353 93 354 20 355 18449 356 21 357 167 358 7186 359 166 360 625 361 18515 362 13 363 504 364 4551 365 15 366 22 367 17864 368 19 369 93 370 3583 371 73 372 24 373 15432 374 21 375 80 376 6236 377 65 378 56 379 14176 380 14 381 467 382 3798 383 81 384 20 385 13398 386 10 387 17 388 2949 389 23 390 19 391 12492 392 8 393 13 394 4665 395 53 396 121 397 12641 398 11 399 299 400 3647 401 23 402 10 403 10218 404 9 405 24 406 2875 407 44 408 87 409 9776 410 2 411 26 412 4042 413 2 414 70 415 10582 416 2 417 275 418 2757 419 38 420 6 421 7483 422 6 423 13 424 2792 425 3 426 205 427 7634 428 4 429 11 430 3020 431 31 432 4 433 7521 434 1 435 182 436 2360 437 2 438 3 439 5452 440 2 441 22 442 2402 443 24 444 134 445 5140 446 3 447 7 448 2348 449 1 450 4 451 5539 452 3 453 160 454 1586 455 22 456 4 457 4397 458 0 459 5 460 2000 461 0 462 80 463 3999 464 0 465 5 466 1849 467 14 468 3 469 4946 470 1 471 92 472 1380 473 0 474 3 475 3847 476 2 477 4 478 1823 479 15 480 249 481 3474 482 0 483 8 484 1590 485 0 486 2 487 4688 488 0 489 107 490 1401 491 8 492 2 493 3001 494 1 495 7 496 1650 497 0 498 183 499 2901 500 1 501 11 502 1208 503 10 504 2 505 3541 506 0 507 58 508 1067 509 0 510 0 511 2336 512 0 513 3 514 1263 515 4 516 2 517 2277 518 0 519 0 520 1036 521 0 522 1 523 3151 524 1 525 47 526 672 527 6 528 0 529 2041 530 0 531 0 532 924 533 0 534 0 535 1805 536 0 537 0 538 1037 539 2 540 1 541 2506 542 0 543 20 544 597 545 0 546 1 547 1983 548 0 549 1 550 998 551 3 552 0 553 1637 554 0 555 3 556 905 557 0 558 0 559 2687 560 0 561 28 562 653 563 1 564 0 565 1726 566 0 567 0 568 921 569 0 570 1 571 1351 572 0 573 0 574 731 575 1 576 0 577 1997 578 0 579 6 580 506 581 0 582 0 583 1285 584 0 585 0 586 753 587 0 588 0 589 1043 590 0 591 0 592 506 593 0 594 0 595 1627 596 0 597 8 598 400 599 0 600 0 601 1044 602 0 603 0 604 759 605 0 606 0 607 754 608 0 609 0 610 533 611 0 612 0 613 1447 614 0 615 2 616 311 617 0 618 0 619 1112 620 0 621 3 622 823 623 0 624 0 625 742 626 0 627 1 628 517 629 0 630 0 631 1858 632 0 633 2 634 354 635 0 636 0 637 909 638 0 639 0 640 740 641 0 642 0 643 567 644 0 645 2 646 435 647 0 648 0 649 1079 650 0 651 0 652 279 653 0 654 0 655 821 656 0 657 0 658 746 659 0 660 0 661 455 662 0 663 0 664 296 665 0 666 0 667 1032 668 0 669 0 670 191 671 0 672 0 673 500 674 0 675 0 676 625 677 0 678 0 679 291 680 0 681 1 682 324 683 0 684 0 685 1114 686 0 687 0 688 136 689 0 690 0 691 623 692 0 693 0 694 663 695 0 696 0 697 317 698 0 699 0 700 292 701 0 702 0 703 960 704 0 705 0 706 166 707 0 708 0 709 464 710 0 711 0 712 772 713 0 714 0 715 230 716 0 717 0 718 250 719 0 720 0 721 502 722 0 723 0 724 108 725 0 726 0 727 478 728 0 729 0 730 534 731 0 732 0 733 156 734 0 735 0 736 166 737 0 738 0 739 526 740 0 741 0 742 71 743 0 744 0 745 214 746 0 747 0 748 448 749 0 750 0 751 115 752 0 753 0 754 184 755 0 756 0 757 314 758 0 759 0 760 49 761 0 762 0 763 385 764 0 765 0 766 738 767 0 768 0 769 110 770 0 771 0 772 173 773 0 774 0 775 359 776 0 777 0 778 62 779 0 780 0 781 224 782 0 783 0 784 494 785 0 786 0 787 85 788 0 789 0 790 148 791 0 792 0 793 273 794 0 795 0 796 50 797 0 798 0 799 228 800 0