// See LICENSE for license details.


#define DATA_SIZE 1000

int input1_data[DATA_SIZE] =
{
   41, 833, 564, 187, 749, 350, 132, 949, 584, 805, 621,   6, 931, 890, 392, 694, 961, 110, 116, 296,
  426, 314, 659, 774, 319, 678, 875, 376, 474, 938, 539, 569, 203, 280, 759, 606, 511, 657, 195,  81,
  267, 229, 337, 944, 902, 241, 913, 826, 933, 985, 195, 960, 566, 350, 649, 657, 181, 111, 859,  65,
  288, 349, 141, 905, 886, 264, 576, 979, 761, 241, 478, 499, 403, 222, 444, 721, 676, 317, 224, 937,
  288, 119, 615, 606, 389, 351, 455, 278, 367, 358, 584,  62, 985, 403, 346, 517, 559, 908, 775, 255,
  778, 598, 143,  33, 125, 941, 933, 799, 553, 431, 648, 952, 287,  19,  49,  86,  95, 441, 587, 614,
  382, 280, 808, 971, 819, 344, 450, 512, 965, 347, 808, 882, 537, 946, 701, 356, 567, 891,  22, 568,
  665, 423, 434, 158,   2,  84, 247,  49, 435, 792, 869, 486, 414, 369, 548, 518, 888, 682, 284, 264,
  499, 290, 897, 215, 731, 688, 251, 786, 555, 302, 528, 544, 322, 947, 287, 824, 304, 788, 733, 959,
  366, 722, 294, 975, 653, 748,  91, 378, 105, 102, 381, 651, 825, 840, 356, 148,  54, 140, 955, 343,
  533, 757, 521, 837, 592,  13, 173,  63, 121, 133, 758, 372, 951,  39, 129, 110, 847, 437, 255, 269,
  409, 628, 399, 549, 753, 564, 171,  19, 727, 501, 777,  43, 753,  81, 202, 853, 153, 760, 357, 943,
  922, 328, 496, 442, 516, 641, 276, 786, 113, 842, 907, 275, 237,  32, 784, 565, 357, 803, 819, 751,
  280,  85, 458, 454, 710, 459,  41, 253, 377, 508, 700, 860, 480, 741, 499, 709,  49, 371, 873, 945,
  992, 526, 721, 435, 232, 497, 697,  30, 348, 250, 350, 250, 573, 784, 749, 502, 823, 826, 170, 160,
  674,  32, 202, 143, 853,  90, 394, 107, 855, 106, 157,   6, 765, 204, 194, 574, 218, 526, 177, 239,
  698, 757, 706,  49,  84, 799, 893, 512, 373, 492,  14, 621,  83, 103, 794, 921, 643, 880, 834, 239,
  462, 114, 561, 529,  10, 997, 904, 387, 407, 105, 559, 936, 512, 409, 302, 202, 427, 613, 359, 521,
  684,  22, 185, 312, 107, 274, 387, 242, 486, 105, 698, 899, 770, 644,  80, 161, 407, 946,  30, 768,
  870, 113, 148,  62, 147, 838, 845, 432, 141, 211, 817, 821, 562, 364, 615, 495, 812, 916, 159, 430,
  803, 180, 544, 840, 458, 786, 872, 795, 806, 758, 104, 401, 254, 984, 136, 729, 584, 794, 414, 528,
  707, 554, 378, 766, 977, 236, 947, 229, 165, 505, 105, 704, 796, 140, 303, 795, 635, 560, 119,   8,
  532, 814,  37, 584, 739, 619, 767, 478,  57, 958, 784, 985, 837, 307,  67, 824, 996, 749, 171, 826,
  621, 155, 826,  43, 694,  80, 236, 747, 744, 265, 124, 731, 941, 425, 370, 320, 269, 542, 763, 752,
  915,  14,   1, 906, 995, 809, 560, 873, 972, 289, 509, 558, 970, 405, 579, 293, 251, 849, 129, 452,
  716,  86, 678, 181, 240, 335, 793, 641,   1, 320, 987, 646, 754, 958, 203, 142, 180, 299, 165, 761,
  974, 646, 559, 619, 422, 260, 565, 542, 492, 991, 745, 207, 372, 932, 664,  34, 533, 478, 908, 203,
   33, 214, 365, 892, 781, 680, 705, 688, 947, 386,  50, 101, 474, 399, 679, 330, 952, 471, 477, 725,
  713, 937, 529, 870,  77, 545, 907, 853, 143, 979, 239, 105, 365,  98,  54,  98, 440, 764, 315, 336,
  697, 774, 726, 324, 282, 536, 622, 594, 890,  75, 290, 496, 726, 449, 548, 135, 644, 838, 290, 767,
  162, 415, 491, 985, 116, 617, 859, 235, 282, 571, 913, 560, 194, 242, 782, 985, 728, 344, 430, 613,
  759, 176, 309, 333, 354, 310, 699,  46, 487, 503, 100, 393, 268, 314,  75, 345, 987, 600, 908, 384,
   92, 545, 277, 668, 351, 853, 863, 312, 100, 532, 567, 836, 370, 989, 461, 912, 182, 268, 160, 771,
   22, 854, 644,  17, 779, 911, 855, 137, 983, 717, 565, 719, 253, 785, 154, 196, 253, 447, 899,   5,
  325, 616, 309, 175, 159, 123, 838, 715, 550, 230,  82, 627, 324, 927, 103,  17, 966, 159, 177, 593,
  372, 393, 599, 745, 377, 865, 591, 553, 440, 345, 593, 290, 908, 544, 377, 456, 781, 110, 495, 896,
  806, 700, 548, 340,  29, 829, 630, 546, 613, 972, 116, 313, 904, 971, 607, 794, 169, 896, 507, 916,
  431, 339, 147, 224, 112, 580, 834, 134, 948, 201, 488, 396, 797, 478, 769, 574, 485, 339, 721, 451,
  821, 744,   0, 594, 277, 120, 680, 757, 555, 847, 517, 379, 505, 904, 246, 243, 394, 430, 214, 244,
  524, 399, 172, 304, 620, 594, 535, 698, 159, 750, 809, 454,  75,  93, 167,  16, 853, 494, 324,  78,
   52, 112,  10, 342, 730, 680, 287, 961,  92, 626, 912, 616, 860, 744, 744, 478, 615, 508, 914, 810,
  288, 974, 129, 581, 548, 868, 981, 270, 623, 653, 626, 990, 386, 323, 472, 164, 239, 189, 865, 231,
  356, 152, 825, 328, 390, 848,  38, 402, 616, 546, 206,   2, 783, 890, 815, 831, 665, 410,  94, 246,
  422, 211, 675,   9, 374, 426,  64,  53, 758, 811, 500, 437, 335, 328, 237, 415, 468, 684, 565, 305,
  449, 597, 136, 882, 383, 938, 268, 115, 908,  50, 952, 366, 397, 257, 231, 667,  35, 990, 443, 213,
  389,  13, 621,  52, 612, 934, 953, 828, 462, 621, 812, 522, 672,  57, 313, 352,  55, 972, 753, 416,
  879, 864, 572, 163, 721,  12, 643, 507, 968, 781, 840, 242, 630, 810, 795, 435, 885, 599, 696, 643,
   93, 710, 785, 112, 581,  12, 923, 615, 652, 359, 261, 233, 609, 686, 539, 118, 560, 739,  20, 317,
  976, 573, 386, 772, 663, 504, 212, 888, 907, 420, 737, 516,  25, 219, 797, 716, 452, 692, 683, 459,
  815, 323, 612, 247, 116, 352, 281, 738, 290, 909, 645, 625, 932, 220, 685, 373, 876, 646, 412, 955
};

