pylucene 3.5.0-3
[pylucene.git] / lucene-java-3.5.0 / lucene / contrib / facet / src / test / org / apache / lucene / util / encoding / EncodingSpeed.java
1 package org.apache.lucene.util.encoding;
2
3 import java.io.ByteArrayInputStream;
4 import java.io.ByteArrayOutputStream;
5 import java.io.IOException;
6 import java.text.NumberFormat;
7 import java.util.Arrays;
8
9 import org.apache.lucene.util.encoding.DGapIntEncoder;
10 import org.apache.lucene.util.encoding.EightFlagsIntEncoder;
11 import org.apache.lucene.util.encoding.FourFlagsIntEncoder;
12 import org.apache.lucene.util.encoding.IntDecoder;
13 import org.apache.lucene.util.encoding.IntEncoder;
14 import org.apache.lucene.util.encoding.NOnesIntEncoder;
15 import org.apache.lucene.util.encoding.SortingIntEncoder;
16 import org.apache.lucene.util.encoding.UniqueValuesIntEncoder;
17 import org.apache.lucene.util.encoding.VInt8IntEncoder;
18
19 /**
20  * Licensed to the Apache Software Foundation (ASF) under one or more
21  * contributor license agreements.  See the NOTICE file distributed with
22  * this work for additional information regarding copyright ownership.
23  * The ASF licenses this file to You under the Apache License, Version 2.0
24  * (the "License"); you may not use this file except in compliance with
25  * the License.  You may obtain a copy of the License at
26  *
27  *     http://www.apache.org/licenses/LICENSE-2.0
28  *
29  * Unless required by applicable law or agreed to in writing, software
30  * distributed under the License is distributed on an "AS IS" BASIS,
31  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
32  * See the License for the specific language governing permissions and
33  * limitations under the License.
34  */
35
36 public class EncodingSpeed {
37
38   private static int[] data3630 = null;
39   private static int[] data9910 = null;
40   private static int[] data501871 = null;
41   private static int[] data10k = null;
42   private static String resultsFormat = "%-20s %10s %20d %26s %20d %26s";
43   private static String headerFormat = "%-20s %10s %20s %26s %20s %26s";
44   private static int integers = 100000000;
45
46   private static NumberFormat nf;
47
48   /**
49    * @param args
50    * @throws IOException
51    */
52   public static void main(String[] args) throws IOException {
53     testFacetIDs(data3630, 3630);
54     testFacetIDs(data9910, 9910);
55     testFacetIDs(data10k, 10000);
56     testFacetIDs(data501871, 501871);
57   }
58
59   private static void testFacetIDs(int[] facetIDs, int docID)
60       throws IOException {
61     int loopFactor = integers / facetIDs.length;
62     System.out
63         .println("\nEstimating ~"
64             + integers
65             + " Integers compression time by\nEncoding/decoding facets' ID payload of docID = "
66             + docID + " (unsorted, length of: " + facetIDs.length
67             + ") " + loopFactor + " times.");
68
69     System.out.println();
70     String header = String.format(headerFormat, "Encoder", "Bits/Int",
71         "Encode Time", "Encode Time", "Decode Time", "Decode Time");
72
73     System.out.println(header);
74     String header2 = String.format(headerFormat, "", "", "[milliseconds]",
75         "[microsecond / int]", "[milliseconds]", "[microsecond / int]");
76
77     System.out.println(header2);
78
79     char[] separator = header.toCharArray();
80     Arrays.fill(separator, '-');
81     System.out.println(separator);
82
83     encoderTest(new VInt8IntEncoder(), facetIDs, loopFactor);
84     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new VInt8IntEncoder())), facetIDs, loopFactor);
85     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new DGapIntEncoder(new VInt8IntEncoder()))), facetIDs, loopFactor);
86     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new DGapIntEncoder(new EightFlagsIntEncoder()))), facetIDs, loopFactor);
87     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new DGapIntEncoder(new FourFlagsIntEncoder()))), facetIDs, loopFactor);
88     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new DGapIntEncoder(new NOnesIntEncoder(3)))), facetIDs, loopFactor);
89     encoderTest(new SortingIntEncoder(new UniqueValuesIntEncoder(new DGapIntEncoder(new NOnesIntEncoder(4)))), facetIDs, loopFactor);
90
91     System.out.println();
92   }
93
94   private static void encoderTest(IntEncoder encoder, int[] data,
95       int loopFactor) throws IOException {
96
97     long startTime, endTime;
98     ByteArrayOutputStream baos = new ByteArrayOutputStream();
99
100     // -- Looping 100 times as a warm up --------------------------
101     for (int i = 100; i != 0; --i) {
102       baos.reset();
103       encoder.reInit(baos);
104       for (int value : data) {
105         encoder.encode(value);
106       }
107       encoder.close();
108     }
109     // -----------------------------------------------------------
110
111     startTime = System.currentTimeMillis();
112     for (int factor = loopFactor; factor > 0; --factor) {
113       baos.reset();
114       encoder.reInit(baos);
115       for (int value : data) {
116         encoder.encode(value);
117       }
118       encoder.close();
119     }
120     endTime = System.currentTimeMillis();
121
122     long encodeTime = endTime - startTime;
123
124     ByteArrayInputStream bais = new ByteArrayInputStream(baos.toByteArray());
125     IntDecoder decoder = encoder.createMatchingDecoder();
126     decoder.reInit(bais);
127     
128     // -- Looping 100 times as a warm up --------------------------
129     for (int i = 100; i != 0; --i) {
130       bais.mark(baos.size());
131       while (decoder.decode() != IntDecoder.EOS) {
132       }
133       bais.reset();
134       decoder.reInit(bais);
135     }
136     // -----------------------------------------------------------
137
138     decoder.reInit(bais);
139     startTime = System.currentTimeMillis();
140     for (int i = loopFactor; i > 0; --i) {
141       bais.mark(baos.size());
142       while (decoder.decode() != IntDecoder.EOS) {
143       }
144       bais.reset();
145       decoder.reInit(bais);
146     }
147
148     endTime = System.currentTimeMillis();
149     long decodeTime = endTime - startTime;
150
151     System.out.println(String.format(resultsFormat, encoder, nf.format(baos
152         .size()
153         * 8.0 / data.length), encodeTime, nf.format(encodeTime
154         * 1000000.0 / (loopFactor * data.length)), decodeTime, nf
155         .format(decodeTime * 1000000.0 / (loopFactor * data.length))));
156   }
157
158   static {
159     nf = NumberFormat.getInstance();
160     nf.setMaximumFractionDigits(4);
161     nf.setMinimumFractionDigits(4);
162
163     data9910 = new int[] { 2, 4, 149085, 11, 12292, 69060, 69061, 149309,
164         99090, 568, 5395, 149310, 3911, 149311, 149312, 148752, 1408,
165         1410, 1411, 1412, 4807, 1413, 1414, 1417, 1415, 1416, 1418,
166         1420, 470, 4808, 1422, 1423, 1424, 4809, 4810, 1427, 1429,
167         1430, 4811, 1432, 1433, 3752, 1435, 3753, 1437, 1439, 1440,
168         4812, 1442, 1443, 4813, 1445, 1446, 1447, 4814, 4815, 1450,
169         4816, 353, 1452, 89004, 1624, 1625, 2052, 1626, 1627, 63991,
170         725, 726, 727, 728, 35543, 729, 730, 731, 1633, 733, 734, 735,
171         37954, 737, 738, 76315, 23068, 76316, 1634, 740, 741, 742, 744,
172         745, 76317, 15645, 748, 17488, 2904, 89005, 752, 753, 89006,
173         754, 755, 756, 757, 41, 261, 758, 89007, 760, 762, 763, 89008,
174         764, 765, 766, 85930, 165, 768, 149313, 33593, 149314, 149315,
175         81589, 39456, 15467, 1296, 149316, 39457, 2235, 144, 2236,
176         2309, 3050, 2237, 2311, 89692, 2240, 2241, 2243, 2244, 2245,
177         2246, 2314, 12856, 2248, 2250, 2251, 2253, 2254, 12857, 7677,
178         12858, 39149, 2257, 23147, 3303, 2258, 7422, 2322, 2262, 2317,
179         2263, 7423, 24264, 2232, 89693, 12862, 89694, 12863, 12864,
180         23201, 2329, 33019, 2255, 12865, 3517, 2492, 2277, 2280, 2267,
181         2260, 25368, 12866, 2281, 2282, 2283, 12867, 2284, 9055, 2287,
182         125133, 2337, 2286, 2288, 2338, 125134, 2290, 125135, 12869,
183         965, 966, 1298, 17945, 1300, 970, 971, 972, 973, 974, 296,
184         17946, 1303, 1391, 902, 1304, 1395, 1308, 1309, 1310, 1312,
185         967, 9414, 1315, 1317, 1318, 9415, 1321, 23592, 1322, 22433,
186         1323, 1324, 1326, 109241, 31225, 1330, 1331, 2540, 27196, 1332,
187         1334, 1335, 11999, 414, 340, 3651, 44040, 31995, 1344, 1343,
188         4618, 116770, 116771, 1474, 1349, 42122, 14199, 149317, 451,
189         149318, 29, 14200, 14198, 14201, 1979, 1980, 1981, 3132, 3147,
190         34090, 1987, 12770, 1329, 80818, 80819, 1988, 23522, 1986,
191         15880, 1985, 32975, 1992, 1993, 7165, 3141, 3143, 86346, 1982,
192         1984, 3145, 86347, 78064, 23456, 29578, 3136, 17752, 4710,
193         4711, 4712, 149319, 424, 4713, 95735, 4715, 149320, 4717, 4718,
194         149321, 192, 149322, 108126, 29976, 5404, 38059, 5406, 2030,
195         289, 1804, 1557, 1558, 94080, 29651, 94317, 1561, 1562, 1563,
196         1565, 24632, 1927, 1928, 1566, 1570, 1571, 1572, 1573, 1574,
197         1575, 94318, 1576, 2674, 9351, 94319, 94320, 2677, 2678, 29654,
198         2946, 2945, 2682, 2683, 2947, 3102, 3402, 3104, 4780, 3106,
199         3107, 3108, 3109, 3110, 3111, 3112, 3113, 3114, 3116, 3117,
200         3118, 19610, 44805, 3119, 3407, 3121, 3122, 3124, 3126, 3127,
201         41745, 41746, 3130, 459, 460, 461, 462, 463, 464, 466, 467,
202         40306, 468, 471, 472, 40307, 4467, 475, 476, 477, 478, 479,
203         40308, 481, 482, 20129, 483, 484, 485, 486, 4473, 488, 489,
204         458, 491, 40309, 494, 495, 496, 497, 499, 500, 501, 502, 355,
205         356, 1549, 358, 359, 360, 37971, 362, 2579, 2581, 24578, 2583,
206         24579, 2586, 2587, 2588, 2590, 2591, 24580, 24581, 3666, 24582,
207         2594, 24583, 2596, 2597, 24584, 2599, 18013, 24585, 2601,
208         49361, 280, 3969, 11651, 11652, 3926, 5103, 11653, 11654,
209         11655, 6896, 417, 168, 149323, 11268, 11657, 38089, 59517,
210         149324, 38092, 149325, 5110, 38094, 59520, 38096, 38097, 28916,
211         59703, 4992, 149326, 32383, 2478, 3985, 2479, 2480, 2481, 2482,
212         2483, 2484, 2485, 2486, 24146, 22184, 2488, 2489, 2490, 2494,
213         2493, 18043, 2495, 2542, 2497, 5062, 2499, 2501, 24147, 24148,
214         2504, 2505, 2506, 2507, 2508, 394, 2660, 2509, 2511, 24149,
215         2512, 2513, 2514, 3988, 4410, 3989, 2518, 2522, 2521, 24150,
216         12082, 2524, 3990, 24151, 387, 24152, 2529, 2530, 2528, 3991,
217         24153, 2534, 24154, 2536, 24155, 2538, 22510, 6332, 3554, 5309,
218         7700, 6333, 6334, 6335, 6336, 6337, 5693, 117020, 6339, 149327,
219         149328, 149329, 6340, 6343, 117022, 4324, 283, 284, 285, 286,
220         2688, 287, 2689, 288, 8880, 290, 291, 2690, 292, 295, 294,
221         24543, 13899, 297, 298, 299, 300, 303, 301, 59178, 302, 8881,
222         34403, 13900, 17811, 305, 307, 306, 308, 2727, 368, 364,
223         110416, 1587, 366, 367, 2692, 26624, 7233, 9082, 35684, 7250,
224         13902, 304, 13903, 991, 110417, 273, 274, 275, 276, 277, 278,
225         41095, 281, 282, 4419, 2768, 229, 230, 231, 232, 233, 234, 235,
226         236, 237, 1065, 239, 2745, 2746, 240, 9250, 241, 242, 244, 245,
227         9251, 246, 247, 248, 249, 250, 251, 253, 254, 255, 9252, 257,
228         258, 259, 9253, 9254, 2751, 265, 266, 267, 268, 9255, 9256,
229         270, 271, 9257, 238, 1024, 829, 1025, 1026, 1028, 1029, 1030,
230         9258, 1032, 1033, 1034, 1027, 1035, 1036, 9259, 1037, 1038,
231         1039, 4594, 4429, 1041, 1042, 1043, 70332, 1045, 1046, 1047,
232         1048, 21128, 1050, 122787, 72433, 1052, 2762, 1054, 1055, 1056,
233         9548, 1057, 71311, 1058, 1059, 1060, 61413, 2765, 4436, 1064,
234         1066, 11610, 3485, 22357, 104580, 149330, 149331, 15471, 5679,
235         5680, 687, 5683, 5684, 953, 8849, 102120, 149332, 5688, 5689,
236         149333, 6920, 60202, 33855, 33856, 33857, 19163, 33858, 3491,
237         149334, 914, 2202, 916, 917, 919, 920, 921, 922, 3568, 924,
238         925, 926, 927, 928, 929, 8752, 931, 932, 933, 934, 3570, 1876,
239         9138, 1877, 1878, 2210, 1880, 1881, 3571, 1883, 1884, 2212,
240         1886, 2214, 1888, 1889, 1890, 8753, 1891, 1892, 1893, 1894,
241         1895, 1896, 1898, 2217, 3572, 1901, 1902, 688, 2219, 107, 1904,
242         1905, 3573, 1907, 3323, 1909, 1910, 1911, 8754, 1912, 55911,
243         1913, 1914, 3574, 1741, 3575, 1916, 2226, 3576, 1919, 2227,
244         1920, 3577, 3578, 2229, 1923, 85396, 174, 175, 114875, 178,
245         180, 181, 182, 1477, 185, 186, 172, 187, 188, 85397, 85398,
246         190, 191, 891, 893, 19778, 18068, 895, 897, 896, 25985, 894,
247         900, 361, 1206, 193, 194, 195, 196, 197, 198, 199, 200, 55009,
248         201, 33266, 29064, 204, 205, 40129, 206, 207, 208, 2842, 209,
249         210, 211, 212, 149335, 870, 871, 18005, 872, 18006, 874, 875,
250         876, 1479, 1480, 1481, 879, 881, 57212, 2779, 57213, 886, 887,
251         57214, 57215, 889, 890, 806, 69305, 808, 809, 86327, 812, 813,
252         814, 815, 26724, 816, 69307, 43484, 818, 819, 63904, 820, 821,
253         822, 86328, 13498, 824, 825, 12218, 149336, 49042, 4464, 4466,
254         35536, 73245, 73246, 474, 73247, 480, 46247, 29624, 21086,
255         73248, 490, 493, 73249, 73250, 401, 403, 405, 2860, 15483,
256         74826, 408, 409, 74827, 410, 411, 413, 74828, 415, 2863, 68707,
257         33284, 2865, 2866, 2867, 2868, 2869, 2870, 17976, 3032, 38498,
258         7350, 2876, 2874, 24506, 918, 923, 64562, 64563, 32648, 930,
259         1875, 32649, 1879, 32650, 1882, 1887, 32651, 64564, 32652,
260         1897, 32653, 18170, 1900, 32654, 1906, 1915, 64565, 1921, 1922,
261         90662, 2234, 37449, 8886, 37450, 7418, 37451, 37452, 37453,
262         37454, 1609, 1610, 1611, 1612, 113456, 1212, 1616, 1617,
263         113457, 1615, 1619, 113458, 1620, 8747, 113459, 8748, 42233,
264         78065, 42235, 2149, 42236, 78066, 42237, 42238, 4335, 42239,
265         78067, 42241, 78068, 42243, 78069, 42244, 78070, 54587, 12993,
266         2040, 1130, 1131, 51172, 1133, 1134, 1135, 1136, 1137, 1138,
267         1139, 1140, 1141, 149337, 1115, 5178, 149338, 452, 7784, 21522,
268         1361, 103718, 149339, 15990, 79432, 149340, 4232, 149341,
269         15998, 53917, 15996, 53918, 149342, 149343, 97544, 53920,
270         97546, 841, 1954, 842, 41926, 844, 2589, 845, 846, 27370, 848,
271         849, 41927, 25165, 852, 1956, 854, 856, 1957, 855, 1959, 35170,
272         23055, 75673, 116783, 857, 116784, 851, 116785, 858, 859, 860,
273         861, 57422, 1964, 864, 866, 867, 1965, 1966, 1968, 1969, 2989,
274         116786, 1972, 1973, 116787, 1975, 1976, 1977, 2580, 39540,
275         2585, 39541, 21755, 39542, 2592, 34859, 2593, 39543, 38540,
276         2595, 39544, 149344, 35433, 81849, 35434, 40257, 873, 877,
277         2778, 32040, 882, 883, 884, 885, 888, 3358, 1559, 1560, 1438,
278         25387, 1569, 38135, 66925, 2673, 3095, 2679, 59053, 25443,
279         34369, 1983, 17749, 9343, 1989, 13565, 31525, 61690, 18165,
280         17751, 78234, 26506, 9348, 20307, 18154, 3133, 2572, 3134,
281         12131, 19770, 48724, 25759, 13549, 65465, 19936, 13545, 25645,
282         4786, 15756, 19547, 1581, 92226, 1362, 21524, 13059, 23717,
283         149345, 20198, 27123, 149346, 149347, 26030, 27126, 27652,
284         10538, 1667, 40282, 14134, 40284, 16368, 149348, 40287, 8870,
285         40288, 149349, 40289, 149350, 149351, 40295, 10424, 7012,
286         13178, 45608, 10423, 13181, 4201, 672, 13182, 10174, 10607,
287         13183, 580, 149352, 149353, 96298, 53691, 3721, 66048, 21584,
288         149354, 48206, 48207, 149355, 1405, 1406, 1407, 11162, 577,
289         149356, 6941, 6942, 16583, 1284, 10511, 16584, 16585, 422, 423,
290         1249, 1244, 1245, 1247, 2544, 1248, 1250, 2545, 1252, 2547,
291         1253, 2549, 1259, 1257, 1258, 1260, 1261, 2551, 1262, 1263,
292         1264, 1265, 2553, 1266, 17795, 2554, 17796, 1270, 1271, 1273,
293         17797, 2556, 1275, 1276, 2557, 1277, 1278, 1279, 1280, 1282,
294         68, 69, 5080, 5256, 6869, 10148, 6960, 10150, 149357, 10152,
295         14413, 149358, 14414, 56037, 651, 56038, 131797, 555, 14415,
296         14416, 149359, 149360, 56042, 14418, 149361, 149, 56043, 97512,
297         34512, 797, 7396, 9395, 9396, 9397, 63417, 805, 23984, 13665,
298         10452, 55147, 5656, 53, 4348, 4349, 4350, 148488, 13669, 6527,
299         149362, 11374, 11376, 11377, 8092, 11378, 11380, 152, 5013,
300         8093, 561, 11381, 5623, 4176, 26840, 3564, 3565, 3708, 3567,
301         18783, 18784, 4039, 10540, 18786, 30100, 30101, 1528, 149363,
302         19561, 19562, 19563, 19564, 1110, 134146, 10600, 149364, 10602,
303         149365, 149366, 10603, 10604, 4981, 57075, 37508, 149367,
304         34589, 1209, 149368, 19592, 19593, 7620, 9674, 3481, 10240,
305         81835, 8001, 33872, 8907, 55155, 1585, 31731, 49694, 25760,
306         31733, 903, 904, 2539, 49695, 1194, 1195, 1196, 31734, 1197,
307         1198, 1199, 1593, 899, 1200, 1201, 9276, 1202, 40181, 40482,
308         55718, 80833, 24596, 3669, 15699, 55720, 55721, 40481, 3672,
309         39826, 80363, 2602, 2603, 2604, 62126, 2605, 2606, 2607, 8714,
310         2608, 2609, 2610, 2612, 149369, 2894, 15241, 15242, 15262,
311         5384, 20290, 20291, 7792, 20295, 64413, 39236, 18011, 71494,
312         898, 51015, 19782, 105107, 149370, 7634, 149371, 149372,
313         115458, 22821, 19894, 2213, 66926 };
314
315     data3630 = new int[] { 2, 4, 86133, 11, 16505, 86134, 86135, 86136,
316         1290, 86137, 86138, 32473, 19346, 32474, 4922, 32475, 86139,
317         16914, 86140, 86141, 86142, 86143, 32478, 86144, 86145, 32480,
318         4884, 4887, 32481, 86146, 16572, 86147, 16295, 165, 86148,
319         3183, 21920, 21921, 21922, 555, 4006, 32484, 21925, 21926,
320         13775, 86149, 13777, 85833, 85834, 13779, 13773, 13780, 75266,
321         17674, 13784, 13785, 13786, 13787, 13788, 6258, 86150, 13790,
322         75267, 13793, 13794, 13795, 312, 4914, 4915, 6222, 86151, 4845,
323         4883, 4918, 4894, 4919, 86152, 4921, 6223, 6224, 6225, 6226,
324         67909, 6229, 18170, 6230, 5198, 25625, 6231, 6232, 6233, 1808,
325         6234, 6235, 6236, 41376, 6238, 6239, 67911, 6240, 86153, 6243,
326         6244, 83549, 6246, 6247, 6248, 6249, 782, 444, 6251, 6250,
327         19863, 28963, 310, 2234, 144, 2236, 2309, 69437, 2311, 2325,
328         2241, 69438, 69439, 2244, 2245, 2246, 23504, 2314, 69440,
329         36603, 2250, 2268, 2271, 2251, 2254, 2255, 2257, 2240, 36604,
330         84726, 36605, 84727, 2262, 2263, 18431, 38853, 2317, 2149,
331         2326, 2327, 2329, 3980, 2275, 2277, 2258, 84728, 2260, 84729,
332         84730, 13766, 36607, 2282, 2283, 84731, 2284, 2286, 2287, 2337,
333         7424, 2288, 2338, 3522, 2290, 84733, 32902, 371, 37708, 2096,
334         3065, 3066, 375, 377, 374, 378, 2100, 86154, 381, 382, 58795,
335         379, 383, 384, 385, 4449, 387, 388, 389, 390, 9052, 391, 18358,
336         2107, 394, 2111, 2108, 393, 2109, 395, 86155, 86156, 397, 2113,
337         398, 399, 400, 273, 274, 275, 40980, 276, 277, 31716, 279, 280,
338         31717, 281, 282, 1628, 1623, 1624, 1625, 2052, 1626, 725, 727,
339         728, 729, 730, 731, 1633, 733, 734, 735, 86157, 737, 738, 739,
340         1634, 3563, 3564, 3565, 1667, 12461, 76276, 3567, 5413, 77622,
341         5415, 5416, 5417, 5418, 107, 86158, 7784, 15363, 153, 3723,
342         2713, 7786, 3835, 7787, 86159, 7789, 7791, 7792, 7794, 86160,
343         7796, 86161, 6708, 7798, 7799, 7800, 7801, 7802, 7803, 1665,
344         43150, 15365, 1581, 5656, 43152, 80258, 7450, 39922, 86162,
345         51587, 9059, 4606, 396, 86163, 86164, 7250, 401, 403, 2860,
346         33281, 2964, 408, 9119, 409, 86165, 7669, 2861, 410, 413,
347         86166, 414, 415, 33282, 405, 33283, 7498, 2865, 7230, 33284,
348         2866, 86167, 2867, 47518, 2868, 86168, 2869, 2870, 4712, 7096,
349         28484, 6913, 6914, 6915, 6916, 37169, 37170, 7103, 28269, 6919,
350         86169, 45431, 6922, 7104, 6923, 7108, 6924, 6925, 6926, 6927,
351         6928, 86170, 86171, 86172, 6930, 6931, 6932, 6934, 6935, 6936,
352         451, 6937, 6938, 4756, 3554, 5309, 8145, 3586, 16417, 9767,
353         14126, 25854, 6580, 10174, 86173, 5519, 21309, 8561, 20938,
354         10386, 86174, 781, 2030, 16419, 30323, 16420, 16421, 16424,
355         86175, 86176, 86177, 28871, 86178, 28872, 63980, 6329, 49561,
356         4271, 38778, 86179, 86180, 20126, 16245, 193, 195, 196, 197,
357         56973, 199, 200, 201, 202, 203, 204, 56974, 56975, 205, 206,
358         4662, 207, 208, 209, 210, 211, 212, 47901, 641, 642, 643, 1380,
359         1079, 47902, 1381, 1081, 1082, 1083, 47903, 1382, 47904, 1087,
360         47905, 965, 966, 1298, 968, 1387, 1300, 50288, 971, 972, 973,
361         974, 23974, 22183, 1390, 23313, 1389, 1391, 902, 23029, 296,
362         1304, 1395, 1303, 1309, 1308, 50289, 1312, 50290, 50291, 1315,
363         1317, 9270, 19796, 3605, 1320, 1321, 44946, 1322, 1323, 50292,
364         967, 1587, 1326, 1331, 17482, 633, 29115, 53858, 29118, 29119,
365         62624, 44494, 6965, 6966, 6959, 6967, 71562, 6969, 23459,
366         23460, 17464, 4225, 23461, 23462, 23463, 5893, 23464, 17467,
367         17468, 23465, 12562, 1405, 1406, 1407, 960, 961, 962, 687, 963,
368         86181, 86182, 5997, 10812, 11976, 11977, 1850, 577, 13393,
369         10810, 13394, 65040, 86183, 3935, 3936, 3937, 710, 86184, 5785,
370         5786, 29949, 5787, 5788, 283, 284, 2687, 285, 286, 287, 2689,
371         288, 289, 8880, 290, 2690, 13899, 991, 292, 295, 42007, 35616,
372         63103, 298, 299, 3520, 297, 9024, 303, 301, 302, 300, 31345,
373         3719, 304, 305, 306, 307, 308, 368, 364, 85002, 9026, 63105,
374         367, 39596, 25835, 19746, 293, 294, 26505, 85003, 18377, 56785,
375         10122, 10123, 10124, 86185, 39863, 86186, 10125, 39865, 4066,
376         4067, 24257, 4068, 4070, 86187, 4073, 4074, 86188, 4076, 7538,
377         4077, 86189, 4078, 4079, 7540, 7541, 4084, 4085, 7542, 86190,
378         4086, 86191, 4087, 4088, 86192, 7545, 44874, 7821, 44875,
379         86193, 4286, 86194, 51470, 17609, 1408, 47486, 1411, 1412,
380         47487, 1413, 1414, 1417, 1415, 47488, 1416, 1418, 1420, 470,
381         1422, 1423, 1424, 5001, 5002, 47489, 1427, 1429, 1430, 31811,
382         1432, 1433, 47490, 1435, 3753, 1437, 1439, 1440, 47491, 1443,
383         47492, 1446, 5004, 5005, 1450, 47493, 353, 1452, 42145, 3103,
384         3402, 3104, 3105, 4780, 3106, 3107, 3108, 12157, 3111, 42146,
385         42147, 3114, 4782, 42148, 3116, 3117, 42149, 42150, 3407, 3121,
386         3122, 18154, 3126, 3127, 3128, 3410, 3130, 3411, 3412, 3415,
387         24241, 3417, 3418, 3449, 42151, 3421, 3422, 7587, 42152, 3424,
388         3427, 3428, 3448, 3430, 3432, 42153, 42154, 41648, 1991, 407,
389         57234, 411, 2862, 57235, 2863, 18368, 57236, 2874, 7350, 4115,
390         2876, 2877, 17975, 86195, 4116, 2881, 2882, 2883, 2886, 463,
391         870, 872, 873, 874, 875, 8783, 8784, 877, 1480, 1481, 459,
392         2778, 881, 8785, 2779, 8786, 8787, 8788, 886, 887, 8789, 889,
393         8790, 86196, 6920, 86197, 5080, 5081, 7395, 7396, 9395, 9396,
394         1528, 42737, 805, 86198, 1209, 13595, 4126, 9680, 34368, 9682,
395         86199, 86200, 174, 175, 176, 177, 178, 179, 180, 182, 183,
396         1477, 31138, 186, 172, 187, 188, 189, 190, 191, 458, 871,
397         31294, 31295, 27604, 31296, 31297, 882, 883, 884, 31298, 890,
398         1089, 1488, 1489, 1092, 1093, 1094, 1095, 1096, 1097, 1490,
399         1098, 1495, 1502, 1099, 1100, 1101, 1493, 2997, 12223, 1103,
400         2654, 1498, 1499, 1500, 80615, 80616, 80617, 33359, 86201,
401         9294, 1501, 86202, 1506, 1507, 23454, 38802, 38803, 1014,
402         86203, 5583, 5584, 651, 74717, 5586, 5587, 5588, 5589, 74720,
403         5590, 38808, 33527, 78330, 10930, 5119, 10931, 1000, 10928,
404         10932, 10933, 10934, 10935, 5863, 10936, 86204, 10938, 10939,
405         86205, 192, 194, 38754, 38755, 198, 38756, 38757, 38758, 2842,
406         640, 22780, 22781, 1080, 86206, 86207, 1084, 1086, 1088, 63916,
407         9412, 970, 9413, 9414, 9415, 9416, 9417, 1310, 7168, 7169,
408         1318, 9418, 1324, 39159, 1804, 1557, 24850, 41499, 1560, 41500,
409         1562, 1563, 1565, 1927, 1928, 1566, 1569, 1570, 1571, 1572,
410         1573, 1574, 1575, 1576, 2674, 2677, 2678, 2679, 2946, 2682,
411         2676, 2683, 2947, 1156, 1157, 1158, 1467, 1160, 1468, 1469,
412         1161, 1162, 1163, 4369, 1165, 1166, 1167, 12923, 2917, 1169,
413         1170, 1171, 1172, 1173, 1174, 1175, 1176, 1177, 18153, 8359,
414         1178, 1164, 1191, 1180, 12924, 86208, 86209, 54817, 66962,
415         2476, 86210, 86211, 41820, 41821, 41822, 41824, 1130, 1131,
416         1132, 32692, 1134, 34848, 1136, 1133, 1137, 1138, 1139, 1140,
417         1141, 1143, 1144, 1145, 34849, 2639, 34850, 1146, 1147, 1148,
418         34851, 1150, 1151, 1152, 1153, 1154, 1155, 1678, 1679, 1680,
419         1681, 40870, 2059, 1685, 1686, 32686, 14970, 1688, 1689, 86212,
420         1692, 1682, 1693, 1695, 1696, 1698, 12955, 8909, 41690, 1700,
421         41691, 86213, 30949, 41692, 1703, 1704, 1705, 41693, 14976,
422         1708, 2071, 1709, 1710, 1711, 1712, 1727, 86214, 86215, 86216,
423         1715, 86217, 1714, 1717, 1690, 41697, 86218, 1720, 86219, 2073,
424         41699, 1724, 2075, 1726, 1729, 1730, 1732, 2078, 2223, 1735,
425         1713, 41700, 1737, 14977, 1739, 1740, 1741, 2080, 1743, 1744,
426         1745, 1746, 1747, 1748, 1749, 1750, 1751, 41701, 1752, 1753,
427         1909, 86220, 2085, 1754, 19548, 86221, 19551, 5733, 3856, 5190,
428         4581, 25145, 86222, 86223, 4846, 86224, 4861, 86225, 86226,
429         86227, 25150, 86228, 86229, 13820, 2027, 4898, 4899, 4901,
430         2135, 4902, 4868, 4904, 86230, 4905, 25155, 4907, 86231, 4909,
431         4910, 4911, 4912, 86232, 6220, 81357, 86233, 2589, 73877,
432         29706, 6227, 6228, 86234, 6237, 86235, 6241, 6242, 1812, 13808,
433         13809, 70908, 2293, 2294, 86236, 2295, 2296, 2297, 22947,
434         16511, 2299, 2300, 2301, 13097, 73079, 86237, 13099, 50121,
435         86238, 86239, 13101, 86240, 2424, 4725, 4726, 4727, 4728, 4729,
436         4730, 86241, 26881, 10944, 4734, 4735, 4736, 26239, 26240,
437         71408, 86242, 57401, 71410, 26244, 5344, 26245, 86243, 4102,
438         71414, 11091, 6736, 86244, 6737, 6738, 38152, 6740, 6741, 6742,
439         6298, 6743, 6745, 6746, 20867, 6749, 20616, 86245, 9801, 65297,
440         20617, 65298, 20619, 5629, 65299, 20621, 20622, 8385, 20623,
441         20624, 5191, 20625, 20626, 442, 443, 445, 27837, 77681, 86246,
442         27839, 86247, 86248, 41435, 66511, 2478, 2479, 2480, 2481,
443         2482, 2483, 2484, 2485, 2486, 2487, 2488, 2489, 2490, 2494,
444         2493, 33025, 12084, 2542, 2497, 2499, 2501, 2503, 2504, 2505,
445         33026, 2506, 2507, 2508, 2509, 2511, 1787, 12080, 2513, 2514,
446         3988, 3176, 3989, 2518, 2521, 9285, 2522, 2524, 2525, 3990,
447         2527, 2528, 27499, 2529, 2530, 3991, 2532, 2534, 2535, 18038,
448         2536, 2538, 2495, 46077, 61493, 61494, 1006, 713, 4971, 4972,
449         4973, 4975, 4976, 650, 170, 7549, 7550, 7551, 7552, 7553,
450         86249, 7936, 956, 11169, 11170, 1249, 1244, 1245, 1247, 2544,
451         1250, 2545, 1252, 2547, 1253, 1254, 2549, 39636, 1259, 1257,
452         1258, 39637, 1260, 1261, 2551, 1262, 1263, 848, 86250, 86251,
453         854, 74596, 856, 1957, 86252, 855, 1959, 1961, 857, 86253, 851,
454         859, 860, 862, 1964, 864, 865, 866, 867, 1965, 1966, 1967,
455         1968, 1969, 86254, 1971, 1972, 1973, 1974, 1975, 1976, 1977,
456         841, 1954, 842, 2978, 846, 847, 849, 850, 852, 1956, 17452,
457         71941, 86255, 86256, 73665, 1471, 13690, 185, 503, 504, 2342,
458         505, 506, 4378, 508, 4379, 17313, 510, 511, 512, 520, 513,
459         4384, 17314, 514, 515, 46158, 17317, 518, 34269, 519, 4386,
460         523, 524, 525, 46159, 528, 529, 17319, 531, 532, 533, 534, 535,
461         7482, 537, 538, 5267, 536, 539, 541, 540, 19858, 17320, 17321,
462         906, 907, 908, 17322, 910, 17323, 912, 15850, 913, 4398, 17324,
463         86257, 278, 2948, 2949, 2950, 3007, 2951, 2952, 2953, 2954,
464         2955, 3013, 35352, 3014, 3015, 2962, 3016, 33505, 39118, 3017,
465         3018, 20492, 4000, 3021, 3022, 35353, 39293, 3024, 18443, 3029,
466         9467, 20529, 39119, 8380, 2965, 3030, 3043, 22714, 39120, 2956,
467         3035, 39121, 3037, 3038, 2688, 86258, 36675, 30894, 24505,
468         8888, 13541, 49728, 27660, 9082, 27661, 365, 366, 2232, 76098,
469         7233, 1494, 17391, 606, 607, 611, 610, 612, 614, 615, 613, 616,
470         9117, 617, 618, 21155, 1789, 619, 620, 7636, 12019, 621, 622,
471         1793, 623, 625, 624, 631, 626, 627, 21578, 21103, 628, 21579,
472         629, 9122, 9123, 12189, 9289, 3168, 3169, 630, 632, 634, 21580,
473         9121, 635, 636, 637, 21581, 12781, 1801, 638, 639, 1559, 24343,
474         9419, 9420, 795, 796, 1611, 86259, 1612, 21551, 21552, 3741,
475         1617, 3742, 1615, 1619, 1620, 6301, 3744, 1622, 67685, 8521,
476         55937, 9025, 27663, 8881, 13581, 86260, 11592, 44720, 86261,
477         63231, 50873, 42925, 52332, 86262, 72706, 17705, 17707, 17708,
478         3401, 40217, 1248, 40218, 86263, 7098, 86264, 86265, 1264,
479         86266, 1266, 1267, 1268, 1269, 86267, 1271, 1272, 1273, 1274,
480         2556, 1275, 1276, 1277, 1278, 1279, 1280, 1282, 1283, 22680,
481         11889, 86268, 45662, 7038, 86269, 19315, 45663, 45664, 86270,
482         5855, 34002, 49245, 10447, 5663, 86271, 15429, 53877, 49249,
483         86272, 86273, 86274, 60128, 60453, 60129, 5552, 31923, 43407,
484         4287, 17980, 64977, 86275, 86276, 8234, 86277, 3649, 8240,
485         1330, 11999, 1332, 27618, 1334, 1335, 340, 3651, 25640, 18165,
486         1343, 4618, 1474, 3653, 75921, 1349, 53519, 1779, 45454, 22778,
487         40153, 67677, 63826, 45455, 15128, 67678, 67679, 1792, 67680,
488         3171, 47816, 45457, 9288, 59891, 67681, 25703, 35731, 35732,
489         369, 35713, 35714, 35715, 34652, 35716, 31681, 35717, 12779,
490         35718, 35719, 11992, 806, 807, 808, 43499, 43500, 810, 776,
491         812, 813, 814, 241, 43501, 43502, 816, 755, 43503, 818, 819,
492         820, 43504, 821, 822, 823, 824, 825, 826, 43505, 43506, 43507,
493         828, 829, 20083, 43508, 43509, 832, 833, 834, 835, 86278,
494         19984, 19985, 86279, 24125, 19986, 86280, 19988, 86281, 5414,
495         86282, 85808, 5479, 5420, 5421, 5422, 5423, 63800, 86283,
496         86284, 30965, 86285, 416, 1510, 5740, 5741, 81991, 86286,
497         28938, 50149, 1003, 55512, 14306, 6960, 688, 86287, 14307,
498         5399, 5400, 17783, 24118, 720, 86288, 44913, 24557, 667, 24876,
499         6529, 24877, 24878, 24879, 24880, 31847, 20671, 4011, 171, 580,
500         86289, 3863, 914, 2202, 916, 917, 918, 919, 921, 922, 923,
501         7585, 925, 7586, 926, 927, 928, 7588, 929, 930, 931, 932, 933,
502         934, 1875, 1876, 7589, 7590, 1878, 1879, 7591, 7592, 1882,
503         1883, 1884, 2212, 7593, 1887, 1888, 1889, 1890, 1891, 1892,
504         1893, 1894, 1895, 1896, 1897, 1898, 2217, 1900, 7594, 1902,
505         2219, 7595, 1905, 1906, 1907, 3323, 7596, 1911, 1912, 7597,
506         1914, 1915, 1916, 2226, 1919, 7598, 2227, 1920, 1921, 7599,
507         7600, 4708, 1923, 355, 356, 1549, 358, 32077, 360, 32078,
508         21117, 362, 19043, 71677, 5716, 86290, 49790, 86291, 86292,
509         86293, 49792, 86294, 86295, 49794, 86296, 86297, 86298, 86299,
510         11882, 86300, 49798, 86301, 49800, 49801, 49802, 49803, 453,
511         49804, 8591, 6794, 49806, 18989, 49807, 49808, 16308, 49809,
512         86302, 86303, 10105, 86304, 5285, 10106, 10107, 6557, 86305,
513         23571, 10109, 38883, 10110, 5401, 86306, 67557, 16430, 67558,
514         40171, 16433, 25878, 86307, 21762, 23, 86308, 86309, 21766,
515         86310, 86311, 5149, 3926, 21768, 21769, 47826, 942, 46985,
516         6588, 58867, 6589, 6590, 86312, 6592, 6006, 53855, 9565, 359,
517         86313, 2845, 876, 879, 27556, 27557, 885, 27558, 888, 2847,
518         27559, 2115, 2116, 2117, 53962, 57839, 315, 316, 317, 318, 319,
519         86314, 321, 322, 2122, 323, 2123, 324, 325, 328, 326, 327,
520         40542, 329, 330, 18079, 18080, 331, 1790, 7382, 332, 7380,
521         7236, 23413, 23414, 18924, 18925, 333, 335, 336, 39750, 337,
522         86315, 339, 341, 342, 343, 16264, 16265, 6615, 86316, 86317,
523         86318, 86319, 16269, 10538, 33226, 86320, 16272, 5824, 16273,
524         16274, 16276, 16277, 16278, 16279, 16280, 14517, 1547, 6463,
525         3394, 49677, 659, 10380, 30013, 10382, 10378, 10379, 10383,
526         10384, 10385, 86321, 4139, 13370, 13371, 86322, 86323, 11878,
527         64509, 15141, 15142, 15143, 32737, 14183, 15144, 39101, 42768,
528         5645, 32738, 801, 803, 804, 86324, 14707, 86325, 6601, 12402,
529         712, 12403, 2936, 1447, 15477, 1410, 44872, 1550, 8614, 15478,
530         15479, 15480, 15481, 4811, 3752, 1442, 15482, 8818, 1445, 5006,
531         16304, 32277, 16305, 16306, 86326, 16307, 53691, 69305, 809,
532         86327, 815, 26724, 69307, 43484, 63904, 86328, 13498, 827,
533         86329, 831, 2857, 836, 86330, 86331, 837, 838, 839, 840, 228,
534         229, 43722, 230, 231, 43723, 234, 235, 236, 237, 238, 239,
535         2745, 2746, 240, 242, 243, 244, 43724, 19788, 246, 247, 21134,
536         248, 250, 251, 252, 253, 254, 255, 256, 257, 258, 43725, 43726,
537         41, 43727, 262, 43728, 2751, 264, 265, 266, 267, 268, 269, 270,
538         271, 272, 1024, 1025, 1026, 1027, 1028, 1029, 1030, 1031, 1032,
539         1033, 1034, 43729, 1035, 43730, 1037, 21821, 2926, 14388,
540         10432, 14389, 14390, 14391, 14392, 86332, 14394, 14395, 2035,
541         2169, 86333, 14397, 14398, 14399, 14400, 52, 14401, 14402,
542         7077, 21822, 14405, 14406, 14396, 86334, 17356, 17357, 84679,
543         84680, 76383, 17360, 17361, 86335, 38801, 2060, 30850, 12963,
544         1684, 1687, 2061, 14978, 1694, 43387, 1697, 1699, 2067, 1701,
545         1702, 1706, 43388, 43389, 76325, 1716, 1718, 26832, 1719, 1723,
546         2081, 2063, 1728, 39059, 76326, 1731, 86336, 1736, 76327, 1738,
547         19657, 6579, 6581, 6582, 6583, 6584, 6585, 29979, 1818, 28239,
548         68, 69, 3391, 86337, 10266, 63528, 86338, 10269, 10270, 10271,
549         10272, 86339, 86340, 63530, 63531, 63532, 63533, 10273, 63534,
550         86341, 10681, 10682, 86342, 9673, 86343, 10683, 460, 461, 462,
551         467, 4464, 4466, 3729, 471, 472, 468, 81634, 474, 81635, 475,
552         476, 477, 479, 480, 81636, 81637, 482, 17442, 81638, 81639,
553         484, 485, 486, 4473, 488, 489, 490, 493, 466, 494, 495, 496,
554         497, 499, 500, 501, 502, 34376, 86344, 63836, 56281, 1707,
555         20416, 61452, 56282, 1755, 56283, 56284, 18508, 53650, 63444,
556         86345, 3579, 63445, 3677, 1979, 1980, 1981, 3132, 3147, 34090,
557         1987, 12770, 1329, 80818, 80819, 1988, 23522, 1986, 15880,
558         1985, 32975, 1992, 1993, 7165, 3141, 3143, 86346, 1982, 1984,
559         3145, 86347, 78064, 55453, 2656, 2657, 35634, 35635, 2167,
560         43479 };
561
562     data10k = new int[] { 2, 4, 149900, 11, 70236, 149901, 149902, 6721,
563         149929, 29212, 34600, 149930, 149931, 149932, 141696, 149908,
564         149909, 149910 };
565
566     data501871 = new int[] { 1368366, 1368367, 1817408, 11, 2513, 1817409,
567         1817410, 1817411, 1382349, 126700, 1817412, 5539, 21862, 21863,
568         21864, 1233, 1127, 121, 15254, 15255, 357, 449, 15256, 8817,
569         15257, 15258, 1406, 1096, 281, 4826, 4827, 223, 166, 2372, 168,
570         169, 2219, 170, 171, 1176, 172, 173, 2222, 3035, 177, 178, 179,
571         180, 181, 183, 3036, 2378, 1157, 1158, 2380, 1160, 1161, 1162,
572         2384, 1164, 1165, 1166, 1167, 1168, 2385, 3037, 1171, 1172,
573         1173, 2238, 1175, 1177, 1178, 1179, 1180, 1181, 2243, 3038,
574         1182, 2244, 1183, 1184, 1185, 1186, 1187, 1188, 1189, 1190,
575         59766, 471, 7349, 3599, 2847, 59767, 59768, 59769, 59770,
576         59771, 59772, 59773, 59774, 59775, 2625, 852, 853, 2632, 854,
577         855, 856, 2284, 857, 862, 1031, 859, 860, 861, 866, 1033, 867,
578         1035, 868, 870, 2294, 871, 2295, 873, 874, 875, 876, 877, 878,
579         879, 66632, 66633, 66634, 66635, 14823, 66636, 66637, 3763,
580         77345, 1370, 3764, 3765, 3766, 5666, 3768, 3770, 16892, 3771,
581         3772, 3773, 3244, 3246, 3247, 1504, 266, 29250, 24764, 29251,
582         689, 12844, 8068, 29252, 38918, 750, 751, 770, 3704, 753, 754,
583         765, 755, 3708, 757, 758, 759, 760, 3710, 761, 762, 763, 3712,
584         766, 767, 768, 769, 771, 3719, 4380, 3722, 3723, 3725, 4381,
585         3727, 3728, 3731, 3732, 764, 4382, 2316, 334, 1637, 4383, 4384,
586         4385, 4386, 4387, 184, 185, 1134, 186, 1135, 187, 188, 1138,
587         197, 191, 3517, 193, 194, 195, 196, 208, 3519, 198, 9210, 937,
588         9211, 9212, 916, 917, 117, 118, 919, 122, 921, 123, 124, 125,
589         126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 924, 137,
590         138, 139, 140, 141, 588, 928, 142, 143, 144, 929, 146, 147,
591         148, 149, 150, 151, 3775, 3776, 3777, 3778, 3780, 3781, 3783,
592         3784, 3785, 3796, 4169, 3788, 4170, 3790, 3791, 3793, 3803,
593         3794, 3797, 4171, 3799, 3800, 3801, 3802, 3804, 4172, 3806,
594         4173, 4174, 3811, 4175, 3813, 3829, 3815, 3816, 3817, 4176,
595         4177, 3820, 3821, 3822, 2168, 3039, 2460, 2170, 2459, 2174,
596         2175, 2176, 2461, 2462, 2463, 3040, 2466, 2467, 2469, 2468,
597         2470, 3041, 2472, 3042, 3043, 3044, 3045, 231, 881, 882, 1219,
598         884, 2038, 886, 887, 888, 891, 892, 1221, 894, 895, 1222, 2039,
599         899, 1225, 900, 901, 902, 2492, 2494, 2495, 2496, 4052, 2498,
600         2502, 2500, 2501, 2503, 2504, 4653, 5514, 18671, 10350, 1122,
601         44317, 44318, 44319, 44320, 44321, 44322, 44323, 44324, 7923,
602         1422, 10284, 10285, 6146, 9803, 10286, 466, 5998, 696, 3257,
603         6043, 6195, 6196, 6197, 6198, 6199, 6200, 6201, 7029, 4405,
604         4864, 450, 349, 11214, 3548, 1092, 5728, 7395, 6533, 1123,
605         5736, 1115, 6535, 6536, 2739, 2832, 2833, 2834, 2835, 2836,
606         23972, 2837, 23973, 2839, 2840, 2691, 1339, 20116, 3219, 8210,
607         3170, 3171, 3172, 3173, 2094, 2095, 2096, 2097, 2099, 2100,
608         2102, 3174, 2104, 1372, 2105, 2107, 2108, 2109, 2110, 2113,
609         2114, 2115, 2117, 2118, 3221, 3222, 2122, 2123, 2124, 4611,
610         2125, 2126, 2127, 2128, 2129, 2130, 2131, 575, 576, 2132, 4612,
611         2134, 2135, 2136, 4368, 5931, 5932, 5933, 5934, 5935, 5936,
612         5937, 5938, 5939, 2902, 4057, 4058, 4059, 4060, 4062, 4063,
613         4064, 4654, 4655, 4067, 4068, 4069, 4656, 4657, 4073, 4658,
614         4074, 4075, 4659, 4660, 4661, 4076, 4662, 4663, 4664, 4078,
615         4079, 4080, 4665, 4082, 4083, 4084, 4666, 4086, 4087, 4088,
616         544, 545, 546, 547, 548, 549, 550, 559, 1227, 552, 553, 5035,
617         555, 554, 1228, 556, 1229, 557, 558, 560, 561, 562, 563, 564,
618         565, 1230, 566, 567, 568, 569, 570, 572, 573, 222, 7461, 2059,
619         2060, 2061, 5664, 2062, 7463, 16997, 2065, 2066, 2067, 2068,
620         2069, 2070, 2072, 2073, 2074, 2075, 2076, 2077, 2078, 7464,
621         2079, 2080, 2081, 7465, 2082, 2083, 2084, 2085, 2086, 2087,
622         199, 206, 200, 203, 205, 211, 1140, 3699, 209, 214, 215, 216,
623         217, 218, 777, 778, 779, 780, 2298, 781, 782, 783, 784, 785,
624         787, 788, 384, 789, 790, 791, 2677, 793, 794, 795, 796, 797,
625         2307, 798, 799, 801, 802, 3645, 803, 4337, 805, 3648, 3649,
626         807, 808, 3651, 810, 812, 813, 814, 815, 816, 3654, 818, 819,
627         13780, 930, 932, 4221, 935, 936, 938, 2197, 939, 940, 941,
628         2200, 943, 1591, 1952, 2630, 1592, 2631, 1602, 1607, 1595,
629         1596, 1597, 1598, 1599, 1955, 1601, 1603, 1956, 1605, 1606,
630         1608, 1610, 1638, 20608, 968, 969, 970, 971, 972, 973, 974,
631         975, 2729, 2730, 977, 2731, 979, 980, 981, 982, 983, 984, 3506,
632         987, 989, 990, 991, 2732, 2733, 6051, 6053, 6055, 910, 6056,
633         4339, 4340, 577, 4341, 579, 580, 581, 616, 584, 585, 586, 4342,
634         4343, 589, 590, 591, 592, 593, 594, 595, 596, 597, 598, 5046,
635         599, 600, 5047, 601, 602, 603, 604, 605, 5053, 608, 609, 610,
636         5055, 612, 613, 5056, 615, 617, 618, 619, 620, 621, 622, 623,
637         624, 6882, 627, 628, 629, 630, 631, 5330, 633, 634, 635, 636,
638         637, 639, 640, 7870, 632, 34480, 13118, 903, 904, 905, 907,
639         2616, 2617, 2618, 2619, 2620, 2621, 2622, 2623, 2624, 2643,
640         1685, 1686, 1687, 1688, 1690, 1691, 2644, 2645, 1695, 2646,
641         1699, 2647, 2648, 1702, 2649, 2650, 1706, 22082, 5516, 4307,
642         2203, 1995, 1996, 1998, 1999, 2206, 2002, 2003, 4407, 2005,
643         4408, 2007, 2008, 2009, 2010, 2011, 4409, 2013, 2014, 2015,
644         2017, 3227, 3149, 6025, 22913, 22914, 3228, 7925, 10123, 10124,
645         10125, 10127, 16978, 14094, 1593, 4869, 4870, 3477, 3844, 3845,
646         9923, 3846, 3847, 39767, 39768, 39769, 3541, 39770, 39771,
647         14179, 39772, 39773, 39774, 42558, 1043, 4203, 42559, 42560,
648         42561, 42562, 42563, 42564, 11018, 42565, 42566, 4589, 4590,
649         4591, 4312, 18283, 4317, 4318, 4319, 12659, 11706, 11707,
650         53395, 53396, 29410, 8040, 8041, 915, 20105, 22952, 22953,
651         20596, 4161, 3047, 3048, 3049, 3050, 3051, 3052, 3053, 3054,
652         3055, 1474, 3056, 3057, 3058, 3059, 3060, 3061, 2549, 2551,
653         3062, 3063, 3064, 3065, 3066, 3067, 3068, 3069, 515, 3070,
654         3071, 3072, 3073, 3074, 3075, 3076, 3077, 3078, 3079, 3080,
655         3081, 3082, 506, 3083, 3084, 3085, 3086, 3087, 3088, 3089,
656         3090, 3091, 527, 528, 2995, 530, 531, 533, 534, 535, 537, 538 };
657   }
658
659 }