1: Average symbolic conclusion length is 13/1 ≈ 13.00. (Median: 13)
   Minimum and maximum symbolic conclusion lengths are 13 (×1) and 13 (×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 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 240/14 ≈ 17.14. (Median: 16.00)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 29 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 14 minimal D-proofs with conclusions of odd symbolic length. [0/14 ≈ 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 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 383/21 ≈ 18.24. (Median: 19)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 35 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 21 minimal D-proofs with conclusions of odd symbolic length. [0/21 ≈ 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 0 14 0 15 3 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 655/31 ≈ 21.13. (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 31 minimal D-proofs with conclusions of odd symbolic length. [0/31 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 1 10 0 11 2 12 0 13 3 14 0 15 2 16 0 17 4 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 996/42 ≈ 23.71. (Median: 22.00)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 49 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 42 minimal D-proofs with conclusions of odd symbolic length. [0/42 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 3 12 0 13 4 14 0 15 4 16 0 17 1 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 1623/65 ≈ 24.97. (Median: 25)
    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 65 minimal D-proofs with conclusions of odd symbolic length. [0/65 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 1 8 0 9 3 10 0 11 1 12 0 13 1 14 0 15 2 16 0 17 9 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 2574/98 ≈ 26.27. (Median: 25)
    Minimum and maximum symbolic conclusion lengths are 3 (×1) and 61 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 98 minimal D-proofs with conclusions of odd symbolic length. [0/98 ≈ 0.00% even]
1 0 2 0 3 1 4 0 5 0 6 0 7 1 8 0 9 2 10 0 11 2 12 0 13 3 14 0 15 8 16 0 17 10 18 0 19 6 20 0 21 6 22 0 23 9 24 0 25 5 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 4045/135 ≈ 29.96. (Median: 27)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 69 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 135 minimal D-proofs with conclusions of odd symbolic length. [0/135 ≈ 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 4 14 0 15 5 16 0 17 3 18 0 19 10 20 0 21 13 22 0 23 17 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 6383/197 ≈ 32.40. (Median: 29)
    Minimum and maximum symbolic conclusion lengths are 13 (×2) and 73 (×2), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 197 minimal D-proofs with conclusions of odd symbolic length. [0/197 ≈ 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 2 14 0 15 5 16 0 17 10 18 0 19 14 20 0 21 10 22 0 23 13 24 0 25 12 26 0 27 16 28 0 29 17 30 0 31 8 32 0 33 13 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 9476/270 ≈ 35.10. (Median: 31)
    Minimum and maximum symbolic conclusion lengths are 11 (×3) and 89 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 270 minimal D-proofs with conclusions of odd symbolic length. [0/270 ≈ 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 4 14 0 15 5 16 0 17 7 18 0 19 6 20 0 21 17 22 0 23 14 24 0 25 20 26 0 27 22 28 0 29 19 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 14422/388 ≈ 37.17. (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 388 minimal D-proofs with conclusions of odd symbolic length. [0/388 ≈ 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 6 16 0 17 5 18 0 19 14 20 0 21 24 22 0 23 16 24 0 25 20 26 0 27 20 28 0 29 26 30 0 31 23 32 0 33 24 34 0 35 31 36 0 37 16 38 0 39 18 40 0 41 21 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 21717/551 ≈ 39.41. (Median: 35)
    Minimum and maximum symbolic conclusion lengths are 7 (×1) and 113 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 551 minimal D-proofs with conclusions of odd symbolic length. [0/551 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 2 12 0 13 9 14 0 15 6 16 0 17 14 18 0 19 19 20 0 21 8 22 0 23 24 24 0 25 29 26 0 27 28 28 0 29 40 30 0 31 31 32 0 33 37 34 0 35 30 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 32557/783 ≈ 41.58. (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 783 minimal D-proofs with conclusions of odd symbolic length. [0/783 ≈ 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 2 14 0 15 7 16 0 17 10 18 0 19 13 20 0 21 27 22 0 23 38 24 0 25 36 26 0 27 40 28 0 29 36 30 0 31 37 32 0 33 46 34 0 35 45 36 0 37 38 38 0 39 43 40 0 41 48 42 0 43 24 44 0 45 36 46 0 47 30 48 0 49 31 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 48644/1106 ≈ 43.98. (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 1106 minimal D-proofs with conclusions of odd symbolic length. [0/1106 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 1 10 0 11 2 12 0 13 3 14 0 15 9 16 0 17 11 18 0 19 28 20 0 21 27 22 0 23 31 24 0 25 46 26 0 27 50 28 0 29 50 30 0 31 64 32 0 33 63 34 0 35 57 36 0 37 58 38 0 39 60 40 0 41 56 42 0 43 47 44 0 45 35 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 72431/1563 ≈ 46.34. (Median: 43)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 161 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 1563 minimal D-proofs with conclusions of odd symbolic length. [0/1563 ≈ 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 3 14 0 15 5 16 0 17 18 18 0 19 14 20 0 21 28 22 0 23 49 24 0 25 49 26 0 27 75 28 0 29 74 30 0 31 72 32 0 33 74 34 0 35 73 36 0 37 66 38 0 39 69 40 0 41 83 42 0 43 69 44 0 45 69 46 0 47 74 48 0 49 52 50 0 51 61 52 0 53 55 54 0 55 42 56 0 57 45 58 0 59 27 60 0 61 35 62 0 63 21 64 0 65 27 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 107265/2211 ≈ 48.51. (Median: 43)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 161 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 2211 minimal D-proofs with conclusions of odd symbolic length. [0/2211 ≈ 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 5 14 0 15 16 16 0 17 17 18 0 19 33 20 0 21 42 22 0 23 43 24 0 25 76 26 0 27 68 28 0 29 92 30 0 31 98 32 0 33 99 34 0 35 111 36 0 37 112 38 0 39 110 40 0 41 93 42 0 43 89 44 0 45 107 46 0 47 96 48 0 49 72 50 0 51 58 52 0 53 60 54 0 55 65 56 0 57 59 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 158068/3116 ≈ 50.73. (Median: 47)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 185 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 3116 minimal D-proofs with conclusions of odd symbolic length. [0/3116 ≈ 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 7 14 0 15 13 16 0 17 21 18 0 19 33 20 0 21 42 22 0 23 62 24 0 25 78 26 0 27 89 28 0 29 127 30 0 31 109 32 0 33 139 34 0 35 135 36 0 37 152 38 0 39 151 40 0 41 126 42 0 43 122 44 0 45 122 46 0 47 135 48 0 49 114 50 0 51 116 52 0 53 121 54 0 55 71 56 0 57 111 58 0 59 81 60 0 61 85 62 0 63 65 64 0 65 62 66 0 67 49 68 0 69 54 70 0 71 36 72 0 73 48 74 0 75 37 76 0 77 40 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 232942/4400 ≈ 52.94. (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 4400 minimal D-proofs with conclusions of odd symbolic length. [0/4400 ≈ 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 3 14 0 15 14 16 0 17 24 18 0 19 34 20 0 21 70 22 0 23 83 24 0 25 92 26 0 27 120 28 0 29 127 30 0 31 181 32 0 33 178 34 0 35 170 36 0 37 215 38 0 39 188 40 0 41 199 42 0 43 202 44 0 45 180 46 0 47 151 48 0 49 157 50 0 51 174 52 0 53 163 54 0 55 110 56 0 57 108 58 0 59 103 60 0 61 108 62 0 63 85 64 0 65 94 66 0 67 74 68 0 69 77 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 343523/6223 ≈ 55.20. (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 6223 minimal D-proofs with conclusions of odd symbolic length. [0/6223 ≈ 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 5 14 0 15 7 16 0 17 23 18 0 19 51 20 0 21 61 22 0 23 88 24 0 25 117 26 0 27 154 28 0 29 187 30 0 31 202 32 0 33 218 34 0 35 264 36 0 37 238 38 0 39 260 40 0 41 289 42 0 43 269 44 0 45 246 46 0 47 224 48 0 49 228 50 0 51 191 52 0 53 220 54 0 55 189 56 0 57 202 58 0 59 172 60 0 61 152 62 0 63 177 64 0 65 157 66 0 67 124 68 0 69 133 70 0 71 81 72 0 73 114 74 0 75 85 76 0 77 101 78 0 79 67 80 0 81 96 82 0 83 57 84 0 85 76 86 0 87 48 88 0 89 69 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 503186/8774 ≈ 57.35. (Median: 51)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 209 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 8774 minimal D-proofs with conclusions of odd symbolic length. [0/8774 ≈ 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 5 14 0 15 12 16 0 17 18 18 0 19 44 20 0 21 82 22 0 23 117 24 0 25 148 26 0 27 207 28 0 29 195 30 0 31 258 32 0 33 311 34 0 35 334 36 0 37 356 38 0 39 352 40 0 41 360 42 0 43 385 44 0 45 364 46 0 47 329 48 0 49 357 50 0 51 297 52 0 53 282 54 0 55 265 56 0 57 294 58 0 59 252 60 0 61 195 62 0 63 176 64 0 65 203 66 0 67 169 68 0 69 172 70 0 71 146 72 0 73 155 74 0 75 103 76 0 77 174 78 0 79 130 80 0 81 132 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 739457/12413 ≈ 59.57. (Median: 53)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 257 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 12413 minimal D-proofs with conclusions of odd symbolic length. [0/12413 ≈ 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 2 14 0 15 15 16 0 17 35 18 0 19 51 20 0 21 83 22 0 23 114 24 0 25 194 26 0 27 202 28 0 29 274 30 0 31 362 32 0 33 384 34 0 35 429 36 0 37 442 38 0 39 458 40 0 41 508 42 0 43 466 44 0 45 503 46 0 47 522 48 0 49 498 50 0 51 421 52 0 53 395 54 0 55 378 56 0 57 343 58 0 59 353 60 0 61 330 62 0 63 318 64 0 65 313 66 0 67 232 68 0 69 331 70 0 71 230 72 0 73 267 74 0 75 194 76 0 77 205 78 0 79 166 80 0 81 210 82 0 83 131 84 0 85 170 86 0 87 134 88 0 89 156 90 0 91 110 92 0 93 138 94 0 95 89 96 0 97 124 98 0 99 75 100 0 101 121 102 0 103 78 104 0 105 88 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 1080789/17529 ≈ 61.66. (Median: 55)
    Minimum and maximum symbolic conclusion lengths are 13 (×9) and 233 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 17529 minimal D-proofs with conclusions of odd symbolic length. [0/17529 ≈ 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 9 14 0 15 12 16 0 17 34 18 0 19 56 20 0 21 88 22 0 23 160 24 0 25 209 26 0 27 294 28 0 29 406 30 0 31 372 32 0 33 504 34 0 35 505 36 0 37 640 38 0 39 654 40 0 41 636 42 0 43 713 44 0 45 691 46 0 47 649 48 0 49 701 50 0 51 610 52 0 53 616 54 0 55 595 56 0 57 536 58 0 59 483 60 0 61 476 62 0 63 470 64 0 65 440 66 0 67 311 68 0 69 358 70 0 71 320 72 0 73 348 74 0 75 257 76 0 77 302 78 0 79 230 80 0 81 268 82 0 83 249 84 0 85 279 86 0 87 176 88 0 89 272 90 0 91 155 92 0 93 231 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 1586563/24829 ≈ 63.90. (Median: 57)
    Minimum and maximum symbolic conclusion lengths are 11 (×4) and 263 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 24829 minimal D-proofs with conclusions of odd symbolic length. [0/24829 ≈ 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 7 14 0 15 15 16 0 17 36 18 0 19 60 20 0 21 111 22 0 23 196 24 0 25 244 26 0 27 342 28 0 29 401 30 0 31 540 32 0 33 656 34 0 35 706 36 0 37 818 38 0 39 811 40 0 41 936 42 0 43 857 44 0 45 943 46 0 47 978 48 0 49 893 50 0 51 870 52 0 53 942 54 0 55 851 56 0 57 729 58 0 59 664 60 0 61 686 62 0 63 561 64 0 65 626 66 0 67 526 68 0 69 589 70 0 71 460 72 0 73 479 74 0 75 498 76 0 77 491 78 0 79 397 80 0 81 428 82 0 83 283 84 0 85 399 86 0 87 301 88 0 89 349 90 0 91 247 92 0 93 342 94 0 95 203 96 0 97 289 98 0 99 189 100 0 101 258 102 0 103 160 104 0 105 237 106 0 107 151 108 0 109 196 110 0 111 111 112 0 113 189 114 0 115 103 116 0 117 138 118 0 119 80 120 0 121 140 122 0 123 52 124 0 125 93 126 0 127 49 128 0 129 82 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 2316006/35088 ≈ 66.01. (Median: 59)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 273 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 35088 minimal D-proofs with conclusions of odd symbolic length. [0/35088 ≈ 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 8 14 0 15 17 16 0 17 40 18 0 19 75 20 0 21 117 22 0 23 159 24 0 25 307 26 0 27 449 28 0 29 555 30 0 31 737 32 0 33 789 34 0 35 910 36 0 37 980 38 0 39 1164 40 0 41 1185 42 0 43 1231 44 0 45 1347 46 0 47 1235 48 0 49 1348 50 0 51 1241 52 0 53 1198 54 0 55 1172 56 0 57 1134 58 0 59 1028 60 0 61 1097 62 0 63 834 64 0 65 881 66 0 67 797 68 0 69 858 70 0 71 685 72 0 73 626 74 0 75 575 76 0 77 662 78 0 79 523 80 0 81 582 82 0 83 462 84 0 85 534 86 0 87 380 88 0 89 558 90 0 91 380 92 0 93 453 94 0 95 382 96 0 97 406 98 0 99 310 100 0 101 425 102 0 103 235 104 0 105 356 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 3400129/49805 ≈ 68.27. (Median: 61)
    Minimum and maximum symbolic conclusion lengths are 9 (×1) and 281 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 49805 minimal D-proofs with conclusions of odd symbolic length. [0/49805 ≈ 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 2 14 0 15 25 16 0 17 37 18 0 19 73 20 0 21 140 22 0 23 266 24 0 25 364 26 0 27 488 28 0 29 653 30 0 31 819 32 0 33 967 34 0 35 1222 36 0 37 1413 38 0 39 1519 40 0 41 1533 42 0 43 1708 44 0 45 1699 46 0 47 1774 48 0 49 1760 50 0 51 1742 52 0 53 1819 54 0 55 1562 56 0 57 1589 58 0 59 1552 60 0 61 1522 62 0 63 1230 64 0 65 1235 66 0 67 1105 68 0 69 1060 70 0 71 1019 72 0 73 1056 74 0 75 924 76 0 77 913 78 0 79 726 80 0 81 999 82 0 83 747 84 0 85 895 86 0 87 635 88 0 89 697 90 0 91 603 92 0 93 727 94 0 95 471 96 0 97 642 98 0 99 471 100 0 101 554 102 0 103 405 104 0 105 535 106 0 107 322 108 0 109 443 110 0 111 297 112 0 113 451 114 0 115 246 116 0 117 363 118 0 119 228 120 0 121 299 122 0 123 168 124 0 125 300 126 0 127 162 128 0 129 241 130 0 131 110 132 0 133 202 134 0 135 93 136 0 137 163 138 0 139 82 140 0 141 132 142 0 143 73 144 0 145 140 146 0 147 53 148 0 149 102 150 0 151 39 152 0 153 94 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 4963593/70539 ≈ 70.37. (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 70539 minimal D-proofs with conclusions of odd symbolic length. [0/70539 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 0 11 2 12 0 13 12 14 0 15 17 16 0 17 43 18 0 19 83 20 0 21 178 22 0 23 252 24 0 25 405 26 0 27 591 28 0 29 840 30 0 31 1069 32 0 33 1357 34 0 35 1621 36 0 37 1649 38 0 39 1913 40 0 41 2102 42 0 43 2276 44 0 45 2428 46 0 47 2391 48 0 49 2468 50 0 51 2535 52 0 53 2345 54 0 55 2334 56 0 57 2328 58 0 59 2055 60 0 61 2141 62 0 63 1834 64 0 65 1981 66 0 67 1735 68 0 69 1593 70 0 71 1483 72 0 73 1545 74 0 75 1331 76 0 77 1309 78 0 79 1000 80 0 81 1257 82 0 83 1034 84 0 85 1157 86 0 87 874 88 0 89 1044 90 0 91 789 92 0 93 987 94 0 95 798 96 0 97 926 98 0 99 634 100 0 101 891 102 0 103 562 104 0 105 786 106 0 107 593 108 0 109 633 110 0 111 452 112 0 113 632 114 0 115 377 116 0 117 571 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 175 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 7284105/100323 ≈ 72.61. (Median: 63)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 513 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 100323 minimal D-proofs with conclusions of odd symbolic length. [0/100323 ≈ 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 10 14 0 15 23 16 0 17 49 18 0 19 129 20 0 21 174 22 0 23 324 24 0 25 555 26 0 27 780 28 0 29 1103 30 0 31 1228 32 0 33 1619 34 0 35 1866 36 0 37 2279 38 0 39 2658 40 0 41 2846 42 0 43 3099 44 0 45 3159 46 0 47 3170 48 0 49 3420 50 0 51 3292 52 0 53 3448 54 0 55 3257 56 0 57 3220 58 0 59 3080 60 0 61 2904 62 0 63 2698 64 0 65 2747 66 0 67 2526 68 0 69 2251 70 0 71 2021 72 0 73 2126 74 0 75 1727 76 0 77 2008 78 0 79 1667 80 0 81 1888 82 0 83 1430 84 0 85 1610 86 0 87 1523 88 0 89 1649 90 0 91 1326 92 0 93 1471 94 0 95 1039 96 0 97 1482 98 0 99 1049 100 0 101 1186 102 0 103 937 104 0 105 1185 106 0 107 768 108 0 109 1068 110 0 111 714 112 0 113 907 114 0 115 603 116 0 117 873 118 0 119 537 120 0 121 734 122 0 123 457 124 0 125 721 126 0 127 359 128 0 129 598 130 0 131 366 132 0 133 481 134 0 135 283 136 0 137 486 138 0 139 236 140 0 141 392 142 0 143 183 144 0 145 354 146 0 147 153 148 0 149 277 150 0 151 154 152 0 153 250 154 0 155 123 156 0 157 225 158 0 159 103 160 0 161 195 162 0 163 84 164 0 165 181 166 0 167 85 168 0 169 166 170 0 171 76 172 0 173 150 174 0 175 60 176 0 177 145 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 10638792/142420 ≈ 74.70. (Median: 65)
    Minimum and maximum symbolic conclusion lengths are 13 (×6) and 449 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 142420 minimal D-proofs with conclusions of odd symbolic length. [0/142420 ≈ 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 6 14 0 15 27 16 0 17 77 18 0 19 110 20 0 21 226 22 0 23 425 24 0 25 582 26 0 27 888 28 0 29 1175 30 0 31 1698 32 0 33 2243 34 0 35 2516 36 0 37 3129 38 0 39 3229 40 0 41 3806 42 0 43 3868 44 0 45 4313 46 0 47 4490 48 0 49 4550 50 0 51 4814 52 0 53 4639 54 0 55 4619 56 0 57 4728 58 0 59 4199 60 0 61 4258 62 0 63 3952 64 0 65 3783 66 0 67 3551 68 0 69 3437 70 0 71 3189 72 0 73 3339 74 0 75 2539 76 0 77 2901 78 0 79 2501 80 0 81 2661 82 0 83 2097 84 0 85 2187 86 0 87 1959 88 0 89 2262 90 0 91 1775 92 0 93 2073 94 0 95 1616 96 0 97 1949 98 0 99 1448 100 0 101 1871 102 0 103 1296 104 0 105 1706 106 0 107 1250 108 0 109 1498 110 0 111 1075 112 0 113 1426 114 0 115 860 116 0 117 1236 118 0 119 853 120 0 121 1087 122 0 123 729 124 0 125 975 126 0 127 591 128 0 129 902 130 0 131 529 132 0 133 710 134 0 135 417 136 0 137 674 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 193 160 0 161 338 162 0 163 201 164 0 165 310 166 0 167 160 168 0 169 351 170 0 171 154 172 0 173 263 174 0 175 118 176 0 177 270 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 15606810/202794 ≈ 76.96. (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 202794 minimal D-proofs with conclusions of odd symbolic length. [0/202794 ≈ 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 10 14 0 15 28 16 0 17 50 18 0 19 139 20 0 21 278 22 0 23 429 24 0 25 688 26 0 27 1103 28 0 29 1670 30 0 31 2203 32 0 33 2593 34 0 35 3285 36 0 37 3777 38 0 39 4307 40 0 41 5148 42 0 43 5394 44 0 45 5916 46 0 47 5965 48 0 49 6436 50 0 51 6292 52 0 53 6334 54 0 55 6469 56 0 57 6349 58 0 59 6174 60 0 61 6095 62 0 63 5620 64 0 65 5560 66 0 67 4941 68 0 69 5002 70 0 71 4497 72 0 73 4576 74 0 75 3702 76 0 77 3979 78 0 79 3462 80 0 81 3547 82 0 83 3252 84 0 85 3476 86 0 87 2948 88 0 89 3149 90 0 91 2516 92 0 93 3259 94 0 95 2503 96 0 97 3020 98 0 99 2220 100 0 101 2548 102 0 103 2149 104 0 105 2597 106 0 107 1724 108 0 109 2388 110 0 111 1645 112 0 113 2015 114 0 115 1530 116 0 117 1897 118 0 119 1236 120 0 121 1718 122 0 123 1137 124 0 125 1495 126 0 127 959 128 0 129 1433 130 0 131 853 132 0 133 1147 134 0 135 731 136 0 137 1206 138 0 139 585 140 0 141 968 142 0 143 578 144 0 145 812 146 0 147 469 148 0 149 793 150 0 151 390 152 0 153 686 154 0 155 326 156 0 157 600 158 0 159 285 160 0 161 530 162 0 163 260 164 0 165 438 166 0 167 232 168 0 169 445 170 0 171 205 172 0 173 367 174 0 175 186 176 0 177 366 178 0 179 171 180 0 181 307 182 0 183 155 184 0 185 307 186 0 187 129 188 0 189 277 190 0 191 124 192 0 193 257 194 0 195 105 196 0 197 224 198 0 199 102 200 0 201 214 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 22811358/288534 ≈ 79.06. (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 288534 minimal D-proofs with conclusions of odd symbolic length. [0/288534 ≈ 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 9 14 0 15 22 16 0 17 65 18 0 19 154 20 0 21 281 22 0 23 549 24 0 25 896 26 0 27 1334 28 0 29 1848 30 0 31 2575 32 0 33 3393 34 0 35 4381 36 0 37 5120 38 0 39 6112 40 0 41 6606 42 0 43 7133 44 0 45 7612 46 0 47 8208 48 0 49 8594 50 0 51 8657 52 0 53 9080 54 0 55 8830 56 0 57 9170 58 0 59 8527 60 0 61 8490 62 0 63 8369 64 0 65 7732 66 0 67 7206 68 0 69 7412 70 0 71 6313 72 0 73 6636 74 0 75 5616 76 0 77 6230 78 0 79 5246 80 0 81 5117 82 0 83 4812 84 0 85 5173 86 0 87 4193 88 0 89 4503 90 0 91 3516 92 0 93 4376 94 0 95 3536 96 0 97 4086 98 0 99 3147 100 0 101 3804 102 0 103 2896 104 0 105 3705 106 0 107 2755 108 0 109 3293 110 0 111 2422 112 0 113 3143 114 0 115 2084 116 0 117 2873 118 0 119 1963 120 0 121 2492 122 0 123 1663 124 0 125 2191 126 0 127 1427 128 0 129 2078 130 0 131 1320 132 0 133 1721 134 0 135 1111 136 0 137 1637 138 0 139 979 140 0 141 1433 142 0 143 846 144 0 145 1185 146 0 147 727 148 0 149 1170 150 0 151 632 152 0 153 1007 154 0 155 569 156 0 157 915 158 0 159 510 160 0 161 886 162 0 163 478 164 0 165 754 166 0 167 387 168 0 169 780 170 0 171 357 172 0 173 592 174 0 175 376 176 0 177 614 178 0 179 296 180 0 181 590 182 0 183 292 184 0 185 500 186 0 187 220 188 0 189 487 190 0 191 188 192 0 193 439 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 33475692/411654 ≈ 81.32. (Median: 71)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 541 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 411654 minimal D-proofs with conclusions of odd symbolic length. [0/411654 ≈ 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 25 16 0 17 81 18 0 19 159 20 0 21 351 22 0 23 649 24 0 25 1089 26 0 27 1572 28 0 29 2335 30 0 31 3389 32 0 33 4376 34 0 35 5503 36 0 37 6455 38 0 39 7612 40 0 41 8595 42 0 43 9762 44 0 45 10614 46 0 47 11370 48 0 49 11609 50 0 51 12179 52 0 53 12321 54 0 55 12329 56 0 57 12351 58 0 59 11918 60 0 61 12369 62 0 63 11218 64 0 65 11476 66 0 67 10553 68 0 69 10475 70 0 71 9234 72 0 73 9329 74 0 75 8355 76 0 77 8451 78 0 79 7567 80 0 81 7335 82 0 83 6458 84 0 85 7127 86 0 87 5807 88 0 89 6897 90 0 91 5590 92 0 93 6413 94 0 95 4930 96 0 97 5799 98 0 99 5052 100 0 101 5751 102 0 103 4504 104 0 105 5288 106 0 107 3850 108 0 109 5132 110 0 111 3699 112 0 113 4356 114 0 115 3412 116 0 117 4222 118 0 119 2881 120 0 121 4067 122 0 123 2652 124 0 125 3287 126 0 127 2398 128 0 129 3199 130 0 131 2020 132 0 133 2830 134 0 135 1835 136 0 137 2543 138 0 139 1500 140 0 141 2327 142 0 143 1423 144 0 145 1958 146 0 147 1187 148 0 149 1905 150 0 151 968 152 0 153 1649 154 0 155 952 156 0 157 1366 158 0 159 813 160 0 161 1434 162 0 163 682 164 0 165 1167 166 0 167 605 168 0 169 1102 170 0 171 520 172 0 173 914 174 0 175 503 176 0 177 859 178 0 179 444 180 0 181 830 182 0 183 409 184 0 185 763 186 0 187 361 188 0 189 671 190 0 191 343 192 0 193 651 194 0 195 308 196 0 197 589 198 0 199 273 200 0 201 576 202 0 203 249 204 0 205 483 206 0 207 223 208 0 209 454 210 0 211 194 212 0 213 421 214 0 215 175 216 0 217 398 218 0 219 155 220 0 221 332 222 0 223 148 224 0 225 309 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 48939885/586547 ≈ 83.44. (Median: 73)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 577 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 586547 minimal D-proofs with conclusions of odd symbolic length. [0/586547 ≈ 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 31 16 0 17 62 18 0 19 182 20 0 21 417 22 0 23 743 24 0 25 1199 26 0 27 1997 28 0 29 3098 30 0 31 3903 32 0 33 5352 34 0 35 6806 36 0 37 8646 38 0 39 10388 40 0 41 11531 42 0 43 13274 44 0 45 14195 46 0 47 15167 48 0 49 15798 50 0 51 16566 52 0 53 17186 54 0 55 16890 56 0 57 17334 58 0 59 17020 60 0 61 16796 62 0 63 16628 64 0 65 15910 66 0 67 14895 68 0 69 15271 70 0 71 13238 72 0 73 13641 74 0 75 12366 76 0 77 12071 78 0 79 10969 80 0 81 11280 82 0 83 10005 84 0 85 10573 86 0 87 8315 88 0 89 10040 90 0 91 8284 92 0 93 8990 94 0 95 7268 96 0 97 8136 98 0 99 6858 100 0 101 8104 102 0 103 6269 104 0 105 7499 106 0 107 5901 108 0 109 7105 110 0 111 5405 112 0 113 6730 114 0 115 4763 116 0 117 6247 118 0 119 4477 120 0 121 5619 122 0 123 4040 124 0 125 5062 126 0 127 3351 128 0 129 4759 130 0 131 3040 132 0 133 4178 134 0 135 2718 136 0 137 3662 138 0 139 2271 140 0 141 3343 142 0 143 2143 144 0 145 2966 146 0 147 1826 148 0 149 2664 150 0 151 1599 152 0 153 2472 154 0 155 1456 156 0 157 2050 158 0 159 1221 160 0 161 2059 162 0 163 1145 164 0 165 1730 166 0 167 1020 168 0 169 1702 170 0 171 923 172 0 173 1570 174 0 175 911 176 0 177 1426 178 0 179 685 180 0 181 1376 182 0 183 701 184 0 185 1182 186 0 187 660 188 0 189 1097 190 0 191 563 192 0 193 1138 194 0 195 548 196 0 197 915 198 0 199 466 200 0 201 944 202 0 203 386 204 0 205 793 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 71816185/837981 ≈ 85.70. (Median: 75)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 577 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 837981 minimal D-proofs with conclusions of odd symbolic length. [0/837981 ≈ 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 3 14 0 15 19 16 0 17 96 18 0 19 197 20 0 21 426 22 0 23 787 24 0 25 1474 26 0 27 2427 28 0 29 3438 30 0 31 5136 32 0 33 7029 34 0 35 8966 36 0 37 11346 38 0 39 12794 40 0 41 15501 42 0 43 17226 44 0 45 18941 46 0 47 20908 48 0 49 21993 50 0 51 22881 52 0 53 23660 54 0 55 23574 56 0 57 24261 58 0 59 23689 60 0 61 23957 62 0 63 22598 64 0 65 22597 66 0 67 21843 68 0 69 21069 70 0 71 19525 72 0 73 19717 74 0 75 17781 76 0 77 17389 78 0 79 15626 80 0 81 16157 82 0 83 13972 84 0 85 14972 86 0 87 12150 88 0 89 13631 90 0 91 11539 92 0 93 12594 94 0 95 11023 96 0 97 12472 98 0 99 10171 100 0 101 11388 102 0 103 9143 104 0 105 11479 106 0 107 8757 108 0 109 10503 110 0 111 8034 112 0 113 9574 114 0 115 7562 116 0 117 9014 118 0 119 6358 120 0 121 8571 122 0 123 5975 124 0 125 7487 126 0 127 5630 128 0 129 7097 130 0 131 4702 132 0 133 6625 134 0 135 4347 136 0 137 5586 138 0 139 3876 140 0 141 5317 142 0 143 3341 144 0 145 4745 146 0 147 3037 148 0 149 4206 150 0 151 2487 152 0 153 4060 154 0 155 2335 156 0 157 3327 158 0 159 1993 160 0 161 3315 162 0 163 1673 164 0 165 2763 166 0 167 1707 168 0 169 2462 170 0 171 1416 172 0 173 2455 174 0 175 1257 176 0 177 2166 178 0 179 1102 180 0 181 1974 182 0 183 991 184 0 185 1862 186 0 187 973 188 0 189 1576 190 0 191 896 192 0 193 1614 194 0 195 783 196 0 197 1428 198 0 199 740 200 0 201 1378 202 0 203 674 204 0 205 1220 206 0 207 632 208 0 209 1209 210 0 211 538 212 0 213 1054 214 0 215 492 216 0 217 1024 218 0 219 450 220 0 221 879 222 0 223 415 224 0 225 838 226 0 227 355 228 0 229 719 230 0 231 314 232 0 233 685 234 0 235 275 236 0 237 615 238 0 239 247 240 0 241 575 242 0 243 209 244 0 245 468 246 0 247 207 248 0 249 477 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 105058841/1196203 ≈ 87.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 1196203 minimal D-proofs with conclusions of odd symbolic length. [0/1196203 ≈ 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 4 14 0 15 28 16 0 17 62 18 0 19 200 20 0 21 466 22 0 23 877 24 0 25 1672 26 0 27 2811 28 0 29 4302 30 0 31 6479 32 0 33 8510 34 0 35 11348 36 0 37 14007 38 0 39 17333 40 0 41 20946 42 0 43 22984 44 0 45 26420 46 0 47 27698 48 0 49 30094 50 0 51 31200 52 0 53 32417 54 0 55 32977 56 0 57 33436 58 0 59 33546 60 0 61 33291 62 0 63 32315 64 0 65 32278 66 0 67 30176 68 0 69 30729 70 0 71 27980 72 0 73 27517 74 0 75 26173 76 0 77 25070 78 0 79 22888 80 0 81 23784 82 0 83 20093 84 0 85 21868 86 0 87 18531 88 0 89 20683 90 0 91 17048 92 0 93 18064 94 0 95 16267 96 0 97 18068 98 0 99 14558 100 0 101 16484 102 0 103 12905 104 0 105 15806 106 0 107 12793 108 0 109 14899 110 0 111 11448 112 0 113 14179 114 0 115 10697 116 0 117 13257 118 0 119 9958 120 0 121 12264 122 0 123 8998 124 0 125 11367 126 0 127 7897 128 0 129 10700 130 0 131 7146 132 0 133 9304 134 0 135 6550 136 0 137 8415 138 0 139 5643 140 0 141 7851 142 0 143 4971 144 0 145 7069 146 0 147 4354 148 0 149 6098 150 0 151 3859 152 0 153 5790 154 0 155 3538 156 0 157 4923 158 0 159 3111 160 0 161 4695 162 0 163 2774 164 0 165 4178 166 0 167 2530 168 0 169 3759 170 0 171 2183 172 0 173 3608 174 0 175 2059 176 0 177 3271 178 0 179 1896 180 0 181 3073 182 0 183 1724 184 0 185 2940 186 0 187 1631 188 0 189 2615 190 0 191 1360 192 0 193 2615 194 0 195 1319 196 0 197 2154 198 0 199 1273 200 0 201 2181 202 0 203 1053 204 0 205 2063 206 0 207 1049 208 0 209 1818 210 0 211 892 212 0 213 1702 214 0 215 760 216 0 217 1633 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 94 318 0 319 33 320 0 321 83 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 154158283/1710627 ≈ 90.12. (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 1710627 minimal D-proofs with conclusions of odd symbolic length. [0/1710627 ≈ 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 2 14 0 15 25 16 0 17 74 18 0 19 214 20 0 21 478 22 0 23 1009 24 0 25 1869 26 0 27 3170 28 0 29 5103 30 0 31 7554 32 0 33 10608 34 0 35 14399 36 0 37 18726 38 0 39 22916 40 0 41 26182 42 0 43 30953 44 0 45 34611 46 0 47 37708 48 0 49 41426 50 0 51 42711 52 0 53 45655 54 0 55 45702 56 0 57 47003 58 0 59 46855 60 0 61 46319 62 0 63 45851 64 0 65 45694 66 0 67 43564 68 0 69 42688 70 0 71 40066 72 0 73 40760 74 0 75 36243 76 0 77 36848 78 0 79 33307 80 0 81 34190 82 0 83 29123 84 0 85 30794 86 0 87 26928 88 0 89 28296 90 0 91 24821 92 0 93 25915 94 0 95 22289 96 0 97 25260 98 0 99 20692 100 0 101 24500 102 0 103 19846 104 0 105 22969 106 0 107 17968 108 0 109 21561 110 0 111 17697 112 0 113 20888 114 0 115 16072 116 0 117 19268 118 0 119 14300 120 0 121 18441 122 0 123 13402 124 0 125 16345 126 0 127 12333 128 0 129 15237 130 0 131 10840 132 0 133 14402 134 0 135 9825 136 0 137 12761 138 0 139 9158 140 0 141 11836 142 0 143 7802 144 0 145 11143 146 0 147 7194 148 0 149 9340 150 0 151 6391 152 0 153 9165 154 0 155 5559 156 0 157 7906 158 0 159 5222 160 0 161 7330 162 0 163 4290 164 0 165 6839 166 0 167 4016 168 0 169 6032 170 0 171 3488 172 0 173 5729 174 0 175 2982 176 0 177 5087 178 0 179 3015 180 0 181 4459 182 0 183 2609 184 0 185 4575 186 0 187 2344 188 0 189 3883 190 0 191 2185 192 0 193 3886 194 0 195 1885 196 0 197 3378 198 0 199 1877 200 0 201 3182 202 0 203 1715 204 0 205 3046 206 0 207 1559 208 0 209 2939 210 0 211 1412 212 0 213 2520 214 0 215 1370 216 0 217 2477 218 0 219 1193 220 0 221 2229 222 0 223 1110 224 0 225 2159 226 0 227 973 228 0 229 1925 230 0 231 889 232 0 233 1852 234 0 235 782 236 0 237 1564 238 0 239 718 240 0 241 1504 242 0 243 660 244 0 245 1312 246 0 247 589 248 0 249 1309 250 0 251 497 252 0 253 1117 254 0 255 484 256 0 257 999 258 0 259 392 260 0 261 913 262 0 263 348 264 0 265 906 266 0 267 315 268 0 269 700 270 0 271 298 272 0 273 697 274 0 275 249 276 0 277 548 278 0 279 203 280 0 281 539 282 0 283 172 284 0 285 467 286 0 287 185 288 0 289 431 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 225585748/2444582 ≈ 92.28. (Median: 79)
    Minimum and maximum symbolic conclusion lengths are 11 (×1) and 705 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 2444582 minimal D-proofs with conclusions of odd symbolic length. [0/2444582 ≈ 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 7 14 0 15 24 16 0 17 87 18 0 19 224 20 0 21 478 22 0 23 1073 24 0 25 2101 26 0 27 3724 28 0 29 6082 30 0 31 9046 32 0 33 13255 34 0 35 18128 36 0 37 22703 38 0 39 28830 40 0 41 35114 42 0 43 41558 44 0 45 46655 46 0 47 51867 48 0 49 56108 50 0 51 59431 52 0 53 61741 54 0 55 63728 56 0 57 65875 58 0 59 65054 60 0 61 65745 62 0 63 64371 64 0 65 64781 66 0 67 61270 68 0 69 61287 70 0 71 57813 72 0 73 56474 74 0 75 53314 76 0 77 52555 78 0 79 47292 80 0 81 49527 82 0 83 42265 84 0 85 45148 86 0 87 39791 88 0 89 40592 90 0 91 36437 92 0 93 39100 94 0 95 33546 96 0 97 36547 98 0 99 29680 100 0 101 35701 102 0 103 28886 104 0 105 32875 106 0 107 26522 108 0 109 30609 110 0 111 25045 112 0 113 30152 114 0 115 22940 116 0 117 27638 118 0 119 21730 120 0 121 26444 122 0 123 19848 124 0 125 24678 126 0 127 17905 128 0 129 22894 130 0 131 16519 132 0 133 20807 134 0 135 15080 136 0 137 19293 138 0 139 13110 140 0 141 17690 142 0 143 11705 144 0 145 16126 146 0 147 10792 148 0 149 14040 150 0 151 9364 152 0 153 13332 154 0 155 8334 156 0 157 11919 158 0 159 7425 160 0 161 10664 162 0 163 6543 164 0 165 9780 166 0 167 6059 168 0 169 8997 170 0 171 5373 172 0 173 8126 174 0 175 4956 176 0 177 7618 178 0 179 4517 180 0 181 6738 182 0 183 4051 184 0 185 6841 186 0 187 3872 188 0 189 5920 190 0 191 3481 192 0 193 5897 194 0 195 3254 196 0 197 5402 198 0 199 3091 200 0 201 5140 202 0 203 2582 204 0 205 4773 206 0 207 2565 208 0 209 4354 210 0 211 2383 212 0 213 3981 214 0 215 2070 216 0 217 4046 218 0 219 1979 220 0 221 3374 222 0 223 1791 224 0 225 3419 226 0 227 1492 228 0 229 3029 230 0 231 1532 232 0 233 2736 234 0 235 1262 236 0 237 2563 238 0 239 1157 240 0 241 2420 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 99 324 0 325 307 326 0 327 86 328 0 329 314 330 0 331 96 332 0 333 234 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 178 350 0 351 57 352 0 353 185 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 331069287/3499861 ≈ 94.59. (Median: 81)
    Minimum and maximum symbolic conclusion lengths are 11 (×3) and 1053 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 3499861 minimal D-proofs with conclusions of odd symbolic length. [0/3499861 ≈ 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 7 14 0 15 26 16 0 17 83 18 0 19 234 20 0 21 581 22 0 23 1200 24 0 25 2354 26 0 27 4094 28 0 29 6974 30 0 31 10866 32 0 33 16051 34 0 35 21671 36 0 37 29554 38 0 39 37813 40 0 41 45745 42 0 43 54077 44 0 45 61336 46 0 47 69560 48 0 49 75909 50 0 51 81139 52 0 53 86145 54 0 55 89605 56 0 57 90694 58 0 59 92306 60 0 61 92674 62 0 63 91022 64 0 65 91340 66 0 67 87066 68 0 69 87236 70 0 71 82358 72 0 73 82234 74 0 75 75060 76 0 77 75956 78 0 79 69801 80 0 81 69837 82 0 83 62363 84 0 85 64585 86 0 87 57260 88 0 89 58576 90 0 91 51559 92 0 93 55648 94 0 95 47364 96 0 97 52632 98 0 99 42809 100 0 101 49547 102 0 103 41270 104 0 105 47007 106 0 107 39391 108 0 109 45639 110 0 111 36540 112 0 113 42539 114 0 115 33957 116 0 117 41287 118 0 119 31627 120 0 121 38741 122 0 123 29426 124 0 125 35692 126 0 127 27442 128 0 129 33456 130 0 131 24256 132 0 133 31205 134 0 135 22143 136 0 137 28610 138 0 139 20622 140 0 141 25614 142 0 143 18079 144 0 145 24538 146 0 147 16504 148 0 149 21566 150 0 151 15101 152 0 153 20353 154 0 155 13146 156 0 157 18604 158 0 159 12230 160 0 161 16286 162 0 163 10667 164 0 165 15702 166 0 167 9567 168 0 169 14121 170 0 171 8888 172 0 173 12548 174 0 175 7702 176 0 177 12435 178 0 179 7162 180 0 181 10496 182 0 183 6306 184 0 185 10598 186 0 187 5624 188 0 189 9041 190 0 191 5580 192 0 193 8534 194 0 195 4794 196 0 197 8296 198 0 199 4526 200 0 201 7664 202 0 203 4150 204 0 205 7081 206 0 207 3739 208 0 209 6824 210 0 211 3630 212 0 213 5949 214 0 215 3419 216 0 217 6068 218 0 219 2987 220 0 221 5424 222 0 223 2826 224 0 225 5106 226 0 227 2564 228 0 229 4710 230 0 231 2369 232 0 233 4618 234 0 235 2174 236 0 237 3942 238 0 239 2024 240 0 241 3868 242 0 243 1727 244 0 245 3448 246 0 247 1618 248 0 249 3332 250 0 251 1436 252 0 253 2870 254 0 255 1377 256 0 257 2832 258 0 259 1199 260 0 261 2476 262 0 263 1043 264 0 265 2378 266 0 267 977 268 0 269 2014 270 0 271 931 272 0 273 2024 274 0 275 735 276 0 277 1677 278 0 279 719 280 0 281 1579 282 0 283 583 284 0 285 1435 286 0 287 561 288 0 289 1348 290 0 291 488 292 0 293 1128 294 0 295 438 296 0 297 1126 298 0 299 388 300 0 301 868 302 0 303 359 304 0 305 880 306 0 307 287 308 0 309 744 310 0 311 283 312 0 313 732 314 0 315 222 316 0 317 593 318 0 319 231 320 0 321 569 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 289 350 0 351 117 352 0 353 299 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 484597506/5006994 ≈ 96.78. (Median: 83)
    Minimum and maximum symbolic conclusion lengths are 11 (×2) and 1073 (×1), respectively.
    There are 0 minimal D-proofs with conclusions of even symbolic length, and there are 5006994 minimal D-proofs with conclusions of odd symbolic length. [0/5006994 ≈ 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 7 14 0 15 25 16 0 17 98 18 0 19 234 20 0 21 556 22 0 23 1332 24 0 25 2612 26 0 27 4860 28 0 29 8018 30 0 31 13061 32 0 33 19361 34 0 35 26967 36 0 37 37218 38 0 39 46323 40 0 41 58873 42 0 43 70331 44 0 45 82643 46 0 47 94689 48 0 49 102676 50 0 51 112275 52 0 53 118768 54 0 55 122880 56 0 57 127141 58 0 59 128502 60 0 61 130882 62 0 63 129101 64 0 65 128223 66 0 67 124267 68 0 69 123900 70 0 71 118356 72 0 73 115851 74 0 75 109067 76 0 77 109059 78 0 79 98425 80 0 81 100698 82 0 83 90444 84 0 85 91313 86 0 87 83528 88 0 89 84712 90 0 91 75987 92 0 93 81058 94 0 95 67937 96 0 97 77288 98 0 99 64468 100 0 101 73080 102 0 103 59659 104 0 105 67239 106 0 107 57669 108 0 109 65400 110 0 111 52991 112 0 113 62144 114 0 115 48558 116 0 117 59155 118 0 119 47087 120 0 121 55539 122 0 123 42948 124 0 125 53017 126 0 127 39644 128 0 129 49122 130 0 131 37022 132 0 133 45577 134 0 135 33447 136 0 137 42731 138 0 139 30179 140 0 141 39010 142 0 143 27490 144 0 145 36038 146 0 147 25081 148 0 149 32426 150 0 151 22178 152 0 153 30286 154 0 155 19662 156 0 157 27214 158 0 159 17940 160 0 161 24461 162 0 163 16076 164 0 165 22740 166 0 167 14317 168 0 169 20977 170 0 171 12839 172 0 173 18333 174 0 175 11707 176 0 177 17892 178 0 179 10775 180 0 181 15707 182 0 183 9709 184 0 185 15187 186 0 187 9017 188 0 189 13691 190 0 191 8485 192 0 193 13006 194 0 195 7545 196 0 197 12314 198 0 199 7208 200 0 201 11684 202 0 203 6644 204 0 205 10753 206 0 207 6288 208 0 209 10488 210 0 211 5817 212 0 213 9402 214 0 215 5080 216 0 217 9410 218 0 219 4856 220 0 221 8177 222 0 223 4664 224 0 225 8065 226 0 227 3961 228 0 229 7434 230 0 231 3886 232 0 233 6841 234 0 235 3469 236 0 237 6261 238 0 239 3036 240 0 241 6077 242 0 243 2900 244 0 245 5253 246 0 247 2633 248 0 249 5340 250 0 251 2290 252 0 253 4567 254 0 255 2224 256 0 257 4323 258 0 259 1891 260 0 261 3905 262 0 263 1770 264 0 265 3678 266 0 267 1651 268 0 269 3201 270 0 271 1506 272 0 273 3223 274 0 275 1292 276 0 277 2706 278 0 279 1304 280 0 281 2692 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 1428 314 0 315 525 316 0 317 1146 318 0 319 541 320 0 321 1128 322 0 323 407 324 0 325 1008 326 0 327 350 328 0 329 959 330 0 331 326 332 0 333 848 334 0 335 319 336 0 337 896 338 0 339 246 340 0 341 695 342 0 343 235 344 0 345 686 346 0 347 188 348 0 349 600 350 0 351 176 352 0 353 563 354 0 355 187 356 0 357 422 358 0 359 187 360 0 361 471 362 0 363 141 364 0 365 402 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