int input2_data[DATA_SIZE] =
{
  454, 335,   1, 989, 365, 572,  64, 153, 216, 140, 210, 572, 339, 593, 898, 228,  12, 883, 750, 646,
  500, 436, 701, 812, 981, 150, 696, 564, 272, 258, 647, 509,  88, 703, 669, 375, 551, 936, 592, 569,
  952, 800, 584, 643, 368, 489, 328, 313, 592, 388, 543, 649, 979, 997, 814,  79, 208, 998, 629, 847,
  704, 997, 253, 715, 430, 415, 538, 700,   4, 494, 100, 864, 693, 416, 296, 285, 620,  78, 351, 540,
  646, 169, 527, 289, 796, 801, 720, 758, 745,  92, 989, 271, 853, 788, 531, 222, 461, 241, 358, 332,
  684, 740, 446, 311, 743, 557, 479, 557, 925, 796, 357, 891, 666, 514, 557, 870, 853, 440,  61, 678,
  396,   9,  17, 170, 291, 380, 536, 185, 917, 539, 983, 887,  54, 612, 951, 479, 151,   7, 641, 335,
  730,  95, 728, 280, 395, 688, 911, 476, 815, 729, 265, 127, 236, 214, 180,   6, 503, 596, 173, 643,
  346, 599,  68, 849, 658, 619, 121, 131, 828, 667, 433, 487, 753, 125, 626,  14,  10, 403, 106, 703,
  818, 964, 406, 874, 856,  86,  60, 660, 667, 153, 121,  98, 412, 236,  12, 423, 965, 216, 621, 361,
  921, 715, 647, 299, 886, 682,  36, 493, 551, 537, 969, 643, 434, 415, 303, 438, 860, 203, 478, 988,
  675, 719, 990, 338, 450, 633, 155, 646, 452, 427, 509, 988, 426,  12, 483, 142, 339, 390,  50, 171,
  601, 105, 968, 121, 879,  81, 870, 600, 603, 871, 887, 610, 404, 234, 745, 526, 275, 441, 226, 752,
  943, 726, 709, 201,  54, 758,  53, 397,  41, 141, 416, 747, 219, 478, 770, 180, 482, 691, 725, 173,
  186, 914,   1, 963, 247, 464, 362, 521, 233, 120,  40, 779, 195, 161, 743, 439, 355, 403, 141, 633,
  289, 782, 320, 636, 118, 852,  70, 816, 388, 954,  36,  16, 698, 695, 677, 598, 883, 824, 746, 462,
  511, 534, 440, 428, 732, 726, 702, 547,  86, 798, 215,  21, 651,  59, 429, 657,  96, 973, 659, 966,
  524,  62, 625, 303, 714, 409,  55, 728, 305, 436, 901, 592, 691, 796, 497, 177, 940, 995, 480, 158,
  822, 611, 680,  14, 111, 797, 185,   0, 718,  96, 749, 739, 814, 435, 326,  37,  33, 605, 935,  27,
   88, 441, 339, 344, 554, 365, 954, 639, 396, 991, 249, 338, 832, 974, 393, 266, 470, 348, 336, 419,
  249, 215, 542, 903, 636, 729, 581, 820, 671, 979, 418, 670, 920, 568, 745, 662, 139, 385, 927, 173,
  457, 316, 183, 477, 196, 399, 416, 805, 996, 270, 735, 696, 825, 528,  50, 623, 537,  87, 294, 867,
  110, 398, 781, 646, 375, 943, 897, 589,  44, 288, 845, 742,  99, 522, 443, 432, 165, 930,  28, 461,
  323, 272, 376, 340, 898, 158, 168, 443, 193, 631, 935, 274, 781, 185, 619, 292, 933, 156, 827,  88,
  987, 629, 649,  32,   1, 744, 399, 915, 791, 554, 984, 530, 600, 401, 683, 540, 903, 120, 995, 521,
  622, 224, 895, 530, 820, 651, 226,  96, 262, 569, 238, 126, 610, 191, 238, 796, 884, 573, 108, 140,
  789, 852,  23, 704, 890, 480,  52, 372, 201, 546, 408, 119, 645, 464,  81, 293,  52, 880, 224, 744,
  735, 886, 167,   1, 532, 321, 169, 485, 101, 177,  42, 708, 654, 915, 625, 242, 822, 795, 641, 252,
  245, 151, 876, 333, 601, 938, 775, 397, 233, 755, 454, 424, 210, 962, 900, 923, 655, 529, 595,  90,
  464, 685,  70, 754,  32, 494,  25, 389, 488,  37, 409, 639,  27, 950, 539,  80, 303, 723, 734, 125,
  552, 248, 107, 362,  48, 869, 144, 841, 724, 335, 470, 263, 343, 809, 677, 339, 336, 410, 465,  56,
  590, 485, 406, 993, 746, 238, 525, 336, 256, 134, 546, 722, 367, 943, 106, 629, 396, 208, 429, 523,
  130, 355, 990, 673, 991, 719, 449,  84, 616, 211, 707, 737, 847, 452, 316, 974, 746, 796, 522, 618,
  115, 727, 226, 165, 200, 830, 742, 187, 705, 671, 785, 886, 962, 657, 293, 620, 144, 173, 796,  72,
  678,  80, 793, 685, 637, 967, 241, 898, 693, 372, 601, 721, 398, 553,  72, 174, 978, 325, 558, 185,
  505, 859, 651, 573, 321, 349, 400, 890, 844, 885, 933, 980, 448, 989,  50, 332, 900, 716, 747, 444,
    6, 394, 285, 703, 450, 652, 771, 485, 534, 559, 481, 507, 434, 343,  42, 784, 865, 421, 415, 871,
  539, 162, 105, 481, 595, 115, 350, 964, 287, 232, 154, 602, 539, 943, 872, 121, 652, 811, 747, 362,
  340, 910, 206, 572, 505, 973, 961, 354, 627, 849, 971, 910, 410, 770,  63, 874, 396, 482, 619, 646,
  557, 328,  67, 884, 512, 972,   6, 513, 882, 562, 764, 366, 506, 786, 831, 382, 638, 452,  72,  83,
   59, 932, 929, 924, 961,  69, 797, 985, 854, 885, 600, 389, 232, 793, 179, 773, 689, 775, 494, 139,
  234, 431, 780, 371,  22, 653, 741, 815, 428, 139, 603, 315, 344, 889, 317, 260, 861, 377, 511, 304,
   70,  35, 854, 576, 490, 326, 303, 431, 813, 708, 388, 962, 967, 442,  49, 831, 251, 321, 741, 179,
  176, 117, 523, 764, 952, 704, 531, 804,  23, 611, 846, 375, 854, 971,  24, 639, 318, 723, 662, 647,
  281, 158, 294, 885, 734, 866, 471, 296, 673, 472, 439,   5, 155, 506, 948, 600, 445, 222, 784, 349,
  943, 150, 366, 444, 604, 720, 340, 972, 911, 321, 435,  50,  78, 761, 950, 238,  27, 226, 201, 176,
  877, 450, 879,  99, 143,  31, 812, 771, 527, 488, 797, 194, 293, 966, 276, 345, 413, 197, 386, 116,
  322, 680, 538, 553, 960, 874,  48, 506, 898, 539, 495, 764, 805, 286, 432, 836, 192, 825, 778, 586,
  359, 352, 746,  11, 749,   5, 408, 643, 441, 368,  97, 169, 359, 527, 672,  69, 880, 298, 300, 327,
  923, 829, 816, 497, 243, 981, 917, 713, 653, 503, 406, 543, 108, 304, 464, 954,  86, 802, 446,  28
};

