w1-plot_data_x400.txt

1: Average symbolic conclusion length is 21/1 ≈ 21.00. (Median: 21)
   There are 0 minimal D-proofs with conclusions of even symbolic length, and there is 1 minimal D-proof with a conclusion of odd symbolic length. [0/1 ≈ 0.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 1

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

5: Average symbolic conclusion length is 47/2 ≈ 23.50. (Median: 23.50)
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there is 1 minimal D-proof with a conclusion of odd symbolic length. [1/2 ≈ 50.00% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 1 22 0 23 0 24 0 25 0 26 1

7: Average symbolic conclusion length is 33/2 ≈ 16.50. (Median: 16.50)
   There is 1 minimal D-proof with a conclusion of even symbolic length, and there is 1 minimal D-proof with a conclusion of odd symbolic length. [1/2 ≈ 50.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 1 15 0 16 0 17 0 18 0 19 1

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

11: Average symbolic conclusion length is undefined (since there are no D-proofs of length 11).

13: Average symbolic conclusion length is 23/1 ≈ 23.00. (Median: 23)
    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

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

17: Average symbolic conclusion length is 91/3 ≈ 30.33. (Median: 33)
    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 1 10 0 11 0 12 0 13 0 14 0 15 0 16 0 17 0 18 0 19 0 20 0 21 0 22 0 23 0 24 0 25 0 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 1 34 0 35 0 36 0 37 0 38 0 39 0 40 0 41 0 42 0 43 0 44 0 45 0 46 0 47 0 48 0 49 1

19: Average symbolic conclusion length is 144/4 ≈ 36.00. (Median: 39.00)
    There are 2 minimal D-proofs with conclusions of even symbolic length, and there are 2 minimal D-proofs with conclusions of odd symbolic length. [2/4 ≈ 50.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 1 20 0 21 0 22 0 23 0 24 0 25 0 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 0 37 0 38 1 39 0 40 1 41 0 42 0 43 0 44 0 45 0 46 0 47 1

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

23: Average symbolic conclusion length is 162/5 ≈ 32.40. (Median: 37)
    There are 3 minimal D-proofs with conclusions of even symbolic length, and there are 2 minimal D-proofs with conclusions of odd symbolic length. [3/5 ≈ 60.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 1 23 0 24 1 25 0 26 0 27 0 28 0 29 0 30 0 31 0 32 0 33 0 34 0 35 0 36 0 37 2 38 0 39 0 40 0 41 0 42 1

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

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

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

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

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

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

37: Average symbolic conclusion length is 1159/30 ≈ 38.63. (Median: 37)
    There are 17 minimal D-proofs with conclusions of even symbolic length, and there are 13 minimal D-proofs with conclusions of odd symbolic length. [17/30 ≈ 56.67% 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 1 19 0 20 0 21 2 22 0 23 0 24 0 25 1 26 1 27 0 28 1 29 0 30 4 31 0 32 1 33 1 34 0 35 2 36 0 37 2 38 0 39 1 40 0 41 0 42 3 43 1 44 0 45 0 46 1 47 0 48 0 49 2 50 1 51 0 52 0 53 0 54 1 55 0 56 1 57 0 58 2 59 0 60 0 61 0 62 0 63 1

39: Average symbolic conclusion length is 1475/37 ≈ 39.86. (Median: 40)
    There are 16 minimal D-proofs with conclusions of even symbolic length, and there are 21 minimal D-proofs with conclusions of odd symbolic length. [16/37 ≈ 43.24% 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 1 20 0 21 1 22 0 23 4 24 0 25 0 26 1 27 0 28 2 29 0 30 1 31 0 32 0 33 1 34 0 35 2 36 1 37 1 38 0 39 2 40 4 41 0 42 2 43 1 44 1 45 0 46 0 47 2 48 0 49 2 50 0 51 1 52 1 53 1 54 1 55 0 56 1 57 0 58 0 59 0 60 1 61 0 62 0 63 1 64 0 65 1

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

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

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

47: Average symbolic conclusion length is 3712/85 ≈ 43.67. (Median: 42)
    There are 43 minimal D-proofs with conclusions of even symbolic length, and there are 42 minimal D-proofs with conclusions of odd symbolic length. [43/85 ≈ 50.59% 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 1 17 0 18 0 19 3 20 1 21 1 22 2 23 1 24 3 25 3 26 2 27 1 28 2 29 1 30 2 31 4 32 1 33 0 34 3 35 1 36 2 37 5 38 0 39 0 40 0 41 3 42 1 43 1 44 5 45 1 46 0 47 0 48 1 49 7 50 1 51 2 52 0 53 2 54 1 55 3 56 3 57 0 58 2 59 0 60 2 61 1 62 1 63 0 64 0 65 0 66 0 67 0 68 0 69 0 70 0 71 0 72 1 73 0 74 1 75 0 76 0 77 0 78 0 79 0 80 1 81 0 82 2 83 0 84 1 85 0 86 0 87 0 88 0 89 2 90 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

77: Average symbolic conclusion length is 191894/2986 ≈ 64.26. (Median: 60)
    There are 1496 minimal D-proofs with conclusions of even symbolic length, and there are 1490 minimal D-proofs with conclusions of odd symbolic length. [1496/2986 ≈ 50.10% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 1 10 0 11 0 12 1 13 0 14 1 15 1 16 1 17 2 18 6 19 0 20 3 21 4 22 5 23 8 24 7 25 11 26 13 27 8 28 7 29 12 30 16 31 20 32 21 33 29 34 13 35 42 36 24 37 38 38 42 39 38 40 33 41 35 42 52 43 47 44 63 45 44 46 42 47 49 48 69 49 71 50 48 51 69 52 42 53 52 54 66 55 78 56 84 57 54 58 47 59 47 60 74 61 69 62 57 63 47 64 50 65 57 66 29 67 56 68 60 69 59 70 54 71 22 72 47 73 34 74 36 75 26 76 45 77 34 78 29 79 39 80 23 81 31 82 26 83 24 84 25 85 30 86 12 87 11 88 28 89 22 90 22 91 9 92 9 93 7 94 16 95 20 96 12 97 6 98 9 99 7 100 13 101 11 102 16 103 7 104 8 105 4 106 1 107 13 108 5 109 9 110 9 111 6 112 3 113 3 114 6 115 5 116 1 117 8 118 5 119 1 120 1 121 4 122 3 123 1 124 2 125 1 126 0 127 4 128 3 129 0 130 1 131 0 132 6 133 2 134 5 135 2 136 0 137 0 138 1 139 6 140 2 141 2 142 3 143 3 144 1 145 1 146 3 147 5 148 2 149 4 150 0 151 0 152 3 153 1 154 0 155 0 156 1 157 0 158 1 159 1 160 3 161 0 162 0 163 1 164 3 165 1 166 1 167 3 168 2 169 0 170 2 171 2 172 1 173 0 174 1 175 0 176 2 177 3 178 0 179 1 180 0 181 0 182 0 183 2 184 1 185 0 186 1 187 0 188 0 189 0 190 0 191 0 192 0 193 0 194 1 195 0 196 0 197 0 198 0 199 0 200 0 201 1 202 0 203 0 204 0 205 0 206 0 207 0 208 1 209 0 210 0 211 0 212 0 213 0 214 0 215 2 216 0 217 0 218 0 219 0 220 0 221 0 222 1 223 0 224 0 225 0 226 0 227 0 228 0 229 0 230 0 231 0 232 0 233 0 234 0 235 0 236 0 237 0 238 0 239 0 240 0 241 0 242 0 243 0 244 0 245 0 246 0 247 0 248 0 249 0 250 0 251 0 252 0 253 0 254 0 255 0 256 0 257 0 258 0 259 0 260 0 261 0 262 0 263 0 264 0 265 0 266 0 267 0 268 0 269 0 270 0 271 0 272 0 273 0 274 0 275 0 276 0 277 0 278 0 279 0 280 0 281 0 282 0 283 0 284 0 285 0 286 0 287 0 288 0 289 0 290 0 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 0 301 0 302 1

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

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

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

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

87: Average symbolic conclusion length is 727687/10182 ≈ 71.47. (Median: 66)
    There are 5085 minimal D-proofs with conclusions of even symbolic length, and there are 5097 minimal D-proofs with conclusions of odd symbolic length. [5085/10182 ≈ 49.94% even]
1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 0 10 0 11 1 12 0 13 1 14 0 15 1 16 0 17 2 18 7 19 3 20 5 21 6 22 8 23 15 24 13 25 17 26 18 27 21 28 30 29 24 30 41 31 41 32 62 33 70 34 49 35 68 36 68 37 88 38 79 39 113 40 81 41 82 42 128 43 117 44 167 45 110 46 168 47 112 48 114 49 168 50 138 51 224 52 148 53 184 54 154 55 188 56 183 57 172 58 225 59 210 60 189 61 164 62 190 63 193 64 149 65 173 66 156 67 207 68 140 69 146 70 179 71 157 72 165 73 143 74 173 75 126 76 126 77 147 78 128 79 163 80 115 81 126 82 104 83 118 84 121 85 122 86 93 87 81 88 87 89 64 90 92 91 75 92 72 93 61 94 87 95 63 96 57 97 41 98 60 99 61 100 44 101 51 102 53 103 51 104 40 105 38 106 52 107 32 108 42 109 25 110 27 111 36 112 22 113 34 114 27 115 31 116 39 117 24 118 31 119 19 120 30 121 12 122 18 123 20 124 19 125 13 126 14 127 21 128 15 129 9 130 27 131 15 132 17 133 7 134 18 135 8 136 15 137 11 138 9 139 12 140 10 141 14 142 7 143 11 144 8 145 7 146 14 147 3 148 6 149 2 150 9 151 15 152 8 153 8 154 5 155 9 156 2 157 3 158 7 159 6 160 7 161 5 162 8 163 3 164 2 165 7 166 6 167 5 168 5 169 4 170 1 171 2 172 2 173 1 174 1 175 3 176 1 177 2 178 3 179 2 180 2 181 8 182 2 183 4 184 0 185 1 186 3 187 0 188 3 189 1 190 1 191 1 192 1 193 4 194 1 195 3 196 1 197 1 198 1 199 1 200 1 201 2 202 2 203 1 204 2 205 1 206 1 207 1 208 0 209 0 210 2 211 0 212 3 213 0 214 3 215 0 216 0 217 1 218 2 219 1 220 0 221 1 222 0 223 0 224 0 225 0 226 0 227 0 228 0 229 2 230 1 231 0 232 0 233 1 234 0 235 0 236 0 237 1 238 0 239 1 240 1 241 0 242 1 243 0 244 0 245 0 246 0 247 0 248 0 249 0 250 0 251 0 252 0 253 0 254 1 255 0 256 0 257 0 258 0 259 0 260 0 261 1 262 0 263 1 264 0 265 1 266 0 267 0 268 0 269 0 270 0 271 1 272 0 273 0 274 0 275 1 276 0 277 0 278 1 279 0 280 0 281 0 282 1 283 0 284 0 285 0 286 1 287 0 288 0 289 1 290 0 291 0 292 1 293 0 294 0 295 0 296 1 297 0 298 0 299 2 300 0 301 0 302 0 303 0 304 0 305 0 306 1 307 0 308 0 309 0 310 0 311 0 312 0 313 2 314 0 315 0 316 0 317 0 318 1 319 0 320 2

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

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

93: Average symbolic conclusion length is 1506661/19614 ≈ 76.82. (Median: 70)
    There are 9891 minimal D-proofs with conclusions of even symbolic length, and there are 9723 minimal D-proofs with conclusions of odd symbolic length. [9891/19614 ≈ 50.43% even]
1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 0 10 0 11 0 12 1 13 0 14 1 15 2 16 2 17 8 18 6 19 4 20 5 21 17 22 11 23 11 24 19 25 24 26 31 27 42 28 40 29 44 30 43 31 57 32 63 33 77 34 81 35 124 36 92 37 82 38 147 39 125 40 148 41 165 42 190 43 169 44 190 45 203 46 222 47 278 48 244 49 232 50 316 51 275 52 223 53 362 54 297 55 312 56 262 57 305 58 362 59 361 60 379 61 320 62 390 63 319 64 323 65 373 66 383 67 337 68 227 69 299 70 272 71 423 72 397 73 314 74 268 75 197 76 255 77 236 78 326 79 279 80 262 81 231 82 187 83 237 84 238 85 211 86 220 87 186 88 179 89 156 90 220 91 135 92 179 93 187 94 93 95 159 96 137 97 128 98 128 99 132 100 124 101 81 102 136 103 82 104 113 105 73 106 103 107 91 108 78 109 85 110 60 111 86 112 66 113 90 114 62 115 57 116 62 117 47 118 74 119 47 120 61 121 40 122 54 123 33 124 55 125 56 126 35 127 46 128 29 129 35 130 50 131 30 132 27 133 23 134 49 135 27 136 26 137 30 138 20 139 26 140 23 141 32 142 31 143 12 144 31 145 22 146 29 147 26 148 25 149 23 150 20 151 30 152 22 153 17 154 27 155 25 156 16 157 17 158 17 159 16 160 11 161 16 162 12 163 10 164 11 165 14 166 22 167 13 168 9 169 17 170 14 171 13 172 13 173 7 174 11 175 8 176 9 177 9 178 10 179 9 180 12 181 13 182 10 183 8 184 8 185 7 186 9 187 11 188 12 189 7 190 5 191 6 192 1 193 6 194 1 195 7 196 6 197 3 198 6 199 2 200 7 201 8 202 8 203 6 204 4 205 6 206 7 207 7 208 7 209 2 210 5 211 3 212 3 213 3 214 5 215 4 216 4 217 2 218 6 219 2 220 3 221 2 222 4 223 3 224 2 225 2 226 2 227 2 228 1 229 5 230 5 231 2 232 3 233 0 234 1 235 2 236 5 237 1 238 2 239 2 240 0 241 2 242 1 243 3 244 0 245 2 246 1 247 0 248 1 249 0 250 5 251 0 252 2 253 0 254 1 255 2 256 1 257 2 258 0 259 2 260 1 261 1 262 2 263 2 264 2 265 0 266 1 267 0 268 0 269 0 270 2 271 1 272 0 273 1 274 0 275 0 276 1 277 2 278 1 279 0 280 1 281 0 282 0 283 0 284 0 285 4 286 1 287 0 288 0 289 0 290 0 291 0 292 3 293 0 294 0 295 0 296 0 297 0 298 1 299 1 300 0 301 0 302 0 303 0 304 1 305 0 306 0 307 0 308 1 309 0 310 0 311 1 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 1 344 0 345 0 346 0 347 1 348 0 349 0 350 0 351 0 352 0 353 0 354 1 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

95: Average symbolic conclusion length is 1965533/25087 ≈ 78.35. (Median: 71)
    There are 12736 minimal D-proofs with conclusions of even symbolic length, and there are 12351 minimal D-proofs with conclusions of odd symbolic length. [12736/25087 ≈ 50.77% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 2 11 1 12 0 13 1 14 4 15 1 16 3 17 3 18 3 19 9 20 23 21 10 22 19 23 13 24 33 25 28 26 49 27 44 28 58 29 55 30 60 31 81 32 74 33 105 34 98 35 103 36 125 37 160 38 138 39 152 40 220 41 183 42 173 43 232 44 236 45 216 46 290 47 251 48 303 49 269 50 299 51 382 52 336 53 405 54 370 55 423 56 349 57 374 58 507 59 430 60 456 61 312 62 369 63 332 64 565 65 526 66 389 67 380 68 315 69 355 70 412 71 487 72 482 73 372 74 364 75 315 76 469 77 405 78 370 79 350 80 301 81 316 82 276 83 321 84 265 85 311 86 303 87 145 88 285 89 222 90 203 91 204 92 203 93 196 94 173 95 230 96 148 97 197 98 156 99 160 100 167 101 147 102 131 103 90 104 144 105 139 106 152 107 119 108 107 109 108 110 103 111 128 112 93 113 84 114 90 115 79 116 85 117 76 118 83 119 58 120 78 121 57 122 53 123 93 124 43 125 56 126 61 127 67 128 58 129 52 130 60 131 38 132 42 133 50 134 61 135 38 136 41 137 63 138 32 139 45 140 34 141 41 142 38 143 33 144 42 145 34 146 33 147 43 148 34 149 37 150 32 151 22 152 25 153 22 154 25 155 25 156 32 157 15 158 22 159 30 160 14 161 18 162 28 163 21 164 30 165 23 166 15 167 19 168 12 169 16 170 17 171 21 172 22 173 16 174 23 175 9 176 13 177 7 178 7 179 14 180 20 181 14 182 12 183 14 184 11 185 5 186 11 187 8 188 11 189 10 190 14 191 10 192 10 193 12 194 7 195 10 196 10 197 8 198 9 199 13 200 12 201 7 202 9 203 7 204 6 205 3 206 7 207 9 208 10 209 5 210 10 211 7 212 8 213 4 214 7 215 7 216 4 217 4 218 7 219 4 220 5 221 5 222 3 223 2 224 6 225 3 226 2 227 3 228 6 229 3 230 2 231 6 232 5 233 1 234 5 235 2 236 2 237 2 238 4 239 2 240 4 241 2 242 1 243 3 244 1 245 2 246 2 247 2 248 4 249 2 250 2 251 0 252 2 253 0 254 1 255 2 256 4 257 2 258 2 259 1 260 1 261 0 262 0 263 2 264 0 265 0 266 1 267 2 268 2 269 0 270 1 271 3 272 1 273 1 274 0 275 0 276 0 277 1 278 4 279 3 280 0 281 0 282 0 283 1 284 1 285 2 286 1 287 0 288 0 289 0 290 1 291 0 292 1 293 0 294 0 295 0 296 0 297 3 298 0 299 0 300 0 301 0 302 0 303 1 304 1 305 0 306 0 307 0 308 0 309 0 310 0 311 0 312 1 313 0 314 1 315 0 316 0 317 0 318 0 319 0 320 0 321 1 322 0 323 0 324 0 325 0 326 0 327 1 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 0 336 0 337 0 338 1 339 0 340 0 341 0 342 0 343 0 344 0 345 1 346 0 347 0 348 0 349 0 350 0 351 1 352 0 353 0 354 0 355 0 356 0 357 0 358 0 359 0 360 0 361 1 362 0 363 1 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 1 397 0 398 0 399 0 400 0

97: Average symbolic conclusion length is 2598282/32452 ≈ 80.07. (Median: 72)
    There are 16102 minimal D-proofs with conclusions of even symbolic length, and there are 16350 minimal D-proofs with conclusions of odd symbolic length. [16102/32452 ≈ 49.62% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 0 13 4 14 1 15 3 16 3 17 6 18 6 19 17 20 7 21 17 22 8 23 25 24 26 25 36 26 56 27 44 28 49 29 62 30 105 31 77 32 85 33 121 34 111 35 126 36 130 37 185 38 159 39 197 40 179 41 241 42 248 43 214 44 300 45 289 46 361 47 362 48 373 49 329 50 358 51 490 52 450 53 484 54 446 55 414 56 467 57 568 58 576 59 443 60 500 61 500 62 494 63 548 64 631 65 643 66 490 67 498 68 492 69 601 70 576 71 537 72 524 73 452 74 473 75 482 76 488 77 489 78 503 79 467 80 300 81 473 82 352 83 360 84 309 85 369 86 347 87 331 88 381 89 234 90 324 91 278 92 301 93 318 94 277 95 265 96 168 97 230 98 200 99 260 100 204 101 195 102 200 103 187 104 196 105 177 106 156 107 148 108 170 109 188 110 155 111 167 112 132 113 114 114 111 115 98 116 145 117 99 118 104 119 129 120 104 121 103 122 88 123 102 124 71 125 82 126 107 127 91 128 92 129 97 130 91 131 65 132 80 133 64 134 68 135 69 136 61 137 56 138 53 139 51 140 63 141 59 142 69 143 56 144 50 145 45 146 33 147 37 148 62 149 41 150 60 151 48 152 51 153 26 154 21 155 36 156 32 157 39 158 38 159 41 160 36 161 32 162 32 163 24 164 32 165 25 166 16 167 33 168 23 169 16 170 18 171 21 172 19 173 16 174 20 175 15 176 33 177 16 178 17 179 24 180 8 181 17 182 18 183 23 184 16 185 21 186 17 187 16 188 24 189 21 190 11 191 15 192 18 193 8 194 13 195 13 196 12 197 11 198 15 199 10 200 13 201 14 202 7 203 14 204 16 205 10 206 9 207 9 208 7 209 3 210 13 211 5 212 11 213 6 214 8 215 5 216 7 217 8 218 8 219 7 220 2 221 6 222 1 223 0 224 11 225 3 226 5 227 5 228 3 229 3 230 5 231 6 232 3 233 5 234 3 235 5 236 4 237 3 238 2 239 1 240 5 241 4 242 3 243 5 244 3 245 1 246 1 247 2 248 2 249 2 250 3 251 4 252 2 253 3 254 1 255 1 256 2 257 1 258 3 259 1 260 0 261 2 262 0 263 0 264 3 265 3 266 0 267 1 268 1 269 0 270 1 271 3 272 3 273 1 274 2 275 2 276 2 277 0 278 2 279 4 280 0 281 0 282 2 283 1 284 1 285 2 286 1 287 0 288 0 289 0 290 3 291 0 292 0 293 0 294 0 295 0 296 0 297 0 298 0 299 0 300 1 301 0 302 0 303 0 304 1 305 1 306 1 307 0 308 0 309 0 310 1 311 0 312 1 313 0 314 1 315 0 316 0 317 0 318 0 319 1 320 0 321 0 322 0 323 1 324 1 325 0 326 0 327 0 328 1 329 2 330 1 331 1 332 0 333 0 334 1 335 0 336 0 337 0 338 1 339 1 340 0 341 0 342 1 343 0 344 0 345 0 346 0 347 0 348 0 349 0 350 0 351 0 352 0 353 0 354 0 355 1 356 0 357 0 358 1 359 0 360 0 361 0 362 0 363 0 364 0 365 1 366 0 367 0 368 1 369 0 370 1 371 0 372 0 373 0 374 0 375 1 376 1 377 0 378 0 379 0 380 0 381 0 382 0 383 0 384 0 385 0 386 0 387 1 388 0 389 0 390 1 391 0 392 0 393 0 394 0 395 0 396 0 397 0 398 0 399 0 400 0

99: Average symbolic conclusion length is 3416169/41840 ≈ 81.65. (Median: 74)
    There are 20961 minimal D-proofs with conclusions of even symbolic length, and there are 20879 minimal D-proofs with conclusions of odd symbolic length. [20961/41840 ≈ 50.10% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 1 12 1 13 0 14 3 15 1 16 2 17 1 18 8 19 10 20 10 21 15 22 12 23 48 24 34 25 41 26 40 27 49 28 57 29 45 30 93 31 83 32 112 33 111 34 137 35 175 36 124 37 169 38 210 39 281 40 281 41 235 42 291 43 300 44 364 45 382 46 425 47 433 48 405 49 512 50 509 51 555 52 487 53 529 54 578 55 567 56 607 57 680 58 690 59 654 60 598 61 664 62 723 63 737 64 624 65 644 66 593 67 650 68 711 69 703 70 671 71 726 72 630 73 486 74 717 75 667 76 614 77 479 78 567 79 588 80 562 81 608 82 434 83 532 84 443 85 460 86 494 87 482 88 450 89 341 90 405 91 328 92 457 93 318 94 327 95 338 96 307 97 351 98 298 99 310 100 268 101 295 102 321 103 275 104 288 105 231 106 234 107 244 108 222 109 268 110 193 111 195 112 225 113 159 114 174 115 183 116 175 117 132 118 175 119 169 120 144 121 150 122 174 123 148 124 128 125 119 126 118 127 118 128 133 129 117 130 91 131 105 132 89 133 105 134 117 135 88 136 109 137 83 138 62 139 71 140 73 141 91 142 69 143 107 144 80 145 71 146 61 147 57 148 55 149 53 150 71 151 40 152 53 153 58 154 56 155 54 156 57 157 58 158 31 159 34 160 46 161 37 162 54 163 33 164 32 165 29 166 27 167 25 168 24 169 44 170 34 171 38 172 24 173 21 174 39 175 31 176 27 177 29 178 23 179 22 180 18 181 34 182 23 183 18 184 23 185 15 186 16 187 23 188 22 189 14 190 23 191 19 192 17 193 17 194 22 195 15 196 26 197 10 198 16 199 10 200 12 201 7 202 13 203 16 204 17 205 15 206 10 207 8 208 8 209 6 210 18 211 9 212 12 213 5 214 7 215 3 216 6 217 13 218 4 219 12 220 5 221 2 222 13 223 7 224 7 225 5 226 15 227 4 228 3 229 10 230 7 231 5 232 2 233 6 234 5 235 2 236 7 237 8 238 5 239 3 240 3 241 0 242 2 243 8 244 6 245 3 246 4 247 1 248 2 249 0 250 7 251 6 252 1 253 0 254 2 255 1 256 2 257 4 258 5 259 2 260 2 261 2 262 2 263 2 264 3 265 3 266 1 267 0 268 2 269 1 270 2 271 2 272 3 273 1 274 2 275 1 276 1 277 2 278 3 279 1 280 1 281 2 282 0 283 1 284 1 285 0 286 4 287 1 288 1 289 1 290 0 291 1 292 2 293 1 294 0 295 0 296 1 297 1 298 1 299 0 300 1 301 1 302 0 303 1 304 0 305 2 306 0 307 2 308 1 309 1 310 1 311 1 312 0 313 1 314 0 315 1 316 0 317 3 318 2 319 0 320 0 321 1 322 2 323 1 324 0 325 0 326 1 327 1 328 0 329 0 330 0 331 0 332 0 333 0 334 0 335 1 336 2 337 1 338 1 339 0 340 0 341 2 342 1 343 0 344 1 345 2 346 2 347 0 348 2 349 1 350 0 351 0 352 0 353 0 354 1 355 0 356 0 357 0 358 2 359 1 360 0 361 0 362 1 363 1 364 0 365 1 366 2 367 0 368 0 369 2 370 0 371 0 372 0 373 0 374 1 375 0 376 1 377 1 378 0 379 0 380 0 381 0 382 2 383 1 384 0 385 0 386 0 387 0 388 0 389 0 390 0 391 0 392 0 393 0 394 1 395 1 396 0 397 0 398 0 399 0 400 0

101: Average symbolic conclusion length is 4450415/53343 ≈ 83.43. (Median: 76)
     There are 27138 minimal D-proofs with conclusions of even symbolic length, and there are 26205 minimal D-proofs with conclusions of odd symbolic length. [27138/53343 ≈ 50.87% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 0 13 3 14 2 15 0 16 12 17 4 18 15 19 3 20 6 21 9 22 9 23 22 24 24 25 43 26 30 27 46 28 76 29 64 30 57 31 109 32 155 33 141 34 139 35 188 36 180 37 222 38 265 39 277 40 317 41 292 42 373 43 368 44 434 45 429 46 424 47 531 48 523 49 544 50 591 51 615 52 652 53 659 54 731 55 755 56 767 57 652 58 728 59 705 60 836 61 846 62 936 63 794 64 903 65 740 66 709 67 926 68 979 69 865 70 763 71 800 72 824 73 743 74 899 75 740 76 859 77 707 78 746 79 733 80 742 81 729 82 626 83 697 84 542 85 712 86 598 87 557 88 581 89 503 90 581 91 462 92 575 93 488 94 478 95 463 96 438 97 499 98 422 99 399 100 400 101 380 102 439 103 335 104 331 105 353 106 341 107 314 108 365 109 336 110 206 111 281 112 238 113 242 114 257 115 283 116 250 117 233 118 210 119 168 120 196 121 194 122 239 123 179 124 189 125 171 126 157 127 170 128 129 129 169 130 125 131 114 132 137 133 122 134 141 135 113 136 147 137 130 138 113 139 108 140 114 141 102 142 102 143 88 144 70 145 73 146 91 147 98 148 123 149 77 150 80 151 54 152 57 153 81 154 70 155 84 156 67 157 72 158 50 159 42 160 63 161 45 162 60 163 54 164 54 165 28 166 41 167 37 168 49 169 38 170 44 171 37 172 38 173 47 174 46 175 30 176 41 177 32 178 32 179 18 180 37 181 26 182 26 183 33 184 41 185 21 186 22 187 22 188 31 189 31 190 33 191 21 192 32 193 17 194 21 195 18 196 32 197 22 198 30 199 21 200 13 201 19 202 18 203 21 204 18 205 16 206 11 207 8 208 18 209 14 210 19 211 9 212 19 213 9 214 9 215 21 216 12 217 9 218 8 219 17 220 5 221 7 222 22 223 12 224 7 225 7 226 6 227 2 228 11 229 12 230 8 231 6 232 4 233 3 234 4 235 4 236 11 237 7 238 9 239 5 240 3 241 5 242 5 243 7 244 10 245 5 246 4 247 2 248 3 249 5 250 6 251 5 252 1 253 1 254 2 255 6 256 3 257 6 258 5 259 3 260 0 261 3 262 3 263 4 264 5 265 4 266 5 267 0 268 3 269 1 270 2 271 3 272 3 273 2 274 2 275 1 276 3 277 1 278 1 279 2 280 1 281 3 282 2 283 0 284 3 285 0 286 1 287 3 288 0 289 3 290 1 291 1 292 2 293 5 294 1 295 0 296 2 297 2 298 0 299 3 300 2 301 3 302 1 303 5 304 2 305 0 306 0 307 0 308 3 309 1 310 5 311 0 312 0 313 3 314 1 315 2 316 2 317 1 318 2 319 0 320 3 321 1 322 1 323 0 324 4 325 2 326 4 327 1 328 2 329 2 330 4 331 2 332 4 333 3 334 2 335 2 336 0 337 1 338 0 339 3 340 1 341 2 342 0 343 0 344 1 345 1 346 0 347 2 348 1 349 0 350 1 351 3 352 3 353 1 354 0 355 2 356 2 357 0 358 0 359 1 360 1 361 0 362 3 363 1 364 0 365 1 366 1 367 3 368 2 369 1 370 0 371 0 372 0 373 1 374 0 375 4 376 1 377 0 378 0 379 0 380 0 381 1 382 0 383 0 384 0 385 0 386 1 387 0 388 1 389 1 390 1 391 0 392 0 393 0 394 0 395 0 396 0 397 2 398 1 399 0 400 1

103: Average symbolic conclusion length is 5733375/67105 ≈ 85.44. (Median: 77)
     There are 33256 minimal D-proofs with conclusions of even symbolic length, and there are 33849 minimal D-proofs with conclusions of odd symbolic length. [33256/67105 ≈ 49.56% 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 0 14 0 15 1 16 0 17 3 18 10 19 6 20 10 21 18 22 17 23 18 24 32 25 32 26 38 27 62 28 63 29 78 30 101 31 116 32 115 33 161 34 156 35 187 36 208 37 264 38 251 39 254 40 335 41 368 42 415 43 408 44 448 45 502 46 551 47 592 48 676 49 633 50 544 51 693 52 712 53 846 54 821 55 967 56 866 57 923 58 850 59 789 60 1074 61 1081 62 1052 63 961 64 978 65 1062 66 1004 67 1225 68 1036 69 1207 70 893 71 983 72 1068 73 1087 74 1080 75 1005 76 1016 77 845 78 1062 79 967 80 824 81 965 82 906 83 897 84 688 85 967 86 780 87 793 88 743 89 717 90 796 91 605 92 618 93 653 94 585 95 722 96 562 97 586 98 506 99 508 100 489 101 573 102 539 103 384 104 521 105 429 106 440 107 397 108 390 109 395 110 302 111 324 112 286 113 363 114 306 115 349 116 321 117 274 118 322 119 232 120 281 121 257 122 275 123 219 124 195 125 201 126 219 127 203 128 224 129 196 130 219 131 177 132 186 133 184 134 188 135 168 136 142 137 131 138 148 139 149 140 170 141 165 142 127 143 103 144 119 145 107 146 113 147 120 148 135 149 97 150 109 151 78 152 96 153 96 154 99 155 89 156 101 157 82 158 61 159 69 160 74 161 73 162 87 163 68 164 92 165 45 166 77 167 54 168 66 169 68 170 70 171 65 172 33 173 56 174 61 175 43 176 50 177 51 178 57 179 35 180 49 181 35 182 53 183 42 184 39 185 55 186 30 187 41 188 32 189 41 190 50 191 40 192 29 193 32 194 39 195 31 196 26 197 34 198 33 199 21 200 28 201 46 202 22 203 31 204 24 205 34 206 25 207 21 208 37 209 15 210 18 211 13 212 21 213 8 214 17 215 30 216 26 217 15 218 13 219 10 220 19 221 16 222 22 223 15 224 13 225 2 226 7 227 13 228 11 229 13 230 8 231 9 232 9 233 5 234 11 235 11 236 15 237 12 238 10 239 5 240 4 241 5 242 6 243 9 244 9 245 7 246 0 247 5 248 9 249 2 250 7 251 8 252 9 253 3 254 7 255 5 256 2 257 8 258 2 259 5 260 4 261 8 262 5 263 2 264 5 265 4 266 4 267 1 268 4 269 2 270 5 271 2 272 5 273 5 274 0 275 6 276 2 277 3 278 2 279 7 280 3 281 2 282 10 283 3 284 4 285 5 286 4 287 2 288 3 289 1 290 3 291 6 292 2 293 1 294 5 295 2 296 3 297 2 298 2 299 2 300 1 301 6 302 5 303 7 304 6 305 0 306 2 307 2 308 3 309 1 310 4 311 7 312 3 313 2 314 1 315 3 316 2 317 3 318 4 319 8 320 3 321 2 322 4 323 9 324 2 325 4 326 1 327 2 328 4 329 0 330 1 331 2 332 3 333 2 334 3 335 2 336 2 337 1 338 1 339 1 340 4 341 2 342 2 343 3 344 4 345 0 346 1 347 1 348 3 349 1 350 0 351 1 352 3 353 3 354 4 355 2 356 1 357 1 358 1 359 4 360 3 361 3 362 1 363 0 364 1 365 0 366 0 367 1 368 3 369 0 370 2 371 0 372 2 373 0 374 1 375 1 376 1 377 0 378 0 379 1 380 2 381 1 382 1 383 2 384 1 385 0 386 1 387 1 388 0 389 0 390 2 391 2 392 1 393 1 394 1 395 0 396 0 397 1 398 0 399 1 400 1

105: Average symbolic conclusion length is 7362524/84222 ≈ 87.42. (Median: 78)
     There are 42642 minimal D-proofs with conclusions of even symbolic length, and there are 41580 minimal D-proofs with conclusions of odd symbolic length. [42642/84222 ≈ 50.63% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 1 12 0 13 1 14 2 15 3 16 3 17 5 18 0 19 4 20 16 21 12 22 22 23 22 24 34 25 38 26 49 27 64 28 77 29 87 30 94 31 98 32 121 33 149 34 177 35 246 36 194 37 246 38 291 39 340 40 350 41 447 42 401 43 376 44 508 45 524 46 663 47 622 48 786 49 761 50 753 51 844 52 780 53 1083 54 960 55 1024 56 946 57 1016 58 1212 59 1149 60 1378 61 1197 62 1388 63 1067 64 1130 65 1383 66 1323 67 1496 68 1330 69 1351 70 1186 71 1336 72 1376 73 1244 74 1473 75 1386 76 1291 77 1057 78 1307 79 1165 80 1120 81 1127 82 1092 83 1198 84 935 85 1008 86 1077 87 943 88 1051 89 879 90 968 91 749 92 834 93 835 94 873 95 885 96 665 97 769 98 656 99 676 100 719 101 639 102 645 103 493 104 589 105 449 106 598 107 513 108 482 109 515 110 425 111 510 112 418 113 422 114 469 115 416 116 393 117 295 118 345 119 378 120 402 121 331 122 343 123 334 124 290 125 223 126 330 127 259 128 292 129 249 130 263 131 260 132 247 133 249 134 254 135 222 136 192 137 181 138 224 139 171 140 203 141 178 142 181 143 168 144 137 145 161 146 175 147 154 148 145 149 152 150 171 151 112 152 147 153 117 154 115 155 156 156 116 157 128 158 97 159 120 160 94 161 83 162 125 163 96 164 93 165 68 166 104 167 89 168 97 169 73 170 79 171 97 172 60 173 73 174 66 175 81 176 78 177 63 178 99 179 60 180 69 181 59 182 69 183 76 184 61 185 62 186 70 187 63 188 56 189 57 190 43 191 55 192 58 193 41 194 73 195 40 196 55 197 44 198 49 199 50 200 41 201 41 202 44 203 29 204 32 205 35 206 33 207 33 208 46 209 44 210 26 211 15 212 29 213 38 214 26 215 38 216 19 217 16 218 15 219 14 220 23 221 12 222 24 223 16 224 22 225 13 226 18 227 20 228 15 229 15 230 20 231 13 232 8 233 14 234 21 235 9 236 16 237 12 238 11 239 7 240 10 241 13 242 10 243 11 244 8 245 15 246 8 247 15 248 8 249 11 250 9 251 9 252 11 253 4 254 12 255 8 256 2 257 5 258 6 259 7 260 4 261 8 262 6 263 10 264 7 265 5 266 9 267 8 268 9 269 7 270 8 271 3 272 9 273 9 274 5 275 8 276 5 277 6 278 4 279 6 280 4 281 4 282 7 283 5 284 7 285 2 286 5 287 8 288 4 289 8 290 10 291 9 292 4 293 2 294 6 295 9 296 5 297 6 298 3 299 1 300 4 301 3 302 3 303 4 304 8 305 3 306 6 307 2 308 5 309 4 310 8 311 6 312 12 313 3 314 5 315 7 316 8 317 3 318 3 319 2 320 3 321 4 322 3 323 3 324 3 325 1 326 2 327 5 328 2 329 4 330 5 331 2 332 1 333 3 334 3 335 3 336 4 337 3 338 4 339 3 340 3 341 3 342 2 343 1 344 2 345 4 346 3 347 5 348 3 349 2 350 4 351 3 352 2 353 2 354 3 355 0 356 2 357 3 358 1 359 1 360 1 361 3 362 1 363 5 364 0 365 1 366 1 367 1 368 0 369 1 370 2 371 2 372 1 373 1 374 1 375 0 376 2 377 2 378 3 379 1 380 1 381 0 382 1 383 1 384 2 385 2 386 2 387 0 388 0 389 1 390 1 391 0 392 2 393 0 394 0 395 0 396 0 397 0 398 0 399 4 400 0

107: Average symbolic conclusion length is 9461810/105925 ≈ 89.33. (Median: 80)
     There are 53509 minimal D-proofs with conclusions of even symbolic length, and there are 52416 minimal D-proofs with conclusions of odd symbolic length. [53509/105925 ≈ 50.52% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 2 12 0 13 2 14 0 15 8 16 2 17 5 18 11 19 9 20 17 21 35 22 31 23 13 24 41 25 36 26 48 27 57 28 104 29 82 30 98 31 119 32 158 33 169 34 211 35 195 36 208 37 290 38 291 39 388 40 397 41 484 42 495 43 486 44 623 45 642 46 795 47 698 48 803 49 835 50 862 51 1067 52 1042 53 1214 54 1137 55 1271 56 1166 57 1152 58 1427 59 1359 60 1740 61 1387 62 1505 63 1436 64 1568 65 1724 66 1600 67 1816 68 1661 69 1585 70 1512 71 1641 72 1704 73 1549 74 1561 75 1530 76 1673 77 1379 78 1476 79 1622 80 1592 81 1514 82 1403 83 1491 84 1208 85 1254 86 1300 87 1265 88 1400 89 1105 90 1241 91 1051 92 1101 93 1171 94 1046 95 971 96 859 97 880 98 800 99 962 100 887 101 846 102 892 103 766 104 764 105 660 106 650 107 716 108 732 109 643 110 551 111 605 112 626 113 588 114 578 115 495 116 505 117 449 118 423 119 493 120 479 121 413 122 437 123 371 124 451 125 387 126 407 127 379 128 342 129 363 130 295 131 312 132 295 133 301 134 310 135 276 136 342 137 240 138 256 139 244 140 254 141 219 142 232 143 304 144 199 145 240 146 204 147 173 148 222 149 184 150 223 151 157 152 197 153 179 154 156 155 151 156 156 157 149 158 133 159 145 160 177 161 152 162 124 163 114 164 158 165 126 166 129 167 132 168 147 169 121 170 117 171 130 172 131 173 93 174 107 175 104 176 98 177 109 178 123 179 87 180 110 181 87 182 95 183 64 184 86 185 120 186 80 187 91 188 85 189 68 190 77 191 70 192 90 193 63 194 57 195 74 196 73 197 65 198 65 199 60 200 52 201 58 202 59 203 34 204 44 205 39 206 58 207 37 208 52 209 40 210 36 211 42 212 36 213 41 214 34 215 28 216 40 217 25 218 37 219 46 220 40 221 29 222 34 223 25 224 26 225 20 226 28 227 35 228 19 229 19 230 21 231 22 232 20 233 17 234 19 235 25 236 25 237 23 238 22 239 13 240 22 241 13 242 19 243 15 244 18 245 17 246 13 247 23 248 17 249 13 250 17 251 8 252 15 253 12 254 15 255 8 256 19 257 9 258 11 259 16 260 18 261 10 262 8 263 8 264 15 265 13 266 15 267 12 268 16 269 7 270 9 271 3 272 13 273 7 274 9 275 10 276 10 277 6 278 6 279 6 280 13 281 9 282 12 283 10 284 9 285 2 286 3 287 6 288 12 289 7 290 6 291 7 292 1 293 5 294 10 295 6 296 12 297 12 298 8 299 9 300 6 301 8 302 9 303 8 304 5 305 9 306 6 307 11 308 9 309 10 310 4 311 3 312 3 313 3 314 6 315 9 316 7 317 6 318 2 319 7 320 7 321 2 322 8 323 5 324 6 325 2 326 4 327 5 328 4 329 5 330 2 331 5 332 3 333 1 334 6 335 5 336 5 337 1 338 8 339 4 340 4 341 3 342 4 343 5 344 3 345 4 346 2 347 3 348 1 349 4 350 7 351 1 352 0 353 1 354 1 355 2 356 7 357 4 358 3 359 0 360 1 361 1 362 2 363 3 364 3 365 0 366 0 367 1 368 2 369 2 370 3 371 6 372 1 373 0 374 1 375 0 376 1 377 1 378 4 379 2 380 1 381 1 382 0 383 2 384 0 385 3 386 1 387 2 388 0 389 1 390 1 391 0 392 6 393 1 394 0 395 0 396 0 397 0 398 0 399 4 400 0

109: Average symbolic conclusion length is 12264629/134564 ≈ 91.14. (Median: 81)
     There are 67087 minimal D-proofs with conclusions of even symbolic length, and there are 67477 minimal D-proofs with conclusions of odd symbolic length. [67087/134564 ≈ 49.86% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 1 11 0 12 1 13 0 14 7 15 8 16 2 17 6 18 2 19 8 20 12 21 28 22 23 23 32 24 40 25 62 26 80 27 84 28 72 29 106 30 137 31 141 32 166 33 204 34 242 35 254 36 289 37 358 38 386 39 436 40 452 41 478 42 601 43 606 44 769 45 761 46 871 47 921 48 916 49 1009 50 1054 51 1230 52 1249 53 1494 54 1276 55 1373 56 1535 57 1573 58 1745 59 1689 60 1814 61 1776 62 1765 63 1901 64 1883 65 2114 66 1915 67 1947 68 1961 69 2109 70 1863 71 2036 72 2058 73 2224 74 2078 75 1949 76 2045 77 1842 78 1858 79 1797 80 1841 81 2114 82 1787 83 1899 84 1645 85 1688 86 1624 87 1597 88 1621 89 1563 90 1555 91 1373 92 1453 93 1347 94 1452 95 1480 96 1256 97 1235 98 1158 99 1157 100 1135 101 1218 102 988 103 961 104 968 105 939 106 918 107 906 108 848 109 776 110 763 111 679 112 728 113 757 114 687 115 740 116 651 117 660 118 670 119 550 120 628 121 543 122 626 123 450 124 507 125 509 126 465 127 505 128 484 129 588 130 408 131 396 132 468 133 337 134 395 135 342 136 483 137 322 138 368 139 335 140 266 141 340 142 296 143 342 144 323 145 300 146 311 147 253 148 259 149 263 150 270 151 214 152 269 153 255 154 259 155 193 156 223 157 248 158 221 159 179 160 226 161 194 162 183 163 183 164 235 165 187 166 163 167 174 168 169 169 143 170 161 171 203 172 133 173 143 174 153 175 119 176 154 177 137 178 150 179 126 180 152 181 138 182 110 183 143 184 105 185 122 186 112 187 102 188 115 189 102 190 116 191 120 192 104 193 94 194 101 195 85 196 52 197 97 198 84 199 79 200 83 201 60 202 66 203 70 204 92 205 67 206 62 207 86 208 63 209 60 210 67 211 70 212 68 213 64 214 42 215 48 216 59 217 35 218 52 219 64 220 59 221 34 222 47 223 36 224 43 225 44 226 56 227 38 228 50 229 38 230 41 231 36 232 34 233 35 234 31 235 35 236 32 237 24 238 27 239 30 240 38 241 21 242 33 243 27 244 21 245 22 246 29 247 26 248 22 249 24 250 20 251 19 252 32 253 24 254 23 255 10 256 18 257 12 258 23 259 27 260 17 261 18 262 14 263 18 264 15 265 15 266 23 267 15 268 18 269 10 270 11 271 16 272 12 273 16 274 14 275 15 276 6 277 11 278 7 279 14 280 12 281 13 282 14 283 9 284 9 285 9 286 10 287 16 288 8 289 18 290 11 291 7 292 11 293 11 294 18 295 9 296 17 297 9 298 11 299 7 300 20 301 9 302 11 303 12 304 11 305 11 306 9 307 10 308 16 309 5 310 9 311 2 312 5 313 8 314 5 315 12 316 7 317 9 318 3 319 4 320 7 321 14 322 11 323 3 324 13 325 4 326 4 327 10 328 9 329 6 330 4 331 9 332 2 333 4 334 7 335 4 336 6 337 1 338 5 339 2 340 1 341 3 342 5 343 8 344 2 345 3 346 2 347 5 348 9 349 2 350 7 351 2 352 1 353 0 354 1 355 3 356 6 357 7 358 2 359 2 360 4 361 2 362 2 363 5 364 7 365 3 366 4 367 1 368 0 369 3 370 2 371 4 372 3 373 1 374 0 375 0 376 5 377 0 378 6 379 3 380 2 381 0 382 0 383 0 384 1 385 6 386 0 387 1 388 1 389 0 390 3 391 0 392 5 393 0 394 1 395 0 396 0 397 1 398 0 399 4 400 1

111: Average symbolic conclusion length is 16010891/172053 ≈ 93.06. (Median: 83)
     There are 87092 minimal D-proofs with conclusions of even symbolic length, and there are 84961 minimal D-proofs with conclusions of odd symbolic length. [87092/172053 ≈ 50.62% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 1 9 0 10 0 11 0 12 0 13 1 14 1 15 3 16 7 17 5 18 13 19 22 20 23 21 10 22 19 23 43 24 46 25 51 26 72 27 89 28 114 29 141 30 160 31 177 32 189 33 276 34 274 35 367 36 365 37 440 38 490 39 517 40 632 41 574 42 724 43 762 44 840 45 913 46 1016 47 971 48 1105 49 1314 50 1289 51 1445 52 1468 53 1536 54 1608 55 1729 56 1756 57 1939 58 2084 59 2075 60 2018 61 2129 62 2315 63 2353 64 2372 65 2208 66 2598 67 2493 68 2306 69 2641 70 2555 71 2430 72 2247 73 2523 74 2762 75 2547 76 2710 77 2389 78 2628 79 2240 80 2364 81 2514 82 2430 83 2366 84 1970 85 2148 86 2101 87 2416 88 2395 89 1900 90 1893 91 1644 92 1766 93 1667 94 1987 95 1738 96 1659 97 1637 98 1480 99 1476 100 1539 101 1356 102 1351 103 1304 104 1194 105 1082 106 1312 107 1098 108 1260 109 1130 110 998 111 1053 112 955 113 962 114 925 115 987 116 864 117 782 118 960 119 662 120 858 121 705 122 895 123 742 124 686 125 759 126 523 127 691 128 636 129 719 130 578 131 552 132 639 133 430 134 609 135 492 136 556 137 442 138 512 139 467 140 434 141 486 142 423 143 470 144 372 145 384 146 464 147 358 148 375 149 363 150 447 151 359 152 338 153 352 154 317 155 305 156 303 157 346 158 293 159 270 160 263 161 246 162 269 163 261 164 261 165 254 166 289 167 242 168 204 169 248 170 219 171 243 172 223 173 233 174 209 175 154 176 262 177 196 178 193 179 186 180 179 181 156 182 171 183 189 184 175 185 159 186 185 187 142 188 139 189 106 190 142 191 145 192 122 193 125 194 138 195 113 196 119 197 128 198 150 199 87 200 118 201 109 202 109 203 109 204 114 205 113 206 109 207 82 208 93 209 93 210 82 211 92 212 108 213 94 214 95 215 71 216 65 217 74 218 100 219 86 220 74 221 72 222 71 223 62 224 60 225 53 226 58 227 44 228 65 229 36 230 60 231 49 232 47 233 59 234 51 235 40 236 46 237 35 238 46 239 44 240 45 241 36 242 43 243 35 244 34 245 45 246 31 247 26 248 24 249 29 250 40 251 35 252 55 253 18 254 37 255 24 256 29 257 29 258 41 259 29 260 23 261 29 262 22 263 16 264 34 265 15 266 31 267 10 268 22 269 11 270 14 271 22 272 22 273 20 274 14 275 29 276 12 277 13 278 25 279 27 280 27 281 16 282 31 283 13 284 16 285 16 286 22 287 22 288 11 289 19 290 8 291 14 292 20 293 17 294 17 295 8 296 25 297 8 298 18 299 18 300 18 301 16 302 12 303 16 304 6 305 10 306 18 307 10 308 17 309 8 310 16 311 5 312 5 313 12 314 11 315 12 316 7 317 15 318 5 319 5 320 17 321 10 322 7 323 5 324 17 325 3 326 5 327 14 328 9 329 8 330 3 331 5 332 3 333 4 334 11 335 7 336 14 337 6 338 7 339 2 340 3 341 7 342 6 343 7 344 1 345 6 346 2 347 0 348 6 349 6 350 11 351 6 352 3 353 3 354 4 355 5 356 6 357 9 358 4 359 4 360 1 361 1 362 6 363 5 364 7 365 4 366 3 367 2 368 2 369 6 370 3 371 7 372 3 373 3 374 0 375 2 376 2 377 1 378 6 379 1 380 2 381 1 382 2 383 2 384 0 385 4 386 2 387 1 388 0 389 0 390 4 391 0 392 5 393 2 394 2 395 1 396 0 397 3 398 1 399 4 400 0

113: Average symbolic conclusion length is 20977118/221055 ≈ 94.90. (Median: 84)
     There are 111309 minimal D-proofs with conclusions of even symbolic length, and there are 109746 minimal D-proofs with conclusions of odd symbolic length. [111309/221055 ≈ 50.35% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 3 13 4 14 1 15 0 16 6 17 6 18 6 19 10 20 17 21 30 22 42 23 46 24 52 25 57 26 113 27 94 28 175 29 149 30 208 31 213 32 244 33 305 34 346 35 398 36 426 37 473 38 543 39 618 40 631 41 703 42 889 43 911 44 954 45 1029 46 1141 47 1248 48 1351 49 1448 50 1691 51 1675 52 1758 53 1792 54 1955 55 2199 56 2421 57 2388 58 2174 59 2596 60 2598 61 2435 62 2965 63 2840 64 2857 65 2604 66 3061 67 3219 68 3089 69 3282 70 3110 71 3311 72 3029 73 3090 74 3614 75 3207 76 3353 77 2684 78 2966 79 2857 80 3530 81 3460 82 2802 83 2768 84 2404 85 2594 86 2582 87 2976 88 2855 89 2491 90 2557 91 2204 92 2561 93 2511 94 2287 95 2219 96 2160 97 2148 98 1827 99 2030 100 1744 101 2027 102 1918 103 1517 104 1867 105 1553 106 1543 107 1508 108 1504 109 1446 110 1352 111 1629 112 1206 113 1494 114 1328 115 1242 116 1241 117 1133 118 1224 119 909 120 1195 121 1136 122 1099 123 986 124 920 125 1010 126 808 127 1031 128 870 129 893 130 837 131 805 132 792 133 699 134 798 135 705 136 794 137 655 138 696 139 760 140 584 141 644 142 620 143 678 144 603 145 565 146 601 147 441 148 544 149 500 150 530 151 486 152 482 153 488 154 429 155 461 156 395 157 391 158 427 159 428 160 405 161 331 162 438 163 400 164 404 165 398 166 394 167 266 168 266 169 351 170 311 171 290 172 296 173 271 174 270 175 255 176 256 177 276 178 269 179 263 180 264 181 212 182 188 183 228 184 243 185 207 186 200 187 225 188 182 189 173 190 224 191 211 192 181 193 157 194 195 195 162 196 189 197 155 198 173 199 144 200 156 201 149 202 131 203 137 204 155 205 152 206 159 207 137 208 134 209 109 210 117 211 124 212 135 213 101 214 114 215 98 216 117 217 87 218 92 219 78 220 104 221 84 222 90 223 92 224 90 225 67 226 86 227 62 228 95 229 60 230 74 231 73 232 55 233 61 234 68 235 56 236 60 237 61 238 74 239 42 240 71 241 38 242 44 243 60 244 62 245 58 246 41 247 55 248 48 249 26 250 61 251 47 252 48 253 33 254 53 255 34 256 45 257 50 258 36 259 42 260 28 261 39 262 24 263 29 264 47 265 33 266 41 267 19 268 41 269 19 270 21 271 46 272 26 273 39 274 21 275 37 276 16 277 22 278 30 279 29 280 35 281 12 282 39 283 7 284 26 285 33 286 22 287 21 288 25 289 26 290 15 291 21 292 29 293 13 294 29 295 18 296 21 297 9 298 15 299 20 300 23 301 19 302 16 303 24 304 9 305 8 306 21 307 16 308 16 309 15 310 19 311 10 312 5 313 22 314 11 315 16 316 8 317 15 318 9 319 7 320 20 321 16 322 17 323 5 324 7 325 4 326 8 327 15 328 14 329 12 330 6 331 14 332 5 333 6 334 13 335 13 336 17 337 6 338 7 339 7 340 4 341 9 342 10 343 14 344 10 345 7 346 5 347 2 348 12 349 11 350 7 351 9 352 8 353 1 354 5 355 7 356 10 357 9 358 6 359 8 360 2 361 3 362 8 363 5 364 10 365 4 366 2 367 0 368 1 369 5 370 4 371 6 372 6 373 4 374 3 375 4 376 4 377 3 378 7 379 4 380 4 381 3 382 2 383 3 384 3 385 3 386 3 387 3 388 2 389 1 390 5 391 4 392 3 393 5 394 3 395 1 396 2 397 3 398 2 399 6 400 4

115: Average symbolic conclusion length is 27440092/283569 ≈ 96.77. (Median: 86)
     There are 141389 minimal D-proofs with conclusions of even symbolic length, and there are 142180 minimal D-proofs with conclusions of odd symbolic length. [141389/283569 ≈ 49.86% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 1 14 0 15 6 16 6 17 7 18 13 19 19 20 21 21 50 22 29 23 58 24 35 25 60 26 78 27 110 28 140 29 138 30 190 31 201 32 313 33 288 34 355 35 464 36 503 37 531 38 551 39 728 40 716 41 890 42 997 43 1170 44 1165 45 1216 46 1309 47 1485 48 1714 49 1909 50 1884 51 1856 52 2164 53 2306 54 2327 55 2666 56 2703 57 2808 58 2769 59 2952 60 3335 61 3380 62 3534 63 3491 64 3656 65 3396 66 3418 67 4215 68 3805 69 4007 70 3529 71 3808 72 3723 73 4426 74 4384 75 3675 76 3843 77 3698 78 3675 79 3865 80 4135 81 4100 82 3374 83 3701 84 3320 85 3908 86 3729 87 3455 88 3329 89 3217 90 3231 91 3046 92 3229 93 3040 94 3150 95 2951 96 2407 97 3015 98 2524 99 2590 100 2525 101 2471 102 2377 103 2311 104 2586 105 1941 106 2326 107 2183 108 2036 109 2149 110 1936 111 2031 112 1609 113 1957 114 1797 115 1801 116 1692 117 1582 118 1644 119 1413 120 1640 121 1476 122 1387 123 1381 124 1380 125 1357 126 1287 127 1330 128 1232 129 1204 130 1145 131 1073 132 1201 133 929 134 1097 135 1034 136 993 137 948 138 970 139 921 140 787 141 847 142 818 143 838 144 843 145 785 146 851 147 669 148 791 149 645 150 654 151 681 152 655 153 604 154 554 155 639 156 617 157 583 158 658 159 570 160 479 161 461 162 485 163 514 164 553 165 460 166 457 167 401 168 442 169 380 170 387 171 413 172 395 173 385 174 381 175 317 176 390 177 388 178 315 179 302 180 393 181 275 182 299 183 355 184 328 185 241 186 245 187 262 188 235 189 270 190 231 191 239 192 294 193 218 194 216 195 195 196 210 197 209 198 213 199 248 200 232 201 181 202 191 203 176 204 179 205 164 206 194 207 174 208 193 209 145 210 164 211 129 212 153 213 136 214 146 215 114 216 157 217 129 218 107 219 133 220 123 221 102 222 106 223 110 224 121 225 89 226 126 227 108 228 110 229 88 230 92 231 108 232 87 233 103 234 76 235 80 236 101 237 95 238 86 239 62 240 118 241 69 242 82 243 95 244 69 245 60 246 82 247 72 248 63 249 62 250 74 251 44 252 73 253 44 254 59 255 44 256 53 257 65 258 55 259 53 260 38 261 48 262 36 263 44 264 66 265 34 266 55 267 42 268 57 269 25 270 35 271 34 272 41 273 47 274 40 275 38 276 33 277 24 278 38 279 34 280 45 281 30 282 37 283 20 284 28 285 38 286 33 287 32 288 41 289 27 290 29 291 28 292 32 293 31 294 35 295 25 296 28 297 20 298 22 299 32 300 24 301 19 302 20 303 23 304 23 305 14 306 29 307 23 308 25 309 16 310 29 311 15 312 15 313 22 314 23 315 30 316 14 317 19 318 17 319 11 320 26 321 17 322 23 323 11 324 17 325 12 326 13 327 18 328 17 329 20 330 13 331 17 332 10 333 12 334 12 335 16 336 14 337 12 338 13 339 10 340 11 341 19 342 15 343 12 344 16 345 13 346 10 347 12 348 14 349 12 350 14 351 11 352 20 353 6 354 7 355 8 356 14 357 11 358 10 359 4 360 9 361 4 362 10 363 7 364 7 365 11 366 12 367 3 368 9 369 5 370 8 371 13 372 9 373 6 374 4 375 8 376 9 377 10 378 14 379 6 380 7 381 7 382 9 383 5 384 8 385 4 386 9 387 4 388 8 389 3 390 5 391 4 392 4 393 3 394 7 395 2 396 5 397 6 398 2 399 2 400 2

117: Average symbolic conclusion length is 35703666/361751 ≈ 98.70. (Median: 88)
     There are 182413 minimal D-proofs with conclusions of even symbolic length, and there are 179338 minimal D-proofs with conclusions of odd symbolic length. [182413/361751 ≈ 50.43% 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 3 14 5 15 2 16 8 17 3 18 6 19 6 20 24 21 29 22 28 23 44 24 36 25 101 26 76 27 126 28 143 29 162 30 203 31 203 32 293 33 285 34 429 35 473 36 535 37 651 38 615 39 732 40 920 41 1072 42 1159 43 1223 44 1367 45 1405 46 1656 47 1850 48 1984 49 2149 50 2258 51 2426 52 2324 53 2871 54 3021 55 3140 56 3213 57 3375 58 3397 59 3430 60 3960 61 3869 62 4128 63 4127 64 4277 65 4466 66 4591 67 4803 68 4339 69 4706 70 4766 71 4759 72 5027 73 5155 74 5165 75 4558 76 4774 77 4796 78 5321 79 5079 80 4695 81 4662 82 4527 83 4586 84 4729 85 4852 86 4614 87 4621 88 4425 89 3796 90 4663 91 4139 92 4178 93 3728 94 3858 95 3886 96 3818 97 3915 98 3173 99 3612 100 3326 101 3133 102 3474 103 3092 104 3110 105 2642 106 2998 107 2719 108 3032 109 2706 110 2608 111 2661 112 2336 113 2594 114 2315 115 2228 116 2120 117 2173 118 2232 119 2100 120 2150 121 1844 122 1918 123 1829 124 1823 125 1860 126 1686 127 1696 128 1666 129 1485 130 1476 131 1399 132 1415 133 1274 134 1404 135 1400 136 1272 137 1349 138 1285 139 1311 140 1124 141 1211 142 1137 143 1066 144 1157 145 976 146 947 147 902 148 938 149 923 150 1001 151 960 152 912 153 764 154 760 155 727 156 804 157 814 158 797 159 762 160 746 161 699 162 673 163 611 164 628 165 578 166 626 167 559 168 590 169 568 170 588 171 490 172 497 173 542 174 462 175 499 176 494 177 471 178 496 179 435 180 416 181 363 182 412 183 347 184 376 185 419 186 373 187 312 188 336 189 300 190 344 191 317 192 358 193 287 194 345 195 291 196 273 197 288 198 336 199 245 200 291 201 260 202 248 203 247 204 269 205 227 206 265 207 209 208 214 209 189 210 230 211 174 212 223 213 184 214 231 215 177 216 189 217 178 218 189 219 214 220 170 221 175 222 178 223 134 224 185 225 157 226 190 227 129 228 144 229 129 230 130 231 135 232 127 233 129 234 118 235 111 236 135 237 100 238 122 239 107 240 130 241 79 242 129 243 100 244 94 245 103 246 102 247 98 248 79 249 71 250 93 251 78 252 106 253 63 254 78 255 63 256 67 257 77 258 85 259 67 260 69 261 70 262 72 263 59 264 48 265 60 266 68 267 71 268 71 269 55 270 60 271 38 272 55 273 55 274 67 275 50 276 53 277 30 278 45 279 40 280 52 281 44 282 48 283 45 284 42 285 36 286 57 287 42 288 42 289 39 290 38 291 45 292 36 293 41 294 39 295 35 296 45 297 35 298 34 299 47 300 32 301 34 302 23 303 40 304 30 305 28 306 32 307 32 308 34 309 28 310 27 311 29 312 26 313 24 314 35 315 33 316 23 317 32 318 30 319 18 320 23 321 24 322 30 323 25 324 28 325 20 326 19 327 19 328 29 329 28 330 30 331 20 332 26 333 24 334 37 335 25 336 34 337 17 338 34 339 27 340 29 341 17 342 28 343 20 344 18 345 21 346 16 347 16 348 11 349 17 350 19 351 15 352 11 353 15 354 19 355 10 356 17 357 16 358 20 359 20 360 12 361 17 362 12 363 17 364 23 365 11 366 14 367 8 368 11 369 16 370 19 371 21 372 6 373 11 374 13 375 16 376 6 377 13 378 9 379 15 380 11 381 8 382 9 383 8 384 8 385 11 386 9 387 19 388 6 389 3 390 12 391 10 392 5 393 10 394 12 395 6 396 9 397 4 398 6 399 9 400 5

119: Average symbolic conclusion length is 46222421/458509 ≈ 100.81. (Median: 89)
     There are 231118 minimal D-proofs with conclusions of even symbolic length, and there are 227391 minimal D-proofs with conclusions of odd symbolic length. [231118/458509 ≈ 50.41% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 2 13 3 14 0 15 7 16 7 17 2 18 21 19 9 20 32 21 21 22 18 23 42 24 47 25 70 26 71 27 139 28 131 29 164 30 230 31 232 32 271 33 386 34 449 35 520 36 580 37 689 38 676 39 916 40 1092 41 1092 42 1303 43 1353 44 1561 45 1555 46 1855 47 2080 48 2227 49 2416 50 2496 51 2872 52 2823 53 3034 54 3337 55 3637 56 3922 57 3939 58 4302 59 4170 60 4779 61 4504 62 4924 63 5097 64 5289 65 5391 66 5610 67 5741 68 5662 69 5693 70 6018 71 6221 72 6148 73 5680 74 5944 75 5970 76 6175 77 6351 78 6743 79 6137 80 6373 81 5863 82 5562 83 6388 84 6357 85 6089 86 5357 87 5659 88 5786 89 5567 90 5766 91 5155 92 5666 93 4870 94 4864 95 5155 96 4786 97 4796 98 4252 99 4672 100 4019 101 4529 102 4159 103 3948 104 4004 105 3638 106 4087 107 3621 108 3637 109 3366 110 3283 111 3325 112 3025 113 3354 114 2906 115 3057 116 2952 117 2732 118 2957 119 2518 120 2585 121 2548 122 2436 123 2431 124 2540 125 2357 126 2036 127 2149 128 2063 129 1957 130 2116 131 1964 132 2071 133 1812 134 1833 135 1688 136 1693 137 1796 138 1680 139 1531 140 1576 141 1567 142 1473 143 1549 144 1453 145 1387 146 1330 147 1212 148 1245 149 1246 150 1310 151 1164 152 1226 153 1176 154 1087 155 1017 156 1056 157 955 158 967 159 945 160 894 161 874 162 942 163 857 164 918 165 776 166 874 167 689 168 815 169 687 170 771 171 756 172 752 173 635 174 691 175 626 176 662 177 636 178 682 179 549 180 637 181 513 182 528 183 472 184 557 185 459 186 524 187 493 188 473 189 448 190 483 191 453 192 474 193 416 194 416 195 397 196 409 197 421 198 400 199 352 200 391 201 346 202 356 203 349 204 391 205 373 206 334 207 322 208 319 209 293 210 332 211 273 212 323 213 277 214 286 215 262 216 246 217 274 218 253 219 267 220 235 221 234 222 219 223 189 224 232 225 199 226 247 227 173 228 220 229 186 230 191 231 207 232 192 233 180 234 176 235 153 236 141 237 132 238 192 239 151 240 184 241 121 242 127 243 121 244 160 245 139 246 134 247 139 248 113 249 108 250 102 251 113 252 119 253 88 254 154 255 110 256 103 257 85 258 103 259 90 260 102 261 91 262 110 263 88 264 66 265 86 266 93 267 76 268 95 269 84 270 60 271 54 272 91 273 73 274 74 275 75 276 74 277 66 278 67 279 66 280 75 281 58 282 60 283 50 284 67 285 59 286 61 287 66 288 57 289 73 290 65 291 59 292 62 293 60 294 54 295 36 296 56 297 57 298 51 299 38 300 57 301 34 302 50 303 47 304 38 305 46 306 60 307 43 308 60 309 40 310 50 311 33 312 40 313 36 314 51 315 53 316 46 317 40 318 41 319 39 320 34 321 56 322 47 323 44 324 51 325 40 326 46 327 55 328 41 329 45 330 39 331 47 332 29 333 32 334 25 335 37 336 31 337 28 338 34 339 21 340 29 341 21 342 33 343 38 344 23 345 36 346 30 347 36 348 24 349 21 350 29 351 29 352 23 353 20 354 25 355 15 356 23 357 28 358 19 359 19 360 20 361 18 362 27 363 39 364 29 365 17 366 26 367 15 368 21 369 18 370 12 371 21 372 24 373 20 374 16 375 3 376 16 377 14 378 17 379 12 380 26 381 11 382 12 383 17 384 22 385 11 386 11 387 20 388 16 389 10 390 12 391 13 392 23 393 12 394 28 395 17 396 13 397 5 398 12 399 23 400 14

121: Average symbolic conclusion length is 59659230/579502 ≈ 102.95. (Median: 91)
     There are 289386 minimal D-proofs with conclusions of even symbolic length, and there are 290116 minimal D-proofs with conclusions of odd symbolic length. [289386/579502 ≈ 49.94% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 2 12 0 13 5 14 1 15 2 16 5 17 4 18 9 19 11 20 29 21 30 22 39 23 49 24 55 25 76 26 109 27 112 28 145 29 209 30 221 31 282 32 337 33 417 34 456 35 562 36 610 37 714 38 839 39 922 40 1068 41 1191 42 1381 43 1458 44 1861 45 1815 46 2007 47 2331 48 2565 49 2878 50 3052 51 3230 52 3237 53 3887 54 3913 55 4101 56 4480 57 4849 58 4848 59 5082 60 5424 61 5682 62 6044 63 6266 64 6461 65 6443 66 6085 67 6747 68 6843 69 7432 70 7466 71 8109 72 7369 73 7837 74 7332 75 7241 76 8118 77 8310 78 7955 79 7264 80 7517 81 7725 82 7343 83 8038 84 7398 85 8267 86 6818 87 6951 88 7297 89 7203 90 7074 91 6464 92 6715 93 6060 94 6755 95 6463 96 5879 97 6137 98 5602 99 6041 100 5220 101 5786 102 5312 103 5213 104 5109 105 4677 106 5214 107 4371 108 4515 109 4455 110 4215 111 4660 112 3956 113 3995 114 3831 115 3725 116 3808 117 3854 118 3789 119 3118 120 3589 121 3269 122 3307 123 3364 124 3108 125 3117 126 2793 127 2774 128 2538 129 2700 130 2755 131 2661 132 2618 133 2442 134 2515 135 2223 136 2382 137 2182 138 2303 139 2038 140 1996 141 1947 142 1908 143 1862 144 1866 145 1806 146 1827 147 1622 148 1727 149 1572 150 1685 151 1499 152 1530 153 1396 154 1396 155 1389 156 1440 157 1434 158 1382 159 1241 160 1319 161 1154 162 1175 163 1116 164 1210 165 1084 166 1080 167 1068 168 1011 169 1009 170 1049 171 990 172 994 173 972 174 854 175 813 176 850 177 809 178 795 179 754 180 861 181 695 182 762 183 706 184 713 185 715 186 717 187 662 188 706 189 711 190 671 191 638 192 606 193 635 194 553 195 582 196 579 197 523 198 593 199 519 200 529 201 535 202 507 203 470 204 493 205 463 206 475 207 434 208 443 209 375 210 458 211 411 212 473 213 349 214 404 215 352 216 384 217 390 218 331 219 388 220 321 221 299 222 318 223 258 224 329 225 279 226 319 227 272 228 278 229 216 230 265 231 272 232 294 233 270 234 237 235 219 236 223 237 229 238 241 239 202 240 243 241 162 242 177 243 166 244 185 245 179 246 190 247 210 248 189 249 164 250 159 251 135 252 182 253 146 254 185 255 181 256 138 257 126 258 146 259 133 260 115 261 135 262 128 263 98 264 135 265 121 266 130 267 129 268 119 269 96 270 108 271 112 272 123 273 113 274 106 275 108 276 114 277 94 278 117 279 116 280 93 281 64 282 111 283 76 284 112 285 98 286 103 287 88 288 56 289 84 290 69 291 79 292 76 293 92 294 78 295 82 296 79 297 63 298 76 299 92 300 75 301 80 302 78 303 73 304 56 305 64 306 70 307 66 308 69 309 69 310 67 311 49 312 78 313 43 314 75 315 73 316 81 317 75 318 67 319 68 320 76 321 56 322 61 323 59 324 65 325 31 326 49 327 46 328 59 329 49 330 51 331 57 332 39 333 52 334 42 335 54 336 60 337 31 338 43 339 47 340 40 341 42 342 27 343 51 344 40 345 40 346 35 347 40 348 29 349 35 350 51 351 38 352 49 353 27 354 33 355 32 356 43 357 38 358 23 359 34 360 48 361 12 362 30 363 19 364 32 365 23 366 35 367 21 368 25 369 29 370 28 371 34 372 20 373 29 374 14 375 22 376 26 377 26 378 27 379 19 380 37 381 19 382 16 383 29 384 24 385 24 386 21 387 37 388 24 389 12 390 21 391 13 392 29 393 17 394 19 395 13 396 13 397 15 398 22 399 15 400 17

123: Average symbolic conclusion length is 77200769/734352 ≈ 105.13. (Median: 92)
     There are 370923 minimal D-proofs with conclusions of even symbolic length, and there are 363429 minimal D-proofs with conclusions of odd symbolic length. [370923/734352 ≈ 50.51% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 1 13 2 14 5 15 6 16 5 17 15 18 11 19 20 20 11 21 22 22 54 23 41 24 94 25 76 26 118 27 135 28 182 29 215 30 257 31 357 32 337 33 451 34 492 35 572 36 691 37 913 38 909 39 1068 40 1243 41 1403 42 1583 43 1877 44 1910 45 2019 46 2474 47 2595 48 2829 49 3195 50 3563 51 3691 52 3814 53 4295 54 4687 55 5282 56 5124 57 5659 58 5835 59 5792 60 6415 61 6654 62 7438 63 7314 64 8123 65 7891 66 8137 67 8274 68 8090 69 9285 70 9113 71 9103 72 8803 73 8997 74 9667 75 9136 76 10216 77 9615 78 10476 79 8699 80 8979 81 9678 82 9828 83 10148 84 9318 85 9512 86 8546 87 9089 88 9393 89 8643 90 9427 91 8912 92 8848 93 7713 94 8531 95 8036 96 7930 97 7768 98 7328 99 7764 100 6756 101 6797 102 6971 103 6454 104 7142 105 6237 106 6322 107 5700 108 5702 109 5863 110 6107 111 5875 112 5019 113 5598 114 5084 115 4975 116 5202 117 4583 118 4860 119 4219 120 4495 121 3992 122 4496 123 4205 124 3982 125 3922 126 3621 127 3729 128 3433 129 3496 130 3554 131 3570 132 3269 133 2822 134 3048 135 2896 136 3230 137 2917 138 3033 139 2852 140 2479 141 2469 142 2432 143 2447 144 2486 145 2377 146 2332 147 2192 148 2255 149 2130 150 2158 151 2134 152 1984 153 1992 154 1865 155 1845 156 1795 157 1669 158 1777 159 1633 160 1624 161 1543 162 1709 163 1500 164 1513 165 1549 166 1581 167 1379 168 1390 169 1312 170 1368 171 1351 172 1340 173 1298 174 1239 175 1191 176 1165 177 1058 178 1215 179 1078 180 1144 181 1006 182 1131 183 1072 184 1028 185 895 186 994 187 954 188 900 189 887 190 888 191 926 192 829 193 756 194 877 195 738 196 760 197 728 198 867 199 675 200 773 201 709 202 691 203 690 204 693 205 649 206 637 207 580 208 608 209 522 210 646 211 516 212 587 213 533 214 507 215 504 216 506 217 463 218 528 219 514 220 484 221 465 222 459 223 430 224 486 225 442 226 478 227 347 228 387 229 380 230 406 231 379 232 350 233 374 234 359 235 277 236 335 237 321 238 311 239 329 240 359 241 276 242 288 243 286 244 258 245 273 246 260 247 270 248 261 249 238 250 244 251 230 252 233 253 184 254 242 255 200 256 206 257 207 258 198 259 186 260 208 261 206 262 210 263 194 264 188 265 167 266 187 267 165 268 170 269 154 270 203 271 173 272 190 273 148 274 152 275 150 276 137 277 151 278 153 279 151 280 139 281 97 282 152 283 111 284 151 285 120 286 135 287 134 288 143 289 115 290 107 291 113 292 126 293 95 294 108 295 106 296 110 297 94 298 103 299 95 300 109 301 104 302 108 303 118 304 100 305 101 306 98 307 105 308 109 309 100 310 116 311 103 312 95 313 88 314 93 315 94 316 82 317 78 318 84 319 74 320 80 321 88 322 83 323 80 324 83 325 61 326 74 327 70 328 79 329 91 330 61 331 67 332 71 333 48 334 55 335 52 336 89 337 55 338 79 339 63 340 69 341 44 342 56 343 68 344 52 345 65 346 63 347 39 348 59 349 37 350 41 351 41 352 62 353 41 354 43 355 54 356 27 357 51 358 46 359 64 360 36 361 33 362 46 363 30 364 49 365 27 366 46 367 37 368 34 369 46 370 44 371 31 372 26 373 44 374 42 375 30 376 43 377 33 378 32 379 36 380 38 381 29 382 29 383 32 384 30 385 34 386 33 387 38 388 25 389 21 390 31 391 28 392 24 393 23 394 34 395 32 396 22 397 19 398 22 399 25 400 20

125: Average symbolic conclusion length is 100320202/935212 ≈ 107.27. (Median: 94)
     There are 469454 minimal D-proofs with conclusions of even symbolic length, and there are 465758 minimal D-proofs with conclusions of odd symbolic length. [469454/935212 ≈ 50.20% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 3 13 3 14 3 15 6 16 3 17 25 18 9 19 21 20 23 21 29 22 42 23 78 24 108 25 96 26 157 27 146 28 167 29 258 30 342 31 365 32 430 33 528 34 646 35 744 36 916 37 949 38 1056 39 1249 40 1432 41 1649 42 1784 43 2088 44 2269 45 2458 46 2794 47 3139 48 3664 49 3537 50 3996 51 4421 52 4517 53 5057 54 5301 55 6091 56 6252 57 6642 58 7009 59 7036 60 7940 61 7669 62 9043 63 8683 64 9019 65 9317 66 9477 67 10345 68 10097 69 11403 70 11051 71 11728 72 10603 73 10487 74 11631 75 11885 76 13031 77 11780 78 12162 79 11379 80 11710 81 12424 82 11971 83 12991 84 12256 85 11815 86 11133 87 11688 88 11624 89 11476 90 11402 91 10854 92 11512 93 10227 94 10063 95 10346 96 10353 97 10540 98 9489 99 9858 100 8800 101 8877 102 8971 103 9080 104 9069 105 7834 106 8492 107 7751 108 7597 109 7996 110 7436 111 7261 112 6447 113 6592 114 6094 115 6811 116 6495 117 6318 118 6448 119 5585 120 5932 121 5220 122 5266 123 5382 124 5418 125 4974 126 4314 127 4806 128 4489 129 4877 130 4613 131 4491 132 4441 133 3907 134 4022 135 3857 136 3959 137 3741 138 3773 139 3381 140 3447 141 3506 142 3303 143 3225 144 3550 145 3095 146 3108 147 2881 148 2921 149 2788 150 2724 151 2855 152 2733 153 2536 154 2553 155 2464 156 2528 157 2176 158 2525 159 2450 160 2197 161 2220 162 2155 163 1981 164 2149 165 2036 166 2147 167 1915 168 2016 169 1851 170 1820 171 1734 172 1780 173 1706 174 1607 175 1630 176 1694 177 1554 178 1506 179 1386 180 1607 181 1361 182 1463 183 1397 184 1416 185 1273 186 1271 187 1314 188 1217 189 1171 190 1244 191 1226 192 1234 193 1205 194 1161 195 1096 196 1056 197 1036 198 1119 199 945 200 976 201 1003 202 892 203 973 204 896 205 882 206 924 207 824 208 829 209 811 210 826 211 734 212 890 213 813 214 773 215 752 216 754 217 736 218 751 219 699 220 664 221 620 222 663 223 613 224 639 225 539 226 611 227 553 228 551 229 542 230 583 231 523 232 600 233 564 234 516 235 467 236 514 237 406 238 454 239 415 240 512 241 377 242 440 243 439 244 393 245 369 246 360 247 318 248 385 249 363 250 358 251 341 252 339 253 275 254 341 255 303 256 332 257 259 258 303 259 285 260 310 261 283 262 292 263 288 264 279 265 236 266 280 267 234 268 273 269 204 270 271 271 201 272 237 273 213 274 198 275 215 276 240 277 199 278 181 279 182 280 195 281 186 282 224 283 204 284 167 285 176 286 166 287 175 288 167 289 170 290 184 291 181 292 152 293 161 294 155 295 154 296 185 297 163 298 148 299 146 300 167 301 143 302 151 303 147 304 182 305 124 306 146 307 128 308 152 309 109 310 144 311 125 312 125 313 114 314 134 315 144 316 113 317 128 318 125 319 93 320 101 321 108 322 115 323 102 324 112 325 105 326 96 327 97 328 85 329 122 330 96 331 114 332 109 333 99 334 86 335 71 336 105 337 76 338 103 339 87 340 73 341 71 342 74 343 59 344 72 345 93 346 73 347 59 348 73 349 38 350 72 351 66 352 73 353 58 354 53 355 57 356 52 357 60 358 51 359 61 360 67 361 37 362 60 363 72 364 41 365 52 366 70 367 63 368 51 369 51 370 57 371 48 372 56 373 47 374 55 375 55 376 50 377 47 378 46 379 37 380 44 381 42 382 45 383 41 384 60 385 36 386 42 387 56 388 45 389 33 390 37 391 34 392 37 393 37 394 44 395 33 396 43 397 24 398 28 399 36 400 36

127: Average symbolic conclusion length is 130908512/1197027 ≈ 109.36. (Median: 96)
     There are 599615 minimal D-proofs with conclusions of even symbolic length, and there are 597412 minimal D-proofs with conclusions of odd symbolic length. [599615/1197027 ≈ 50.09% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 1 8 0 9 0 10 2 11 1 12 3 13 0 14 1 15 0 16 11 17 20 18 15 19 28 20 16 21 35 22 55 23 77 24 92 25 119 26 145 27 209 28 275 29 338 30 324 31 422 32 519 33 622 34 706 35 833 36 1001 37 1158 38 1324 39 1516 40 1692 41 2000 42 2134 43 2298 44 2798 45 2902 46 3330 47 3423 48 4053 49 4600 50 4583 51 5159 52 5379 53 6168 54 6073 55 6951 56 7173 57 7669 58 8387 59 8561 60 9339 61 9519 62 10703 63 10872 64 11219 65 11422 66 11188 67 12326 68 12673 69 14011 70 12794 71 13705 72 13748 73 13810 74 14432 75 14801 76 15616 77 15086 78 14606 79 14942 80 14972 81 15316 82 15376 83 15552 84 14820 85 15590 86 14425 87 14394 88 14720 89 15543 90 15133 91 13834 92 14215 93 13013 94 12919 95 13049 96 13312 97 13796 98 12148 99 12951 100 11615 101 11404 102 11496 103 11431 104 11205 105 10201 106 10340 107 9697 108 10358 109 9734 110 9749 111 10010 112 8734 113 9061 114 8321 115 8309 116 8450 117 8349 118 7809 119 6967 120 7752 121 6995 122 7359 123 7117 124 6835 125 6568 126 6177 127 6200 128 6176 129 6041 130 6160 131 5803 132 5443 133 5374 134 5751 135 5095 136 5289 137 5262 138 4980 139 4629 140 4609 141 4520 142 4571 143 4461 144 4560 145 4445 146 4008 147 3922 148 4017 149 3780 150 3763 151 3652 152 4009 153 3424 154 3632 155 3193 156 3304 157 3214 158 3233 159 3264 160 3083 161 3194 162 2980 163 2825 164 2838 165 2694 166 2767 167 2484 168 2662 169 2625 170 2548 171 2335 172 2346 173 2443 174 2296 175 2148 176 2238 177 2143 178 2142 179 1998 180 2024 181 2016 182 1888 183 1914 184 1955 185 1865 186 1876 187 1777 188 1739 189 1629 190 1663 191 1532 192 1671 193 1495 194 1499 195 1513 196 1549 197 1345 198 1422 199 1461 200 1393 201 1271 202 1293 203 1251 204 1222 205 1296 206 1280 207 1161 208 1261 209 1094 210 1193 211 1116 212 1148 213 1073 214 1060 215 1013 216 1037 217 965 218 936 219 981 220 1021 221 886 222 948 223 882 224 919 225 812 226 886 227 791 228 846 229 769 230 722 231 721 232 710 233 633 234 712 235 692 236 712 237 611 238 623 239 532 240 592 241 584 242 597 243 530 244 554 245 507 246 525 247 527 248 551 249 462 250 433 251 450 252 460 253 389 254 516 255 469 256 432 257 362 258 433 259 400 260 422 261 415 262 393 263 366 264 366 265 332 266 338 267 331 268 384 269 342 270 318 271 249 272 281 273 284 274 308 275 344 276 324 277 266 278 267 279 271 280 284 281 247 282 314 283 290 284 277 285 236 286 259 287 240 288 271 289 250 290 292 291 227 292 228 293 217 294 233 295 214 296 235 297 225 298 203 299 185 300 207 301 206 302 190 303 233 304 226 305 143 306 186 307 177 308 187 309 171 310 209 311 186 312 190 313 122 314 174 315 177 316 169 317 154 318 181 319 157 320 153 321 133 322 173 323 140 324 175 325 132 326 136 327 122 328 135 329 125 330 123 331 131 332 139 333 96 334 118 335 118 336 124 337 84 338 123 339 108 340 101 341 91 342 104 343 116 344 123 345 118 346 96 347 80 348 74 349 88 350 82 351 107 352 93 353 86 354 85 355 79 356 102 357 72 358 96 359 88 360 93 361 70 362 70 363 96 364 80 365 62 366 85 367 57 368 81 369 73 370 94 371 67 372 86 373 70 374 77 375 66 376 61 377 66 378 59 379 52 380 74 381 48 382 56 383 59 384 57 385 46 386 57 387 44 388 61 389 46 390 51 391 46 392 63 393 49 394 74 395 36 396 57 397 31 398 53 399 46 400 62

129: Average symbolic conclusion length is 170970341/1534565 ≈ 111.41. (Median: 97)
     There are 774078 minimal D-proofs with conclusions of even symbolic length, and there are 760487 minimal D-proofs with conclusions of odd symbolic length. [774078/1534565 ≈ 50.44% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 5 13 0 14 2 15 4 16 7 17 8 18 16 19 15 20 34 21 64 22 87 23 55 24 76 25 127 26 177 27 172 28 247 29 312 30 435 31 529 32 589 33 708 34 740 35 1053 36 1055 37 1415 38 1494 39 1777 40 1866 41 2149 42 2741 43 2716 44 3214 45 3418 46 3918 47 4001 48 4429 49 5079 50 5372 51 6269 52 6432 53 7015 54 7639 55 8461 56 8816 57 9180 58 10074 59 10675 60 10960 61 11875 62 12506 63 12406 64 13559 65 14181 66 14323 67 14780 68 15688 69 16374 70 16326 71 16546 72 17177 73 17398 74 18109 75 18277 76 18647 77 18392 78 19310 79 18649 80 18792 81 18378 82 20241 83 19798 84 18557 85 19211 86 18377 87 18245 88 17704 89 18196 90 19375 91 17623 92 18586 93 16861 94 17304 95 16373 96 16737 97 17101 98 15797 99 16004 100 14670 101 14994 102 14837 103 15152 104 15594 105 13160 106 13923 107 12475 108 12863 109 12558 110 12806 111 11924 112 11369 113 12130 114 11179 115 11460 116 11429 117 10464 118 10484 119 9701 120 9838 121 9366 122 9910 123 9476 124 9269 125 8705 126 8550 127 8615 128 8152 129 8155 130 8177 131 7698 132 7491 133 7296 134 7372 135 6891 136 7161 137 6666 138 7145 139 6421 140 6432 141 6433 142 5922 143 6010 144 5752 145 6141 146 5441 147 5685 148 5538 149 4931 150 5675 151 4808 152 5069 153 4653 154 4904 155 4652 156 4379 157 4587 158 4203 159 4288 160 3908 161 4064 162 4087 163 3848 164 4069 165 3742 166 3940 167 3715 168 3461 169 3337 170 3375 171 3358 172 3220 173 3088 174 3233 175 2902 176 2978 177 2776 178 2939 179 2739 180 2672 181 2685 182 2645 183 2488 184 2518 185 2526 186 2536 187 2222 188 2401 189 2363 190 2140 191 2114 192 2355 193 1982 194 2039 195 1971 196 1985 197 1861 198 2112 199 1877 200 1847 201 1852 202 1763 203 1760 204 1700 205 1572 206 1676 207 1639 208 1614 209 1534 210 1664 211 1322 212 1528 213 1496 214 1487 215 1365 216 1392 217 1240 218 1314 219 1195 220 1306 221 1212 222 1235 223 1064 224 1167 225 1055 226 1160 227 1111 228 1158 229 1004 230 1048 231 868 232 844 233 894 234 1042 235 850 236 854 237 820 238 822 239 751 240 900 241 749 242 780 243 656 244 735 245 613 246 781 247 726 248 750 249 610 250 673 251 624 252 652 253 605 254 696 255 607 256 557 257 483 258 573 259 476 260 574 261 614 262 599 263 472 264 452 265 433 266 488 267 490 268 552 269 406 270 457 271 404 272 438 273 449 274 441 275 482 276 482 277 367 278 383 279 366 280 378 281 357 282 422 283 393 284 365 285 288 286 379 287 313 288 355 289 331 290 360 291 292 292 310 293 260 294 341 295 272 296 355 297 285 298 288 299 233 300 307 301 228 302 294 303 309 304 265 305 244 306 250 307 249 308 246 309 256 310 236 311 229 312 288 313 196 314 242 315 239 316 236 317 226 318 213 319 192 320 188 321 227 322 212 323 178 324 215 325 177 326 177 327 165 328 202 329 164 330 197 331 175 332 188 333 165 334 147 335 150 336 183 337 165 338 168 339 138 340 150 341 107 342 181 343 127 344 159 345 143 346 141 347 122 348 139 349 136 350 134 351 161 352 170 353 105 354 127 355 94 356 143 357 123 358 158 359 119 360 111 361 112 362 104 363 108 364 125 365 101 366 131 367 93 368 93 369 94 370 97 371 101 372 100 373 84 374 99 375 96 376 86 377 91 378 119 379 77 380 97 381 100 382 91 383 78 384 87 385 82 386 82 387 107 388 73 389 60 390 61 391 81 392 82 393 73 394 91 395 47 396 68 397 59 398 79 399 83 400 71

131: Average symbolic conclusion length is 223085992/1965596 ≈ 113.50. (Median: 99)
     There are 986670 minimal D-proofs with conclusions of even symbolic length, and there are 978926 minimal D-proofs with conclusions of odd symbolic length. [986670/1965596 ≈ 50.20% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 1 13 1 14 7 15 11 16 3 17 4 18 18 19 18 20 18 21 44 22 48 23 88 24 111 25 143 26 176 27 180 28 302 29 304 30 513 31 516 32 633 33 654 34 819 35 1104 36 1211 37 1533 38 1612 39 1922 40 2126 41 2411 42 2784 43 3050 44 3804 45 4037 46 4382 47 5077 48 5490 49 5939 50 6407 51 7354 52 8125 53 8205 54 9068 55 9518 56 10380 57 11462 58 12143 59 12754 60 13196 61 13902 62 14815 63 15545 64 16513 65 16945 66 18138 67 18089 68 18750 69 19571 70 20079 71 21027 72 21301 73 21511 74 21060 75 23216 76 23232 77 21875 78 23705 79 23221 80 23531 81 22513 82 23671 83 24966 84 23223 85 24414 86 22998 87 24028 88 22965 89 22932 90 24313 91 22422 92 23187 93 20575 94 21613 95 21596 96 22404 97 22961 98 19685 99 20162 100 18056 101 19365 102 19229 103 19456 104 18980 105 17638 106 18342 107 16452 108 17742 109 17651 110 16273 111 16304 112 15573 113 15629 114 14434 115 15212 116 14151 117 14361 118 14043 119 13168 120 13767 121 12613 122 12603 123 12269 124 11782 125 11610 126 11536 127 11730 128 10964 129 11552 130 10738 131 10594 132 10295 133 10002 134 10161 135 8817 136 9797 137 8924 138 9333 139 8554 140 8645 141 8588 142 7667 143 8784 144 7722 145 7767 146 7591 147 7378 148 7371 149 6542 150 7455 151 6286 152 6770 153 6233 154 6124 155 6353 156 5956 157 6218 158 5825 159 6012 160 5847 161 5267 162 5435 163 5012 164 5324 165 4978 166 4978 167 4968 168 4761 169 4482 170 4610 171 4537 172 4311 173 4065 174 4262 175 4005 176 3894 177 3739 178 4014 179 3715 180 3712 181 3651 182 3605 183 3219 184 3347 185 3410 186 3369 187 3024 188 3112 189 2847 190 2901 191 2961 192 2843 193 2750 194 2936 195 2650 196 2661 197 2404 198 2560 199 2399 200 2446 201 2399 202 2372 203 2353 204 2256 205 2178 206 2301 207 2211 208 2087 209 2021 210 2011 211 1825 212 2021 213 1840 214 1923 215 1747 216 1781 217 1559 218 1699 219 1683 220 1715 221 1645 222 1685 223 1456 224 1399 225 1356 226 1500 227 1476 228 1417 229 1215 230 1356 231 1183 232 1387 233 1309 234 1221 235 1178 236 1152 237 1049 238 1106 239 1151 240 1228 241 1017 242 1067 243 965 244 1015 245 924 246 1048 247 954 248 1044 249 841 250 888 251 782 252 863 253 817 254 931 255 833 256 795 257 699 258 797 259 703 260 817 261 779 262 678 263 649 264 696 265 565 266 713 267 668 268 747 269 633 270 668 271 563 272 633 273 553 274 562 275 598 276 655 277 488 278 537 279 497 280 524 281 465 282 559 283 437 284 521 285 411 286 484 287 448 288 547 289 447 290 414 291 450 292 397 293 425 294 425 295 386 296 431 297 353 298 422 299 318 300 428 301 353 302 406 303 360 304 361 305 366 306 321 307 338 308 362 309 335 310 390 311 316 312 368 313 263 314 377 315 304 316 337 317 345 318 312 319 286 320 264 321 273 322 305 323 290 324 299 325 230 326 275 327 234 328 251 329 263 330 303 331 218 332 221 333 264 334 205 335 277 336 251 337 224 338 244 339 209 340 210 341 177 342 225 343 214 344 226 345 208 346 188 347 183 348 175 349 195 350 225 351 248 352 231 353 161 354 208 355 172 356 191 357 191 358 189 359 198 360 175 361 131 362 155 363 141 364 186 365 137 366 147 367 141 368 138 369 125 370 156 371 162 372 155 373 130 374 151 375 151 376 148 377 130 378 157 379 122 380 158 381 126 382 132 383 108 384 154 385 136 386 138 387 137 388 116 389 119 390 123 391 98 392 152 393 87 394 110 395 83 396 111 397 66 398 98 399 126 400 100

133: Average symbolic conclusion length is 290310676/2509883 ≈ 115.67. (Median: 101)
     There are 1259639 minimal D-proofs with conclusions of even symbolic length, and there are 1250244 minimal D-proofs with conclusions of odd symbolic length. [1259639/2509883 ≈ 50.19% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 1 11 0 12 2 13 1 14 2 15 1 16 8 17 12 18 14 19 20 20 27 21 39 22 64 23 116 24 84 25 161 26 123 27 177 28 231 29 335 30 474 31 477 32 671 33 696 34 978 35 1066 36 1278 37 1641 38 1858 39 2149 40 2385 41 2842 42 3131 43 3584 44 4128 45 4891 46 5131 47 5577 48 6029 49 7057 50 7960 51 8428 52 9441 53 9781 54 10342 55 11357 56 12469 57 13668 58 14335 59 15457 60 15845 61 16478 62 17964 63 18680 64 19638 65 20688 66 21234 67 21590 68 22977 69 24043 70 22964 71 25510 72 25768 73 26863 74 26226 75 27013 76 28868 77 28054 78 29104 79 28341 80 29660 81 29046 82 28335 83 31529 84 29103 85 30526 86 27999 87 29370 88 29001 89 30732 90 31611 91 27595 92 28347 93 26460 94 27834 95 27844 96 27864 97 28058 98 25652 99 26646 100 24415 101 26949 102 25979 103 23979 104 24028 105 22922 106 23298 107 21755 108 23039 109 21681 110 21988 111 21519 112 20042 113 21124 114 19346 115 19372 116 18869 117 18317 118 18107 119 17600 120 18141 121 16150 122 17527 123 16342 124 15913 125 15970 126 15378 127 15314 128 13792 129 15066 130 14158 131 13920 132 13529 133 12800 134 12973 135 11576 136 13397 137 11862 138 11834 139 11841 140 11199 141 11129 142 10576 143 11175 144 10325 145 10508 146 10169 147 9350 148 10045 149 8788 150 9539 151 8837 152 8949 153 8847 154 8317 155 8271 156 7884 157 7888 158 7862 159 7627 160 7903 161 7258 162 7525 163 6883 164 7253 165 6465 166 6565 167 6383 168 6257 169 5920 170 6050 171 6040 172 5899 173 5625 174 5630 175 5240 176 5081 177 4970 178 5248 179 4987 180 5261 181 4706 182 4588 183 4517 184 4652 185 4249 186 4270 187 4278 188 4078 189 3899 190 3929 191 3728 192 3826 193 3696 194 3661 195 3487 196 3704 197 3264 198 3384 199 3311 200 3415 201 3167 202 3015 203 2736 204 3056 205 2885 206 2970 207 2740 208 2901 209 2507 210 2569 211 2461 212 2834 213 2404 214 2577 215 2411 216 2451 217 2101 218 2310 219 2293 220 2282 221 2185 222 2153 223 1951 224 2135 225 2066 226 2051 227 1804 228 2029 229 1688 230 1746 231 1721 232 1907 233 1665 234 1741 235 1562 236 1593 237 1492 238 1511 239 1512 240 1623 241 1374 242 1429 243 1311 244 1418 245 1183 246 1394 247 1374 248 1345 249 1224 250 1181 251 1089 252 1170 253 1068 254 1184 255 1042 256 1148 257 945 258 1123 259 969 260 1075 261 968 262 1015 263 917 264 1009 265 905 266 932 267 819 268 926 269 826 270 941 271 757 272 881 273 786 274 798 275 811 276 754 277 700 278 695 279 702 280 749 281 633 282 714 283 602 284 718 285 581 286 700 287 625 288 657 289 578 290 610 291 641 292 572 293 565 294 595 295 572 296 590 297 523 298 612 299 445 300 568 301 521 302 524 303 541 304 517 305 510 306 497 307 478 308 516 309 471 310 548 311 482 312 482 313 377 314 460 315 459 316 451 317 414 318 411 319 392 320 392 321 389 322 435 323 410 324 404 325 304 326 398 327 363 328 377 329 350 330 377 331 358 332 336 333 331 334 324 335 318 336 388 337 310 338 379 339 284 340 361 341 268 342 353 343 309 344 378 345 333 346 295 347 298 348 325 349 224 350 318 351 248 352 288 353 238 354 262 355 239 356 244 357 264 358 254 359 231 360 252 361 214 362 237 363 279 364 266 365 234 366 237 367 203 368 245 369 228 370 211 371 229 372 233 373 203 374 222 375 203 376 209 377 180 378 226 379 200 380 191 381 178 382 197 383 173 384 185 385 175 386 162 387 178 388 143 389 179 390 174 391 142 392 193 393 147 394 161 395 151 396 127 397 121 398 141 399 179 400 145

135: Average symbolic conclusion length is 376873903/3196594 ≈ 117.90. (Median: 103)
     There are 1610585 minimal D-proofs with conclusions of even symbolic length, and there are 1586009 minimal D-proofs with conclusions of odd symbolic length. [1610585/3196594 ≈ 50.38% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 2 12 1 13 1 14 1 15 11 16 8 17 5 18 30 19 15 20 19 21 23 22 61 23 67 24 99 25 157 26 139 27 272 28 266 29 373 30 450 31 554 32 706 33 772 34 1010 35 1181 36 1514 37 1646 38 2062 39 2419 40 2518 41 2913 42 3678 43 4247 44 4667 45 5336 46 5856 47 6128 48 7141 49 8095 50 9098 51 9814 52 10506 53 11519 54 12070 55 13737 56 14445 57 15527 58 16788 59 17509 60 19140 61 19571 62 21064 63 21624 64 23577 65 24840 66 25886 67 26619 68 26365 69 29510 70 29959 71 30943 72 31370 73 32779 74 32584 75 31653 76 35568 77 34013 78 36100 79 35216 80 36530 81 36193 82 37377 83 38614 84 35717 85 37018 86 36564 87 37504 88 37923 89 37261 90 38319 91 34906 92 36448 93 34963 94 37813 95 36181 96 34343 97 34098 98 32674 99 33121 100 32720 101 33552 102 31819 103 31673 104 31586 105 29207 106 31557 107 28931 108 29237 109 27773 110 27576 111 27589 112 26588 113 26696 114 23652 115 25799 116 24807 117 23763 118 24813 119 22554 120 22809 121 20481 122 22197 123 21148 124 21567 125 20992 126 20019 127 19973 128 18258 129 19402 130 18092 131 17798 132 17676 133 17067 134 17351 135 16347 136 16766 137 15429 138 15864 139 15310 140 14954 141 15254 142 14322 143 14177 144 14195 145 13408 146 13229 147 12736 148 12698 149 11780 150 12297 151 11919 152 11948 153 11678 154 11285 155 11322 156 10704 157 10765 158 10340 159 10115 160 10074 161 9393 162 9447 163 8976 164 9349 165 8771 166 8968 167 8571 168 8478 169 7685 170 7774 171 7689 172 7562 173 7693 174 7505 175 6918 176 7299 177 6926 178 6941 179 6385 180 6735 181 5948 182 6251 183 5990 184 5874 185 5717 186 5860 187 5336 188 5458 189 5257 190 5433 191 4988 192 5455 193 4940 194 4963 195 4539 196 4409 197 4361 198 4745 199 4346 200 4371 201 4382 202 4188 203 3752 204 4173 205 3808 206 3957 207 3867 208 3937 209 3478 210 3816 211 3456 212 3467 213 3314 214 3484 215 3233 216 3290 217 3175 218 3225 219 3113 220 3018 221 2853 222 2929 223 2614 224 2673 225 2704 226 2828 227 2556 228 2603 229 2338 230 2566 231 2173 232 2396 233 2270 234 2363 235 2150 236 2153 237 2125 238 2001 239 1900 240 2113 241 1814 242 2100 243 1766 244 1903 245 1645 246 1902 247 1646 248 1726 249 1732 250 1599 251 1636 252 1666 253 1384 254 1609 255 1436 256 1594 257 1311 258 1549 259 1373 260 1343 261 1325 262 1417 263 1283 264 1353 265 1179 266 1321 267 1178 268 1279 269 1145 270 1245 271 966 272 1191 273 1084 274 1104 275 1030 276 1042 277 999 278 969 279 1009 280 1003 281 886 282 1046 283 873 284 987 285 867 286 891 287 819 288 914 289 812 290 896 291 873 292 841 293 769 294 859 295 749 296 866 297 725 298 794 299 728 300 776 301 696 302 768 303 711 304 733 305 660 306 709 307 607 308 758 309 642 310 696 311 605 312 688 313 549 314 617 315 665 316 647 317 588 318 586 319 557 320 566 321 547 322 577 323 570 324 598 325 483 326 563 327 538 328 536 329 504 330 542 331 542 332 493 333 503 334 519 335 453 336 496 337 469 338 517 339 448 340 464 341 427 342 449 343 418 344 411 345 423 346 419 347 431 348 444 349 374 350 448 351 393 352 403 353 371 354 390 355 364 356 358 357 367 358 358 359 337 360 314 361 318 362 339 363 338 364 316 365 346 366 347 367 326 368 310 369 307 370 343 371 302 372 301 373 269 374 291 375 278 376 265 377 269 378 306 379 246 380 270 381 222 382 252 383 259 384 257 385 252 386 249 387 290 388 224 389 203 390 255 391 224 392 268 393 209 394 226 395 208 396 214 397 185 398 223 399 226 400 194

137: Average symbolic conclusion length is 488886513/4066027 ≈ 120.24. (Median: 105)
     There are 2042024 minimal D-proofs with conclusions of even symbolic length, and there are 2024003 minimal D-proofs with conclusions of odd symbolic length. [2042024/4066027 ≈ 50.22% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 0 12 2 13 0 14 3 15 5 16 5 17 15 18 26 19 11 20 50 21 35 22 75 23 80 24 93 25 166 26 173 27 245 28 291 29 476 30 484 31 611 32 806 33 855 34 1040 35 1362 36 1657 37 1893 38 2174 39 2564 40 2865 41 3452 42 3940 43 4562 44 5172 45 5525 46 6570 47 7163 48 8335 49 8981 50 9839 51 11305 52 11825 53 13911 54 13748 55 15560 56 17037 57 18030 58 20294 59 20994 60 22708 61 22202 62 25380 63 26807 64 28009 65 29958 66 31104 67 32002 68 31373 69 34512 70 35460 71 38050 72 38755 73 39217 74 40476 75 40864 76 42952 77 41671 78 43777 79 44316 80 44934 81 45690 82 45611 83 46870 84 45286 85 46400 86 46523 87 48520 88 47071 89 45071 90 45547 91 44739 92 45880 93 46115 94 46843 95 43982 96 44193 97 43947 98 41475 99 44706 100 42407 101 41834 102 38928 103 39898 104 40395 105 39328 106 39328 107 36047 108 37949 109 35889 110 34773 111 36457 112 34028 113 33929 114 31477 115 32957 116 31291 117 32133 118 30738 119 29455 120 30110 121 27246 122 29254 123 27676 124 27300 125 26487 126 25792 127 25898 128 24394 129 24925 130 23458 131 24242 132 23166 133 22830 134 23156 135 21258 136 21412 137 20925 138 20529 139 19965 140 20286 141 19124 142 18393 143 18501 144 18068 145 17601 146 17545 147 16805 148 17153 149 15760 150 16227 151 15071 152 15433 153 14985 154 14654 155 14014 156 14155 157 14108 158 13541 159 13549 160 13395 161 12396 162 12787 163 11367 164 11942 165 11212 166 11833 167 10771 168 11222 169 10981 170 10613 171 10316 172 10295 173 9788 174 9747 175 9300 176 9524 177 8793 178 9437 179 8636 180 8768 181 8113 182 8439 183 7832 184 7766 185 7733 186 7608 187 7400 188 7524 189 6784 190 7130 191 6851 192 7072 193 6630 194 6923 195 6365 196 6330 197 6107 198 6036 199 5752 200 6013 201 5738 202 5646 203 5534 204 5568 205 5148 206 5473 207 5182 208 5222 209 4920 210 5025 211 4652 212 4910 213 4621 214 4543 215 4222 216 4463 217 3855 218 4424 219 4125 220 4237 221 3965 222 3990 223 3761 224 3669 225 3553 226 3560 227 3323 228 3608 229 3107 230 3542 231 3096 232 3168 233 3080 234 3139 235 3060 236 2897 237 2892 238 2848 239 2635 240 2876 241 2573 242 2996 243 2314 244 2709 245 2499 246 2381 247 2325 248 2344 249 2340 250 2225 251 2217 252 2388 253 1823 254 2299 255 2008 256 2170 257 1906 258 2121 259 1857 260 1978 261 1904 262 1895 263 1771 264 1807 265 1611 266 1771 267 1637 268 1745 269 1575 270 1712 271 1473 272 1652 273 1403 274 1514 275 1460 276 1522 277 1408 278 1464 279 1441 280 1317 281 1319 282 1466 283 1237 284 1368 285 1235 286 1299 287 1190 288 1329 289 1173 290 1187 291 1140 292 1131 293 1067 294 1240 295 1048 296 1126 297 1054 298 1073 299 1000 300 1075 301 1004 302 1090 303 1075 304 1011 305 973 306 992 307 869 308 986 309 942 310 985 311 867 312 871 313 865 314 869 315 834 316 888 317 866 318 800 319 796 320 815 321 803 322 846 323 802 324 886 325 695 326 803 327 741 328 684 329 680 330 745 331 682 332 726 333 638 334 693 335 659 336 703 337 580 338 677 339 664 340 632 341 620 342 634 343 585 344 588 345 621 346 579 347 580 348 584 349 533 350 553 351 538 352 536 353 544 354 510 355 496 356 561 357 481 358 514 359 514 360 499 361 421 362 480 363 524 364 476 365 395 366 466 367 391 368 421 369 406 370 459 371 393 372 450 373 365 374 407 375 367 376 416 377 367 378 424 379 346 380 386 381 345 382 340 383 364 384 357 385 359 386 347 387 345 388 350 389 309 390 341 391 306 392 348 393 328 394 340 395 310 396 331 397 266 398 275 399 292 400 302

139: Average symbolic conclusion length is 635138675/5180139 ≈ 122.61. (Median: 106)
     There are 2600866 minimal D-proofs with conclusions of even symbolic length, and there are 2579273 minimal D-proofs with conclusions of odd symbolic length. [2600866/5180139 ≈ 50.21% even]
1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 2 11 2 12 0 13 5 14 1 15 8 16 6 17 12 18 21 19 25 20 31 21 48 22 104 23 107 24 132 25 162 26 192 27 292 28 381 29 413 30 515 31 721 32 817 33 1066 34 1285 35 1470 36 1764 37 2125 38 2312 39 2847 40 3460 41 3965 42 4355 43 4920 44 6011 45 6441 46 7875 47 7982 48 9341 49 10540 50 11329 51 13377 52 14095 53 15675 54 16080 55 17928 56 19976 57 21285 58 23659 59 24678 60 26405 61 26921 62 28935 63 31693 64 34445 65 35673 66 36313 67 38779 68 39464 69 42196 70 42519 71 45347 72 46819 73 47628 74 48554 75 49512 76 51853 77 52771 78 54275 79 54940 80 56013 81 55468 82 53983 83 56236 84 56328 85 59212 86 59348 87 60736 88 56870 89 58080 90 57103 91 56293 92 59710 93 59229 94 57748 95 54153 96 55191 97 55862 98 55104 99 56435 100 53066 101 55434 102 50957 103 50735 104 51996 105 50146 106 50382 107 46363 108 48070 109 45500 110 47294 111 45313 112 43614 113 44326 114 40997 115 42973 116 40760 117 40768 118 39481 119 38509 120 38559 121 35881 122 38109 123 34644 124 35975 125 34806 126 33705 127 34540 128 31246 129 31516 130 30686 131 30424 132 30300 133 30008 134 29369 135 26457 136 28165 137 26295 138 27285 139 26374 140 25878 141 25635 142 23905 143 23698 144 22254 145 22257 146 22757 147 21723 148 22062 149 20809 150 21679 151 19739 152 20474 153 19639 154 19675 155 19298 156 18169 157 18068 158 17456 159 17270 160 16892 161 16585 162 16809 163 15392 164 16131 165 15347 166 15291 167 14581 168 14755 169 13921 170 13724 171 13756 172 13606 173 13374 174 13122 175 12347 176 12453 177 11709 178 12149 179 11257 180 11972 181 11133 182 11090 183 10524 184 10709 185 10606 186 10540 187 10109 188 10244 189 9726 190 9602 191 8881 192 9504 193 8969 194 8826 195 8669 196 8682 197 8052 198 8310 199 7990 200 8003 201 7755 202 7979 203 7207 204 7652 205 7290 206 7293 207 6844 208 6902 209 6828 210 6429 211 6322 212 6598 213 6189 214 6390 215 5738 216 6266 217 5512 218 5794 219 5440 220 5531 221 5396 222 5447 223 5236 224 5248 225 4758 226 5098 227 4634 228 5112 229 4302 230 4742 231 4486 232 4368 233 4413 234 4271 235 4286 236 4095 237 4036 238 4042 239 3606 240 4231 241 3492 242 3771 243 3521 244 3685 245 3317 246 3335 247 3469 248 3397 249 3259 250 3213 251 3044 252 3228 253 2910 254 3142 255 2795 256 2901 257 2689 258 2824 259 2616 260 2801 261 2606 262 2542 263 2551 264 2624 265 2392 266 2435 267 2319 268 2384 269 2215 270 2418 271 2130 272 2329 273 2032 274 2151 275 2143 276 2096 277 1941 278 2030 279 1964 280 1954 281 1889 282 1989 283 1722 284 1840 285 1687 286 1837 287 1645 288 1701 289 1653 290 1746 291 1592 292 1635 293 1552 294 1694 295 1484 296 1715 297 1411 298 1521 299 1412 300 1544 301 1335 302 1485 303 1460 304 1333 305 1220 306 1351 307 1290 308 1377 309 1292 310 1349 311 1256 312 1282 313 1147 314 1249 315 1250 316 1222 317 1169 318 1153 319 1073 320 1173 321 1031 322 1108 323 1085 324 1155 325 1004 326 1032 327 1037 328 1068 329 929 330 1018 331 1028 332 1070 333 940 334 953 335 942 336 919 337 793 338 942 339 896 340 875 341 828 342 883 343 773 344 876 345 810 346 834 347 767 348 849 349 741 350 787 351 794 352 727 353 688 354 693 355 638 356 789 357 679 358 630 359 631 360 716 361 543 362 609 363 674 364 649 365 575 366 642 367 581 368 597 369 528 370 572 371 620 372 608 373 512 374 543 375 562 376 551 377 466 378 592 379 488 380 542 381 561 382 504 383 488 384 481 385 426 386 459 387 465 388 459 389 423 390 450 391 416 392 493 393 422 394 435 395 390 396 401 397 382 398 412 399 461 400 414