m-plot_data_x200.txt

1: Average symbolic conclusion length is 21/1 ≈ 21.00. (Median: 21)
   Minimum and maximum symbolic conclusion lengths are 21 (×1) and 21 (×1), respectively.
   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 17/1 ≈ 17.00. (Median: 17)
   Minimum and maximum symbolic conclusion lengths are 17 (×1) and 17 (×1), respectively.
   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 1

5: Average symbolic conclusion length is 12/1 ≈ 12.00. (Median: 12)
   Minimum and maximum symbolic conclusion lengths are 12 (×1) and 12 (×1), respectively.
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 0 minimal D-proofs with conclusions of odd symbolic length. [1/1 ≈ 100.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 1

7: Average symbolic conclusion length is 32/3 ≈ 10.67. (Median: 11)
   Minimum and maximum symbolic conclusion lengths are 9 (×1) and 12 (×1), respectively.
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there are 2 minimal D-proofs with conclusions of odd symbolic length. [1/3 ≈ 33.33% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 1 12 1

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

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

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

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

17: Average symbolic conclusion length is 866/37 ≈ 23.41. (Median: 21)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 50 (×1), respectively.
    There are 17 minimal D-proofs with conclusions of even symbolic length, and there are 20 minimal D-proofs with conclusions of odd symbolic length. [17/37 ≈ 45.95% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 0 10 1 11 2 12 1 13 2 14 1 15 1 16 1 17 2 18 2 19 2 20 2 21 1 22 0 23 0 24 3 25 1 26 0 27 2 28 2 29 0 30 1 31 2 32 0 33 0 34 0 35 2 36 1 37 0 38 1 39 1 40 0 41 0 42 0 43 0 44 0 45 1 46 0 47 0 48 0 49 0 50 1

19: Average symbolic conclusion length is 1310/56 ≈ 23.39. (Median: 23.50)
    Minimum and maximum symbolic conclusion lengths are 3 (×1) and 44 (×1), respectively.
    There are 30 minimal D-proofs with conclusions of even symbolic length, and there are 26 minimal D-proofs with conclusions of odd symbolic length. [30/56 ≈ 53.57% even]
1 0 2 0 3 1 4 0 5 0 6 0 7 0 8 1 9 2 10 1 11 1 12 2 13 1 14 4 15 3 16 4 17 2 18 1 19 1 20 1 21 1 22 1 23 1 24 3 25 0 26 2 27 1 28 3 29 1 30 1 31 4 32 2 33 1 34 0 35 3 36 0 37 1 38 1 39 2 40 0 41 0 42 2 43 0 44 1

21: Average symbolic conclusion length is 2181/87 ≈ 25.07. (Median: 24)
    Minimum and maximum symbolic conclusion lengths are 6 (×1) and 75 (×1), respectively.
    There are 46 minimal D-proofs with conclusions of even symbolic length, and there are 41 minimal D-proofs with conclusions of odd symbolic length. [46/87 ≈ 52.87% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 2 10 0 11 1 12 2 13 1 14 3 15 2 16 3 17 3 18 4 19 4 20 4 21 1 22 6 23 4 24 6 25 3 26 4 27 2 28 2 29 5 30 2 31 2 32 3 33 3 34 2 35 4 36 1 37 0 38 0 39 1 40 2 41 0 42 1 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 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 1

23: Average symbolic conclusion length is 3704/140 ≈ 26.46. (Median: 25)
    Minimum and maximum symbolic conclusion lengths are 10 (×3) and 60 (×1), respectively.
    There are 78 minimal D-proofs with conclusions of even symbolic length, and there are 62 minimal D-proofs with conclusions of odd symbolic length. [78/140 ≈ 55.71% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 3 11 1 12 3 13 2 14 1 15 2 16 5 17 2 18 6 19 7 20 5 21 5 22 9 23 8 24 5 25 9 26 7 27 4 28 7 29 6 30 7 31 1 32 5 33 3 34 1 35 3 36 3 37 2 38 2 39 2 40 4 41 1 42 0 43 2 44 3 45 0 46 1 47 0 48 0 49 0 50 0 51 0 52 0 53 0 54 0 55 2 56 0 57 0 58 0 59 0 60 1

25: Average symbolic conclusion length is 6553/227 ≈ 28.87. (Median: 28)
    Minimum and maximum symbolic conclusion lengths are 8 (×2) and 69 (×1), respectively.
    There are 122 minimal D-proofs with conclusions of even symbolic length, and there are 105 minimal D-proofs with conclusions of odd symbolic length. [122/227 ≈ 53.74% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 2 9 0 10 0 11 1 12 2 13 3 14 6 15 3 16 6 17 5 18 8 19 9 20 12 21 8 22 9 23 13 24 8 25 5 26 6 27 7 28 6 29 14 30 10 31 4 32 3 33 11 34 4 35 2 36 12 37 6 38 3 39 3 40 7 41 0 42 2 43 2 44 6 45 1 46 1 47 4 48 3 49 1 50 0 51 0 52 1 53 0 54 1 55 0 56 0 57 1 58 1 59 1 60 2 61 0 62 0 63 0 64 0 65 0 66 0 67 0 68 1 69 1

27: Average symbolic conclusion length is 11273/369 ≈ 30.55. (Median: 29)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 85 (×1), respectively.
    There are 180 minimal D-proofs with conclusions of even symbolic length, and there are 189 minimal D-proofs with conclusions of odd symbolic length. [180/369 ≈ 48.78% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 2 11 1 12 1 13 2 14 2 15 8 16 8 17 10 18 8 19 10 20 10 21 17 22 15 23 16 24 17 25 12 26 14 27 18 28 8 29 20 30 8 31 10 32 10 33 14 34 11 35 8 36 7 37 12 38 7 39 5 40 14 41 6 42 5 43 4 44 10 45 2 46 3 47 4 48 4 49 1 50 4 51 4 52 4 53 2 54 2 55 1 56 1 57 0 58 0 59 0 60 1 61 0 62 0 63 0 64 1 65 0 66 1 67 0 68 0 69 0 70 0 71 0 72 0 73 0 74 0 75 0 76 0 77 0 78 1 79 0 80 1 81 0 82 0 83 0 84 0 85 1

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

31: Average symbolic conclusion length is 30976/918 ≈ 33.74. (Median: 32)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 99 (×1), respectively.
    There are 436 minimal D-proofs with conclusions of even symbolic length, and there are 482 minimal D-proofs with conclusions of odd symbolic length. [436/918 ≈ 47.49% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 2 10 0 11 1 12 2 13 4 14 7 15 7 16 4 17 11 18 13 19 24 20 15 21 22 22 20 23 22 24 35 25 41 26 31 27 37 28 39 29 30 30 21 31 41 32 33 33 29 34 43 35 37 36 21 37 26 38 37 39 19 40 17 41 34 42 19 43 14 44 19 45 20 46 9 47 10 48 11 49 17 50 5 51 6 52 9 53 9 54 3 55 1 56 3 57 2 58 2 59 2 60 1 61 1 62 3 63 3 64 3 65 2 66 1 67 0 68 3 69 2 70 3 71 0 72 0 73 1 74 0 75 1 76 0 77 1 78 2 79 1 80 2 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 0 96 0 97 0 98 0 99 1

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

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

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

39: Average symbolic conclusion length is 259494/6254 ≈ 41.49. (Median: 39)
    Minimum and maximum symbolic conclusion lengths are 8 (×2) and 136 (×1), respectively.
    There are 3324 minimal D-proofs with conclusions of even symbolic length, and there are 2930 minimal D-proofs with conclusions of odd symbolic length. [3324/6254 ≈ 53.15% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 2 9 1 10 0 11 5 12 5 13 5 14 6 15 11 16 12 17 24 18 24 19 28 20 41 21 38 22 61 23 77 24 89 25 89 26 121 27 136 28 153 29 168 30 205 31 152 32 205 33 221 34 221 35 207 36 255 37 225 38 186 39 191 40 210 41 156 42 203 43 215 44 199 45 126 46 162 47 164 48 99 49 113 50 184 51 101 52 83 53 101 54 112 55 41 56 69 57 67 58 79 59 27 60 44 61 46 62 45 63 25 64 29 65 21 66 29 67 19 68 21 69 13 70 20 71 17 72 17 73 16 74 17 75 12 76 12 77 3 78 18 79 10 80 11 81 6 82 7 83 9 84 7 85 8 86 12 87 7 88 17 89 6 90 4 91 2 92 2 93 5 94 5 95 3 96 5 97 0 98 2 99 3 100 3 101 0 102 1 103 1 104 1 105 1 106 0 107 2 108 2 109 1 110 0 111 2 112 1 113 1 114 0 115 0 116 0 117 0 118 3 119 0 120 0 121 0 122 0 123 1 124 0 125 0 126 0 127 0 128 1 129 0 130 0 131 0 132 0 133 1 134 1 135 0 136 1

41: Average symbolic conclusion length is 439430/10109 ≈ 43.47. (Median: 41)
    Minimum and maximum symbolic conclusion lengths are 6 (×1) and 163 (×1), respectively.
    There are 5311 minimal D-proofs with conclusions of even symbolic length, and there are 4798 minimal D-proofs with conclusions of odd symbolic length. [5311/10109 ≈ 52.54% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 2 8 1 9 3 10 2 11 3 12 3 13 7 14 8 15 14 16 15 17 22 18 24 19 27 20 55 21 57 22 58 23 85 24 108 25 111 26 174 27 184 28 204 29 195 30 287 31 272 32 272 33 317 34 336 35 300 36 352 37 391 38 334 39 286 40 366 41 349 42 283 43 356 44 301 45 211 46 275 47 297 48 245 49 181 50 260 51 203 52 154 53 166 54 242 55 106 56 115 57 116 58 150 59 59 60 84 61 78 62 80 63 50 64 65 65 55 66 56 67 40 68 51 69 26 70 35 71 28 72 29 73 25 74 42 75 28 76 20 77 18 78 27 79 21 80 27 81 11 82 17 83 14 84 18 85 10 86 19 87 13 88 15 89 14 90 7 91 8 92 12 93 6 94 15 95 7 96 16 97 6 98 7 99 3 100 4 101 1 102 6 103 2 104 5 105 2 106 3 107 1 108 4 109 1 110 3 111 1 112 1 113 1 114 0 115 2 116 3 117 1 118 1 119 0 120 1 121 1 122 4 123 0 124 0 125 0 126 1 127 1 128 2 129 1 130 1 131 0 132 0 133 0 134 1 135 0 136 0 137 0 138 1 139 0 140 0 141 0 142 0 143 0 144 1 145 0 146 1 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 1 156 1 157 0 158 0 159 0 160 0 161 0 162 0 163 1

43: Average symbolic conclusion length is 746525/16460 ≈ 45.35. (Median: 43)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 178 (×1), respectively.
    There are 8501 minimal D-proofs with conclusions of even symbolic length, and there are 7959 minimal D-proofs with conclusions of odd symbolic length. [8501/16460 ≈ 51.65% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 1 8 0 9 0 10 2 11 6 12 7 13 7 14 9 15 10 16 14 17 21 18 32 19 35 20 59 21 61 22 76 23 105 24 155 25 152 26 182 27 235 28 271 29 299 30 375 31 404 32 396 33 418 34 539 35 504 36 491 37 558 38 512 39 492 40 537 41 636 42 485 43 484 44 498 45 464 46 414 47 534 48 485 49 317 50 356 51 417 52 344 53 255 54 378 55 253 56 231 57 208 58 300 59 155 60 153 61 173 62 188 63 94 64 126 65 96 66 99 67 88 68 91 69 59 70 72 71 56 72 62 73 49 74 61 75 35 76 58 77 25 78 55 79 30 80 38 81 25 82 36 83 36 84 34 85 27 86 30 87 17 88 39 89 18 90 24 91 16 92 27 93 14 94 25 95 9 96 17 97 14 98 14 99 9 100 13 101 6 102 14 103 5 104 9 105 2 106 7 107 3 108 8 109 3 110 7 111 1 112 5 113 2 114 9 115 1 116 6 117 0 118 2 119 1 120 0 121 1 122 3 123 1 124 0 125 1 126 2 127 1 128 4 129 1 130 0 131 1 132 0 133 1 134 1 135 0 136 1 137 1 138 3 139 0 140 1 141 0 142 1 143 1 144 0 145 0 146 0 147 0 148 0 149 0 150 0 151 0 152 0 153 0 154 0 155 0 156 0 157 2 158 1 159 0 160 1 161 0 162 0 163 1 164 1 165 0 166 0 167 1 168 2 169 0 170 0 171 0 172 2 173 0 174 0 175 0 176 0 177 0 178 1

45: Average symbolic conclusion length is 1267094/26753 ≈ 47.36. (Median: 45)
    Minimum and maximum symbolic conclusion lengths are 9 (×4) and 235 (×1), respectively.
    There are 13637 minimal D-proofs with conclusions of even symbolic length, and there are 13116 minimal D-proofs with conclusions of odd symbolic length. [13637/26753 ≈ 50.97% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 4 10 5 11 3 12 8 13 13 14 12 15 16 16 30 17 23 18 39 19 32 20 60 21 80 22 112 23 123 24 166 25 193 26 207 27 286 28 379 29 364 30 422 31 545 32 598 33 607 34 746 35 792 36 661 37 835 38 880 39 847 40 801 41 1014 42 827 43 743 44 822 45 865 46 655 47 809 48 814 49 678 50 596 51 689 52 651 53 407 54 542 55 618 56 466 57 328 58 475 59 362 60 283 61 276 62 374 63 240 64 216 65 217 66 238 67 153 68 174 69 112 70 137 71 120 72 117 73 77 74 111 75 71 76 102 77 72 78 101 79 60 80 75 81 51 82 71 83 51 84 79 85 38 86 58 87 32 88 68 89 37 90 52 91 36 92 58 93 38 94 37 95 16 96 41 97 24 98 45 99 18 100 26 101 19 102 22 103 11 104 23 105 11 106 23 107 5 108 14 109 9 110 13 111 2 112 10 113 5 114 11 115 6 116 7 117 3 118 8 119 3 120 4 121 3 122 11 123 5 124 7 125 0 126 4 127 1 128 6 129 1 130 2 131 0 132 3 133 4 134 1 135 1 136 1 137 0 138 4 139 1 140 1 141 1 142 0 143 3 144 2 145 0 146 0 147 0 148 3 149 0 150 3 151 0 152 1 153 0 154 0 155 0 156 5 157 0 158 1 159 0 160 0 161 1 162 0 163 0 164 2 165 0 166 2 167 1 168 1 169 1 170 0 171 0 172 1 173 0 174 1 175 0 176 1 177 0 178 0 179 0 180 0 181 0 182 0 183 0 184 0 185 0 186 0 187 2 188 1 189 0 190 0 191 0 192 0 193 0 194 0 195 0 196 0 197 0 198 1 199 0 200 0

47: Average symbolic conclusion length is 2134061/43360 ≈ 49.22. (Median: 46)
    Minimum and maximum symbolic conclusion lengths are 7 (×2) and 228 (×1), respectively.
    There are 21959 minimal D-proofs with conclusions of even symbolic length, and there are 21401 minimal D-proofs with conclusions of odd symbolic length. [21959/43360 ≈ 50.64% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 2 8 2 9 0 10 2 11 10 12 7 13 13 14 19 15 15 16 32 17 31 18 56 19 45 20 68 21 88 22 126 23 145 24 190 25 273 26 286 27 324 28 447 29 522 30 541 31 735 32 816 33 836 34 886 35 1143 36 1104 37 1138 38 1305 39 1386 40 1214 41 1441 42 1445 43 1334 44 1224 45 1503 46 1294 47 1186 48 1348 49 1199 50 937 51 1149 52 1210 53 919 54 823 55 1009 56 883 57 588 58 805 59 841 60 565 61 452 62 619 63 513 64 368 65 348 66 418 67 311 68 271 69 226 70 284 71 210 72 222 73 176 74 192 75 159 76 204 77 111 78 172 79 121 80 142 81 87 82 140 83 101 84 153 85 93 86 105 87 67 88 107 89 67 90 97 91 61 92 92 93 55 94 89 95 42 96 88 97 53 98 73 99 44 100 46 101 36 102 55 103 22 104 49 105 21 106 53 107 27 108 32 109 18 110 30 111 9 112 26 113 19 114 23 115 9 116 22 117 7 118 12 119 6 120 13 121 7 122 9 123 3 124 5 125 7 126 13 127 8 128 9 129 1 130 3 131 1 132 11 133 3 134 8 135 3 136 12 137 1 138 6 139 2 140 2 141 1 142 4 143 2 144 4 145 1 146 3 147 0 148 7 149 2 150 1 151 1 152 3 153 1 154 3 155 0 156 2 157 1 158 1 159 0 160 3 161 1 162 2 163 2 164 4 165 1 166 2 167 1 168 1 169 0 170 1 171 0 172 2 173 2 174 1 175 1 176 0 177 0 178 0 179 0 180 0 181 0 182 0 183 1 184 1 185 0 186 0 187 0 188 1 189 0 190 0 191 0 192 0 193 0 194 0 195 0 196 0 197 0 198 0 199 0 200 0

49: Average symbolic conclusion length is 3619350/70709 ≈ 51.19. (Median: 48)
    Minimum and maximum symbolic conclusion lengths are 9 (×2) and 274 (×1), respectively.
    There are 35943 minimal D-proofs with conclusions of even symbolic length, and there are 34766 minimal D-proofs with conclusions of odd symbolic length. [35943/70709 ≈ 50.83% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 2 11 6 12 9 13 11 14 16 15 23 16 40 17 41 18 52 19 71 20 81 21 103 22 174 23 139 24 207 25 289 26 352 27 406 28 532 29 725 30 690 31 876 32 1049 33 1173 34 1253 35 1621 36 1659 37 1669 38 1813 39 2143 40 1901 41 2044 42 2211 43 2121 44 2036 45 2337 46 2409 47 1959 48 1975 49 2074 50 1857 51 1834 52 2121 53 1793 54 1367 55 1561 56 1712 57 1265 58 1252 59 1474 60 1136 61 888 62 1056 63 1080 64 732 65 634 66 775 67 671 68 496 69 481 70 510 71 389 72 462 73 337 74 393 75 262 76 364 77 249 78 303 79 205 80 261 81 179 82 247 83 196 84 245 85 141 86 211 87 130 88 216 89 122 90 186 91 122 92 176 93 130 94 135 95 95 96 144 97 82 98 147 99 86 100 104 101 69 102 114 103 58 104 97 105 54 106 84 107 45 108 49 109 35 110 57 111 28 112 61 113 30 114 51 115 23 116 34 117 17 118 34 119 21 120 38 121 19 122 24 123 17 124 28 125 4 126 21 127 12 128 17 129 6 130 8 131 11 132 17 133 7 134 7 135 7 136 17 137 5 138 13 139 6 140 5 141 2 142 5 143 8 144 6 145 2 146 8 147 4 148 15 149 3 150 6 151 1 152 2 153 2 154 3 155 3 156 2 157 2 158 3 159 0 160 1 161 2 162 4 163 2 164 5 165 4 166 3 167 1 168 2 169 3 170 1 171 0 172 2 173 3 174 3 175 1 176 1 177 3 178 4 179 1 180 2 181 0 182 3 183 1 184 2 185 2 186 1 187 1 188 2 189 0 190 1 191 0 192 1 193 0 194 0 195 1 196 0 197 0 198 2 199 0 200 0

51: Average symbolic conclusion length is 6152621/115604 ≈ 53.22. (Median: 50)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 268 (×1), respectively.
    There are 59267 minimal D-proofs with conclusions of even symbolic length, and there are 56337 minimal D-proofs with conclusions of odd symbolic length. [59267/115604 ≈ 51.27% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 4 10 2 11 6 12 8 13 7 14 20 15 38 16 38 17 48 18 63 19 77 20 113 21 130 22 166 23 211 24 216 25 341 26 450 27 557 28 614 29 857 30 941 31 1016 32 1369 33 1715 34 1652 35 2027 36 2312 37 2452 38 2579 39 3162 40 3124 41 2898 42 3376 43 3578 44 3326 45 3408 46 3880 47 3268 48 3100 49 3513 50 3499 51 2842 52 3290 53 3161 54 2697 55 2590 56 2962 57 2523 58 1972 59 2248 60 2357 61 1787 62 1661 63 1881 64 1479 65 1241 66 1387 67 1390 68 1042 69 883 70 1066 71 851 72 826 73 670 74 732 75 511 76 678 77 480 78 522 79 419 80 533 81 375 82 467 83 349 84 434 85 275 86 391 87 270 88 393 89 251 90 306 91 209 92 331 93 213 94 295 95 178 96 281 97 173 98 263 99 154 100 207 101 138 102 211 103 141 104 173 105 89 106 189 107 94 108 136 109 68 110 123 111 69 112 113 113 48 114 106 115 43 116 73 117 37 118 79 119 42 120 68 121 35 122 55 123 31 124 55 125 25 126 44 127 23 128 40 129 20 130 25 131 21 132 41 133 19 134 24 135 8 136 27 137 15 138 19 139 14 140 13 141 5 142 15 143 12 144 11 145 10 146 17 147 7 148 24 149 8 150 8 151 6 152 9 153 6 154 3 155 6 156 8 157 3 158 10 159 4 160 10 161 6 162 8 163 4 164 7 165 1 166 11 167 2 168 5 169 6 170 2 171 2 172 8 173 4 174 8 175 0 176 11 177 3 178 4 179 2 180 7 181 5 182 2 183 1 184 5 185 2 186 8 187 1 188 4 189 0 190 2 191 1 192 4 193 1 194 2 195 0 196 2 197 1 198 0 199 1 200 1

53: Average symbolic conclusion length is 10408106/188634 ≈ 55.18. (Median: 51)
    Minimum and maximum symbolic conclusion lengths are 8 (×1) and 324 (×1), respectively.
    There are 97474 minimal D-proofs with conclusions of even symbolic length, and there are 91160 minimal D-proofs with conclusions of odd symbolic length. [97474/188634 ≈ 51.67% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 2 10 3 11 3 12 11 13 14 14 17 15 20 16 35 17 48 18 77 19 101 20 125 21 156 22 186 23 293 24 296 25 413 26 537 27 651 28 730 29 1041 30 1273 31 1488 32 1700 33 2197 34 2313 35 2527 36 3162 37 3570 38 3567 39 4093 40 4628 41 4612 42 4866 43 5559 44 5505 45 5044 46 5852 47 5649 48 5381 49 5333 50 6205 51 5054 52 4957 53 5321 54 4924 55 4084 56 4948 57 4695 58 3749 59 3598 60 4151 61 3397 62 2771 63 3261 64 3246 65 2362 66 2264 67 2434 68 2126 69 1622 70 1906 71 1705 72 1603 73 1176 74 1372 75 1076 76 1183 77 893 78 960 79 715 80 1012 81 711 82 808 83 635 84 805 85 542 86 732 87 534 88 688 89 486 90 578 91 384 92 603 93 392 94 571 95 350 96 490 97 332 98 422 99 305 100 420 101 286 102 393 103 225 104 324 105 164 106 369 107 209 108 267 109 161 110 237 111 141 112 228 113 109 114 217 115 112 116 197 117 104 118 154 119 76 120 132 121 65 122 116 123 70 124 107 125 46 126 96 127 44 128 72 129 32 130 73 131 41 132 65 133 37 134 43 135 23 136 54 137 36 138 27 139 25 140 38 141 26 142 44 143 19 144 37 145 12 146 33 147 13 148 30 149 22 150 16 151 10 152 24 153 16 154 16 155 9 156 27 157 13 158 21 159 13 160 17 161 7 162 16 163 12 164 22 165 11 166 13 167 4 168 19 169 9 170 14 171 4 172 15 173 10 174 15 175 8 176 13 177 7 178 12 179 4 180 5 181 2 182 9 183 5 184 14 185 1 186 6 187 3 188 4 189 3 190 4 191 2 192 8 193 5 194 4 195 1 196 5 197 3 198 3 199 2 200 4

55: Average symbolic conclusion length is 17603457/308241 ≈ 57.11. (Median: 53)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 319 (×1), respectively.
    There are 159828 minimal D-proofs with conclusions of even symbolic length, and there are 148413 minimal D-proofs with conclusions of odd symbolic length. [159828/308241 ≈ 51.85% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 4 11 8 12 4 13 12 14 19 15 27 16 46 17 62 18 72 19 101 20 147 21 205 22 227 23 343 24 395 25 470 26 615 27 859 28 874 29 1243 30 1570 31 1872 32 2060 33 2691 34 3283 35 3398 36 4170 37 4915 38 5050 39 5603 40 6787 41 6963 42 7059 43 7923 44 8642 45 7814 46 8665 47 9101 48 8888 49 8472 50 9829 51 9055 52 8189 53 8367 54 8744 55 7371 56 7795 57 8179 58 7168 59 5839 60 6915 61 6652 62 5225 63 5173 64 6023 65 4575 66 4061 67 4483 68 4486 69 2982 70 3200 71 3190 72 2986 73 2126 74 2527 75 2038 76 2147 77 1726 78 1870 79 1450 80 1740 81 1307 82 1550 83 1075 84 1419 85 1024 86 1274 87 918 88 1228 89 826 90 992 91 757 92 1069 93 786 94 1008 95 654 96 909 97 597 98 825 99 499 100 787 101 523 102 725 103 505 104 600 105 363 106 608 107 392 108 547 109 332 110 477 111 294 112 436 113 229 114 427 115 238 116 378 117 204 118 274 119 173 120 279 121 137 122 262 123 136 124 237 125 127 126 162 127 87 128 179 129 92 130 149 131 85 132 117 133 75 134 124 135 44 136 122 137 56 138 76 139 42 140 77 141 52 142 84 143 44 144 65 145 34 146 62 147 33 148 68 149 37 150 46 151 25 152 48 153 33 154 49 155 23 156 48 157 25 158 54 159 11 160 36 161 20 162 27 163 19 164 38 165 13 166 27 167 7 168 33 169 14 170 26 171 15 172 23 173 12 174 22 175 15 176 27 177 5 178 21 179 14 180 19 181 6 182 23 183 8 184 24 185 7 186 10 187 7 188 12 189 6 190 13 191 1 192 12 193 6 194 10 195 3 196 9 197 4 198 9 199 1 200 8

57: Average symbolic conclusion length is 29854500/504870 ≈ 59.13. (Median: 55)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 363 (×1), respectively.
    There are 261490 minimal D-proofs with conclusions of even symbolic length, and there are 243380 minimal D-proofs with conclusions of odd symbolic length. [261490/504870 ≈ 51.79% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 2 11 5 12 12 13 13 14 24 15 32 16 48 17 72 18 85 19 131 20 183 21 237 22 251 23 350 24 497 25 626 26 700 27 1102 28 1174 29 1370 30 1843 31 2391 32 2654 33 3291 34 4218 35 4626 36 5098 37 6468 38 7561 39 7588 40 9219 41 10027 42 10359 43 11161 44 13152 45 12724 46 12727 47 14074 48 14681 49 13431 50 14548 51 15050 52 13591 53 13256 54 15049 55 13778 56 12368 57 13272 58 12784 59 10653 60 11503 61 12066 62 10282 63 8468 64 9889 65 9079 66 7463 67 7247 68 8205 69 5936 70 5793 71 5739 72 5874 73 3988 74 4583 75 4099 76 4102 77 3093 78 3564 79 2776 80 3020 81 2552 82 2912 83 2057 84 2522 85 1984 86 2202 87 1703 88 2160 89 1565 90 1922 91 1431 92 1911 93 1356 94 1767 95 1174 96 1632 97 1133 98 1473 99 1014 100 1424 101 960 102 1386 103 890 104 1223 105 737 106 1144 107 724 108 1072 109 624 110 891 111 604 112 837 113 497 114 743 115 459 116 752 117 377 118 565 119 346 120 540 121 295 122 487 123 266 124 478 125 234 126 347 127 199 128 365 129 192 130 311 131 172 132 284 133 152 134 240 135 111 136 243 137 124 138 198 139 102 140 183 141 119 142 166 143 87 144 155 145 64 146 132 147 61 148 120 149 56 150 95 151 59 152 100 153 66 154 101 155 45 156 98 157 46 158 88 159 37 160 67 161 34 162 70 163 35 164 58 165 27 166 77 167 32 168 71 169 27 170 53 171 28 172 56 173 19 174 50 175 21 176 43 177 20 178 38 179 21 180 33 181 18 182 39 183 11 184 47 185 16 186 38 187 14 188 24 189 12 190 28 191 16 192 22 193 9 194 31 195 10 196 31 197 11 198 19 199 5 200 26

59: Average symbolic conclusion length is 50611160/827701 ≈ 61.15. (Median: 57)
    Minimum and maximum symbolic conclusion lengths are 5 (×1) and 449 (×1), respectively.
    There are 427179 minimal D-proofs with conclusions of even symbolic length, and there are 400522 minimal D-proofs with conclusions of odd symbolic length. [427179/827701 ≈ 51.61% even]
1 0 2 0 3 0 4 0 5 1 6 1 7 0 8 0 9 0 10 5 11 6 12 4 13 21 14 22 15 29 16 44 17 77 18 93 19 162 20 188 21 255 22 315 23 434 24 559 25 785 26 883 27 1179 28 1548 29 1736 30 2231 31 3073 32 3396 33 3952 34 5236 35 6233 36 7053 37 8362 38 10332 39 10560 40 11843 41 14161 42 15432 43 15694 44 18338 45 19436 46 19425 47 20904 48 23263 49 21985 50 21728 51 23805 52 23188 53 22057 54 23363 55 24262 56 20982 57 20681 58 22163 59 20015 60 18406 61 20277 62 19145 63 15287 64 16230 65 16648 66 14261 67 11995 68 14272 69 12133 70 10591 71 9746 72 10882 73 7888 74 8109 75 7767 76 8009 77 5868 78 6392 79 5474 80 5628 81 4566 82 5196 83 3847 84 4247 85 3727 86 4148 87 3010 88 3781 89 2996 90 3673 91 2696 92 3440 93 2428 94 3097 95 2153 96 2884 97 2206 98 2754 99 1940 100 2464 101 1793 102 2523 103 1610 104 2385 105 1538 106 2075 107 1385 108 1788 109 1147 110 1721 111 1169 112 1632 113 921 114 1364 115 859 116 1435 117 781 118 1088 119 725 120 1083 121 624 122 997 123 515 124 965 125 497 126 758 127 455 128 719 129 355 130 626 131 337 132 568 133 315 134 442 135 253 136 485 137 232 138 393 139 210 140 352 141 191 142 352 143 136 144 285 145 162 146 270 147 142 148 234 149 133 150 221 151 114 152 227 153 96 154 209 155 83 156 194 157 104 158 144 159 64 160 143 161 64 162 127 163 67 164 143 165 56 166 137 167 70 168 130 169 66 170 113 171 46 172 114 173 52 174 118 175 59 176 93 177 40 178 101 179 40 180 73 181 39 182 84 183 42 184 96 185 37 186 62 187 28 188 66 189 37 190 66 191 18 192 63 193 24 194 63 195 15 196 49 197 22 198 33 199 16 200 40

61: Average symbolic conclusion length is 85737193/1357539 ≈ 63.16. (Median: 58)
    Minimum and maximum symbolic conclusion lengths are 8 (×2) and 478 (×1), respectively.
    There are 697798 minimal D-proofs with conclusions of even symbolic length, and there are 659741 minimal D-proofs with conclusions of odd symbolic length. [697798/1357539 ≈ 51.40% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 2 9 2 10 2 11 7 12 4 13 15 14 23 15 42 16 45 17 95 18 112 19 155 20 192 21 298 22 388 23 535 24 641 25 917 26 1042 27 1357 28 1853 29 2278 30 2670 31 3578 32 4489 33 4909 34 6581 35 8109 36 9298 37 10418 38 13358 39 15025 40 16125 41 19439 42 22296 43 22302 44 25416 45 28828 46 29573 47 30231 48 34260 49 35272 50 33251 51 36671 52 38377 53 36466 54 36179 55 39891 56 36389 57 34151 58 36239 59 36133 60 31233 61 32398 62 33346 63 28613 64 26521 65 28789 66 27214 67 21447 68 23205 69 23331 70 19773 71 16885 72 19714 73 16587 74 14481 75 13377 76 14759 77 11343 78 11222 79 10349 80 10580 81 8418 82 9224 83 7526 84 7952 85 6692 86 7521 87 5718 88 6543 89 5386 90 6583 91 4790 92 5950 93 4410 94 5489 95 3921 96 5184 97 3929 98 5039 99 3415 100 4381 101 3338 102 4404 103 3061 104 4114 105 2820 106 3796 107 2522 108 3442 109 2230 110 3307 111 2166 112 3106 113 1902 114 2499 115 1671 116 2516 117 1554 118 2285 119 1458 120 2032 121 1257 122 1804 123 1049 124 1893 125 1029 126 1534 127 915 128 1335 129 757 130 1302 131 640 132 1207 133 676 134 1014 135 539 136 871 137 429 138 815 139 459 140 743 141 429 142 633 143 315 144 597 145 277 146 534 147 259 148 472 149 264 150 448 151 270 152 429 153 226 154 383 155 172 156 363 157 196 158 312 159 169 160 315 161 162 162 282 163 144 164 308 165 124 166 275 167 123 168 237 169 131 170 186 171 108 172 209 173 109 174 191 175 108 176 208 177 83 178 191 179 85 180 164 181 95 182 146 183 75 184 166 185 76 186 143 187 62 188 146 189 61 190 121 191 56 192 133 193 46 194 128 195 53 196 88 197 41 198 79 199 41 200 87

63: Average symbolic conclusion length is 145183281/2227822 ≈ 65.17. (Median: 60)
    Minimum and maximum symbolic conclusion lengths are 6 (×1) and 521 (×1), respectively.
    There are 1142327 minimal D-proofs with conclusions of even symbolic length, and there are 1085495 minimal D-proofs with conclusions of odd symbolic length. [1142327/2227822 ≈ 51.28% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 1 8 1 9 2 10 1 11 5 12 12 13 29 14 14 15 45 16 47 17 86 18 118 19 186 20 211 21 340 22 461 23 593 24 757 25 1080 26 1361 27 1550 28 2091 29 2870 30 3400 31 4142 32 5850 33 6479 34 7761 35 10083 36 12158 37 13481 38 16893 39 20166 40 22281 41 25014 42 30479 43 33207 44 34945 45 40956 46 43946 47 44562 48 49270 49 54646 50 53456 51 54927 52 60050 53 60227 54 56437 55 61548 56 61222 57 57123 58 57425 59 62690 60 55926 61 52144 62 55570 63 52025 64 45376 65 48737 66 49417 67 40839 68 38004 69 40607 70 37841 71 30596 72 33137 73 32227 74 26798 75 23822 76 26639 77 22492 78 19760 79 18751 80 19828 81 15675 82 15883 83 14004 84 14831 85 11927 86 13804 87 10900 88 11877 89 9820 90 11493 91 8574 92 10376 93 7983 94 9732 95 7249 96 8859 97 6967 98 8784 99 6263 100 8097 101 5999 102 7826 103 5515 104 7278 105 5108 106 6852 107 4639 108 6015 109 4369 110 5986 111 4020 112 5716 113 3616 114 4939 115 3205 116 4755 117 2918 118 4398 119 2679 120 3913 121 2548 122 3399 123 2035 124 3414 125 2013 126 3032 127 1721 128 2603 129 1562 130 2423 131 1343 132 2271 133 1313 134 2067 135 1087 136 1717 137 957 138 1585 139 920 140 1505 141 852 142 1344 143 726 144 1098 145 687 146 1095 147 551 148 994 149 568 150 850 151 540 152 816 153 420 154 760 155 384 156 667 157 367 158 649 159 334 160 655 161 355 162 532 163 336 164 564 165 269 166 492 167 259 168 443 169 264 170 391 171 225 172 428 173 240 174 373 175 228 176 429 177 201 178 361 179 188 180 315 181 172 182 295 183 136 184 311 185 141 186 252 187 147 188 268 189 136 190 224 191 138 192 255 193 87 194 217 195 92 196 215 197 92 198 158 199 96 200 197

65: Average symbolic conclusion length is 246013046/3660735 ≈ 67.20. (Median: 62)
    Minimum and maximum symbolic conclusion lengths are 8 (×1) and 556 (×1), respectively.
    There are 1876763 minimal D-proofs with conclusions of even symbolic length, and there are 1783972 minimal D-proofs with conclusions of odd symbolic length. [1876763/3660735 ≈ 51.27% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 3 10 1 11 11 12 6 13 25 14 13 15 44 16 51 17 97 18 129 19 188 20 265 21 389 22 519 23 681 24 896 25 1159 26 1622 27 1962 28 2575 29 3456 30 4293 31 4921 32 6840 33 8442 34 9811 35 12230 36 16143 37 17549 38 20892 39 26327 40 30490 41 33574 42 40370 43 46932 44 48651 45 55298 46 63745 47 67077 48 70179 49 80137 50 82586 51 83365 52 90225 53 96891 54 91032 55 94105 56 99598 57 96227 58 93196 59 99597 60 96911 61 87650 62 89006 63 92326 64 82920 65 79123 66 84634 67 76457 68 66200 69 69469 70 70000 71 57600 72 54831 73 57846 74 51725 75 43200 76 45851 77 43157 78 36523 79 33829 80 36388 81 30587 82 28391 83 26197 84 27006 85 22063 86 23932 87 20080 88 21088 89 16996 90 20214 91 16028 92 18127 93 14292 94 17185 95 13422 96 15807 97 12490 98 15319 99 11239 100 14640 101 10846 102 13860 103 9978 104 12763 105 9095 106 12178 107 8747 108 11104 109 8190 110 10733 111 7404 112 10483 113 6702 114 9377 115 6175 116 8483 117 5653 118 7745 119 4889 120 7554 121 4878 122 6590 123 3909 124 6247 125 3855 126 5814 127 3480 128 4933 129 3191 130 4683 131 2686 132 4326 133 2570 134 4036 135 2199 136 3375 137 2045 138 3141 139 1757 140 2936 141 1610 142 2705 143 1511 144 2219 145 1377 146 2261 147 1182 148 1890 149 1105 150 1665 151 1006 152 1677 153 858 154 1530 155 842 156 1298 157 782 158 1168 159 684 160 1239 161 674 162 1081 163 633 164 1069 165 522 166 946 167 518 168 823 169 526 170 785 171 424 172 820 173 440 174 748 175 453 176 792 177 409 178 615 179 394 180 639 181 344 182 590 183 319 184 606 185 299 186 494 187 307 188 543 189 283 190 469 191 243 192 466 193 258 194 444 195 220 196 371 197 203 198 369 199 195 200 357

67: Average symbolic conclusion length is 417042043/6021110 ≈ 69.26. (Median: 64)
    Minimum and maximum symbolic conclusion lengths are 9 (×5) and 729 (×1), respectively.
    There are 3091299 minimal D-proofs with conclusions of even symbolic length, and there are 2929811 minimal D-proofs with conclusions of odd symbolic length. [3091299/6021110 ≈ 51.34% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 5 10 1 11 9 12 5 13 23 14 30 15 63 16 60 17 109 18 123 19 257 20 299 21 377 22 605 23 792 24 1063 25 1338 26 1899 27 2348 28 3060 29 3987 30 5296 31 6149 32 8075 33 10401 34 12663 35 14812 36 19708 37 23320 38 26553 39 33643 40 40954 41 45228 42 51977 43 63428 44 69625 45 75796 46 89307 47 99275 48 100417 49 113747 50 124758 51 126933 52 131804 53 146923 54 147088 55 143991 56 156514 57 160851 58 151258 59 155020 60 163110 61 150161 62 146113 63 154624 64 148749 65 132517 66 137933 67 136084 68 120259 69 115860 70 122702 71 109695 72 95107 73 98550 74 97595 75 80646 76 77732 77 80482 78 70567 79 61093 80 63176 81 58447 82 51595 83 47337 84 49928 85 42037 86 41989 87 37102 88 38817 89 31242 90 35327 91 29222 92 31328 93 25315 94 30568 95 24312 96 28009 97 22214 98 26669 99 20475 100 25877 101 19338 102 23838 103 18042 104 22078 105 16256 106 22048 107 16004 108 20560 109 14642 110 19034 111 13631 112 18408 113 12657 114 16931 115 11810 116 15586 117 10459 118 14284 119 9352 120 13934 121 9155 122 12615 123 7857 124 11408 125 7306 126 10392 127 6545 128 9813 129 6266 130 8922 131 5400 132 8098 133 4970 134 7905 135 4419 136 6635 137 4109 138 6107 139 3560 140 5806 141 3111 142 5387 143 2996 144 4497 145 2756 146 4232 147 2165 148 3865 149 2192 150 3422 151 2085 152 3102 153 1721 154 3008 155 1625 156 2610 157 1539 158 2365 159 1328 160 2326 161 1336 162 2074 163 1185 164 1990 165 1088 166 1862 167 1054 168 1673 169 1070 170 1591 171 898 172 1634 173 860 174 1484 175 832 176 1465 177 747 178 1208 179 735 180 1168 181 704 182 1094 183 613 184 1164 185 609 186 1053 187 566 188 1005 189 529 190 914 191 529 192 924 193 505 194 806 195 411 196 820 197 407 198 714 199 422 200 727

69: Average symbolic conclusion length is 706620328/9907537 ≈ 71.32. (Median: 65)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 656 (×1), respectively.
    There are 5095227 minimal D-proofs with conclusions of even symbolic length, and there are 4812310 minimal D-proofs with conclusions of odd symbolic length. [5095227/9907537 ≈ 51.43% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 1 9 2 10 3 11 6 12 5 13 35 14 31 15 56 16 60 17 151 18 171 19 227 20 332 21 440 22 678 23 887 24 1267 25 1488 26 2210 27 2895 28 3731 29 4584 30 6497 31 7700 32 9450 33 12524 34 16057 35 18522 36 23805 37 30470 38 34816 39 41708 40 52578 41 60560 42 68019 43 83637 44 96220 45 105462 46 119771 47 140305 48 148258 49 159837 50 181800 51 192349 52 195195 53 216888 54 230579 55 227124 56 237439 57 254900 58 249655 59 242435 60 260368 61 254731 62 242551 63 247455 64 258885 65 231150 66 224122 67 233115 68 218102 69 195170 70 208410 71 200371 72 172531 73 166242 74 173639 75 153591 76 135535 77 139970 78 135203 79 111786 80 109949 81 109334 82 98471 83 84242 84 88467 85 79762 86 74721 87 65920 88 69864 89 58771 90 61547 91 54028 92 56933 93 45919 94 54205 95 43926 96 48608 97 39375 98 46425 99 36855 100 44152 101 34289 102 41502 103 32150 104 39340 105 29867 106 37601 107 28894 108 36405 109 26312 110 34056 111 24709 112 32039 113 22659 114 30405 115 21706 116 28410 117 19442 118 25631 119 18026 120 25032 121 17101 122 23323 123 14959 124 21075 125 13784 126 19622 127 12511 128 18731 129 11795 130 16933 131 10532 132 14708 133 9384 134 14554 135 8693 136 13188 137 7968 138 11621 139 7218 140 10776 141 6183 142 10327 143 5874 144 8993 145 5331 146 7994 147 4525 148 7660 149 4244 150 6973 151 4194 152 6164 153 3496 154 5727 155 3224 156 5258 157 3070 158 4754 159 2708 160 4529 161 2568 162 3981 163 2350 164 3736 165 2130 166 3465 167 2008 168 3366 169 2022 170 3184 171 1755 172 2986 173 1726 174 2780 175 1614 176 2716 177 1498 178 2466 179 1427 180 2355 181 1439 182 2201 183 1211 184 2324 185 1210 186 2026 187 1119 188 1850 189 1036 190 1764 191 995 192 1772 193 974 194 1587 195 830 196 1624 197 854 198 1363 199 772 200 1392