1: Average symbolic conclusion length is 16/2 ≈ 8.00. (Median: 8.00)
   Minimum and maximum symbolic conclusion lengths are 3 (×1) and 13 (×1), respectively.
   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 1 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 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 23/1 ≈ 23.00. (Median: 23)
   Minimum and maximum symbolic conclusion lengths are 23 (×1) and 23 (×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 0 22 0 23 1

7: Average symbolic conclusion length is 45/3 ≈ 15.00. (Median: 11)
   Minimum and maximum symbolic conclusion lengths are 11 (×2) and 23 (×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 0 6 0 7 0 8 0 9 0 10 0 11 2 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 0 22 0 23 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

45: Average symbolic conclusion length is 352494/6426 ≈ 54.85. (Median: 49)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 209 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 6426 minimal D-proofs with conclusions of odd symbolic length. [0/6426 ≈ 0.00% 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 6 14 0 15 12 16 0 17 29 18 0 19 54 20 0 21 66 22 0 23 93 24 0 25 129 26 0 27 161 28 0 29 194 30 0 31 211 32 0 33 235 34 0 35 273 36 0 37 248 38 0 39 264 40 0 41 295 42 0 43 277 44 0 45 249 46 0 47 232 48 0 49 237 50 0 51 196 52 0 53 222 54 0 55 191 56 0 57 210 58 0 59 180 60 0 61 159 62 0 63 181 64 0 65 161 66 0 67 125 68 0 69 137 70 0 71 82 72 0 73 117 74 0 75 88 76 0 77 104 78 0 79 70 80 0 81 100 82 0 83 58 84 0 85 80 86 0 87 48 88 0 89 71 90 0 91 54 92 0 93 59 94 0 95 40 96 0 97 65 98 0 99 23 100 0 101 44 102 0 103 22 104 0 105 30 106 0 107 17 108 0 109 30 110 0 111 11 112 0 113 23 114 0 115 6 116 0 117 14 118 0 119 9 120 0 121 9 122 0 123 6 124 0 125 12 126 0 127 4 128 0 129 12 130 0 131 4 132 0 133 4 134 0 135 2 136 0 137 10 138 0 139 2 140 0 141 7 142 0 143 4 144 0 145 6 146 0 147 3 148 0 149 8 150 0 151 2 152 0 153 5 154 0 155 3 156 0 157 4 158 0 159 2 160 0 161 6 162 0 163 1 164 0 165 3 166 0 167 2 168 0 169 2 170 0 171 0 172 0 173 3 174 0 175 0 176 0 177 2 178 0 179 0 180 0 181 1 182 0 183 0 184 0 185 2 186 0 187 0 188 0 189 0 190 0 191 0 192 0 193 1 194 0 195 0 196 0 197 0 198 0 199 0 200 0 201 0 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 1

47: Average symbolic conclusion length is 513464/9042 ≈ 56.79. (Median: 51)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 209 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 9042 minimal D-proofs with conclusions of odd symbolic length. [0/9042 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 3 12 0 13 6 14 0 15 15 16 0 17 25 18 0 19 54 20 0 21 94 22 0 23 131 24 0 25 162 26 0 27 218 28 0 29 210 30 0 31 263 32 0 33 326 34 0 35 348 36 0 37 370 38 0 39 366 40 0 41 372 42 0 43 398 44 0 45 369 46 0 47 338 48 0 49 378 50 0 51 314 52 0 53 290 54 0 55 269 56 0 57 300 58 0 59 255 60 0 61 201 62 0 63 179 64 0 65 206 66 0 67 169 68 0 69 174 70 0 71 147 72 0 73 155 74 0 75 104 76 0 77 175 78 0 79 130 80 0 81 134 82 0 83 105 84 0 85 106 86 0 87 79 88 0 89 115 90 0 91 62 92 0 93 82 94 0 95 60 96 0 97 70 98 0 99 45 100 0 101 75 102 0 103 42 104 0 105 59 106 0 107 32 108 0 109 56 110 0 111 22 112 0 113 40 114 0 115 27 116 0 117 34 118 0 119 21 120 0 121 45 122 0 123 13 124 0 125 25 126 0 127 8 128 0 129 23 130 0 131 6 132 0 133 13 134 0 135 7 136 0 137 11 138 0 139 5 140 0 141 16 142 0 143 5 144 0 145 15 146 0 147 3 148 0 149 9 150 0 151 2 152 0 153 7 154 0 155 4 156 0 157 4 158 0 159 3 160 0 161 7 162 0 163 1 164 0 165 5 166 0 167 3 168 0 169 2 170 0 171 1 172 0 173 4 174 0 175 0 176 0 177 3 178 0 179 1 180 0 181 1 182 0 183 1 184 0 185 3 186 0 187 0 188 0 189 1 190 0 191 0 192 0 193 1 194 0 195 0 196 0 197 1 198 0 199 0 200 0 201 1 202 0 203 0 204 0 205 0 206 0 207 0 208 0 209 1

49: Average symbolic conclusion length is 758955/12829 ≈ 59.16. (Median: 53)
    Minimum and maximum symbolic conclusion lengths are 9 (×2) and 257 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 12829 minimal D-proofs with conclusions of odd symbolic length. [0/12829 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 0 11 5 12 0 13 6 14 0 15 22 16 0 17 44 18 0 19 65 20 0 21 92 22 0 23 125 24 0 25 207 26 0 27 220 28 0 29 289 30 0 31 376 32 0 33 406 34 0 35 442 36 0 37 458 38 0 39 485 40 0 41 525 42 0 43 485 44 0 45 510 46 0 47 531 48 0 49 509 50 0 51 427 52 0 53 408 54 0 55 390 56 0 57 350 58 0 59 358 60 0 61 338 62 0 63 327 64 0 65 326 66 0 67 240 68 0 69 340 70 0 71 235 72 0 73 274 74 0 75 198 76 0 77 211 78 0 79 169 80 0 81 216 82 0 83 134 84 0 85 174 86 0 87 138 88 0 89 160 90 0 91 114 92 0 93 144 94 0 95 91 96 0 97 130 98 0 99 75 100 0 101 124 102 0 103 78 104 0 105 89 106 0 107 52 108 0 109 89 110 0 111 34 112 0 113 70 114 0 115 35 116 0 117 46 118 0 119 26 120 0 121 45 122 0 123 16 124 0 125 35 126 0 127 10 128 0 129 28 130 0 131 12 132 0 133 23 134 0 135 11 136 0 137 27 138 0 139 4 140 0 141 19 142 0 143 10 144 0 145 10 146 0 147 7 148 0 149 13 150 0 151 5 152 0 153 15 154 0 155 8 156 0 157 12 158 0 159 5 160 0 161 18 162 0 163 4 164 0 165 11 166 0 167 5 168 0 169 11 170 0 171 3 172 0 173 9 174 0 175 2 176 0 177 5 178 0 179 3 180 0 181 3 182 0 183 2 184 0 185 5 186 0 187 1 188 0 189 3 190 0 191 2 192 0 193 2 194 0 195 0 196 0 197 3 198 0 199 0 200 0 201 2 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 1 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 1 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 1

51: Average symbolic conclusion length is 1103704/18076 ≈ 61.06. (Median: 55)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 233 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 18076 minimal D-proofs with conclusions of odd symbolic length. [0/18076 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 1 12 0 13 15 14 0 15 16 16 0 17 44 18 0 19 70 20 0 21 102 22 0 23 183 24 0 25 230 26 0 27 319 28 0 29 430 30 0 31 398 32 0 33 529 34 0 35 531 36 0 37 656 38 0 39 682 40 0 41 664 42 0 43 734 44 0 45 720 46 0 47 671 48 0 49 723 50 0 51 618 52 0 53 633 54 0 55 624 56 0 57 562 58 0 59 495 60 0 61 490 62 0 63 477 64 0 65 445 66 0 67 318 68 0 69 366 70 0 71 323 72 0 73 357 74 0 75 259 76 0 77 307 78 0 79 230 80 0 81 271 82 0 83 250 84 0 85 279 86 0 87 178 88 0 89 274 90 0 91 155 92 0 93 232 94 0 95 164 96 0 97 165 98 0 99 110 100 0 101 160 102 0 103 95 104 0 105 137 106 0 107 86 108 0 109 104 110 0 111 68 112 0 113 116 114 0 115 63 116 0 117 82 118 0 119 45 120 0 121 88 122 0 123 38 124 0 125 65 126 0 127 45 128 0 129 56 130 0 131 28 132 0 133 70 134 0 135 23 136 0 137 51 138 0 139 14 140 0 141 40 142 0 143 10 144 0 145 31 146 0 147 16 148 0 149 20 150 0 151 14 152 0 153 32 154 0 155 9 156 0 157 21 158 0 159 7 160 0 161 17 162 0 163 4 164 0 165 17 166 0 167 7 168 0 169 14 170 0 171 5 172 0 173 13 174 0 175 2 176 0 177 11 178 0 179 4 180 0 181 5 182 0 183 3 184 0 185 8 186 0 187 1 188 0 189 5 190 0 191 3 192 0 193 2 194 0 195 1 196 0 197 4 198 0 199 0 200 0 201 3 202 0 203 1 204 0 205 1 206 0 207 1 208 0 209 3 210 0 211 0 212 0 213 1 214 0 215 0 216 0 217 1 218 0 219 0 220 0 221 1 222 0 223 0 224 0 225 2 226 0 227 0 228 0 229 0 230 0 231 0 232 0 233 1

53: Average symbolic conclusion length is 1628797/25667 ≈ 63.46. (Median: 57)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 263 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 25667 minimal D-proofs with conclusions of odd symbolic length. [0/25667 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 7 12 0 13 11 14 0 15 22 16 0 17 52 18 0 19 70 20 0 21 135 22 0 23 227 24 0 25 263 26 0 27 367 28 0 29 435 30 0 31 580 32 0 33 690 34 0 35 735 36 0 37 849 38 0 39 852 40 0 41 963 42 0 43 884 44 0 45 988 46 0 47 1009 48 0 49 924 50 0 51 882 52 0 53 955 54 0 55 866 56 0 57 742 58 0 59 684 60 0 61 704 62 0 63 573 64 0 65 639 66 0 67 535 68 0 69 607 70 0 71 476 72 0 73 500 74 0 75 509 76 0 77 501 78 0 79 405 80 0 81 439 82 0 83 290 84 0 85 412 86 0 87 307 88 0 89 362 90 0 91 251 92 0 93 350 94 0 95 207 96 0 97 295 98 0 99 195 100 0 101 265 102 0 103 166 104 0 105 245 106 0 107 154 108 0 109 203 110 0 111 112 112 0 113 193 114 0 115 103 116 0 117 140 118 0 119 80 120 0 121 141 122 0 123 52 124 0 125 94 126 0 127 49 128 0 129 83 130 0 131 42 132 0 133 77 134 0 135 30 136 0 137 62 138 0 139 27 140 0 141 47 142 0 143 27 144 0 145 37 146 0 147 19 148 0 149 42 150 0 151 10 152 0 153 43 154 0 155 13 156 0 157 27 158 0 159 14 160 0 161 34 162 0 163 12 164 0 165 25 166 0 167 18 168 0 169 25 170 0 171 11 172 0 173 25 174 0 175 10 176 0 177 22 178 0 179 9 180 0 181 20 182 0 183 5 184 0 185 22 186 0 187 3 188 0 189 13 190 0 191 4 192 0 193 10 194 0 195 3 196 0 197 9 198 0 199 2 200 0 201 6 202 0 203 3 204 0 205 3 206 0 207 2 208 0 209 5 210 0 211 1 212 0 213 3 214 0 215 2 216 0 217 2 218 0 219 0 220 0 221 3 222 0 223 0 224 0 225 2 226 0 227 0 228 0 229 1 230 0 231 0 232 0 233 2 234 0 235 0 236 0 237 0 238 0 239 0 240 0 241 1 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 1 258 0 259 0 260 0 261 0 262 0 263 1

55: Average symbolic conclusion length is 2367312/36224 ≈ 65.35. (Median: 57)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 273 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 36224 minimal D-proofs with conclusions of odd symbolic length. [0/36224 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 1 10 0 11 5 12 0 13 11 14 0 15 29 16 0 17 54 18 0 19 96 20 0 21 148 22 0 23 185 24 0 25 348 26 0 27 496 28 0 29 602 30 0 31 783 32 0 33 831 34 0 35 967 36 0 37 1034 38 0 39 1215 40 0 41 1239 42 0 43 1265 44 0 45 1401 46 0 47 1276 48 0 49 1389 50 0 51 1284 52 0 53 1246 54 0 55 1202 56 0 57 1155 58 0 59 1052 60 0 61 1144 62 0 63 873 64 0 65 908 66 0 67 815 68 0 69 873 70 0 71 691 72 0 73 647 74 0 75 585 76 0 77 667 78 0 79 533 80 0 81 590 82 0 83 468 84 0 85 548 86 0 87 383 88 0 89 566 90 0 91 380 92 0 93 460 94 0 95 384 96 0 97 406 98 0 99 311 100 0 101 426 102 0 103 235 104 0 105 357 106 0 107 219 108 0 109 268 110 0 111 173 112 0 113 258 114 0 115 137 116 0 117 211 118 0 119 131 120 0 121 186 122 0 123 100 124 0 125 172 126 0 127 95 128 0 129 153 130 0 131 72 132 0 133 141 134 0 135 63 136 0 137 104 138 0 139 73 140 0 141 91 142 0 143 56 144 0 145 114 146 0 147 41 148 0 149 83 150 0 151 30 152 0 153 79 154 0 155 21 156 0 157 54 158 0 159 31 160 0 161 42 162 0 163 21 164 0 165 58 166 0 167 16 168 0 169 49 170 0 171 17 172 0 173 31 174 0 175 13 176 0 177 38 178 0 179 13 180 0 181 23 182 0 183 11 184 0 185 25 186 0 187 5 188 0 189 24 190 0 191 8 192 0 193 19 194 0 195 5 196 0 197 14 198 0 199 2 200 0 201 10 202 0 203 4 204 0 205 7 206 0 207 3 208 0 209 10 210 0 211 1 212 0 213 6 214 0 215 3 216 0 217 2 218 0 219 1 220 0 221 4 222 0 223 0 224 0 225 3 226 0 227 1 228 0 229 1 230 0 231 2 232 0 233 4 234 0 235 0 236 0 237 1 238 0 239 0 240 0 241 1 242 0 243 0 244 0 245 1 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 1 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 1

57: Average symbolic conclusion length is 3492232/51530 ≈ 67.77. (Median: 59)
    Minimum and maximum symbolic conclusion lengths are 9 (×3) and 281 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 51530 minimal D-proofs with conclusions of odd symbolic length. [0/51530 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 3 10 0 11 5 12 0 13 10 14 0 15 40 16 0 17 46 18 0 19 99 20 0 21 173 22 0 23 309 24 0 25 426 26 0 27 537 28 0 29 722 30 0 31 877 32 0 33 1043 34 0 35 1290 36 0 37 1482 38 0 39 1582 40 0 41 1599 42 0 43 1766 44 0 45 1776 46 0 47 1811 48 0 49 1815 50 0 51 1815 52 0 53 1879 54 0 55 1611 56 0 57 1613 58 0 59 1573 60 0 61 1544 62 0 63 1252 64 0 65 1273 66 0 67 1132 68 0 69 1079 70 0 71 1039 72 0 73 1080 74 0 75 948 76 0 77 943 78 0 79 752 80 0 81 1026 82 0 83 761 84 0 85 922 86 0 87 648 88 0 89 713 90 0 91 618 92 0 93 743 94 0 95 485 96 0 97 663 98 0 99 479 100 0 101 574 102 0 103 411 104 0 105 549 106 0 107 329 108 0 109 452 110 0 111 305 112 0 113 461 114 0 115 253 116 0 117 375 118 0 119 232 120 0 121 309 122 0 123 170 124 0 125 306 126 0 127 163 128 0 129 245 130 0 131 111 132 0 133 203 134 0 135 94 136 0 137 164 138 0 139 82 140 0 141 134 142 0 143 73 144 0 145 141 146 0 147 53 148 0 149 103 150 0 151 39 152 0 153 95 154 0 155 46 156 0 157 74 158 0 159 43 160 0 161 77 162 0 163 29 164 0 165 72 166 0 167 33 168 0 169 58 170 0 171 26 172 0 173 58 174 0 175 25 176 0 177 54 178 0 179 25 180 0 181 52 182 0 183 21 184 0 185 54 186 0 187 20 188 0 189 39 190 0 191 21 192 0 193 37 194 0 195 13 196 0 197 29 198 0 199 9 200 0 201 27 202 0 203 9 204 0 205 22 206 0 207 5 208 0 209 24 210 0 211 3 212 0 213 15 214 0 215 4 216 0 217 13 218 0 219 3 220 0 221 10 222 0 223 2 224 0 225 9 226 0 227 3 228 0 229 3 230 0 231 2 232 0 233 6 234 0 235 1 236 0 237 4 238 0 239 2 240 0 241 3 242 0 243 0 244 0 245 3 246 0 247 0 248 0 249 2 250 0 251 0 252 0 253 2 254 0 255 1 256 0 257 3 258 0 259 1 260 0 261 0 262 0 263 0 264 0 265 2 266 0 267 0 268 0 269 2 270 0 271 0 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 1

59: Average symbolic conclusion length is 5078221/72889 ≈ 69.67. (Median: 61)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 289 (×2), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 72889 minimal D-proofs with conclusions of odd symbolic length. [0/72889 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 6 12 0 13 19 14 0 15 24 16 0 17 53 18 0 19 127 20 0 21 220 22 0 23 309 24 0 25 480 26 0 27 667 28 0 29 926 30 0 31 1162 32 0 33 1452 34 0 35 1708 36 0 37 1749 38 0 39 1996 40 0 41 2217 42 0 43 2380 44 0 45 2537 46 0 47 2485 48 0 49 2539 50 0 51 2625 52 0 53 2421 54 0 55 2393 56 0 57 2410 58 0 59 2128 60 0 61 2202 62 0 63 1868 64 0 65 2034 66 0 67 1798 68 0 69 1657 70 0 71 1522 72 0 73 1591 74 0 75 1353 76 0 77 1338 78 0 79 1025 80 0 81 1284 82 0 83 1042 84 0 85 1185 86 0 87 885 88 0 89 1055 90 0 91 804 92 0 93 1000 94 0 95 806 96 0 97 945 98 0 99 641 100 0 101 906 102 0 103 562 104 0 105 792 106 0 107 594 108 0 109 634 110 0 111 453 112 0 113 634 114 0 115 377 116 0 117 572 118 0 119 331 120 0 121 433 122 0 123 263 124 0 125 418 126 0 127 228 128 0 129 338 130 0 131 199 132 0 133 283 134 0 135 180 136 0 137 304 138 0 139 159 140 0 141 245 142 0 143 114 144 0 145 253 146 0 147 104 148 0 149 179 150 0 151 119 152 0 153 176 154 0 155 91 156 0 157 185 158 0 159 82 160 0 161 150 162 0 163 55 164 0 165 141 166 0 167 44 168 0 169 114 170 0 171 59 172 0 173 83 174 0 175 48 176 0 177 115 178 0 179 33 180 0 181 79 182 0 183 37 184 0 185 63 186 0 187 23 188 0 189 74 190 0 191 24 192 0 193 59 194 0 195 24 196 0 197 48 198 0 199 18 200 0 201 55 202 0 203 14 204 0 205 33 206 0 207 10 208 0 209 31 210 0 211 7 212 0 213 26 214 0 215 10 216 0 217 23 218 0 219 6 220 0 221 17 222 0 223 3 224 0 225 11 226 0 227 4 228 0 229 8 230 0 231 3 232 0 233 12 234 0 235 1 236 0 237 9 238 0 239 4 240 0 241 4 242 0 243 1 244 0 245 5 246 0 247 0 248 0 249 5 250 0 251 1 252 0 253 2 254 0 255 1 256 0 257 4 258 0 259 1 260 0 261 1 262 0 263 0 264 0 265 1 266 0 267 0 268 0 269 1 270 0 271 1 272 0 273 1 274 0 275 0 276 0 277 0 278 0 279 1 280 0 281 1 282 0 283 0 284 0 285 1 286 0 287 0 288 0 289 2

61: Average symbolic conclusion length is 7486711/103901 ≈ 72.06. (Median: 63)
    Minimum and maximum symbolic conclusion lengths are 9 (×2) and 513 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 103901 minimal D-proofs with conclusions of odd symbolic length. [0/103901 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 2 10 0 11 3 12 0 13 19 14 0 15 35 16 0 17 77 18 0 19 159 20 0 21 227 22 0 23 415 24 0 25 646 26 0 27 885 28 0 29 1226 30 0 31 1353 32 0 33 1736 34 0 35 2022 36 0 37 2420 38 0 39 2772 40 0 41 2990 42 0 43 3222 44 0 45 3297 46 0 47 3296 48 0 49 3538 50 0 51 3413 52 0 53 3530 54 0 55 3348 56 0 57 3345 58 0 59 3182 60 0 61 2993 62 0 63 2736 64 0 65 2793 66 0 67 2566 68 0 69 2302 70 0 71 2072 72 0 73 2172 74 0 75 1762 76 0 77 2060 78 0 79 1699 80 0 81 1935 82 0 83 1473 84 0 85 1664 86 0 87 1560 88 0 89 1686 90 0 91 1360 92 0 93 1509 94 0 95 1061 96 0 97 1524 98 0 99 1068 100 0 101 1215 102 0 103 960 104 0 105 1211 106 0 107 789 108 0 109 1098 110 0 111 728 112 0 113 938 114 0 115 612 116 0 117 894 118 0 119 547 120 0 121 750 122 0 123 469 124 0 125 736 126 0 127 369 128 0 129 616 130 0 131 372 132 0 133 496 134 0 135 287 136 0 137 498 138 0 139 237 140 0 141 400 142 0 143 184 144 0 145 358 146 0 147 155 148 0 149 280 150 0 151 155 152 0 153 254 154 0 155 124 156 0 157 227 158 0 159 104 160 0 161 197 162 0 163 84 164 0 165 183 166 0 167 85 168 0 169 167 170 0 171 76 172 0 173 151 174 0 175 60 176 0 177 146 178 0 179 61 180 0 181 118 182 0 183 55 184 0 185 117 186 0 187 53 188 0 189 101 190 0 191 54 192 0 193 102 194 0 195 39 196 0 197 84 198 0 199 37 200 0 201 84 202 0 203 29 204 0 205 71 206 0 207 26 208 0 209 66 210 0 211 22 212 0 213 44 214 0 215 22 216 0 217 44 218 0 219 15 220 0 221 37 222 0 223 12 224 0 225 34 226 0 227 11 228 0 229 28 230 0 231 9 232 0 233 30 234 0 235 3 236 0 237 17 238 0 239 5 240 0 241 14 242 0 243 4 244 0 245 10 246 0 247 3 248 0 249 11 250 0 251 3 252 0 253 6 254 0 255 2 256 0 257 7 258 0 259 2 260 0 261 7 262 0 263 4 264 0 265 7 266 0 267 0 268 0 269 6 270 0 271 1 272 0 273 5 274 0 275 2 276 0 277 1 278 0 279 0 280 0 281 2 282 0 283 0 284 0 285 2 286 0 287 0 288 0 289 3 290 0 291 0 292 0 293 1 294 0 295 0 296 0 297 1 298 0 299 0 300 0 301 0 302 0 303 0 304 0 305 1 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 0 400 0

63: Average symbolic conclusion length is 10898166/147416 ≈ 73.93. (Median: 65)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 449 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 147416 minimal D-proofs with conclusions of odd symbolic length. [0/147416 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 7 12 0 13 13 14 0 15 37 16 0 17 102 18 0 19 167 20 0 21 303 22 0 23 524 24 0 25 724 26 0 27 1050 28 0 29 1332 30 0 31 1889 32 0 33 2431 34 0 35 2726 36 0 37 3308 38 0 39 3422 40 0 41 4001 42 0 43 4063 44 0 45 4473 46 0 47 4707 48 0 49 4743 50 0 51 5000 52 0 53 4815 54 0 55 4749 56 0 57 4892 58 0 59 4314 60 0 61 4373 62 0 63 4082 64 0 65 3936 66 0 67 3644 68 0 69 3511 70 0 71 3263 72 0 73 3445 74 0 75 2630 76 0 77 2995 78 0 79 2563 80 0 81 2721 82 0 83 2136 84 0 85 2254 86 0 87 1998 88 0 89 2316 90 0 91 1809 92 0 93 2114 94 0 95 1632 96 0 97 1993 98 0 99 1463 100 0 101 1887 102 0 103 1316 104 0 105 1734 106 0 107 1265 108 0 109 1525 110 0 111 1081 112 0 113 1445 114 0 115 861 116 0 117 1245 118 0 119 855 120 0 121 1089 122 0 123 730 124 0 125 978 126 0 127 591 128 0 129 904 130 0 131 529 132 0 133 712 134 0 135 417 136 0 137 676 138 0 139 358 140 0 141 582 142 0 143 344 144 0 145 525 146 0 147 286 148 0 149 495 150 0 151 288 152 0 153 434 154 0 155 204 156 0 157 412 158 0 159 194 160 0 161 338 162 0 163 201 164 0 165 310 166 0 167 160 168 0 169 352 170 0 171 154 172 0 173 264 174 0 175 118 176 0 177 271 178 0 179 92 180 0 181 204 182 0 183 118 184 0 185 176 186 0 187 80 188 0 189 205 190 0 191 65 192 0 193 164 194 0 195 75 196 0 197 121 198 0 199 57 200 0 201 152 202 0 203 49 204 0 205 108 206 0 207 54 208 0 209 93 210 0 211 33 212 0 213 99 214 0 215 31 216 0 217 88 218 0 219 26 220 0 221 65 222 0 223 22 224 0 225 65 226 0 227 18 228 0 229 44 230 0 231 11 232 0 233 43 234 0 235 10 236 0 237 31 238 0 239 12 240 0 241 29 242 0 243 9 244 0 245 22 246 0 247 4 248 0 249 17 250 0 251 5 252 0 253 15 254 0 255 5 256 0 257 17 258 0 259 2 260 0 261 9 262 0 263 5 264 0 265 9 266 0 267 3 268 0 269 7 270 0 271 0 272 0 273 7 274 0 275 2 276 0 277 5 278 0 279 1 280 0 281 5 282 0 283 0 284 0 285 6 286 0 287 0 288 0 289 3 290 0 291 1 292 0 293 2 294 0 295 2 296 0 297 5 298 0 299 0 300 0 301 2 302 0 303 0 304 0 305 2 306 0 307 0 308 0 309 0 310 0 311 0 312 0 313 0 314 0 315 0 316 0 317 1 318 0 319 0 320 0 321 1 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 0 400 0

65: Average symbolic conclusion length is 16055582/210360 ≈ 76.32. (Median: 67)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 529 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 210360 minimal D-proofs with conclusions of odd symbolic length. [0/210360 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 3 12 0 13 17 14 0 15 48 16 0 17 88 18 0 19 212 20 0 21 385 22 0 23 544 24 0 25 875 26 0 27 1334 28 0 29 1894 30 0 31 2472 32 0 33 2831 34 0 35 3552 36 0 37 4055 38 0 39 4615 40 0 41 5448 42 0 43 5643 44 0 45 6155 46 0 47 6234 48 0 49 6686 50 0 51 6526 52 0 53 6589 54 0 55 6672 56 0 57 6584 58 0 59 6300 60 0 61 6265 62 0 63 5811 64 0 65 5747 66 0 67 5073 68 0 69 5084 70 0 71 4574 72 0 73 4673 74 0 75 3779 76 0 77 4100 78 0 79 3534 80 0 81 3628 82 0 83 3319 84 0 85 3550 86 0 87 3015 88 0 89 3252 90 0 91 2587 92 0 93 3339 94 0 95 2559 96 0 97 3101 98 0 99 2273 100 0 101 2608 102 0 103 2202 104 0 105 2657 106 0 107 1763 108 0 109 2453 110 0 111 1674 112 0 113 2065 114 0 115 1563 116 0 117 1939 118 0 119 1268 120 0 121 1769 122 0 123 1158 124 0 125 1538 126 0 127 975 128 0 129 1466 130 0 131 868 132 0 133 1170 134 0 135 749 136 0 137 1231 138 0 139 600 140 0 141 995 142 0 143 590 144 0 145 834 146 0 147 477 148 0 149 809 150 0 151 394 152 0 153 702 154 0 155 329 156 0 157 611 158 0 159 289 160 0 161 540 162 0 163 262 164 0 165 448 166 0 167 234 168 0 169 453 170 0 171 207 172 0 173 372 174 0 175 187 176 0 177 371 178 0 179 172 180 0 181 309 182 0 183 156 184 0 185 309 186 0 187 129 188 0 189 280 190 0 191 124 192 0 193 259 194 0 195 105 196 0 197 225 198 0 199 102 200 0 201 215 202 0 203 90 204 0 205 184 206 0 207 85 208 0 209 168 210 0 211 72 212 0 213 150 214 0 215 65 216 0 217 147 218 0 219 44 220 0 221 110 222 0 223 43 224 0 225 99 226 0 227 39 228 0 229 84 230 0 231 34 232 0 233 84 234 0 235 28 236 0 237 66 238 0 239 28 240 0 241 59 242 0 243 17 244 0 245 51 246 0 247 13 248 0 249 49 250 0 251 10 252 0 253 34 254 0 255 10 256 0 257 35 258 0 259 6 260 0 261 22 262 0 263 7 264 0 265 23 266 0 267 9 268 0 269 20 270 0 271 8 272 0 273 15 274 0 275 6 276 0 277 12 278 0 279 5 280 0 281 18 282 0 283 1 284 0 285 9 286 0 287 2 288 0 289 5 290 0 291 2 292 0 293 9 294 0 295 2 296 0 297 13 298 0 299 1 300 0 301 5 302 0 303 1 304 0 305 5 306 0 307 0 308 0 309 3 310 0 311 0 312 0 313 4 314 0 315 0 316 0 317 4 318 0 319 0 320 0 321 4 322 0 323 0 324 0 325 0 326 0 327 0 328 0 329 1 330 0 331 0 332 0 333 2 334 0 335 0 336 0 337 2 338 0 339 0 340 0 341 0 342 0 343 0 344 0 345 0 346 0 347 0 348 0 349 1 350 0 351 0 352 0 353 1 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 0 400 0

67: Average symbolic conclusion length is 23399875/299183 ≈ 78.21. (Median: 69)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 529 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 299183 minimal D-proofs with conclusions of odd symbolic length. [0/299183 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 4 12 0 13 15 14 0 15 42 16 0 17 116 18 0 19 230 20 0 21 384 22 0 23 741 24 0 25 1145 26 0 27 1586 28 0 29 2193 30 0 31 2972 32 0 33 3801 34 0 35 4747 36 0 37 5532 38 0 39 6512 40 0 41 6981 42 0 43 7530 44 0 45 8004 46 0 47 8589 48 0 49 8977 50 0 51 8980 52 0 53 9471 54 0 55 9166 56 0 57 9520 58 0 59 8816 60 0 61 8741 62 0 63 8620 64 0 65 7970 66 0 67 7391 68 0 69 7687 70 0 71 6521 72 0 73 6839 74 0 75 5740 76 0 77 6400 78 0 79 5404 80 0 81 5302 82 0 83 4942 84 0 85 5307 86 0 87 4276 88 0 89 4634 90 0 91 3604 92 0 93 4477 94 0 95 3609 96 0 97 4199 98 0 99 3207 100 0 101 3892 102 0 103 2948 104 0 105 3776 106 0 107 2774 108 0 109 3359 110 0 111 2451 112 0 113 3182 114 0 115 2112 116 0 117 2904 118 0 119 1982 120 0 121 2530 122 0 123 1672 124 0 125 2220 126 0 127 1429 128 0 129 2093 130 0 131 1323 132 0 133 1731 134 0 135 1113 136 0 137 1646 138 0 139 981 140 0 141 1436 142 0 143 848 144 0 145 1188 146 0 147 727 148 0 149 1174 150 0 151 632 152 0 153 1009 154 0 155 570 156 0 157 918 158 0 159 510 160 0 161 889 162 0 163 478 164 0 165 757 166 0 167 387 168 0 169 780 170 0 171 357 172 0 173 592 174 0 175 377 176 0 177 614 178 0 179 297 180 0 181 590 182 0 183 293 184 0 185 501 186 0 187 220 188 0 189 489 190 0 191 188 192 0 193 440 194 0 195 216 196 0 197 351 198 0 199 168 200 0 201 407 202 0 203 130 204 0 205 295 206 0 207 154 208 0 209 257 210 0 211 109 212 0 213 274 214 0 215 95 216 0 217 226 218 0 219 101 220 0 221 192 222 0 223 86 224 0 225 215 226 0 227 66 228 0 229 150 230 0 231 65 232 0 233 136 234 0 235 45 236 0 237 139 238 0 239 44 240 0 241 124 242 0 243 31 244 0 245 86 246 0 247 28 248 0 249 86 250 0 251 23 252 0 253 64 254 0 255 17 256 0 257 60 258 0 259 15 260 0 261 46 262 0 263 17 264 0 265 46 266 0 267 10 268 0 269 35 270 0 271 11 272 0 273 26 274 0 275 7 276 0 277 24 278 0 279 8 280 0 281 32 282 0 283 5 284 0 285 17 286 0 287 6 288 0 289 14 290 0 291 6 292 0 293 11 294 0 295 2 296 0 297 13 298 0 299 2 300 0 301 11 302 0 303 5 304 0 305 9 306 0 307 2 308 0 309 6 310 0 311 1 312 0 313 8 314 0 315 0 316 0 317 8 318 0 319 0 320 0 321 8 322 0 323 1 324 0 325 3 326 0 327 1 328 0 329 5 330 0 331 0 332 0 333 2 334 0 335 0 336 0 337 1 338 0 339 0 340 0 341 2 342 0 343 0 344 0 345 3 346 0 347 0 348 0 349 1 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 2 366 0 367 0 368 0 369 2 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

69: Average symbolic conclusion length is 34472716/427694 ≈ 80.60. (Median: 69)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 541 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 427694 minimal D-proofs with conclusions of odd symbolic length. [0/427694 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 2 12 0 13 17 14 0 15 56 16 0 17 140 18 0 19 252 20 0 21 520 22 0 23 886 24 0 25 1358 26 0 27 1962 28 0 29 2799 30 0 31 3873 32 0 33 4956 34 0 35 6058 36 0 37 7046 38 0 39 8106 40 0 41 9193 42 0 43 10347 44 0 45 11202 46 0 47 11932 48 0 49 12118 50 0 51 12629 52 0 53 12875 54 0 55 12761 56 0 57 12843 58 0 59 12340 60 0 61 12800 62 0 63 11576 64 0 65 11764 66 0 67 10804 68 0 69 10827 70 0 71 9519 72 0 73 9596 74 0 75 8500 76 0 77 8625 78 0 79 7712 80 0 81 7535 82 0 83 6622 84 0 85 7299 86 0 87 5938 88 0 89 7083 90 0 91 5700 92 0 93 6565 94 0 95 5055 96 0 97 5959 98 0 99 5157 100 0 101 5912 102 0 103 4611 104 0 105 5416 106 0 107 3942 108 0 109 5257 110 0 111 3782 112 0 113 4458 114 0 115 3494 116 0 117 4320 118 0 119 2945 120 0 121 4160 122 0 123 2702 124 0 125 3363 126 0 127 2451 128 0 129 3275 130 0 131 2065 132 0 133 2909 134 0 135 1868 136 0 137 2609 138 0 139 1524 140 0 141 2380 142 0 143 1448 144 0 145 2004 146 0 147 1214 148 0 149 1945 150 0 151 990 152 0 153 1690 154 0 155 968 156 0 157 1404 158 0 159 829 160 0 161 1465 162 0 163 693 164 0 165 1190 166 0 167 615 168 0 169 1121 170 0 171 530 172 0 173 932 174 0 175 511 176 0 177 878 178 0 179 449 180 0 181 847 182 0 183 414 184 0 185 780 186 0 187 363 188 0 189 687 190 0 191 345 192 0 193 662 194 0 195 311 196 0 197 595 198 0 199 275 200 0 201 583 202 0 203 250 204 0 205 487 206 0 207 224 208 0 209 457 210 0 211 194 212 0 213 424 214 0 215 175 216 0 217 400 218 0 219 155 220 0 221 333 222 0 223 148 224 0 225 310 226 0 227 112 228 0 229 264 230 0 231 100 232 0 233 237 234 0 235 85 236 0 237 202 238 0 239 83 240 0 241 206 242 0 243 68 244 0 245 143 246 0 247 58 248 0 249 138 250 0 251 53 252 0 253 121 254 0 255 48 256 0 257 113 258 0 259 35 260 0 261 80 262 0 263 36 264 0 265 71 266 0 267 23 268 0 269 76 270 0 271 24 272 0 273 79 274 0 275 23 276 0 277 60 278 0 279 14 280 0 281 63 282 0 283 13 284 0 285 38 286 0 287 18 288 0 289 35 290 0 291 10 292 0 293 27 294 0 295 5 296 0 297 27 298 0 299 9 300 0 301 16 302 0 303 13 304 0 305 18 306 0 307 5 308 0 309 18 310 0 311 5 312 0 313 16 314 0 315 3 316 0 317 21 318 0 319 3 320 0 321 19 322 0 323 4 324 0 325 9 326 0 327 4 328 0 329 16 330 0 331 0 332 0 333 12 334 0 335 0 336 0 337 8 338 0 339 2 340 0 341 6 342 0 343 2 344 0 345 10 346 0 347 0 348 0 349 6 350 0 351 0 352 0 353 5 354 0 355 1 356 0 357 2 358 0 359 1 360 0 361 4 362 0 363 0 364 0 365 4 366 0 367 0 368 0 369 3 370 0 371 0 372 0 373 1 374 0 375 0 376 0 377 1 378 0 379 0 380 0 381 1 382 0 383 0 384 0 385 1 386 0 387 0 388 0 389 1 390 0 391 0 392 0 393 1 394 0 395 0 396 0 397 0 398 0 399 0 400 0

71: Average symbolic conclusion length is 50271296/609264 ≈ 82.51. (Median: 71)
    Minimum and maximum symbolic conclusion lengths are 11 (×4) and 577 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 609264 minimal D-proofs with conclusions of odd symbolic length. [0/609264 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 4 12 0 13 20 14 0 15 57 16 0 17 123 18 0 19 305 20 0 21 617 22 0 23 1019 24 0 25 1597 26 0 27 2530 28 0 29 3677 30 0 31 4634 32 0 33 6113 34 0 35 7636 36 0 37 9557 38 0 39 11225 40 0 41 12357 42 0 43 14043 44 0 45 14987 46 0 47 15909 48 0 49 16598 50 0 51 17285 52 0 53 17949 54 0 55 17597 56 0 57 17933 58 0 59 17711 60 0 61 17445 62 0 63 17192 64 0 65 16472 66 0 67 15328 68 0 69 15774 70 0 71 13601 72 0 73 14031 74 0 75 12772 76 0 77 12523 78 0 79 11276 80 0 81 11594 82 0 83 10242 84 0 85 10900 86 0 87 8581 88 0 89 10355 90 0 91 8496 92 0 93 9221 94 0 95 7449 96 0 97 8359 98 0 99 7003 100 0 101 8336 102 0 103 6415 104 0 105 7678 106 0 107 6021 108 0 109 7277 110 0 111 5498 112 0 113 6878 114 0 115 4840 116 0 117 6375 118 0 119 4520 120 0 121 5720 122 0 123 4074 124 0 125 5110 126 0 127 3390 128 0 129 4814 130 0 131 3069 132 0 133 4237 134 0 135 2733 136 0 137 3708 138 0 139 2281 140 0 141 3371 142 0 143 2152 144 0 145 2987 146 0 147 1829 148 0 149 2680 150 0 151 1602 152 0 153 2480 154 0 155 1460 156 0 157 2061 158 0 159 1224 160 0 161 2072 162 0 163 1148 164 0 165 1733 166 0 167 1023 168 0 169 1708 170 0 171 927 172 0 173 1576 174 0 175 911 176 0 177 1429 178 0 179 685 180 0 181 1383 182 0 183 701 184 0 185 1187 186 0 187 660 188 0 189 1098 190 0 191 564 192 0 193 1138 194 0 195 550 196 0 197 918 198 0 199 467 200 0 201 948 202 0 203 386 204 0 205 794 206 0 207 427 208 0 209 693 210 0 211 314 212 0 213 727 214 0 215 267 216 0 217 644 218 0 219 289 220 0 221 501 222 0 223 228 224 0 225 563 226 0 227 203 228 0 229 437 230 0 231 217 232 0 233 412 234 0 235 153 236 0 237 394 238 0 239 140 240 0 241 326 242 0 243 143 244 0 245 270 246 0 247 122 248 0 249 301 250 0 251 89 252 0 253 234 254 0 255 86 256 0 257 198 258 0 259 65 260 0 261 188 262 0 263 60 264 0 265 189 266 0 267 48 268 0 269 140 270 0 271 46 272 0 273 130 274 0 275 38 276 0 277 106 278 0 279 29 280 0 281 100 282 0 283 24 284 0 285 74 286 0 287 34 288 0 289 74 290 0 291 19 292 0 293 48 294 0 295 14 296 0 297 46 298 0 299 13 300 0 301 48 302 0 303 13 304 0 305 47 306 0 307 11 308 0 309 36 310 0 311 9 312 0 313 33 314 0 315 6 316 0 317 24 318 0 319 8 320 0 321 24 322 0 323 8 324 0 325 14 326 0 327 8 328 0 329 23 330 0 331 3 332 0 333 16 334 0 335 4 336 0 337 13 338 0 339 2 340 0 341 14 342 0 343 1 344 0 345 14 346 0 347 2 348 0 349 10 350 0 351 3 352 0 353 11 354 0 355 1 356 0 357 6 358 0 359 2 360 0 361 7 362 0 363 0 364 0 365 9 366 0 367 0 368 0 369 8 370 0 371 2 372 0 373 2 374 0 375 2 376 0 377 4 378 0 379 0 380 0 381 3 382 0 383 0 384 0 385 2 386 0 387 0 388 0 389 2 390 0 391 0 392 0 393 3 394 0 395 0 396 0 397 2 398 0 399 0 400 0

73: Average symbolic conclusion length is 74035707/872065 ≈ 84.90. (Median: 73)
    Minimum and maximum symbolic conclusion lengths are 11 (×10) and 577 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 872065 minimal D-proofs with conclusions of odd symbolic length. [0/872065 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 10 12 0 13 12 14 0 15 47 16 0 17 168 18 0 19 314 20 0 21 663 22 0 23 1148 24 0 25 1949 26 0 27 3144 28 0 29 4257 30 0 31 6106 32 0 33 8121 34 0 35 10119 36 0 37 12518 38 0 39 14043 40 0 41 16666 42 0 43 18429 44 0 45 20084 46 0 47 22014 48 0 49 23175 50 0 51 23979 52 0 53 24752 54 0 55 24483 56 0 57 25188 58 0 59 24638 60 0 61 24820 62 0 63 23406 64 0 65 23462 66 0 67 22539 68 0 69 21836 70 0 71 19971 72 0 73 20279 74 0 75 18320 76 0 77 17968 78 0 79 16027 80 0 81 16533 82 0 83 14267 84 0 85 15335 86 0 87 12442 88 0 89 14033 90 0 91 11803 92 0 93 12933 94 0 95 11278 96 0 97 12767 98 0 99 10398 100 0 101 11718 102 0 103 9358 104 0 105 11753 106 0 107 8958 108 0 109 10759 110 0 111 8197 112 0 113 9852 114 0 115 7726 116 0 117 9222 118 0 119 6500 120 0 121 8772 122 0 123 6113 124 0 125 7662 126 0 127 5752 128 0 129 7255 130 0 131 4800 132 0 133 6775 134 0 135 4432 136 0 137 5706 138 0 139 3962 140 0 141 5430 142 0 143 3412 144 0 145 4865 146 0 147 3092 148 0 149 4309 150 0 151 2532 152 0 153 4152 154 0 155 2377 156 0 157 3402 158 0 159 2034 160 0 161 3380 162 0 163 1712 164 0 165 2833 166 0 167 1738 168 0 169 2533 170 0 171 1440 172 0 173 2506 174 0 175 1276 176 0 177 2216 178 0 179 1120 180 0 181 2019 182 0 183 1010 184 0 185 1901 186 0 187 990 188 0 189 1608 190 0 191 913 192 0 193 1644 194 0 195 799 196 0 197 1453 198 0 199 751 200 0 201 1408 202 0 203 680 204 0 205 1248 206 0 207 639 208 0 209 1231 210 0 211 542 212 0 213 1076 214 0 215 495 216 0 217 1043 218 0 219 453 220 0 221 890 222 0 223 417 224 0 225 849 226 0 227 356 228 0 229 723 230 0 231 315 232 0 233 689 234 0 235 275 236 0 237 619 238 0 239 247 240 0 241 578 242 0 243 209 244 0 245 469 246 0 247 207 248 0 249 478 250 0 251 151 252 0 253 376 254 0 255 142 256 0 257 335 258 0 259 124 260 0 261 300 262 0 263 111 264 0 265 298 266 0 267 87 268 0 269 230 270 0 271 74 272 0 273 195 274 0 275 78 276 0 277 160 278 0 279 80 280 0 281 183 282 0 283 63 284 0 285 132 286 0 287 63 288 0 289 122 290 0 291 38 292 0 293 127 294 0 295 34 296 0 297 111 298 0 299 30 300 0 301 89 302 0 303 26 304 0 305 92 306 0 307 16 308 0 309 63 310 0 311 17 312 0 313 52 314 0 315 19 316 0 317 51 318 0 319 16 320 0 321 59 322 0 323 22 324 0 325 35 326 0 327 20 328 0 329 47 330 0 331 9 332 0 333 40 334 0 335 16 336 0 337 29 338 0 339 12 340 0 341 35 342 0 343 7 344 0 345 44 346 0 347 6 348 0 349 27 350 0 351 10 352 0 353 26 354 0 355 6 356 0 357 20 358 0 359 4 360 0 361 27 362 0 363 2 364 0 365 21 366 0 367 4 368 0 369 18 370 0 371 4 372 0 373 11 374 0 375 3 376 0 377 16 378 0 379 1 380 0 381 11 382 0 383 1 384 0 385 9 386 0 387 1 388 0 389 7 390 0 391 1 392 0 393 11 394 0 395 1 396 0 397 4 398 0 399 1 400 0

75: Average symbolic conclusion length is 108069410/1244628 ≈ 86.83. (Median: 75)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 641 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 1244628 minimal D-proofs with conclusions of odd symbolic length. [0/1244628 ≈ 0.00% 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 14 14 0 15 53 16 0 17 123 18 0 19 344 20 0 21 738 22 0 23 1296 24 0 25 2294 26 0 27 3645 28 0 29 5437 30 0 31 7790 32 0 33 9970 34 0 35 13016 36 0 37 15806 38 0 39 19157 40 0 41 22694 42 0 43 24877 44 0 45 28113 46 0 47 29241 48 0 49 31675 50 0 51 32709 52 0 53 33883 54 0 55 34450 56 0 57 34863 58 0 59 34909 60 0 61 34609 62 0 63 33385 64 0 65 33554 66 0 67 31235 68 0 69 31808 70 0 71 28922 72 0 73 28468 74 0 75 26954 76 0 77 25842 78 0 79 23530 80 0 81 24676 82 0 83 20758 84 0 85 22541 86 0 87 19008 88 0 89 21272 90 0 91 17539 92 0 93 18699 94 0 95 16704 96 0 97 18579 98 0 99 14910 100 0 101 16981 102 0 103 13241 104 0 105 16237 106 0 107 13103 108 0 109 15288 110 0 111 11700 112 0 113 14574 114 0 115 10923 116 0 117 13528 118 0 119 10144 120 0 121 12561 122 0 123 9156 124 0 125 11618 126 0 127 8014 128 0 129 10903 130 0 131 7204 132 0 133 9455 134 0 135 6608 136 0 137 8516 138 0 139 5704 140 0 141 7937 142 0 143 5017 144 0 145 7171 146 0 147 4383 148 0 149 6175 150 0 151 3880 152 0 153 5851 154 0 155 3554 156 0 157 4966 158 0 159 3119 160 0 161 4735 162 0 163 2785 164 0 165 4203 166 0 167 2545 168 0 169 3790 170 0 171 2186 172 0 173 3633 174 0 175 2066 176 0 177 3291 178 0 179 1902 180 0 181 3088 182 0 183 1727 184 0 185 2957 186 0 187 1638 188 0 189 2622 190 0 191 1365 192 0 193 2622 194 0 195 1320 196 0 197 2163 198 0 199 1273 200 0 201 2188 202 0 203 1056 204 0 205 2070 206 0 207 1053 208 0 209 1827 210 0 211 893 212 0 213 1708 214 0 215 760 216 0 217 1636 218 0 219 790 220 0 221 1331 222 0 223 677 224 0 225 1415 226 0 227 544 228 0 229 1146 230 0 231 582 232 0 233 1073 234 0 235 470 236 0 237 1039 238 0 239 422 240 0 241 926 242 0 243 409 244 0 245 810 246 0 247 331 248 0 249 859 250 0 251 286 252 0 253 635 254 0 255 302 256 0 257 588 258 0 259 242 260 0 261 577 262 0 263 205 264 0 265 535 266 0 267 192 268 0 269 424 270 0 271 193 272 0 273 432 274 0 275 145 276 0 277 336 278 0 279 133 280 0 281 336 282 0 283 116 284 0 285 321 286 0 287 98 288 0 289 298 290 0 291 79 292 0 293 231 294 0 295 74 296 0 297 211 298 0 299 50 300 0 301 187 302 0 303 49 304 0 305 170 306 0 307 48 308 0 309 105 310 0 311 47 312 0 313 129 314 0 315 38 316 0 317 95 318 0 319 33 320 0 321 84 322 0 323 25 324 0 325 91 326 0 327 23 328 0 329 100 330 0 331 15 332 0 333 67 334 0 335 23 336 0 337 57 338 0 339 16 340 0 341 49 342 0 343 11 344 0 345 56 346 0 347 15 348 0 349 40 350 0 351 15 352 0 353 48 354 0 355 10 356 0 357 28 358 0 359 10 360 0 361 29 362 0 363 6 364 0 365 36 366 0 367 7 368 0 369 29 370 0 371 9 372 0 373 17 374 0 375 8 376 0 377 30 378 0 379 2 380 0 381 21 382 0 383 4 384 0 385 14 386 0 387 3 388 0 389 17 390 0 391 2 392 0 393 20 394 0 395 2 396 0 397 9 398 0 399 3 400 0

77: Average symbolic conclusion length is 159098876/1782980 ≈ 89.23. (Median: 77)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 1041 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 1782980 minimal D-proofs with conclusions of odd symbolic length. [0/1782980 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 4 12 0 13 10 14 0 15 53 16 0 17 144 18 0 19 379 20 0 21 764 22 0 23 1533 24 0 25 2702 26 0 27 4241 28 0 29 6569 30 0 31 9227 32 0 33 12743 34 0 35 16734 36 0 37 21030 38 0 39 25481 40 0 41 28687 42 0 43 33477 44 0 45 37058 46 0 47 40088 48 0 49 43912 50 0 51 44865 52 0 53 47769 54 0 55 47862 56 0 57 49151 58 0 59 48825 60 0 61 48218 62 0 63 47442 64 0 65 47591 66 0 67 45003 68 0 69 44327 70 0 71 41470 72 0 73 42255 74 0 75 37382 76 0 77 37916 78 0 79 34179 80 0 81 35418 82 0 83 30027 84 0 85 31701 86 0 87 27548 88 0 89 29068 90 0 91 25366 92 0 93 26703 94 0 95 22874 96 0 97 25963 98 0 99 21205 100 0 101 25167 102 0 103 20277 104 0 105 23607 106 0 107 18420 108 0 109 22109 110 0 111 18073 112 0 113 21449 114 0 115 16429 116 0 117 19705 118 0 119 14635 120 0 121 18884 122 0 123 13654 124 0 125 16776 126 0 127 12583 128 0 129 15614 130 0 131 11086 132 0 133 14707 134 0 135 10039 136 0 137 13053 138 0 139 9350 140 0 141 12107 142 0 143 7955 144 0 145 11396 146 0 147 7330 148 0 149 9537 150 0 151 6520 152 0 153 9368 154 0 155 5670 156 0 157 8094 158 0 159 5320 160 0 161 7499 162 0 163 4368 164 0 165 6980 166 0 167 4084 168 0 169 6173 170 0 171 3560 172 0 173 5843 174 0 175 3053 176 0 177 5204 178 0 179 3068 180 0 181 4573 182 0 183 2659 184 0 185 4683 186 0 187 2391 188 0 189 3968 190 0 191 2225 192 0 193 3975 194 0 195 1917 196 0 197 3457 198 0 199 1907 200 0 201 3257 202 0 203 1740 204 0 205 3109 206 0 207 1589 208 0 209 2994 210 0 211 1440 212 0 213 2566 214 0 215 1392 216 0 217 2527 218 0 219 1215 220 0 221 2269 222 0 223 1129 224 0 225 2200 226 0 227 984 228 0 229 1965 230 0 231 900 232 0 233 1886 234 0 235 786 236 0 237 1596 238 0 239 722 240 0 241 1528 242 0 243 664 244 0 245 1326 246 0 247 592 248 0 249 1326 250 0 251 498 252 0 253 1127 254 0 255 485 256 0 257 1008 258 0 259 392 260 0 261 918 262 0 263 348 264 0 265 910 266 0 267 315 268 0 269 702 270 0 271 298 272 0 273 699 274 0 275 249 276 0 277 548 278 0 279 203 280 0 281 539 282 0 283 172 284 0 285 468 286 0 287 185 288 0 289 432 290 0 291 139 292 0 293 364 294 0 295 126 296 0 297 348 298 0 299 132 300 0 301 271 302 0 303 114 304 0 305 276 306 0 307 92 308 0 309 209 310 0 311 89 312 0 313 227 314 0 315 67 316 0 317 194 318 0 319 51 320 0 321 183 322 0 323 54 324 0 325 138 326 0 327 59 328 0 329 163 330 0 331 39 332 0 333 124 334 0 335 47 336 0 337 104 338 0 339 40 340 0 341 108 342 0 343 29 344 0 345 117 346 0 347 37 348 0 349 74 350 0 351 43 352 0 353 90 354 0 355 28 356 0 357 83 358 0 359 26 360 0 361 77 362 0 363 21 364 0 365 75 366 0 367 26 368 0 369 75 370 0 371 21 372 0 373 57 374 0 375 18 376 0 377 66 378 0 379 11 380 0 381 55 382 0 383 15 384 0 385 51 386 0 387 11 388 0 389 41 390 0 391 9 392 0 393 44 394 0 395 7 396 0 397 32 398 0 399 11 400 0

79: Average symbolic conclusion length is 232380238/2547752 ≈ 91.21. (Median: 79)
    Minimum and maximum symbolic conclusion lengths are 11 (×3) and 705 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 2547752 minimal D-proofs with conclusions of odd symbolic length. [0/2547752 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 3 12 0 13 20 14 0 15 51 16 0 17 173 18 0 19 406 20 0 21 809 22 0 23 1660 24 0 25 3020 26 0 27 5053 28 0 29 7865 30 0 31 11382 32 0 33 16082 34 0 35 21073 36 0 37 26200 38 0 39 32489 40 0 41 38897 42 0 43 45316 44 0 45 50342 46 0 47 55484 48 0 49 59677 50 0 51 62663 52 0 53 64888 54 0 55 66715 56 0 57 68861 58 0 59 67763 60 0 61 68703 62 0 63 66811 64 0 65 67454 66 0 67 63526 68 0 69 63467 70 0 71 59930 72 0 73 58627 74 0 75 55082 76 0 77 54481 78 0 79 48806 80 0 81 51242 82 0 83 43514 84 0 85 46636 86 0 87 41117 88 0 89 42120 90 0 91 37499 92 0 93 40341 94 0 95 34430 96 0 97 37686 98 0 99 30607 100 0 101 36733 102 0 103 29653 104 0 105 33882 106 0 107 27214 108 0 109 31469 110 0 111 25655 112 0 113 31039 114 0 115 23497 116 0 117 28380 118 0 119 22257 120 0 121 27122 122 0 123 20228 124 0 125 25311 126 0 127 18265 128 0 129 23412 130 0 131 16830 132 0 133 21239 134 0 135 15335 136 0 137 19696 138 0 139 13287 140 0 141 18025 142 0 143 11815 144 0 145 16409 146 0 147 10887 148 0 149 14205 150 0 151 9472 152 0 153 13505 154 0 155 8415 156 0 157 12078 158 0 159 7485 160 0 161 10811 162 0 163 6590 164 0 165 9886 166 0 167 6098 168 0 169 9105 170 0 171 5402 172 0 173 8212 174 0 175 4986 176 0 177 7678 178 0 179 4543 180 0 181 6807 182 0 183 4072 184 0 185 6905 186 0 187 3887 188 0 189 5966 190 0 191 3498 192 0 193 5955 194 0 195 3261 196 0 197 5442 198 0 199 3098 200 0 201 5169 202 0 203 2591 204 0 205 4799 206 0 207 2572 208 0 209 4383 210 0 211 2390 212 0 213 3992 214 0 215 2079 216 0 217 4060 218 0 219 1985 220 0 221 3392 222 0 223 1794 224 0 225 3436 226 0 227 1492 228 0 229 3039 230 0 231 1532 232 0 233 2743 234 0 235 1262 236 0 237 2563 238 0 239 1157 240 0 241 2421 242 0 243 1116 244 0 245 2049 246 0 247 965 248 0 249 2100 250 0 251 867 252 0 253 1740 254 0 255 885 256 0 257 1679 258 0 259 670 260 0 261 1537 262 0 263 604 264 0 265 1427 266 0 267 610 268 0 269 1203 270 0 271 544 272 0 273 1272 274 0 275 447 276 0 277 1051 278 0 279 439 280 0 281 978 282 0 283 348 284 0 285 873 286 0 287 347 288 0 289 824 290 0 291 334 292 0 293 657 294 0 295 302 296 0 297 733 298 0 299 241 300 0 301 598 302 0 303 211 304 0 305 525 306 0 307 196 308 0 309 499 310 0 311 172 312 0 313 538 314 0 315 110 316 0 317 392 318 0 319 130 320 0 321 351 322 0 323 100 324 0 325 307 326 0 327 87 328 0 329 315 330 0 331 96 332 0 333 235 334 0 335 99 336 0 337 235 338 0 339 67 340 0 341 177 342 0 343 56 344 0 345 179 346 0 347 51 348 0 349 179 350 0 351 57 352 0 353 186 354 0 355 41 356 0 357 132 358 0 359 49 360 0 361 139 362 0 363 31 364 0 365 115 366 0 367 27 368 0 369 105 370 0 371 36 372 0 373 80 374 0 375 29 376 0 377 107 378 0 379 17 380 0 381 77 382 0 383 29 384 0 385 62 386 0 387 21 388 0 389 68 390 0 391 14 392 0 393 79 394 0 395 18 396 0 397 53 398 0 399 20 400 0

81: Average symbolic conclusion length is 342063863/3653261 ≈ 93.63. (Median: 81)
    Minimum and maximum symbolic conclusion lengths are 11 (×5) and 1053 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 3653261 minimal D-proofs with conclusions of odd symbolic length. [0/3653261 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 5 12 0 13 14 14 0 15 55 16 0 17 165 18 0 19 404 20 0 21 929 22 0 23 1878 24 0 25 3376 26 0 27 5780 28 0 29 9261 30 0 31 13810 32 0 33 19663 34 0 35 25931 36 0 37 34374 38 0 39 42888 40 0 41 51116 42 0 43 59250 44 0 45 66801 46 0 47 74514 48 0 49 80958 50 0 51 86054 52 0 53 90874 54 0 55 94143 56 0 57 95023 58 0 59 96191 60 0 61 96955 62 0 63 94777 64 0 65 95218 66 0 67 90278 68 0 69 90644 70 0 71 85471 72 0 73 85330 74 0 75 77640 76 0 77 78928 78 0 79 72166 80 0 81 72441 82 0 83 64010 84 0 85 66734 86 0 87 59066 88 0 89 60646 90 0 91 53008 92 0 93 57338 94 0 95 48592 96 0 97 54127 98 0 99 43969 100 0 101 51032 102 0 103 42317 104 0 105 48483 106 0 107 40376 108 0 109 46819 110 0 111 37416 112 0 113 43786 114 0 115 34738 116 0 117 42392 118 0 119 32377 120 0 121 39696 122 0 123 30046 124 0 125 36636 126 0 127 28021 128 0 129 34205 130 0 131 24769 132 0 133 31895 134 0 135 22586 136 0 137 29372 138 0 139 21014 140 0 141 26216 142 0 143 18462 144 0 145 25100 146 0 147 16861 148 0 149 22031 150 0 151 15422 152 0 153 20794 154 0 155 13402 156 0 157 19004 158 0 159 12462 160 0 161 16653 162 0 163 10885 164 0 165 16046 166 0 167 9752 168 0 169 14461 170 0 171 9048 172 0 173 12834 174 0 175 7849 176 0 177 12711 178 0 179 7287 180 0 181 10729 182 0 183 6430 184 0 185 10805 186 0 187 5742 188 0 189 9246 190 0 191 5692 192 0 193 8753 194 0 195 4883 196 0 197 8476 198 0 199 4614 200 0 201 7835 202 0 203 4233 204 0 205 7243 206 0 207 3813 208 0 209 6971 210 0 211 3693 212 0 213 6085 214 0 215 3474 216 0 217 6210 218 0 219 3034 220 0 221 5534 222 0 223 2877 224 0 225 5214 226 0 227 2605 228 0 229 4810 230 0 231 2410 232 0 233 4708 234 0 235 2215 236 0 237 4020 238 0 239 2058 240 0 241 3941 242 0 243 1759 244 0 245 3505 246 0 247 1642 248 0 249 3392 250 0 251 1450 252 0 253 2931 254 0 255 1394 256 0 257 2879 258 0 259 1209 260 0 261 2520 262 0 263 1052 264 0 265 2419 266 0 267 982 268 0 269 2041 270 0 271 935 272 0 273 2047 274 0 275 737 276 0 277 1687 278 0 279 721 280 0 281 1591 282 0 283 583 284 0 285 1444 286 0 287 561 288 0 289 1356 290 0 291 489 292 0 293 1133 294 0 295 439 296 0 297 1133 298 0 299 388 300 0 301 871 302 0 303 359 304 0 305 882 306 0 307 287 308 0 309 744 310 0 311 283 312 0 313 733 314 0 315 222 316 0 317 595 318 0 319 231 320 0 321 571 322 0 323 203 324 0 325 449 326 0 327 181 328 0 329 491 330 0 331 148 332 0 333 413 334 0 335 165 336 0 337 376 338 0 339 130 340 0 341 345 342 0 343 101 344 0 345 369 346 0 347 113 348 0 349 290 350 0 351 117 352 0 353 300 354 0 355 79 356 0 357 232 358 0 359 88 360 0 361 248 362 0 363 90 364 0 365 225 366 0 367 77 368 0 369 225 370 0 371 78 372 0 373 175 374 0 375 73 376 0 377 203 378 0 379 60 380 0 381 181 382 0 383 65 384 0 385 159 386 0 387 55 388 0 389 152 390 0 391 51 392 0 393 168 394 0 395 45 396 0 397 126 398 0 399 43 400 0

83: Average symbolic conclusion length is 499887011/5226411 ≈ 95.65. (Median: 81)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 1073 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 5226411 minimal D-proofs with conclusions of odd symbolic length. [0/5226411 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 5 12 0 13 19 14 0 15 49 16 0 17 183 18 0 19 416 20 0 21 929 22 0 23 2078 24 0 25 3913 26 0 27 6825 28 0 29 10793 30 0 31 16828 32 0 33 24106 34 0 35 32659 36 0 37 43481 38 0 39 53429 40 0 41 66417 42 0 43 78215 44 0 45 90690 46 0 47 102262 48 0 49 110390 50 0 51 119329 52 0 53 125805 54 0 55 129673 56 0 57 133421 58 0 59 134206 60 0 61 136845 62 0 63 134508 64 0 65 133604 66 0 67 129336 68 0 69 129010 70 0 71 122886 72 0 73 120427 74 0 75 112730 76 0 77 113365 78 0 79 101899 80 0 81 104501 82 0 83 93598 84 0 85 94836 86 0 87 86149 88 0 89 87636 90 0 91 78368 92 0 93 84079 94 0 95 70265 96 0 97 79885 98 0 99 66333 100 0 101 75345 102 0 103 61420 104 0 105 69572 106 0 107 59270 108 0 109 67310 110 0 111 54447 112 0 113 63965 114 0 115 49840 116 0 117 60901 118 0 119 48273 120 0 121 57071 122 0 123 44001 124 0 125 54499 126 0 127 40588 128 0 129 50355 130 0 131 37829 132 0 133 46707 134 0 135 34104 136 0 137 43830 138 0 139 30729 140 0 141 39829 142 0 143 27991 144 0 145 36799 146 0 147 25489 148 0 149 33113 150 0 151 22497 152 0 153 30885 154 0 155 19862 156 0 157 27668 158 0 159 18123 160 0 161 24823 162 0 163 16244 164 0 165 23055 166 0 167 14474 168 0 169 21304 170 0 171 12952 172 0 173 18585 174 0 175 11819 176 0 177 18141 178 0 179 10867 180 0 181 15898 182 0 183 9769 184 0 185 15369 186 0 187 9091 188 0 189 13843 190 0 191 8550 192 0 193 13171 194 0 195 7594 196 0 197 12436 198 0 199 7265 200 0 201 11803 202 0 203 6685 204 0 205 10862 206 0 207 6317 208 0 209 10593 210 0 211 5843 212 0 213 9481 214 0 215 5109 216 0 217 9494 218 0 219 4867 220 0 221 8243 222 0 223 4678 224 0 225 8110 226 0 227 3979 228 0 229 7473 230 0 231 3901 232 0 233 6887 234 0 235 3479 236 0 237 6286 238 0 239 3043 240 0 241 6100 242 0 243 2900 244 0 245 5270 246 0 247 2633 248 0 249 5350 250 0 251 2290 252 0 253 4576 254 0 255 2224 256 0 257 4332 258 0 259 1891 260 0 261 3905 262 0 263 1770 264 0 265 3680 266 0 267 1651 268 0 269 3201 270 0 271 1506 272 0 273 3224 274 0 275 1292 276 0 277 2707 278 0 279 1304 280 0 281 2694 282 0 283 1145 284 0 285 2410 286 0 287 1010 288 0 289 2273 290 0 291 913 292 0 293 1989 294 0 295 845 296 0 297 2059 298 0 299 700 300 0 301 1600 302 0 303 746 304 0 305 1564 306 0 307 630 308 0 309 1442 310 0 311 533 312 0 313 1429 314 0 315 525 316 0 317 1146 318 0 319 541 320 0 321 1129 322 0 323 407 324 0 325 1008 326 0 327 350 328 0 329 961 330 0 331 326 332 0 333 849 334 0 335 320 336 0 337 896 338 0 339 247 340 0 341 698 342 0 343 235 344 0 345 689 346 0 347 188 348 0 349 600 350 0 351 176 352 0 353 563 354 0 355 188 356 0 357 422 358 0 359 188 360 0 361 472 362 0 363 141 364 0 365 403 366 0 367 142 368 0 369 365 370 0 371 119 372 0 373 344 374 0 375 105 376 0 377 392 378 0 379 85 380 0 381 280 382 0 383 106 384 0 385 249 386 0 387 77 388 0 389 223 390 0 391 60 392 0 393 239 394 0 395 72 396 0 397 206 398 0 399 78 400 0