-
Notifications
You must be signed in to change notification settings - Fork 3
/
w3-plot_data_x1000.txt
128 lines (96 loc) · 130 KB
/
w3-plot_data_x1000.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
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 39/1 ≈ 39.00. (Median: 39)
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 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 1
5: Average symbolic conclusion length is 102/2 ≈ 51.00. (Median: 51.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 0 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 0 44 0 45 1 46 0 47 0 48 0 49 0 50 0 51 0 52 0 53 0 54 0 55 0 56 0 57 1
7: Average symbolic conclusion length is 218/4 ≈ 54.50. (Median: 61.00)
There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 4 minimal D-proofs with conclusions of odd symbolic length. [0/4 ≈ 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 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 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 1 60 0 61 0 62 0 63 1 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 0 74 0 75 1
9: Average symbolic conclusion length is 493/7 ≈ 70.43. (Median: 77)
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 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 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 1 36 0 37 0 38 0 39 1 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 0 68 0 69 0 70 0 71 0 72 0 73 0 74 0 75 0 76 0 77 1 78 0 79 0 80 0 81 1 82 0 83 0 84 0 85 0 86 0 87 0 88 0 89 0 90 0 91 0 92 0 93 1 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 0 110 0 111 0 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 1
11: Average symbolic conclusion length is 1037/14 ≈ 74.07. (Median: 61.00)
There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 13 minimal D-proofs with conclusions of odd symbolic length. [1/14 ≈ 7.14% 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 0 22 0 23 0 24 0 25 1 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 1 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 1 54 0 55 0 56 0 57 2 58 0 59 2 60 0 61 0 62 0 63 1 64 0 65 0 66 0 67 1 68 0 69 0 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 0 92 0 93 0 94 0 95 1 96 0 97 0 98 0 99 1 100 0 101 0 102 0 103 0 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 1 112 0 113 0 114 0 115 0 116 0 117 0 118 0 119 1 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 1
13: Average symbolic conclusion length is 1999/23 ≈ 86.91. (Median: 77)
There are 2 minimal D-proofs with conclusions of even symbolic length, and there are 21 minimal D-proofs with conclusions of odd symbolic length. [2/23 ≈ 8.70% 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 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 1 36 0 37 0 38 0 39 1 40 0 41 0 42 0 43 1 44 0 45 0 46 0 47 1 48 0 49 0 50 0 51 0 52 0 53 1 54 2 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 1 72 0 73 0 74 0 75 2 76 0 77 4 78 0 79 0 80 0 81 1 82 0 83 0 84 0 85 1 86 0 87 0 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 0 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 1 114 0 115 0 116 0 117 1 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 1 130 0 131 0 132 0 133 0 134 0 135 0 136 0 137 1 138 0 139 0 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 2 156 0 157 0 158 0 159 0 160 0 161 0 162 0 163 0 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 1
15: Average symbolic conclusion length is 4018/42 ≈ 95.67. (Median: 86.00)
There are 4 minimal D-proofs with conclusions of even symbolic length, and there are 38 minimal D-proofs with conclusions of odd symbolic length. [4/42 ≈ 9.52% 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 0 22 0 23 1 24 0 25 0 26 0 27 0 28 0 29 1 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 0 44 0 45 0 46 0 47 1 48 0 49 0 50 0 51 0 52 0 53 2 54 0 55 0 56 0 57 2 58 0 59 1 60 1 61 2 62 0 63 1 64 0 65 2 66 0 67 1 68 0 69 1 70 0 71 1 72 3 73 0 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 1 84 0 85 0 86 0 87 0 88 0 89 2 90 0 91 0 92 0 93 2 94 0 95 5 96 0 97 0 98 0 99 1 100 0 101 0 102 0 103 1 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 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 1 132 0 133 0 134 0 135 1 136 0 137 0 138 0 139 0 140 0 141 0 142 0 143 0 144 0 145 0 146 0 147 1 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 1 156 0 157 0 158 0 159 0 160 0 161 0 162 0 163 0 164 0 165 0 166 0 167 1 168 0 169 0 170 0 171 0 172 0 173 2 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 2 192 0 193 0 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 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 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 0 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 1
17: Average symbolic conclusion length is 7600/72 ≈ 105.56. (Median: 89.50)
There are 8 minimal D-proofs with conclusions of even symbolic length, and there are 64 minimal D-proofs with conclusions of odd symbolic length. [8/72 ≈ 11.11% 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 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 1 37 1 38 0 39 1 40 0 41 3 42 0 43 1 44 0 45 1 46 0 47 2 48 0 49 2 50 0 51 1 52 0 53 0 54 0 55 0 56 0 57 1 58 0 59 1 60 0 61 0 62 0 63 0 64 0 65 1 66 0 67 0 68 0 69 0 70 0 71 2 72 0 73 0 74 1 75 1 76 0 77 2 78 2 79 4 80 0 81 2 82 0 83 2 84 0 85 1 86 0 87 1 88 0 89 2 90 4 91 0 92 0 93 1 94 0 95 0 96 0 97 1 98 0 99 0 100 0 101 2 102 0 103 0 104 0 105 0 106 0 107 2 108 0 109 0 110 0 111 2 112 0 113 6 114 0 115 0 116 0 117 1 118 0 119 1 120 0 121 1 122 0 123 0 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 0 140 0 141 0 142 0 143 0 144 0 145 0 146 0 147 0 148 0 149 1 150 0 151 0 152 0 153 1 154 0 155 0 156 0 157 0 158 0 159 0 160 0 161 0 162 0 163 0 164 0 165 1 166 0 167 0 168 0 169 0 170 0 171 1 172 0 173 1 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 1 188 0 189 0 190 0 191 2 192 0 193 0 194 0 195 1 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 1 204 0 205 0 206 0 207 0 208 0 209 2 210 0 211 0 212 0 213 0 214 0 215 0 216 0 217 0 218 0 219 1 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 1 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 0 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 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 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 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 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 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 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 0 392 0 393 1
19: Average symbolic conclusion length is 12926/119 ≈ 108.62. (Median: 96)
There are 17 minimal D-proofs with conclusions of even symbolic length, and there are 102 minimal D-proofs with conclusions of odd symbolic length. [17/119 ≈ 14.29% 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 0 22 0 23 0 24 0 25 1 26 0 27 1 28 0 29 0 30 0 31 0 32 0 33 1 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 1 48 0 49 0 50 1 51 0 52 0 53 1 54 3 55 2 56 1 57 2 58 0 59 4 60 0 61 2 62 0 63 1 64 1 65 5 66 0 67 6 68 0 69 4 70 0 71 3 72 0 73 1 74 0 75 1 76 0 77 3 78 0 79 2 80 0 81 0 82 0 83 2 84 0 85 0 86 0 87 2 88 0 89 2 90 0 91 0 92 2 93 1 94 0 95 1 96 3 97 4 98 0 99 2 100 0 101 2 102 0 103 2 104 0 105 1 106 0 107 1 108 5 109 0 110 0 111 1 112 0 113 1 114 0 115 2 116 0 117 0 118 0 119 3 120 0 121 0 122 0 123 0 124 0 125 2 126 0 127 0 128 0 129 2 130 0 131 7 132 0 133 0 134 1 135 1 136 0 137 0 138 0 139 1 140 0 141 0 142 0 143 0 144 0 145 0 146 0 147 1 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 2 156 0 157 1 158 0 159 1 160 0 161 0 162 0 163 0 164 0 165 0 166 0 167 1 168 0 169 0 170 0 171 1 172 0 173 0 174 0 175 1 176 0 177 0 178 0 179 0 180 0 181 0 182 0 183 1 184 0 185 0 186 0 187 0 188 0 189 0 190 0 191 1 192 0 193 0 194 0 195 0 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 0 204 0 205 1 206 0 207 0 208 0 209 2 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 1 228 0 229 0 230 0 231 1 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 1 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 0 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 1 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 1 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 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 0 302 0 303 0 304 0 305 0 306 0 307 0 308 0 309 1 310 0 311 0 312 0 313 0 314 0 315 1 316 0 317 0 318 0 319 0 320 0 321 1
21: Average symbolic conclusion length is 18506/180 ≈ 102.81. (Median: 95)
There are 34 minimal D-proofs with conclusions of even symbolic length, and there are 146 minimal D-proofs with conclusions of odd symbolic length. [34/180 ≈ 18.89% 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 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 1 36 0 37 0 38 0 39 1 40 1 41 4 42 0 43 4 44 0 45 2 46 0 47 2 48 0 49 1 50 0 51 4 52 0 53 2 54 0 55 1 56 0 57 1 58 0 59 1 60 0 61 1 62 0 63 1 64 0 65 2 66 0 67 0 68 2 69 0 70 0 71 1 72 5 73 2 74 6 75 2 76 0 77 4 78 1 79 6 80 0 81 3 82 2 83 4 84 0 85 7 86 0 87 5 88 0 89 3 90 0 91 2 92 0 93 2 94 0 95 6 96 1 97 8 98 0 99 0 100 0 101 3 102 0 103 0 104 0 105 3 106 0 107 2 108 0 109 0 110 3 111 1 112 0 113 1 114 4 115 5 116 0 117 3 118 0 119 3 120 0 121 2 122 0 123 1 124 0 125 1 126 6 127 0 128 0 129 1 130 0 131 0 132 0 133 3 134 1 135 0 136 0 137 4 138 0 139 1 140 0 141 0 142 0 143 2 144 0 145 0 146 0 147 2 148 0 149 8 150 0 151 0 152 2 153 1 154 0 155 0 156 0 157 2 158 0 159 0 160 0 161 0 162 0 163 0 164 0 165 0 166 0 167 0 168 0 169 0 170 0 171 1 172 0 173 0 174 0 175 2 176 0 177 0 178 0 179 0 180 0 181 0 182 0 183 0 184 0 185 1 186 0 187 0 188 0 189 2 190 0 191 0 192 0 193 0 194 0 195 1 196 0 197 0 198 0 199 0 200 0 201 2 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 1 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 1 224 0 225 0 226 0 227 2 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 1
23: Average symbolic conclusion length is 31952/296 ≈ 107.95. (Median: 99.50)
There are 62 minimal D-proofs with conclusions of even symbolic length, and there are 234 minimal D-proofs with conclusions of odd symbolic length. [62/296 ≈ 20.95% 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 0 22 0 23 0 24 0 25 0 26 0 27 2 28 0 29 3 30 0 31 1 32 0 33 0 34 0 35 0 36 0 37 1 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 2 48 0 49 2 50 2 51 0 52 0 53 1 54 1 55 3 56 0 57 5 58 2 59 4 60 0 61 6 62 2 63 4 64 0 65 4 66 0 67 11 68 1 69 11 70 0 71 6 72 0 73 5 74 0 75 2 76 0 77 3 78 0 79 4 80 1 81 4 82 0 83 3 84 0 85 3 86 3 87 2 88 0 89 2 90 7 91 4 92 13 93 3 94 0 95 4 96 2 97 6 98 0 99 3 100 3 101 4 102 0 103 8 104 0 105 6 106 0 107 2 108 0 109 3 110 0 111 2 112 0 113 8 114 1 115 13 116 0 117 1 118 0 119 4 120 0 121 0 122 0 123 4 124 0 125 2 126 0 127 0 128 4 129 1 130 0 131 1 132 5 133 5 134 0 135 3 136 0 137 3 138 0 139 3 140 0 141 1 142 0 143 1 144 7 145 0 146 0 147 1 148 0 149 0 150 1 151 4 152 2 153 0 154 0 155 5 156 0 157 2 158 0 159 0 160 0 161 2 162 0 163 0 164 0 165 2 166 0 167 9 168 0 169 0 170 4 171 1 172 0 173 0 174 0 175 3 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 1 189 0 190 0 191 0 192 0 193 4 194 0 195 0 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 1 204 0 205 0 206 0 207 1 208 0 209 0 210 0 211 1 212 0 213 0 214 0 215 0 216 0 217 0 218 0 219 2 220 0 221 0 222 0 223 0 224 0 225 0 226 0 227 1 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 1 242 0 243 0 244 0 245 2 246 0 247 0 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 1 264 0 265 1 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 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 0 320 0 321 0 322 0 323 0 324 0 325 0 326 0 327 0 328 0 329 1
25: Average symbolic conclusion length is 55919/493 ≈ 113.43. (Median: 109)
There are 114 minimal D-proofs with conclusions of even symbolic length, and there are 379 minimal D-proofs with conclusions of odd symbolic length. [114/493 ≈ 23.12% 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 1 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 0 37 1 38 2 39 0 40 0 41 2 42 0 43 7 44 1 45 6 46 0 47 5 48 0 49 3 50 0 51 4 52 0 53 2 54 0 55 7 56 2 57 3 58 0 59 2 60 0 61 4 62 1 63 2 64 0 65 4 66 0 67 9 68 5 69 1 70 0 71 1 72 2 73 4 74 1 75 7 76 6 77 5 78 2 79 8 80 4 81 10 82 1 83 7 84 1 85 13 86 2 87 13 88 0 89 10 90 1 91 7 92 0 93 2 94 1 95 6 96 1 97 8 98 4 99 8 100 0 101 8 102 0 103 7 104 5 105 2 106 0 107 4 108 9 109 5 110 22 111 4 112 0 113 6 114 3 115 8 116 0 117 6 118 4 119 4 120 0 121 11 122 0 123 10 124 0 125 2 126 0 127 5 128 0 129 2 130 0 131 10 132 1 133 21 134 0 135 1 136 0 137 5 138 0 139 1 140 0 141 5 142 0 143 2 144 0 145 1 146 5 147 1 148 0 149 2 150 6 151 5 152 0 153 3 154 0 155 3 156 0 157 4 158 0 159 1 160 0 161 1 162 8 163 0 164 0 165 1 166 0 167 0 168 2 169 5 170 3 171 0 172 0 173 6 174 0 175 3 176 0 177 0 178 0 179 2 180 0 181 1 182 0 183 2 184 0 185 10 186 0 187 0 188 6 189 1 190 0 191 0 192 0 193 5 194 0 195 0 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 0 204 1 205 1 206 2 207 0 208 0 209 1 210 0 211 6 212 0 213 0 214 0 215 1 216 0 217 0 218 0 219 0 220 0 221 1 222 0 223 0 224 0 225 1 226 0 227 0 228 0 229 2 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 2 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 1 246 0 247 0 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 1 260 0 261 0 262 0 263 2 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 1
27: Average symbolic conclusion length is 96376/809 ≈ 119.13. (Median: 113)
There are 197 minimal D-proofs with conclusions of even symbolic length, and there are 612 minimal D-proofs with conclusions of odd symbolic length. [197/809 ≈ 24.35% 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 0 22 0 23 0 24 0 25 0 26 0 27 1 28 0 29 1 30 0 31 7 32 0 33 2 34 0 35 1 36 0 37 0 38 0 39 0 40 0 41 2 42 0 43 2 44 0 45 1 46 0 47 0 48 0 49 1 50 0 51 3 52 1 53 0 54 2 55 5 56 5 57 5 58 1 59 4 60 0 61 12 62 3 63 7 64 3 65 12 66 3 67 7 68 0 69 17 70 1 71 11 72 1 73 14 74 7 75 10 76 2 77 10 78 0 79 11 80 2 81 9 82 0 83 8 84 3 85 16 86 8 87 8 88 0 89 11 90 3 91 8 92 2 93 10 94 10 95 6 96 5 97 13 98 6 99 15 100 2 101 8 102 2 103 18 104 3 105 18 106 0 107 14 108 2 109 10 110 0 111 3 112 4 113 6 114 0 115 9 116 9 117 13 118 0 119 11 120 0 121 12 122 7 123 3 124 0 125 8 126 11 127 8 128 33 129 5 130 0 131 9 132 4 133 8 134 0 135 7 136 5 137 6 138 0 139 15 140 0 141 11 142 0 143 2 144 0 145 8 146 0 147 1 148 0 149 12 150 2 151 28 152 0 153 2 154 1 155 7 156 0 157 0 158 0 159 7 160 0 161 2 162 0 163 1 164 6 165 1 166 0 167 3 168 7 169 6 170 0 171 3 172 0 173 3 174 0 175 4 176 0 177 2 178 0 179 1 180 9 181 0 182 0 183 2 184 0 185 0 186 2 187 6 188 4 189 0 190 0 191 7 192 0 193 4 194 0 195 0 196 0 197 2 198 0 199 0 200 0 201 2 202 1 203 11 204 0 205 0 206 8 207 1 208 0 209 0 210 1 211 7 212 0 213 0 214 0 215 0 216 0 217 0 218 0 219 0 220 0 221 1 222 2 223 0 224 3 225 1 226 0 227 0 228 0 229 8 230 0 231 0 232 0 233 1 234 0 235 0 236 0 237 0 238 0 239 1 240 0 241 0 242 0 243 1 244 0 245 0 246 0 247 3 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 2 256 0 257 0 258 1 259 0 260 0 261 0 262 0 263 1 264 0 265 0 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 0 274 0 275 1 276 0 277 1 278 0 279 0 280 0 281 2 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 1 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 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 0 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 1
29: Average symbolic conclusion length is 167325/1330 ≈ 125.81. (Median: 118)
There are 345 minimal D-proofs with conclusions of even symbolic length, and there are 985 minimal D-proofs with conclusions of odd symbolic length. [345/1330 ≈ 25.94% 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 1 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 1 32 0 33 1 34 0 35 0 36 1 37 1 38 0 39 1 40 1 41 1 42 3 43 3 44 0 45 13 46 0 47 8 48 1 49 14 50 0 51 6 52 0 53 6 54 0 55 4 56 1 57 7 58 0 59 11 60 1 61 9 62 2 63 4 64 0 65 6 66 0 67 7 68 0 69 16 70 3 71 4 72 4 73 8 74 9 75 6 76 4 77 7 78 1 79 17 80 7 81 10 82 10 83 21 84 9 85 17 86 2 87 25 88 4 89 15 90 2 91 16 92 18 93 14 94 10 95 14 96 0 97 20 98 6 99 20 100 0 101 14 102 6 103 25 104 11 105 24 106 0 107 26 108 4 109 11 110 3 111 16 112 15 113 10 114 8 115 19 116 9 117 28 118 4 119 9 120 3 121 25 122 4 123 25 124 0 125 20 126 4 127 15 128 0 129 6 130 9 131 9 132 0 133 12 134 16 135 19 136 1 137 15 138 2 139 16 140 9 141 6 142 0 143 11 144 13 145 9 146 46 147 7 148 0 149 12 150 7 151 9 152 0 153 10 154 7 155 4 156 1 157 19 158 0 159 14 160 0 161 2 162 0 163 12 164 0 165 2 166 0 167 15 168 2 169 36 170 0 171 2 172 4 173 9 174 0 175 1 176 0 177 11 178 0 179 2 180 1 181 2 182 7 183 1 184 0 185 6 186 8 187 7 188 0 189 4 190 0 191 4 192 0 193 5 194 0 195 4 196 0 197 1 198 10 199 1 200 0 201 2 202 0 203 0 204 3 205 7 206 5 207 1 208 0 209 8 210 0 211 4 212 0 213 0 214 0 215 3 216 0 217 0 218 0 219 3 220 2 221 12 222 0 223 0 224 10 225 1 226 0 227 0 228 1 229 10 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 1 240 2 241 0 242 4 243 2 244 0 245 1 246 0 247 10 248 0 249 0 250 0 251 1 252 0 253 0 254 0 255 0 256 0 257 1 258 0 259 0 260 0 261 1 262 0 263 0 264 1 265 4 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 2 274 0 275 0 276 2 277 0 278 0 279 0 280 0 281 1 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 1 296 0 297 0 298 0 299 2 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 1 313 0 314 0 315 0 316 0 317 1 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 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 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 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 1
31: Average symbolic conclusion length is 289958/2190 ≈ 132.40. (Median: 125)
There are 596 minimal D-proofs with conclusions of even symbolic length, and there are 1594 minimal D-proofs with conclusions of odd symbolic length. [596/2190 ≈ 27.21% 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 1 16 0 17 0 18 0 19 0 20 0 21 1 22 0 23 0 24 0 25 1 26 0 27 1 28 0 29 0 30 0 31 0 32 0 33 6 34 0 35 5 36 0 37 2 38 0 39 3 40 0 41 3 42 0 43 0 44 1 45 4 46 0 47 2 48 0 49 3 50 1 51 1 52 1 53 2 54 3 55 4 56 5 57 6 58 6 59 10 60 7 61 15 62 2 63 23 64 2 65 14 66 5 67 23 68 3 69 15 70 4 71 20 72 1 73 21 74 3 75 24 76 2 77 27 78 5 79 22 80 6 81 19 82 2 83 29 84 0 85 14 86 3 87 37 88 6 89 26 90 7 91 18 92 13 93 16 94 12 95 16 96 4 97 26 98 12 99 20 100 18 101 36 102 17 103 22 104 4 105 35 106 10 107 18 108 4 109 24 110 33 111 23 112 31 113 19 114 0 115 29 116 11 117 37 118 0 119 20 120 12 121 36 122 14 123 38 124 0 125 41 126 5 127 16 128 4 129 25 130 20 131 12 132 11 133 28 134 13 135 42 136 7 137 10 138 4 139 32 140 5 141 31 142 0 143 24 144 5 145 18 146 0 147 8 148 16 149 13 150 0 151 11 152 26 153 26 154 2 155 21 156 2 157 21 158 11 159 10 160 0 161 15 162 16 163 13 164 61 165 10 166 0 167 16 168 8 169 11 170 1 171 15 172 11 173 4 174 1 175 24 176 0 177 20 178 0 179 3 180 0 181 16 182 0 183 4 184 0 185 18 186 1 187 45 188 0 189 3 190 10 191 10 192 2 193 2 194 0 195 16 196 0 197 2 198 2 199 3 200 8 201 2 202 0 203 9 204 11 205 7 206 0 207 4 208 1 209 4 210 5 211 4 212 0 213 9 214 0 215 2 216 12 217 1 218 0 219 2 220 0 221 1 222 4 223 8 224 6 225 3 226 0 227 9 228 0 229 4 230 0 231 1 232 0 233 2 234 1 235 0 236 0 237 3 238 3 239 15 240 0 241 0 242 12 243 1 244 0 245 0 246 1 247 10 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 1 258 3 259 0 260 5 261 3 262 0 263 1 264 0 265 12 266 0 267 0 268 0 269 1 270 0 271 0 272 0 273 0 274 0 275 2 276 0 277 0 278 0 279 1 280 0 281 0 282 1 283 6 284 0 285 1 286 0 287 0 288 0 289 0 290 0 291 2 292 0 293 0 294 2 295 0 296 0 297 0 298 0 299 1 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 1 314 0 315 0 316 0 317 2 318 1 319 0 320 0 321 0 322 0 323 0 324 0 325 0 326 0 327 0 328 0 329 0 330 2 331 0 332 0 333 0 334 0 335 2 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 0 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 0 364 0 365 0 366 1 367 0 368 0 369 1 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 1 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 1 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 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 1
33: Average symbolic conclusion length is 504752/3606 ≈ 139.98. (Median: 131)
There are 1032 minimal D-proofs with conclusions of even symbolic length, and there are 2574 minimal D-proofs with conclusions of odd symbolic length. [1032/3606 ≈ 28.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 0 13 0 14 0 15 1 16 0 17 0 18 0 19 0 20 0 21 1 22 0 23 0 24 0 25 0 26 0 27 0 28 0 29 2 30 0 31 1 32 0 33 2 34 0 35 1 36 0 37 1 38 0 39 3 40 0 41 3 42 2 43 2 44 2 45 3 46 2 47 14 48 0 49 17 50 1 51 17 52 1 53 16 54 1 55 10 56 1 57 6 58 3 59 12 60 1 61 11 62 2 63 17 64 5 65 17 66 3 67 15 68 2 69 12 70 5 71 18 72 8 73 11 74 11 75 18 76 15 77 30 78 14 79 21 80 7 81 33 82 15 83 25 84 16 85 35 86 15 87 49 88 14 89 38 90 3 91 35 92 8 93 33 94 6 95 39 96 15 97 32 98 14 99 42 100 12 101 52 102 2 103 30 104 7 105 77 106 12 107 63 108 12 109 44 110 19 111 35 112 22 113 24 114 8 115 41 116 18 117 28 118 31 119 50 120 30 121 37 122 6 123 50 124 19 125 28 126 6 127 30 128 52 129 34 130 68 131 27 132 1 133 40 134 18 135 54 136 0 137 30 138 23 139 41 140 17 141 57 142 0 143 65 144 6 145 22 146 5 147 39 148 25 149 12 150 17 151 42 152 17 153 68 154 11 155 16 156 6 157 42 158 6 159 42 160 0 161 32 162 7 163 22 164 0 165 16 166 26 167 17 168 0 169 15 170 38 171 32 172 5 173 26 174 3 175 27 176 13 177 17 178 0 179 21 180 18 181 14 182 78 183 13 184 0 185 21 186 9 187 14 188 3 189 22 190 18 191 6 192 2 193 32 194 0 195 28 196 0 197 5 198 1 199 20 200 0 201 5 202 0 203 24 204 1 205 55 206 1 207 5 208 20 209 12 210 2 211 2 212 0 213 24 214 0 215 2 216 2 217 4 218 9 219 3 220 0 221 12 222 13 223 7 224 1 225 5 226 4 227 4 228 5 229 5 230 0 231 16 232 0 233 3 234 14 235 1 236 0 237 3 238 0 239 2 240 3 241 9 242 7 243 3 244 0 245 13 246 2 247 5 248 0 249 4 250 0 251 2 252 1 253 0 254 0 255 3 256 4 257 18 258 2 259 0 260 14 261 3 262 0 263 0 264 7 265 11 266 0 267 0 268 0 269 0 270 1 271 0 272 0 273 0 274 0 275 2 276 4 277 0 278 6 279 4 280 0 281 2 282 0 283 14 284 0 285 0 286 0 287 1 288 1 289 0 290 0 291 0 292 0 293 3 294 0 295 0 296 0 297 1 298 0 299 0 300 1 301 7 302 0 303 0 304 0 305 0 306 0 307 0 308 0 309 2 310 0 311 0 312 3 313 1 314 0 315 0 316 0 317 1 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 1 332 0 333 0 334 0 335 2 336 1 337 0 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 1 346 0 347 0 348 2 349 0 350 0 351 0 352 0 353 2 354 0 355 0 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 0 364 0 365 1 366 0 367 0 368 0 369 0 370 0 371 0 372 1 373 0 374 0 375 0 376 0 377 0 378 0 379 0 380 0 381 0 382 0 383 0 384 2 385 0 386 0 387 0 388 0 389 0 390 1 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 1 409 0 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 1 421 0 422 0 423 0 424 0 425 1 426 1 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 1 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 1 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 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 2 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 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 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 1
35: Average symbolic conclusion length is 873383/5925 ≈ 147.41. (Median: 139)
There are 1774 minimal D-proofs with conclusions of even symbolic length, and there are 4151 minimal D-proofs with conclusions of odd symbolic length. [1774/5925 ≈ 29.94% 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 0 22 0 23 1 24 0 25 1 26 0 27 2 28 1 29 4 30 0 31 1 32 0 33 3 34 0 35 6 36 1 37 8 38 0 39 5 40 1 41 4 42 1 43 5 44 0 45 3 46 1 47 4 48 0 49 4 50 0 51 6 52 2 53 6 54 0 55 7 56 3 57 9 58 7 59 8 60 7 61 11 62 9 63 25 64 5 65 34 66 4 67 32 68 4 69 28 70 7 71 34 72 6 73 30 74 10 75 42 76 14 77 42 78 7 79 35 80 11 81 49 82 18 83 42 84 14 85 47 86 8 87 44 88 11 89 46 90 16 91 43 92 19 93 51 94 36 95 60 96 34 97 48 98 16 99 59 100 36 101 57 102 31 103 65 104 32 105 76 106 33 107 59 108 8 109 64 110 17 111 48 112 16 113 62 114 36 115 45 116 32 117 72 118 28 119 97 120 7 121 49 122 15 123 122 124 21 125 109 126 21 127 68 128 27 129 55 130 34 131 31 132 17 133 57 134 23 135 43 136 51 137 74 138 46 139 53 140 9 141 72 142 32 143 35 144 7 145 39 146 75 147 50 148 122 149 37 150 3 151 51 152 28 153 75 154 1 155 45 156 33 157 52 158 22 159 80 160 2 161 92 162 7 163 27 164 8 165 60 166 32 167 15 168 19 169 56 170 22 171 99 172 16 173 18 174 8 175 53 176 7 177 53 178 0 179 44 180 9 181 25 182 0 183 25 184 38 185 25 186 0 187 19 188 51 189 44 190 8 191 34 192 6 193 39 194 15 195 24 196 0 197 28 198 20 199 17 200 97 201 21 202 0 203 32 204 13 205 15 206 5 207 28 208 27 209 8 210 6 211 39 212 1 213 35 214 0 215 10 216 3 217 24 218 0 219 9 220 0 221 30 222 5 223 69 224 2 225 7 226 34 227 15 228 3 229 4 230 2 231 34 232 0 233 4 234 5 235 6 236 10 237 3 238 0 239 15 240 15 241 7 242 3 243 4 244 9 245 7 246 6 247 6 248 0 249 28 250 0 251 3 252 17 253 2 254 0 255 6 256 0 257 3 258 4 259 10 260 9 261 3 262 0 263 13 264 2 265 5 266 0 267 7 268 0 269 2 270 2 271 0 272 0 273 4 274 5 275 21 276 2 277 0 278 18 279 4 280 0 281 0 282 8 283 14 284 0 285 0 286 0 287 0 288 1 289 0 290 0 291 0 292 0 293 1 294 4 295 1 296 7 297 6 298 0 299 3 300 3 301 16 302 0 303 0 304 0 305 2 306 1 307 1 308 0 309 0 310 0 311 4 312 2 313 1 314 0 315 2 316 0 317 0 318 8 319 8 320 0 321 0 322 0 323 0 324 0 325 0 326 0 327 2 328 0 329 0 330 4 331 1 332 0 333 0 334 0 335 2 336 0 337 0 338 0 339 0 340 0 341 0 342 2 343 0 344 0 345 0 346 0 347 1 348 0 349 2 350 0 351 0 352 0 353 2 354 1 355 0 356 0 357 0 358 0 359 0 360 0 361 0 362 0 363 1 364 0 365 0 366 3 367 0 368 0 369 0 370 0 371 2 372 0 373 0 374 0 375 0 376 0 377 0 378 1 379 0 380 0 381 0 382 0 383 1 384 0 385 0 386 0 387 0 388 0 389 0 390 2 391 0 392 0 393 0 394 0 395 0 396 0 397 0 398 0 399 1 400 0 401 0 402 2 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 1 426 2 427 0 428 0 429 0 430 0 431 0 432 0 433 0 434 0 435 1 436 0 437 0 438 2 439 0 440 0 441 0 442 0 443 1 444 2 445 0 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 1 456 0 457 0 458 0 459 0 460 0 461 0 462 1 463 0 464 0 465 0 466 0 467 0 468 0 469 0 470 0 471 0 472 0 473 0 474 1 475 0 476 0 477 0 478 0 479 0 480 1 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 1 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 1 516 2 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 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 2 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 1 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 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 1 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 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 0 644 0 645 1
37: Average symbolic conclusion length is 1511483/9738 ≈ 155.21. (Median: 145)
There are 3035 minimal D-proofs with conclusions of even symbolic length, and there are 6703 minimal D-proofs with conclusions of odd symbolic length. [3035/9738 ≈ 31.17% 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 1 18 0 19 0 20 0 21 0 22 0 23 1 24 0 25 1 26 0 27 1 28 0 29 0 30 0 31 2 32 0 33 1 34 0 35 0 36 0 37 2 38 1 39 2 40 1 41 2 42 1 43 7 44 2 45 4 46 9 47 9 48 1 49 14 50 4 51 31 52 0 53 25 54 3 55 25 56 7 57 19 58 4 59 18 60 7 61 24 62 4 63 21 64 4 65 27 66 6 67 26 68 1 69 40 70 11 71 42 72 5 73 35 74 8 75 36 76 20 77 38 78 15 79 41 80 24 81 55 82 17 83 55 84 24 85 54 86 16 87 51 88 23 89 102 90 22 91 74 92 24 93 75 94 41 95 71 96 26 97 63 98 24 99 80 100 47 101 84 102 45 103 92 104 38 105 92 106 25 107 110 108 32 109 111 110 29 111 97 112 73 113 101 114 70 115 83 116 25 117 108 118 68 119 98 120 50 121 91 122 57 123 127 124 60 125 105 126 12 127 106 128 30 129 73 130 28 131 100 132 66 133 62 134 56 135 107 136 51 137 156 138 16 139 65 140 32 141 176 142 33 143 180 144 31 145 111 146 40 147 91 148 48 149 41 150 36 151 77 152 30 153 62 154 83 155 100 156 65 157 81 158 15 159 99 160 52 161 52 162 10 163 57 164 103 165 72 166 196 167 54 168 5 169 74 170 43 171 94 172 3 173 63 174 52 175 60 176 27 177 108 178 3 179 127 180 12 181 34 182 15 183 89 184 40 185 19 186 26 187 85 188 27 189 142 190 22 191 23 192 17 193 64 194 9 195 66 196 0 197 61 198 18 199 28 200 2 201 32 202 53 203 35 204 2 205 27 206 67 207 52 208 13 209 42 210 9 211 41 212 18 213 31 214 0 215 42 216 23 217 23 218 118 219 26 220 1 221 42 222 14 223 17 224 8 225 38 226 39 227 13 228 4 229 54 230 2 231 44 232 0 233 13 234 3 235 29 236 1 237 15 238 1 239 40 240 9 241 84 242 4 243 8 244 52 245 23 246 6 247 5 248 4 249 44 250 0 251 3 252 4 253 8 254 11 255 5 256 0 257 18 258 19 259 9 260 5 261 8 262 16 263 13 264 11 265 8 266 1 267 42 268 0 269 5 270 23 271 3 272 0 273 8 274 0 275 4 276 7 277 14 278 11 279 4 280 0 281 14 282 3 283 5 284 1 285 11 286 0 287 2 288 4 289 0 290 0 291 6 292 6 293 22 294 3 295 0 296 22 297 3 298 0 299 1 300 9 301 16 302 0 303 5 304 0 305 1 306 2 307 1 308 0 309 3 310 0 311 1 312 5 313 2 314 9 315 9 316 0 317 4 318 3 319 18 320 0 321 1 322 0 323 3 324 3 325 2 326 0 327 1 328 0 329 4 330 2 331 1 332 1 333 3 334 0 335 2 336 10 337 10 338 0 339 0 340 0 341 0 342 0 343 1 344 0 345 7 346 0 347 0 348 3 349 2 350 1 351 0 352 0 353 2 354 3 355 0 356 0 357 0 358 0 359 0 360 2 361 0 362 0 363 0 364 0 365 4 366 3 367 2 368 0 369 0 370 0 371 3 372 9 373 0 374 0 375 0 376 0 377 0 378 2 379 0 380 0 381 1 382 0 383 0 384 4 385 3 386 0 387 1 388 0 389 2 390 0 391 0 392 1 393 0 394 0 395 0 396 1 397 0 398 0 399 0 400 0 401 2 402 0 403 0 404 0 405 0 406 0 407 0 408 1 409 0 410 1 411 0 412 0 413 0 414 1 415 0 416 0 417 1 418 0 419 0 420 3 421 1 422 0 423 0 424 0 425 2 426 0 427 0 428 0 429 0 430 0 431 0 432 1 433 0 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 1 444 3 445 0 446 0 447 0 448 0 449 0 450 1 451 0 452 0 453 1 454 0 455 0 456 2 457 0 458 0 459 0 460 0 461 1 462 1 463 0 464 0 465 0 466 0 467 1 468 0 469 0 470 0 471 0 472 0 473 1 474 0 475 0 476 0 477 0 478 0 479 1 480 2 481 0 482 0 483 0 484 0 485 0 486 0 487 0 488 0 489 0 490 0 491 0 492 2 493 0 494 0 495 0 496 0 497 0 498 3 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 1 517 0 518 1 519 0 520 0 521 0 522 0 523 0 524 0 525 1 526 0 527 0 528 1 529 0 530 0 531 0 532 0 533 1 534 2 535 0 536 0 537 0 538 0 539 0 540 0 541 0 542 0 543 0 544 0 545 1 546 0 547 0 548 0 549 0 550 0 551 0 552 2 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 2 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 1 589 0 590 0 591 0 592 0 593 0 594 1 595 0 596 0 597 0 598 0 599 0 600 0 601 0 602 0 603 0 604 0 605 1 606 2 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 1 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 0 644 0 645 1 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 1 661 0 662 0 663 1 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 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 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 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 0 734 0 735 1
39: Average symbolic conclusion length is 2599689/15948 ≈ 163.01. (Median: 153)
There are 5159 minimal D-proofs with conclusions of even symbolic length, and there are 10789 minimal D-proofs with conclusions of odd symbolic length. [5159/15948 ≈ 32.35% 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 2 20 0 21 0 22 0 23 0 24 0 25 0 26 0 27 1 28 0 29 1 30 0 31 5 32 1 33 3 34 0 35 3 36 0 37 8 38 2 39 10 40 1 41 10 42 0 43 9 44 0 45 11 46 2 47 9 48 1 49 11 50 0 51 6 52 0 53 9 54 3 55 7 56 4 57 12 58 8 59 17 60 15 61 17 62 11 63 28 64 25 65 49 66 9 67 49 68 9 69 65 70 7 71 54 72 15 73 56 74 29 75 46 76 23 77 82 78 27 79 84 80 28 81 76 82 19 83 86 84 29 85 90 86 12 87 102 88 28 89 115 90 18 91 83 92 19 93 92 94 47 95 95 96 34 97 131 98 63 99 124 100 45 101 98 102 60 103 135 104 35 105 105 106 48 107 206 108 52 109 131 110 49 111 131 112 83 113 119 114 74 115 94 116 51 117 138 118 95 119 160 120 106 121 168 122 95 123 153 124 44 125 201 126 64 127 180 128 45 129 150 130 135 131 150 132 139 133 126 134 37 135 160 136 114 137 172 138 77 139 131 140 96 141 191 142 96 143 169 144 19 145 186 146 45 147 105 148 42 149 159 150 110 151 75 152 89 153 155 154 88 155 236 156 29 157 97 158 55 159 243 160 50 161 273 162 46 163 151 164 57 165 124 166 64 167 64 168 63 169 106 170 36 171 78 172 130 173 140 174 92 175 108 176 19 177 135 178 78 179 71 180 14 181 86 182 137 183 97 184 293 185 73 186 9 187 99 188 60 189 122 190 8 191 85 192 76 193 74 194 32 195 149 196 6 197 182 198 15 199 38 200 27 201 128 202 48 203 29 204 32 205 110 206 33 207 198 208 29 209 33 210 33 211 80 212 18 213 82 214 2 215 87 216 22 217 33 218 6 219 52 220 70 221 43 222 7 223 48 224 88 225 65 226 19 227 48 228 13 229 51 230 28 231 39 232 0 233 62 234 36 235 31 236 143 237 33 238 2 239 56 240 19 241 23 242 12 243 47 244 54 245 20 246 8 247 63 248 3 249 55 250 0 251 15 252 10 253 37 254 4 255 19 256 1 257 47 258 17 259 99 260 5 261 11 262 74 263 26 264 12 265 14 266 7 267 59 268 0 269 5 270 13 271 11 272 13 273 6 274 0 275 21 276 19 277 12 278 13 279 8 280 25 281 16 282 10 283 13 284 1 285 58 286 0 287 6 288 24 289 4 290 0 291 10 292 0 293 9 294 11 295 20 296 12 297 5 298 0 299 22 300 7 301 7 302 2 303 17 304 0 305 3 306 3 307 1 308 0 309 8 310 8 311 25 312 6 313 1 314 26 315 6 316 0 317 4 318 15 319 18 320 3 321 8 322 0 323 2 324 6 325 2 326 0 327 7 328 0 329 1 330 9 331 6 332 12 333 11 334 0 335 4 336 4 337 22 338 1 339 1 340 0 341 2 342 7 343 3 344 0 345 2 346 0 347 4 348 3 349 2 350 3 351 3 352 0 353 4 354 11 355 12 356 0 357 5 358 0 359 0 360 1 361 1 362 0 363 8 364 0 365 1 366 4 367 2 368 2 369 1 370 0 371 3 372 3 373 0 374 0 375 1 376 0 377 0 378 5 379 3 380 1 381 0 382 0 383 3 384 3 385 3 386 1 387 1 388 0 389 3 390 12 391 0 392 1 393 0 394 0 395 0 396 2 397 0 398 0 399 1 400 0 401 0 402 3 403 3 404 1 405 3 406 0 407 3 408 3 409 0 410 2 411 0 412 0 413 1 414 1 415 1 416 0 417 0 418 0 419 3 420 2 421 2 422 1 423 0 424 0 425 2 426 11 427 1 428 2 429 0 430 0 431 0 432 2 433 0 434 0 435 8 436 0 437 0 438 5 439 1 440 0 441 1 442 0 443 1 444 0 445 0 446 1 447 0 448 0 449 0 450 2 451 0 452 0 453 0 454 0 455 3 456 0 457 1 458 0 459 0 460 0 461 1 462 2 463 1 464 1 465 0 466 0 467 0 468 1 469 0 470 0 471 1 472 0 473 0 474 3 475 1 476 0 477 0 478 0 479 2 480 1 481 0 482 0 483 0 484 0 485 0 486 3 487 0 488 0 489 0 490 0 491 1 492 0 493 0 494 0 495 0 496 0 497 1 498 3 499 0 500 0 501 0 502 0 503 0 504 2 505 0 506 0 507 0 508 0 509 0 510 2 511 0 512 0 513 0 514 0 515 1 516 1 517 0 518 1 519 0 520 0 521 0 522 1 523 0 524 0 525 0 526 0 527 0 528 0 529 0 530 0 531 0 532 0 533 2 534 2 535 0 536 1 537 0 538 0 539 0 540 1 541 0 542 0 543 1 544 0 545 0 546 2 547 0 548 0 549 0 550 0 551 1 552 4 553 0 554 0 555 0 556 0 557 0 558 0 559 0 560 0 561 0 562 0 563 1 564 0 565 0 566 0 567 0 568 0 569 0 570 1 571 0 572 0 573 0 574 0 575 0 576 0 577 0 578 0 579 0 580 0 581 0 582 1 583 0 584 0 585 0 586 0 587 1 588 2 589 0 590 1 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 3 607 0 608 0 609 0 610 0 611 0 612 1 613 0 614 0 615 1 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 1 624 2 625 0 626 0 627 0 628 0 629 0 630 0 631 0 632 0 633 0 634 0 635 1 636 0 637 0 638 0 639 0 640 0 641 0 642 1 643 0 644 0 645 1 646 0 647 0 648 1 649 0 650 0 651 0 652 0 653 0 654 0 655 0 656 0 657 0 658 0 659 0 660 2 661 0 662 0 663 1 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 1 679 0 680 0 681 1 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 1 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 1 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 0 734 0 735 1 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 1 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 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 801 0 802 0 803 0 804 0 805 0 806 0 807 0 808 0 809 0 810 0 811 0 812 0 813 0 814 0 815 0 816 0 817 0 818 0 819 0 820 0 821 0 822 0 823 0 824 0 825 2 826 0 827 0 828 0 829 0 830 0 831 0 832 0 833 0 834 0 835 0 836 0 837 0 838 0 839 0 840 0 841 0 842 0 843 0 844 0 845 0 846 0 847 0 848 0 849 0 850 0 851 0 852 0 853 0 854 0 855 0 856 0 857 0 858 0 859 0 860 0 861 0 862 0 863 0 864 0 865 0 866 0 867 0 868 0 869 0 870 0 871 0 872 0 873 0 874 0 875 0 876 0 877 0 878 0 879 0 880 0 881 0 882 0 883 0 884 0 885 0 886 0 887 0 888 0 889 0 890 0 891 0 892 0 893 0 894 0 895 0 896 0 897 0 898 0 899 0 900 0 901 0 902 0 903 0 904 0 905 0 906 0 907 0 908 0 909 0 910 0 911 0 912 0 913 0 914 0 915 1
41: Average symbolic conclusion length is 4470434/26109 ≈ 171.22. (Median: 159)
There are 8703 minimal D-proofs with conclusions of even symbolic length, and there are 17406 minimal D-proofs with conclusions of odd symbolic length. [8703/26109 ≈ 33.33% 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 2 20 0 21 1 22 0 23 0 24 0 25 3 26 0 27 0 28 0 29 2 30 1 31 2 32 0 33 4 34 0 35 4 36 1 37 3 38 0 39 1 40 0 41 2 42 2 43 5 44 1 45 6 46 0 47 11 48 7 49 13 50 8 51 19 52 1 53 45 54 4 55 41 56 4 57 41 58 2 59 38 60 7 61 41 62 6 63 33 64 13 65 42 66 7 67 47 68 12 69 60 70 10 71 58 72 13 73 72 74 24 75 67 76 26 77 69 78 44 79 70 80 30 81 87 82 58 83 106 84 41 85 108 86 43 87 125 88 36 89 100 90 50 91 148 92 73 93 140 94 65 95 188 96 86 97 177 98 92 99 139 100 52 101 173 102 93 103 173 104 60 105 189 106 79 107 257 108 59 109 210 110 44 111 207 112 89 113 210 114 68 115 239 116 130 117 227 118 94 119 195 120 116 121 251 122 64 123 165 124 86 125 378 126 93 127 255 128 87 129 217 130 143 131 202 132 154 133 158 134 92 135 232 136 155 137 248 138 198 139 258 140 195 141 240 142 75 143 307 144 112 145 265 146 65 147 231 148 227 149 240 150 269 151 187 152 53 153 239 154 178 155 267 156 116 157 179 158 151 159 260 160 131 161 260 162 37 163 307 164 67 165 143 166 61 167 253 168 165 169 109 170 137 171 220 172 135 173 357 174 55 175 124 176 89 177 337 178 71 179 385 180 70 181 216 182 83 183 177 184 84 185 104 186 112 187 157 188 43 189 113 190 194 191 190 192 131 193 151 194 27 195 181 196 111 197 109 198 26 199 119 200 181 201 118 202 416 203 103 204 17 205 142 206 80 207 146 208 15 209 117 210 118 211 86 212 39 213 198 214 13 215 236 216 24 217 55 218 44 219 167 220 55 221 40 222 42 223 148 224 39 225 264 226 38 227 39 228 66 229 103 230 27 231 99 232 4 233 136 234 27 235 42 236 11 237 70 238 88 239 54 240 10 241 73 242 111 243 79 244 26 245 60 246 20 247 62 248 37 249 55 250 0 251 89 252 39 253 41 254 174 255 59 256 3 257 75 258 27 259 39 260 17 261 67 262 72 263 28 264 9 265 77 266 12 267 66 268 0 269 25 270 16 271 45 272 8 273 22 274 1 275 59 276 26 277 124 278 10 279 13 280 101 281 34 282 17 283 14 284 19 285 74 286 0 287 7 288 23 289 17 290 17 291 9 292 0 293 29 294 26 295 14 296 16 297 11 298 37 299 21 300 13 301 21 302 3 303 80 304 0 305 10 306 35 307 6 308 1 309 15 310 1 311 10 312 12 313 24 314 13 315 9 316 0 317 28 318 14 319 8 320 4 321 25 322 0 323 6 324 17 325 5 326 1 327 8 328 9 329 27 330 6 331 1 332 31 333 8 334 0 335 10 336 15 337 24 338 3 339 9 340 0 341 3 342 9 343 3 344 0 345 13 346 0 347 5 348 12 349 9 350 21 351 12 352 0 353 14 354 8 355 27 356 2 357 2 358 0 359 2 360 5 361 3 362 2 363 6 364 0 365 10 366 8 367 2 368 5 369 4 370 0 371 3 372 18 373 16 374 1 375 11 376 0 377 1 378 7 379 2 380 2 381 11 382 1 383 1 384 8 385 9 386 3 387 1 388 0 389 5 390 5 391 0 392 1 393 1 394 1 395 1 396 9 397 3 398 1 399 0 400 0 401 3 402 4 403 3 404 3 405 5 406 0 407 4 408 13 409 0 410 5 411 6 412 0 413 0 414 4 415 2 416 0 417 2 418 0 419 0 420 4 421 6 422 3 423 5 424 0 425 5 426 3 427 1 428 3 429 1 430 0 431 0 432 5 433 1 434 0 435 1 436 0 437 3 438 2 439 2 440 2 441 1 442 0 443 3 444 15 445 3 446 4 447 0 448 0 449 1 450 3 451 1 452 0 453 7 454 0 455 1 456 4 457 4 458 1 459 2 460 0 461 2 462 3 463 2 464 2 465 2 466 0 467 0 468 2 469 0 470 0 471 0 472 0 473 3 474 2 475 1 476 0 477 1 478 0 479 2 480 12 481 1 482 2 483 0 484 0 485 0 486 2 487 0 488 0 489 3 490 0 491 0 492 4 493 2 494 1 495 4 496 0 497 2 498 1 499 0 500 2 501 0 502 0 503 1 504 4 505 1 506 0 507 0 508 0 509 2 510 1 511 0 512 0 513 0 514 0 515 3 516 2 517 0 518 3 519 0 520 0 521 0 522 2 523 0 524 0 525 7 526 0 527 0 528 3 529 0 530 0 531 0 532 0 533 2 534 1 535 0 536 1 537 0 538 1 539 0 540 3 541 0 542 0 543 0 544 0 545 2 546 0 547 0 548 0 549 1 550 0 551 2 552 3 553 0 554 2 555 0 556 0 557 0 558 5 559 0 560 0 561 1 562 0 563 0 564 2 565 1 566 1 567 0 568 0 569 1 570 3 571 0 572 1 573 0 574 0 575 0 576 0 577 0 578 0 579 0 580 0 581 1 582 0 583 0 584 0 585 0 586 0 587 2 588 2 589 1 590 1 591 0 592 0 593 0 594 2 595 0 596 0 597 0 598 0 599 0 600 2 601 0 602 0 603 0 604 0 605 2 606 4 607 0 608 1 609 0 610 0 611 0 612 1 613 0 614 0 615 0 616 0 617 0 618 0 619 0 620 0 621 0 622 0 623 0 624 2 625 0 626 0 627 0 628 0 629 0 630 1 631 0 632 0 633 2 634 0 635 0 636 2 637 0 638 0 639 0 640 0 641 2 642 2 643 0 644 0 645 1 646 0 647 0 648 0 649 0 650 0 651 0 652 0 653 1 654 0 655 0 656 0 657 0 658 0 659 0 660 3 661 0 662 2 663 0 664 0 665 0 666 2 667 0 668 0 669 0 670 0 671 0 672 0 673 0 674 0 675 0 676 0 677 0 678 2 679 0 680 0 681 1 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 1 697 0 698 0 699 1 700 0 701 0 702 1 703 0 704 0 705 1 706 0 707 0 708 0 709 0 710 0 711 0 712 0 713 1 714 2 715 0 716 0 717 0 718 0 719 0 720 0 721 0 722 0 723 0 724 0 725 1 726 0 727 0 728 0 729 0 730 0 731 0 732 1 733 0 734 1 735 1 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 1 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 1 769 0 770 0 771 1 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 1 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 801 0 802 0 803 0 804 0 805 0 806 0 807 0 808 0 809 0 810 0 811 0 812 0 813 0 814 0 815 0 816 0 817 0 818 0 819 0 820 0 821 0 822 0 823 0 824 0 825 1 826 0 827 0 828 0 829 0 830 0 831 0 832 0 833 0 834 0 835 0 836 0 837 0 838 0 839 0 840 0 841 0 842 0 843 2 844 0 845 0 846 0 847 0 848 0 849 0 850 0 851 0 852 0 853 0 854 0 855 0 856 0 857 0 858 0 859 0 860 0 861 0 862 0 863 0 864 0 865 0 866 0 867 0 868 0 869 0 870 0 871 0 872 0 873 0 874 0 875 0 876 0 877 0 878 0 879 0 880 0 881 0 882 0 883 0 884 0 885 0 886 0 887 0 888 0 889 0 890 0 891 0 892 0 893 0 894 0 895 0 896 0 897 0 898 0 899 0 900 0 901 0 902 0 903 0 904 0 905 0 906 0 907 0 908 0 909 0 910 0 911 0 912 0 913 0 914 0 915 2 916 0 917 0 918 0 919 0 920 0 921 0 922 0 923 0 924 0 925 0 926 0 927 0 928 0 929 0 930 0 931 0 932 0 933 1 934 0 935 0 936 0 937 0 938 0 939 0 940 0 941 0 942 0 943 0 944 0 945 0 946 0 947 0 948 0 949 0 950 0 951 0 952 0 953 0 954 0 955 0 956 0 957 0 958 0 959 0 960 0 961 0 962 0 963 0 964 0 965 0 966 0 967 0 968 0 969 0 970 0 971 0 972 0 973 0 974 0 975 0 976 0 977 0 978 0 979 0 980 0 981 0 982 0 983 0 984 0 985 0 986 0 987 0 988 0 989 0 990 0 991 0 992 0 993 0 994 0 995 0 996 0 997 0 998 0 999 0 1000 0
43: Average symbolic conclusion length is 7696663/42844 ≈ 179.64. (Median: 167)
There are 14689 minimal D-proofs with conclusions of even symbolic length, and there are 28155 minimal D-proofs with conclusions of odd symbolic length. [14689/42844 ≈ 34.28% 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 0 22 0 23 1 24 1 25 0 26 0 27 1 28 0 29 3 30 2 31 2 32 0 33 5 34 0 35 6 36 1 37 7 38 2 39 9 40 0 41 17 42 2 43 17 44 5 45 15 46 2 47 17 48 2 49 21 50 2 51 17 52 3 53 22 54 4 55 12 56 5 57 25 58 9 59 17 60 10 61 31 62 21 63 29 64 18 65 40 66 23 67 82 68 28 69 87 70 19 71 111 72 16 73 105 74 23 75 94 76 21 77 85 78 43 79 127 80 38 81 134 82 61 83 168 84 42 85 166 86 50 87 171 88 36 89 186 90 44 91 230 92 70 93 176 94 74 95 207 96 114 97 209 98 82 99 217 100 124 101 246 102 132 103 243 104 125 105 263 106 97 107 282 108 106 109 300 110 153 111 267 112 130 113 330 114 202 115 311 116 218 117 240 118 116 119 321 120 236 121 335 122 169 123 358 124 182 125 477 126 139 127 392 128 89 129 379 130 161 131 344 132 121 133 396 134 242 135 366 136 185 137 340 138 220 139 425 140 109 141 276 142 145 143 617 144 167 145 483 146 147 147 347 148 221 149 337 150 278 151 235 152 154 153 347 154 234 155 351 156 336 157 391 158 347 159 333 160 117 161 458 162 191 163 390 164 90 165 324 166 356 167 342 168 478 169 284 170 77 171 340 172 262 173 403 174 162 175 261 176 231 177 364 178 179 179 375 180 63 181 488 182 95 183 205 184 88 185 395 186 243 187 141 188 193 189 307 190 197 191 513 192 92 193 167 194 140 195 435 196 96 197 552 198 98 199 290 200 120 201 228 202 109 203 157 204 176 205 223 206 54 207 146 208 281 209 261 210 186 211 201 212 44 213 251 214 157 215 150 216 41 217 180 218 238 219 161 220 572 221 156 222 23 223 218 224 107 225 192 226 29 227 158 228 181 229 109 230 52 231 261 232 22 233 313 234 42 235 69 236 69 237 220 238 62 239 63 240 59 241 196 242 53 243 349 244 49 245 55 246 131 247 125 248 32 249 138 250 7 251 191 252 41 253 51 254 24 255 91 256 106 257 73 258 18 259 99 260 139 261 88 262 36 263 74 264 40 265 92 266 47 267 71 268 2 269 142 270 56 271 54 272 210 273 73 274 2 275 102 276 37 277 57 278 25 279 90 280 96 281 40 282 18 283 106 284 16 285 83 286 4 287 40 288 17 289 49 290 12 291 43 292 2 293 78 294 41 295 160 296 15 297 21 298 134 299 41 300 20 301 17 302 34 303 102 304 1 305 20 306 25 307 24 308 22 309 31 310 3 311 33 312 34 313 19 314 22 315 25 316 52 317 36 318 17 319 23 320 17 321 98 322 1 323 13 324 45 325 13 326 4 327 20 328 2 329 15 330 22 331 34 332 18 333 18 334 1 335 33 336 18 337 21 338 18 339 37 340 0 341 9 342 31 343 7 344 3 345 14 346 12 347 32 348 14 349 3 350 37 351 11 352 0 353 16 354 18 355 28 356 4 357 17 358 1 359 6 360 22 361 2 362 2 363 12 364 0 365 5 366 15 367 9 368 22 369 16 370 0 371 17 372 18 373 33 374 6 375 6 376 0 377 5 378 30 379 7 380 4 381 7 382 0 383 10 384 7 385 3 386 8 387 5 388 0 389 9 390 19 391 20 392 1 393 11 394 3 395 4 396 7 397 3 398 5 399 16 400 1 401 3 402 13 403 9 404 3 405 5 406 0 407 13 408 9 409 2 410 5 411 2 412 1 413 5 414 10 415 6 416 1 417 6 418 0 419 5 420 8 421 5 422 12 423 7 424 0 425 9 426 22 427 1 428 6 429 11 430 0 431 1 432 8 433 2 434 1 435 10 436 0 437 2 438 11 439 7 440 7 441 6 442 0 443 8 444 5 445 5 446 5 447 1 448 0 449 1 450 10 451 3 452 2 453 1 454 1 455 9 456 3 457 6 458 5 459 3 460 0 461 4 462 16 463 7 464 6 465 9 466 0 467 1 468 3 469 1 470 0 471 9 472 0 473 1 474 5 475 7 476 2 477 3 478 0 479 2 480 3 481 2 482 3 483 5 484 0 485 5 486 8 487 1 488 1 489 2 490 0 491 3 492 2 493 3 494 1 495 3 496 0 497 3 498 17 499 2 500 8 501 0 502 0 503 1 504 5 505 0 506 2 507 3 508 0 509 0 510 3 511 2 512 2 513 7 514 0 515 4 516 4 517 3 518 4 519 0 520 0 521 0 522 5 523 1 524 0 525 0 526 0 527 3 528 3 529 1 530 0 531 0 532 0 533 4 534 13 535 3 536 4 537 0 538 0 539 0 540 3 541 0 542 1 543 10 544 0 545 0 546 4 547 0 548 0 549 2 550 0 551 2 552 1 553 0 554 3 555 3 556 1 557 0 558 6 559 0 560 0 561 0 562 0 563 2 564 0 565 0 566 1 567 2 568 0 569 2 570 2 571 0 572 4 573 0 574 0 575 0 576 5 577 0 578 0 579 1 580 0 581 0 582 5 583 2 584 2 585 2 586 0 587 2 588 3 589 0 590 3 591 1 592 0 593 1 594 2 595 0 596 0 597 1 598 0 599 1 600 0 601 0 602 0 603 2 604 0 605 4 606 3 607 1 608 2 609 0 610 0 611 0 612 7 613 0 614 0 615 8 616 0 617 0 618 2 619 0 620 1 621 0 622 0 623 1 624 2 625 0 626 2 627 0 628 0 629 1 630 2 631 1 632 0 633 1 634 0 635 2 636 0 637 0 638 0 639 0 640 0 641 2 642 4 643 0 644 0 645 0 646 0 647 1 648 3 649 0 650 0 651 1 652 0 653 0 654 3 655 1 656 0 657 0 658 0 659 2 660 4 661 0 662 1 663 0 664 0 665 1 666 2 667 0 668 0 669 0 670 0 671 1 672 0 673 0 674 0 675 0 676 0 677 0 678 2 679 0 680 2 681 0 682 1 683 0 684 2 685 0 686 0 687 0 688 0 689 0 690 2 691 0 692 0 693 0 694 0 695 2 696 2 697 0 698 0 699 1 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 4 715 1 716 0 717 1 718 0 719 0 720 1 721 0 722 0 723 2 724 0 725 0 726 0 727 0 728 1 729 0 730 0 731 1 732 2 733 0 734 2 735 1 736 0 737 0 738 0 739 0 740 0 741 0 742 0 743 1 744 0 745 1 746 0 747 0 748 0 749 0 750 1 751 0 752 1 753 0 754 0 755 0 756 1 757 0 758 0 759 0 760 0 761 0 762 0 763 0 764 0 765 0 766 0 767 0 768 2 769 0 770 0 771 1 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 1 787 0 788 0 789 1 790 0 791 0 792 0 793 0 794 0 795 1 796 0 797 0 798 0 799 0 800 0 801 0 802 0 803 1 804 0 805 0 806 1 807 0 808 0 809 0 810 1 811 0 812 0 813 0 814 0 815 1 816 0 817 0 818 0 819 0 820 0 821 0 822 1 823 0 824 0 825 2 826 0 827 0 828 0 829 0 830 0 831 0 832 0 833 0 834 0 835 0 836 0 837 0 838 0 839 0 840 0 841 0 842 0 843 1 844 0 845 0 846 0 847 0 848 0 849 0 850 0 851 0 852 0 853 0 854 0 855 0 856 0 857 0 858 0 859 0 860 0 861 2 862 0 863 0 864 0 865 0 866 0 867 0 868 0 869 0 870 0 871 0 872 0 873 0 874 0 875 1 876 0 877 0 878 0 879 0 880 0 881 0 882 0 883 0 884 0 885 0 886 0 887 0 888 0 889 0 890 0 891 0 892 0 893 0 894 0 895 0 896 0 897 1 898 0 899 0 900 0 901 0 902 0 903 0 904 0 905 0 906 0 907 0 908 0 909 0 910 0 911 0 912 0 913 0 914 0 915 2 916 0 917 0 918 0 919 0 920 0 921 0 922 0 923 0 924 0 925 0 926 0 927 0 928 0 929 0 930 0 931 0 932 0 933 2 934 0 935 0 936 0 937 0 938 0 939 0 940 0 941 0 942 0 943 0 944 0 945 0 946 0 947 0 948 0 949 0 950 0 951 1 952 0 953 0 954 0 955 0 956 0 957 0 958 0 959 0 960 0 961 0 962 0 963 0 964 0 965 0 966 0 967 0 968 0 969 0 970 0 971 0 972 0 973 0 974 0 975 0 976 0 977 0 978 0 979 0 980 0 981 0 982 0 983 0 984 0 985 1 986 0 987 0 988 0 989 0 990 0 991 0 992 0 993 0 994 0 995 0 996 0 997 0 998 0 999 0 1000 0
45: Average symbolic conclusion length is 13205080/70083 ≈ 188.42. (Median: 175)
There are 24557 minimal D-proofs with conclusions of even symbolic length, and there are 45526 minimal D-proofs with conclusions of odd symbolic length. [24557/70083 ≈ 35.04% 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 2 22 0 23 2 24 0 25 0 26 0 27 2 28 0 29 3 30 0 31 2 32 0 33 6 34 0 35 4 36 0 37 7 38 0 39 4 40 1 41 7 42 2 43 7 44 5 45 4 46 4 47 8 48 7 49 22 50 6 51 26 52 10 53 24 54 9 55 63 56 11 57 69 58 14 59 69 60 10 61 63 62 17 63 59 64 20 65 58 66 27 67 92 68 19 69 74 70 26 71 125 72 30 73 103 74 27 75 129 76 37 77 119 78 49 79 147 80 71 81 115 82 65 83 169 84 72 85 208 86 91 87 201 88 68 89 248 90 81 91 254 92 90 93 255 94 82 95 300 96 137 97 340 98 124 99 335 100 165 101 337 102 131 103 329 104 161 105 366 106 118 107 374 108 141 109 547 110 177 111 444 112 176 113 478 114 255 115 449 116 200 117 465 118 243 119 475 120 301 121 488 122 274 123 490 124 223 125 485 126 197 127 540 128 284 129 518 130 215 131 556 132 383 133 556 134 453 135 421 136 214 137 573 138 472 139 587 140 347 141 575 142 345 143 755 144 267 145 648 146 153 147 615 148 265 149 548 150 203 151 657 152 409 153 546 154 327 155 537 156 379 157 721 158 182 159 408 160 236 161 982 162 271 163 841 164 236 165 552 166 326 167 526 168 453 169 345 170 255 171 506 172 331 173 500 174 547 175 564 176 557 177 513 178 172 179 651 180 318 181 546 182 126 183 463 184 534 185 518 186 799 187 405 188 102 189 487 190 376 191 567 192 229 193 368 194 343 195 482 196 224 197 555 198 118 199 728 200 137 201 278 202 128 203 582 204 332 205 191 206 272 207 446 208 273 209 717 210 154 211 221 212 216 213 569 214 140 215 733 216 140 217 409 218 175 219 299 220 136 221 234 222 266 223 320 224 71 225 203 226 399 227 341 228 258 229 269 230 80 231 319 232 213 233 211 234 68 235 261 236 299 237 218 238 766 239 210 240 40 241 314 242 141 243 238 244 42 245 232 246 269 247 141 248 62 249 349 250 36 251 397 252 50 253 110 254 106 255 292 256 71 257 108 258 81 259 271 260 74 261 462 262 64 263 76 264 222 265 163 266 49 267 181 268 18 269 289 270 65 271 60 272 45 273 128 274 130 275 109 276 32 277 147 278 177 279 108 280 49 281 97 282 71 283 100 284 65 285 99 286 6 287 204 288 76 289 74 290 255 291 90 292 2 293 139 294 58 295 71 296 30 297 124 298 124 299 52 300 36 301 131 302 22 303 109 304 6 305 84 306 32 307 61 308 19 309 55 310 3 311 92 312 59 313 188 314 23 315 29 316 173 317 57 318 34 319 29 320 50 321 129 322 5 323 24 324 43 325 32 326 33 327 52 328 3 329 44 330 51 331 36 332 32 333 41 334 71 335 51 336 31 337 46 338 23 339 121 340 3 341 21 342 57 343 16 344 9 345 43 346 4 347 28 348 25 349 42 350 27 351 22 352 5 353 40 354 27 355 31 356 32 357 62 358 5 359 15 360 34 361 11 362 6 363 50 364 14 365 48 366 25 367 10 368 46 369 26 370 3 371 17 372 21 373 41 374 17 375 25 376 1 377 11 378 33 379 5 380 6 381 17 382 5 383 16 384 24 385 24 386 29 387 24 388 1 389 25 390 24 391 34 392 21 393 7 394 1 395 13 396 46 397 5 398 11 399 9 400 1 401 14 402 22 403 4 404 14 405 14 406 0 407 13 408 21 409 25 410 7 411 20 412 5 413 11 414 24 415 9 416 7 417 18 418 2 419 4 420 15 421 12 422 4 423 13 424 0 425 27 426 21 427 2 428 6 429 6 430 4 431 7 432 41 433 6 434 3 435 15 436 0 437 9 438 10 439 3 440 16 441 10 442 0 443 13 444 24 445 13 446 9 447 14 448 1 449 5 450 10 451 5 452 4 453 9 454 0 455 6 456 14 457 13 458 8 459 9 460 0 461 19 462 9 463 12 464 9 465 6 466 1 467 1 468 8 469 3 470 7 471 7 472 1 473 10 474 7 475 5 476 7 477 13 478 0 479 6 480 27 481 8 482 8 483 16 484 0 485 9 486 10 487 3 488 2 489 13 490 1 491 1 492 11 493 11 494 12 495 8 496 0 497 3 498 5 499 2 500 5 501 5 502 1 503 5 504 13 505 4 506 3 507 5 508 0 509 4 510 9 511 4 512 3 513 4 514 0 515 8 516 18 517 4 518 13 519 9 520 1 521 3 522 8 523 1 524 1 525 10 526 1 527 2 528 5 529 4 530 7 531 8 532 0 533 5 534 4 535 9 536 4 537 3 538 6 539 2 540 10 541 1 542 2 543 3 544 0 545 9 546 3 547 2 548 1 549 1 550 0 551 3 552 19 553 4 554 8 555 2 556 1 557 0 558 9 559 0 560 1 561 12 562 0 563 0 564 3 565 5 566 0 567 4 568 0 569 3 570 6 571 4 572 5 573 3 574 1 575 2 576 6 577 0 578 1 579 0 580 0 581 3 582 2 583 0 584 1 585 4 586 0 587 3 588 14 589 1 590 12 591 1 592 0 593 0 594 6 595 0 596 1 597 8 598 1 599 0 600 5 601 2 602 4 603 5 604 0 605 3 606 4 607 1 608 5 609 2 610 0 611 0 612 7 613 0 614 1 615 1 616 0 617 2 618 0 619 0 620 0 621 3 622 0 623 5 624 2 625 8 626 4 627 0 628 0 629 0 630 7 631 0 632 0 633 7 634 0 635 1 636 5 637 0 638 2 639 0 640 0 641 2 642 3 643 0 644 3 645 6 646 0 647 2 648 4 649 1 650 1 651 2 652 0 653 1 654 2 655 1 656 0 657 1 658 0 659 2 660 6 661 0 662 3 663 0 664 0 665 2 666 10 667 0 668 0 669 1 670 0 671 0 672 3 673 1 674 0 675 2 676 0 677 2 678 3 679 0 680 2 681 0 682 0 683 4 684 2 685 0 686 0 687 0 688 0 689 2 690 1 691 0 692 0 693 0 694 0 695 4 696 3 697 0 698 2 699 0 700 1 701 0 702 5 703 0 704 0 705 9 706 0 707 0 708 3 709 1 710 0 711 0 712 0 713 1 714 4 715 0 716 0 717 2 718 0 719 0 720 4 721 0 722 0 723 1 724 0 725 2 726 0 727 0 728 0 729 1 730 0 731 0 732 4 733 1 734 2 735 1 736 0 737 1 738 1 739 0 740 0 741 1 742 0 743 0 744 2 745 2 746 2 747 0 748 0 749 2 750 2 751 0 752 2 753 1 754 0 755 1 756 0 757 1 758 0 759 0 760 0 761 1 762 0 763 1 764 0 765 0 766 0 767 0 768 3 769 0 770 1 771 0 772 0 773 0 774 1 775 0 776 0 777 0 778 0 779 0 780 0 781 0 782 1 783 0 784 0 785 1 786 2 787 0 788 0 789 1 790 1 791 0 792 0 793 0 794 0 795 0 796 0 797 0 798 0 799 0 800 0 801 0 802 0 803 0 804 1 805 0 806 2 807 1 808 0 809 0 810 1 811 0 812 0 813 3 814 0 815 0 816 0 817 0 818 0 819 0 820 0 821 1 822 2 823 0 824 1 825 1 826 1 827 0 828 1 829 0 830 0 831 0 832 0 833 1 834 0 835 2 836 0 837 0 838 0 839 0 840 1 841 1 842 0 843 0 844 0 845 0 846 1 847 0 848 0 849 0 850 0 851 0 852 0 853 0 854 0 855 0 856 0 857 0 858 1 859 0 860 0 861 1 862 0 863 0 864 0 865 0 866 0 867 0 868 0 869 0 870 0 871 0 872 0 873 0 874 0 875 0 876 1 877 0 878 1 879 2 880 0 881 0 882 0 883 0 884 0 885 1 886 0 887 0 888 0 889 0 890 1 891 1 892 0 893 1 894 0 895 0 896 0 897 1 898 0 899 0 900 0 901 0 902 0 903 1 904 0 905 1 906 0 907 0 908 0 909 0 910 0 911 0 912 0 913 0 914 0 915 3 916 0 917 0 918 0 919 0 920 0 921 0 922 0 923 0 924 0 925 0 926 0 927 0 928 0 929 0 930 0 931 0 932 0 933 1 934 0 935 0 936 0 937 0 938 0 939 0 940 0 941 0 942 0 943 0 944 0 945 0 946 0 947 0 948 0 949 0 950 0 951 2 952 0 953 0 954 1 955 0 956 0 957 0 958 0 959 0 960 0 961 0 962 0 963 0 964 0 965 1 966 0 967 0 968 0 969 1 970 0 971 0 972 0 973 0 974 0 975 0 976 0 977 0 978 0 979 0 980 0 981 0 982 0 983 0 984 0 985 0 986 0 987 0 988 0 989 0 990 0 991 0 992 0 993 0 994 0 995 0 996 0 997 0 998 0 999 0 1000 0
47: Average symbolic conclusion length is 22708074/115027 ≈ 197.42. (Median: 181)
There are 41251 minimal D-proofs with conclusions of even symbolic length, and there are 73776 minimal D-proofs with conclusions of odd symbolic length. [41251/115027 ≈ 35.86% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 1 20 0 21 1 22 0 23 3 24 0 25 1 26 0 27 3 28 0 29 3 30 0 31 1 32 1 33 3 34 0 35 6 36 0 37 12 38 1 39 7 40 4 41 14 42 5 43 27 44 0 45 26 46 4 47 34 48 4 49 23 50 1 51 39 52 1 53 33 54 5 55 40 56 2 57 25 58 13 59 42 60 21 61 45 62 24 63 51 64 26 65 60 66 49 67 80 68 44 69 121 70 41 71 178 72 35 73 179 74 52 75 177 76 61 77 165 78 53 79 161 80 87 81 212 82 87 83 225 84 130 85 336 86 110 87 298 88 98 89 377 90 99 91 346 92 110 93 402 94 125 95 324 96 163 97 436 98 192 99 408 100 185 101 439 102 189 103 476 104 276 105 484 106 188 107 554 108 231 109 684 110 227 111 604 112 193 113 596 114 308 115 647 116 298 117 680 118 384 119 637 120 328 121 613 122 428 123 736 124 326 125 719 126 348 127 1134 128 373 129 884 130 360 131 877 132 513 133 802 134 445 135 773 136 424 137 863 138 603 139 862 140 568 141 834 142 491 143 837 144 352 145 966 146 503 147 926 148 341 149 933 150 702 151 927 152 855 153 692 154 350 155 916 156 836 157 946 158 632 159 864 160 608 161 1143 162 480 163 1024 164 240 165 1033 166 419 167 786 168 323 169 1026 170 665 171 787 172 546 173 841 174 621 175 1143 176 280 177 628 178 390 179 1478 180 420 181 1383 182 370 183 828 184 472 185 799 186 679 187 512 188 409 189 749 190 453 191 673 192 831 193 805 194 863 195 721 196 241 197 933 198 510 199 753 200 171 201 662 202 783 203 698 204 1266 205 580 206 148 207 676 208 519 209 804 210 324 211 510 212 519 213 658 214 292 215 764 216 184 217 1090 218 201 219 374 220 209 221 853 222 460 223 281 224 362 225 638 226 361 227 990 228 244 229 295 230 331 231 724 232 192 233 994 234 203 235 575 236 252 237 395 238 176 239 343 240 396 241 432 242 102 243 306 244 545 245 463 246 361 247 366 248 112 249 423 250 286 251 265 252 105 253 371 254 388 255 314 256 995 257 305 258 70 259 461 260 188 261 315 262 74 263 324 264 392 265 192 266 87 267 457 268 67 269 527 270 68 271 151 272 157 273 372 274 86 275 150 276 105 277 367 278 111 279 591 280 90 281 118 282 363 283 216 284 77 285 246 286 44 287 374 288 92 289 91 290 82 291 185 292 161 293 152 294 61 295 207 296 217 297 148 298 73 299 127 300 125 301 142 302 89 303 141 304 10 305 325 306 96 307 98 308 310 309 129 310 12 311 185 312 85 313 101 314 50 315 165 316 154 317 74 318 59 319 152 320 34 321 147 322 18 323 119 324 62 325 89 326 37 327 83 328 11 329 132 330 104 331 223 332 38 333 48 334 222 335 77 336 41 337 47 338 77 339 169 340 13 341 57 342 66 343 52 344 44 345 76 346 9 347 67 348 79 349 43 350 52 351 67 352 94 353 83 354 53 355 62 356 29 357 164 358 12 359 46 360 80 361 24 362 18 363 60 364 6 365 44 366 34 367 58 368 27 369 36 370 9 371 47 372 45 373 47 374 49 375 92 376 9 377 35 378 66 379 16 380 13 381 67 382 17 383 60 384 43 385 20 386 54 387 44 388 6 389 27 390 45 391 56 392 26 393 30 394 3 395 17 396 38 397 9 398 24 399 39 400 9 401 19 402 31 403 31 404 35 405 37 406 4 407 31 408 35 409 52 410 47 411 23 412 6 413 28 414 54 415 17 416 15 417 65 418 3 419 23 420 43 421 5 422 28 423 30 424 3 425 36 426 31 427 32 428 15 429 30 430 13 431 15 432 40 433 8 434 9 435 30 436 3 437 17 438 33 439 18 440 13 441 16 442 8 443 32 444 25 445 21 446 26 447 12 448 7 449 12 450 60 451 12 452 10 453 21 454 5 455 24 456 22 457 10 458 23 459 20 460 3 461 23 462 27 463 15 464 12 465 31 466 3 467 8 468 29 469 6 470 8 471 19 472 1 473 9 474 23 475 22 476 9 477 16 478 0 479 25 480 23 481 12 482 12 483 12 484 2 485 16 486 49 487 7 488 11 489 11 490 2 491 12 492 9 493 9 494 11 495 20 496 0 497 15 498 34 499 13 500 13 501 20 502 7 503 12 504 12 505 8 506 8 507 15 508 2 509 4 510 18 511 16 512 12 513 17 514 0 515 17 516 9 517 6 518 14 519 9 520 3 521 6 522 10 523 7 524 7 525 19 526 2 527 6 528 10 529 7 530 7 531 8 532 0 533 13 534 31 535 20 536 15 537 17 538 2 539 8 540 15 541 1 542 6 543 10 544 1 545 4 546 15 547 6 548 10 549 10 550 0 551 6 552 6 553 10 554 6 555 11 556 7 557 4 558 21 559 2 560 6 561 4 562 0 563 11 564 7 565 6 566 14 567 2 568 0 569 3 570 20 571 7 572 13 573 11 574 1 575 5 576 5 577 1 578 3 579 13 580 0 581 0 582 7 583 6 584 8 585 10 586 1 587 4 588 5 589 6 590 6 591 8 592 2 593 6 594 13 595 1 596 1 597 6 598 2 599 4 600 7 601 1 602 2 603 12 604 0 605 6 606 21 607 0 608 14 609 2 610 1 611 0 612 15 613 0 614 2 615 16 616 1 617 3 618 4 619 3 620 10 621 6 622 0 623 4 624 8 625 10 626 8 627 4 628 0 629 1 630 7 631 2 632 4 633 1 634 1 635 11 636 2 637 1 638 0 639 5 640 0 641 4 642 15 643 9 644 6 645 5 646 0 647 1 648 8 649 1 650 3 651 15 652 0 653 1 654 5 655 7 656 3 657 2 658 0 659 3 660 4 661 0 662 7 663 7 664 0 665 4 666 14 667 1 668 2 669 2 670 2 671 3 672 2 673 1 674 0 675 3 676 0 677 3 678 6 679 2 680 9 681 0 682 6 683 3 684 10 685 0 686 0 687 1 688 0 689 0 690 6 691 1 692 1 693 3 694 0 695 4 696 4 697 1 698 4 699 2 700 0 701 4 702 4 703 0 704 0 705 3 706 0 707 2 708 3 709 0 710 2 711 1 712 0 713 5 714 7 715 6 716 5 717 1 718 1 719 0 720 14 721 0 722 1 723 10 724 0 725 1 726 4 727 1 728 0 729 0 730 0 731 1 732 4 733 0 734 3 735 7 736 0 737 2 738 4 739 0 740 0 741 0 742 0 743 1 744 0 745 2 746 1 747 1 748 0 749 2 750 6 751 2 752 1 753 1 754 0 755 2 756 3 757 0 758 0 759 1 760 0 761 0 762 3 763 2 764 2 765 3 766 0 767 2 768 4 769 0 770 2 771 2 772 0 773 3 774 5 775 1 776 0 777 0 778 0 779 2 780 0 781 1 782 0 783 1 784 0 785 2 786 2 787 0 788 1 789 0 790 0 791 0 792 1 793 0 794 1 795 10 796 0 797 0 798 2 799 0 800 1 801 0 802 0 803 1 804 2 805 0 806 2 807 4 808 1 809 0 810 3 811 0 812 0 813 1 814 0 815 2 816 0 817 0 818 0 819 0 820 0 821 0 822 5 823 0 824 2 825 1 826 0 827 2 828 1 829 0 830 0 831 1 832 0 833 0 834 0 835 4 836 0 837 0 838 0 839 1 840 3 841 0 842 1 843 0 844 1 845 2 846 1 847 0 848 0 849 0 850 0 851 1 852 0 853 2 854 0 855 1 856 0 857 0 858 1 859 1 860 0 861 0 862 1 863 0 864 2 865 0 866 0 867 0 868 0 869 0 870 0 871 0 872 1 873 0 874 0 875 1 876 3 877 0 878 2 879 1 880 0 881 0 882 0 883 1 884 0 885 0 886 0 887 0 888 0 889 0 890 0 891 1 892 0 893 0 894 1 895 0 896 1 897 3 898 0 899 0 900 0 901 0 902 0 903 3 904 0 905 0 906 0 907 0 908 2 909 1 910 0 911 1 912 1 913 0 914 0 915 3 916 0 917 1 918 0 919 0 920 0 921 0 922 0 923 1 924 1 925 4 926 0 927 0 928 0 929 0 930 1 931 0 932 0 933 1 934 0 935 1 936 0 937 0 938 0 939 0 940 0 941 0 942 0 943 0 944 1 945 0 946 0 947 0 948 0 949 0 950 1 951 1 952 0 953 0 954 0 955 0 956 0 957 0 958 0 959 1 960 0 961 0 962 0 963 0 964 0 965 0 966 0 967 1 968 0 969 2 970 1 971 0 972 1 973 0 974 0 975 1 976 0 977 0 978 0 979 0 980 0 981 0 982 0 983 1 984 0 985 1 986 0 987 1 988 0 989 0 990 0 991 0 992 0 993 1 994 0 995 1 996 0 997 0 998 0 999 0 1000 0
49: Average symbolic conclusion length is 38968929/188519 ≈ 206.71. (Median: 189)
There are 69034 minimal D-proofs with conclusions of even symbolic length, and there are 119485 minimal D-proofs with conclusions of odd symbolic length. [69034/188519 ≈ 36.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 0 13 1 14 0 15 0 16 0 17 2 18 0 19 0 20 0 21 0 22 0 23 3 24 0 25 4 26 0 27 2 28 0 29 3 30 0 31 8 32 1 33 8 34 2 35 10 36 0 37 10 38 1 39 10 40 0 41 13 42 0 43 7 44 1 45 12 46 5 47 11 48 9 49 11 50 9 51 31 52 13 53 31 54 13 55 49 56 19 57 88 58 21 59 109 60 21 61 113 62 25 63 104 64 26 65 108 66 23 67 100 68 35 69 170 70 28 71 131 72 47 73 222 74 50 75 194 76 49 77 228 78 81 79 257 80 106 81 253 82 110 83 251 84 163 85 329 86 144 87 370 88 133 89 452 90 127 91 431 92 200 93 482 94 221 95 477 96 208 97 599 98 291 99 613 100 280 101 567 102 376 103 744 104 342 105 665 106 308 107 791 108 303 109 770 110 336 111 911 112 396 113 854 114 427 115 1036 116 471 117 1020 118 499 119 907 120 419 121 958 122 674 123 1015 124 436 125 1107 126 528 127 1340 128 476 129 1164 130 400 131 1152 132 612 133 1191 134 609 135 1304 136 806 137 1211 138 671 139 1146 140 887 141 1360 142 667 143 1165 144 657 145 2022 146 705 147 1552 148 654 149 1409 150 929 151 1384 152 877 153 1262 154 717 155 1398 156 1056 157 1424 158 1068 159 1355 160 996 161 1355 162 601 163 1581 164 849 165 1572 166 519 167 1482 168 1191 169 1469 170 1506 171 1087 172 542 173 1469 174 1364 175 1488 176 1056 177 1306 178 1000 179 1663 180 787 181 1586 182 395 183 1638 184 645 185 1130 186 501 187 1615 188 1029 189 1145 190 860 191 1228 192 970 193 1782 194 445 195 897 196 615 197 2159 198 622 199 2159 200 580 201 1222 202 684 203 1150 204 980 205 775 206 647 207 1100 208 598 209 930 210 1262 211 1140 212 1278 213 1024 214 343 215 1289 216 794 217 1026 218 253 219 911 220 1114 221 965 222 1931 223 832 224 210 225 973 226 711 227 1091 228 461 229 718 230 780 231 836 232 383 233 1093 234 292 235 1542 236 283 237 538 238 336 239 1185 240 613 241 383 242 476 243 883 244 473 245 1375 246 363 247 375 248 500 249 972 250 271 251 1293 252 291 253 852 254 352 255 516 256 243 257 537 258 547 259 594 260 145 261 457 262 729 263 589 264 484 265 477 266 172 267 547 268 386 269 407 270 156 271 550 272 501 273 444 274 1288 275 442 276 111 277 658 278 261 279 436 280 109 281 460 282 577 283 264 284 112 285 600 286 115 287 656 288 103 289 215 290 227 291 485 292 108 293 228 294 159 295 516 296 161 297 777 298 127 299 173 300 556 301 265 302 108 303 320 304 69 305 512 306 134 307 129 308 127 309 267 310 204 311 194 312 87 313 267 314 277 315 218 316 103 317 188 318 205 319 184 320 124 321 212 322 29 323 432 324 122 325 145 326 390 327 159 328 16 329 247 330 133 331 146 332 75 333 231 334 198 335 113 336 93 337 215 338 76 339 192 340 41 341 203 342 103 343 115 344 77 345 145 346 22 347 177 348 155 349 275 350 60 351 65 352 287 353 116 354 81 355 66 356 95 357 242 358 30 359 84 360 90 361 66 362 74 363 118 364 9 365 111 366 123 367 69 368 76 369 116 370 135 371 100 372 78 373 85 374 45 375 232 376 23 377 91 378 124 379 39 380 39 381 89 382 24 383 86 384 74 385 102 386 48 387 62 388 15 389 73 390 63 391 54 392 74 393 135 394 15 395 68 396 82 397 27 398 29 399 93 400 25 401 83 402 86 403 38 404 69 405 92 406 13 407 45 408 73 409 78 410 37 411 52 412 12 413 54 414 66 415 26 416 29 417 51 418 18 419 30 420 42 421 39 422 52 423 61 424 6 425 63 426 57 427 66 428 65 429 39 430 28 431 37 432 87 433 29 434 27 435 97 436 9 437 42 438 69 439 16 440 32 441 57 442 11 443 51 444 55 445 80 446 33 447 37 448 19 449 23 450 60 451 19 452 22 453 64 454 8 455 36 456 47 457 27 458 15 459 30 460 13 461 42 462 44 463 29 464 49 465 47 466 13 467 21 468 67 469 11 470 19 471 86 472 5 473 37 474 39 475 18 476 32 477 46 478 5 479 32 480 41 481 23 482 27 483 44 484 7 485 25 486 47 487 12 488 15 489 24 490 6 491 21 492 44 493 29 494 22 495 30 496 2 497 41 498 32 499 14 500 38 501 14 502 12 503 18 504 73 505 20 506 23 507 25 508 7 509 16 510 47 511 7 512 21 513 25 514 1 515 27 516 36 517 22 518 20 519 36 520 10 521 19 522 47 523 15 524 14 525 26 526 6 527 13 528 25 529 20 530 19 531 18 532 1 533 31 534 27 535 22 536 15 537 16 538 10 539 14 540 61 541 9 542 12 543 28 544 1 545 23 546 23 547 10 548 12 549 20 550 4 551 17 552 37 553 21 554 21 555 32 556 5 557 8 558 22 559 3 560 18 561 11 562 3 563 13 564 23 565 27 566 11 567 17 568 3 569 20 570 16 571 18 572 12 573 12 574 15 575 15 576 16 577 2 578 18 579 13 580 1 581 14 582 12 583 8 584 16 585 12 586 4 587 6 588 38 589 9 590 26 591 25 592 4 593 15 594 11 595 9 596 4 597 28 598 3 599 0 600 18 601 10 602 12 603 17 604 1 605 8 606 8 607 6 608 8 609 16 610 4 611 7 612 24 613 1 614 8 615 16 616 2 617 9 618 16 619 4 620 6 621 14 622 0 623 7 624 24 625 32 626 20 627 14 628 3 629 1 630 12 631 0 632 5 633 11 634 2 635 7 636 6 637 6 638 25 639 10 640 0 641 6 642 11 643 11 644 10 645 22 646 2 647 8 648 14 649 4 650 10 651 8 652 1 653 13 654 9 655 2 656 2 657 7 658 0 659 6 660 23 661 10 662 9 663 8 664 2 665 10 666 18 667 3 668 3 669 16 670 4 671 2 672 4 673 9 674 3 675 8 676 0 677 4 678 10 679 4 680 9 681 8 682 3 683 4 684 12 685 2 686 4 687 5 688 2 689 5 690 10 691 1 692 1 693 6 694 0 695 6 696 22 697 2 698 12 699 2 700 5 701 6 702 14 703 1 704 1 705 20 706 0 707 2 708 5 709 2 710 8 711 4 712 0 713 4 714 4 715 9 716 7 717 4 718 0 719 5 720 15 721 2 722 5 723 3 724 0 725 12 726 3 727 1 728 4 729 9 730 2 731 5 732 5 733 9 734 8 735 5 736 2 737 1 738 16 739 1 740 0 741 11 742 5 743 1 744 7 745 7 746 5 747 0 748 0 749 2 750 6 751 0 752 2 753 12 754 1 755 4 756 6 757 2 758 0 759 5 760 0 761 1 762 3 763 1 764 2 765 4 766 0 767 3 768 9 769 2 770 9 771 2 772 0 773 3 774 13 775 0 776 0 777 2 778 2 779 0 780 3 781 2 782 7 783 5 784 0 785 4 786 3 787 1 788 3 789 3 790 1 791 4 792 5 793 1 794 1 795 0 796 0 797 2 798 2 799 1 800 2 801 1 802 0 803 5 804 4 805 6 806 3 807 1 808 0 809 0 810 8 811 0 812 1 813 9 814 1 815 2 816 3 817 0 818 2 819 0 820 0 821 1 822 5 823 0 824 1 825 11 826 8 827 1 828 7 829 0 830 0 831 0 832 0 833 1 834 0 835 4 836 0 837 0 838 0 839 0 840 6 841 1 842 3 843 1 844 0 845 3 846 4 847 0 848 0 849 2 850 0 851 0 852 2 853 4 854 0 855 3 856 0 857 2 858 5 859 0 860 1 861 2 862 1 863 5 864 1 865 0 866 1 867 0 868 0 869 1 870 0 871 2 872 0 873 1 874 0 875 2 876 3 877 2 878 2 879 0 880 1 881 0 882 2 883 0 884 0 885 13 886 0 887 0 888 0 889 0 890 2 891 2 892 0 893 1 894 3 895 0 896 2 897 4 898 0 899 0 900 4 901 1 902 0 903 1 904 0 905 3 906 0 907 0 908 0 909 1 910 0 911 0 912 3 913 0 914 3 915 2 916 0 917 2 918 2 919 0 920 0 921 1 922 0 923 0 924 0 925 5 926 2 927 1 928 0 929 1 930 4 931 0 932 0 933 3 934 1 935 3 936 0 937 0 938 1 939 0 940 0 941 1 942 1 943 4 944 0 945 0 946 0 947 0 948 1 949 0 950 2 951 1 952 0 953 2 954 1 955 0 956 0 957 0 958 0 959 0 960 0 961 1 962 1 963 0 964 0 965 1 966 0 967 0 968 1 969 3 970 0 971 0 972 0 973 1 974 0 975 0 976 0 977 1 978 0 979 0 980 1 981 1 982 0 983 0 984 2 985 1 986 0 987 3 988 1 989 1 990 2 991 0 992 0 993 3 994 0 995 0 996 0 997 0 998 0 999 0 1000 0
51: Average symbolic conclusion length is 66828686/308975 ≈ 216.29. (Median: 196)
There are 115321 minimal D-proofs with conclusions of even symbolic length, and there are 193654 minimal D-proofs with conclusions of odd symbolic length. [115321/308975 ≈ 37.32% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 1 20 0 21 3 22 0 23 0 24 0 25 1 26 1 27 2 28 0 29 1 30 0 31 6 32 0 33 3 34 2 35 5 36 0 37 7 38 1 39 19 40 5 41 10 42 2 43 16 44 6 45 47 46 4 47 42 48 9 49 50 50 12 51 45 52 9 53 65 54 5 55 70 56 11 57 67 58 11 59 58 60 16 61 68 62 34 63 80 64 39 65 95 66 57 67 110 68 79 69 142 70 79 71 188 72 75 73 297 74 69 75 298 76 95 77 310 78 106 79 306 80 112 81 296 82 145 83 360 84 166 85 419 86 189 87 564 88 208 89 539 90 207 91 706 92 197 93 710 94 200 95 692 96 243 97 744 98 333 99 763 100 343 101 804 102 444 103 879 104 405 105 984 106 448 107 1083 108 388 109 1039 110 538 111 1379 112 585 113 1237 114 526 115 1321 116 729 117 1287 118 687 119 1207 120 844 121 1440 122 909 123 1352 124 837 125 1537 126 791 127 1693 128 794 129 1847 130 929 131 1770 132 920 133 2006 134 1039 135 1915 136 1135 137 1608 138 852 139 1827 140 1460 141 1876 142 957 143 1922 144 1080 145 2484 146 938 147 2155 148 754 149 2129 150 1132 151 2081 152 1104 153 2374 154 1493 155 2179 156 1248 157 1909 158 1626 159 2270 160 1215 161 1873 162 1148 163 3356 164 1221 165 2689 166 1110 167 2233 168 1557 169 2254 170 1601 171 1924 172 1162 173 2197 174 1712 175 2193 176 1863 177 2141 178 1855 179 2042 180 957 181 2489 182 1404 183 2468 184 761 185 2264 186 1901 187 2248 188 2526 189 1718 190 813 191 2223 192 2100 193 2258 194 1679 195 1880 196 1568 197 2424 198 1197 199 2326 200 624 201 2604 202 966 203 1605 204 742 205 2458 206 1555 207 1605 208 1297 209 1814 210 1456 211 2660 212 688 213 1344 214 976 215 3011 216 897 217 3296 218 874 219 1747 220 1009 221 1652 222 1386 223 1134 224 991 225 1660 226 782 227 1278 228 1834 229 1575 230 1847 231 1435 232 483 233 1792 234 1194 235 1385 236 383 237 1306 238 1567 239 1282 240 2832 241 1172 242 302 243 1415 244 950 245 1490 246 658 247 1016 248 1168 249 1137 250 495 251 1507 252 434 253 2134 254 411 255 701 256 526 257 1663 258 808 259 572 260 637 261 1244 262 628 263 1899 264 532 265 521 266 798 267 1228 268 381 269 1725 270 440 271 1187 272 491 273 737 274 354 275 733 276 772 277 810 278 222 279 658 280 968 281 790 282 669 283 620 284 259 285 776 286 518 287 530 288 243 289 836 290 649 291 587 292 1641 293 633 294 185 295 926 296 342 297 603 298 164 299 606 300 820 301 344 302 170 303 786 304 176 305 904 306 168 307 336 308 309 309 665 310 165 311 353 312 209 313 683 314 242 315 1014 316 172 317 257 318 816 319 362 320 153 321 415 322 125 323 680 324 191 325 212 326 203 327 391 328 265 329 296 330 156 331 391 332 357 333 314 334 155 335 299 336 335 337 276 338 158 339 323 340 68 341 600 342 187 343 225 344 483 345 249 346 37 347 336 348 193 349 182 350 132 351 338 352 246 353 178 354 135 355 278 356 100 357 295 358 76 359 253 360 150 361 156 362 133 363 218 364 33 365 281 366 217 367 340 368 97 369 168 370 360 371 162 372 117 373 124 374 142 375 328 376 49 377 184 378 128 379 91 380 132 381 141 382 23 383 162 384 171 385 107 386 112 387 164 388 182 389 141 390 144 391 118 392 88 393 336 394 53 395 125 396 179 397 66 398 107 399 144 400 47 401 106 402 143 403 124 404 64 405 100 406 32 407 107 408 120 409 90 410 131 411 206 412 25 413 125 414 121 415 68 416 55 417 160 418 37 419 139 420 149 421 58 422 109 423 142 424 24 425 92 426 109 427 109 428 47 429 103 430 47 431 83 432 120 433 47 434 60 435 104 436 28 437 73 438 124 439 79 440 81 441 96 442 37 443 86 444 66 445 111 446 97 447 77 448 37 449 71 450 115 451 47 452 45 453 125 454 31 455 79 456 115 457 38 458 52 459 102 460 27 461 79 462 101 463 96 464 35 465 91 466 29 467 69 468 102 469 29 470 38 471 77 472 18 473 54 474 75 475 60 476 22 477 72 478 27 479 58 480 78 481 53 482 83 483 65 484 23 485 63 486 116 487 30 488 29 489 120 490 10 491 65 492 73 493 27 494 54 495 95 496 10 497 62 498 79 499 49 500 41 501 49 502 39 503 28 504 62 505 32 506 31 507 55 508 13 509 29 510 72 511 39 512 24 513 45 514 8 515 61 516 51 517 32 518 79 519 46 520 28 521 33 522 85 523 37 524 29 525 120 526 16 527 29 528 63 529 12 530 32 531 53 532 6 533 63 534 54 535 41 536 31 537 55 538 20 539 24 540 79 541 16 542 24 543 41 544 6 545 42 546 53 547 28 548 25 549 33 550 2 551 33 552 36 553 27 554 45 555 47 556 11 557 26 558 95 559 17 560 26 561 33 562 6 563 37 564 47 565 25 566 27 567 27 568 5 569 32 570 49 571 25 572 25 573 49 574 16 575 26 576 51 577 7 578 32 579 17 580 7 581 16 582 37 583 27 584 15 585 41 586 7 587 35 588 36 589 19 590 26 591 17 592 21 593 25 594 80 595 16 596 25 597 27 598 7 599 16 600 52 601 10 602 29 603 33 604 6 605 19 606 50 607 14 608 24 609 36 610 11 611 18 612 22 613 17 614 18 615 34 616 4 617 18 618 42 619 18 620 21 621 15 622 2 623 25 624 12 625 29 626 16 627 23 628 11 629 12 630 20 631 5 632 24 633 33 634 5 635 29 636 21 637 8 638 11 639 27 640 4 641 8 642 53 643 28 644 23 645 37 646 11 647 10 648 19 649 2 650 13 651 28 652 5 653 14 654 19 655 29 656 31 657 20 658 1 659 11 660 14 661 12 662 21 663 30 664 2 665 21 666 34 667 5 668 17 669 6 670 5 671 16 672 20 673 5 674 6 675 15 676 0 677 9 678 27 679 17 680 22 681 24 682 10 683 11 684 13 685 12 686 9 687 20 688 3 689 6 690 10 691 10 692 6 693 18 694 5 695 9 696 12 697 6 698 16 699 16 700 6 701 16 702 24 703 4 704 7 705 29 706 2 707 5 708 17 709 5 710 16 711 9 712 1 713 8 714 37 715 39 716 18 717 8 718 5 719 10 720 25 721 2 722 8 723 21 724 1 725 6 726 9 727 3 728 10 729 6 730 3 731 7 732 10 733 16 734 11 735 17 736 4 737 6 738 11 739 4 740 5 741 4 742 6 743 16 744 6 745 3 746 6 747 15 748 2 749 7 750 23 751 11 752 9 753 11 754 4 755 14 756 17 757 1 758 1 759 24 760 5 761 1 762 8 763 6 764 6 765 8 766 0 767 2 768 7 769 0 770 5 771 23 772 4 773 5 774 19 775 2 776 2 777 8 778 2 779 4 780 8 781 1 782 2 783 9 784 0 785 8 786 15 787 4 788 13 789 3 790 1 791 4 792 14 793 0 794 4 795 13 796 2 797 2 798 6 799 2 800 16 801 4 802 0 803 8 804 4 805 7 806 5 807 11 808 1 809 5 810 10 811 1 812 4 813 7 814 7 815 11 816 5 817 3 818 2 819 3 820 0 821 5 822 6 823 10 824 2 825 4 826 1 827 0 828 20 829 3 830 2 831 9 832 1 833 2 834 4 835 8 836 3 837 0 838 0 839 2 840 6 841 2 842 4 843 15 844 8 845 7 846 10 847 0 848 0 849 1 850 0 851 1 852 0 853 3 854 3 855 10 856 0 857 3 858 10 859 0 860 11 861 1 862 1 863 4 864 5 865 0 866 1 867 2 868 0 869 0 870 4 871 4 872 6 873 4 874 3 875 5 876 6 877 2 878 3 879 5 880 1 881 6 882 8 883 2 884 1 885 1 886 2 887 1 888 0 889 2 890 4 891 3 892 0 893 4 894 3 895 9 896 1 897 2 898 1 899 2 900 5 901 0 902 1 903 12 904 0 905 3 906 2 907 0 908 9 909 1 910 0 911 3 912 4 913 0 914 2 915 13 916 0 917 2 918 7 919 2 920 0 921 0 922 2 923 2 924 2 925 6 926 0 927 1 928 0 929 0 930 7 931 0 932 3 933 2 934 0 935 4 936 4 937 0 938 0 939 2 940 0 941 0 942 1 943 5 944 3 945 5 946 0 947 1 948 5 949 0 950 2 951 3 952 2 953 6 954 3 955 0 956 1 957 0 958 0 959 1 960 1 961 4 962 0 963 0 964 0 965 2 966 1 967 1 968 2 969 1 970 8 971 3 972 1 973 2 974 0 975 13 976 1 977 0 978 0 979 1 980 5 981 0 982 1 983 0 984 2 985 0 986 2 987 7 988 0 989 0 990 6 991 0 992 0 993 1 994 0 995 4 996 0 997 0 998 2 999 3 1000 0
53: Average symbolic conclusion length is 114507092/506415 ≈ 226.11. (Median: 204)
There are 192279 minimal D-proofs with conclusions of even symbolic length, and there are 314136 minimal D-proofs with conclusions of odd symbolic length. [192279/506415 ≈ 37.97% 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 0 15 1 16 0 17 0 18 0 19 2 20 0 21 0 22 0 23 1 24 0 25 3 26 0 27 7 28 1 29 4 30 0 31 6 32 0 33 13 34 2 35 14 36 0 37 16 38 2 39 17 40 1 41 17 42 1 43 22 44 4 45 14 46 3 47 13 48 8 49 24 50 14 51 23 52 17 53 54 54 15 55 46 56 28 57 73 58 35 59 127 60 26 61 184 62 45 63 185 64 49 65 168 66 63 67 196 68 61 69 200 70 61 71 272 72 78 73 274 74 70 75 330 76 120 77 385 78 117 79 392 80 156 81 459 82 196 83 456 84 226 85 484 86 297 87 631 88 279 89 648 90 271 91 821 92 251 93 798 94 363 95 847 96 389 97 876 98 440 99 1092 100 539 101 1152 102 567 103 1203 104 620 105 1380 106 725 107 1345 108 618 109 1605 110 639 111 1735 112 655 113 1568 114 729 115 1901 116 910 117 1922 118 917 119 2058 120 1083 121 2003 122 1044 123 2055 124 1143 125 2362 126 960 127 2252 128 1208 129 2956 130 1313 131 2543 132 1159 133 2600 134 1585 135 2573 136 1501 137 2451 138 1706 139 2761 140 2001 141 2691 142 1845 143 2865 144 1673 145 3023 146 1561 147 3265 148 1883 149 3269 150 1710 151 3425 152 2054 153 3408 154 2334 155 2721 156 1556 157 3147 158 2856 159 3252 160 1946 161 3230 162 2044 163 4145 164 1762 165 3831 166 1331 167 3603 168 1913 169 3423 170 1848 171 4012 172 2580 173 3610 174 2180 175 3093 176 2761 177 3833 178 2031 179 2851 180 1888 181 5387 182 2014 183 4518 184 1812 185 3445 186 2470 187 3488 188 2728 189 2981 190 1847 191 3414 192 2619 193 3293 194 3079 195 3221 196 3208 197 3099 198 1483 199 3729 200 2260 201 3818 202 1106 203 3339 204 2943 205 3418 206 4085 207 2582 208 1187 209 3306 210 3119 211 3327 212 2542 213 2767 214 2398 215 3362 216 1756 217 3429 218 1007 219 3950 220 1435 221 2216 222 1107 223 3692 224 2269 225 2309 226 1900 227 2621 228 2139 229 3885 230 1080 231 1843 232 1506 233 4185 234 1309 235 4790 236 1313 237 2565 238 1482 239 2338 240 1894 241 1671 242 1486 243 2383 244 1016 245 1815 246 2629 247 2187 248 2610 249 2063 250 698 251 2451 252 1715 253 1903 254 584 255 1833 256 2155 257 1789 258 4026 259 1696 260 435 261 2116 262 1283 263 2000 264 917 265 1396 266 1752 267 1520 268 641 269 2097 270 665 271 2892 272 581 273 1023 274 846 275 2285 276 1044 277 862 278 858 279 1748 280 823 281 2556 282 765 283 712 284 1241 285 1681 286 544 287 2237 288 648 289 1650 290 719 291 924 292 515 293 1049 294 1077 295 1129 296 327 297 1024 298 1280 299 1058 300 925 301 823 302 435 303 1013 304 664 305 788 306 353 307 1189 308 842 309 876 310 2086 311 852 312 259 313 1280 314 488 315 816 316 233 317 884 318 1140 319 468 320 252 321 1076 322 271 323 1126 324 278 325 563 326 423 327 887 328 237 329 562 330 347 331 928 332 375 333 1332 334 257 335 384 336 1174 337 511 338 237 339 552 340 221 341 932 342 312 343 309 344 292 345 602 346 360 347 446 348 267 349 497 350 469 351 442 352 222 353 439 354 561 355 425 356 222 357 486 358 131 359 797 360 294 361 319 362 605 363 361 364 54 365 534 366 279 367 330 368 186 369 468 370 322 371 292 372 199 373 360 374 166 375 424 376 120 377 429 378 235 379 244 380 212 381 332 382 97 383 398 384 323 385 434 386 170 387 285 388 444 389 276 390 226 391 158 392 187 393 513 394 83 395 274 396 211 397 185 398 223 399 207 400 50 401 236 402 262 403 165 404 171 405 332 406 248 407 203 408 196 409 200 410 123 411 421 412 94 413 215 414 261 415 135 416 178 417 271 418 75 419 176 420 209 421 166 422 134 423 255 424 55 425 186 426 174 427 139 428 175 429 321 430 82 431 172 432 177 433 96 434 136 435 218 436 61 437 200 438 230 439 95 440 144 441 198 442 54 443 134 444 174 445 203 446 110 447 182 448 77 449 140 450 189 451 85 452 146 453 183 454 58 455 160 456 215 457 125 458 117 459 132 460 62 461 139 462 169 463 147 464 130 465 163 466 52 467 122 468 157 469 63 470 93 471 204 472 43 473 136 474 216 475 90 476 79 477 167 478 53 479 110 480 152 481 130 482 88 483 162 484 56 485 155 486 183 487 54 488 65 489 112 490 45 491 101 492 176 493 90 494 50 495 134 496 45 497 103 498 108 499 71 500 128 501 113 502 55 503 99 504 150 505 73 506 54 507 158 508 27 509 95 510 160 511 36 512 89 513 153 514 35 515 126 516 117 517 96 518 58 519 94 520 59 521 91 522 111 523 67 524 49 525 80 526 46 527 59 528 98 529 43 530 53 531 87 532 23 533 111 534 101 535 77 536 92 537 85 538 51 539 52 540 157 541 34 542 56 543 176 544 12 545 92 546 116 547 36 548 51 549 95 550 30 551 76 552 98 553 66 554 61 555 92 556 27 557 41 558 121 559 26 560 48 561 79 562 21 563 67 564 82 565 75 566 47 567 52 568 11 569 64 570 78 571 38 572 82 573 81 574 55 575 67 576 107 577 27 578 40 579 139 580 10 581 54 582 77 583 28 584 30 585 76 586 14 587 55 588 78 589 33 590 57 591 76 592 27 593 36 594 80 595 36 596 34 597 41 598 11 599 35 600 72 601 36 602 36 603 71 604 11 605 69 606 52 607 28 608 55 609 29 610 42 611 34 612 121 613 29 614 46 615 45 616 9 617 39 618 92 619 14 620 41 621 38 622 19 623 35 624 54 625 50 626 41 627 75 628 21 629 30 630 76 631 22 632 27 633 42 634 8 635 47 636 54 637 21 638 31 639 39 640 4 641 46 642 53 643 30 644 19 645 69 646 23 647 26 648 98 649 8 650 39 651 40 652 10 653 41 654 41 655 22 656 21 657 59 658 8 659 11 660 67 661 30 662 30 663 55 664 16 665 34 666 30 667 16 668 36 669 27 670 21 671 18 672 48 673 35 674 38 675 42 676 1 677 31 678 21 679 19 680 42 681 36 682 15 683 24 684 28 685 21 686 37 687 34 688 7 689 21 690 78 691 6 692 16 693 28 694 0 695 21 696 56 697 24 698 29 699 47 700 8 701 19 702 30 703 21 704 17 705 53 706 4 707 18 708 27 709 21 710 22 711 22 712 5 713 8 714 24 715 27 716 25 717 26 718 15 719 17 720 40 721 8 722 23 723 35 724 6 725 31 726 40 727 11 728 18 729 24 730 11 731 13 732 40 733 41 734 31 735 30 736 11 737 18 738 28 739 4 740 15 741 29 742 10 743 22 744 13 745 26 746 13 747 17 748 3 749 13 750 13 751 14 752 15 753 27 754 6 755 37 756 21 757 11 758 10 759 19 760 7 761 17 762 22 763 5 764 11 765 27 766 4 767 11 768 36 769 11 770 19 771 19 772 8 773 17 774 33 775 15 776 2 777 29 778 9 779 2 780 15 781 8 782 24 783 20 784 0 785 14 786 13 787 5 788 10 789 26 790 5 791 5 792 15 793 2 794 13 795 26 796 2 797 5 798 16 799 2 800 8 801 15 802 2 803 13 804 39 805 46 806 17 807 12 808 2 809 12 810 29 811 0 812 4 813 23 814 9 815 6 816 7 817 5 818 18 819 7 820 7 821 10 822 4 823 12 824 7 825 33 826 14 827 8 828 26 829 4 830 6 831 8 832 10 833 16 834 8 835 7 836 3 837 8 838 3 839 5 840 8 841 13 842 12 843 11 844 2 845 14 846 23 847 3 848 4 849 20 850 2 851 2 852 6 853 6 854 4 855 10 856 0 857 4 858 13 859 4 860 8 861 24 862 8 863 11 864 12 865 1 866 10 867 8 868 0 869 4 870 13 871 5 872 3 873 13 874 3 875 8 876 15 877 4 878 14 879 6 880 2 881 7 882 20 883 0 884 0 885 16 886 8 887 4 888 5 889 4 890 17 891 4 892 3 893 7 894 7 895 8 896 2 897 12 898 3 899 11 900 13 901 1 902 5 903 2 904 2 905 13 906 1 907 4 908 4 909 2 910 0 911 7 912 8 913 15 914 3 915 7 916 2 917 3 918 10 919 3 920 1 921 13 922 1 923 4 924 4 925 9 926 12 927 2 928 0 929 5 930 13 931 0 932 2 933 24 934 2 935 10 936 15 937 2 938 1 939 4 940 2 941 2 942 2 943 2 944 0 945 3 946 0 947 1 948 9 949 0 950 16 951 4 952 1 953 6 954 5 955 1 956 1 957 2 958 4 959 2 960 2 961 6 962 7 963 6 964 0 965 5 966 6 967 4 968 1 969 8 970 3 971 7 972 4 973 0 974 3 975 1 976 0 977 1 978 1 979 4 980 3 981 9 982 1 983 4 984 4 985 8 986 5 987 5 988 7 989 8 990 9 991 2 992 1 993 12 994 1 995 4 996 0 997 2 998 6 999 1 1000 2
55: Average symbolic conclusion length is 196095009/830126 ≈ 236.22. (Median: 212)
There are 320221 minimal D-proofs with conclusions of even symbolic length, and there are 509905 minimal D-proofs with conclusions of odd symbolic length. [320221/830126 ≈ 38.57% 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 1 16 0 17 0 18 0 19 2 20 0 21 1 22 0 23 4 24 1 25 4 26 0 27 3 28 1 29 3 30 0 31 4 32 0 33 6 34 0 35 4 36 3 37 7 38 3 39 6 40 3 41 31 42 4 43 22 44 8 45 29 46 11 47 62 48 14 49 81 50 11 51 74 52 26 53 87 54 8 55 103 56 21 57 118 58 14 59 115 60 24 61 102 62 33 63 138 64 62 65 129 66 77 67 160 68 71 69 202 70 127 71 256 72 136 73 317 74 125 75 501 76 149 77 524 78 153 79 591 80 180 81 571 82 254 83 534 84 278 85 619 86 371 87 797 88 342 89 959 90 407 91 1102 92 373 93 1178 94 504 95 1328 96 443 97 1293 98 504 99 1462 100 660 101 1380 102 690 103 1500 104 928 105 1801 106 923 107 1809 108 859 109 2094 110 872 111 2072 112 1066 113 2409 114 1092 115 2454 116 1190 117 2715 118 1393 119 2690 120 1439 121 2563 122 1532 123 2853 124 1998 125 2901 126 1629 127 3283 128 1747 129 4002 130 1680 131 3564 132 1720 133 3953 134 2047 135 3995 136 2094 137 4200 138 2361 139 3797 140 2297 141 3936 142 2582 143 4472 144 2179 145 4106 146 2490 147 5753 148 2659 149 5011 150 2313 151 4796 152 3175 153 4946 154 3015 155 4553 156 3113 157 5052 158 3888 159 4762 160 3620 161 4816 162 3304 163 5119 164 2794 165 5568 166 3478 167 5662 168 2901 169 5740 170 3758 171 5782 172 4420 173 4379 174 2669 175 5171 176 5153 177 5472 178 3656 179 5166 180 3618 181 6586 182 3103 183 6277 184 2210 185 5951 186 3106 187 5264 188 2952 189 6577 190 4212 191 5782 192 3609 193 4918 194 4497 195 6085 196 3185 197 4302 198 3010 199 8312 200 3199 201 7384 202 2868 203 5152 204 3762 205 5426 206 4384 207 4381 208 2858 209 5140 210 3863 211 4767 212 4845 213 4881 214 5293 215 4565 216 2226 217 5535 218 3571 219 5558 220 1588 221 4890 222 4466 223 4857 224 6393 225 3930 226 1689 227 4923 228 4487 229 4843 230 3753 231 3899 232 3588 233 4721 234 2529 235 4869 236 1572 237 6058 238 2104 239 3087 240 1649 241 5482 242 3257 243 3240 244 2724 245 3770 246 3017 247 5561 248 1636 249 2650 250 2320 251 5630 252 1900 253 6891 254 1921 255 3614 256 2154 257 3255 258 2562 259 2443 260 2221 261 3491 262 1360 263 2535 264 3693 265 3014 266 3633 267 2801 268 1015 269 3334 270 2484 271 2479 272 873 273 2723 274 2948 275 2546 276 5608 277 2416 278 667 279 3098 280 1703 281 2675 282 1336 283 2050 284 2577 285 2148 286 862 287 2887 288 1023 289 3940 290 860 291 1390 292 1284 293 3130 294 1375 295 1299 296 1140 297 2515 298 1098 299 3466 300 1086 301 985 302 1971 303 2205 304 737 305 2980 306 928 307 2314 308 1000 309 1322 310 772 311 1467 312 1458 313 1566 314 505 315 1517 316 1646 317 1438 318 1291 319 1101 320 705 321 1457 322 893 323 1095 324 532 325 1744 326 1128 327 1187 328 2649 329 1252 330 418 331 1777 332 700 333 1186 334 338 335 1287 336 1575 337 688 338 407 339 1448 340 405 341 1522 342 503 343 850 344 642 345 1306 346 363 347 803 348 517 349 1239 350 609 351 1744 352 372 353 596 354 1657 355 705 356 324 357 857 358 344 359 1227 360 467 361 523 362 463 363 816 364 478 365 737 366 397 367 705 368 623 369 696 370 347 371 625 372 838 373 600 374 344 375 715 376 209 377 1156 378 460 379 452 380 768 381 603 382 158 383 765 384 453 385 502 386 302 387 690 388 420 389 473 390 415 391 501 392 258 393 648 394 211 395 606 396 351 397 376 398 346 399 473 400 155 401 568 402 539 403 630 404 267 405 428 406 576 407 467 408 414 409 257 410 318 411 721 412 151 413 430 414 382 415 318 416 303 417 368 418 115 419 435 420 378 421 227 422 271 423 462 424 314 425 359 426 284 427 298 428 193 429 600 430 209 431 304 432 391 433 246 434 285 435 414 436 124 437 346 438 368 439 257 440 229 441 397 442 120 443 338 444 297 445 287 446 241 447 520 448 104 449 336 450 338 451 189 452 220 453 330 454 113 455 337 456 353 457 160 458 253 459 360 460 93 461 212 462 282 463 263 464 143 465 345 466 112 467 210 468 284 469 132 470 287 471 329 472 96 473 237 474 307 475 211 476 179 477 392 478 125 479 214 480 234 481 214 482 193 483 274 484 96 485 288 486 228 487 121 488 187 489 272 490 91 491 211 492 329 493 134 494 144 495 293 496 86 497 185 498 265 499 195 500 159 501 254 502 127 503 192 504 272 505 111 506 197 507 220 508 86 509 159 510 348 511 142 512 84 513 184 514 71 515 174 516 232 517 132 518 204 519 189 520 104 521 172 522 226 523 109 524 93 525 301 526 64 527 182 528 267 529 64 530 139 531 224 532 66 533 202 534 183 535 148 536 72 537 205 538 98 539 153 540 227 541 79 542 100 543 136 544 59 545 184 546 268 547 88 548 78 549 144 550 52 551 137 552 127 553 130 554 185 555 180 556 79 557 116 558 217 559 77 560 95 561 208 562 53 563 139 564 184 565 83 566 92 567 147 568 56 569 139 570 189 571 97 572 64 573 155 574 53 575 159 576 192 577 45 578 80 579 103 580 45 581 80 582 138 583 88 584 68 585 163 586 39 587 98 588 129 589 63 590 128 591 117 592 68 593 88 594 191 595 72 596 58 597 226 598 38 599 103 600 166 601 34 602 72 603 140 604 17 605 139 606 149 607 74 608 72 609 95 610 57 611 64 612 121 613 59 614 64 615 101 616 31 617 73 618 134 619 50 620 67 621 93 622 42 623 106 624 96 625 85 626 93 627 84 628 64 629 59 630 157 631 42 632 68 633 184 634 18 635 116 636 124 637 29 638 72 639 77 640 45 641 63 642 112 643 34 644 67 645 128 646 73 647 50 648 111 649 26 650 46 651 68 652 16 653 87 654 102 655 80 656 41 657 94 658 22 659 73 660 75 661 37 662 72 663 93 664 35 665 77 666 157 667 30 668 60 669 46 670 22 671 59 672 86 673 40 674 38 675 111 676 10 677 30 678 93 679 46 680 47 681 86 682 45 683 49 684 74 685 53 686 54 687 41 688 15 689 29 690 69 691 36 692 46 693 71 694 6 695 62 696 59 697 27 698 75 699 55 700 37 701 36 702 133 703 45 704 51 705 69 706 9 707 30 708 91 709 18 710 49 711 75 712 8 713 41 714 80 715 68 716 35 717 87 718 24 719 29 720 64 721 26 722 40 723 61 724 10 725 59 726 67 727 29 728 24 729 42 730 22 731 26 732 42 733 32 734 38 735 83 736 25 737 39 738 39 739 12 740 49 741 51 742 16 743 59 744 49 745 39 746 39 747 55 748 14 749 25 750 89 751 46 752 37 753 56 754 14 755 56 756 37 757 10 758 29 759 51 760 9 761 26 762 52 763 28 764 25 765 52 766 6 767 25 768 23 769 16 770 42 771 50 772 10 773 47 774 41 775 26 776 23 777 27 778 11 779 24 780 115 781 7 782 17 783 35 784 6 785 30 786 48 787 20 788 26 789 42 790 20 791 17 792 35 793 24 794 23 795 51 796 10 797 22 798 27 799 14 800 39 801 21 802 2 803 18 804 22 805 25 806 21 807 43 808 7 809 24 810 33 811 3 812 17 813 54 814 22 815 35 816 26 817 10 818 8 819 21 820 13 821 16 822 53 823 45 824 19 825 23 826 16 827 17 828 43 829 4 830 11 831 31 832 14 833 18 834 24 835 37 836 24 837 20 838 7 839 16 840 9 841 18 842 28 843 41 844 8 845 32 846 26 847 7 848 9 849 13 850 13 851 20 852 16 853 7 854 19 855 33 856 3 857 9 858 35 859 15 860 24 861 17 862 8 863 24 864 24 865 21 866 15 867 42 868 2 869 10 870 11 871 8 872 8 873 26 874 7 875 15 876 13 877 5 878 11 879 37 880 12 881 16 882 34 883 5 884 10 885 34 886 9 887 9 888 22 889 4 890 7 891 21 892 4 893 12 894 16 895 56 896 18 897 11 898 7 899 10 900 25 901 4 902 3 903 14 904 9 905 13 906 18 907 10 908 18 909 3 910 9 911 14 912 10 913 13 914 9 915 34 916 6 917 18 918 15 919 4 920 8 921 12 922 12 923 17 924 13 925 10 926 11 927 10 928 1 929 9 930 15 931 12 932 3 933 14 934 1 935 24 936 37 937 4 938 8 939 18 940 3 941 4 942 7 943 5 944 18 945 15 946 10 947 12 948 14 949 1 950 11 951 26 952 2 953 11 954 27 955 5 956 0 957 8 958 12 959 2 960 9 961 4 962 3 963 9 964 2 965 8 966 16 967 3 968 16 969 9 970 9 971 7 972 12 973 2 974 2 975 33 976 5 977 5 978 11 979 5 980 24 981 5 982 1 983 6 984 11 985 11 986 7 987 22 988 6 989 11 990 21 991 0 992 7 993 2 994 0 995 15 996 2 997 9 998 4 999 11 1000 1
57: Average symbolic conclusion length is 335555301/1360461 ≈ 246.65. (Median: 219)
There are 532468 minimal D-proofs with conclusions of even symbolic length, and there are 827993 minimal D-proofs with conclusions of odd symbolic length. [532468/1360461 ≈ 39.14% 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 1 14 0 15 0 16 0 17 2 18 0 19 1 20 0 21 1 22 0 23 3 24 1 25 1 26 0 27 0 28 0 29 12 30 1 31 6 32 1 33 6 34 1 35 16 36 2 37 24 38 6 39 24 40 2 41 34 42 6 43 40 44 5 45 30 46 8 47 31 48 6 49 28 50 10 51 50 52 25 53 40 54 30 55 74 56 26 57 100 58 56 59 120 60 60 61 180 62 61 63 295 64 77 65 308 66 117 67 319 68 87 69 306 70 130 71 359 72 94 73 419 74 153 75 508 76 143 77 551 78 193 79 662 80 263 81 725 82 300 83 778 84 353 85 825 86 388 87 937 88 488 89 1123 90 488 91 1270 92 479 93 1515 94 564 95 1531 96 596 97 1600 98 719 99 1769 100 990 101 1935 102 983 103 2139 104 1298 105 2475 106 1197 107 2645 108 1307 109 2821 110 1166 111 2958 112 1563 113 3436 114 1457 115 3020 116 1551 117 3798 118 1894 119 3768 120 1960 121 3769 122 2418 123 4255 124 2528 125 4203 126 2310 127 4611 128 2329 129 4880 130 2534 131 5292 132 2689 133 5207 134 2774 135 5597 136 3104 137 5670 138 3320 139 5168 140 3331 141 5696 142 4672 143 5924 144 3623 145 6495 146 3881 147 7824 148 3559 149 6855 150 3500 151 7315 152 4102 153 7362 154 4216 155 7852 156 4687 157 6996 158 4536 159 6939 160 5273 161 7901 162 4484 163 7011 164 4698 165 10565 166 4989 167 9213 168 4265 169 8271 170 5836 171 8736 172 5618 173 7921 174 5319 175 8449 176 6894 177 8088 178 6602 179 7879 180 6199 181 8394 182 4726 183 9044 184 5978 185 9533 186 4674 187 9201 188 6466 189 9320 190 7881 191 6981 192 4354 193 8451 194 8733 195 8668 196 6426 197 8070 198 6110 199 10036 200 5160 201 10057 202 3557 203 9542 204 4892 205 7978 206 4544 207 10396 208 6615 209 8970 210 5766 211 7347 212 7017 213 9620 214 4868 215 6359 216 4672 217 12557 218 4880 219 11731 220 4431 221 7605 222 5643 223 7971 224 6744 225 6538 226 4374 227 7696 228 5516 229 6852 230 7454 231 7078 232 8341 233 6600 234 3287 235 7971 236 5523 237 8062 238 2325 239 6980 240 6644 241 7009 242 9761 243 5770 244 2336 245 7163 246 6339 247 6966 248 5421 249 5633 250 5357 251 6532 252 3534 253 6971 254 2455 255 8892 256 3016 257 4339 258 2513 259 7817 260 4544 261 4626 262 3804 263 5528 264 4199 265 7876 266 2482 267 3664 268 3501 269 7626 270 2758 271 9601 272 2798 273 5348 274 3126 275 4474 276 3458 277 3708 278 3274 279 4949 280 1824 281 3595 282 5142 283 4091 284 4971 285 3973 286 1485 287 4538 288 3512 289 3474 290 1305 291 3769 292 4023 293 3612 294 7698 295 3375 296 1025 297 4673 298 2290 299 3668 300 1915 301 2889 302 3775 303 2834 304 1143 305 3956 306 1602 307 5179 308 1203 309 2099 310 1913 311 4256 312 1821 313 1967 314 1563 315 3561 316 1480 317 4725 318 1571 319 1472 320 3008 321 3017 322 1046 323 3897 324 1327 325 3277 326 1429 327 1803 328 1122 329 2149 330 1996 331 2257 332 777 333 2285 334 2165 335 2054 336 1804 337 1563 338 1164 339 2072 340 1203 341 1617 342 903 343 2462 344 1482 345 1835 346 3343 347 1763 348 681 349 2434 350 1043 351 1659 352 498 353 1819 354 2195 355 1020 356 636 357 2124 358 631 359 1990 360 803 361 1277 362 922 363 1706 364 535 365 1293 366 803 367 1775 368 935 369 2405 370 563 371 976 372 2302 373 1045 374 568 375 1294 376 530 377 1747 378 748 379 805 380 697 381 1276 382 735 383 1085 384 610 385 995 386 897 387 1025 388 478 389 971 390 1331 391 810 392 521 393 1161 394 341 395 1572 396 741 397 829 398 1119 399 855 400 306 401 1076 402 733 403 732 404 504 405 1128 406 594 407 734 408 651 409 722 410 431 411 852 412 317 413 981 414 583 415 628 416 516 417 803 418 296 419 886 420 749 421 809 422 475 423 737 424 730 425 812 426 642 427 443 428 449 429 1024 430 294 431 599 432 607 433 471 434 456 435 690 436 217 437 699 438 677 439 443 440 422 441 701 442 474 443 663 444 567 445 515 446 335 447 858 448 310 449 514 450 611 451 384 452 453 453 651 454 222 455 623 456 587 457 405 458 394 459 550 460 204 461 497 462 660 463 401 464 354 465 899 466 174 467 505 468 568 469 325 470 389 471 474 472 164 473 638 474 531 475 346 476 351 477 564 478 155 479 339 480 404 481 381 482 274 483 544 484 200 485 530 486 476 487 247 488 410 489 499 490 216 491 446 492 500 493 306 494 306 495 633 496 174 497 385 498 420 499 295 500 288 501 541 502 204 503 392 504 409 505 291 506 307 507 393 508 138 509 301 510 554 511 179 512 281 513 527 514 139 515 333 516 348 517 342 518 226 519 386 520 197 521 288 522 438 523 196 524 327 525 463 526 174 527 317 528 473 529 192 530 196 531 533 532 114 533 333 534 378 535 254 536 266 537 373 538 157 539 278 540 349 541 132 542 249 543 422 544 98 545 315 546 420 547 166 548 220 549 330 550 166 551 275 552 311 553 248 554 158 555 396 556 157 557 249 558 341 559 128 560 270 561 259 562 139 563 267 564 435 565 218 566 159 567 212 568 82 569 228 570 333 571 171 572 251 573 291 574 136 575 269 576 300 577 135 578 191 579 334 580 98 581 199 582 372 583 127 584 136 585 290 586 100 587 199 588 286 589 153 590 135 591 258 592 99 593 264 594 350 595 125 596 112 597 191 598 96 599 169 600 395 601 120 602 134 603 260 604 74 605 195 606 203 607 107 608 181 609 199 610 164 611 159 612 271 613 106 614 100 615 321 616 77 617 183 618 282 619 61 620 115 621 177 622 77 623 211 624 230 625 169 626 141 627 198 628 78 629 165 630 236 631 81 632 112 633 133 634 68 635 198 636 176 637 69 638 124 639 191 640 70 641 183 642 189 643 116 644 127 645 200 646 105 647 111 648 270 649 61 650 139 651 277 652 27 653 191 654 216 655 95 656 101 657 149 658 89 659 100 660 197 661 76 662 110 663 186 664 85 665 159 666 176 667 60 668 76 669 133 670 94 671 94 672 182 673 97 674 66 675 187 676 27 677 129 678 160 679 56 680 119 681 159 682 73 683 97 684 191 685 87 686 94 687 224 688 32 689 93 690 176 691 43 692 72 693 170 694 38 695 118 696 144 697 72 698 98 699 136 700 78 701 87 702 122 703 94 704 66 705 98 706 26 707 87 708 141 709 69 710 122 711 124 712 23 713 91 714 94 715 99 716 117 717 103 718 111 719 63 720 214 721 53 722 92 723 106 724 18 725 145 726 160 727 34 728 55 729 107 730 55 731 81 732 100 733 54 734 63 735 163 736 38 737 73 738 136 739 58 740 64 741 77 742 28 743 91 744 85 745 99 746 41 747 85 748 18 749 57 750 121 751 34 752 54 753 112 754 39 755 105 756 153 757 33 758 73 759 87 760 21 761 92 762 89 763 50 764 62 765 169 766 21 767 43 768 114 769 52 770 61 771 88 772 25 773 70 774 67 775 54 776 44 777 59 778 18 779 44 780 103 781 36 782 65 783 72 784 9 785 91 786 54 787 32 788 64 789 63 790 51 791 51 792 40 793 49 794 64 795 78 796 15 797 36 798 131 799 20 800 30 801 62 802 44 803 42 804 94 805 68 806 44 807 88 808 23 809 40 810 100 811 29 812 32 813 90 814 21 815 61 816 51 817 29 818 49 819 52 820 13 821 28 822 57 823 37 824 26 825 118 826 29 827 45 828 65 829 7 830 42 831 52 832 16 833 54 834 92 835 42 836 18 837 38 838 17 839 21 840 76 841 51 842 45 843 68 844 21 845 64 846 48 847 12 848 36 849 48 850 19 851 22 852 34 853 39 854 30 855 71 856 11 857 38 858 36 859 21 860 56 861 52 862 23 863 60 864 44 865 28 866 29 867 42 868 21 869 48 870 112 871 8 872 28 873 48 874 14 875 29 876 54 877 25 878 34 879 37 880 13 881 36 882 58 883 36 884 16 885 68 886 13 887 28 888 30 889 16 890 34 891 29 892 10 893 24 894 25 895 36 896 14 897 56 898 18 899 20 900 32 901 10 902 20 903 47 904 7 905 55 906 42 907 13 908 15 909 33 910 21 911 20 912 46 913 56 914 31 915 34 916 12 917 29 918 32 919 7 920 9 921 44 922 19 923 24 924 23 925 52 926 45 927 20 928 9 929 19 930 28 931 10 932 16 933 52 934 8 935 50 936 36 937 9 938 28 939 20 940 22 941 20 942 25 943 8 944 14 945 24 946 3 947 16 948 17 949 16 950 23 951 24 952 8 953 30 954 41 955 28 956 7 957 25 958 26 959 6 960 20 961 10 962 22 963 34 964 11 965 22 966 18 967 4 968 13 969 38 970 19 971 15 972 34 973 11 974 4 975 46 976 12 977 6 978 28 979 4 980 8 981 20 982 11 983 10 984 24 985 69 986 41 987 20 988 9 989 19 990 38 991 2 992 5 993 24 994 5 995 16 996 14 997 16 998 29 999 7 1000 15
59: Average symbolic conclusion length is 573728848/2229126 ≈ 257.38. (Median: 227)
There are 884236 minimal D-proofs with conclusions of even symbolic length, and there are 1344890 minimal D-proofs with conclusions of odd symbolic length. [884236/2229126 ≈ 39.67% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 1 12 0 13 0 14 0 15 1 16 0 17 4 18 0 19 0 20 0 21 1 22 0 23 1 24 0 25 5 26 0 27 8 28 1 29 3 30 1 31 10 32 2 33 5 34 0 35 8 36 2 37 11 38 2 39 10 40 6 41 11 42 6 43 34 44 7 45 46 46 9 47 45 48 20 49 83 50 19 51 121 52 24 53 128 54 31 55 152 56 40 57 153 58 21 59 190 60 47 61 201 62 38 63 198 64 48 65 222 66 93 67 263 68 151 69 285 70 162 71 365 72 203 73 455 74 237 75 570 76 283 77 788 78 257 79 931 80 316 81 995 82 355 83 979 84 486 85 978 86 477 87 1130 88 719 89 1426 90 610 91 1549 92 795 93 2066 94 785 95 2087 96 823 97 2328 98 972 99 2534 100 1066 101 2758 102 1239 103 2488 104 1429 105 2986 106 1550 107 3433 108 1729 109 3640 110 1679 111 4000 112 1896 113 4276 114 1893 115 4456 116 2125 117 5243 118 2744 119 5232 120 2678 121 5274 122 3353 123 5599 124 3187 125 5851 126 3582 127 6339 128 3193 129 6469 130 4104 131 8035 132 4000 133 7244 134 3851 135 8329 136 4544 137 8292 138 4657 139 7757 140 5377 141 8494 142 5969 143 8476 144 5369 145 9049 146 5372 147 9601 148 5474 149 10340 150 5962 151 10416 152 5829 153 10935 154 6424 155 11277 156 6980 157 9790 158 6467 159 10717 160 9607 161 10996 162 7233 163 11383 164 7643 165 14190 166 6926 167 12499 168 6531 169 12882 170 7604 171 12923 172 7738 173 14075 174 8718 175 12335 176 8293 177 11673 178 9857 179 13504 180 8475 181 11594 182 8320 183 17940 184 8666 185 15978 186 7462 187 13444 188 10108 189 14611 190 9919 191 13022 192 8688 193 13906 194 11498 195 13097 196 11362 197 12489 198 11036 199 13060 200 7587 201 14377 202 9958 203 15282 204 7226 205 14452 206 10597 207 14712 208 13333 209 10834 210 6852 211 13144 212 14021 213 13584 214 10785 215 12300 216 9849 217 15128 218 8219 219 15351 220 5627 221 14978 222 7608 223 11597 224 6826 225 16039 226 10081 227 13545 228 8928 229 11164 230 10644 231 14656 232 7216 233 9330 234 7199 235 18367 236 7291 237 18337 238 6747 239 11101 240 8301 241 11734 242 10022 243 9554 244 6594 245 11480 246 7731 247 9558 248 11111 249 10257 250 12712 251 9544 252 4748 253 11562 254 8373 255 11339 256 3353 257 9955 258 9694 259 9719 260 14531 261 8535 262 3285 263 10451 264 8812 265 9923 266 7759 267 8010 268 7913 269 8952 270 4972 271 9701 272 3740 273 13003 274 4307 275 6040 276 3903 277 11261 278 6283 279 6521 280 5240 281 7945 282 5851 283 11028 284 3683 285 5270 286 5309 287 10252 288 3957 289 13437 290 4107 291 7566 292 4508 293 6166 294 4781 295 5240 296 4740 297 7122 298 2482 299 5186 300 7068 301 5677 302 6825 303 5371 304 2158 305 6282 306 4963 307 4721 308 1991 309 5699 310 5473 311 5037 312 10369 313 5014 314 1560 315 6762 316 3066 317 5013 318 2709 319 4039 320 5428 321 4035 322 1600 323 5401 324 2452 325 7124 326 1773 327 2988 328 2796 329 5937 330 2534 331 2808 332 2180 333 5193 334 2086 335 6446 336 2290 337 2192 338 4535 339 3992 340 1481 341 5155 342 2065 343 4383 344 1969 345 2756 346 1659 347 3173 348 2775 349 3173 350 1269 351 3269 352 2844 353 2865 354 2573 355 2386 356 1827 357 3031 358 1631 359 2442 360 1433 361 3591 362 2037 363 2571 364 4204 365 2613 366 1110 367 3531 368 1473 369 2447 370 797 371 2794 372 2949 373 1505 374 1041 375 2972 376 891 377 2818 378 1243 379 1848 380 1345 381 2469 382 886 383 2021 384 1188 385 2584 386 1427 387 3251 388 827 389 1525 390 3376 391 1472 392 887 393 2083 394 808 395 2502 396 1225 397 1354 398 1091 399 1804 400 1055 401 1610 402 1042 403 1499 404 1302 405 1660 406 766 407 1627 408 2011 409 1207 410 914 411 1708 412 564 413 2285 414 1192 415 1247 416 1438 417 1488 418 536 419 1498 420 1173 421 1088 422 870 423 1733 424 802 425 1246 426 1031 427 1010 428 724 429 1552 430 652 431 1373 432 949 433 1103 434 810 435 1213 436 494 437 1447 438 1134 439 1121 440 842 441 1131 442 1002 443 1235 444 1011 445 842 446 726 447 1537 448 438 449 1012 450 1080 451 765 452 800 453 1192 454 440 455 1104 456 1037 457 727 458 801 459 1176 460 689 461 975 462 1027 463 816 464 493 465 1326 466 479 467 821 468 975 469 636 470 778 471 997 472 363 473 1008 474 874 475 779 476 630 477 1013 478 366 479 923 480 1009 481 624 482 609 483 1296 484 278 485 903 486 896 487 530 488 596 489 864 490 429 491 983 492 893 493 546 494 593 495 943 496 254 497 715 498 844 499 577 500 419 501 845 502 403 503 690 504 698 505 515 506 647 507 774 508 312 509 743 510 915 511 476 512 492 513 862 514 309 515 695 516 869 517 493 518 498 519 832 520 310 521 740 522 804 523 463 524 436 525 730 526 243 527 732 528 799 529 311 530 489 531 750 532 218 533 512 534 572 535 499 536 342 537 722 538 318 539 481 540 736 541 322 542 587 543 701 544 240 545 642 546 742 547 358 548 337 549 799 550 231 551 492 552 605 553 437 554 430 555 786 556 238 557 498 558 656 559 326 560 424 561 522 562 228 563 478 564 637 565 349 566 395 567 635 568 220 569 422 570 513 571 347 572 240 573 616 574 264 575 477 576 504 577 214 578 477 579 541 580 233 581 414 582 692 583 310 584 243 585 835 586 162 587 348 588 474 589 279 590 402 591 492 592 195 593 438 594 458 595 272 596 327 597 513 598 222 599 307 600 583 601 175 602 271 603 428 604 138 605 452 606 505 607 282 608 233 609 429 610 228 611 334 612 520 613 180 614 339 615 404 616 161 617 316 618 667 619 201 620 265 621 299 622 163 623 322 624 451 625 279 626 264 627 345 628 205 629 281 630 424 631 193 632 179 633 563 634 142 635 377 636 506 637 134 638 250 639 321 640 165 641 310 642 362 643 222 644 176 645 456 646 164 647 303 648 407 649 109 650 248 651 225 652 115 653 343 654 509 655 233 656 180 657 326 658 123 659 285 660 286 661 133 662 253 663 321 664 149 665 305 666 380 667 142 668 180 669 371 670 139 671 240 672 351 673 162 674 187 675 285 676 141 677 215 678 400 679 128 680 151 681 263 682 140 683 305 684 287 685 155 686 153 687 211 688 139 689 138 690 327 691 119 692 130 693 305 694 55 695 259 696 255 697 137 698 263 699 243 700 210 701 175 702 411 703 130 704 133 705 424 706 66 707 202 708 211 709 79 710 146 711 279 712 96 713 196 714 274 715 174 716 132 717 217 718 128 719 141 720 233 721 82 722 133 723 178 724 73 725 253 726 265 727 88 728 148 729 171 730 96 731 146 732 196 733 147 734 176 735 281 736 141 737 128 738 272 739 97 740 168 741 294 742 73 743 206 744 221 745 125 746 112 747 179 748 67 749 136 750 247 751 81 752 99 753 260 754 57 755 201 756 197 757 100 758 86 759 142 760 51 761 160 762 196 763 123 764 66 765 256 766 53 767 93 768 178 769 54 770 129 771 176 772 58 773 157 774 246 775 105 776 106 777 112 778 49 779 146 780 236 781 61 782 139 783 216 784 32 785 155 786 138 787 84 788 90 789 141 790 126 791 111 792 130 793 119 794 89 795 120 796 23 797 93 798 144 799 58 800 102 801 106 802 51 803 136 804 121 805 110 806 102 807 137 808 68 809 74 810 214 811 68 812 84 813 138 814 36 815 185 816 174 817 46 818 56 819 159 820 97 821 55 822 147 823 53 824 47 825 164 826 60 827 82 828 130 829 44 830 81 831 107 832 28 833 104 834 151 835 132 836 67 837 86 838 16 839 76 840 91 841 65 842 73 843 167 844 35 845 123 846 85 847 27 848 85 849 89 850 26 851 69 852 118 853 53 854 60 855 128 856 20 857 55 858 162 859 59 860 66 861 104 862 51 863 118 864 71 865 61 866 54 867 98 868 29 869 58 870 79 871 47 872 48 873 116 874 39 875 102 876 57 877 35 878 82 879 79 880 70 881 90 882 89 883 66 884 39 885 88 886 36 887 56 888 175 889 15 890 61 891 75 892 30 893 52 894 83 895 93 896 43 897 95 898 28 899 46 900 107 901 45 902 37 903 89 904 9 905 99 906 66 907 35 908 38 909 41 910 27 911 51 912 53 913 40 914 28 915 144 916 21 917 62 918 67 919 20 920 41 921 80 922 20 923 68 924 69 925 69 926 27 927 59 928 25 929 37 930 105 931 58 932 41 933 65 934 24 935 78 936 67 937 16 938 46 939 63 940 29 941 31 942 57 943 59 944 58 945 73 946 50 947 39 948 34 949 18 950 70 951 62 952 14 953 69 954 44 955 38 956 36 957 45 958 47 959 26 960 127 961 12 962 28 963 55 964 6 965 53 966 59 967 32 968 30 969 44 970 28 971 44 972 69 973 44 974 18 975 101 976 29 977 30 978 42 979 12 980 62 981 48 982 21 983 26 984 31 985 27 986 29 987 71 988 23 989 30 990 80 991 19 992 14 993 68 994 15 995 88 996 40 997 20 998 33 999 26 1000 36
61: Average symbolic conclusion length is 980354998/3652191 ≈ 268.43. (Median: 235)
There are 1466359 minimal D-proofs with conclusions of even symbolic length, and there are 2185832 minimal D-proofs with conclusions of odd symbolic length. [1466359/3652191 ≈ 40.15% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 0 12 0 13 1 14 0 15 1 16 0 17 0 18 0 19 0 20 0 21 2 22 0 23 1 24 1 25 2 26 0 27 1 28 0 29 4 30 3 31 17 32 0 33 10 34 0 35 17 36 6 37 26 38 2 39 39 40 1 41 39 42 8 43 50 44 7 45 62 46 10 47 54 48 10 49 56 50 21 51 49 52 22 53 70 54 40 55 77 56 47 57 105 58 45 59 175 60 99 61 185 62 95 63 267 64 105 65 449 66 128 67 513 68 191 69 533 70 191 71 530 72 188 73 637 74 220 75 746 76 259 77 877 78 287 79 903 80 346 81 1227 82 453 83 1251 84 524 85 1363 86 689 87 1523 88 823 89 1765 90 839 91 1967 92 928 93 2436 94 997 95 2675 96 1105 97 2888 98 1237 99 2940 100 1406 101 3216 102 1839 103 3444 104 1892 105 4074 106 2531 107 4612 108 2396 109 4671 110 2548 111 5572 112 2488 113 5741 114 2771 115 6176 116 3030 117 6257 118 3289 119 7369 120 3796 121 7115 122 4207 123 7630 124 4363 125 8506 126 5198 127 8689 128 4654 129 9328 130 5117 131 10695 132 4935 133 10312 134 5243 135 11489 136 6473 137 11364 138 6379 139 11745 140 7601 141 11702 142 7584 143 12224 144 8466 145 13398 146 7531 147 13543 148 9086 149 16591 150 8987 151 14812 152 8169 153 16086 154 9718 155 16127 156 9847 157 14721 158 10804 159 16162 160 12516 161 15833 162 11405 163 16391 164 11242 165 17670 166 10728 167 18930 168 12059 169 19551 170 11286 171 19690 172 12244 173 20638 174 13619 175 17335 176 11642 177 18603 178 18165 179 19207 180 13516 181 19462 182 13963 183 24300 184 12586 185 21872 186 11425 187 21730 188 13212 189 21725 190 13363 191 24034 192 15307 193 21300 194 14338 195 19202 196 17177 197 22332 198 14923 199 18147 200 13955 201 29441 202 14455 203 26670 204 12475 205 21387 206 16686 207 23505 208 16726 209 20923 210 13859 211 21874 212 18220 213 20345 214 18748 215 19310 216 18914 217 20261 218 11776 219 21894 220 16049 221 24017 222 10907 223 21875 224 16786 225 22527 226 21756 227 16504 228 10449 229 20406 230 21646 231 20609 232 17348 233 18547 234 15497 235 21826 236 12662 237 23115 238 8726 239 22873 240 11658 241 16829 242 10135 243 24313 244 15005 245 20079 246 13483 247 16340 248 15766 249 22088 250 10600 251 13549 252 10990 253 26749 254 10699 255 27611 256 10090 257 16264 258 12222 259 16694 260 14530 261 13921 262 9782 263 16987 264 10665 265 13784 266 16216 267 14661 268 18782 269 13748 270 6804 271 16314 272 12392 273 16016 274 4936 275 14084 276 13989 277 13889 278 21160 279 12530 280 4612 281 15232 282 12145 283 13759 284 10887 285 11483 286 11641 287 12461 288 6887 289 13906 290 5726 291 18416 292 6068 293 8545 294 6126 295 15682 296 8589 297 9421 298 7207 299 11547 300 8063 301 15421 302 5491 303 7392 304 7995 305 13865 306 5728 307 18255 308 5954 309 10923 310 6489 311 8483 312 6563 313 7679 314 6775 315 10199 316 3384 317 7491 318 9762 319 7881 320 9311 321 7596 322 3328 323 8768 324 6888 325 6753 326 3031 327 8260 328 7395 329 7098 330 13997 331 6782 332 2330 333 9990 334 4236 335 7156 336 3787 337 5885 338 7765 339 5633 340 2240 341 7507 342 3784 343 9446 344 2619 345 4860 346 4056 347 8145 348 3597 349 4516 350 3271 351 7224 352 2967 353 8592 354 3409 355 3245 356 6681 357 5752 358 2149 359 6821 360 3101 361 6354 362 2933 363 3828 364 2448 365 4996 366 3926 367 4481 368 1990 369 4838 370 3818 371 4166 372 3608 373 3525 374 2969 375 4343 376 2190 377 3758 378 2401 379 4924 380 2866 381 3894 382 5395 383 3794 384 1807 385 5100 386 2206 387 3722 388 1254 389 4041 390 4254 391 2372 392 1654 393 4299 394 1384 395 4122 396 2047 397 2936 398 1997 399 3402 400 1392 401 2949 402 1943 403 3697 404 2062 405 4541 406 1333 407 2639 408 4709 409 2226 410 1524 411 3021 412 1223 413 3642 414 2097 415 2075 416 1607 417 2864 418 1586 419 2446 420 1707 421 2240 422 1965 423 2452 424 1109 425 2732 426 2865 427 1836 428 1358 429 2709 430 949 431 3107 432 1788 433 1955 434 2044 435 2337 436 922 437 2528 438 1852 439 1784 440 1405 441 2592 442 1263 443 2103 444 1749 445 1740 446 1267 447 2449 448 964 449 2332 450 1690 451 1650 452 1267 453 2304 454 884 455 2229 456 1734 457 1725 458 1434 459 1787 460 1379 461 1900 462 1867 463 1186 464 1135 465 2619 466 709 467 1538 468 1663 469 1384 470 1306 471 1768 472 697 473 1693 474 1623 475 1300 476 1278 477 2063 478 1048 479 1572 480 1563 481 1214 482 961 483 2213 484 776 485 1582 486 1523 487 1122 488 1104 489 1609 490 717 491 1593 492 1365 493 1151 494 1177 495 1696 496 548 497 1494 498 1654 499 968 500 971 501 1946 502 595 503 1303 504 1473 505 1089 506 1121 507 1380 508 651 509 1374 510 1518 511 949 512 1132 513 1556 514 509 515 1313 516 1381 517 1021 518 735 519 1229 520 670 521 1143 522 1344 523 863 524 945 525 1366 526 538 527 1282 528 1281 529 710 530 927 531 1408 532 490 533 1247 534 1474 535 907 536 738 537 1465 538 494 539 1009 540 1257 541 683 542 793 543 1253 544 450 545 1281 546 1300 547 664 548 799 549 1133 550 469 551 887 552 1221 553 876 554 648 555 1249 556 492 557 923 558 1114 559 528 560 927 561 1058 562 533 563 1137 564 1147 565 685 566 627 567 1158 568 379 569 807 570 1358 571 597 572 612 573 1306 574 389 575 945 576 1106 577 549 578 681 579 851 580 382 581 844 582 1109 583 562 584 569 585 1090 586 381 587 654 588 706 589 520 590 493 591 954 592 410 593 793 594 916 595 562 596 669 597 854 598 410 599 756 600 1109 601 455 602 513 603 1222 604 256 605 758 606 876 607 489 608 579 609 921 610 367 611 638 612 829 613 489 614 615 615 818 616 282 617 555 618 947 619 331 620 526 621 818 622 275 623 653 624 711 625 530 626 401 627 678 628 313 629 524 630 936 631 314 632 626 633 789 634 336 635 663 636 866 637 373 638 447 639 1016 640 283 641 489 642 726 643 415 644 386 645 789 646 364 647 531 648 646 649 270 650 459 651 682 652 233 653 537 654 885 655 372 656 335 657 545 658 276 659 509 660 634 661 357 662 362 663 733 664 205 665 671 666 632 667 272 668 498 669 413 670 327 671 489 672 872 673 371 674 318 675 594 676 162 677 518 678 691 679 196 680 388 681 504 682 235 683 459 684 532 685 332 686 319 687 724 688 212 689 386 690 722 691 209 692 357 693 423 694 253 695 468 696 494 697 219 698 234 699 488 700 302 701 475 702 571 703 201 704 215 705 454 706 242 707 311 708 764 709 202 710 326 711 430 712 116 713 436 714 381 715 325 716 362 717 469 718 334 719 302 720 578 721 166 722 243 723 641 724 119 725 437 726 429 727 180 728 246 729 362 730 272 731 312 732 464 733 283 734 231 735 494 736 176 737 388 738 390 739 160 740 266 741 258 742 177 743 348 744 344 745 270 746 288 747 379 748 125 749 255 750 394 751 176 752 263 753 401 754 202 755 323 756 486 757 203 758 271 759 491 760 145 761 345 762 394 763 196 764 164 765 426 766 121 767 203 768 426 769 140 770 277 771 338 772 102 773 268 774 331 775 226 776 135 777 293 778 141 779 234 780 390 781 144 782 176 783 301 784 77 785 294 786 392 787 147 788 192 789 284 790 296 791 195 792 340 793 161 794 192 795 455 796 77 797 223 798 290 799 110 800 197 801 297 802 145 803 228 804 263 805 189 806 148 807 275 808 144 809 189 810 307 811 124 812 120 813 211 814 114 815 341 816 244 817 96 818 165 819 209 820 78 821 182 822 262 823 171 824 162 825 316 826 123 827 167 828 356 829 131 830 209 831 160 832 59 833 254 834 324 835 160 836 97 837 202 838 144 839 95 840 237 841 86 842 121 843 295 844 80 845 293 846 239 847 112 848 130 849 163 850 65 851 125 852 203 853 149 854 132 855 297 856 32 857 155 858 234 859 89 860 115 861 241 862 135 863 181 864 265 865 103 866 131 867 164 868 41 869 163 870 248 871 72 872 96 873 291 874 81 875 193 876 208 877 110 878 110 879 178 880 94 881 176 882 112 883 147 884 83 885 170 886 57 887 101 888 180 889 90 890 159 891 165 892 64 893 159 894 125 895 154 896 101 897 160 898 108 899 117 900 122 901 90 902 97 903 133 904 39 905 283 906 250 907 41 908 84 909 119 910 97 911 70 912 166 913 78 914 82 915 192 916 29 917 111 918 167 919 89 920 70 921 160 922 46 923 143 924 116 925 159 926 86 927 119 928 30 929 76 930 141 931 49 932 57 933 215 934 49 935 181 936 116 937 45 938 99 939 102 940 30 941 89 942 174 943 81 944 53 945 149 946 64 947 90 948 120 949 74 950 93 951 127 952 43 953 112 954 83 955 86 956 58 957 92 958 60 959 57 960 143 961 79 962 87 963 112 964 43 965 105 966 87 967 49 968 93 969 107 970 122 971 103 972 83 973 66 974 57 975 157 976 48 977 49 978 179 979 16 980 50 981 78 982 30 983 87 984 96 985 121 986 69 987 89 988 44 989 111 990 193 991 58 992 29 993 109 994 46 995 111 996 79 997 36 998 65 999 73 1000 49
63: Average symbolic conclusion length is 1674021161/5983166 ≈ 279.79. (Median: 243)
There are 2428915 minimal D-proofs with conclusions of even symbolic length, and there are 3554251 minimal D-proofs with conclusions of odd symbolic length. [2428915/5983166 ≈ 40.60% 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 1 14 1 15 0 16 0 17 0 18 0 19 4 20 0 21 0 22 0 23 2 24 0 25 6 26 2 27 6 28 0 29 15 30 1 31 6 32 1 33 12 34 1 35 14 36 0 37 10 38 5 39 20 40 6 41 12 42 15 43 26 44 13 45 48 46 15 47 74 48 35 49 68 50 31 51 111 52 32 53 208 54 46 55 201 56 54 57 256 58 63 59 254 60 59 61 327 62 58 63 366 64 102 65 339 66 101 67 372 68 181 69 462 70 252 71 503 72 290 73 660 74 338 75 745 76 421 77 1010 78 464 79 1257 80 466 81 1634 82 551 83 1760 84 665 85 1703 86 885 87 1779 88 915 89 2015 90 1123 91 2567 92 1253 93 2860 94 1353 95 3639 96 1578 97 3797 98 1595 99 4357 100 1750 101 4705 102 2141 103 4852 104 2405 105 4841 106 2943 107 5836 108 2909 109 6315 110 3239 111 7145 112 3361 113 7437 114 3992 115 8341 116 4007 117 8372 118 4362 119 10033 120 5407 121 10007 122 5434 123 10454 124 6863 125 11140 126 6976 127 11329 128 6853 129 12782 130 7057 131 13280 132 7729 133 14687 134 8286 135 15214 136 8439 137 16890 138 9504 139 16622 140 10310 141 16446 142 10449 143 17753 144 12986 145 18388 146 11165 147 19405 148 12013 149 22420 150 11480 151 20958 152 11785 153 23264 154 13880 155 23288 156 13770 157 24383 158 15752 159 22989 160 15975 161 23878 162 17770 163 25859 164 15858 165 25013 166 18013 167 31566 168 18192 169 28509 170 15827 171 28980 172 19072 173 30095 174 19306 175 26847 176 20059 177 29100 178 24042 179 28162 180 22333 181 28492 182 21789 183 30672 184 19581 185 32856 186 22608 187 34145 188 20275 189 33746 190 22061 191 35556 192 25057 193 29127 194 19820 195 31198 196 32286 197 32472 198 24185 199 31626 200 24145 201 39603 202 21791 203 36763 204 19129 205 35855 206 21946 207 34750 208 21944 209 40026 210 25516 211 35238 212 23667 213 30459 214 28590 215 35842 216 24809 217 28082 218 22513 219 46802 220 23175 221 43528 222 20191 223 32514 224 26578 225 36999 226 27140 227 32234 228 21534 229 34061 230 27920 231 31107 232 29814 233 29614 234 31323 235 30171 236 17815 237 33152 238 25348 239 36443 240 16196 241 32906 242 25933 243 33632 244 34324 245 25124 246 15640 247 30947 248 32359 249 30565 250 27081 251 27374 252 23724 253 31806 254 18962 255 33805 256 13346 257 34723 258 17545 259 23679 260 14857 261 36126 262 21946 263 29050 264 19895 265 24116 266 22878 267 32774 268 15385 269 19702 270 16695 271 37526 272 15569 273 41245 274 15054 275 23520 276 17913 277 24196 278 20697 279 20346 280 14376 281 24960 282 14758 283 19265 284 23346 285 20929 286 27177 287 19779 288 9850 289 23488 290 18223 291 21970 292 7264 293 20287 294 20148 295 19149 296 30336 297 18257 298 6586 299 22215 300 16640 301 19440 302 15279 303 16297 304 16969 305 17399 306 9579 307 19327 308 8603 309 26087 310 8655 311 11845 312 9555 313 22346 314 11644 315 13765 316 9798 317 16777 318 11212 319 21173 320 7973 321 10554 322 12080 323 18845 324 8107 325 25200 326 8609 327 15569 328 9199 329 11985 330 9290 331 10702 332 9604 333 14732 334 4829 335 11305 336 13239 337 11317 338 12677 339 10752 340 5041 341 12163 342 9816 343 9332 344 4633 345 12242 346 9980 347 10090 348 18760 349 9820 350 3669 351 14371 352 5884 353 10016 354 5498 355 8643 356 10935 357 8141 358 3422 359 10680 360 5689 361 12950 362 4076 363 7298 364 5703 365 11343 366 5170 367 6432 368 4634 369 10462 370 4342 371 11900 372 5020 373 5113 374 9876 375 8269 376 3109 377 9534 378 4659 379 8708 380 4304 381 6204 382 3774 383 7182 384 5544 385 7051 386 3091 387 7046 388 5163 389 6051 390 5269 391 4970 392 4681 393 6675 394 3057 395 5577 396 3692 397 7630 398 4189 399 5735 400 7006 401 5927 402 3136 403 7009 404 3511 405 5820 406 2128 407 5922 408 5978 409 3757 410 2893 411 5963 412 2093 413 5918 414 3373 415 4277 416 2978 417 5250 418 2191 419 4575 420 3074 421 5359 422 3358 423 6376 424 2034 425 4217 426 6510 427 3669 428 2484 429 4697 430 2029 431 5376 432 3376 433 3386 434 2597 435 4378 436 2307 437 3851 438 2951 439 3413 440 2890 441 3908 442 1964 443 4557 444 4328 445 2941 446 2301 447 4364 448 1409 449 4784 450 3323 451 2826 452 2919 453 3753 454 1602 455 3846 456 2837 457 2849 458 2253 459 3858 460 1900 461 3157 462 3125 463 2684 464 1987 465 4001 466 1531 467 3576 468 2930 469 2680 470 2185 471 3316 472 1479 473 3489 474 2775 475 2976 476 2174 477 3019 478 2008 479 3338 480 2651 481 1991 482 1876 483 3825 484 1077 485 2801 486 2544 487 2146 488 1955 489 3123 490 1416 491 2739 492 2548 493 2175 494 2089 495 3363 496 1510 497 2732 498 2772 499 1879 500 1590 501 3559 502 1303 503 2425 504 2447 505 2236 506 1753 507 2837 508 1179 509 2408 510 2498 511 1801 512 1942 513 2566 514 975 515 2529 516 2635 517 1598 518 1770 519 3043 520 995 521 2200 522 2447 523 1728 524 1624 525 2463 526 1037 527 2227 528 2296 529 1552 530 2044 531 2634 532 835 533 2087 534 2298 535 1679 536 1266 537 2653 538 1149 539 1762 540 2088 541 1488 542 1685 543 2091 544 834 545 2259 546 1928 547 1409 548 1623 549 2048 550 1006 551 1944 552 2272 553 1528 554 1159 555 2492 556 773 557 1832 558 2215 559 1189 560 1437 561 2005 562 887 563 1843 564 2009 565 1244 566 1605 567 2024 568 705 569 1444 570 2173 571 1219 572 1009 573 1932 574 856 575 1610 576 1957 577 1027 578 1389 579 1677 580 826 581 1718 582 1832 583 1111 584 1058 585 2202 586 705 587 1438 588 2131 589 1037 590 1213 591 1893 592 627 593 1569 594 1724 595 1075 596 1082 597 1575 598 809 599 1455 600 1808 601 820 602 1038 603 1686 604 547 605 1435 606 1746 607 961 608 796 609 1542 610 837 611 1122 612 1347 613 870 614 1154 615 1484 616 543 617 1380 618 1779 619 802 620 956 621 1576 622 589 623 1123 624 1795 625 1028 626 974 627 1546 628 469 629 1122 630 1564 631 786 632 913 633 1356 634 609 635 1385 636 1394 637 693 638 926 639 1228 640 551 641 943 642 1118 643 785 644 572 645 1562 646 564 647 912 648 1462 649 525 650 1120 651 1154 652 487 653 1133 654 1468 655 803 656 702 657 1646 658 484 659 833 660 1304 661 619 662 716 663 1355 664 476 665 1113 666 1218 667 654 668 681 669 925 670 528 671 751 672 1322 673 660 674 655 675 1310 676 406 677 858 678 1084 679 533 680 588 681 1003 682 395 683 906 684 986 685 654 686 933 687 951 688 475 689 751 690 1326 691 492 692 538 693 1505 694 303 695 981 696 966 697 396 698 742 699 822 700 491 701 732 702 1055 703 509 704 547 705 1239 706 390 707 617 708 1096 709 365 710 634 711 698 712 381 713 854 714 900 715 530 716 423 717 872 718 544 719 691 720 941 721 296 722 661 723 769 724 382 725 748 726 1316 727 424 728 488 729 613 730 359 731 659 732 869 733 488 734 529 735 971 736 345 737 653 738 837 739 309 740 465 741 955 742 336 743 658 744 857 745 492 746 448 747 650 748 345 749 521 750 835 751 366 752 352 753 811 754 255 755 861 756 699 757 300 758 441 759 468 760 318 761 529 762 1032 763 404 764 399 765 883 766 247 767 459 768 505 769 247 770 487 771 708 772 322 773 514 774 696 775 515 776 340 777 780 778 333 779 493 780 677 781 263 782 444 783 516 784 193 785 580 786 653 787 307 788 331 789 522 790 352 791 477 792 541 793 355 794 309 795 540 796 192 797 404 798 621 799 234 800 438 801 487 802 196 803 452 804 580 805 358 806 328 807 515 808 314 809 342 810 742 811 216 812 277 813 786 814 169 815 551 816 443 817 250 818 350 819 501 820 364 821 326 822 518 823 306 824 231 825 577 826 204 827 361 828 425 829 175 830 321 831 359 832 210 833 454 834 488 835 346 836 253 837 305 838 131 839 303 840 492 841 231 842 446 843 528 844 173 845 435 846 508 847 258 848 321 849 495 850 182 851 315 852 399 853 215 854 230 855 465 856 200 857 219 858 525 859 164 860 194 861 415 862 177 863 425 864 380 865 270 866 193 867 343 868 89 869 338 870 527 871 189 872 182 873 451 874 124 875 333 876 363 877 214 878 227 879 349 880 466 881 259 882 462 883 219 884 188 885 354 886 154 887 258 888 346 889 126 890 193 891 360 892 151 893 301 894 361 895 259 896 140 897 372 898 152 899 254 900 311 901 185 902 163 903 252 904 82 905 369 906 298 907 158 908 203 909 216 910 120 911 256 912 270 913 232 914 171 915 419 916 136 917 229 918 380 919 159 920 218 921 221 922 110 923 368 924 302 925 199 926 206 927 338 928 116 929 126 930 334 931 102 932 135 933 348 934 137 935 344 936 219 937 141 938 158 939 264 940 91 941 182 942 274 943 204 944 124 945 368 946 119 947 159 948 212 949 75 950 158 951 295 952 73 953 232 954 216 955 184 956 151 957 205 958 80 959 132 960 356 961 116 962 118 963 252 964 76 965 287 966 258 967 110 968 124 969 194 970 134 971 193 972 143 973 161 974 133 975 264 976 91 977 166 978 227 979 105 980 195 981 202 982 97 983 155 984 158 985 206 986 169 987 191 988 158 989 174 990 198 991 109 992 91 993 203 994 78 995 366 996 308 997 70 998 125 999 137 1000 109