pmGenerator/data/plot/default-plot_data_x500.txt at master · xamidi/pmGenerator · GitHub

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
1: Average symbolic conclusion length is 27/3 ≈ 9.00. (Median: 9)
   Minimum and maximum symbolic conclusion lengths are 5 (×1) and 13 (×1), respectively.
   There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 3 minimal D-proofs with conclusions of odd symbolic length. [0/3 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 1 10 0 11 0 12 0 13 1

3: Average symbolic conclusion length is 74/6 ≈ 12.33. (Median: 13.00)
   Minimum and maximum symbolic conclusion lengths are 7 (×2) and 19 (×1), respectively.
   There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 6 minimal D-proofs with conclusions of odd symbolic length. [0/6 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 2 8 0 9 0 10 0 11 1 12 0 13 0 14 0 15 2 16 0 17 0 18 0 19 1

5: Average symbolic conclusion length is 180/12 ≈ 15.00. (Median: 15.00)
   Minimum and maximum symbolic conclusion lengths are 3 (×1) and 29 (×1), respectively.
   There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 12 minimal D-proofs with conclusions of odd symbolic length. [0/12 ≈ 0.00% even]
1 0 2 0 3 1 4 0 5 0 6 0 7 0 8 0 9 3 10 0 11 0 12 0 13 2 14 0 15 0 16 0 17 3 18 0 19 0 20 0 21 1 22 0 23 1 24 0 25 0 26 0 27 0 28 0 29 1

7: Average symbolic conclusion length is 641/38 ≈ 16.87. (Median: 15)
   Minimum and maximum symbolic conclusion lengths are 5 (×1) and 45 (×1), respectively.
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 37 minimal D-proofs with conclusions of odd symbolic length. [1/38 ≈ 2.63% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 1 8 0 9 1 10 0 11 11 12 0 13 1 14 0 15 5 16 0 17 1 18 0 19 6 20 0 21 2 22 0 23 3 24 0 25 2 26 0 27 0 28 0 29 0 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 1

9: Average symbolic conclusion length is 1974/89 ≈ 22.18. (Median: 21)
   Minimum and maximum symbolic conclusion lengths are 7 (×1) and 71 (×1), respectively.
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 88 minimal D-proofs with conclusions of odd symbolic length. [1/89 ≈ 1.12% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 1 9 3 10 0 11 1 12 0 13 16 14 0 15 4 16 0 17 12 18 0 19 4 20 0 21 13 22 0 23 4 24 0 25 6 26 0 27 5 28 0 29 2 30 0 31 2 32 0 33 5 34 0 35 4 36 0 37 0 38 0 39 2 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 0 54 0 55 0 56 0 57 0 58 0 59 1 60 0 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 1

11: Average symbolic conclusion length is 6142/229 ≈ 26.82. (Median: 23)
    Minimum and maximum symbolic conclusion lengths are 9 (×3) and 113 (×1), respectively.
    There are 5 minimal D-proofs with conclusions of even symbolic length, and there are 224 minimal D-proofs with conclusions of odd symbolic length. [5/229 ≈ 2.18% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 3 10 2 11 8 12 0 13 4 14 1 15 35 16 1 17 9 18 0 19 28 20 0 21 6 22 0 23 27 24 0 25 12 26 0 27 14 28 0 29 12 30 0 31 9 32 1 33 4 34 0 35 9 36 0 37 4 38 0 39 5 40 0 41 7 42 0 43 3 44 0 45 2 46 0 47 2 48 0 49 7 50 0 51 1 52 0 53 4 54 0 55 2 56 0 57 1 58 0 59 0 60 0 61 2 62 0 63 0 64 0 65 1 66 0 67 0 68 0 69 0 70 0 71 0 72 0 73 1 74 0 75 0 76 0 77 0 78 0 79 0 80 0 81 0 82 0 83 0 84 0 85 0 86 0 87 0 88 0 89 0 90 0 91 0 92 0 93 0 94 0 95 1 96 0 97 0 98 0 99 0 100 0 101 0 102 0 103 0 104 0 105 0 106 0 107 0 108 0 109 0 110 0 111 0 112 0 113 1

13: Average symbolic conclusion length is 20894/672 ≈ 31.09. (Median: 25)
    Minimum and maximum symbolic conclusion lengths are 7 (×2) and 181 (×1), respectively.
    There are 18 minimal D-proofs with conclusions of even symbolic length, and there are 654 minimal D-proofs with conclusions of odd symbolic length. [18/672 ≈ 2.68% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 2 8 3 9 4 10 0 11 9 12 5 13 32 14 1 15 14 16 2 17 72 18 1 19 23 20 0 21 69 22 1 23 29 24 1 25 74 26 0 27 32 28 0 29 44 30 0 31 24 32 0 33 22 34 2 35 18 36 0 37 22 38 0 39 21 40 0 41 15 42 1 43 21 44 0 45 7 46 0 47 12 48 0 49 7 50 0 51 15 52 1 53 5 54 0 55 6 56 0 57 4 58 0 59 6 60 0 61 3 62 0 63 6 64 0 65 1 66 0 67 5 68 0 69 2 70 0 71 4 72 0 73 0 74 0 75 6 76 0 77 2 78 0 79 1 80 0 81 2 82 0 83 1 84 0 85 2 86 0 87 4 88 0 89 0 90 0 91 0 92 0 93 0 94 0 95 0 96 0 97 1 98 0 99 1 100 0 101 0 102 0 103 0 104 0 105 0 106 0 107 1 108 0 109 0 110 0 111 0 112 0 113 0 114 0 115 1 116 0 117 0 118 0 119 0 120 0 121 0 122 0 123 0 124 0 125 0 126 0 127 0 128 0 129 0 130 0 131 0 132 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 0 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 0 166 0 167 0 168 0 169 0 170 0 171 0 172 0 173 0 174 0 175 0 176 0 177 0 178 0 179 0 180 0 181 1

15: Average symbolic conclusion length is 69153/1844 ≈ 37.50. (Median: 31)
    Minimum and maximum symbolic conclusion lengths are 6 (×1) and 291 (×1), respectively.
    There are 45 minimal D-proofs with conclusions of even symbolic length, and there are 1799 minimal D-proofs with conclusions of odd symbolic length. [45/1844 ≈ 2.44% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 1 8 1 9 4 10 5 11 15 12 0 13 19 14 9 15 66 16 3 17 31 18 7 19 169 20 4 21 54 22 3 23 160 24 1 25 54 26 1 27 160 28 0 29 77 30 1 31 117 32 0 33 68 34 0 35 92 36 4 37 56 38 1 39 82 40 0 41 49 42 0 43 43 44 2 45 47 46 1 47 41 48 0 49 22 50 0 51 29 52 0 53 43 54 1 55 32 56 0 57 21 58 0 59 27 60 0 61 19 62 0 63 18 64 0 65 25 66 0 67 9 68 0 69 11 70 0 71 14 72 0 73 7 74 0 75 8 76 0 77 18 78 0 79 6 80 0 81 4 82 0 83 6 84 0 85 1 86 0 87 6 88 0 89 7 90 0 91 3 92 0 93 0 94 0 95 4 96 0 97 5 98 0 99 4 100 0 101 2 102 0 103 1 104 0 105 1 106 0 107 6 108 0 109 3 110 0 111 2 112 0 113 1 114 0 115 2 116 0 117 6 118 0 119 2 120 0 121 0 122 0 123 2 124 0 125 0 126 0 127 2 128 0 129 1 130 0 131 2 132 0 133 0 134 0 135 0 136 0 137 2 138 0 139 2 140 0 141 2 142 0 143 0 144 0 145 0 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 1 156 0 157 0 158 0 159 1 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 0 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 0 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 1 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 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 1

17: Average symbolic conclusion length is 229265/5221 ≈ 43.91. (Median: 35)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 469 (×1), respectively.
    There are 130 minimal D-proofs with conclusions of even symbolic length, and there are 5091 minimal D-proofs with conclusions of odd symbolic length. [130/5221 ≈ 2.49% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 0 8 2 9 3 10 2 11 12 12 17 13 43 14 1 15 57 16 21 17 195 18 10 19 92 20 14 21 377 22 6 23 132 24 6 25 402 26 7 27 149 28 5 29 406 30 2 31 193 32 3 33 305 34 4 35 180 36 1 37 192 38 8 39 138 40 1 41 193 42 0 43 165 44 1 45 117 46 4 47 144 48 1 49 113 50 0 51 122 52 0 53 95 54 2 55 120 56 4 57 73 58 3 59 119 60 1 61 57 62 0 63 76 64 0 65 58 66 0 67 69 68 0 69 28 70 0 71 57 72 0 73 36 74 0 75 41 76 0 77 35 78 0 79 39 80 0 81 26 82 1 83 42 84 0 85 19 86 0 87 26 88 0 89 22 90 0 91 29 92 0 93 17 94 0 95 23 96 0 97 18 98 0 99 12 100 0 101 15 102 1 103 11 104 0 105 7 106 0 107 15 108 0 109 10 110 0 111 12 112 0 113 6 114 0 115 8 116 0 117 3 118 0 119 12 120 0 121 5 122 0 123 8 124 0 125 5 126 0 127 7 128 0 129 4 130 0 131 7 132 0 133 4 134 1 135 1 136 0 137 2 138 0 139 6 140 0 141 4 142 0 143 4 144 0 145 0 146 0 147 4 148 0 149 0 150 0 151 2 152 0 153 1 154 0 155 5 156 0 157 4 158 0 159 2 160 0 161 3 162 0 163 0 164 0 165 3 166 0 167 3 168 0 169 1 170 0 171 1 172 0 173 3 174 0 175 2 176 0 177 0 178 0 179 2 180 0 181 1 182 0 183 0 184 0 185 5 186 0 187 4 188 0 189 0 190 0 191 1 192 0 193 0 194 0 195 0 196 0 197 2 198 0 199 0 200 0 201 1 202 0 203 1 204 0 205 2 206 0 207 0 208 0 209 1 210 0 211 0 212 0 213 1 214 0 215 0 216 0 217 0 218 0 219 1 220 0 221 1 222 0 223 0 224 0 225 3 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 1 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 1 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 1 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 1 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 0 394 0 395 0 396 0 397 0 398 0 399 1 400 0 401 0 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 0 410 0 411 0 412 0 413 0 414 0 415 0 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 0 428 0 429 0 430 0 431 0 432 0 433 0 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 0 446 0 447 0 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 0 464 0 465 0 466 0 467 0 468 0 469 1

19: Average symbolic conclusion length is 777218/15275 ≈ 50.88. (Median: 41)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 757 (×1), respectively.
    There are 371 minimal D-proofs with conclusions of even symbolic length, and there are 14904 minimal D-proofs with conclusions of odd symbolic length. [371/15275 ≈ 2.43% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 1 8 3 9 4 10 8 11 16 12 6 13 46 14 44 15 150 16 10 17 155 18 45 19 459 20 24 21 250 22 40 23 903 24 21 25 373 26 24 27 1030 28 21 29 426 30 14 31 993 32 8 33 469 34 5 35 779 36 8 37 500 38 5 39 618 40 16 41 429 42 5 43 552 44 4 45 456 46 6 47 430 48 8 49 359 50 5 51 344 52 2 53 336 54 2 55 324 56 3 57 273 58 6 59 252 60 3 61 273 62 6 63 260 64 0 65 232 66 0 67 189 68 0 69 186 70 0 71 192 72 1 73 150 74 0 75 137 76 0 77 167 78 1 79 137 80 1 81 126 82 3 83 118 84 1 85 100 86 0 87 113 88 0 89 117 90 1 91 72 92 3 93 72 94 0 95 81 96 1 97 70 98 0 99 57 100 0 101 75 102 1 103 53 104 1 105 41 106 0 107 47 108 0 109 34 110 0 111 39 112 0 113 49 114 0 115 33 116 0 117 45 118 0 119 39 120 0 121 39 122 0 123 36 124 0 125 33 126 0 127 23 128 0 129 18 130 0 131 25 132 0 133 24 134 0 135 20 136 2 137 24 138 0 139 21 140 0 141 19 142 0 143 27 144 0 145 19 146 0 147 18 148 0 149 11 150 0 151 11 152 0 153 10 154 0 155 13 156 0 157 17 158 0 159 12 160 0 161 9 162 1 163 10 164 0 165 5 166 0 167 16 168 0 169 7 170 0 171 12 172 0 173 5 174 0 175 5 176 0 177 7 178 0 179 7 180 0 181 5 182 0 183 5 184 0 185 5 186 0 187 7 188 0 189 7 190 0 191 1 192 0 193 1 194 0 195 5 196 0 197 8 198 0 199 7 200 0 201 4 202 0 203 6 204 0 205 3 206 0 207 5 208 0 209 4 210 0 211 1 212 0 213 1 214 0 215 3 216 1 217 3 218 0 219 3 220 0 221 3 222 0 223 3 224 0 225 0 226 0 227 5 228 0 229 1 230 0 231 0 232 0 233 2 234 0 235 1 236 0 237 2 238 0 239 1 240 0 241 0 242 0 243 3 244 0 245 0 246 0 247 0 248 0 249 3 250 0 251 6 252 0 253 2 254 0 255 2 256 0 257 0 258 0 259 3 260 0 261 0 262 0 263 1 264 0 265 0 266 0 267 3 268 0 269 0 270 0 271 1 272 0 273 2 274 0 275 0 276 0 277 1 278 0 279 3 280 0 281 1 282 0 283 1 284 0 285 0 286 0 287 1 288 0 289 1 290 0 291 0 292 0 293 0 294 0 295 4 296 0 297 2 298 0 299 2 300 0 301 1 302 0 303 2 304 0 305 0 306 0 307 1 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 1 318 0 319 2 320 0 321 1 322 0 323 0 324 0 325 1 326 0 327 0 328 0 329 0 330 0 331 2 332 0 333 0 334 0 335 0 336 0 337 1 338 0 339 0 340 0 341 1 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 1 356 0 357 1 358 0 359 0 360 0 361 0 362 0 363 3 364 0 365 0 366 0 367 1 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 0 394 0 395 0 396 0 397 0 398 0 399 0 400 0 401 1 402 0 403 0 404 0 405 0 406 0 407 0 408 0 409 0 410 0 411 0 412 0 413 0 414 0 415 1 416 0 417 0 418 0 419 0 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 0 428 0 429 0 430 0 431 0 432 0 433 0 434 0 435 0 436 0 437 0 438 0 439 0 440 0 441 0 442 0 443 0 444 0 445 0 446 0 447 1 448 0 449 0 450 0 451 0 452 0 453 0 454 0 455 0 456 0 457 0 458 0 459 0 460 0 461 0 462 0 463 0 464 0 465 0 466 0 467 0 468 0 469 0 470 0 471 1 472 0 473 0 474 0 475 0 476 0 477 0 478 0 479 0 480 0 481 0 482 0 483 0 484 0 485 0 486 0 487 0 488 0 489 0 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 0 498 0 499 0 500 0

21: Average symbolic conclusion length is 2619118/44206 ≈ 59.25. (Median: 47)
    Minimum and maximum symbolic conclusion lengths are 7 (×2) and 1223 (×1), respectively.
    There are 1046 minimal D-proofs with conclusions of even symbolic length, and there are 43160 minimal D-proofs with conclusions of odd symbolic length. [1046/44206 ≈ 2.37% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 2 8 3 9 2 10 9 11 10 12 19 13 65 14 13 15 120 16 109 17 368 18 26 19 400 20 120 21 1220 22 59 23 636 24 106 25 2118 26 51 27 877 28 56 29 2447 30 44 31 1112 32 34 33 2500 34 26 35 1294 36 30 37 1995 38 36 39 1343 40 22 41 1659 42 43 43 1262 44 23 45 1308 46 14 47 1263 48 11 49 1135 50 29 51 1160 52 10 53 916 54 6 55 1031 56 7 57 856 58 11 59 1152 60 16 61 663 62 14 63 871 64 16 65 739 66 2 67 880 68 5 69 539 70 4 71 713 72 2 73 465 74 5 75 621 76 2 77 452 78 0 79 532 80 3 81 380 82 4 83 558 84 4 85 297 86 8 87 376 88 3 89 326 90 0 91 369 92 1 93 225 94 6 95 379 96 0 97 209 98 2 99 279 100 0 101 223 102 1 103 207 104 3 105 157 106 3 107 293 108 2 109 135 110 0 111 192 112 0 113 175 114 1 115 156 116 0 117 114 118 0 119 225 120 0 121 97 122 2 123 154 124 2 125 111 126 0 127 145 128 1 129 86 130 1 131 144 132 0 133 82 134 2 135 117 136 1 137 77 138 4 139 76 140 2 141 59 142 1 143 107 144 0 145 65 146 1 147 95 148 0 149 61 150 0 151 54 152 0 153 36 154 1 155 100 156 0 157 47 158 0 159 69 160 1 161 43 162 0 163 48 164 1 165 32 166 0 167 60 168 0 169 35 170 0 171 33 172 0 173 47 174 0 175 26 176 0 177 29 178 0 179 47 180 0 181 30 182 0 183 32 184 0 185 24 186 0 187 65 188 0 189 22 190 0 191 39 192 0 193 13 194 0 195 18 196 0 197 24 198 0 199 29 200 0 201 19 202 0 203 23 204 0 205 16 206 0 207 29 208 1 209 18 210 0 211 11 212 0 213 15 214 0 215 18 216 0 217 14 218 1 219 23 220 0 221 8 222 0 223 17 224 0 225 20 226 0 227 15 228 0 229 19 230 0 231 12 232 0 233 8 234 0 235 15 236 0 237 9 238 0 239 11 240 0 241 5 242 0 243 5 244 0 245 13 246 0 247 14 248 0 249 7 250 0 251 17 252 0 253 13 254 0 255 4 256 0 257 11 258 0 259 6 260 0 261 8 262 0 263 6 264 0 265 2 266 0 267 8 268 0 269 8 270 0 271 1 272 0 273 4 274 0 275 3 276 0 277 9 278 0 279 5 280 0 281 7 282 0 283 8 284 0 285 3 286 0 287 2 288 0 289 6 290 0 291 4 292 0 293 2 294 0 295 2 296 0 297 7 298 0 299 3 300 0 301 3 302 0 303 6 304 0 305 2 306 0 307 4 308 0 309 1 310 0 311 6 312 0 313 1 314 0 315 8 316 0 317 1 318 0 319 3 320 0 321 8 322 0 323 3 324 0 325 1 326 0 327 3 328 0 329 4 330 0 331 2 332 0 333 3 334 0 335 3 336 0 337 3 338 0 339 1 340 0 341 1 342 0 343 4 344 0 345 0 346 0 347 2 348 0 349 3 350 0 351 2 352 0 353 0 354 0 355 0 356 0 357 1 358 0 359 3 360 0 361 0 362 0 363 1 364 0 365 5 366 0 367 1 368 0 369 1 370 0 371 1 372 0 373 0 374 0 375 0 376 0 377 0 378 0 379 2 380 0 381 1 382 0 383 1 384 0 385 0 386 0 387 1 388 0 389 1 390 0 391 2 392 0 393 0 394 0 395 0 396 0 397 1 398 0 399 2 400 0 401 3 402 0 403 3 404 0 405 3 406 0 407 2 408 0 409 0 410 0 411 2 412 0 413 0 414 0 415 0 416 0 417 2 418 0 419 1 420 0 421 0 422 0 423 0 424 0 425 0 426 0 427 2 428 0 429 0 430 0 431 1 432 0 433 0 434 0 435 0 436 0 437 2 438 0 439 2 440 0 441 0 442 0 443 1 444 0 445 0 446 0 447 0 448 0 449 1 450 0 451 2 452 0 453 0 454 0 455 1 456 0 457 1 458 0 459 1 460 0 461 0 462 0 463 0 464 0 465 0 466 0 467 1 468 0 469 0 470 0 471 0 472 0 473 4 474 0 475 2 476 0 477 0 478 0 479 1 480 0 481 0 482 0 483 1 484 0 485 2 486 0 487 0 488 0 489 2 490 0 491 0 492 0 493 0 494 0 495 0 496 0 497 1 498 0 499 0 500 0

23: Average symbolic conclusion length is 8848047/129885 ≈ 68.12. (Median: 53)
    Minimum and maximum symbolic conclusion lengths are 9 (×5) and 1977 (×1), respectively.
    There are 3106 minimal D-proofs with conclusions of even symbolic length, and there are 126779 minimal D-proofs with conclusions of odd symbolic length. [3106/129885 ≈ 2.39% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 5 10 6 11 13 12 22 13 52 14 66 15 214 16 50 17 373 18 281 19 1109 20 96 21 1054 22 281 23 3036 24 138 25 1655 26 261 27 5179 28 146 29 2405 30 167 31 6250 32 139 33 2970 34 104 35 6428 36 88 37 3402 38 98 39 5177 40 95 41 3390 42 56 43 4467 44 103 45 3407 46 64 47 3893 48 57 49 3263 50 52 51 3271 52 73 53 3121 54 38 55 3071 56 47 57 2681 58 35 59 2596 60 33 61 2767 62 64 63 2492 64 37 65 2374 66 41 67 2109 68 21 69 2141 70 12 71 2341 72 14 73 1787 74 21 75 1618 76 15 77 1821 78 12 79 1696 80 11 81 1405 82 8 83 1516 84 10 85 1372 86 16 87 1376 88 14 89 1397 90 9 91 1112 92 9 93 1040 94 10 95 1203 96 17 97 1004 98 10 99 947 100 4 101 1018 102 5 103 807 104 10 105 693 106 9 107 767 108 10 109 662 110 8 111 624 112 4 113 735 114 2 115 557 116 6 117 558 118 2 119 643 120 1 121 546 122 3 123 509 124 4 125 571 126 5 127 397 128 4 129 435 130 1 131 407 132 1 133 357 134 2 135 347 136 5 137 505 138 4 139 296 140 8 141 245 142 5 143 392 144 2 145 269 146 0 147 307 148 1 149 314 150 4 151 222 152 2 153 207 154 0 155 243 156 1 157 295 158 1 159 231 160 4 161 251 162 1 163 180 164 0 165 167 166 4 167 249 168 2 169 142 170 0 171 212 172 0 173 167 174 1 175 156 176 1 177 162 178 0 179 173 180 0 181 122 182 2 183 148 184 0 185 118 186 1 187 141 188 1 189 133 190 1 191 138 192 1 193 103 194 0 195 103 196 0 197 127 198 1 199 98 200 1 201 93 202 1 203 143 204 1 205 90 206 1 207 98 208 1 209 85 210 1 211 73 212 0 213 57 214 0 215 94 216 0 217 88 218 2 219 77 220 3 221 67 222 2 223 54 224 1 225 53 226 0 227 90 228 1 229 49 230 0 231 70 232 0 233 58 234 1 235 71 236 2 237 60 238 0 239 66 240 2 241 39 242 0 243 41 244 1 245 26 246 0 247 56 248 1 249 32 250 0 251 91 252 0 253 42 254 0 255 47 256 0 257 42 258 0 259 40 260 0 261 20 262 0 263 39 264 0 265 17 266 0 267 46 268 0 269 34 270 0 271 31 272 0 273 17 274 0 275 32 276 0 277 26 278 0 279 35 280 0 281 26 282 0 283 35 284 0 285 26 286 0 287 30 288 0 289 12 290 0 291 23 292 0 293 31 294 0 295 10 296 0 297 16 298 0 299 47 300 0 301 13 302 0 303 40 304 0 305 27 306 0 307 20 308 0 309 15 310 0 311 22 312 0 313 13 314 0 315 23 316 0 317 18 318 0 319 11 320 0 321 19 322 0 323 25 324 0 325 10 326 0 327 11 328 0 329 14 330 0 331 27 332 0 333 12 334 1 335 18 336 0 337 12 338 0 339 9 340 0 341 7 342 0 343 6 344 0 345 16 346 0 347 15 348 0 349 7 350 0 351 10 352 0 353 10 354 0 355 18 356 0 357 9 358 0 359 9 360 0 361 8 362 0 363 16 364 0 365 11 366 0 367 16 368 0 369 9 370 0 371 10 372 0 373 7 374 0 375 11 376 0 377 2 378 0 379 9 380 0 381 6 382 0 383 11 384 0 385 5 386 0 387 11 388 0 389 3 390 0 391 5 392 0 393 7 394 0 395 10 396 0 397 6 398 0 399 7 400 0 401 9 402 0 403 6 404 0 405 14 406 0 407 13 408 0 409 6 410 0 411 4 412 0 413 3 414 0 415 2 416 1 417 3 418 0 419 5 420 0 421 6 422 0 423 3 424 0 425 2 426 0 427 4 428 0 429 3 430 0 431 4 432 0 433 4 434 0 435 4 436 0 437 1 438 0 439 2 440 0 441 5 442 0 443 4 444 0 445 3 446 0 447 8 448 0 449 3 450 0 451 3 452 0 453 3 454 0 455 2 456 0 457 4 458 0 459 7 460 0 461 2 462 0 463 1 464 0 465 0 466 0 467 10 468 0 469 3 470 0 471 2 472 0 473 2 474 0 475 8 476 0 477 2 478 0 479 3 480 0 481 1 482 0 483 1 484 0 485 3 486 0 487 2 488 0 489 0 490 0 491 5 492 0 493 2 494 0 495 2 496 0 497 2 498 0 499 2 500 0

25: Average symbolic conclusion length is 30064575/385789 ≈ 77.93. (Median: 59)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 3197 (×1), respectively.
    There are 9376 minimal D-proofs with conclusions of even symbolic length, and there are 376413 minimal D-proofs with conclusions of odd symbolic length. [9376/385789 ≈ 2.43% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 2 8 3 9 5 10 8 11 31 12 36 13 89 14 66 15 229 16 201 17 741 18 156 19 1058 20 682 21 2875 22 264 23 2750 24 758 25 7804 26 396 27 4442 28 739 29 12846 30 409 31 6278 32 501 33 15642 34 378 35 7671 36 292 37 16095 38 260 39 9232 40 279 41 14163 42 283 43 9513 44 204 45 12026 46 302 47 9594 48 197 49 10590 50 239 51 9480 52 148 53 8823 54 216 55 8836 56 149 57 8078 58 138 59 8937 60 97 61 6664 62 118 63 8091 64 143 65 6921 66 107 67 7996 68 143 69 5645 70 70 71 6886 72 58 73 5725 74 77 75 6770 76 61 77 4782 78 56 79 5617 80 70 81 4445 82 55 83 6034 84 43 85 3882 86 49 87 4585 88 44 89 4058 90 47 91 4616 92 51 93 3082 94 37 95 4284 96 31 97 2958 98 44 99 3634 100 35 101 2908 102 39 103 3182 104 22 105 2251 106 21 107 3542 108 22 109 2054 110 29 111 2537 112 26 113 2203 114 13 115 2295 116 17 117 1774 118 24 119 2601 120 10 121 1573 122 23 123 2089 124 7 125 1757 126 19 127 2087 128 20 129 1317 130 11 131 2045 132 15 133 1227 134 16 135 1610 136 9 137 1331 138 13 139 1466 140 20 141 979 142 19 143 1504 144 10 145 1041 146 12 147 1381 148 7 149 1110 150 7 151 1119 152 11 153 773 154 7 155 1219 156 3 157 800 158 8 159 1052 160 3 161 848 162 10 163 861 164 7 165 597 166 3 167 1171 168 9 169 620 170 5 171 690 172 6 173 719 174 2 175 612 176 6 177 616 178 2 179 785 180 5 181 478 182 5 183 596 184 3 185 565 186 2 187 719 188 4 189 396 190 1 191 612 192 4 193 422 194 3 195 474 196 0 197 464 198 2 199 442 200 1 201 340 202 1 203 531 204 2 205 374 206 4 207 470 208 3 209 335 210 3 211 322 212 7 213 280 214 3 215 402 216 2 217 301 218 3 219 422 220 5 221 310 222 7 223 246 224 3 225 220 226 2 227 404 228 2 229 234 230 1 231 248 232 3 233 248 234 1 235 234 236 1 237 266 238 2 239 271 240 0 241 174 242 4 243 214 244 2 245 201 246 1 247 218 248 0 249 170 250 1 251 334 252 1 253 212 254 0 255 177 256 0 257 245 258 3 259 162 260 0 261 123 262 1 263 171 264 0 265 122 266 0 267 179 268 1 269 140 270 0 271 140 272 0 273 107 274 0 275 145 276 0 277 175 278 0 279 136 280 0 281 125 282 0 283 156 284 0 285 133 286 0 287 164 288 1 289 104 290 0 291 98 292 0 293 103 294 1 295 114 296 0 297 103 298 0 299 106 300 1 301 96 302 1 303 99 304 0 305 113 306 0 307 101 308 1 309 89 310 1 311 86 312 0 313 66 314 1 315 107 316 0 317 86 318 0 319 83 320 1 321 82 322 0 323 98 324 0 325 74 326 0 327 90 328 0 329 93 330 0 331 67 332 0 333 77 334 2 335 63 336 1 337 73 338 0 339 47 340 0 341 65 342 0 343 54 344 0 345 37 346 0 347 118 348 0 349 45 350 0 351 44 352 0 353 43 354 0 355 53 356 0 357 60 358 0 359 75 360 0 361 30 362 2 363 67 364 0 365 52 366 0 367 56 368 0 369 48 370 0 371 39 372 0 373 39 374 0 375 38 376 0 377 53 378 1 379 34 380 1 381 60 382 0 383 38 384 1 385 27 386 0 387 41 388 1 389 45 390 0 391 26 392 1 393 27 394 0 395 49 396 0 397 34 398 0 399 31 400 0 401 27 402 0 403 29 404 0 405 50 406 0 407 47 408 0 409 36 410 0 411 34 412 0 413 24 414 0 415 21 416 1 417 35 418 1 419 30 420 0 421 24 422 0 423 19 424 0 425 25 426 0 427 30 428 0 429 16 430 0 431 19 432 0 433 31 434 0 435 22 436 0 437 22 438 0 439 13 440 0 441 16 442 0 443 29 444 0 445 13 446 0 447 28 448 0 449 23 450 0 451 22 452 0 453 15 454 0 455 16 456 0 457 20 458 0 459 39 460 0 461 18 462 0 463 16 464 0 465 10 466 0 467 11 468 0 469 22 470 0 471 16 472 0 473 12 474 0 475 20 476 0 477 25 478 0 479 16 480 0 481 9 482 0 483 15 484 0 485 24 486 0 487 19 488 0 489 35 490 0 491 21 492 0 493 19 494 0 495 11 496 0 497 10 498 0 499 11 500 0

27: Average symbolic conclusion length is 102125860/1149058 ≈ 88.88. (Median: 67)
    Minimum and maximum symbolic conclusion lengths are 7 (×3) and 5171 (×1), respectively.
    There are 28232 minimal D-proofs with conclusions of even symbolic length, and there are 1120826 minimal D-proofs with conclusions of odd symbolic length. [28232/1149058 ≈ 2.46% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 3 8 2 9 7 10 18 11 20 12 37 13 113 14 110 15 324 16 179 17 710 18 593 19 2091 20 408 21 3012 22 1767 23 8037 24 738 25 7160 26 1981 27 19712 28 1011 29 11548 30 1902 31 31828 32 1087 33 16454 34 1382 35 39970 36 1029 37 20778 38 988 39 41654 40 790 41 24153 42 845 43 37639 44 852 45 25390 46 670 47 33141 48 799 49 24974 50 572 51 29299 52 691 53 25553 54 498 55 26270 56 664 57 23011 58 424 59 23667 60 442 61 23752 62 474 63 22236 64 378 65 21354 66 447 67 20078 68 382 69 20858 70 405 71 21073 72 266 73 17854 74 304 75 17487 76 201 77 18105 78 251 79 17888 80 250 81 14601 82 187 83 15834 84 175 85 14665 86 217 87 15212 88 147 89 13781 90 155 91 12819 92 178 93 11950 94 133 95 13650 96 116 97 10746 98 150 99 11040 100 114 101 11323 102 119 103 10644 104 119 105 8663 106 81 107 9869 108 81 109 8327 110 119 111 8362 112 117 113 8849 114 78 115 7587 116 68 117 6664 118 68 119 8351 120 74 121 6513 122 70 123 6683 124 58 125 7135 126 58 127 5896 128 72 129 5619 130 53 131 6212 132 64 133 5106 134 69 135 5039 136 42 137 6145 138 53 139 4779 140 70 141 4051 142 70 143 5172 144 59 145 3793 146 48 147 4313 148 35 149 4496 150 23 151 3589 152 59 153 3352 154 30 155 3914 156 23 157 3691 158 30 159 3349 160 22 161 3588 162 36 163 2985 164 40 165 2647 166 32 167 3446 168 16 169 2710 170 27 171 2918 172 27 173 2658 174 16 175 2506 176 12 177 2603 178 19 179 2843 180 15 181 1997 182 26 183 2295 184 13 185 2135 186 19 187 2307 188 12 189 1869 190 14 191 2457 192 13 193 1734 194 21 195 1893 196 13 197 2235 198 14 199 1622 200 12 201 1389 202 16 203 2179 204 14 205 1424 206 13 207 1757 208 12 209 1596 210 16 211 1290 212 16 213 1054 214 18 215 1718 216 14 217 1454 218 6 219 1437 220 9 221 1363 222 16 223 1229 224 15 225 901 226 10 227 1432 228 11 229 997 230 13 231 1094 232 8 233 1039 234 10 235 1238 236 4 237 1058 238 12 239 1266 240 13 241 819 242 10 243 1007 244 14 245 801 246 9 247 928 248 8 249 670 250 4 251 1115 252 8 253 776 254 8 255 911 256 3 257 893 258 2 259 779 260 7 261 566 262 5 263 832 264 3 265 517 266 3 267 1039 268 2 269 675 270 3 271 605 272 5 273 499 274 2 275 731 276 1 277 588 278 2 279 648 280 1 281 484 282 4 283 636 284 2 285 451 286 2 287 711 288 2 289 424 290 4 291 466 292 4 293 466 294 3 295 427 296 1 297 432 298 1 299 689 300 2 301 296 302 3 303 532 304 2 305 432 306 2 307 515 308 1 309 355 310 4 311 492 312 5 313 286 314 1 315 450 316 5 317 452 318 1 319 319 320 1 321 298 322 1 323 428 324 1 325 300 326 2 327 374 328 0 329 276 330 2 331 484 332 2 333 251 334 0 335 353 336 5 337 293 338 4 339 329 340 1 341 275 342 2 343 245 344 1 345 198 346 2 347 378 348 1 349 263 350 4 351 227 352 0 353 190 354 1 355 319 356 2 357 260 358 3 359 275 360 2 361 169 362 2 363 297 364 2 365 213 366 1 367 252 368 0 369 173 370 1 371 234 372 1 373 150 374 1 375 202 376 0 377 216 378 0 379 225 380 1 381 139 382 1 383 242 384 1 385 137 386 1 387 242 388 0 389 151 390 1 391 180 392 1 393 107 394 3 395 242 396 0 397 182 398 0 399 145 400 0 401 144 402 0 403 135 404 0 405 133 406 0 407 318 408 0 409 144 410 0 411 195 412 0 413 140 414 0 415 153 416 0 417 133 418 1 419 143 420 3 421 92 422 4 423 115 424 0 425 102 426 0 427 178 428 2 429 84 430 0 431 128 432 0 433 109 434 0 435 103 436 1 437 126 438 0 439 88 440 0 441 60 442 0 443 163 444 0 445 77 446 0 447 155 448 0 449 101 450 0 451 109 452 1 453 84 454 0 455 96 456 0 457 86 458 0 459 168 460 0 461 98 462 0 463 68 464 0 465 65 466 2 467 111 468 0 469 62 470 0 471 98 472 0 473 61 474 1 475 122 476 1 477 104 478 1 479 104 480 0 481 50 482 0 483 59 484 0 485 80 486 0 487 92 488 0 489 60 490 0 491 124 492 1 493 60 494 1 495 73 496 0 497 55 498 0 499 68 500 1

29: Average symbolic conclusion length is 347393279/3449251 ≈ 100.72. (Median: 75)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 8365 (×1), respectively.
    There are 85734 minimal D-proofs with conclusions of even symbolic length, and there are 3363517 minimal D-proofs with conclusions of odd symbolic length. [85734/3449251 ≈ 2.49% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 2 9 10 10 10 11 28 12 57 13 97 14 128 15 385 16 392 17 1164 18 566 19 2315 20 1766 21 6486 22 1214 23 8459 24 4381 25 21387 26 2040 27 18980 28 5201 29 50571 30 2735 31 31262 32 5198 33 80942 34 3069 35 44169 36 4048 37 102450 38 2949 39 55475 40 2875 41 108273 42 2350 43 64446 44 2460 45 100277 46 2416 47 69647 48 1883 49 91413 50 2417 51 70478 52 1692 53 79598 54 2016 55 70998 56 1559 57 72249 58 1957 59 69450 60 1341 61 62577 62 1547 63 67034 64 1304 65 60526 66 1316 67 67274 68 1421 69 52688 70 1129 71 61364 72 1082 73 54022 74 1092 75 61277 76 876 77 47537 78 682 79 53937 80 926 81 45608 82 807 83 55760 84 634 85 40160 86 745 87 46385 88 627 89 42130 90 526 91 47809 92 686 93 34283 94 541 95 43754 96 459 97 34142 98 591 99 39937 100 418 101 32866 102 507 103 35080 104 491 105 28198 106 385 107 37840 108 299 109 25463 110 399 111 29989 112 322 113 26498 114 356 115 27966 116 332 117 21336 118 293 119 29567 120 239 121 20321 122 373 123 24178 124 200 125 21542 126 258 127 23844 128 240 129 17445 130 229 131 24586 132 226 133 16268 134 287 135 19868 136 173 137 17228 138 180 139 18223 140 209 141 13367 142 249 143 19645 144 174 145 13497 146 223 147 16086 148 126 149 14599 150 167 151 15003 152 147 153 10984 154 141 155 16021 156 108 157 10706 158 146 159 13680 160 99 161 11771 162 145 163 11601 164 117 165 8866 166 115 167 14287 168 103 169 8970 170 117 171 10442 172 91 173 10320 174 113 175 9410 176 86 177 8134 178 64 179 11146 180 72 181 7417 182 116 183 9026 184 74 185 8067 186 66 187 9428 188 87 189 6642 190 50 191 8703 192 70 193 6615 194 68 195 7083 196 53 197 7261 198 61 199 7124 200 61 201 5210 202 56 203 7662 204 52 205 5527 206 60 207 7431 208 45 209 6056 210 42 211 5146 212 96 213 4420 214 44 215 6081 216 62 217 4987 218 57 219 5833 220 40 221 4945 222 53 223 4761 224 58 225 3800 226 50 227 6014 228 44 229 3734 230 46 231 4435 232 54 233 4158 234 30 235 3891 236 40 237 4077 238 33 239 4622 240 27 241 3310 242 42 243 3626 244 32 245 3587 246 45 247 3814 248 32 249 2880 250 34 251 4658 252 32 253 3077 254 27 255 3378 256 15 257 3934 258 28 259 2961 260 25 261 2373 262 31 263 3300 264 35 265 2213 266 21 267 3105 268 16 269 2925 270 16 271 2369 272 22 273 2084 274 9 275 2768 276 13 277 2646 278 12 279 2454 280 11 281 2302 282 6 283 2684 284 13 285 2020 286 10 287 3023 288 10 289 2026 290 14 291 2041 292 16 293 2090 294 13 295 1860 296 9 297 1839 298 12 299 2255 300 13 301 1651 302 20 303 1859 304 10 305 1964 306 9 307 1826 308 10 309 1648 310 8 311 1872 312 16 313 1424 314 14 315 1980 316 14 317 1798 318 19 319 1554 320 13 321 1300 322 15 323 1758 324 9 325 1164 326 8 327 1669 328 9 329 1627 330 3 331 1451 332 16 333 1365 334 5 335 1421 336 10 337 1450 338 14 339 1177 340 10 341 1293 342 12 343 1075 344 9 345 887 346 7 347 1813 348 5 349 1047 350 6 351 1150 352 7 353 955 354 7 355 986 356 4 357 1184 358 3 359 1347 360 6 361 857 362 6 363 1166 364 5 365 976 366 14 367 1026 368 12 369 824 370 1 371 960 372 3 373 810 374 8 375 881 376 2 377 1026 378 3 379 1000 380 2 381 967 382 6 383 953 384 12 385 757 386 7 387 888 388 6 389 833 390 8 391 697 392 6 393 679 394 5 395 1019 396 7 397 746 398 6 399 714 400 4 401 704 402 3 403 604 404 3 405 598 406 3 407 927 408 4 409 699 410 4 411 788 412 2 413 727 414 3 415 626 416 2 417 633 418 3 419 644 420 8 421 495 422 7 423 563 424 5 425 534 426 6 427 699 428 3 429 476 430 4 431 578 432 1 433 696 434 7 435 466 436 4 437 597 438 3 439 487 440 4 441 340 442 4 443 602 444 1 445 411 446 3 447 625 448 1 449 511 450 0 451 434 452 4 453 387 454 1 455 482 456 2 457 451 458 2 459 567 460 1 461 446 462 2 463 398 464 0 465 314 466 1 467 492 468 6 469 317 470 2 471 383 472 2 473 391 474 1 475 407 476 1 477 429 478 4 479 411 480 2 481 298 482 2 483 295 484 2 485 477 486 1 487 383 488 0 489 369 490 1 491 474 492 1 493 364 494 1 495 314 496 3 497 375 498 2 499 236 500 0

31: Average symbolic conclusion length is 1183839544/10411430 ≈ 113.71. (Median: 83)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 13533 (×1), respectively.
    There are 263350 minimal D-proofs with conclusions of even symbolic length, and there are 10148080 minimal D-proofs with conclusions of odd symbolic length. [263350/10411430 ≈ 2.53% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 2 9 12 10 13 11 40 12 50 13 148 14 220 15 496 16 445 17 1440 18 1266 19 4065 20 1677 21 6995 22 4940 23 18287 24 3364 25 23519 26 11439 27 58024 28 5677 29 50955 30 13990 31 130043 32 7587 33 83242 34 14062 35 205922 36 8401 37 117460 38 11413 39 263188 40 8190 41 149547 42 8670 43 285184 44 7121 45 175382 46 7493 47 270463 48 7113 49 187585 50 6076 51 251182 52 6884 53 193915 54 5273 55 224453 56 6264 57 190580 58 4767 59 204355 60 5483 61 190347 62 4580 63 188497 64 4587 65 180743 66 4123 67 174630 68 4259 69 180428 70 4241 71 173682 72 3459 73 162459 74 3931 75 158590 76 3028 77 164880 78 3029 79 161290 80 2733 81 141757 82 2659 83 146505 84 2405 85 142169 86 2761 87 146386 88 2151 89 129841 90 2021 91 129489 92 2205 93 122699 94 2050 95 134870 96 1747 97 110161 98 2075 99 114688 100 1555 101 113097 102 1486 103 115665 104 1840 105 93934 106 1397 107 106010 108 1242 109 91654 110 1506 111 96076 112 1279 113 92782 114 1176 115 87603 116 1294 117 75483 118 1053 119 91652 120 924 121 72938 122 1197 123 75982 124 1065 125 77692 126 824 127 72045 128 994 129 64593 130 801 131 73655 132 963 133 60070 134 973 135 62185 136 767 137 68799 138 753 139 58726 140 807 141 50568 142 804 143 61499 144 714 145 48704 146 755 147 52751 148 703 149 54060 150 567 151 47616 152 864 153 43220 154 493 155 50134 156 505 157 42826 158 588 159 42443 160 433 161 45667 162 504 163 40223 164 502 165 33919 166 427 167 43864 168 429 169 35480 170 440 171 35769 172 443 173 36362 174 356 175 33517 176 456 177 32136 178 322 179 36998 180 268 181 28120 182 409 183 31199 184 298 185 30960 186 331 187 29824 188 324 189 25112 190 269 191 31790 192 297 193 24368 194 294 195 26158 196 202 197 29180 198 276 199 23896 200 282 201 21018 202 260 203 27881 204 216 205 20130 206 251 207 24113 208 192 209 22933 210 189 211 20140 212 233 213 16508 214 257 215 23625 216 163 217 19852 218 246 219 19999 220 169 221 19499 222 241 223 17895 224 194 225 14665 226 180 227 20481 228 169 229 15252 230 188 231 15833 232 178 233 16106 234 181 235 16220 236 150 237 15102 238 164 239 18728 240 118 241 12511 242 159 243 14779 244 139 245 12941 246 134 247 14319 248 149 249 11187 250 104 251 15199 252 122 253 11690 254 120 255 12742 256 88 257 14388 258 110 259 12359 260 109 261 9610 262 110 263 13278 264 106 265 8856 266 113 267 13854 268 70 269 10776 270 90 271 10230 272 80 273 8420 274 62 275 11499 276 58 277 9588 278 74 279 10029 280 48 281 8532 282 103 283 9302 284 52 285 7377 286 49 287 11577 288 48 289 7563 290 93 291 8334 292 61 293 8206 294 72 295 7401 296 66 297 7259 298 64 299 10623 300 41 301 6024 302 75 303 7946 304 53 305 7564 306 56 307 7976 308 60 309 5650 310 51 311 8286 312 64 313 5452 314 47 315 7270 316 69 317 7176 318 51 319 5964 320 65 321 5191 322 63 323 6913 324 56 325 5024 326 62 327 6597 328 27 329 5575 330 36 331 7115 332 52 333 4639 334 40 335 6405 336 34 337 5108 338 35 339 5536 340 45 341 4882 342 74 343 4789 344 46 345 3791 346 32 347 6906 348 31 349 4459 350 31 351 4366 352 41 353 4245 354 28 355 4451 356 33 357 4252 358 26 359 5462 360 28 361 3659 362 33 363 5207 364 35 365 4065 366 33 367 4477 368 53 369 3393 370 33 371 4232 372 27 373 2959 374 33 375 3890 376 24 377 4104 378 17 379 4031 380 23 381 2962 382 23 383 4341 384 27 385 2713 386 34 387 4149 388 24 389 3014 390 25 391 3165 392 30 393 2547 394 45 395 4458 396 17 397 3248 398 27 399 3054 400 18 401 2774 402 19 403 2736 404 16 405 2283 406 9 407 4268 408 10 409 2393 410 16 411 3621 412 18 413 2951 414 10 415 2670 416 13 417 2591 418 15 419 3202 420 20 421 2176 422 29 423 2446 424 27 425 2177 426 35 427 3125 428 21 429 1992 430 12 431 2662 432 16 433 2012 434 12 435 2473 436 12 437 2301 438 14 439 2071 440 18 441 1566 442 19 443 2720 444 14 445 1602 446 19 447 2642 448 9 449 2171 450 12 451 1962 452 11 453 1713 454 15 455 2102 456 9 457 1885 458 17 459 3023 460 6 461 1831 462 9 463 1712 464 9 465 1511 466 4 467 2217 468 11 469 1434 470 21 471 1646 472 9 473 1559 474 11 475 2005 476 6 477 1751 478 9 479 2007 480 15 481 1299 482 8 483 1611 484 8 485 1632 486 11 487 1967 488 8 489 1256 490 4 491 2209 492 4 493 1382 494 8 495 1563 496 6 497 1474 498 13 499 1434 500 5

33: Average symbolic conclusion length is 4036708131/31559297 ≈ 127.91. (Median: 91)
    Minimum and maximum symbolic conclusion lengths are 6 (×1) and 21895 (×1), respectively.
    There are 809654 minimal D-proofs with conclusions of even symbolic length, and there are 30749643 minimal D-proofs with conclusions of odd symbolic length. [809654/31559297 ≈ 2.57% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 6 10 17 11 36 12 63 13 154 14 183 15 559 16 696 17 1811 18 1379 19 4593 20 3904 21 12347 22 4844 23 21011 24 14054 25 53122 26 9594 27 64962 28 29596 29 154856 30 15653 31 136178 32 37132 33 335591 34 20668 35 223478 36 38268 37 530433 38 23518 39 317827 40 32692 41 684870 42 23374 43 403709 44 25866 45 750533 46 20887 47 475990 48 21885 49 730719 50 21162 51 514198 52 17777 53 683775 54 19806 55 540043 56 15816 57 623238 58 18658 59 542991 60 14058 61 557855 62 17074 63 537174 64 13261 65 525315 66 14656 67 537192 68 13147 69 469494 70 12980 71 520547 72 12214 73 467500 74 12368 75 513251 76 11030 77 426005 78 9625 79 481931 80 10491 81 424582 82 8844 83 486188 84 8350 85 380840 86 8868 87 430778 88 7625 89 393691 90 7105 91 445055 92 8084 93 340475 94 6650 95 406786 96 6021 97 342157 98 6994 99 394740 100 5660 101 322143 102 5773 103 353546 104 6324 105 301317 106 5183 107 370530 108 4593 109 272571 110 5300 111 312333 112 4192 113 278312 114 4318 115 306181 116 4854 117 236400 118 4085 119 300172 120 3336 121 227194 122 4517 123 264999 124 3330 125 231273 126 3588 127 250943 128 3678 129 199327 130 3051 131 264934 132 2691 133 187429 134 3727 135 219697 136 2629 137 194972 138 2797 139 212292 140 3041 141 160974 142 3035 143 223664 144 2416 145 156292 146 2994 147 181985 148 2233 149 168888 150 2504 151 174144 152 2472 153 135137 154 2276 155 185964 156 1740 157 128663 158 2339 159 159757 160 1628 161 141122 162 2129 163 143103 164 1957 165 112622 166 1743 167 163987 168 1520 169 110561 170 1957 171 128103 172 1587 173 122068 174 1543 175 120651 176 1482 177 100263 178 1350 179 135476 180 1119 181 93608 182 1888 183 112492 184 1207 185 102944 186 1159 187 112553 188 1306 189 84713 190 1099 191 113550 192 1088 193 85248 194 1261 195 92508 196 896 197 92029 198 971 199 92785 200 1042 201 70374 202 1094 203 99527 204 930 205 70760 206 1109 207 93192 208 786 209 80807 210 779 211 73946 212 1155 213 61941 214 842 215 81236 216 845 217 65025 218 847 219 74201 220 727 221 67541 222 847 223 67398 224 844 225 52983 226 637 227 81011 228 712 229 53101 230 754 231 61907 232 734 233 57670 234 672 235 55507 236 698 237 51981 238 597 239 64210 240 574 241 48496 242 708 243 52625 244 492 245 51113 246 589 247 54778 248 599 249 41676 250 522 251 59976 252 540 253 41394 254 564 255 47053 256 392 257 51013 258 441 259 45383 260 445 261 35895 262 464 263 49704 264 479 265 34586 266 468 267 45461 268 380 269 41977 270 376 271 37524 272 493 273 32632 274 266 275 42144 276 302 277 36842 278 392 279 37438 280 277 281 34631 282 315 283 36400 284 367 285 28951 286 253 287 43686 288 247 289 30014 290 262 291 32174 292 375 293 31521 294 273 295 29817 296 272 297 27473 298 250 299 34871 300 208 301 25409 302 341 303 28133 304 225 305 28259 306 255 307 28790 308 255 309 24004 310 206 311 29851 312 261 313 22984 314 271 315 28994 316 278 317 28139 318 251 319 24556 320 210 321 20325 322 277 323 28291 324 194 325 18929 326 246 327 25582 328 191 329 22767 330 183 331 22349 332 276 333 20244 334 198 335 23788 336 192 337 21617 338 193 339 20304 340 145 341 20804 342 264 343 18580 344 235 345 15335 346 176 347 27212 348 164 349 17191 350 161 351 18502 352 158 353 16670 354 161 355 16910 356 129 357 17141 358 136 359 21335 360 122 361 14849 362 186 363 18463 364 109 365 16334 366 131 367 17014 368 211 369 13651 370 141 371 16833 372 158 373 12905 374 129 375 14482 376 86 377 16905 378 110 379 16425 380 79 381 13785 382 105 383 16704 384 129 385 12405 386 115 387 15070 388 105 389 13824 390 100 391 12330 392 116 393 10914 394 119 395 16308 396 113 397 13303 398 92 399 12825 400 88 401 11909 402 104 403 11096 404 105 405 9425 406 80 407 14540 408 62 409 10337 410 105 411 13341 412 71 413 12400 414 85 415 10947 416 57 417 11086 418 56 419 12218 420 110 421 8837 422 89 423 10311 424 93 425 9316 426 92 427 11943 428 106 429 8657 430 82 431 11117 432 84 433 9882 434 88 435 9260 436 59 437 11074 438 76 439 8859 440 81 441 6964 442 81 443 11024 444 59 445 7224 446 93 447 10079 448 61 449 8898 450 61 451 8009 452 68 453 7187 454 58 455 8976 456 52 457 7925 458 56 459 9934 460 48 461 8407 462 56 463 6899 464 51 465 6291 466 45 467 8997 468 74 469 5984 470 51 471 7337 472 89 473 6844 474 46 475 8099 476 63 477 7129 478 39 479 7915 480 38 481 5798 482 62 483 6210 484 37 485 8097 486 42 487 7452 488 44 489 5946 490 36 491 8371 492 59 493 6033 494 47 495 6064 496 28 497 6930 498 45 499 5610 500 51