summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/regress/lib/libc/qsort/Makefile3
-rw-r--r--src/regress/lib/libc/qsort/antiqsort.c58
-rw-r--r--src/regress/lib/libc/qsort/qsort_test.c1792
3 files changed, 315 insertions, 1538 deletions
diff --git a/src/regress/lib/libc/qsort/Makefile b/src/regress/lib/libc/qsort/Makefile
index 9062e26f95..473432f423 100644
--- a/src/regress/lib/libc/qsort/Makefile
+++ b/src/regress/lib/libc/qsort/Makefile
@@ -1,6 +1,7 @@
1# $OpenBSD: Makefile,v 1.2 2017/05/17 20:28:35 millert Exp $ 1# $OpenBSD: Makefile,v 1.3 2017/05/22 17:16:43 millert Exp $
2 2
3PROG= qsort_test 3PROG= qsort_test
4SRCS= qsort_test.c antiqsort.c
4CFLAGS+=-Wall 5CFLAGS+=-Wall
5 6
6qsort-regress: ${PROG} 7qsort-regress: ${PROG}
diff --git a/src/regress/lib/libc/qsort/antiqsort.c b/src/regress/lib/libc/qsort/antiqsort.c
new file mode 100644
index 0000000000..cb3b7b2525
--- /dev/null
+++ b/src/regress/lib/libc/qsort/antiqsort.c
@@ -0,0 +1,58 @@
1/*
2 * A Killer Adversary for Quicksort
3 * M. D. MCILROY
4 * http://www.cs.dartmouth.edu/~doug/mdmspe.pdf
5 *
6 * For comparison:
7 * Bentley & McIlroy: 4096 items, 1645585 compares
8 * random pivot: 4096 items, 8388649 compares
9 * introsort: 4096 items, 151580 compares
10 * heapsort: 4096 items, 48233 compares
11 */
12
13#include <stdio.h>
14#include <stdlib.h>
15
16static int *val; /* item values */
17static int ncmp; /* number of comparisons */
18static int nsolid; /* number of solid items */
19static int candidate; /* pivot candidate */
20static int gas; /* gas value */
21
22#define freeze(x) (val[(x)] = nsolid++)
23
24static int
25cmp(const void *px, const void *py)
26{
27 const int x = *(const int *)px;
28 const int y = *(const int *)py;
29
30 ncmp++;
31 if (val[x] == gas && val[y] == gas) {
32 if (x == candidate)
33 freeze(x);
34 else
35 freeze(y);
36 }
37 if (val[x] == gas)
38 candidate = x;
39 else if (val[y] == gas)
40 candidate = y;
41 return val[x] > val[y] ? 1 : val[x] < val[y] ? -1 : 0;
42}
43
44int
45antiqsort(int n, int *a, int *ptr)
46{
47 int i;
48
49 val = a;
50 gas = n - 1;
51 nsolid = ncmp = candidate = 0;
52 for (i = 0; i < n; i++) {
53 ptr[i] = i;
54 val[i] = gas;
55 }
56 qsort(ptr, n, sizeof(*ptr), cmp);
57 return ncmp;
58}
diff --git a/src/regress/lib/libc/qsort/qsort_test.c b/src/regress/lib/libc/qsort/qsort_test.c
index 0596aa4eb4..45566353a7 100644
--- a/src/regress/lib/libc/qsort/qsort_test.c
+++ b/src/regress/lib/libc/qsort/qsort_test.c
@@ -14,10 +14,12 @@
14 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. 14 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
15 */ 15 */
16 16
17#include <stdbool.h>
17#include <stdio.h> 18#include <stdio.h>
18#include <stdlib.h> 19#include <stdlib.h>
19#include <string.h> 20#include <string.h>
20#include <setjmp.h> 21#include <setjmp.h>
22#include <unistd.h>
21#include <err.h> 23#include <err.h>
22 24
23/* 25/*
@@ -27,19 +29,13 @@
27 * Additional "killer" input taken from: 29 * Additional "killer" input taken from:
28 * David R. Musser's "Introspective Sorting and Selection Algorithms" 30 * David R. Musser's "Introspective Sorting and Selection Algorithms"
29 * http://calmerthanyouare.org/2014/06/11/algorithmic-complexity-attacks-and-libc-qsort.html 31 * http://calmerthanyouare.org/2014/06/11/algorithmic-complexity-attacks-and-libc-qsort.html
30 * M. D. McIlroy's "A Killer Adversary for Quicksort" targeting B & M qsort 32 * M. D. McIlroy's "A Killer Adversary for Quicksort"
31 */ 33 */
32 34
33enum distribution { 35struct test_distribution {
34 SAWTOOTH, 36 const char *name;
35 RAND, 37 void (*fill)(int *x, int n, int m);
36 STAGGER, 38 int (*test)(struct test_distribution *d, int n, int *x, int *y, int *z);
37 PLATEAU,
38 SHUFFLE,
39 BM_KILLER,
40 BSD_KILLER,
41 MED3_KILLER,
42 INVALID
43}; 39};
44 40
45#define min(a, b) (((a) < (b)) ? (a) : (b)) 41#define min(a, b) (((a) < (b)) ? (a) : (b))
@@ -48,1324 +44,9 @@ static size_t compares;
48static size_t max_compares; 44static size_t max_compares;
49static size_t abrt_compares; 45static size_t abrt_compares;
50static sigjmp_buf cmpjmp; 46static sigjmp_buf cmpjmp;
47static bool dump_table, verbose;
51 48
52/* 49extern int antiqsort(int n, int *a, int *ptr);
53 * Bentley and McIlroy "killer" input generated by from McIlroy's
54 * "A Killer Adversary for Quicksort" program.
55 */
56static const int bmkiller_100[] = {
57 0, 28, 90, 87, 6, 15, 75, 77, 10, 33, 64, 80,
58 1, 31, 16, 25, 7, 39, 52, 11, 21, 79, 70, 99,
59 17, 26, 36, 92, 89, 95, 22, 81, 86, 82, 27, 37,
60 46, 83, 32, 41, 76, 54, 84, 38, 56, 47, 42, 85,
61 59, 72, 2, 48, 8, 96, 12, 63, 57, 18, 67, 78,
62 23, 58, 3, 53, 9, 13, 66, 19, 68, 43, 24, 29,
63 49, 34, 74, 40, 44, 88, 50, 94, 62, 55, 65, 60,
64 69, 71, 73, 4, 14, 20, 30, 35, 45, 51, 61, 91,
65 93, 97, 98, 5
66};
67
68static const int bmkiller_1023[] = {
69 0, 956, 731, 129, 6, 15, 687, 133, 10, 643, 684, 853,
70 443, 691, 16, 25, 692, 773, 20, 833, 269, 953, 449, 144,
71 26, 35, 983, 275, 882, 149, 31, 920, 972, 459, 915, 36,
72 46, 285, 539, 160, 41, 698, 663, 813, 164, 47, 56, 702,
73 652, 51, 295, 910, 469, 535, 743, 57, 66, 783, 714, 61,
74 835, 300, 819, 540, 180, 67, 76, 971, 673, 545, 185, 72,
75 708, 618, 885, 200, 77, 87, 316, 551, 403, 82, 712, 922,
76 978, 961, 88, 97, 986, 205, 92, 674, 624, 757, 490, 717,
77 98, 107, 718, 628, 561, 754, 103, 794, 1012, 500, 924, 108,
78 118, 938, 1011, 231, 113, 968, 341, 792, 226, 119, 128, 723,
79 232, 123, 694, 347, 510, 580, 851, 1, 138, 728, 751, 7,
80 357, 735, 11, 576, 987, 139, 148, 994, 17, 581, 830, 21,
81 733, 367, 802, 767, 27, 159, 649, 586, 770, 154, 32, 372,
82 925, 263, 37, 169, 739, 740, 42, 779, 378, 883, 592, 48,
83 170, 179, 52, 868, 536, 375, 175, 814, 58, 778, 448, 62,
84 190, 393, 611, 746, 68, 749, 665, 546, 780, 191, 73, 906,
85 303, 195, 78, 669, 552, 607, 83, 201, 210, 820, 304, 89,
86 675, 409, 93, 556, 787, 211, 220, 99, 869, 617, 613, 216,
87 996, 104, 952, 890, 221, 109, 423, 623, 899, 114, 759, 825,
88 907, 334, 120, 241, 764, 124, 236, 896, 685, 798, 727, 130,
89 242, 251, 134, 989, 577, 339, 247, 140, 804, 905, 345, 252,
90 262, 145, 732, 349, 257, 150, 450, 587, 638, 155, 272, 774,
91 916, 267, 161, 700, 593, 165, 360, 273, 282, 936, 171, 277,
92 465, 980, 884, 597, 176, 283, 292, 931, 181, 603, 452, 288,
93 186, 475, 839, 998, 293, 192, 865, 658, 196, 298, 784, 481,
94 962, 933, 202, 313, 845, 206, 308, 942, 485, 908, 212, 396,
95 314, 323, 790, 491, 217, 401, 319, 941, 222, 947, 416, 324,
96 227, 501, 683, 762, 329, 233, 726, 1005, 237, 335, 344, 795,
97 421, 243, 511, 949, 634, 679, 680, 248, 354, 800, 855, 253,
98 771, 516, 990, 258, 432, 355, 364, 999, 264, 644, 437, 268,
99 805, 993, 834, 831, 365, 274, 532, 695, 278, 370, 861, 944,
100 736, 284, 376, 385, 811, 591, 380, 289, 781, 840, 654, 294,
101 386, 395, 815, 299, 705, 886, 391, 866, 305, 895, 609, 309,
102 406, 1007, 943, 842, 315, 821, 557, 844, 479, 407, 320, 871,
103 619, 411, 325, 563, 973, 724, 330, 417, 426, 937, 493, 336,
104 573, 921, 340, 720, 721, 427, 436, 826, 346, 725, 995, 350,
105 876, 583, 874, 803, 356, 447, 969, 690, 519, 442, 361, 588,
106 992, 514, 366, 457, 836, 520, 371, 817, 594, 954, 696, 377,
107 458, 467, 381, 782, 991, 737, 463, 387, 951, 880, 777, 468,
108 478, 392, 755, 979, 473, 397, 926, 967, 550, 402, 488, 846,
109 957, 483, 408, 959, 930, 412, 707, 489, 498, 892, 864, 418,
110 974, 625, 422, 756, 796, 499, 508, 428, 1013, 761, 893, 504,
111 852, 433, 875, 668, 509, 438, 639, 2, 897, 8, 856, 12,
112 807, 877, 18, 529, 22, 453, 524, 28, 809, 881, 33, 637,
113 530, 38, 862, 43, 464, 828, 49, 902, 53, 747, 932, 59,
114 474, 63, 841, 648, 69, 480, 666, 74, 484, 79, 560, 867,
115 84, 555, 90, 940, 94, 494, 612, 100, 570, 872, 105, 565,
116 681, 110, 1000, 115, 505, 571, 121, 1008, 125, 797, 627, 131,
117 515, 135, 911, 633, 141, 521, 900, 146, 525, 151, 963, 697,
118 156, 531, 162, 601, 166, 889, 596, 172, 701, 955, 177, 541,
119 602, 182, 887, 187, 964, 653, 193, 1003, 197, 788, 903, 203,
120 622, 207, 827, 664, 213, 562, 850, 218, 566, 223, 632, 982,
121 228, 572, 234, 854, 238, 823, 988, 244, 642, 927, 249, 582,
122 860, 254, 3, 259, 9, 13, 265, 898, 19, 23, 689, 29,
123 1010, 279, 34, 704, 39, 44, 748, 290, 50, 54, 608, 1004,
124 60, 64, 306, 70, 310, 709, 75, 80, 870, 85, 321, 91,
125 95, 326, 101, 331, 824, 106, 337, 111, 116, 879, 799, 122,
126 126, 351, 1017, 132, 136, 914, 142, 362, 730, 147, 152, 918,
127 157, 699, 163, 167, 382, 173, 659, 388, 178, 1022, 183, 188,
128 789, 398, 194, 198, 934, 715, 204, 208, 413, 214, 958, 419,
129 219, 224, 946, 229, 429, 235, 239, 434, 245, 439, 928, 250,
130 444, 255, 260, 745, 454, 266, 270, 460, 810, 276, 280, 706,
131 286, 470, 710, 291, 296, 808, 301, 716, 307, 311, 965, 317,
132 766, 495, 322, 977, 327, 332, 912, 506, 338, 342, 776, 939,
133 348, 352, 522, 358, 526, 741, 363, 368, 786, 373, 537, 379,
134 383, 542, 389, 547, 752, 394, 553, 399, 404, 891, 901, 410,
135 414, 567, 1019, 420, 424, 768, 430, 578, 772, 435, 440, 1002,
136 445, 838, 451, 455, 598, 461, 812, 604, 466, 1001, 471, 476,
137 818, 614, 482, 486, 793, 843, 492, 496, 629, 502, 849, 635,
138 507, 512, 948, 517, 645, 523, 527, 650, 533, 655, 848, 538,
139 660, 543, 548, 1006, 670, 554, 558, 676, 858, 564, 568, 829,
140 574, 686, 1018, 579, 584, 859, 589, 970, 595, 599, 923, 605,
141 985, 711, 610, 1015, 615, 620, 984, 722, 626, 630, 975, 913,
142 636, 640, 738, 646, 742, 997, 651, 656, 917, 661, 753, 667,
143 671, 758, 677, 763, 1009, 682, 769, 4, 14, 24, 30, 40,
144 45, 55, 65, 71, 81, 86, 96, 102, 112, 117, 127, 137,
145 143, 153, 158, 168, 174, 184, 189, 199, 209, 215, 225, 230,
146 240, 246, 256, 261, 271, 281, 287, 297, 302, 312, 318, 328,
147 333, 343, 353, 359, 369, 374, 384, 390, 400, 405, 415, 425,
148 431, 441, 446, 456, 462, 472, 477, 487, 497, 503, 513, 518,
149 528, 534, 544, 549, 559, 569, 575, 585, 590, 600, 606, 616,
150 621, 631, 641, 647, 657, 662, 672, 678, 688, 693, 703, 713,
151 719, 729, 734, 744, 750, 760, 765, 775, 785, 791, 801, 806,
152 816, 822, 832, 837, 847, 857, 863, 873, 878, 888, 894, 904,
153 909, 919, 929, 935, 945, 950, 960, 966, 976, 981, 1014, 1016,
154 1020, 1021, 5
155};
156
157static const int bmkiller_1024[] = {
158 0, 260, 732, 130, 6, 16, 770, 685, 444, 752, 11, 688,
159 266, 808, 577, 17, 26, 693, 774, 21, 834, 270, 954, 450,
160 145, 27, 36, 984, 276, 883, 150, 32, 921, 973, 460, 916,
161 37, 47, 286, 540, 161, 42, 699, 664, 814, 165, 48, 57,
162 703, 653, 52, 296, 911, 470, 536, 744, 58, 67, 784, 715,
163 62, 836, 301, 820, 541, 181, 68, 77, 972, 674, 546, 186,
164 73, 709, 619, 886, 201, 78, 88, 317, 552, 404, 83, 713,
165 923, 979, 962, 89, 98, 987, 206, 93, 675, 625, 758, 491,
166 718, 99, 108, 719, 629, 562, 755, 104, 795, 1013, 501, 925,
167 109, 119, 939, 1012, 232, 114, 969, 342, 793, 227, 120, 129,
168 724, 233, 124, 695, 348, 511, 581, 852, 1, 139, 729, 7,
169 134, 358, 736, 692, 12, 988, 140, 149, 995, 18, 582, 831,
170 22, 734, 368, 803, 768, 28, 160, 650, 587, 771, 155, 33,
171 373, 926, 264, 38, 170, 740, 741, 43, 780, 379, 884, 593,
172 49, 171, 180, 53, 869, 537, 376, 176, 815, 59, 779, 449,
173 63, 191, 394, 612, 747, 69, 750, 666, 547, 781, 192, 74,
174 907, 304, 196, 79, 670, 553, 608, 84, 202, 211, 821, 305,
175 90, 676, 410, 94, 557, 788, 212, 221, 100, 870, 618, 614,
176 217, 997, 105, 953, 891, 222, 110, 424, 624, 900, 115, 760,
177 826, 908, 335, 121, 242, 765, 125, 237, 897, 686, 799, 728,
178 131, 243, 252, 135, 990, 578, 340, 248, 141, 805, 906, 346,
179 253, 263, 146, 733, 350, 258, 151, 451, 588, 639, 156, 273,
180 775, 917, 268, 162, 701, 594, 166, 361, 274, 283, 937, 172,
181 278, 466, 981, 885, 598, 177, 284, 293, 932, 182, 604, 453,
182 289, 187, 476, 840, 999, 294, 193, 866, 659, 197, 299, 785,
183 482, 963, 934, 203, 314, 846, 207, 309, 943, 486, 909, 213,
184 397, 315, 324, 791, 492, 218, 402, 320, 942, 223, 948, 417,
185 325, 228, 502, 684, 763, 330, 234, 727, 1006, 238, 336, 345,
186 796, 422, 244, 512, 950, 635, 680, 681, 249, 355, 801, 856,
187 254, 772, 517, 991, 259, 433, 356, 365, 1000, 265, 645, 438,
188 269, 806, 994, 835, 832, 366, 275, 533, 696, 279, 371, 862,
189 945, 737, 285, 377, 386, 812, 592, 381, 290, 782, 841, 655,
190 295, 387, 396, 816, 300, 706, 887, 392, 867, 306, 896, 610,
191 310, 407, 1008, 944, 843, 316, 822, 558, 845, 480, 408, 321,
192 872, 620, 412, 326, 564, 974, 725, 331, 418, 427, 938, 494,
193 337, 574, 922, 341, 721, 722, 428, 437, 827, 347, 726, 996,
194 351, 877, 584, 875, 804, 357, 448, 970, 691, 520, 443, 362,
195 589, 993, 515, 367, 458, 837, 521, 372, 818, 595, 955, 697,
196 378, 459, 468, 382, 783, 992, 738, 464, 388, 952, 881, 778,
197 469, 479, 393, 756, 980, 474, 398, 927, 968, 551, 403, 489,
198 847, 958, 484, 409, 960, 931, 413, 708, 490, 499, 893, 865,
199 419, 975, 626, 423, 757, 797, 500, 509, 429, 1014, 762, 894,
200 505, 853, 434, 876, 669, 510, 439, 640, 2, 898, 8, 857,
201 854, 13, 878, 19, 530, 23, 454, 525, 29, 810, 882, 34,
202 638, 531, 39, 863, 44, 465, 829, 50, 903, 54, 748, 933,
203 60, 475, 64, 842, 649, 70, 481, 667, 75, 485, 80, 561,
204 868, 85, 556, 91, 941, 95, 495, 613, 101, 571, 873, 106,
205 566, 682, 111, 1001, 116, 506, 572, 122, 1009, 126, 798, 628,
206 132, 516, 136, 912, 634, 142, 522, 901, 147, 526, 152, 964,
207 698, 157, 532, 163, 602, 167, 890, 597, 173, 702, 956, 178,
208 542, 603, 183, 888, 188, 965, 654, 194, 1004, 198, 789, 904,
209 204, 623, 208, 828, 665, 214, 563, 851, 219, 567, 224, 633,
210 983, 229, 573, 235, 855, 239, 824, 989, 245, 643, 928, 250,
211 583, 861, 255, 957, 3, 9, 644, 14, 899, 20, 24, 690,
212 30, 1011, 280, 35, 705, 40, 45, 749, 291, 51, 55, 609,
213 1005, 61, 65, 307, 71, 311, 710, 76, 81, 871, 86, 322,
214 92, 96, 327, 102, 332, 825, 107, 338, 112, 117, 880, 800,
215 123, 127, 352, 1018, 133, 137, 915, 143, 363, 731, 148, 153,
216 919, 158, 700, 164, 168, 383, 174, 660, 389, 179, 1023, 184,
217 189, 790, 399, 195, 199, 935, 716, 205, 209, 414, 215, 959,
218 420, 220, 225, 947, 230, 430, 236, 240, 435, 246, 440, 929,
219 251, 445, 256, 261, 746, 455, 267, 271, 461, 811, 277, 281,
220 707, 287, 471, 711, 292, 297, 809, 302, 717, 308, 312, 966,
221 318, 767, 496, 323, 978, 328, 333, 913, 507, 339, 343, 777,
222 940, 349, 353, 523, 359, 527, 742, 364, 369, 787, 374, 538,
223 380, 384, 543, 390, 548, 753, 395, 554, 400, 405, 892, 902,
224 411, 415, 568, 1020, 421, 425, 769, 431, 579, 773, 436, 441,
225 1003, 446, 839, 452, 456, 599, 462, 813, 605, 467, 1002, 472,
226 477, 819, 615, 483, 487, 794, 844, 493, 497, 630, 503, 850,
227 636, 508, 513, 949, 518, 646, 524, 528, 651, 534, 656, 849,
228 539, 661, 544, 549, 1007, 671, 555, 559, 677, 859, 565, 569,
229 830, 575, 687, 1019, 580, 585, 860, 590, 971, 596, 600, 924,
230 606, 986, 712, 611, 1016, 616, 621, 985, 723, 627, 631, 976,
231 914, 637, 641, 739, 647, 743, 998, 652, 657, 918, 662, 754,
232 668, 672, 759, 678, 764, 1010, 683, 4, 10, 15, 25, 31,
233 41, 46, 56, 66, 72, 82, 87, 97, 103, 113, 118, 128,
234 138, 144, 154, 159, 169, 175, 185, 190, 200, 210, 216, 226,
235 231, 241, 247, 257, 262, 272, 282, 288, 298, 303, 313, 319,
236 329, 334, 344, 354, 360, 370, 375, 385, 391, 401, 406, 416,
237 426, 432, 442, 447, 457, 463, 473, 478, 488, 498, 504, 514,
238 519, 529, 535, 545, 550, 560, 570, 576, 586, 591, 601, 607,
239 617, 622, 632, 642, 648, 658, 663, 673, 679, 689, 694, 704,
240 714, 720, 730, 735, 745, 751, 761, 766, 776, 786, 792, 802,
241 807, 817, 823, 833, 838, 848, 858, 864, 874, 879, 889, 895,
242 905, 910, 920, 930, 936, 946, 951, 961, 967, 977, 982, 1015,
243 1017, 1021, 1022, 5
244};
245
246static const int bmkiller_1025[] = {
247 0, 588, 777, 130, 6, 16, 688, 260, 444, 418, 11, 882,
248 265, 928, 577, 17, 26, 774, 901, 21, 690, 270, 454, 530,
249 145, 27, 36, 693, 160, 31, 937, 280, 992, 1007, 917, 37,
250 46, 698, 286, 540, 263, 42, 986, 291, 535, 784, 47, 57,
251 608, 656, 834, 52, 703, 296, 739, 278, 58, 67, 972, 702,
252 62, 614, 301, 475, 550, 190, 68, 77, 709, 307, 546, 186,
253 73, 713, 669, 1000, 201, 78, 88, 317, 561, 196, 83, 892,
254 824, 797, 299, 89, 98, 719, 206, 93, 327, 675, 495, 908,
255 718, 99, 108, 795, 414, 103, 998, 332, 501, 571, 217, 109,
256 118, 896, 830, 970, 222, 114, 724, 685, 506, 912, 119, 129,
257 348, 581, 233, 124, 800, 352, 798, 237, 1, 139, 729, 7,
258 134, 358, 726, 927, 12, 765, 140, 149, 734, 18, 582, 859,
259 22, 902, 695, 996, 767, 150, 28, 780, 964, 32, 155, 916,
260 373, 980, 38, 161, 170, 740, 268, 165, 43, 379, 536, 602,
261 48, 171, 180, 744, 53, 175, 389, 706, 542, 59, 885, 181,
262 63, 815, 393, 612, 781, 69, 968, 399, 547, 782, 191, 74,
263 670, 712, 304, 79, 750, 404, 700, 84, 202, 211, 754, 305,
264 90, 925, 409, 94, 622, 715, 212, 221, 999, 100, 618, 674,
265 104, 760, 929, 794, 319, 110, 232, 938, 633, 891, 227, 115,
266 825, 872, 852, 120, 242, 1024, 796, 125, 435, 989, 974, 894,
267 131, 243, 252, 135, 340, 247, 805, 440, 141, 643, 721, 253,
268 262, 770, 146, 733, 1006, 258, 151, 935, 694, 433, 156, 273,
269 455, 653, 523, 162, 775, 944, 166, 862, 274, 283, 932, 376,
270 172, 465, 1010, 176, 598, 449, 284, 293, 182, 747, 654, 453,
271 289, 785, 187, 849, 543, 294, 192, 821, 1013, 837, 197, 923,
272 481, 941, 811, 203, 314, 791, 207, 309, 757, 486, 710, 213,
273 406, 315, 324, 942, 947, 218, 900, 496, 966, 223, 489, 325,
274 334, 228, 502, 684, 484, 330, 234, 507, 679, 238, 335, 345,
275 1003, 764, 422, 244, 856, 512, 248, 680, 346, 355, 801, 254,
276 350, 808, 517, 1015, 639, 259, 356, 365, 806, 264, 645, 438,
277 361, 269, 803, 835, 943, 366, 275, 533, 650, 279, 371, 952,
278 945, 869, 285, 377, 386, 812, 592, 381, 290, 1001, 933, 919,
279 295, 387, 396, 816, 300, 391, 788, 548, 922, 306, 478, 397,
280 310, 953, 758, 926, 474, 402, 316, 997, 979, 320, 407, 417,
281 564, 725, 326, 412, 822, 568, 870, 551, 331, 427, 826, 494,
282 336, 574, 823, 911, 341, 722, 428, 437, 877, 347, 686, 853,
283 351, 832, 773, 1014, 804, 357, 448, 1005, 691, 520, 443, 362,
284 589, 1021, 515, 367, 458, 883, 521, 372, 956, 595, 772, 746,
285 378, 459, 468, 382, 638, 463, 605, 867, 890, 388, 903, 469,
286 392, 842, 609, 756, 809, 398, 948, 615, 751, 963, 479, 403,
287 960, 907, 868, 408, 847, 620, 934, 413, 490, 499, 893, 556,
288 419, 955, 625, 423, 766, 906, 500, 509, 429, 630, 762, 1011,
289 505, 857, 434, 895, 759, 510, 439, 949, 2, 897, 8, 954,
290 880, 13, 1016, 450, 19, 863, 23, 525, 651, 29, 742, 33,
291 460, 531, 39, 464, 593, 44, 887, 49, 470, 787, 54, 541,
292 60, 958, 64, 841, 818, 70, 480, 975, 75, 607, 485, 80,
293 671, 85, 965, 491, 91, 850, 95, 924, 562, 101, 873, 105,
294 566, 681, 111, 763, 793, 116, 572, 121, 878, 511, 126, 1008,
295 132, 516, 136, 921, 634, 142, 522, 860, 147, 526, 587, 152,
296 697, 157, 838, 532, 163, 884, 167, 597, 995, 173, 783, 177,
297 649, 603, 183, 888, 664, 188, 978, 193, 789, 552, 198, 613,
298 204, 557, 208, 828, 741, 214, 563, 723, 219, 567, 623, 224,
299 855, 229, 573, 628, 235, 728, 239, 939, 578, 245, 898, 249,
300 583, 861, 255, 957, 3, 9, 644, 14, 991, 594, 20, 24,
301 276, 904, 30, 34, 705, 40, 604, 749, 45, 50, 659, 55,
302 1009, 61, 65, 665, 71, 1012, 311, 76, 619, 81, 86, 321,
303 624, 92, 96, 909, 629, 102, 106, 337, 112, 635, 342, 117,
304 122, 914, 127, 990, 133, 137, 983, 143, 363, 984, 148, 368,
305 153, 158, 737, 655, 164, 168, 383, 660, 174, 178, 993, 184,
306 666, 790, 189, 194, 865, 199, 716, 205, 209, 676, 215, 962,
307 420, 220, 424, 225, 230, 430, 736, 236, 240, 940, 731, 246,
308 250, 445, 256, 696, 451, 261, 266, 701, 271, 461, 277, 281,
309 707, 287, 471, 711, 292, 476, 297, 302, 717, 918, 308, 312,
310 492, 959, 318, 322, 950, 328, 727, 831, 333, 338, 732, 343,
311 1004, 349, 353, 738, 359, 836, 527, 364, 778, 369, 374, 537,
312 748, 380, 384, 752, 886, 390, 394, 553, 400, 846, 558, 405,
313 410, 969, 415, 967, 421, 425, 768, 431, 579, 931, 436, 584,
314 441, 446, 1020, 779, 452, 456, 599, 813, 462, 466, 982, 472,
315 910, 819, 477, 482, 844, 487, 994, 493, 497, 799, 503, 829,
316 636, 508, 640, 513, 518, 646, 810, 524, 528, 814, 839, 534,
317 538, 661, 544, 820, 667, 549, 554, 976, 559, 677, 565, 569,
318 854, 575, 687, 1019, 580, 692, 585, 590, 985, 840, 596, 600,
319 708, 845, 606, 610, 973, 616, 851, 1002, 621, 626, 875, 631,
320 913, 637, 641, 881, 647, 988, 743, 652, 866, 657, 662, 753,
321 871, 668, 672, 981, 876, 678, 682, 769, 4, 10, 15, 25,
322 35, 41, 51, 56, 66, 72, 82, 87, 97, 107, 113, 123,
323 128, 138, 144, 154, 159, 169, 179, 185, 195, 200, 210, 216,
324 226, 231, 241, 251, 257, 267, 272, 282, 288, 298, 303, 313,
325 323, 329, 339, 344, 354, 360, 370, 375, 385, 395, 401, 411,
326 416, 426, 432, 442, 447, 457, 467, 473, 483, 488, 498, 504,
327 514, 519, 529, 539, 545, 555, 560, 570, 576, 586, 591, 601,
328 611, 617, 627, 632, 642, 648, 658, 663, 673, 683, 689, 699,
329 704, 714, 720, 730, 735, 745, 755, 761, 771, 776, 786, 792,
330 802, 807, 817, 827, 833, 843, 848, 858, 864, 874, 879, 889,
331 899, 905, 915, 920, 930, 936, 946, 951, 961, 971, 977, 987,
332 1017, 1018, 1022, 1023, 5
333};
334
335static const int bmkiller_4095[] = {
336 0, 1026, 3946, 3997, 6, 15, 3585, 1411, 10, 3878, 1030, 2052,
337 3080, 520, 16, 25, 3077, 3507, 20, 2567, 2761, 2057, 1765, 2757,
338 26, 35, 2739, 2352, 3330, 3656, 31, 2744, 2356, 2072, 2315, 36,
339 46, 3226, 2067, 2545, 41, 3083, 3332, 2573, 3654, 47, 56, 2749,
340 3211, 51, 3592, 1061, 1786, 2320, 2767, 57, 66, 3087, 570, 61,
341 1071, 3954, 3338, 1790, 565, 67, 76, 2755, 3230, 1796, 1777, 72,
342 2759, 2596, 3428, 3711, 77, 87, 1082, 2948, 4087, 82, 3093, 1087,
343 3906, 1462, 88, 97, 2765, 3600, 92, 1092, 2592, 2093, 1806, 592,
344 98, 107, 3604, 1098, 3524, 2783, 103, 3098, 2607, 3597, 611, 108,
345 118, 1108, 3764, 3337, 113, 2770, 3660, 2113, 2360, 119, 128, 3103,
346 2355, 123, 3358, 2393, 3348, 2108, 3227, 129, 138, 2775, 2940, 133,
347 3725, 1123, 1832, 3880, 3664, 139, 148, 2780, 1129, 3812, 633, 144,
348 3108, 3353, 3602, 3124, 149, 159, 3246, 1842, 643, 154, 4001, 2618,
349 2134, 2581, 160, 169, 2786, 3995, 164, 3462, 3603, 2129, 1848, 663,
350 170, 179, 2790, 2413, 3121, 3237, 175, 3118, 3544, 2144, 3606, 180,
351 190, 3813, 2139, 2808, 185, 3615, 2628, 3257, 674, 191, 200, 2796,
352 1849, 195, 4052, 1170, 2154, 2391, 2823, 201, 210, 2800, 2974, 205,
353 1180, 3914, 1873, 2149, 3935, 211, 220, 3667, 2639, 2392, 704, 216,
354 2806, 3139, 3852, 3456, 221, 231, 1190, 1883, 714, 226, 3129, 1195,
355 3454, 4045, 232, 241, 3545, 715, 236, 1201, 3612, 2165, 1889, 1561,
356 242, 251, 2811, 1205, 2994, 3461, 247, 2816, 1211, 1899, 2171, 252,
357 262, 1215, 3885, 2834, 257, 3549, 3272, 2185, 745, 263, 272, 2821,
358 3675, 267, 2668, 2454, 1909, 2180, 1167, 273, 282, 3938, 3729, 277,
359 3915, 1231, 2195, 3937, 3155, 283, 292, 2827, 1236, 3625, 2665, 288,
360 2831, 3467, 3464, 3827, 293, 303, 1246, 3152, 3782, 298, 3555, 3026,
361 2206, 1602, 304, 313, 2837, 786, 308, 2674, 3553, 2201, 1930, 781,
362 314, 323, 3857, 3031, 3689, 3130, 319, 3822, 2680, 1940, 1208, 324,
363 334, 2480, 2211, 3547, 329, 2842, 3685, 2682, 1622, 335, 344, 3626,
364 1627, 339, 3389, 1277, 1950, 2857, 808, 345, 354, 2847, 3476, 349,
365 1287, 2490, 3566, 2221, 3477, 355, 364, 2852, 3042, 2463, 3627, 360,
366 3894, 2695, 3475, 2459, 365, 375, 1298, 3994, 3471, 370, 3165, 1303,
367 3479, 3491, 376, 385, 2858, 3012, 380, 1308, 2700, 2237, 3788, 2884,
368 386, 395, 2862, 1314, 1976, 849, 391, 3170, 2510, 3633, 1663, 396,
369 406, 1324, 2474, 859, 401, 4022, 3745, 1986, 3169, 407, 416, 2868,
370 3694, 411, 3896, 3751, 1992, 2252, 879, 417, 426, 2872, 3190, 421,
371 2521, 1339, 2267, 1996, 880, 427, 436, 3636, 1345, 3570, 2890, 432,
372 2878, 3639, 3638, 899, 437, 447, 3924, 3051, 3697, 442, 4008, 2531,
373 2278, 2504, 448, 457, 3186, 2499, 452, 3837, 3313, 2273, 3750, 3299,
374 458, 467, 2883, 2537, 2017, 920, 463, 2888, 2541, 2288, 2280, 468,
375 478, 3647, 2283, 930, 473, 3580, 2736, 2027, 1719, 479, 488, 2893,
376 931, 483, 2915, 1386, 2033, 2509, 3586, 489, 498, 3196, 3572, 493,
377 1396, 3948, 2743, 2037, 951, 499, 508, 2899, 2746, 2043, 3309, 504,
378 2903, 3430, 3500, 3053, 509, 519, 1406, 1, 2916, 514, 3201, 7,
379 3649, 962, 11, 529, 2909, 1353, 524, 1417, 17, 2309, 2053, 21,
380 530, 539, 4064, 1421, 27, 1756, 535, 3206, 1427, 3843, 32, 540,
381 550, 1431, 37, 3319, 545, 2914, 42, 2329, 3930, 551, 560, 48,
382 1002, 555, 52, 2578, 2074, 2324, 997, 561, 58, 2919, 1003, 62,
383 3432, 1447, 2339, 2078, 68, 571, 580, 2924, 1452, 2084, 73, 576,
384 3217, 2946, 78, 3987, 581, 591, 83, 3092, 2778, 586, 3596, 89,
385 2350, 1033, 93, 601, 2930, 4049, 596, 99, 3231, 2345, 2094, 3202,
386 602, 104, 2934, 2598, 3437, 109, 607, 4016, 4032, 114, 2568, 612,
387 622, 3349, 120, 2571, 617, 124, 3517, 2789, 2952, 623, 632, 130,
388 3084, 627, 134, 1493, 2370, 3532, 3224, 140, 642, 2944, 1074, 637,
389 1503, 145, 2120, 2365, 1069, 150, 652, 3848, 3445, 155, 1455, 648,
390 2950, 2812, 161, 3970, 653, 165, 1514, 2130, 4011, 658, 171, 1519,
391 3526, 1838, 664, 673, 176, 1843, 668, 1524, 181, 2381, 2136, 1096,
392 186, 683, 2955, 1530, 4048, 192, 679, 2960, 196, 3669, 1115, 684,
393 694, 1540, 202, 3773, 689, 206, 3672, 2401, 3884, 695, 212, 2965,
394 3114, 699, 3886, 2640, 217, 2396, 3964, 705, 222, 3728, 3109, 709,
395 227, 1555, 2161, 2608, 2983, 233, 724, 2971, 237, 3128, 1137, 720,
396 2975, 243, 3536, 1879, 725, 735, 3370, 248, 1147, 730, 3955, 253,
397 2422, 3936, 736, 258, 2981, 3608, 740, 3149, 264, 2417, 2177, 268,
398 746, 755, 4094, 3268, 3138, 274, 751, 3262, 278, 2187, 3125, 756,
399 766, 284, 2427, 4028, 761, 2986, 2844, 289, 1178, 767, 776, 294,
400 4002, 771, 3732, 299, 2197, 3731, 4030, 777, 305, 2991, 2643, 309,
401 1612, 2675, 2851, 2437, 315, 787, 796, 2996, 2855, 3821, 320, 792,
402 3682, 3018, 325, 2658, 797, 807, 330, 3858, 1218, 802, 3273, 336,
403 3551, 1935, 340, 817, 3002, 1219, 812, 1633, 346, 2453, 2218, 350,
404 818, 827, 3006, 1637, 356, 3028, 823, 3278, 1643, 2228, 361, 828,
405 838, 1647, 366, 1951, 833, 3688, 371, 2473, 1249, 839, 848, 377,
406 3024, 843, 381, 2701, 2238, 2468, 1600, 387, 858, 3016, 3687, 853,
407 3893, 392, 2483, 2679, 3039, 397, 868, 3739, 1668, 402, 1972, 864,
408 3022, 4029, 408, 2689, 869, 412, 1678, 3296, 3156, 874, 3793, 418,
409 2494, 2886, 422, 889, 3293, 1290, 884, 428, 3642, 2489, 3291, 1285,
410 890, 433, 3027, 2722, 2264, 438, 895, 3032, 2726, 443, 1641, 900,
411 910, 3701, 449, 3746, 905, 453, 3963, 2274, 3493, 911, 459, 3037,
412 3050, 915, 3497, 1709, 464, 3922, 1312, 921, 469, 3303, 3747, 925,
413 474, 2906, 3980, 2284, 1671, 480, 940, 3043, 484, 3634, 3409, 936,
414 3047, 2911, 490, 3290, 941, 494, 1730, 3195, 2715, 946, 500, 1735,
415 3898, 3060, 952, 961, 505, 3181, 956, 1740, 510, 2525, 3835, 4058,
416 515, 971, 3703, 1746, 2305, 521, 967, 3314, 525, 3705, 2922, 972,
417 982, 531, 3802, 1363, 977, 3058, 3708, 536, 2896, 983, 992, 541,
418 3644, 987, 3757, 546, 2321, 2540, 1383, 993, 552, 3063, 2059, 556,
419 2768, 1771, 2555, 2325, 1384, 562, 1012, 3068, 566, 2331, 2065, 1008,
420 3324, 572, 3710, 1403, 1013, 1023, 3090, 577, 3968, 1018, 3807, 582,
421 2566, 4071, 1024, 587, 3074, 3512, 1028, 3436, 593, 2561, 2341, 597,
422 1034, 1043, 3078, 2784, 603, 1424, 1039, 3334, 2788, 2576, 608, 1044,
423 1054, 3875, 613, 1434, 1049, 3662, 618, 3442, 2953, 1055, 1064, 624,
424 1435, 1059, 628, 1818, 2362, 3706, 2100, 1065, 634, 3088, 3766, 638,
425 1828, 3242, 2959, 2366, 644, 1075, 1084, 3769, 2962, 2372, 649, 1080,
426 3094, 3911, 654, 3218, 1085, 1095, 659, 3236, 3234, 1090, 3345, 665,
427 3598, 1466, 669, 1105, 3973, 2077, 1100, 675, 3355, 2597, 2382, 2973,
428 1106, 680, 3099, 1853, 3668, 685, 1111, 3104, 1859, 690, 2603, 1116,
429 1126, 1863, 696, 3228, 1121, 700, 3726, 2617, 2141, 1127, 1136, 706,
430 1506, 1131, 710, 2825, 4034, 2612, 1501, 716, 1146, 3673, 1507, 1141,
431 3131, 721, 2408, 2797, 3365, 726, 1156, 3115, 1884, 731, 3127, 1152,
432 3119, 3775, 737, 4019, 1157, 741, 1894, 2418, 2167, 1162, 747, 3738,
433 2638, 1537, 1168, 1177, 752, 3132, 1172, 2999, 757, 2633, 2424, 3958,
434 762, 1187, 4082, 2845, 3546, 768, 1183, 4026, 772, 2648, 2419, 1188,
435 1198, 3473, 778, 2978, 1193, 782, 3548, 3005, 3265, 1199, 788, 3683,
436 3253, 1203, 3736, 1925, 793, 2824, 3780, 1209, 798, 3135, 1578, 1213,
437 803, 3632, 2449, 2653, 1573, 809, 1228, 3140, 813, 3621, 1888, 1224,
438 4073, 819, 3619, 3474, 1229, 1239, 1946, 824, 3680, 1234, 3381, 829,
439 3623, 3369, 1240, 834, 3146, 3961, 1244, 1956, 840, 2669, 2465, 844,
440 1250, 1259, 3150, 1962, 3282, 850, 1255, 3386, 854, 2475, 1619, 1260,
441 1270, 860, 3942, 1928, 1265, 3693, 3163, 865, 2864, 1271, 1280, 870,
442 2859, 1275, 3574, 875, 2485, 2684, 3274, 1281, 881, 3160, 4023, 885,
443 3834, 1987, 2699, 3631, 891, 1291, 1300, 3744, 1993, 3992, 896, 1296,
444 3166, 3569, 901, 3406, 1301, 1311, 906, 3921, 1651, 1306, 3699, 912,
445 2710, 3289, 916, 1321, 3402, 3691, 1316, 3648, 922, 2705, 2506, 926,
446 1322, 1331, 3171, 4009, 932, 3489, 1327, 3176, 3652, 2516, 937, 1332,
447 1342, 2912, 942, 3306, 1337, 3759, 947, 3504, 1682, 1343, 1352, 953,
448 2511, 1347, 957, 2034, 2526, 2895, 2291, 963, 1362, 3412, 3049, 1357,
449 2044, 968, 3067, 2725, 4037, 973, 1372, 3187, 3071, 978, 1712, 1368,
450 3191, 3400, 984, 3698, 1373, 988, 2054, 3704, 1722, 1378, 3417, 994,
451 3756, 3577, 998, 1393, 3197, 1723, 1388, 1004, 4047, 2741, 3926, 2316,
452 1394, 1009, 3934, 2069, 2552, 1014, 1399, 3422, 2075, 1019, 2747, 1404,
453 1414, 2079, 1025, 3810, 1409, 1029, 3715, 2562, 1753, 1415, 1035, 3427,
454 3996, 1419, 3100, 3091, 1040, 2756, 2293, 1425, 1045, 3207, 3874, 1429,
455 1050, 2095, 2771, 2572, 3929, 1056, 1444, 3212, 1060, 3714, 3097, 1440,
456 3433, 3666, 1066, 3221, 1445, 1070, 2110, 3339, 3325, 1450, 1076, 2963,
457 2782, 2357, 1456, 1465, 1081, 1794, 1460, 3106, 1086, 2777, 3435, 1789,
458 1091, 1475, 3222, 2969, 2593, 1097, 1471, 3905, 1101, 2792, 3073, 1476,
459 1486, 1107, 2787, 3716, 1481, 3443, 3235, 1112, 2378, 1487, 1496, 1117,
460 2383, 1491, 3605, 1122, 2609, 3877, 1816, 1497, 1128, 3232, 3240, 1132,
461 2151, 3122, 3539, 2613, 2104, 1138, 1516, 4083, 1142, 2619, 3771, 1512,
462 3238, 1148, 3988, 2123, 1517, 1527, 2162, 1153, 3350, 1522, 3453, 1158,
463 3670, 3723, 1528, 1163, 3730, 3535, 1532, 2172, 1169, 2813, 2629, 1173,
464 1538, 1547, 3243, 2178, 1179, 1857, 1543, 3248, 3004, 3777, 1184, 1548,
465 1558, 2188, 1189, 1867, 1553, 3734, 1194, 2833, 3457, 1559, 1568, 1200,
466 3818, 1563, 1204, 3010, 2650, 2828, 1887, 1569, 1210, 4077, 3266, 1214,
467 4035, 2203, 2843, 2654, 1220, 1579, 1588, 3259, 2209, 2660, 1225, 1584,
468 3263, 3783, 1230, 1907, 1589, 1599, 1235, 3380, 3916, 1594, 3740, 1241,
469 2854, 3008, 1245, 1609, 3269, 3003, 1604, 1251, 3560, 2849, 2670, 3831,
470 1610, 1256, 4051, 3030, 3481, 1261, 1615, 3478, 3396, 1266, 2856, 1620,
471 1630, 3484, 1272, 1938, 1625, 1276, 3168, 3565, 2476, 1631, 1640, 1282,
472 1939, 1635, 1286, 2250, 2874, 3013, 3287, 1292, 1650, 3279, 3960, 1645,
473 2260, 1297, 2696, 2869, 1959, 1302, 1660, 3284, 3178, 1307, 3561, 1656,
474 3791, 3646, 1313, 3792, 1661, 1317, 2270, 2706, 3692, 1666, 1323, 2275,
475 3695, 1970, 1672, 1681, 1328, 3983, 1676, 2281, 1333, 2885, 2712, 2507,
476 1338, 1691, 3294, 2285, 3800, 1344, 1687, 3494, 1348, 3945, 2891, 1692,
477 1702, 2295, 1354, 3397, 1697, 1358, 3798, 2905, 3307, 1703, 1364, 3300,
478 2010, 1707, 3199, 3072, 1369, 2900, 2005, 1713, 1374, 3304, 2011, 1717,
479 1379, 2311, 2737, 3183, 2532, 1385, 1732, 4042, 1389, 3416, 3419, 1728,
480 3310, 1395, 4076, 3584, 1733, 1743, 2326, 1400, 3210, 1738, 3801, 1405,
481 2926, 2041, 1744, 1410, 3509, 3966, 1748, 3215, 1416, 2921, 2753, 1420,
482 1754, 1763, 3315, 3804, 3426, 1426, 1759, 3320, 1430, 2763, 3967, 1764,
483 1774, 1436, 2931, 3075, 1769, 3515, 3803, 1441, 3869, 1775, 1784, 1446,
484 3842, 1779, 3808, 1451, 2773, 3998, 3713, 1785, 1457, 3519, 2082, 1461,
485 2367, 3107, 3772, 2941, 1467, 1795, 1804, 3331, 3661, 3085, 1472, 1800,
486 3335, 3244, 1477, 3762, 1805, 1815, 1482, 3589, 3763, 1810, 3525, 1488,
487 4012, 2594, 1492, 1825, 3341, 2599, 1820, 2388, 1498, 2957, 2794, 1502,
488 1826, 1835, 3820, 2394, 1508, 2604, 1831, 3530, 3255, 2804, 1513, 1836,
489 1846, 2404, 1518, 2361, 1841, 3346, 1523, 2977, 3849, 1847, 1856, 1529,
490 3447, 1851, 1533, 3133, 2814, 2972, 4070, 1539, 1866, 3351, 3444, 1861,
491 3977, 1544, 2987, 3112, 3451, 1549, 1876, 3356, 2425, 1554, 2145, 1872,
492 3540, 3677, 1560, 2635, 1877, 1564, 3617, 3957, 2155, 1882, 3991, 1570,
493 2998, 3956, 1574, 1897, 3362, 3854, 1892, 1580, 3819, 2993, 4057, 2175,
494 1898, 1585, 3366, 3154, 2840, 1590, 1903, 3550, 3158, 1595, 3618, 1908,
495 1918, 3786, 1601, 3823, 1913, 1605, 3276, 2850, 2186, 1919, 1611, 3372,
496 2432, 1923, 3379, 2466, 1616, 3778, 3826, 1929, 1621, 3376, 3147, 1933,
497 1626, 3890, 3283, 2860, 4079, 1632, 1948, 3986, 1636, 3748, 2216, 1944,
498 3382, 3979, 1642, 3162, 1949, 1646, 2486, 3483, 2226, 1954, 1652, 2491,
499 3742, 2692, 1960, 1969, 1657, 2227, 1964, 2497, 1662, 3029, 3962, 3394,
500 1667, 1979, 3387, 2501, 2881, 1673, 1975, 3392, 1677, 4081, 3035, 1980,
501 1990, 1683, 3985, 2707, 1985, 3796, 3707, 1688, 2257, 1991, 2000, 1693,
502 4044, 1995, 3316, 1698, 2897, 3044, 3405, 2001, 1704, 4010, 3635, 1708,
503 3200, 2527, 3059, 2901, 2723, 1714, 2020, 3403, 1718, 2907, 2727, 2016,
504 3407, 1724, 3752, 3193, 2021, 2031, 2542, 1729, 3643, 2026, 3900, 1734,
505 3070, 3318, 2032, 1739, 3413, 2298, 2036, 3322, 1745, 3065, 2917, 1749,
506 2042, 2051, 3965, 3216, 1755, 3503, 2047, 2, 3220, 8, 1760, 12,
507 2062, 3845, 18, 4063, 22, 3418, 1770, 28, 2758, 2063, 33, 1776,
508 4014, 38, 1780, 43, 2938, 3760, 49, 2073, 53, 3423, 3653, 59,
509 2583, 63, 4039, 2942, 69, 2083, 2092, 74, 3811, 79, 1801, 2088,
510 84, 3343, 90, 3323, 94, 2103, 1811, 100, 3219, 2098, 105, 1817,
511 3767, 110, 1821, 115, 3434, 3516, 121, 1827, 125, 3101, 2958, 131,
512 2114, 135, 3438, 2610, 141, 1837, 2119, 146, 3850, 151, 3354, 2124,
513 156, 2620, 162, 2371, 166, 1852, 3817, 172, 4090, 2135, 177, 1858,
514 4066, 182, 1862, 187, 3908, 3116, 193, 1868, 197, 3448, 2815, 203,
515 3678, 207, 2984, 4003, 213, 1878, 2164, 218, 2641, 223, 2820, 2160,
516 228, 3855, 234, 2411, 238, 1893, 4091, 244, 3538, 2170, 249, 3556,
517 3142, 254, 2176, 259, 1904, 3816, 265, 3733, 269, 3137, 3000, 275,
518 1914, 279, 3459, 3277, 285, 1920, 2191, 290, 1924, 295, 3144, 2196,
519 300, 4017, 306, 2442, 310, 1934, 3384, 316, 3385, 2207, 321, 3469,
520 2443, 326, 3941, 331, 1945, 3931, 337, 2217, 341, 3628, 3824, 347,
521 1955, 351, 3025, 3157, 357, 1961, 2236, 362, 1965, 367, 4074, 2232,
522 372, 1971, 378, 3557, 382, 2247, 2702, 388, 3891, 2242, 393, 1981,
523 3865, 398, 2248, 403, 3485, 3741, 409, 2713, 413, 3173, 3041, 419,
524 2258, 423, 4068, 2717, 429, 2002, 2263, 434, 2006, 439, 3179, 2268,
525 444, 2012, 450, 4027, 454, 3490, 3870, 460, 2898, 2279, 465, 2022,
526 2514, 470, 3415, 475, 3061, 3188, 481, 2289, 485, 3495, 2515, 491,
527 3755, 495, 3203, 3301, 501, 2299, 2308, 506, 2748, 511, 2048, 2304,
528 516, 3901, 522, 4080, 526, 2319, 2058, 532, 2923, 2314, 537, 2064,
529 3214, 542, 2068, 547, 3506, 3832, 553, 3431, 557, 3209, 3082, 563,
530 2330, 567, 3510, 3876, 573, 4069, 2335, 578, 3847, 583, 2089, 2340,
531 588, 3344, 594, 4060, 598, 3659, 2099, 604, 3971, 2351, 609, 2105,
532 3588, 614, 2109, 619, 3102, 3328, 625, 2115, 629, 3520, 2586, 635,
533 2799, 639, 3770, 3229, 645, 2125, 2380, 650, 3724, 655, 3721, 2376,
534 660, 3460, 666, 3529, 670, 2140, 2810, 676, 3910, 2386, 681, 2146,
535 3814, 686, 2150, 691, 3853, 3674, 697, 2156, 701, 3245, 4089, 707,
536 2402, 711, 3531, 2826, 717, 2166, 2407, 722, 3374, 727, 2627, 2412,
537 732, 2836, 738, 2967, 742, 2181, 3679, 748, 3368, 2423, 753, 3541,
538 3363, 758, 3790, 763, 2192, 3260, 769, 2433, 773, 4053, 3613, 779,
539 2202, 783, 3275, 3148, 789, 2208, 2452, 794, 2212, 799, 2649, 2448,
540 804, 3785, 810, 3554, 814, 2222, 3939, 820, 2659, 2458, 825, 3395,
541 3286, 830, 2464, 835, 2233, 3860, 841, 3833, 845, 3281, 4062, 851,
542 2243, 855, 3923, 3401, 861, 2249, 2479, 866, 2253, 871, 3629, 2484,
543 876, 2259, 882, 3564, 886, 3562, 3492, 892, 2690, 2495, 897, 2269,
544 2865, 902, 4061, 907, 3185, 3399, 913, 2505, 917, 3567, 3482, 923,
545 2908, 927, 3499, 3189, 933, 2290, 2524, 938, 2294, 943, 2720, 2520,
546 948, 2300, 954, 4020, 958, 2535, 2918, 964, 2730, 2530, 969, 2310,
547 3839, 974, 2536, 979, 3578, 2731, 985, 2929, 989, 3317, 3205, 995,
548 2546, 999, 3582, 2933, 1005, 3927, 2551, 1010, 2939, 1015, 2336, 2556,
549 1020, 2943, 3, 4050, 9, 13, 2346, 1036, 19, 23, 1041, 29,
550 3851, 1046, 34, 1051, 39, 44, 1057, 2577, 50, 54, 2936, 1067,
551 60, 64, 3347, 70, 1077, 2587, 75, 80, 2964, 85, 2377, 91,
552 95, 3657, 101, 3873, 1102, 106, 2387, 111, 116, 2602, 1113, 122,
553 126, 1118, 2397, 132, 136, 2802, 142, 2403, 1133, 147, 152, 1139,
554 157, 1143, 163, 167, 1149, 173, 2623, 1154, 178, 1159, 183, 188,
555 1164, 3917, 194, 198, 1174, 2428, 204, 208, 3134, 214, 1185, 2434,
556 219, 224, 2438, 229, 3378, 235, 239, 2444, 245, 3735, 4067, 250,
557 3015, 255, 260, 3373, 1221, 266, 270, 1226, 3690, 276, 280, 2664,
558 286, 3559, 1242, 291, 296, 2469, 301, 1252, 307, 311, 1257, 317,
559 4007, 1262, 322, 1267, 327, 332, 1273, 3036, 338, 342, 3288, 1283,
560 348, 352, 3919, 358, 1293, 2496, 363, 368, 2500, 373, 3175, 379,
561 383, 3052, 389, 2875, 1318, 394, 3872, 399, 404, 2711, 1329, 410,
562 414, 1334, 3867, 420, 424, 3404, 430, 2721, 1349, 435, 440, 1355,
563 445, 1359, 451, 455, 1365, 461, 2740, 1370, 466, 1375, 471, 476,
564 1380, 2547, 482, 486, 1390, 2751, 492, 496, 3841, 502, 1401, 2557,
565 507, 512, 2752, 517, 3650, 523, 527, 3806, 533, 3425, 3329, 538,
566 2762, 543, 548, 3595, 1437, 554, 558, 1442, 2582, 564, 568, 2772,
567 574, 2588, 1458, 579, 584, 3909, 589, 1468, 595, 599, 1473, 605,
568 2947, 1478, 610, 1483, 615, 620, 1489, 2793, 626, 630, 3907, 1499,
569 636, 640, 3607, 646, 1509, 2803, 651, 656, 3610, 661, 2624, 667,
570 671, 3862, 677, 3722, 1534, 682, 2634, 687, 692, 2818, 1545, 698,
571 702, 1550, 2644, 708, 712, 3361, 718, 3145, 1565, 723, 728, 1571,
572 733, 1575, 739, 743, 1581, 749, 2839, 1586, 754, 1591, 759, 764,
573 1596, 3159, 770, 774, 1606, 4065, 780, 784, 3787, 790, 1617, 2681,
574 795, 800, 2685, 805, 3390, 811, 815, 2691, 821, 3920, 3019, 826,
575 4038, 831, 836, 3616, 1653, 842, 846, 1658, 3180, 852, 856, 2880,
576 862, 4021, 1674, 867, 872, 2716, 877, 1684, 883, 887, 1689, 893,
577 3502, 1694, 898, 1699, 903, 908, 1705, 2732, 914, 918, 3795, 1715,
578 924, 928, 4075, 934, 1725, 2742, 939, 944, 3590, 949, 3794, 955,
579 959, 3882, 965, 3579, 1750, 970, 3903, 975, 980, 2927, 1761, 986,
580 990, 1766, 3952, 996, 1000, 4006, 1006, 2937, 1781, 1011, 1016, 1787,
581 1021, 1791, 1027, 1031, 1797, 1037, 2956, 1802, 1042, 1807, 1047, 1052,
582 1812, 3676, 1058, 1062, 1822, 2798, 1068, 1072, 3932, 1078, 1833, 3247,
583 1083, 1088, 2968, 1093, 2809, 1099, 1103, 3252, 1109, 3533, 4004, 1114,
584 2819, 1119, 1124, 3258, 1869, 1130, 1134, 1874, 2829, 1140, 1144, 2988,
585 1150, 2835, 1890, 1155, 1160, 3940, 1165, 1900, 1171, 1175, 1905, 1181,
586 3904, 1910, 1186, 1915, 1191, 1196, 1921, 3009, 1202, 1206, 3859, 1931,
587 1212, 1216, 3563, 1222, 1941, 2866, 1227, 1232, 2870, 1237, 3153, 1243,
588 1247, 2876, 1253, 3391, 1966, 1258, 3864, 1263, 1268, 3034, 1977, 1274,
589 1278, 1982, 3040, 1284, 1288, 3982, 1294, 3797, 1997, 1299, 1304, 2003,
590 1309, 2007, 1315, 1319, 2013, 1325, 3055, 2018, 1330, 2023, 1335, 1340,
591 2028, 3899, 1346, 1350, 2038, 3950, 1356, 1360, 3194, 1366, 2049, 2928,
592 1371, 1376, 2932, 1381, 3514, 1387, 1391, 3081, 1397, 3844, 3651, 1402,
593 3340, 1407, 1412, 3518, 2085, 1418, 1422, 2090, 3719, 1428, 1432, 3096,
594 1438, 4085, 2106, 1443, 1448, 3111, 1453, 2116, 1459, 1463, 2121, 1469,
595 3972, 2126, 1474, 2131, 1479, 1484, 2137, 2979, 1490, 1494, 3534, 2147,
596 1500, 1504, 4078, 1510, 2157, 2989, 1515, 1520, 3371, 1525, 3611, 1531,
597 1535, 3375, 1541, 3463, 2182, 1546, 3889, 1551, 1556, 3143, 2193, 1562,
598 1566, 2198, 3014, 1572, 1576, 3620, 1582, 3020, 2213, 1587, 1592, 2219,
599 1597, 2223, 1603, 1607, 2229, 1613, 3172, 2234, 1618, 2239, 1623, 1628,
600 2244, 3978, 1634, 1638, 2254, 3045, 1644, 1648, 3829, 1654, 2265, 3838,
601 1659, 1664, 3184, 1669, 3056, 1675, 1679, 3754, 1685, 3641, 3576, 1690,
602 3066, 1695, 1700, 3709, 2301, 1706, 1710, 2306, 3076, 1716, 1720, 3204,
603 1726, 3989, 2322, 1731, 1736, 3086, 1741, 2332, 1747, 1751, 2337, 1757,
604 3879, 2342, 1762, 2347, 1767, 1772, 2353, 3225, 1778, 1782, 4054, 2363,
605 1788, 1792, 3601, 1798, 2373, 3113, 1803, 1808, 3117, 1813, 3913, 1819,
606 1823, 3123, 1829, 3720, 2398, 1834, 3458, 1839, 1844, 3250, 2409, 1850,
607 1854, 2414, 3256, 1860, 1864, 4084, 1870, 3468, 2429, 1875, 1880, 2435,
608 1885, 2439, 1891, 1895, 2445, 1901, 3271, 2450, 1906, 2455, 1911, 1916,
609 2460, 3164, 1922, 1926, 2470, 3981, 1932, 1936, 3976, 1942, 2481, 3174,
610 1947, 1952, 3895, 1957, 3637, 1963, 1967, 3297, 1973, 4043, 3571, 1978,
611 3925, 1983, 1988, 3828, 2517, 1994, 1998, 2522, 3505, 2004, 2008, 3312,
612 2014, 3999, 2538, 2019, 2024, 3327, 2029, 2548, 2035, 2039, 2553, 2045,
613 3718, 2558, 2050, 2563, 2055, 2060, 2569, 3949, 2066, 2070, 3658, 2579,
614 2076, 2080, 4072, 2086, 2589, 3440, 2091, 2096, 4013, 2101, 3241, 2107,
615 2111, 3776, 2117, 3450, 2614, 2122, 3251, 2127, 2132, 3359, 2625, 2138,
616 2142, 2630, 3261, 2148, 2152, 3805, 2158, 3267, 2645, 2163, 2168, 2651,
617 2173, 2655, 2179, 2183, 2661, 2189, 3388, 2666, 2194, 2671, 2199, 2204,
618 2676, 4055, 2210, 2214, 2686, 3292, 2220, 2224, 4033, 2230, 2697, 3298,
619 2235, 2240, 3302, 2245, 3866, 2251, 2255, 3308, 2261, 3749, 4040, 2266,
620 3410, 2271, 2276, 3581, 2733, 2282, 2286, 2738, 3587, 2292, 2296, 3420,
621 2302, 3591, 2754, 2307, 2312, 3333, 2317, 2764, 2323, 2327, 2769, 2333,
622 3522, 2774, 2338, 2779, 2343, 2348, 2785, 3441, 2354, 2358, 3523, 2795,
623 2364, 2368, 3779, 2374, 2805, 3360, 2379, 2384, 3364, 2389, 3892, 2395,
624 2399, 3883, 2405, 3975, 2830, 2410, 3622, 2415, 2420, 3466, 2841, 2426,
625 2430, 2846, 3472, 2436, 2440, 3888, 2446, 3863, 2861, 2451, 2456, 2867,
626 2461, 2871, 2467, 2471, 2877, 2477, 3487, 2882, 2482, 2887, 2487, 2492,
627 2892, 3411, 2498, 2502, 2902, 3947, 2508, 2512, 3944, 2518, 2913, 3421,
628 2523, 2528, 4024, 2533, 3761, 2539, 2543, 3513, 2549, 3951, 3594, 2554,
629 3663, 2559, 2564, 3765, 2949, 2570, 2574, 2954, 3446, 2580, 2584, 3528,
630 2590, 3452, 2970, 2595, 2600, 3543, 2605, 2980, 2611, 2615, 2985, 2621,
631 4059, 2990, 2626, 2995, 2631, 2636, 3001, 3684, 2642, 2646, 3781, 3011,
632 2652, 2656, 4036, 2662, 3021, 4018, 2667, 2672, 3868, 2677, 3488, 2683,
633 2687, 3700, 2693, 3993, 3046, 2698, 3498, 2703, 2708, 3575, 3057, 2714,
634 2718, 3062, 3508, 2724, 2728, 3836, 2734, 4, 14, 24, 30, 40,
635 45, 55, 65, 71, 81, 86, 96, 102, 112, 117, 127, 137,
636 143, 153, 158, 168, 174, 184, 189, 199, 209, 215, 225, 230,
637 240, 246, 256, 261, 271, 281, 287, 297, 302, 312, 318, 328,
638 333, 343, 353, 359, 369, 374, 384, 390, 400, 405, 415, 425,
639 431, 441, 446, 456, 462, 472, 477, 487, 497, 503, 513, 518,
640 528, 534, 544, 549, 559, 569, 575, 585, 590, 600, 606, 616,
641 621, 631, 641, 647, 657, 662, 672, 678, 688, 693, 703, 713,
642 719, 729, 734, 744, 750, 760, 765, 775, 785, 791, 801, 806,
643 816, 822, 832, 837, 847, 857, 863, 873, 878, 888, 894, 904,
644 909, 919, 929, 935, 945, 950, 960, 966, 976, 981, 991, 1001,
645 1007, 1017, 1022, 1032, 1038, 1048, 1053, 1063, 1073, 1079, 1089, 1094,
646 1104, 1110, 1120, 1125, 1135, 1145, 1151, 1161, 1166, 1176, 1182, 1192,
647 1197, 1207, 1217, 1223, 1233, 1238, 1248, 1254, 1264, 1269, 1279, 1289,
648 1295, 1305, 1310, 1320, 1326, 1336, 1341, 1351, 1361, 1367, 1377, 1382,
649 1392, 1398, 1408, 1413, 1423, 1433, 1439, 1449, 1454, 1464, 1470, 1480,
650 1485, 1495, 1505, 1511, 1521, 1526, 1536, 1542, 1552, 1557, 1567, 1577,
651 1583, 1593, 1598, 1608, 1614, 1624, 1629, 1639, 1649, 1655, 1665, 1670,
652 1680, 1686, 1696, 1701, 1711, 1721, 1727, 1737, 1742, 1752, 1758, 1768,
653 1773, 1783, 1793, 1799, 1809, 1814, 1824, 1830, 1840, 1845, 1855, 1865,
654 1871, 1881, 1886, 1896, 1902, 1912, 1917, 1927, 1937, 1943, 1953, 1958,
655 1968, 1974, 1984, 1989, 1999, 2009, 2015, 2025, 2030, 2040, 2046, 2056,
656 2061, 2071, 2081, 2087, 2097, 2102, 2112, 2118, 2128, 2133, 2143, 2153,
657 2159, 2169, 2174, 2184, 2190, 2200, 2205, 2215, 2225, 2231, 2241, 2246,
658 2256, 2262, 2272, 2277, 2287, 2297, 2303, 2313, 2318, 2328, 2334, 2344,
659 2349, 2359, 2369, 2375, 2385, 2390, 2400, 2406, 2416, 2421, 2431, 2441,
660 2447, 2457, 2462, 2472, 2478, 2488, 2493, 2503, 2513, 2519, 2529, 2534,
661 2544, 2550, 2560, 2565, 2575, 2585, 2591, 2601, 2606, 2616, 2622, 2632,
662 2637, 2647, 2657, 2663, 2673, 2678, 2688, 2694, 2704, 2709, 2719, 2729,
663 2735, 2745, 2750, 2760, 2766, 2776, 2781, 2791, 2801, 2807, 2817, 2822,
664 2832, 2838, 2848, 2853, 2863, 2873, 2879, 2889, 2894, 2904, 2910, 2920,
665 2925, 2935, 2945, 2951, 2961, 2966, 2976, 2982, 2992, 2997, 3007, 3017,
666 3023, 3033, 3038, 3048, 3054, 3064, 3069, 3079, 3089, 3095, 3105, 3110,
667 3120, 3126, 3136, 3141, 3151, 3161, 3167, 3177, 3182, 3192, 3198, 3208,
668 3213, 3223, 3233, 3239, 3249, 3254, 3264, 3270, 3280, 3285, 3295, 3305,
669 3311, 3321, 3326, 3336, 3342, 3352, 3357, 3367, 3377, 3383, 3393, 3398,
670 3408, 3414, 3424, 3429, 3439, 3449, 3455, 3465, 3470, 3480, 3486, 3496,
671 3501, 3511, 3521, 3527, 3537, 3542, 3552, 3558, 3568, 3573, 3583, 3593,
672 3599, 3609, 3614, 3624, 3630, 3640, 3645, 3655, 3665, 3671, 3681, 3686,
673 3696, 3702, 3712, 3717, 3727, 3737, 3743, 3753, 3758, 3768, 3774, 3784,
674 3789, 3799, 3809, 3815, 3825, 3830, 3840, 3846, 3856, 3861, 3871, 3881,
675 3887, 3897, 3902, 3912, 3918, 3928, 3933, 3943, 3953, 3959, 3969, 3974,
676 3984, 3990, 4000, 4005, 4015, 4025, 4031, 4041, 4046, 4056, 4086, 4088,
677 4092, 4093, 5
678};
679
680static const int bmkiller_4096[] = {
681 0, 4051, 3947, 3998, 6, 16, 2735, 1031, 3081, 3202, 11, 3586,
682 2347, 2063, 530, 17, 26, 3078, 3508, 21, 2568, 2762, 2058, 1766,
683 2758, 27, 36, 2740, 2353, 3331, 3657, 32, 2745, 2357, 2073, 2316,
684 37, 47, 3227, 2068, 2546, 42, 3084, 3333, 2574, 3655, 48, 57,
685 2750, 3212, 52, 3593, 1062, 1787, 2321, 2768, 58, 67, 3088, 571,
686 62, 1072, 3955, 3339, 1791, 566, 68, 77, 2756, 3231, 1797, 1778,
687 73, 2760, 2597, 3429, 3712, 78, 88, 1083, 2949, 4088, 83, 3094,
688 1088, 3907, 1463, 89, 98, 2766, 3601, 93, 1093, 2593, 2094, 1807,
689 593, 99, 108, 3605, 1099, 3525, 2784, 104, 3099, 2608, 3598, 612,
690 109, 119, 1109, 3765, 3338, 114, 2771, 3661, 2114, 2361, 120, 129,
691 3104, 2356, 124, 3359, 2394, 3349, 2109, 3228, 130, 139, 2776, 2941,
692 134, 3726, 1124, 1833, 3881, 3665, 140, 149, 2781, 1130, 3813, 634,
693 145, 3109, 3354, 3603, 3125, 150, 160, 3247, 1843, 644, 155, 4002,
694 2619, 2135, 2582, 161, 170, 2787, 3996, 165, 3463, 3604, 2130, 1849,
695 664, 171, 180, 2791, 2414, 3122, 3238, 176, 3119, 3545, 2145, 3607,
696 181, 191, 3814, 2140, 2809, 186, 3616, 2629, 3258, 675, 192, 201,
697 2797, 1850, 196, 4053, 1171, 2155, 2392, 2824, 202, 211, 2801, 2975,
698 206, 1181, 3915, 1874, 2150, 3936, 212, 221, 3668, 2640, 2393, 705,
699 217, 2807, 3140, 3853, 3457, 222, 232, 1191, 1884, 715, 227, 3130,
700 1196, 3455, 4046, 233, 242, 3546, 716, 237, 1202, 3613, 2166, 1890,
701 1562, 243, 252, 2812, 1206, 2995, 3462, 248, 2817, 1212, 1900, 2172,
702 253, 263, 1216, 3886, 2835, 258, 3550, 3273, 2186, 746, 264, 273,
703 2822, 3676, 268, 2669, 2455, 1910, 2181, 1168, 274, 283, 3939, 3730,
704 278, 3916, 1232, 2196, 3938, 3156, 284, 293, 2828, 1237, 3626, 2666,
705 289, 2832, 3468, 3465, 3828, 294, 304, 1247, 3153, 3783, 299, 3556,
706 3027, 2207, 1603, 305, 314, 2838, 787, 309, 2675, 3554, 2202, 1931,
707 782, 315, 324, 3858, 3032, 3690, 3131, 320, 3823, 2681, 1941, 1209,
708 325, 335, 2481, 2212, 3548, 330, 2843, 3686, 2683, 1623, 336, 345,
709 3627, 1628, 340, 3390, 1278, 1951, 2858, 809, 346, 355, 2848, 3477,
710 350, 1288, 2491, 3567, 2222, 3478, 356, 365, 2853, 3043, 2464, 3628,
711 361, 3895, 2696, 3476, 2460, 366, 376, 1299, 3995, 3472, 371, 3166,
712 1304, 3480, 3492, 377, 386, 2859, 3013, 381, 1309, 2701, 2238, 3789,
713 2885, 387, 396, 2863, 1315, 1977, 850, 392, 3171, 2511, 3634, 1664,
714 397, 407, 1325, 2475, 860, 402, 4023, 3746, 1987, 3170, 408, 417,
715 2869, 3695, 412, 3897, 3752, 1993, 2253, 880, 418, 427, 2873, 3191,
716 422, 2522, 1340, 2268, 1997, 881, 428, 437, 3637, 1346, 3571, 2891,
717 433, 2879, 3640, 3639, 900, 438, 448, 3925, 3052, 3698, 443, 4009,
718 2532, 2279, 2505, 449, 458, 3187, 2500, 453, 3838, 3314, 2274, 3751,
719 3300, 459, 468, 2884, 2538, 2018, 921, 464, 2889, 2542, 2289, 2281,
720 469, 479, 3648, 2284, 931, 474, 3581, 2737, 2028, 1720, 480, 489,
721 2894, 932, 484, 2916, 1387, 2034, 2510, 3587, 490, 499, 3197, 3573,
722 494, 1397, 3949, 2744, 2038, 952, 500, 509, 2900, 2747, 2044, 3310,
723 505, 2904, 3431, 3501, 3054, 510, 520, 1407, 1, 2917, 515, 7,
724 1412, 3650, 963, 521, 12, 2910, 1354, 525, 1418, 18, 2310, 2054,
725 22, 531, 540, 4065, 1422, 28, 1757, 536, 3207, 1428, 3844, 33,
726 541, 551, 1432, 38, 3320, 546, 2915, 43, 2330, 3931, 552, 561,
727 49, 1003, 556, 53, 2579, 2075, 2325, 998, 562, 59, 2920, 1004,
728 63, 3433, 1448, 2340, 2079, 69, 572, 581, 2925, 1453, 2085, 74,
729 577, 3218, 2947, 79, 3988, 582, 592, 84, 3093, 2779, 587, 3597,
730 90, 2351, 1034, 94, 602, 2931, 4050, 597, 100, 3232, 2346, 2095,
731 3203, 603, 105, 2935, 2599, 3438, 110, 608, 4017, 4033, 115, 2569,
732 613, 623, 3350, 121, 2572, 618, 125, 3518, 2790, 2953, 624, 633,
733 131, 3085, 628, 135, 1494, 2371, 3533, 3225, 141, 643, 2945, 1075,
734 638, 1504, 146, 2121, 2366, 1070, 151, 653, 3849, 3446, 156, 1456,
735 649, 2951, 2813, 162, 3971, 654, 166, 1515, 2131, 4012, 659, 172,
736 1520, 3527, 1839, 665, 674, 177, 1844, 669, 1525, 182, 2382, 2137,
737 1097, 187, 684, 2956, 1531, 4049, 193, 680, 2961, 197, 3670, 1116,
738 685, 695, 1541, 203, 3774, 690, 207, 3673, 2402, 3885, 696, 213,
739 2966, 3115, 700, 3887, 2641, 218, 2397, 3965, 706, 223, 3729, 3110,
740 710, 228, 1556, 2162, 2609, 2984, 234, 725, 2972, 238, 3129, 1138,
741 721, 2976, 244, 3537, 1880, 726, 736, 3371, 249, 1148, 731, 3956,
742 254, 2423, 3937, 737, 259, 2982, 3609, 741, 3150, 265, 2418, 2178,
743 269, 747, 756, 4095, 3269, 3139, 275, 752, 3263, 279, 2188, 3126,
744 757, 767, 285, 2428, 4029, 762, 2987, 2845, 290, 1179, 768, 777,
745 295, 4003, 772, 3733, 300, 2198, 3732, 4031, 778, 306, 2992, 2644,
746 310, 1613, 2676, 2852, 2438, 316, 788, 797, 2997, 2856, 3822, 321,
747 793, 3683, 3019, 326, 2659, 798, 808, 331, 3859, 1219, 803, 3274,
748 337, 3552, 1936, 341, 818, 3003, 1220, 813, 1634, 347, 2454, 2219,
749 351, 819, 828, 3007, 1638, 357, 3029, 824, 3279, 1644, 2229, 362,
750 829, 839, 1648, 367, 1952, 834, 3689, 372, 2474, 1250, 840, 849,
751 378, 3025, 844, 382, 2702, 2239, 2469, 1601, 388, 859, 3017, 3688,
752 854, 3894, 393, 2484, 2680, 3040, 398, 869, 3740, 1669, 403, 1973,
753 865, 3023, 4030, 409, 2690, 870, 413, 1679, 3297, 3157, 875, 3794,
754 419, 2495, 2887, 423, 890, 3294, 1291, 885, 429, 3643, 2490, 3292,
755 1286, 891, 434, 3028, 2723, 2265, 439, 896, 3033, 2727, 444, 1642,
756 901, 911, 3702, 450, 3747, 906, 454, 3964, 2275, 3494, 912, 460,
757 3038, 3051, 916, 3498, 1710, 465, 3923, 1313, 922, 470, 3304, 3748,
758 926, 475, 2907, 3981, 2285, 1672, 481, 941, 3044, 485, 3635, 3410,
759 937, 3048, 2912, 491, 3291, 942, 495, 1731, 3196, 2716, 947, 501,
760 1736, 3899, 3061, 953, 962, 506, 3182, 957, 1741, 511, 2526, 3836,
761 4059, 516, 972, 3704, 1747, 2306, 522, 968, 3315, 526, 3706, 2923,
762 973, 983, 532, 3803, 1364, 978, 3059, 3709, 537, 2897, 984, 993,
763 542, 3645, 988, 3758, 547, 2322, 2541, 1384, 994, 553, 3064, 2060,
764 557, 2769, 1772, 2556, 2326, 1385, 563, 1013, 3069, 567, 2332, 2066,
765 1009, 3325, 573, 3711, 1404, 1014, 1024, 3091, 578, 3969, 1019, 3808,
766 583, 2567, 4072, 1025, 588, 3075, 3513, 1029, 3437, 594, 2562, 2342,
767 598, 1035, 1044, 3079, 2785, 604, 1425, 1040, 3335, 2789, 2577, 609,
768 1045, 1055, 3876, 614, 1435, 1050, 3663, 619, 3443, 2954, 1056, 1065,
769 625, 1436, 1060, 629, 1819, 2363, 3707, 2101, 1066, 635, 3089, 3767,
770 639, 1829, 3243, 2960, 2367, 645, 1076, 1085, 3770, 2963, 2373, 650,
771 1081, 3095, 3912, 655, 3219, 1086, 1096, 660, 3237, 3235, 1091, 3346,
772 666, 3599, 1467, 670, 1106, 3974, 2078, 1101, 676, 3356, 2598, 2383,
773 2974, 1107, 681, 3100, 1854, 3669, 686, 1112, 3105, 1860, 691, 2604,
774 1117, 1127, 1864, 697, 3229, 1122, 701, 3727, 2618, 2142, 1128, 1137,
775 707, 1507, 1132, 711, 2826, 4035, 2613, 1502, 717, 1147, 3674, 1508,
776 1142, 3132, 722, 2409, 2798, 3366, 727, 1157, 3116, 1885, 732, 3128,
777 1153, 3120, 3776, 738, 4020, 1158, 742, 1895, 2419, 2168, 1163, 748,
778 3739, 2639, 1538, 1169, 1178, 753, 3133, 1173, 3000, 758, 2634, 2425,
779 3959, 763, 1188, 4083, 2846, 3547, 769, 1184, 4027, 773, 2649, 2420,
780 1189, 1199, 3474, 779, 2979, 1194, 783, 3549, 3006, 3266, 1200, 789,
781 3684, 3254, 1204, 3737, 1926, 794, 2825, 3781, 1210, 799, 3136, 1579,
782 1214, 804, 3633, 2450, 2654, 1574, 810, 1229, 3141, 814, 3622, 1889,
783 1225, 4074, 820, 3620, 3475, 1230, 1240, 1947, 825, 3681, 1235, 3382,
784 830, 3624, 3370, 1241, 835, 3147, 3962, 1245, 1957, 841, 2670, 2466,
785 845, 1251, 1260, 3151, 1963, 3283, 851, 1256, 3387, 855, 2476, 1620,
786 1261, 1271, 861, 3943, 1929, 1266, 3694, 3164, 866, 2865, 1272, 1281,
787 871, 2860, 1276, 3575, 876, 2486, 2685, 3275, 1282, 882, 3161, 4024,
788 886, 3835, 1988, 2700, 3632, 892, 1292, 1301, 3745, 1994, 3993, 897,
789 1297, 3167, 3570, 902, 3407, 1302, 1312, 907, 3922, 1652, 1307, 3700,
790 913, 2711, 3290, 917, 1322, 3403, 3692, 1317, 3649, 923, 2706, 2507,
791 927, 1323, 1332, 3172, 4010, 933, 3490, 1328, 3177, 3653, 2517, 938,
792 1333, 1343, 2913, 943, 3307, 1338, 3760, 948, 3505, 1683, 1344, 1353,
793 954, 2512, 1348, 958, 2035, 2527, 2896, 2292, 964, 1363, 3413, 3050,
794 1358, 2045, 969, 3068, 2726, 4038, 974, 1373, 3188, 3072, 979, 1713,
795 1369, 3192, 3401, 985, 3699, 1374, 989, 2055, 3705, 1723, 1379, 3418,
796 995, 3757, 3578, 999, 1394, 3198, 1724, 1389, 1005, 4048, 2742, 3927,
797 2317, 1395, 1010, 3935, 2070, 2553, 1015, 1400, 3423, 2076, 1020, 2748,
798 1405, 1415, 2080, 1026, 3811, 1410, 1030, 3716, 2563, 1754, 1416, 1036,
799 3428, 3997, 1420, 3101, 3092, 1041, 2757, 2294, 1426, 1046, 3208, 3875,
800 1430, 1051, 2096, 2772, 2573, 3930, 1057, 1445, 3213, 1061, 3715, 3098,
801 1441, 3434, 3667, 1067, 3222, 1446, 1071, 2111, 3340, 3326, 1451, 1077,
802 2964, 2783, 2358, 1457, 1466, 1082, 1795, 1461, 3107, 1087, 2778, 3436,
803 1790, 1092, 1476, 3223, 2970, 2594, 1098, 1472, 3906, 1102, 2793, 3074,
804 1477, 1487, 1108, 2788, 3717, 1482, 3444, 3236, 1113, 2379, 1488, 1497,
805 1118, 2384, 1492, 3606, 1123, 2610, 3878, 1817, 1498, 1129, 3233, 3241,
806 1133, 2152, 3123, 3540, 2614, 2105, 1139, 1517, 4084, 1143, 2620, 3772,
807 1513, 3239, 1149, 3989, 2124, 1518, 1528, 2163, 1154, 3351, 1523, 3454,
808 1159, 3671, 3724, 1529, 1164, 3731, 3536, 1533, 2173, 1170, 2814, 2630,
809 1174, 1539, 1548, 3244, 2179, 1180, 1858, 1544, 3249, 3005, 3778, 1185,
810 1549, 1559, 2189, 1190, 1868, 1554, 3735, 1195, 2834, 3458, 1560, 1569,
811 1201, 3819, 1564, 1205, 3011, 2651, 2829, 1888, 1570, 1211, 4078, 3267,
812 1215, 4036, 2204, 2844, 2655, 1221, 1580, 1589, 3260, 2210, 2661, 1226,
813 1585, 3264, 3784, 1231, 1908, 1590, 1600, 1236, 3381, 3917, 1595, 3741,
814 1242, 2855, 3009, 1246, 1610, 3270, 3004, 1605, 1252, 3561, 2850, 2671,
815 3832, 1611, 1257, 4052, 3031, 3482, 1262, 1616, 3479, 3397, 1267, 2857,
816 1621, 1631, 3485, 1273, 1939, 1626, 1277, 3169, 3566, 2477, 1632, 1641,
817 1283, 1940, 1636, 1287, 2251, 2875, 3014, 3288, 1293, 1651, 3280, 3961,
818 1646, 2261, 1298, 2697, 2870, 1960, 1303, 1661, 3285, 3179, 1308, 3562,
819 1657, 3792, 3647, 1314, 3793, 1662, 1318, 2271, 2707, 3693, 1667, 1324,
820 2276, 3696, 1971, 1673, 1682, 1329, 3984, 1677, 2282, 1334, 2886, 2713,
821 2508, 1339, 1692, 3295, 2286, 3801, 1345, 1688, 3495, 1349, 3946, 2892,
822 1693, 1703, 2296, 1355, 3398, 1698, 1359, 3799, 2906, 3308, 1704, 1365,
823 3301, 2011, 1708, 3200, 3073, 1370, 2901, 2006, 1714, 1375, 3305, 2012,
824 1718, 1380, 2312, 2738, 3184, 2533, 1386, 1733, 4043, 1390, 3417, 3420,
825 1729, 3311, 1396, 4077, 3585, 1734, 1744, 2327, 1401, 3211, 1739, 3802,
826 1406, 2927, 2042, 1745, 1411, 3510, 3967, 1749, 3216, 1417, 2922, 2754,
827 1421, 1755, 1764, 3316, 3805, 3427, 1427, 1760, 3321, 1431, 2764, 3968,
828 1765, 1775, 1437, 2932, 3076, 1770, 3516, 3804, 1442, 3870, 1776, 1785,
829 1447, 3843, 1780, 3809, 1452, 2774, 3999, 3714, 1786, 1458, 3520, 2083,
830 1462, 2368, 3108, 3773, 2942, 1468, 1796, 1805, 3332, 3662, 3086, 1473,
831 1801, 3336, 3245, 1478, 3763, 1806, 1816, 1483, 3590, 3764, 1811, 3526,
832 1489, 4013, 2595, 1493, 1826, 3342, 2600, 1821, 2389, 1499, 2958, 2795,
833 1503, 1827, 1836, 3821, 2395, 1509, 2605, 1832, 3531, 3256, 2805, 1514,
834 1837, 1847, 2405, 1519, 2362, 1842, 3347, 1524, 2978, 3850, 1848, 1857,
835 1530, 3448, 1852, 1534, 3134, 2815, 2973, 4071, 1540, 1867, 3352, 3445,
836 1862, 3978, 1545, 2988, 3113, 3452, 1550, 1877, 3357, 2426, 1555, 2146,
837 1873, 3541, 3678, 1561, 2636, 1878, 1565, 3618, 3958, 2156, 1883, 3992,
838 1571, 2999, 3957, 1575, 1898, 3363, 3855, 1893, 1581, 3820, 2994, 4058,
839 2176, 1899, 1586, 3367, 3155, 2841, 1591, 1904, 3551, 3159, 1596, 3619,
840 1909, 1919, 3787, 1602, 3824, 1914, 1606, 3277, 2851, 2187, 1920, 1612,
841 3373, 2433, 1924, 3380, 2467, 1617, 3779, 3827, 1930, 1622, 3377, 3148,
842 1934, 1627, 3891, 3284, 2861, 4080, 1633, 1949, 3987, 1637, 3749, 2217,
843 1945, 3383, 3980, 1643, 3163, 1950, 1647, 2487, 3484, 2227, 1955, 1653,
844 2492, 3743, 2693, 1961, 1970, 1658, 2228, 1965, 2498, 1663, 3030, 3963,
845 3395, 1668, 1980, 3388, 2502, 2882, 1674, 1976, 3393, 1678, 4082, 3036,
846 1981, 1991, 1684, 3986, 2708, 1986, 3797, 3708, 1689, 2258, 1992, 2001,
847 1694, 4045, 1996, 3317, 1699, 2898, 3045, 3406, 2002, 1705, 4011, 3636,
848 1709, 3201, 2528, 3060, 2902, 2724, 1715, 2021, 3404, 1719, 2908, 2728,
849 2017, 3408, 1725, 3753, 3194, 2022, 2032, 2543, 1730, 3644, 2027, 3901,
850 1735, 3071, 3319, 2033, 1740, 3414, 2299, 2037, 3323, 1746, 3066, 2918,
851 1750, 2043, 2052, 3966, 3217, 1756, 3504, 2048, 2, 3221, 8, 1761,
852 2053, 13, 3846, 19, 4064, 23, 3419, 1771, 29, 2759, 2064, 34,
853 1777, 4015, 39, 1781, 44, 2939, 3761, 50, 2074, 54, 3424, 3654,
854 60, 2584, 64, 4040, 2943, 70, 2084, 2093, 75, 3812, 80, 1802,
855 2089, 85, 3344, 91, 3324, 95, 2104, 1812, 101, 3220, 2099, 106,
856 1818, 3768, 111, 1822, 116, 3435, 3517, 122, 1828, 126, 3102, 2959,
857 132, 2115, 136, 3439, 2611, 142, 1838, 2120, 147, 3851, 152, 3355,
858 2125, 157, 2621, 163, 2372, 167, 1853, 3818, 173, 4091, 2136, 178,
859 1859, 4067, 183, 1863, 188, 3909, 3117, 194, 1869, 198, 3449, 2816,
860 204, 3679, 208, 2985, 4004, 214, 1879, 2165, 219, 2642, 224, 2821,
861 2161, 229, 3856, 235, 2412, 239, 1894, 4092, 245, 3539, 2171, 250,
862 3557, 3143, 255, 2177, 260, 1905, 3817, 266, 3734, 270, 3138, 3001,
863 276, 1915, 280, 3460, 3278, 286, 1921, 2192, 291, 1925, 296, 3145,
864 2197, 301, 4018, 307, 2443, 311, 1935, 3385, 317, 3386, 2208, 322,
865 3470, 2444, 327, 3942, 332, 1946, 3932, 338, 2218, 342, 3629, 3825,
866 348, 1956, 352, 3026, 3158, 358, 1962, 2237, 363, 1966, 368, 4075,
867 2233, 373, 1972, 379, 3558, 383, 2248, 2703, 389, 3892, 2243, 394,
868 1982, 3866, 399, 2249, 404, 3486, 3742, 410, 2714, 414, 3174, 3042,
869 420, 2259, 424, 4069, 2718, 430, 2003, 2264, 435, 2007, 440, 3180,
870 2269, 445, 2013, 451, 4028, 455, 3491, 3871, 461, 2899, 2280, 466,
871 2023, 2515, 471, 3416, 476, 3062, 3189, 482, 2290, 486, 3496, 2516,
872 492, 3756, 496, 3204, 3302, 502, 2300, 2309, 507, 2749, 512, 2049,
873 2305, 517, 3902, 523, 4081, 527, 2320, 2059, 533, 2924, 2315, 538,
874 2065, 3215, 543, 2069, 548, 3507, 3833, 554, 3432, 558, 3210, 3083,
875 564, 2331, 568, 3511, 3877, 574, 4070, 2336, 579, 3848, 584, 2090,
876 2341, 589, 3345, 595, 4061, 599, 3660, 2100, 605, 3972, 2352, 610,
877 2106, 3589, 615, 2110, 620, 3103, 3329, 626, 2116, 630, 3521, 2587,
878 636, 2800, 640, 3771, 3230, 646, 2126, 2381, 651, 3725, 656, 3722,
879 2377, 661, 3461, 667, 3530, 671, 2141, 2811, 677, 3911, 2387, 682,
880 2147, 3815, 687, 2151, 692, 3854, 3675, 698, 2157, 702, 3246, 4090,
881 708, 2403, 712, 3532, 2827, 718, 2167, 2408, 723, 3375, 728, 2628,
882 2413, 733, 2837, 739, 2968, 743, 2182, 3680, 749, 3369, 2424, 754,
883 3542, 3364, 759, 3791, 764, 2193, 3261, 770, 2434, 774, 4054, 3614,
884 780, 2203, 784, 3276, 3149, 790, 2209, 2453, 795, 2213, 800, 2650,
885 2449, 805, 3786, 811, 3555, 815, 2223, 3940, 821, 2660, 2459, 826,
886 3396, 3287, 831, 2465, 836, 2234, 3861, 842, 3834, 846, 3282, 4063,
887 852, 2244, 856, 3924, 3402, 862, 2250, 2480, 867, 2254, 872, 3630,
888 2485, 877, 2260, 883, 3565, 887, 3563, 3493, 893, 2691, 2496, 898,
889 2270, 2866, 903, 4062, 908, 3186, 3400, 914, 2506, 918, 3568, 3483,
890 924, 2909, 928, 3500, 3190, 934, 2291, 2525, 939, 2295, 944, 2721,
891 2521, 949, 2301, 955, 4021, 959, 2536, 2919, 965, 2731, 2531, 970,
892 2311, 3840, 975, 2537, 980, 3579, 2732, 986, 2930, 990, 3318, 3206,
893 996, 2547, 1000, 3583, 2934, 1006, 3928, 2552, 1011, 2940, 1016, 2337,
894 2557, 1021, 2944, 1027, 3, 9, 3879, 14, 1037, 20, 24, 1042,
895 30, 3852, 1047, 35, 1052, 40, 45, 1058, 2578, 51, 55, 2937,
896 1068, 61, 65, 3348, 71, 1078, 2588, 76, 81, 2965, 86, 2378,
897 92, 96, 3658, 102, 3874, 1103, 107, 2388, 112, 117, 2603, 1114,
898 123, 127, 1119, 2398, 133, 137, 2803, 143, 2404, 1134, 148, 153,
899 1140, 158, 1144, 164, 168, 1150, 174, 2624, 1155, 179, 1160, 184,
900 189, 1165, 3918, 195, 199, 1175, 2429, 205, 209, 3135, 215, 1186,
901 2435, 220, 225, 2439, 230, 3379, 236, 240, 2445, 246, 3736, 4068,
902 251, 3016, 256, 261, 3374, 1222, 267, 271, 1227, 3691, 277, 281,
903 2665, 287, 3560, 1243, 292, 297, 2470, 302, 1253, 308, 312, 1258,
904 318, 4008, 1263, 323, 1268, 328, 333, 1274, 3037, 339, 343, 3289,
905 1284, 349, 353, 3920, 359, 1294, 2497, 364, 369, 2501, 374, 3176,
906 380, 384, 3053, 390, 2876, 1319, 395, 3873, 400, 405, 2712, 1330,
907 411, 415, 1335, 3868, 421, 425, 3405, 431, 2722, 1350, 436, 441,
908 1356, 446, 1360, 452, 456, 1366, 462, 2741, 1371, 467, 1376, 472,
909 477, 1381, 2548, 483, 487, 1391, 2752, 493, 497, 3842, 503, 1402,
910 2558, 508, 513, 2753, 518, 3651, 524, 528, 3807, 534, 3426, 3330,
911 539, 2763, 544, 549, 3596, 1438, 555, 559, 1443, 2583, 565, 569,
912 2773, 575, 2589, 1459, 580, 585, 3910, 590, 1469, 596, 600, 1474,
913 606, 2948, 1479, 611, 1484, 616, 621, 1490, 2794, 627, 631, 3908,
914 1500, 637, 641, 3608, 647, 1510, 2804, 652, 657, 3611, 662, 2625,
915 668, 672, 3863, 678, 3723, 1535, 683, 2635, 688, 693, 2819, 1546,
916 699, 703, 1551, 2645, 709, 713, 3362, 719, 3146, 1566, 724, 729,
917 1572, 734, 1576, 740, 744, 1582, 750, 2840, 1587, 755, 1592, 760,
918 765, 1597, 3160, 771, 775, 1607, 4066, 781, 785, 3788, 791, 1618,
919 2682, 796, 801, 2686, 806, 3391, 812, 816, 2692, 822, 3921, 3020,
920 827, 4039, 832, 837, 3617, 1654, 843, 847, 1659, 3181, 853, 857,
921 2881, 863, 4022, 1675, 868, 873, 2717, 878, 1685, 884, 888, 1690,
922 894, 3503, 1695, 899, 1700, 904, 909, 1706, 2733, 915, 919, 3796,
923 1716, 925, 929, 4076, 935, 1726, 2743, 940, 945, 3591, 950, 3795,
924 956, 960, 3883, 966, 3580, 1751, 971, 3904, 976, 981, 2928, 1762,
925 987, 991, 1767, 3953, 997, 1001, 4007, 1007, 2938, 1782, 1012, 1017,
926 1788, 1022, 1792, 1028, 1032, 1798, 1038, 2957, 1803, 1043, 1808, 1048,
927 1053, 1813, 3677, 1059, 1063, 1823, 2799, 1069, 1073, 3933, 1079, 1834,
928 3248, 1084, 1089, 2969, 1094, 2810, 1100, 1104, 3253, 1110, 3534, 4005,
929 1115, 2820, 1120, 1125, 3259, 1870, 1131, 1135, 1875, 2830, 1141, 1145,
930 2989, 1151, 2836, 1891, 1156, 1161, 3941, 1166, 1901, 1172, 1176, 1906,
931 1182, 3905, 1911, 1187, 1916, 1192, 1197, 1922, 3010, 1203, 1207, 3860,
932 1932, 1213, 1217, 3564, 1223, 1942, 2867, 1228, 1233, 2871, 1238, 3154,
933 1244, 1248, 2877, 1254, 3392, 1967, 1259, 3865, 1264, 1269, 3035, 1978,
934 1275, 1279, 1983, 3041, 1285, 1289, 3983, 1295, 3798, 1998, 1300, 1305,
935 2004, 1310, 2008, 1316, 1320, 2014, 1326, 3056, 2019, 1331, 2024, 1336,
936 1341, 2029, 3900, 1347, 1351, 2039, 3951, 1357, 1361, 3195, 1367, 2050,
937 2929, 1372, 1377, 2933, 1382, 3515, 1388, 1392, 3082, 1398, 3845, 3652,
938 1403, 3341, 1408, 1413, 3519, 2086, 1419, 1423, 2091, 3720, 1429, 1433,
939 3097, 1439, 4086, 2107, 1444, 1449, 3112, 1454, 2117, 1460, 1464, 2122,
940 1470, 3973, 2127, 1475, 2132, 1480, 1485, 2138, 2980, 1491, 1495, 3535,
941 2148, 1501, 1505, 4079, 1511, 2158, 2990, 1516, 1521, 3372, 1526, 3612,
942 1532, 1536, 3376, 1542, 3464, 2183, 1547, 3890, 1552, 1557, 3144, 2194,
943 1563, 1567, 2199, 3015, 1573, 1577, 3621, 1583, 3021, 2214, 1588, 1593,
944 2220, 1598, 2224, 1604, 1608, 2230, 1614, 3173, 2235, 1619, 2240, 1624,
945 1629, 2245, 3979, 1635, 1639, 2255, 3046, 1645, 1649, 3830, 1655, 2266,
946 3839, 1660, 1665, 3185, 1670, 3057, 1676, 1680, 3755, 1686, 3642, 3577,
947 1691, 3067, 1696, 1701, 3710, 2302, 1707, 1711, 2307, 3077, 1717, 1721,
948 3205, 1727, 3990, 2323, 1732, 1737, 3087, 1742, 2333, 1748, 1752, 2338,
949 1758, 3880, 2343, 1763, 2348, 1768, 1773, 2354, 3226, 1779, 1783, 4055,
950 2364, 1789, 1793, 3602, 1799, 2374, 3114, 1804, 1809, 3118, 1814, 3914,
951 1820, 1824, 3124, 1830, 3721, 2399, 1835, 3459, 1840, 1845, 3251, 2410,
952 1851, 1855, 2415, 3257, 1861, 1865, 4085, 1871, 3469, 2430, 1876, 1881,
953 2436, 1886, 2440, 1892, 1896, 2446, 1902, 3272, 2451, 1907, 2456, 1912,
954 1917, 2461, 3165, 1923, 1927, 2471, 3982, 1933, 1937, 3977, 1943, 2482,
955 3175, 1948, 1953, 3896, 1958, 3638, 1964, 1968, 3298, 1974, 4044, 3572,
956 1979, 3926, 1984, 1989, 3829, 2518, 1995, 1999, 2523, 3506, 2005, 2009,
957 3313, 2015, 4000, 2539, 2020, 2025, 3328, 2030, 2549, 2036, 2040, 2554,
958 2046, 3719, 2559, 2051, 2564, 2056, 2061, 2570, 3950, 2067, 2071, 3659,
959 2580, 2077, 2081, 4073, 2087, 2590, 3441, 2092, 2097, 4014, 2102, 3242,
960 2108, 2112, 3777, 2118, 3451, 2615, 2123, 3252, 2128, 2133, 3360, 2626,
961 2139, 2143, 2631, 3262, 2149, 2153, 3806, 2159, 3268, 2646, 2164, 2169,
962 2652, 2174, 2656, 2180, 2184, 2662, 2190, 3389, 2667, 2195, 2672, 2200,
963 2205, 2677, 4056, 2211, 2215, 2687, 3293, 2221, 2225, 4034, 2231, 2698,
964 3299, 2236, 2241, 3303, 2246, 3867, 2252, 2256, 3309, 2262, 3750, 4041,
965 2267, 3411, 2272, 2277, 3582, 2734, 2283, 2287, 2739, 3588, 2293, 2297,
966 3421, 2303, 3592, 2755, 2308, 2313, 3334, 2318, 2765, 2324, 2328, 2770,
967 2334, 3523, 2775, 2339, 2780, 2344, 2349, 2786, 3442, 2355, 2359, 3524,
968 2796, 2365, 2369, 3780, 2375, 2806, 3361, 2380, 2385, 3365, 2390, 3893,
969 2396, 2400, 3884, 2406, 3976, 2831, 2411, 3623, 2416, 2421, 3467, 2842,
970 2427, 2431, 2847, 3473, 2437, 2441, 3889, 2447, 3864, 2862, 2452, 2457,
971 2868, 2462, 2872, 2468, 2472, 2878, 2478, 3488, 2883, 2483, 2888, 2488,
972 2493, 2893, 3412, 2499, 2503, 2903, 3948, 2509, 2513, 3945, 2519, 2914,
973 3422, 2524, 2529, 4025, 2534, 3762, 2540, 2544, 3514, 2550, 3952, 3595,
974 2555, 3664, 2560, 2565, 3766, 2950, 2571, 2575, 2955, 3447, 2581, 2585,
975 3529, 2591, 3453, 2971, 2596, 2601, 3544, 2606, 2981, 2612, 2616, 2986,
976 2622, 4060, 2991, 2627, 2996, 2632, 2637, 3002, 3685, 2643, 2647, 3782,
977 3012, 2653, 2657, 4037, 2663, 3022, 4019, 2668, 2673, 3869, 2678, 3489,
978 2684, 2688, 3701, 2694, 3994, 3047, 2699, 3499, 2704, 2709, 3576, 3058,
979 2715, 2719, 3063, 3509, 2725, 2729, 3837, 4, 10, 15, 25, 31,
980 41, 46, 56, 66, 72, 82, 87, 97, 103, 113, 118, 128,
981 138, 144, 154, 159, 169, 175, 185, 190, 200, 210, 216, 226,
982 231, 241, 247, 257, 262, 272, 282, 288, 298, 303, 313, 319,
983 329, 334, 344, 354, 360, 370, 375, 385, 391, 401, 406, 416,
984 426, 432, 442, 447, 457, 463, 473, 478, 488, 498, 504, 514,
985 519, 529, 535, 545, 550, 560, 570, 576, 586, 591, 601, 607,
986 617, 622, 632, 642, 648, 658, 663, 673, 679, 689, 694, 704,
987 714, 720, 730, 735, 745, 751, 761, 766, 776, 786, 792, 802,
988 807, 817, 823, 833, 838, 848, 858, 864, 874, 879, 889, 895,
989 905, 910, 920, 930, 936, 946, 951, 961, 967, 977, 982, 992,
990 1002, 1008, 1018, 1023, 1033, 1039, 1049, 1054, 1064, 1074, 1080, 1090,
991 1095, 1105, 1111, 1121, 1126, 1136, 1146, 1152, 1162, 1167, 1177, 1183,
992 1193, 1198, 1208, 1218, 1224, 1234, 1239, 1249, 1255, 1265, 1270, 1280,
993 1290, 1296, 1306, 1311, 1321, 1327, 1337, 1342, 1352, 1362, 1368, 1378,
994 1383, 1393, 1399, 1409, 1414, 1424, 1434, 1440, 1450, 1455, 1465, 1471,
995 1481, 1486, 1496, 1506, 1512, 1522, 1527, 1537, 1543, 1553, 1558, 1568,
996 1578, 1584, 1594, 1599, 1609, 1615, 1625, 1630, 1640, 1650, 1656, 1666,
997 1671, 1681, 1687, 1697, 1702, 1712, 1722, 1728, 1738, 1743, 1753, 1759,
998 1769, 1774, 1784, 1794, 1800, 1810, 1815, 1825, 1831, 1841, 1846, 1856,
999 1866, 1872, 1882, 1887, 1897, 1903, 1913, 1918, 1928, 1938, 1944, 1954,
1000 1959, 1969, 1975, 1985, 1990, 2000, 2010, 2016, 2026, 2031, 2041, 2047,
1001 2057, 2062, 2072, 2082, 2088, 2098, 2103, 2113, 2119, 2129, 2134, 2144,
1002 2154, 2160, 2170, 2175, 2185, 2191, 2201, 2206, 2216, 2226, 2232, 2242,
1003 2247, 2257, 2263, 2273, 2278, 2288, 2298, 2304, 2314, 2319, 2329, 2335,
1004 2345, 2350, 2360, 2370, 2376, 2386, 2391, 2401, 2407, 2417, 2422, 2432,
1005 2442, 2448, 2458, 2463, 2473, 2479, 2489, 2494, 2504, 2514, 2520, 2530,
1006 2535, 2545, 2551, 2561, 2566, 2576, 2586, 2592, 2602, 2607, 2617, 2623,
1007 2633, 2638, 2648, 2658, 2664, 2674, 2679, 2689, 2695, 2705, 2710, 2720,
1008 2730, 2736, 2746, 2751, 2761, 2767, 2777, 2782, 2792, 2802, 2808, 2818,
1009 2823, 2833, 2839, 2849, 2854, 2864, 2874, 2880, 2890, 2895, 2905, 2911,
1010 2921, 2926, 2936, 2946, 2952, 2962, 2967, 2977, 2983, 2993, 2998, 3008,
1011 3018, 3024, 3034, 3039, 3049, 3055, 3065, 3070, 3080, 3090, 3096, 3106,
1012 3111, 3121, 3127, 3137, 3142, 3152, 3162, 3168, 3178, 3183, 3193, 3199,
1013 3209, 3214, 3224, 3234, 3240, 3250, 3255, 3265, 3271, 3281, 3286, 3296,
1014 3306, 3312, 3322, 3327, 3337, 3343, 3353, 3358, 3368, 3378, 3384, 3394,
1015 3399, 3409, 3415, 3425, 3430, 3440, 3450, 3456, 3466, 3471, 3481, 3487,
1016 3497, 3502, 3512, 3522, 3528, 3538, 3543, 3553, 3559, 3569, 3574, 3584,
1017 3594, 3600, 3610, 3615, 3625, 3631, 3641, 3646, 3656, 3666, 3672, 3682,
1018 3687, 3697, 3703, 3713, 3718, 3728, 3738, 3744, 3754, 3759, 3769, 3775,
1019 3785, 3790, 3800, 3810, 3816, 3826, 3831, 3841, 3847, 3857, 3862, 3872,
1020 3882, 3888, 3898, 3903, 3913, 3919, 3929, 3934, 3944, 3954, 3960, 3970,
1021 3975, 3985, 3991, 4001, 4006, 4016, 4026, 4032, 4042, 4047, 4057, 4087,
1022 4089, 4093, 4094, 5
1023};
1024
1025static const int bmkiller_4097[] = {
1026 0, 1027, 3081, 3842, 6, 16, 3586, 2562, 2749, 3587, 11, 3515,
1027 2950, 3418, 530, 17, 26, 2740, 1417, 21, 1041, 2567, 3843, 2755,
1028 2731, 27, 36, 3906, 1428, 31, 2572, 1047, 2073, 3205, 3952, 37,
1029 46, 2745, 1052, 3598, 1432, 42, 2750, 2578, 4050, 3654, 47, 57,
1030 2363, 2330, 2579, 52, 3088, 3721, 4015, 2920, 58, 67, 3852, 571,
1031 62, 1072, 2960, 3339, 1791, 566, 68, 77, 2756, 3231, 1797, 1777,
1032 73, 2760, 2597, 3883, 1782, 78, 88, 2965, 1802, 3093, 83, 3596,
1033 3237, 3429, 1463, 89, 98, 3605, 3726, 93, 2971, 1093, 2104, 2341,
1034 593, 99, 108, 2766, 2783, 103, 1103, 2598, 3434, 3880, 3770, 109,
1035 118, 2770, 3242, 3350, 607, 114, 3813, 1113, 4002, 613, 119, 129,
1036 2394, 2109, 3443, 124, 2776, 1119, 3112, 2794, 130, 139, 3601, 2610,
1037 134, 1124, 2618, 2124, 1832, 628, 140, 149, 3109, 1129, 1838, 634,
1038 145, 2781, 1134, 4044, 3818, 150, 160, 1140, 1843, 644, 155, 2786,
1039 2619, 4009, 2126, 161, 170, 3115, 3527, 165, 1150, 2804, 3445, 2582,
1040 664, 171, 180, 2791, 4093, 175, 3878, 1155, 2145, 4013, 665, 181,
1041 190, 3119, 1160, 3815, 2630, 186, 2797, 2996, 2631, 684, 191, 201,
1042 2424, 3613, 1535, 196, 2801, 2634, 3862, 4003, 202, 211, 3125, 2975,
1043 206, 3822, 2429, 1874, 2150, 2966, 212, 221, 2807, 2639, 2393, 705,
1044 217, 3129, 3775, 3455, 1551, 222, 232, 2439, 3619, 715, 227, 3546,
1045 3736, 4085, 1556, 233, 242, 2812, 716, 237, 2445, 1201, 1894, 2412,
1046 1561, 243, 252, 3135, 3134, 247, 1212, 3145, 3823, 2831, 736, 253,
1047 262, 2817, 1216, 2798, 3618, 258, 2822, 1222, 3460, 3259, 263, 273,
1048 2455, 2181, 3732, 268, 3140, 1227, 3986, 747, 274, 283, 4031, 3991,
1049 278, 1232, 2460, 1915, 3542, 2629, 284, 293, 2828, 1237, 2191, 1592,
1050 289, 2832, 1243, 3153, 2847, 294, 304, 1247, 2197, 2671, 299, 3556,
1051 3488, 3465, 2992, 305, 314, 3150, 787, 309, 1257, 2675, 1935, 2434,
1052 782, 315, 324, 2838, 788, 319, 2480, 1263, 1941, 3482, 2855, 325,
1053 334, 2842, 1268, 2444, 3477, 330, 3627, 2486, 1946, 2650, 335, 345,
1054 3037, 3271, 3788, 340, 2848, 3892, 3629, 818, 346, 355, 3943, 1633,
1055 350, 1288, 2691, 3293, 2222, 3478, 356, 365, 4076, 2875, 2464, 823,
1056 361, 2853, 3570, 3476, 829, 366, 376, 3863, 3864, 3278, 371, 2858,
1057 2501, 3480, 1654, 377, 386, 3747, 2876, 381, 3499, 1309, 1976, 3691,
1058 844, 387, 396, 2863, 859, 391, 1319, 2706, 1982, 3695, 854, 397,
1059 406, 3958, 4053, 2475, 3554, 402, 2869, 1329, 1987, 2882, 407, 417,
1060 3504, 2253, 3297, 412, 2873, 1335, 3046, 1679, 418, 427, 3646, 2717,
1061 422, 1340, 3640, 2268, 4008, 881, 428, 437, 2879, 1345, 2263, 1689,
1062 433, 3752, 1350, 3794, 900, 438, 448, 1356, 2269, 2727, 443, 3576,
1063 2532, 3490, 1993, 449, 458, 2884, 3047, 453, 1366, 4065, 4025, 2505,
1064 3038, 459, 468, 3642, 3647, 463, 2542, 1371, 2289, 3498, 916, 469,
1065 478, 2889, 1376, 2515, 922, 474, 2894, 3078, 2739, 2907, 479, 489,
1066 2548, 4088, 932, 484, 3927, 2742, 4048, 3900, 490, 499, 3197, 3899,
1067 494, 3421, 3084, 3324, 2038, 952, 500, 509, 2900, 2747, 3503, 3648,
1068 505, 2904, 4012, 3649, 4079, 510, 520, 2753, 1, 1741, 515, 7,
1069 2762, 3501, 963, 521, 12, 3948, 1751, 525, 3094, 18, 2320, 4024,
1070 22, 531, 540, 2910, 3068, 535, 28, 3513, 3506, 32, 3653, 541,
1071 550, 2914, 38, 2546, 993, 546, 3953, 1438, 43, 1767, 551, 561,
1072 48, 2325, 1003, 556, 53, 1443, 3087, 1772, 562, 59, 4068, 1004,
1073 63, 1448, 2932, 2340, 2079, 69, 572, 581, 3217, 1453, 2085, 74,
1074 577, 2925, 1459, 79, 2557, 582, 592, 84, 2090, 3232, 587, 2930,
1075 90, 3660, 1034, 94, 602, 3222, 3518, 597, 1473, 100, 3517, 2944,
1076 104, 603, 612, 2935, 3848, 110, 2788, 1479, 2361, 3907, 3763, 115,
1077 622, 3228, 1484, 120, 1808, 618, 2941, 125, 3524, 2955, 623, 633,
1078 131, 3593, 2795, 135, 2945, 3908, 3996, 3089, 141, 643, 4075, 1075,
1079 638, 1504, 146, 3608, 2120, 1070, 151, 653, 2951, 3446, 156, 1456,
1080 649, 3238, 2813, 162, 3218, 654, 166, 2624, 2131, 3599, 659, 3607,
1081 172, 3670, 2969, 176, 674, 2956, 2978, 669, 182, 1525, 2392, 3104,
1082 1097, 675, 187, 3243, 1849, 679, 192, 2814, 3884, 3669, 197, 685,
1083 694, 2961, 2635, 203, 1111, 690, 207, 1545, 3532, 1117, 695, 213,
1084 2640, 2397, 3665, 700, 3248, 218, 3128, 1870, 706, 223, 3673, 2826,
1085 710, 228, 2645, 2162, 2609, 1132, 234, 725, 2972, 238, 2407, 1138,
1086 721, 2976, 1566, 244, 3812, 726, 248, 1572, 2413, 1148, 731, 254,
1087 2835, 3537, 2414, 737, 746, 259, 3369, 741, 1582, 264, 2182, 2623,
1088 1168, 269, 756, 2982, 3273, 751, 275, 1587, 2433, 279, 1169, 757,
1089 766, 2986, 285, 3452, 1905, 762, 3920, 3160, 290, 1188, 767, 777,
1090 295, 3942, 3004, 772, 300, 2850, 3889, 3253, 778, 306, 3269, 3626,
1091 310, 3386, 2676, 2203, 2438, 3684, 316, 797, 3683, 320, 2644, 1209,
1092 793, 2997, 326, 3548, 3690, 798, 808, 2686, 331, 1219, 803, 3002,
1093 336, 3552, 1936, 809, 341, 4070, 1220, 813, 2866, 347, 2223, 3555,
1094 351, 819, 828, 3007, 3620, 357, 1644, 3020, 2229, 2660, 1240, 362,
1095 838, 3632, 1648, 367, 3146, 834, 3013, 372, 2234, 3749, 839, 849,
1096 378, 2469, 1957, 382, 3017, 1659, 3830, 1251, 850, 388, 3740, 1967,
1097 392, 1664, 3487, 2484, 2680, 398, 860, 869, 3023, 1669, 2479, 403,
1098 865, 3638, 1675, 408, 3963, 870, 880, 413, 2485, 2887, 875, 3793,
1099 419, 3562, 3161, 423, 890, 3028, 1291, 885, 429, 2891, 2264, 3494,
1100 1286, 891, 434, 3924, 1292, 895, 439, 1695, 2270, 2700, 444, 901,
1101 910, 3033, 1700, 450, 1998, 906, 454, 2733, 2275, 2701, 911, 921,
1102 460, 2870, 3051, 464, 3304, 3997, 3701, 1322, 470, 931, 3999, 3839,
1103 926, 1720, 475, 3874, 2510, 1672, 480, 941, 3044, 4023, 485, 1327,
1104 937, 3048, 3207, 491, 1333, 942, 495, 4091, 2721, 3801, 947, 501,
1105 2748, 3573, 2918, 953, 962, 506, 4083, 957, 3212, 511, 2536, 3063,
1106 1348, 516, 972, 3054, 1363, 967, 522, 2922, 3578, 526, 1358, 973,
1107 982, 3058, 3427, 532, 3301, 978, 536, 1761, 4071, 1713, 983, 542,
1108 2764, 2541, 3757, 988, 3064, 547, 3328, 3076, 994, 552, 3718, 2933,
1109 998, 557, 3712, 2556, 2326, 1385, 563, 1013, 3325, 567, 2551, 3082,
1110 1009, 3069, 573, 3988, 1404, 1014, 1024, 1788, 578, 2076, 1019, 3074,
1111 583, 3879, 1744, 1025, 588, 3331, 3637, 1029, 1798, 594, 3589, 3650,
1112 598, 1035, 1044, 3079, 3092, 1039, 604, 1803, 2577, 608, 1420, 1045,
1113 1054, 3335, 614, 3807, 1426, 1050, 3085, 3677, 619, 3525, 1055, 1065,
1114 624, 2763, 1436, 1060, 629, 2958, 4027, 2767, 1066, 635, 3341, 3441,
1115 639, 3652, 3935, 3868, 2367, 645, 1076, 1085, 3095, 2963, 2373, 650,
1116 1081, 3345, 3912, 655, 3438, 1086, 1096, 660, 2378, 3107, 1091, 3936,
1117 666, 3885, 1467, 670, 1106, 3100, 2974, 1101, 4040, 676, 2608, 3603,
1118 680, 1107, 1116, 3351, 2948, 686, 1860, 3658, 4054, 3535, 3229, 691,
1119 1126, 3105, 1864, 696, 1497, 1122, 3110, 701, 3604, 4029, 1127, 1137,
1120 707, 2613, 1507, 711, 3356, 1875, 4030, 2152, 717, 1147, 3992, 1508,
1121 1142, 1880, 722, 2628, 2408, 3959, 727, 1157, 3116, 1885, 732, 3977,
1122 1153, 3120, 1891, 738, 3722, 1158, 742, 1895, 2419, 3256, 1163, 3679,
1123 748, 3609, 1538, 752, 1178, 3366, 2173, 1173, 758, 2999, 3614, 4080,
1124 1852, 1179, 763, 3126, 2183, 1183, 768, 1911, 2649, 3893, 773, 1189,
1125 1198, 3130, 1916, 779, 3979, 1194, 783, 3010, 3853, 3676, 1199, 789,
1126 2856, 2834, 3011, 1204, 3136, 794, 4084, 3464, 1210, 799, 3890, 1579,
1127 1214, 804, 2861, 2450, 2654, 1574, 810, 1229, 4046, 814, 3957, 1889,
1128 1225, 3141, 3029, 820, 2446, 1230, 824, 2871, 2839, 3381, 1235, 830,
1129 3559, 3624, 2220, 1241, 1250, 835, 3392, 1245, 2877, 840, 2470, 2845,
1130 1601, 845, 1260, 3151, 3560, 1255, 851, 3030, 3895, 855, 3373, 1261,
1131 1270, 3694, 861, 3166, 1615, 1266, 3157, 1977, 866, 1621, 1271, 1281,
1132 871, 2685, 3019, 1276, 876, 1983, 3400, 3403, 1282, 882, 3745, 3042,
1133 886, 1988, 2892, 2491, 2860, 1636, 892, 1301, 3167, 896, 2695, 1642,
1134 1297, 3835, 902, 3866, 3407, 1302, 1312, 2004, 907, 1652, 1307, 3700,
1135 912, 3634, 2702, 1313, 917, 3172, 3692, 1317, 2014, 923, 2511, 3289,
1136 927, 1323, 1332, 3750, 3194, 933, 2912, 2019, 2517, 3294, 1673, 938,
1137 1342, 3177, 2024, 943, 3062, 1338, 3182, 948, 2522, 1692, 1343, 1353,
1138 954, 3191, 2292, 958, 3925, 3066, 3934, 3398, 1354, 964, 3413, 3050,
1139 968, 2923, 3808, 3509, 2726, 974, 1364, 1373, 3188, 3071, 2897, 979,
1140 1369, 3192, 3968, 984, 2307, 1374, 1384, 989, 3201, 1723, 1379, 4049,
1141 995, 3645, 2312, 999, 1394, 4041, 1724, 1389, 1005, 2065, 2552, 2916,
1142 2317, 1395, 1010, 3198, 3422, 1399, 1015, 3804, 2558, 3591, 1020, 1405,
1143 1414, 3202, 2080, 1026, 3762, 1410, 1030, 2086, 2563, 3316, 1415, 1425,
1144 1036, 2757, 3215, 1040, 3208, 2091, 3334, 1755, 1046, 1435, 3811, 3220,
1145 1430, 2096, 1051, 2772, 4034, 3711, 1056, 1445, 3433, 2101, 1061, 2348,
1146 1441, 3213, 2107, 1067, 3940, 1446, 1071, 2111, 2773, 3103, 1451, 1077,
1147 2964, 3767, 3520, 1457, 1466, 1082, 1795, 1461, 2121, 1087, 3661, 2938,
1148 1790, 1092, 1476, 3223, 1796, 1471, 1098, 2127, 2793, 1102, 3662, 1477,
1149 1486, 3444, 2132, 1108, 3245, 1482, 1112, 3730, 3606, 3805, 1487, 1118,
1150 2980, 3590, 3974, 1492, 3233, 1123, 3773, 1826, 1498, 1128, 3990, 2389,
1151 1502, 1133, 3123, 3540, 2614, 2105, 1139, 1517, 3239, 1143, 2968, 1831,
1152 1513, 3454, 1149, 3671, 1837, 1518, 1528, 3668, 1154, 3724, 1523, 3731,
1153 1159, 3777, 2409, 1529, 1164, 3244, 4058, 1533, 3376, 1170, 2824, 3965,
1154 1174, 1539, 1548, 3459, 1867, 1543, 1180, 3138, 3916, 1184, 1862, 1549,
1155 1558, 3249, 1190, 2979, 2140, 1554, 3254, 2193, 1195, 2146, 1559, 1569,
1156 1200, 2829, 4019, 1564, 1205, 2199, 3375, 2436, 1570, 1211, 3790, 3149,
1157 1215, 2204, 3784, 2844, 2655, 1221, 1580, 1589, 3260, 2209, 2661, 1226,
1158 1585, 3264, 2214, 1231, 1908, 1590, 1600, 1236, 2666, 3159, 1595, 3956,
1159 1242, 3681, 2177, 1246, 1610, 3475, 3854, 1605, 2230, 1252, 3686, 3009,
1160 1256, 1611, 1620, 3270, 3824, 1262, 3397, 2235, 2865, 3279, 1924, 1267,
1161 1630, 3274, 2240, 1272, 1930, 1626, 4063, 1277, 3171, 3489, 1631, 1641,
1162 1283, 3284, 1940, 1287, 3280, 3174, 4077, 3148, 1293, 1651, 3485, 3743,
1163 1646, 3571, 1298, 3689, 2696, 1960, 1303, 1661, 3791, 3179, 1308, 3792,
1164 1657, 3285, 3983, 1314, 3388, 1662, 1318, 3056, 2707, 2497, 1667, 3290,
1165 1324, 3696, 1971, 1328, 1682, 4045, 2508, 1677, 1334, 2281, 2896, 3565,
1166 3164, 1683, 1339, 3295, 3566, 1687, 1344, 3926, 3955, 3699, 1349, 1693,
1167 1702, 3796, 2296, 1355, 2001, 1698, 1359, 2302, 3798, 2523, 1703, 1365,
1168 3072, 2901, 2011, 1708, 3305, 1370, 3416, 2528, 1714, 1375, 4086, 2012,
1169 1718, 1380, 3077, 2738, 3184, 2533, 1386, 1733, 3311, 1390, 2911, 2539,
1170 1729, 3802, 2323, 1396, 3061, 1734, 1400, 2327, 2917, 3516, 1739, 1406,
1171 3849, 3706, 2042, 1745, 1754, 1411, 3323, 1749, 2337, 1416, 2758, 3320,
1172 2294, 1421, 1764, 3901, 3329, 1759, 1427, 2343, 2937, 1431, 3204, 1765,
1173 1774, 3321, 1437, 3659, 2564, 1770, 3326, 3226, 1442, 3714, 1775, 1785,
1174 1447, 4051, 3227, 1780, 1452, 3950, 4066, 3424, 1786, 1458, 3931, 2083,
1175 1462, 2368, 3108, 2779, 2942, 2078, 1468, 1805, 3332, 1472, 3086, 3073,
1176 1801, 3336, 1478, 4022, 2335, 1806, 1816, 3118, 1483, 3764, 1811, 3772,
1177 1488, 3717, 4014, 1817, 1493, 3821, 3436, 1821, 3855, 1499, 2799, 3225,
1178 1503, 1827, 1836, 3342, 2605, 1509, 2399, 3246, 2805, 3973, 2356, 1514,
1179 1846, 3346, 3729, 1519, 2119, 1842, 3976, 1524, 2810, 2125, 1847, 1857,
1180 1530, 2973, 3448, 1534, 3352, 2415, 3544, 2625, 1858, 1540, 3817, 3258,
1181 1544, 2420, 3266, 2988, 3113, 1550, 1868, 1877, 3541, 2425, 2983, 1555,
1182 1873, 3357, 2430, 1560, 3856, 1878, 1888, 1565, 2989, 2156, 1883, 3362,
1183 1571, 4043, 2990, 1575, 1898, 3547, 3938, 1893, 1581, 3379, 2840, 3127,
1184 2176, 1899, 1586, 3367, 3787, 1903, 1591, 2451, 2846, 3133, 1596, 1909,
1185 1918, 3551, 2456, 1602, 2662, 1914, 1606, 3165, 2851, 2196, 1919, 1929,
1186 1612, 3382, 3827, 1616, 3377, 3282, 3961, 2428, 1622, 1939, 3557, 3469,
1187 1934, 3170, 1627, 3698, 3014, 3470, 1632, 1949, 3383, 3287, 1637, 2217,
1188 1945, 3561, 3693, 1643, 3390, 1950, 1647, 3292, 3154, 2227, 1955, 1653,
1189 3180, 4082, 3860, 1961, 1970, 1658, 2228, 1965, 3298, 1663, 3040, 3919,
1190 3395, 1668, 1980, 3567, 3865, 1975, 1674, 3797, 3947, 1678, 2248, 1981,
1191 1990, 3393, 2512, 1684, 3834, 1986, 1688, 2518, 3748, 3981, 1991, 1694,
1192 3196, 3045, 2713, 1996, 3572, 1699, 4078, 2259, 2002, 1704, 4062, 2724,
1193 2006, 1709, 3703, 3060, 2902, 3751, 1715, 2021, 3404, 1719, 3055, 2728,
1194 2017, 3408, 1725, 3585, 3870, 2022, 2032, 2543, 1730, 3319, 2027, 3803,
1195 1735, 3753, 3496, 2033, 1740, 3582, 2299, 2037, 2553, 1746, 3758, 3417,
1196 1750, 2043, 2052, 3414, 2300, 2047, 1756, 2559, 2, 1760, 8, 2053,
1197 2062, 13, 1766, 3761, 19, 2058, 23, 3526, 1771, 29, 2063, 33,
1198 1776, 3505, 39, 2068, 1781, 44, 3845, 49, 2074, 1787, 54, 3431,
1199 60, 2584, 64, 3814, 2943, 70, 2084, 2093, 75, 3911, 2949, 80,
1200 2089, 85, 3531, 1807, 91, 2094, 95, 1812, 2954, 101, 2099, 105,
1201 1818, 3768, 111, 1822, 2114, 116, 3451, 121, 3536, 1828, 126, 3946,
1202 132, 2115, 136, 3439, 2371, 142, 2615, 3354, 147, 3235, 2366, 152,
1203 2134, 157, 3674, 1848, 163, 2130, 167, 1853, 4081, 173, 2135, 177,
1204 1859, 3117, 183, 1863, 3449, 188, 3616, 193, 1869, 2155, 198, 3365,
1205 204, 2636, 208, 3132, 2984, 214, 1879, 2165, 219, 2641, 1884, 224,
1206 2161, 229, 2646, 1890, 235, 2166, 239, 2652, 2995, 245, 2171, 249,
1207 1900, 3778, 255, 1904, 2186, 260, 3782, 265, 1910, 3734, 270, 3978,
1208 276, 2187, 280, 3858, 3828, 286, 1920, 2667, 291, 3820, 1925, 296,
1209 2206, 301, 2672, 1931, 307, 2202, 311, 4056, 3387, 317, 2207, 321,
1210 3288, 3267, 327, 2212, 3962, 332, 4020, 337, 2218, 1951, 342, 4039,
1211 348, 1956, 352, 3026, 3158, 358, 1962, 2237, 363, 1966, 3739, 368,
1212 2233, 373, 3984, 1972, 379, 2238, 383, 3303, 3746, 389, 2243, 393,
1213 3410, 3789, 399, 2249, 2258, 404, 3406, 409, 3309, 1992, 414, 3964,
1214 420, 1997, 424, 3486, 3980, 430, 2003, 4038, 435, 2007, 3869, 440,
1215 2278, 445, 2013, 3896, 451, 2274, 455, 2734, 2018, 461, 2279, 465,
1216 2023, 3189, 471, 2284, 2028, 476, 3949, 481, 2290, 2034, 486, 2516,
1217 492, 2744, 496, 3067, 3302, 502, 2044, 2309, 507, 2048, 3199, 512,
1218 2305, 517, 2054, 3657, 523, 2310, 527, 2759, 2059, 533, 2315, 537,
1219 2064, 3876, 543, 2321, 2069, 548, 2929, 553, 2769, 2075, 558, 3510,
1220 564, 2331, 568, 3511, 2940, 574, 3344, 2775, 579, 3709, 3588, 584,
1221 2350, 589, 2780, 2095, 595, 2346, 599, 2100, 3098, 605, 2351, 609,
1222 2106, 3338, 615, 2110, 3521, 620, 4069, 625, 2362, 2116, 630, 2587,
1223 636, 2800, 640, 3725, 3230, 646, 2372, 2381, 651, 3806, 3877, 656,
1224 2377, 661, 3461, 2136, 667, 2382, 671, 2141, 3343, 677, 2387, 681,
1225 2147, 3886, 687, 2151, 2402, 692, 3937, 697, 2157, 2821, 702, 3349,
1226 708, 2403, 712, 3675, 3539, 718, 2167, 3462, 723, 3971, 2172, 728,
1227 2422, 733, 3781, 2178, 739, 2418, 743, 2841, 3139, 749, 2423, 753,
1228 2188, 3261, 759, 2192, 3680, 764, 3622, 769, 2198, 2443, 774, 3474,
1229 780, 2852, 784, 3276, 3364, 790, 2208, 2453, 795, 2857, 2213, 800,
1230 2449, 805, 2862, 2219, 811, 2454, 815, 2868, 3277, 821, 2459, 825,
1231 3396, 3825, 831, 2465, 2474, 836, 4007, 841, 2878, 2239, 846, 3472,
1232 852, 2244, 856, 3558, 3688, 862, 2250, 2883, 867, 2254, 2681, 872,
1233 2494, 877, 2888, 2260, 883, 2490, 887, 3644, 3495, 893, 2495, 897,
1234 3412, 3833, 903, 2500, 3568, 908, 4006, 913, 2506, 2280, 918, 3483,
1235 924, 2285, 928, 3756, 3190, 934, 2291, 2525, 939, 2295, 3401, 944,
1236 2521, 949, 2301, 3836, 955, 2526, 959, 3508, 2306, 965, 2531, 969,
1237 2311, 3840, 975, 2537, 2316, 980, 2732, 985, 3514, 2322, 990, 3420,
1238 996, 2547, 1000, 3583, 3710, 1006, 2332, 3595, 1011, 2336, 2752, 1016,
1239 2566, 1021, 2342, 3902, 3, 9, 1031, 14, 2347, 1037, 20, 24,
1240 2352, 3333, 30, 34, 2357, 40, 3663, 1057, 45, 50, 1062, 55,
1241 1068, 61, 65, 3348, 71, 1078, 2588, 76, 1083, 81, 86, 1088,
1242 2593, 92, 96, 2383, 1099, 102, 106, 2388, 112, 1109, 2603, 117,
1243 122, 3850, 127, 2398, 133, 137, 2803, 143, 2985, 2404, 148, 3442,
1244 153, 158, 1144, 4017, 164, 168, 3545, 2991, 174, 178, 3611, 184,
1245 2638, 1165, 189, 194, 1171, 199, 1175, 205, 209, 1181, 215, 1185,
1246 2435, 220, 1191, 225, 230, 1196, 3917, 236, 240, 2659, 1206, 246,
1247 250, 3016, 256, 3982, 3272, 261, 266, 2669, 271, 4064, 277, 281,
1248 2665, 287, 3894, 2466, 292, 2670, 297, 302, 3283, 1253, 308, 312,
1249 2476, 3861, 318, 322, 2690, 328, 4035, 1273, 333, 338, 1278, 343,
1250 1284, 349, 353, 3630, 359, 1294, 2496, 364, 1299, 369, 374, 1304,
1251 2710, 380, 384, 2507, 1315, 390, 394, 3057, 400, 1325, 2711, 405,
1252 410, 3405, 415, 2716, 421, 425, 3704, 431, 2722, 2527, 436, 3581,
1253 441, 446, 1360, 3314, 452, 456, 2538, 2741, 462, 466, 3415, 472,
1254 2737, 1381, 477, 482, 1387, 487, 1391, 493, 497, 1397, 503, 1401,
1255 3716, 508, 1407, 513, 518, 1412, 3875, 524, 528, 2568, 1422, 534,
1256 538, 2573, 544, 3655, 3667, 549, 554, 3099, 559, 2583, 565, 569,
1257 2782, 575, 2589, 3523, 580, 2778, 585, 590, 2594, 1469, 596, 600,
1258 2599, 3664, 606, 610, 2604, 616, 4074, 1489, 621, 626, 1494, 631,
1259 1500, 637, 641, 3355, 647, 1510, 2620, 652, 1515, 657, 662, 1520,
1260 2809, 668, 672, 3887, 1531, 678, 682, 3550, 688, 1541, 2819, 693,
1261 698, 4018, 703, 2825, 709, 713, 3263, 719, 3742, 2651, 724, 3847,
1262 729, 734, 1576, 3783, 740, 744, 3156, 3905, 750, 754, 3733, 760,
1263 2854, 1597, 765, 770, 1603, 775, 1607, 781, 785, 1613, 791, 1617,
1264 2682, 796, 1623, 801, 806, 1628, 4059, 812, 816, 2692, 1638, 822,
1265 826, 3176, 832, 3492, 3617, 837, 842, 2885, 847, 3181, 853, 857,
1266 2881, 863, 3187, 2712, 868, 2886, 873, 878, 3493, 1685, 884, 888,
1267 2723, 3897, 894, 898, 2906, 904, 3998, 1705, 909, 914, 1710, 919,
1268 1716, 925, 929, 3702, 935, 1726, 2743, 940, 1731, 945, 950, 1736,
1269 2926, 956, 960, 2754, 1747, 966, 970, 3597, 976, 1757, 2927, 981,
1270 986, 3928, 991, 2768, 997, 1001, 4096, 1007, 2774, 2947, 1012, 3091,
1271 1017, 1022, 1792, 3932, 1028, 1032, 2784, 2957, 1038, 1042, 2789, 1048,
1272 2953, 1813, 1053, 1058, 1819, 1063, 1823, 1069, 1073, 1829, 1079, 1833,
1273 3612, 1084, 1839, 1089, 1094, 1844, 4004, 1100, 1104, 2815, 1854, 1110,
1274 1114, 2820, 1120, 3727, 3361, 1125, 1130, 3678, 1135, 2830, 1141, 1145,
1275 2998, 1151, 3859, 2836, 1156, 2994, 1161, 1166, 4037, 1901, 1172, 1176,
1276 3628, 3549, 1182, 1186, 3737, 1192, 3832, 1921, 1197, 1202, 1926, 1207,
1277 1932, 1213, 1217, 3564, 1223, 1942, 2867, 1228, 1947, 1233, 1238, 1952,
1278 3025, 1244, 1248, 4010, 1963, 1254, 1258, 3300, 1264, 1973, 3035, 1269,
1279 1274, 3922, 1279, 3041, 1285, 1289, 3873, 1295, 3310, 2898, 1300, 3631,
1280 1305, 1310, 2008, 3966, 1316, 1320, 2908, 3315, 1326, 1330, 3185, 1336,
1281 3070, 2029, 1341, 1346, 2035, 1351, 2039, 1357, 1361, 2045, 1367, 2049,
1282 2928, 1372, 2055, 1377, 1382, 2060, 4033, 1388, 1392, 2939, 2070, 1398,
1283 1402, 4036, 1408, 3914, 3519, 1413, 1418, 3101, 1423, 3719, 1429, 1433,
1284 3097, 1439, 3909, 2959, 1444, 3102, 1449, 1454, 3530, 2117, 1460, 1464,
1285 2970, 3933, 1470, 1474, 3122, 1480, 3236, 2137, 1485, 1490, 2142, 1495,
1286 2148, 1501, 1505, 3774, 1511, 2158, 3372, 1516, 2163, 1521, 1526, 2168,
1287 3142, 1532, 1536, 3000, 2179, 1542, 1546, 3005, 1552, 2189, 3143, 1557,
1288 1562, 3621, 1567, 3015, 1573, 1577, 4021, 1583, 3021, 3163, 1588, 3479,
1289 1593, 1598, 2224, 3636, 1604, 1608, 3031, 3173, 1614, 1618, 3036, 1624,
1290 3169, 2245, 1629, 1634, 2251, 1639, 2255, 1645, 1649, 2261, 1655, 2265,
1291 3052, 1660, 2271, 1665, 1670, 2276, 3307, 1676, 1680, 3755, 2286, 1686,
1292 1690, 3195, 1696, 3799, 3308, 1701, 1706, 3423, 1711, 3708, 1717, 1721,
1293 3214, 1727, 3428, 3083, 1732, 3210, 1737, 1742, 3930, 2333, 1748, 1752,
1294 3720, 3760, 1758, 1762, 3809, 1768, 3989, 2353, 1773, 1778, 2358, 1783,
1295 2364, 1789, 1793, 3602, 1799, 2374, 3114, 1804, 2379, 1809, 1814, 2384,
1296 3241, 1820, 1824, 3124, 2395, 1830, 1834, 3735, 1840, 2405, 3251, 1845,
1297 1850, 3993, 1855, 3257, 1861, 1865, 4052, 1871, 3741, 3144, 1876, 3819,
1298 1881, 1886, 2440, 3891, 1892, 1896, 3155, 3786, 1902, 1906, 3374, 1912,
1299 3286, 2461, 1917, 1922, 2467, 1927, 2471, 1933, 1937, 2477, 1943, 2481,
1300 3175, 1948, 2487, 1953, 1958, 2492, 3904, 1964, 1968, 3186, 2502, 1974,
1301 1978, 3500, 1984, 3643, 3829, 1989, 1994, 3317, 1999, 3200, 2005, 2009,
1302 3313, 2015, 3206, 4092, 2020, 3318, 2025, 2030, 3211, 2549, 2036, 2040,
1303 3216, 3969, 2046, 2050, 3221, 2056, 4000, 2569, 2061, 2066, 2574, 2071,
1304 2580, 2077, 2081, 3846, 2087, 2590, 3776, 2092, 2595, 2097, 2102, 2600,
1305 3358, 2108, 2112, 3247, 2611, 2118, 2122, 3252, 2128, 2621, 3359, 2133,
1306 2138, 3771, 2143, 3262, 2149, 2153, 4061, 2159, 3370, 3268, 2164, 3945,
1307 2169, 2174, 2656, 3941, 2180, 2184, 3380, 3389, 2190, 2194, 4055, 2200,
1308 3385, 2677, 2205, 2210, 2683, 2215, 2687, 2221, 2225, 2693, 2231, 2697,
1309 3299, 2236, 2703, 2241, 2246, 2708, 3838, 2252, 2256, 3577, 2718, 2262,
1310 2266, 3411, 2272, 3871, 4073, 2277, 2282, 4067, 2287, 3967, 2293, 2297,
1311 3430, 2303, 3592, 3330, 2308, 3426, 2313, 2318, 3715, 2765, 2324, 2328,
1312 3340, 3765, 2334, 2338, 3881, 2344, 3910, 2785, 2349, 2354, 2790, 2359,
1313 2796, 2365, 2369, 3780, 2375, 2806, 3360, 2380, 2811, 2385, 2390, 2816,
1314 3457, 2396, 2400, 3371, 2827, 2406, 2410, 3623, 2416, 2837, 3467, 2421,
1315 2426, 3994, 2431, 3473, 2437, 2441, 3685, 2447, 3633, 3391, 2452, 4072,
1316 2457, 2462, 2872, 4028, 2468, 2472, 3402, 3639, 2478, 2482, 3987, 2488,
1317 3502, 2893, 2493, 2498, 2899, 2503, 2903, 2509, 2513, 2909, 2519, 2913,
1318 3844, 2524, 2919, 2529, 2534, 2924, 4087, 2540, 2544, 3432, 2934, 2550,
1319 2554, 3437, 2560, 3972, 3766, 2565, 2570, 3533, 2575, 3447, 2581, 2585,
1320 3529, 2591, 3453, 4060, 2596, 3534, 2601, 2606, 3458, 2981, 2612, 2616,
1321 3463, 4005, 2622, 2626, 3468, 2632, 3915, 3001, 2637, 2642, 3006, 2647,
1322 3012, 2653, 2657, 3918, 2663, 3022, 3484, 2668, 3027, 2673, 2678, 3032,
1323 3574, 2684, 2688, 3921, 3043, 2694, 2698, 3705, 2704, 3053, 3575, 2709,
1324 2714, 3837, 2719, 3580, 2725, 2729, 3951, 2735, 4, 10, 15, 25,
1325 35, 41, 51, 56, 66, 72, 82, 87, 97, 107, 113, 123,
1326 128, 138, 144, 154, 159, 169, 179, 185, 195, 200, 210, 216,
1327 226, 231, 241, 251, 257, 267, 272, 282, 288, 298, 303, 313,
1328 323, 329, 339, 344, 354, 360, 370, 375, 385, 395, 401, 411,
1329 416, 426, 432, 442, 447, 457, 467, 473, 483, 488, 498, 504,
1330 514, 519, 529, 539, 545, 555, 560, 570, 576, 586, 591, 601,
1331 611, 617, 627, 632, 642, 648, 658, 663, 673, 683, 689, 699,
1332 704, 714, 720, 730, 735, 745, 755, 761, 771, 776, 786, 792,
1333 802, 807, 817, 827, 833, 843, 848, 858, 864, 874, 879, 889,
1334 899, 905, 915, 920, 930, 936, 946, 951, 961, 971, 977, 987,
1335 992, 1002, 1008, 1018, 1023, 1033, 1043, 1049, 1059, 1064, 1074, 1080,
1336 1090, 1095, 1105, 1115, 1121, 1131, 1136, 1146, 1152, 1162, 1167, 1177,
1337 1187, 1193, 1203, 1208, 1218, 1224, 1234, 1239, 1249, 1259, 1265, 1275,
1338 1280, 1290, 1296, 1306, 1311, 1321, 1331, 1337, 1347, 1352, 1362, 1368,
1339 1378, 1383, 1393, 1403, 1409, 1419, 1424, 1434, 1440, 1450, 1455, 1465,
1340 1475, 1481, 1491, 1496, 1506, 1512, 1522, 1527, 1537, 1547, 1553, 1563,
1341 1568, 1578, 1584, 1594, 1599, 1609, 1619, 1625, 1635, 1640, 1650, 1656,
1342 1666, 1671, 1681, 1691, 1697, 1707, 1712, 1722, 1728, 1738, 1743, 1753,
1343 1763, 1769, 1779, 1784, 1794, 1800, 1810, 1815, 1825, 1835, 1841, 1851,
1344 1856, 1866, 1872, 1882, 1887, 1897, 1907, 1913, 1923, 1928, 1938, 1944,
1345 1954, 1959, 1969, 1979, 1985, 1995, 2000, 2010, 2016, 2026, 2031, 2041,
1346 2051, 2057, 2067, 2072, 2082, 2088, 2098, 2103, 2113, 2123, 2129, 2139,
1347 2144, 2154, 2160, 2170, 2175, 2185, 2195, 2201, 2211, 2216, 2226, 2232,
1348 2242, 2247, 2257, 2267, 2273, 2283, 2288, 2298, 2304, 2314, 2319, 2329,
1349 2339, 2345, 2355, 2360, 2370, 2376, 2386, 2391, 2401, 2411, 2417, 2427,
1350 2432, 2442, 2448, 2458, 2463, 2473, 2483, 2489, 2499, 2504, 2514, 2520,
1351 2530, 2535, 2545, 2555, 2561, 2571, 2576, 2586, 2592, 2602, 2607, 2617,
1352 2627, 2633, 2643, 2648, 2658, 2664, 2674, 2679, 2689, 2699, 2705, 2715,
1353 2720, 2730, 2736, 2746, 2751, 2761, 2771, 2777, 2787, 2792, 2802, 2808,
1354 2818, 2823, 2833, 2843, 2849, 2859, 2864, 2874, 2880, 2890, 2895, 2905,
1355 2915, 2921, 2931, 2936, 2946, 2952, 2962, 2967, 2977, 2987, 2993, 3003,
1356 3008, 3018, 3024, 3034, 3039, 3049, 3059, 3065, 3075, 3080, 3090, 3096,
1357 3106, 3111, 3121, 3131, 3137, 3147, 3152, 3162, 3168, 3178, 3183, 3193,
1358 3203, 3209, 3219, 3224, 3234, 3240, 3250, 3255, 3265, 3275, 3281, 3291,
1359 3296, 3306, 3312, 3322, 3327, 3337, 3347, 3353, 3363, 3368, 3378, 3384,
1360 3394, 3399, 3409, 3419, 3425, 3435, 3440, 3450, 3456, 3466, 3471, 3481,
1361 3491, 3497, 3507, 3512, 3522, 3528, 3538, 3543, 3553, 3563, 3569, 3579,
1362 3584, 3594, 3600, 3610, 3615, 3625, 3635, 3641, 3651, 3656, 3666, 3672,
1363 3682, 3687, 3697, 3707, 3713, 3723, 3728, 3738, 3744, 3754, 3759, 3769,
1364 3779, 3785, 3795, 3800, 3810, 3816, 3826, 3831, 3841, 3851, 3857, 3867,
1365 3872, 3882, 3888, 3898, 3903, 3913, 3923, 3929, 3939, 3944, 3954, 3960,
1366 3970, 3975, 3985, 3995, 4001, 4011, 4016, 4026, 4032, 4042, 4047, 4057,
1367 4089, 4090, 4094, 4095, 5
1368};
1369 50
1370static int 51static int
1371cmp(const void *v1, const void *v2) 52cmp(const void *v1, const void *v2)
@@ -1389,224 +70,207 @@ cmp_checked(const void *v1, const void *v2)
1389} 70}
1390 71
1391static int 72static int
1392check_result(char *prefix, int *got, int *expected, enum distribution dist, 73check_result(char *sub, int *got, int *expected, struct test_distribution *d,
1393 int m, int n) 74 int m, int n)
1394{ 75{
1395 int i; 76 int i;
1396 77
1397 if (compares > max_compares) { 78 if (verbose || compares > max_compares) {
1398 warnx("%s: %zu compares, max %zu, dist %d, m: %d, n: %d", 79 if (sub != NULL) {
1399 prefix, compares, max_compares, dist, m, n); 80 warnx("%s (%s): m: %d, n: %d, %zu compares, max %zu(%zu)",
81 d->name, sub, m, n, compares, max_compares, abrt_compares);
82 } else {
83 warnx("%s: m: %d, n: %d, %zu compares, max %zu(%zu)",
84 d->name, m, n, compares, max_compares, abrt_compares);
85 }
1400 } 86 }
1401 87
1402 for (i = 0; i < n; i++) { 88 for (i = 0; i < n; i++) {
1403 if (got[i] != expected[i]) { 89 if (got[i] != expected[i])
1404 warnx("%s: failure at %d, dist %d, m: %d, n: %d", 90 break;
1405 prefix, i, dist, m, n); 91 }
1406 return 1; 92 if (i == n)
1407 } 93 return 0;
94
95 if (sub != NULL) {
96 warnx("%s (%s): failure at %d, m: %d, n: %d",
97 d->name, sub, i, m, n);
98 } else {
99 warnx("%s: failure at %d, m: %d, n: %d",
100 d->name, i, m, n);
1408 } 101 }
1409 return 0; 102 return 1;
103}
104
105static void
106fill_sawtooth(int *x, int n, int m)
107{
108 int i;
109
110 for (i = 0; i < n; i++)
111 x[i] = i % m;
112}
113
114static void
115fill_random(int *x, int n, int m)
116{
117 int i;
118
119 for (i = 0; i < n; i++)
120 x[i] = arc4random_uniform(m);
121}
122
123static void
124fill_stagger(int *x, int n, int m)
125{
126 int i;
127
128 for (i = 0; i < n; i++)
129 x[i] = (i * m + i) % n;
1410} 130}
1411 131
1412static void 132static void
1413fill_test_array(int *x, int n, int dist, int m) 133fill_plateau(int *x, int n, int m)
134{
135 int i;
136
137 for (i = 0; i < n; i++)
138 x[i] = min(i, m);
139}
140
141static void
142fill_shuffle(int *x, int n, int m)
1414{ 143{
1415 int i, j, k; 144 int i, j, k;
1416 const int *bmk;
1417 145
1418 switch (dist) { 146 for (i = 0, j = 0, k = 1; i < n; i++)
1419 case SAWTOOTH: 147 x[i] = arc4random_uniform(m) ? (j += 2) : (k += 2);
1420 for (i = 0; i < n; i++) 148}
1421 x[i] = i % m; 149
1422 break; 150static void
1423 case RAND: 151fill_bsd_killer(int *x, int n, int m)
1424 for (i = 0; i < n; i++) 152{
1425 x[i] = arc4random_uniform(m); 153 int i, k;
1426 break; 154
1427 case STAGGER: 155 /* 4.4BSD insertion sort optimization killer, Mats Linander */
1428 for (i = 0; i < n; i++) 156 k = n / 2;
1429 x[i] = (i * m + i) % n; 157 for (i = 0; i < n; i++) {
1430 break; 158 if (i < k)
1431 case PLATEAU: 159 x[i] = k - i;
1432 for (i = 0; i < n; i++) 160 else if (i > k)
1433 x[i] = min(i, m); 161 x[i] = n + k + 1 - i;
1434 break; 162 else
1435 case SHUFFLE: 163 x[i] = k + 1;
1436 for (i = 0, j = 0, k = 1; i < n; i++) 164 }
1437 x[i] = arc4random_uniform(m) ? (j += 2) : (k += 2); 165}
1438 break; 166
1439 case BM_KILLER: 167static void
1440 switch (n) { 168fill_med3_killer(int *x, int n, int m)
1441 case 100: 169{
1442 bmk = bmkiller_100; 170 int i, k;
1443 break; 171
1444 case 1023: 172 /*
1445 bmk = bmkiller_1023; 173 * Median of 3 killer, as seen in David R Musser's
1446 break; 174 * "Introspective Sorting and Selection Algorithms"
1447 case 1024: 175 */
1448 bmk = bmkiller_1024; 176 if (n & 1) {
1449 break; 177 /* odd size, store last at end and make even. */
1450 case 1025: 178 x[n - 1] = n;
1451 bmk = bmkiller_1025; 179 n--;
1452 break; 180 }
1453 case 4095: 181 k = n / 2;
1454 bmk = bmkiller_4095; 182 for (i = 0; i < n; i++) {
1455 break; 183 if (i & 1) {
1456 case 4096: 184 x[i] = k + x[i - 1];
1457 bmk = bmkiller_4096; 185 } else {
1458 break; 186 x[i] = i + 1;
1459 case 4097:
1460 bmk = bmkiller_4097;
1461 break;
1462 default:
1463 err(1, "unexpected array length %d", n);
1464 }
1465 for (i = 0; i < n; i++)
1466 x[i] = bmk[i];
1467 break;
1468 case BSD_KILLER:
1469 /* 4.4BSD insertion sort optimization killer, Mats Linander */
1470 k = n / 2;
1471 for (i = 0; i < n; i++) {
1472 if (i < k)
1473 x[i] = k - i;
1474 else if (i > k)
1475 x[i] = n + k + 1 - i;
1476 else
1477 x[i] = k + 1;
1478 }
1479 break;
1480 case MED3_KILLER:
1481 /*
1482 * Median of 3 killer, as seen in David R Musser's
1483 * Introspective Sorting and Selection Algorithms
1484 */
1485 if (n & 1) {
1486 /* odd size, store last at end and make even. */
1487 x[n - 1] = n;
1488 n--;
1489 }
1490 k = n / 2;
1491 for (i = 0; i < n; i++) {
1492 if (i & 1) {
1493 x[i] = k + x[i - 1];
1494 } else {
1495 x[i] = i + 1;
1496 }
1497 } 187 }
1498 break;
1499 default:
1500 err(1, "unexpected distribution %d", dist);
1501 } 188 }
1502} 189}
1503 190
1504static int 191static int
1505test_distribution(int dist, int m, int n, int *x, int *y, int *z) 192do_test(struct test_distribution *d, char *sub, int m, int n, int *y, int *z)
1506{ 193{
1507 int i, j;
1508 int ret = 0; 194 int ret = 0;
1509 195
1510 /* Fill in x[] based on distribution and 'm' */
1511 fill_test_array(x, n, dist, m);
1512
1513 /* Test on copy of x[] */
1514 for (i = 0; i < n; i++)
1515 y[i] = z[i] = x[i];
1516 compares = 0; 196 compares = 0;
1517 if (sigsetjmp(cmpjmp, 1) != 0) { 197 if (sigsetjmp(cmpjmp, 1) != 0) {
1518 warnx("qsort aborted: %zu compares, dist %d, m: %d, n: %d", 198 if (sub != NULL) {
1519 compares, dist, m, n); 199 warnx("%s (%s): qsort aborted after %zu compares, m: %d, n: %d",
200 d->name, sub, compares, m, n);
201 } else {
202 warnx("%s: qsort aborted after %zu compares, m: %d, n: %d",
203 d->name, compares, m, n);
204 }
1520 ret = 1; 205 ret = 1;
1521 } else { 206 } else {
1522 qsort(y, n, sizeof(y[0]), cmp_checked); 207 qsort(y, n, sizeof(y[0]), cmp_checked);
208 if (check_result(sub, y, z, d, m, n) != 0)
209 ret = 1;
210 }
211 return ret;
212}
213
214static int
215test_perturbed(struct test_distribution *d, int n, int *x, int *y, int *z)
216{
217 int i, j, m;
218 int ret = 0;
219
220 for (m = 1; m < 2 * n; m *= 2) {
221 /* Fill in x[n] modified by m */
222 d->fill(x, n, m);
223
224 /* Test on copy of x[] */
225 for (i = 0; i < n; i++)
226 y[i] = z[i] = x[i];
1523 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 227 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1524 err(1, NULL); 228 err(1, NULL);
1525 if (check_result("copy", y, z, dist, m, n) != 0) 229 if (do_test(d, "copy", m, n, y, z) != 0)
1526 ret = 1; 230 ret = 1;
1527 }
1528 231
1529 /* Test on reversed copy of x[] */ 232 /* Test on reversed copy of x[] */
1530 for (i = 0, j = n - 1; i < n; i++, j--) 233 for (i = 0, j = n - 1; i < n; i++, j--)
1531 y[i] = z[i] = x[j]; 234 y[i] = z[i] = x[j];
1532 compares = 0;
1533 if (sigsetjmp(cmpjmp, 1) != 0) {
1534 warnx("qsort aborted (%s): %zu compares, dist %d, m: %d, n: %d",
1535 "reversed", compares, dist, m, n);
1536 ret = 1;
1537 } else {
1538 qsort(y, n, sizeof(y[0]), cmp_checked);
1539 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 235 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1540 err(1, NULL); 236 err(1, NULL);
1541 if (check_result("reversed", y, z, dist, m, n) != 0) 237 if (do_test(d, "reversed", m, n, y, z) != 0)
1542 ret = 1; 238 ret = 1;
1543 }
1544 239
1545 /* Test with front half of x[] reversed */ 240 /* Test with front half of x[] reversed */
1546 for (i = 0, j = (n / 2) - 1; i < n / 2; i++, j--) 241 for (i = 0, j = (n / 2) - 1; i < n / 2; i++, j--)
1547 y[i] = z[i] = x[j]; 242 y[i] = z[i] = x[j];
1548 for (; i < n; i++) 243 for (; i < n; i++)
1549 y[i] = z[i] = x[i]; 244 y[i] = z[i] = x[i];
1550 compares = 0;
1551 if (sigsetjmp(cmpjmp, 1) != 0) {
1552 warnx("qsort aborted (%s): %zu compares, dist %d, m: %d, n: %d",
1553 "front reversed", compares, dist, m, n);
1554 ret = 1;
1555 } else {
1556 qsort(y, n, sizeof(y[0]), cmp_checked);
1557 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 245 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1558 err(1, NULL); 246 err(1, NULL);
1559 if (check_result("front reversed", y, z, dist, m, n) != 0) 247 if (do_test(d, "front reversed", m, n, y, z) != 0)
1560 ret = 1; 248 ret = 1;
1561 }
1562 249
1563 /* Test with back half of x[] reversed */ 250 /* Test with back half of x[] reversed */
1564 for (i = 0; i < n / 2; i++) 251 for (i = 0; i < n / 2; i++)
1565 y[i] = z[i] = x[i]; 252 y[i] = z[i] = x[i];
1566 for (j = n - 1; i < n; i++, j--) 253 for (j = n - 1; i < n; i++, j--)
1567 y[i] = z[i] = x[j]; 254 y[i] = z[i] = x[j];
1568 compares = 0;
1569 if (sigsetjmp(cmpjmp, 1) != 0) {
1570 warnx("qsort aborted (%s): %zu compares, dist %d, m: %d, n: %d",
1571 "back reversed", compares, dist, m, n);
1572 ret = 1;
1573 } else {
1574 qsort(y, n, sizeof(y[0]), cmp_checked);
1575 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 255 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1576 err(1, NULL); 256 err(1, NULL);
1577 if (check_result("back reversed", y, z, dist, m, n) != 0) 257 if (do_test(d, "back reversed", m, n, y, z) != 0)
1578 ret = 1; 258 ret = 1;
1579 }
1580 259
1581 /* Test on sorted copy of x[] */ 260 /* Test on sorted copy of x[] */
1582 if (mergesort(x, n, sizeof(x[0]), cmp) != 0) 261 if (mergesort(x, n, sizeof(x[0]), cmp) != 0)
1583 err(1, NULL); 262 err(1, NULL);
1584 for (i = 0; i < n; i++) 263 for (i = 0; i < n; i++)
1585 y[i] = x[i]; 264 y[i] = x[i];
1586 compares = 0; 265 if (do_test(d, "sorted", m, n, y, x) != 0)
1587 if (sigsetjmp(cmpjmp, 1) != 0) {
1588 warnx("qsort aborted (%s): %zu compares, dist %d, m: %d, n: %d",
1589 "sorted", compares, dist, m, n);
1590 ret = 1;
1591 } else {
1592 qsort(y, n, sizeof(y[0]), cmp_checked);
1593 if (check_result("sorted", y, x, dist, m, n) != 0)
1594 ret = 1; 266 ret = 1;
1595 }
1596 267
1597 /* Test with i%5 added to x[i] (dither) */ 268 /* Test with i%5 added to x[i] (dither) */
1598 for (i = 0, j = n - 1; i < n; i++, j--) 269 for (i = 0, j = n - 1; i < n; i++, j--)
1599 y[i] = z[i] = x[j] + (i % 5); 270 y[i] = z[i] = x[j] + (i % 5);
1600 compares = 0;
1601 if (sigsetjmp(cmpjmp, 1) != 0) {
1602 warnx("qsort aborted (%s): %zu compares, dist %d, m: %d, n: %d",
1603 "dithered", compares, dist, m, n);
1604 ret = 1;
1605 } else {
1606 qsort(y, n, sizeof(y[0]), cmp_checked);
1607 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 271 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1608 err(1, NULL); 272 err(1, NULL);
1609 if (check_result("dithered", y, z, dist, m, n) != 0) 273 if (do_test(d, "front reversed", m, n, y, z) != 0)
1610 ret = 1; 274 ret = 1;
1611 } 275 }
1612 276
@@ -1614,52 +278,87 @@ test_distribution(int dist, int m, int n, int *x, int *y, int *z)
1614} 278}
1615 279
1616/* 280/*
1617 * Like test_distribution() but because the input is tailored to cause 281 * Like test_perturbed() but because the input is tailored to cause
1618 * quicksort to go quadratic we don't perturb the input. 282 * quicksort to go quadratic we don't perturb the input.
1619 */ 283 */
1620static int 284static int
1621test_killer(int dist, int n, int *x, int *y, int *z) 285test_simple(struct test_distribution *d, int n, int *x, int *y, int *z)
1622{ 286{
1623 int i, ret = 0; 287 int i, ret = 0;
1624 288
1625 /* Fill in x[] with "killer" input */ 289 /* Fill in x[n] */
1626 fill_test_array(x, n, dist, 0); 290 d->fill(x, n, 0);
1627 291
1628 /* Make a copy of x[] */ 292 /* Make a copy of x[] */
1629 for (i = 0; i < n; i++) 293 for (i = 0; i < n; i++)
1630 y[i] = z[i] = x[i]; 294 y[i] = z[i] = x[i];
1631 compares = 0; 295 if (mergesort(z, n, sizeof(z[0]), cmp) != 0)
1632 if (sigsetjmp(cmpjmp, 1) != 0) { 296 err(1, NULL);
1633 warnx("qsort aborted: %zu compares, dist %d, n: %d", 297 if (do_test(d, NULL, 0, n, y, z) != 0)
1634 compares, dist, n);
1635 ret = 1; 298 ret = 1;
1636 } else { 299
1637 qsort(y, n, sizeof(y[0]), cmp_checked); 300 return ret;
1638 if (mergesort(z, n, sizeof(z[0]), cmp) != 0) 301}
1639 err(1, NULL); 302
1640 /* For killer input we don't check max_compares. */ 303/*
1641 compares = 0; 304 * Use D. McIlroy's "Killer Adversary for Quicksort"
1642 if (check_result("killer", y, z, dist, 0, n) != 0) 305 * We don't compare the results in this case.
1643 ret = 1; 306 */
307static int
308test_antiqsort(struct test_distribution *d, int n, int *x, int *y, int *z)
309{
310 int i, ret = 0;
311
312 /*
313 * We expect antiqsort to generate > 1.5 * nlgn compares.
314 * If introspection is not used, it will be > 10 * nlgn compares.
315 */
316 i = antiqsort(n, x, y);
317 if (i > abrt_compares)
318 ret = 1;
319 if (dump_table) {
320 printf("/* %d items, %d compares */\n", n, i);
321 printf("static const int table_%d[] = {", n);
322 for (i = 0; i < n - 1; i++) {
323 if ((i % 12) == 0)
324 printf("\n\t");
325 printf("%4d, ", x[i]);
326 }
327 printf("%4d\n};\n", x[i]);
328 } else if (verbose || ret != 0) {
329 warnx("%s: n: %d, %d compares, max %zu(%zu)",
330 d->name, n, i, max_compares, abrt_compares);
1644 } 331 }
1645 332
1646 return ret; 333 return ret;
1647} 334}
1648 335
336static struct test_distribution distributions[] = {
337 { "sawtooth", fill_sawtooth, test_perturbed },
338 { "random", fill_random, test_perturbed },
339 { "stagger", fill_stagger, test_perturbed },
340 { "plateau", fill_plateau, test_perturbed },
341 { "shuffle", fill_shuffle, test_perturbed },
342 { "bsd_killer", fill_bsd_killer, test_simple },
343 { "med3_killer", fill_med3_killer, test_simple },
344 { "antiqsort", NULL, test_antiqsort },
345 { NULL }
346};
347
1649static int 348static int
1650run_tests(int n) 349run_tests(int n)
1651{ 350{
1652 int *x, *y, *z; 351 int *x, *y, *z;
1653 int m, ret = 0; 352 int i, nlgn = 0;
1654 int idx, nlgn = 0; 353 int ret = 0;
1655 enum distribution dist; 354 struct test_distribution *d;
1656 355
1657 /* 356 /*
1658 * We expect A*n*lg(n) compares where A is between 1 and 2. 357 * We expect A*n*lg(n) compares where A is between 1 and 2.
1659 * For A > 1.5, print a warning. 358 * For A > 1.5, print a warning.
1660 * For A > 10 abort the test since qsort has probably gone quadratic. 359 * For A > 10 abort the test since qsort has probably gone quadratic.
1661 */ 360 */
1662 for (idx = n - 1; idx > 0; idx >>= 1) 361 for (i = n - 1; i > 0; i >>= 1)
1663 nlgn++; 362 nlgn++;
1664 nlgn *= n; 363 nlgn *= n;
1665 max_compares = nlgn * 1.5; 364 max_compares = nlgn * 1.5;
@@ -1671,21 +370,9 @@ run_tests(int n)
1671 if (x == NULL || y == NULL || z == NULL) 370 if (x == NULL || y == NULL || z == NULL)
1672 err(1, NULL); 371 err(1, NULL);
1673 372
1674 for (dist = SAWTOOTH; dist != INVALID; dist++) { 373 for (d = distributions; d->name != NULL; d++) {
1675 switch (dist) { 374 if (d->test(d, n, x, y, z) != 0)
1676 case BM_KILLER: 375 ret = 1;
1677 case BSD_KILLER:
1678 case MED3_KILLER:
1679 if (test_killer(dist, n, x, y, z) != 0)
1680 ret = 1;
1681 break;
1682 default:
1683 for (m = 1; m < 2 * n; m *= 2) {
1684 if (test_distribution(dist, m, n, x, y, z) != 0)
1685 ret = 1;
1686 }
1687 break;
1688 }
1689 } 376 }
1690 377
1691 free(x); 378 free(x);
@@ -1694,15 +381,46 @@ run_tests(int n)
1694 return ret; 381 return ret;
1695} 382}
1696 383
384__dead void
385usage(void)
386{
387 fprintf(stderr, "usage: qsort_test [-dv] [num ...]\n");
388 exit(1);
389}
390
1697int 391int
1698main(int argc, char *argv[]) 392main(int argc, char *argv[])
1699{ 393{
1700 int *nn, nums[] = { 100, 1023, 1024, 1025, 4095, 4096, 4097, -1 }; 394 char *nums[] = { "100", "1023", "1024", "1025", "4095", "4096", "4097" };
1701 int n, ret = 0; 395 int ch, n, ret = 0;
396
397 while ((ch = getopt(argc, argv, "dv")) != -1) {
398 switch (ch) {
399 case 'd':
400 dump_table = true;
401 break;
402 case 'v':
403 verbose = true;
404 break;
405 default:
406 usage();
407 break;
408 }
409 }
410 argc -= optind;
411 argv += optind;
412
413 if (argc == 0) {
414 argv = nums;
415 argc = sizeof(nums) / sizeof(nums[0]);
416 }
1702 417
1703 for (nn = nums; (n = *nn) > 0; nn++) { 418 while (argc > 0) {
419 n = atoi(*argv);
1704 if (run_tests(n) != 0) 420 if (run_tests(n) != 0)
1705 ret = 1; 421 ret = 1;
422 argc--;
423 argv++;
1706 } 424 }
1707 425
1708 return ret; 426 return ret;
generated by cgit v1.2.3-55-g6feb (git 2.39.1) at 2025-03-20 13:29:54 +0000