int verify_data[DATA_SIZE] =
{
  495, 1168, 565, 1176, 1114, 922, 196, 1102, 800, 945, 831, 578, 1270, 1483, 1290, 922, 973, 993, 866, 942,
  926, 750, 1360, 1586, 1300, 828, 1571, 940, 746, 1196, 1186, 1078, 291, 983, 1428, 981, 1062, 1593, 787, 650,
  1219, 1029, 921, 1587, 1270, 730, 1241, 1139, 1525, 1373, 738, 1609, 1545, 1347, 1463, 736, 389, 1109, 1488, 912,
  992, 1346, 394, 1620, 1316, 679, 1114, 1679, 765, 735, 578, 1363, 1096, 638, 740, 1006, 1296, 395, 575, 1477,
  934, 288, 1142, 895, 1185, 1152, 1175, 1036, 1112, 450, 1573, 333, 1838, 1191, 877, 739, 1020, 1149, 1133, 587,
  1462, 1338, 589, 344, 868, 1498, 1412, 1356, 1478, 1227, 1005, 1843, 953, 533, 606, 956, 948, 881, 648, 1292,
  778, 289, 825, 1141, 1110, 724, 986, 697, 1882, 886, 1791, 1769, 591, 1558, 1652, 835, 718, 898, 663, 903,
  1395, 518, 1162, 438, 397, 772, 1158, 525, 1250, 1521, 1134, 613, 650, 583, 728, 524, 1391, 1278, 457, 907,
  845, 889, 965, 1064, 1389, 1307, 372, 917, 1383, 969, 961, 1031, 1075, 1072, 913, 838, 314, 1191, 839, 1662,
  1184, 1686, 700, 1849, 1509, 834, 151, 1038, 772, 255, 502, 749, 1237, 1076, 368, 571, 1019, 356, 1576, 704,
  1454, 1472, 1168, 1136, 1478, 695, 209, 556, 672, 670, 1727, 1015, 1385, 454, 432, 548, 1707, 640, 733, 1257,
  1084, 1347, 1389, 887, 1203, 1197, 326, 665, 1179, 928, 1286, 1031, 1179,  93, 685, 995, 492, 1150, 407, 1114,
  1523, 433, 1464, 563, 1395, 722, 1146, 1386, 716, 1713, 1794, 885, 641, 266, 1529, 1091, 632, 1244, 1045, 1503,
  1223, 811, 1167, 655, 764, 1217,  94, 650, 418, 649, 1116, 1607, 699, 1219, 1269, 889, 531, 1062, 1598, 1118,
  1178, 1440, 722, 1398, 479, 961, 1059, 551, 581, 370, 390, 1029, 768, 945, 1492, 941, 1178, 1229, 311, 793,
  963, 814, 522, 779, 971, 942, 464, 923, 1243, 1060, 193,  22, 1463, 899, 871, 1172, 1101, 1350, 923, 701,
  1209, 1291, 1146, 477, 816, 1525, 1595, 1059, 459, 1290, 229, 642, 734, 162, 1223, 1578, 739, 1853, 1493, 1205,
  986, 176, 1186, 832, 724, 1406, 959, 1115, 712, 541, 1460, 1528, 1203, 1205, 799, 379, 1367, 1608, 839, 679,
  1506, 633, 865, 326, 218, 1071, 572, 242, 1204, 201, 1447, 1638, 1584, 1079, 406, 198, 440, 1551, 965, 795,
  958, 554, 487, 406, 701, 1203, 1799, 1071, 537, 1202, 1066, 1159, 1394, 1338, 1008, 761, 1282, 1264, 495, 849,
  1052, 395, 1086, 1743, 1094, 1515, 1453, 1615, 1477, 1737, 522, 1071, 1174, 1552, 881, 1391, 723, 1179, 1341, 701,
  1164, 870, 561, 1243, 1173, 635, 1363, 1034, 1161, 775, 840, 1400, 1621, 668, 353, 1418, 1172, 647, 413, 875,
  642, 1212, 818, 1230, 1114, 1562, 1664, 1067, 101, 1246, 1629, 1727, 936, 829, 510, 1256, 1161, 1679, 199, 1287,
  944, 427, 1202, 383, 1592, 238, 404, 1190, 937, 896, 1059, 1005, 1722, 610, 989, 612, 1202, 698, 1590, 840,
  1902, 643, 650, 938, 996, 1553, 959, 1788, 1763, 843, 1493, 1088, 1570, 806, 1262, 833, 1154, 969, 1124, 973,
  1338, 310, 1573, 711, 1060, 986, 1019, 737, 263, 889, 1225, 772, 1364, 1149, 441, 938, 1064, 872, 273, 901,
  1763, 1498, 582, 1323, 1312, 740, 617, 914, 693, 1537, 1153, 326, 1017, 1396, 745, 327, 585, 1358, 1132, 947,
  768, 1100, 532, 893, 1313, 1001, 874, 1173, 1048, 563,  92, 809, 1128, 1314, 1304, 572, 1774, 1266, 1118, 977,
  958, 1088, 1405, 1203, 678, 1483, 1682, 1250, 376, 1734, 693, 529, 575, 1060, 954, 1021, 1095, 1293, 910, 426,
  1161, 1459, 796, 1078, 314, 1030, 647, 983, 1378, 112, 699, 1135, 753, 1399, 1087, 215, 947, 1561, 1024, 892,
  714, 663, 598, 1347, 164, 1486, 1003, 1076, 1006, 906, 1383, 823, 537, 1051, 1459, 1324, 1064, 754, 895, 669,
  1349, 661, 715, 1326, 1100, 548, 1224, 382, 743, 637, 646, 1115, 635, 1257, 181, 974, 1383, 808, 1337, 907,
  222, 900, 1267, 1341, 1342, 1572, 1312, 396, 716, 743, 1274, 1573, 1217, 1441, 777, 1886, 928, 1064, 682, 1389,
  137, 1581, 870, 182, 979, 1741, 1597, 324, 1688, 1388, 1350, 1605, 1215, 1442, 447, 816, 397, 620, 1695,  77,
  1003, 696, 1102, 860, 796, 1090, 1079, 1613, 1243, 602, 683, 1348, 722, 1480, 175, 191, 1944, 484, 735, 778,
  877, 1252, 1250, 1318, 698, 1214, 991, 1443, 1284, 1230, 1526, 1270, 1356, 1533, 427, 788, 1681, 826, 1242, 1340,
  812, 1094, 833, 1043, 479, 1481, 1401, 1031, 1147, 1531, 597, 820, 1338, 1314, 649, 1578, 1034, 1317, 922, 1787,
  970, 501, 252, 705, 707, 695, 1184, 1098, 1235, 433, 642, 998, 1336, 1421, 1641, 695, 1137, 1150, 1468, 813,
  1161, 1654, 206, 1166, 782, 1093, 1641, 1111, 1182, 1696, 1488, 1289, 915, 1674, 309, 1117, 790, 912, 833, 890,
  1081, 727, 239, 1188, 1132, 1566, 541, 1211, 1041, 1312, 1573, 820, 581, 879, 998, 398, 1491, 946, 396, 161,
  111, 1044, 939, 1266, 1691, 749, 1084, 1946, 946, 1511, 1512, 1005, 1092, 1537, 923, 1251, 1304, 1283, 1408, 949,
  522, 1405, 909, 952, 570, 1521, 1722, 1085, 1051, 792, 1229, 1305, 730, 1212, 789, 424, 1100, 566, 1376, 535,
  426, 187, 1679, 904, 880, 1174, 341, 833, 1429, 1254, 594, 964, 1750, 1332, 864, 1662, 916, 731, 835, 425,
  598, 328, 1198, 773, 1326, 1130, 595, 857, 781, 1422, 1346, 812, 1189, 1299, 261, 1054, 786, 1407, 1227, 952,
  730, 755, 430, 1767, 1117, 1804, 739, 411, 1581, 522, 1391, 371, 552, 763, 1179, 1267, 480, 1212, 1227, 562,
  1332, 163, 987, 496, 1216, 1654, 1293, 1800, 1373, 942, 1247, 572, 750, 818, 1263, 590,  82, 1198, 954, 592,
  1756, 1314, 1451, 262, 864,  43, 1455, 1278, 1495, 1269, 1637, 436, 923, 1776, 1071, 780, 1298, 796, 1082, 759,
  415, 1390, 1323, 665, 1541, 886, 971, 1121, 1550, 898, 756, 997, 1414, 972, 971, 954, 752, 1564, 798, 903,
  1335, 925, 1132, 783, 1412, 509, 620, 1531, 1348, 788, 834, 685, 384, 746, 1469, 785, 1332, 990, 983, 786,
  1738, 1152, 1428, 744, 359, 1333, 1198, 1451, 943, 1412, 1051, 1168, 1040, 524, 1149, 1327, 962, 1448, 858, 983
};