bex 0.1.5

A rust library for working with boolean expressions (syntax trees, decision diagrams, algebraic normal form, etc.)
Documentation 
// note: i temporarily replaced '//!' with '///'
// until i get benchmarks cleanly factored out.
/// example for bdd-based general solver with bex:
///
/// ```text
///     NB. k =: 614889782588491410
///     k =: */2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
/// ```
///
/// That is, k is the product of the first 15 primes. This is the value with the
/// largest number of unique prime factors that still fits into a u64.
///
/// Now, we want to find all pairs (x,y) of 32 bit numbers such that x>y and x*y=k.
/// (The first condition strips out duplicates, but also just makes our BDD
/// a little more interesting.)
///
/// There are 2^15=32,768 ways to group the factors into two products that multiply to k.
/// But since we only care about one ordering, this brings us down to 2^14 = 16,384.
/// However, many of these (for example, 307,444,891,294,245,705 * 2) involve an x
/// that's too big to fit in a u32. Once we eliminate these numbers, we wind up with
/// 3827 possible solutions.
///
/// The list was generated with the following J program:
///
/// ```text
///     xy0 =: */L:0 (0,"1#:i.2^n-1) </."1 |.p:i.n=:15
///     xys =: ({~[:I.([:*./(2^32)>])"1) \:~\:~@;"1 xy0
///     txt =: ,('    ',LF,~}:)"1 ] _4 ;\ ([: < ','10}  3|.'), (', ": )"1 xys
///     txt 1!:2 <'nums.txt'
/// ```


/// Product of the first 15 primes: 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
#[cfg(not(test))]
const K:u64 = 614_889_782_588_491_410;

/// All 3,827 ordered pairs of 32-bit ints that multiply to produce K.
#[cfg(not(test))]
#[allow(clippy::unreadable_literal)]
fn factors()->Vec<(u64,u64)> {
  vec![
    (429400657, 143197215), (429319798, 143224185), (429192489, 143266669),
    (429092163, 143300166), (428929966, 143354354), (428759840, 143411235),
    (428350132, 143548405), (427995090, 143667485), (427896131, 143700711),
    (427891905, 143702130), (427713143, 143762190), (427662391, 143779251),
    (427545970, 143818402), (427435437, 143855593), (426797553, 144070597),
    (426655128, 144118690), (426531359, 144160510), (426328023, 144229267),
    (426239813, 144259115), (426222854, 144264855), (426079933, 144313246),
    (425565809, 144487590), (425100439, 144645765), (424961733, 144692977),
    (424871196, 144723810), (424832565, 144736970), (424808137, 144745293),
    (424765183, 144759930), (424752566, 144764230), (424604622, 144814670),
    (424302378, 144917826), (423948201, 145038894), (423417603, 145220647),
    (423238297, 145282170), (423045486, 145348385), (423013691, 145359310),
    (422631649, 145490709), (422600194, 145501538), (422138067, 145660823),
    (421954460, 145724205), (421628699, 145836795), (421510316, 145877754),
    (421470549, 145891518), (421182463, 145991307), (421139876, 146006070),
    (420837796, 146110874), (420612792, 146189035), (420288901, 146301694),
    (420261695, 146311165), (419962543, 146415387), (419803797, 146470753),
    (419699049, 146507309), (419647728, 146525226), (419138301, 146703315),
    (419014011, 146746831), (418508413, 146924115), (418489480, 146930762),
    (418368079, 146973398), (418351433, 146979246), (418100640, 147067410),
    (418065479, 147079779), (417804731, 147171570), (417577360, 147251705),
    (417181219, 147391530), (417073365, 147429645), (416959827, 147469790),
    (416910351, 147487291), (416736177, 147548933), (416732061, 147550390),
    (416726040, 147552522), (416701798, 147561106), (416635706, 147584514),
    (415864807, 147858095), (415727626, 147906885), (415570481, 147962815),
    (415473340, 147997410), (415154807, 148110963), (414936506, 148188885),
    (414843596, 148222074), (414679383, 148280770), (414088941, 148492201),
    (414013399, 148519295), (413947734, 148542855), (413778529, 148603598),
    (413642036, 148652634), (413559251, 148682391), (413336231, 148762614),
    (413320303, 148768347), (412721809, 148984078), (412636415, 149014910),
    (412597485, 149028970), (412500364, 149064058), (412179453, 149180115),
    (412167186, 149184555), (412117088, 149202690), (412044963, 149228807),
    (411063081, 149585261), (411029170, 149597602), (410943533, 149628777),
    (410857453, 149660126), (410796341, 149682390), (410738266, 149703554),
    (410533207, 149778330), (410498683, 149790927), (409913254, 150004855),
    (409882445, 150016130), (409706214, 150080658), (409585449, 150124909),
    (409544034, 150140090), (409428533, 150182445), (409287909, 150234045),
    (408985323, 150345195), (408794743, 150415286), (408377369, 150569015),
    (408088342, 150675655), (408066798, 150683610), (407782428, 150788690),
    (407771117, 150792873), (407758981, 150797361), (407635042, 150843210),
    (407554719, 150872939), (406849088, 151134610), (406810704, 151148870),
    (406633481, 151214745), (406532638, 151252255), (406414705, 151296145),
    (406398535, 151302165), (406017137, 151444293), (405769435, 151536742),
    (405515671, 151631571), (405196071, 151751171), (405072911, 151797310),
    (405049619, 151806039), (404974731, 151834111), (404836632, 151885905),
    (404806502, 151897210), (404634416, 151961810), (404229680, 152113962),
    (404192926, 152127794), (403723761, 152304581), (403421119, 152418838),
    (403183781, 152508561), (403046279, 152560590), (402944371, 152599174),
    (402231221, 152869730), (402055994, 152936355), (402018062, 152950785),
    (402015471, 152951771), (401933852, 152982830), (401905185, 152993742),
    (401804903, 153031926), (401530259, 153136599), (401320681, 153216570),
    (401201674, 153262018), (401097915, 153301665), (400989061, 153343281),
    (400797242, 153416670), (400740580, 153438362), (400714639, 153448295),
    (400489961, 153534381), (400178163, 153654007), (400129229, 153672798),
    (399174581, 154040315), (399042905, 154091145), (398654098, 154241430),
    (398584329, 154268429), (398524021, 154291774), (398312827, 154373583),
    (398155157, 154434715), (397674604, 154621335), (397544847, 154671803),
    (397424012, 154718830), (397376497, 154737330), (397349175, 154747970),
    (397290201, 154770941), (396988061, 154888734), (396830916, 154950070),
    (396522258, 155070685), (395932600, 155301630), (395530333, 155459577),
    (395500605, 155471262), (395365091, 155524551), (395332475, 155537382),
    (394903353, 155706397), (394695701, 155788315), (394607323, 155823206),
    (394533016, 155852554), (394426848, 155894505), (394075456, 156033514),
    (393673110, 156192985), (393444023, 156283930), (393385629, 156307129),
    (393255863, 156358707), (393173488, 156391466), (393158337, 156397493),
    (392880081, 156508261), (392781943, 156547365), (392573681, 156630414),
    (392269641, 156751815), (392061469, 156835045), (391894801, 156901745),
    (391689535, 156983970), (391512364, 157055010), (391479439, 157068219),
    (391475573, 157069770), (391438639, 157084590), (390818145, 157333990),
    (390474357, 157472513), (390324763, 157532865), (390230817, 157570790),
    (390044787, 157645943), (389927293, 157693445), (389840489, 157728558),
    (389817811, 157737734), (389720545, 157777102), (389034820, 158055205),
    (388921678, 158101185), (388862833, 158125110), (388710844, 158186938),
    (388614955, 158225970), (388079493, 158444286), (387925874, 158507030),
    (387868299, 158530559), (387830910, 158545842), (387755781, 158576561),
    (387708366, 158595954), (387083140, 158852122), (387041615, 158869165),
    (386878009, 158936349), (386654477, 159028233), (386211423, 159210667),
    (386150167, 159235923), (386138697, 159240653), (385978292, 159306830),
    (385600715, 159462822), (385393255, 159548662), (385298184, 159588030),
    (384557901, 159895241), (384511159, 159914678), (384458467, 159936595),
    (384431047, 159948003), (384299941, 160002570), (384047194, 160107870),
    (384019304, 160119498), (383627225, 160283145), (383466956, 160350135),
    (383355715, 160396665), (383317077, 160412833), (383179781, 160470310),
    (382907024, 160584618), (382854433, 160606677), (382762285, 160645342),
    (382726672, 160660290), (382541131, 160738214), (382407425, 160794415),
    (382155510, 160900410), (381744062, 161073830), (381633321, 161120570),
    (381541760, 161159235), (381473885, 161187910), (381428619, 161207039),
    (381259994, 161278338), (381177348, 161313306), (380680006, 161524055),
    (380351471, 161663574), (380272774, 161697030), (380207698, 161724706),
    (380091491, 161774151), (380053059, 161790510), (379988020, 161818202),
    (379909398, 161851690), (379822483, 161888727), (379727711, 161929131),
    (379577398, 161993255), (379054389, 162216769), (378939174, 162266090),
    (378882933, 162290177), (378847329, 162305429), (378811587, 162320743),
    (378718139, 162360795), (378633339, 162397158), (378523500, 162444282),
    (378144107, 162607263), (378115963, 162619366), (377551681, 162862414),
    (377482805, 162892130), (377393950, 162930482), (377246731, 162994065),
    (377105228, 163055226), (377043294, 163082010), (376337761, 163387745),
    (376280820, 163412470), (376253494, 163424338), (376081413, 163499115),
    (376078989, 163500169), (376047964, 163513658), (375799493, 163621770),
    (375088623, 163931867), (375027019, 163958795), (374939355, 163997130),
    (374886349, 164020318), (374651899, 164122959), (374583552, 164152905),
    (374454896, 164209305), (374371050, 164246082), (374314440, 164270922),
    (374024541, 164398245), (373826052, 164485535), (373621848, 164575435),
    (373421382, 164663785), (373337708, 164700690), (373302486, 164716230),
    (373267407, 164731710), (373212007, 164756163), (372869211, 164907631),
    (372582728, 165034430), (372344072, 165140210), (372312759, 165154099),
    (372188516, 165209230), (372080547, 165257170), (371966823, 165307695),
    (371955753, 165312615), (371903169, 165335989), (371826220, 165370205),
    (371739304, 165408870), (371594008, 165473546), (370940177, 165765215),
    (370851481, 165804861), (370776189, 165838530), (370711299, 165867559),
    (370666240, 165887722), (370662111, 165889570), (370577311, 165927531),
    (370539841, 165944310), (369827913, 166263757), (369827154, 166264098),
    (369734876, 166305594), (369484286, 166418385), (369344621, 166481315),
    (369148786, 166569634), (369079273, 166601006), (368912329, 166676398),
    (368651233, 166794446), (368300168, 166953435), (368274845, 166964915),
    (368248101, 166977041), (368005911, 167086931), (367998777, 167090170),
    (367803759, 167178765), (367793283, 167183527), (367608741, 167267454),
    (367322813, 167397657), (366961922, 167562285), (366764490, 167652485),
    (366611266, 167722555), (366405709, 167816649), (366253501, 167886390),
    (366184534, 167918010), (366120447, 167947403), (365664747, 168156703),
    (365553602, 168207830), (365357465, 168298130), (364836983, 168538227),
    (364770694, 168568855), (364726090, 168589470), (364655436, 168622135),
    (363988524, 168931090), (363829957, 169004715), (363739175, 169046895),
    (363687753, 169070797), (363676929, 169075829), (363632725, 169096382),
    (363526971, 169145574), (362796788, 169486005), (362775683, 169495865),
    (362694923, 169533606), (362585668, 169584690), (362467360, 169640042),
    (362412817, 169665573), (362065957, 169828113), (361868177, 169920933),
    (361294557, 170190713), (361260471, 170206771), (361226523, 170222767),
    (361157954, 170255085), (361136391, 170265251), (360955738, 170350466),
    (360529174, 170552018), (360058939, 170774758), (359700371, 170944995),
    (359698053, 170946097), (359625026, 170980810), (359509650, 171035682),
    (359506396, 171037230), (359453039, 171062619), (359243865, 171162222),
    (358877082, 171337155), (358608058, 171465690), (358586943, 171475787),
    (358557361, 171489934), (358354255, 171587130), (358124713, 171697110),
    (357735978, 171883685), (357583902, 171956785), (357557027, 171969710),
    (357500315, 171996990), (357467810, 172012630), (357193749, 172144609),
    (357105634, 172187085), (357038389, 172219515), (356958443, 172258086),
    (356662575, 172400982), (356385161, 172535181), (356244088, 172603505),
    (356120005, 172663645), (355973164, 172734870), (355920331, 172760511),
    (355853309, 172793049), (355629070, 172902002), (355199844, 173110938),
    (355059240, 173179490), (354755289, 173327869), (354655485, 173376645),
    (354550317, 173428073), (354106483, 173645446), (353747713, 173821557),
    (353475922, 173955210), (353286323, 174048567), (353129076, 174126070),
    (352908232, 174235035), (352689546, 174343070), (352593829, 174390398),
    (352537905, 174418062), (352111150, 174629455), (351979075, 174694982),
    (351885606, 174741385), (351860509, 174753849), (351786805, 174790462),
    (351753616, 174806954), (351554364, 174906030), (351169928, 175097505),
    (350978100, 175193205), (350889357, 175237513), (350882555, 175240910),
    (350626321, 175368974), (350510660, 175426842), (350300536, 175532070),
    (350271077, 175546833), (350218079, 175573398), (349893926, 175736055),
    (349862112, 175752035), (349631636, 175867890), (349512163, 175928007),
    (349363583, 176002827), (349218455, 176075970), (349153889, 176108530),
    (349133813, 176118657), (348321873, 176529190), (347981133, 176702046),
    (347933339, 176726319), (347793913, 176797166), (347708117, 176840790),
    (347648614, 176871058), (347040057, 177181213), (346939383, 177232627),
    (346925579, 177239679), (346823607, 177291790), (346821074, 177293085),
    (346794441, 177306701), (346748426, 177330230), (346572303, 177420347),
    (346554006, 177429714), (346308734, 177555378), (345955157, 177736845),
    (345793948, 177819706), (345608413, 177915166), (345502781, 177969561),
    (345419623, 178012406), (345387485, 178028970), (345287290, 178080630),
    (345037099, 178209759), (345011166, 178223154), (344538867, 178467465),
    (344490159, 178492699), (344404203, 178537247), (344318174, 178581855),
    (344256920, 178613630), (344231920, 178626602), (344074484, 178708335),
    (343989155, 178752665), (343624567, 178942323), (343540493, 178986115),
    (343166187, 179181343), (343114264, 179208458), (342967911, 179284931),
    (342845067, 179349170), (342766631, 179390211), (342734293, 179407137),
    (342663379, 179444265), (342154012, 179711405), (342073473, 179753717),
    (342011069, 179786515), (341969499, 179808370), (341928614, 179829870),
    (341635903, 179983947), (341594378, 180005826), (341532062, 180038670),
    (340873560, 180386470), (340841400, 180403490), (340655214, 180502090),
    (340608426, 180526885), (340496070, 180586455), (340314474, 180682818),
    (340185835, 180751142), (340073618, 180810786), (339968986, 180866434),
    (339756373, 180979617), (339621882, 181051285), (339545836, 181091834),
    (339390543, 181174695), (339370800, 181185235), (339365897, 181187853),
    (339220769, 181265370), (339136128, 181310610), (339088183, 181336246),
    (339000519, 181383139), (338777198, 181502706), (338678921, 181555374),
    (338494611, 181654231), (338353197, 181730153), (338255043, 181782887),
    (338038815, 181899165), (337857441, 181996815), (337700005, 182081662),
    (337668271, 182098774), (337355218, 182267755), (336882731, 182523390),
    (336854401, 182538741), (336755390, 182592410), (336493896, 182734305),
    (336491727, 182735483), (336241651, 182871390), (336055010, 182972955),
    (335780006, 183122810), (335733887, 183147965), (335550491, 183248065),
    (335518834, 183265355), (335472055, 183290910), (335424628, 183316826),
    (335340934, 183362578), (335019892, 183538290), (334653537, 183739215),
    (334544343, 183799187), (334405371, 183875570), (334263213, 183953770),
    (334148991, 184016651), (334007488, 184094610), (333928866, 184137954),
    (333898504, 184154698), (333589456, 184325305), (333310999, 184479295),
    (333010778, 184645610), (332957729, 184675029), (332914173, 184699190),
    (332895031, 184709811), (332864763, 184726607), (332685259, 184826278),
    (332645484, 184848378), (332321457, 185028613), (331920465, 185252145),
    (331795964, 185321658), (331727314, 185360010), (331569173, 185448417),
    (331535647, 185467170), (331486441, 185494701), (331251833, 185626077),
    (330898659, 185824199), (330692277, 185940170), (330514899, 186039959),
    (330435215, 186084822), (330401379, 186103879), (329845840, 186417322),
    (329513338, 186605430), (329415625, 186660782), (329353594, 186695938),
    (329322951, 186713310), (329183309, 186792515), (329087574, 186846855),
    (328913084, 186945978), (328513803, 187173195), (328334351, 187275495),
    (328303375, 187293165), (328244970, 187326490), (328206021, 187348721),
    (328196253, 187354297), (328060925, 187431582), (328005268, 187463386),
    (327700501, 187637730), (327561865, 187717145), (327290363, 187872865),
    (327211457, 187918170), (327155461, 187950334), (327074757, 187996710),
    (326898785, 188097910), (326823997, 188140953), (326794281, 188158061),
    (326742449, 188187909), (326717891, 188202054), (326579001, 188282094),
    (326015547, 188607503), (325948092, 188646535), (325803995, 188729970),
    (325567921, 188866821), (325395147, 188967103), (325355596, 188990074),
    (325018976, 189185810), (324970737, 189213893), (324939411, 189232134),
    (324810786, 189307070), (324607652, 189425535), (324472040, 189504705),
    (324312901, 189597694), (324195683, 189666246), (323953751, 189807891),
    (323484661, 190083134), (323392864, 190137090), (323362354, 190155030),
    (323233053, 190231097), (323141327, 190285095), (322673414, 190561030),
    (322534679, 190642998), (322316079, 190772295), (322157998, 190865906),
    (322113851, 190892065), (322023409, 190945678), (321817138, 191068066),
    (321769270, 191096490), (321615877, 191187633), (321376590, 191329985),
    (321283125, 191385645), (321244075, 191408910), (321026433, 191538677),
    (320840949, 191649409), (320382056, 191923914), (320079559, 192105295),
    (319943491, 192186995), (319868703, 192231930), (319839620, 192249410),
    (319766447, 192293403), (319594877, 192396633), (319497735, 192455130),
    (318984141, 192765001), (318851633, 192845110), (318677459, 192950510),
    (318672854, 192953298), (318633689, 192977015), (318455033, 193085277),
    (318368341, 193137854), (318194431, 193243414), (317808162, 193478285),
    (317639653, 193580926), (317471323, 193683567), (317412627, 193719383),
    (317382681, 193737661), (317304387, 193785465), (317256377, 193814790),
    (317233338, 193828866), (317211526, 193842194), (316909447, 194026965),
    (316656249, 194182109), (316482304, 194288835), (316418875, 194327782),
    (316314498, 194391906), (316194931, 194465414), (316098289, 194524869),
    (316068467, 194543223), (315901138, 194646270), (315294189, 195020969),
    (315262308, 195040690), (315186671, 195087495), (315148362, 195111210),
    (315093207, 195145363), (315033873, 195182117), (315029235, 195184990),
    (314548642, 195483210), (314138379, 195738510), (314093968, 195766186),
    (313988623, 195831867), (313897537, 195888693), (313872457, 195904345),
    (313637171, 196051310), (313614801, 196065294), (313565417, 196096173),
    (313062986, 196410885), (313034521, 196428745), (312984872, 196459905),
    (312960837, 196474993), (312931311, 196493531), (312866563, 196534195),
    (312828306, 196558230), (312522516, 196750554), (312458617, 196790790),
    (312356665, 196855022), (312067555, 197037395), (311890519, 197149238),
    (311833622, 197185210), (311638604, 197308605), (311594547, 197336503),
    (311521710, 197382642), (311389617, 197466373), (311351540, 197490522),
    (311184485, 197596542), (310881363, 197789207), (310787716, 197848805),
    (310650321, 197936310), (310648318, 197937586), (310506242, 198028155),
    (310483693, 198042537), (310100219, 198287439), (309855819, 198443839),
    (309855183, 198444246), (309686559, 198552299), (309567915, 198628395),
    (309232805, 198843645), (309228580, 198846362), (309116814, 198918258),
    (309088708, 198936346), (308644135, 199222895), (308554600, 199280705),
    (308351336, 199412070), (308305571, 199441671), (308211861, 199502310),
    (308151129, 199541629), (307856117, 199732845), (307787184, 199777578),
    (307665348, 199856690), (307588581, 199906570), (307454583, 199993695),
    (307378336, 200043305), (307276941, 200109315), (307160790, 200184985),
    (306996973, 200291806), (306964039, 200313295), (306895704, 200357898),
    (306892285, 200360130), (306803258, 200418270), (306801280, 200419562),
    (306656999, 200513859), (306428842, 200663155), (306257029, 200775729),
    (305710779, 201134479), (305674229, 201158529), (305637075, 201182982),
    (305581318, 201219690), (305509388, 201267066), (305254551, 201435091),
    (304963358, 201627430), (304893589, 201673569), (304784382, 201745830),
    (304753663, 201766166), (304665256, 201824714), (304563539, 201892119),
    (304004883, 202263127), (303975578, 202282626), (303901205, 202332130),
    (303879530, 202346562), (303855251, 202362730), (303665223, 202489365),
    (303643171, 202504071), (303437588, 202641270), (303394690, 202669922),
    (302979361, 202947745), (302737071, 203110171), (302649249, 203169109),
    (302548253, 203236930), (302500267, 203269170), (302313069, 203395038),
    (302293500, 203408205), (302152636, 203503034), (301701718, 203807186),
    (301421391, 203996730), (301396043, 204013887), (301332312, 204057035),
    (301307454, 204073870), (301295465, 204081990), (301208062, 204141210),
    (301163357, 204171513), (301044143, 204252365), (300680798, 204499185),
    (300629343, 204534187), (300555182, 204584655), (300437709, 204664649),
    (300434742, 204666670), (300362662, 204715785), (299684260, 205179205),
    (299527291, 205286730), (299384501, 205384641), (299363673, 205398930),
    (299312443, 205434086), (299204805, 205507990), (299077611, 205595390),
    (298934581, 205693761), (298474776, 206010635), (298429616, 206041810),
    (298404519, 206059139), (298269543, 206152387), (298113315, 206260422),
    (297986585, 206348142), (297909547, 206401503), (297828448, 206457706),
    (297665758, 206570546), (297365695, 206778990), (297143785, 206933415),
    (297081543, 206976770), (296981469, 207046515), (296906379, 207098879),
    (296870073, 207124206), (296766671, 207196374), (296683810, 207254242),
    (296463676, 207408135), (296383219, 207464439), (296199559, 207593078),
    (296161786, 207619555), (296064091, 207688065), (296004754, 207729698),
    (295842154, 207843870), (295723857, 207927013), (295676953, 207959997),
    (295496646, 208086890), (295282533, 208237777), (294849884, 208543335),
    (294827724, 208559010), (294740296, 208620874), (294712489, 208640558),
    (294405133, 208858377), (294288594, 208941085), (293965777, 209170533),
    (293876425, 209234130), (293649279, 209395979), (293425958, 209555346),
    (293402514, 209572090), (293309807, 209638330), (293238005, 209689662),
    (293154370, 209749485), (293081669, 209801515), (292838746, 209975555),
    (292773175, 210022582), (292718044, 210062138), (292645835, 210113970),
    (292531453, 210196126), (292517519, 210206139), (292348507, 210327663),
    (291837245, 210696130), (291715323, 210784190), (291698121, 210796621),
    (291551760, 210902442), (291532887, 210916095), (291491673, 210945917),
    (291273163, 211104166), (290763291, 211474351), (290760659, 211476265),
    (290688109, 211529045), (290667377, 211544133), (290608364, 211587090),
    (290606491, 211588454), (290579074, 211608418), (290518952, 211652210),
    (290452487, 211700643), (290371389, 211759769), (289938430, 212075985),
    (289865121, 212129621), (289766265, 212201990), (289706781, 212245561),
    (289595792, 212326905), (289378703, 212486190), (289324212, 212526210),
    (289169023, 212640267), (289147501, 212656094), (288482794, 213146085),
    (288431474, 213184010), (288414889, 213196269), (288327224, 213261090),
    (288207130, 213349955), (287744156, 213693230), (287547475, 213839395),
    (287474113, 213893966), (287308015, 214017622), (287182853, 214110897),
    (287159908, 214128005), (287155759, 214131099), (286657629, 214503198),
    (286602099, 214544759), (286514985, 214609990), (286498511, 214622331),
    (286418517, 214682273), (286347861, 214735245), (286298859, 214771999),
    (286283744, 214783338), (285953311, 215031531), (285866395, 215096910),
    (285439781, 215418390), (285346645, 215488702), (285288303, 215532770),
    (285128343, 215653686), (285124701, 215656441), (285030647, 215727603),
    (285009224, 215743818), (284436752, 216178035), (284396541, 216208601),
    (284354239, 216240765), (284337697, 216253345), (284294676, 216286070),
    (284211995, 216348990), (284053289, 216469869), (283860969, 216616530),
    (283840355, 216632262), (283820839, 216647158), (283534733, 216865770),
    (283485111, 216903731), (283450654, 216930098), (283221710, 217105455),
    (283168377, 217146345), (283069748, 217222005), (283018235, 217261542),
    (282911254, 217343698), (282809000, 217422282), (282648966, 217545385),
    (282440004, 217706335), (282342996, 217781135), (282237091, 217862854),
    (282009127, 218038965), (281974850, 218065470), (281925501, 218103641),
    (281868263, 218147930), (281733463, 218252307), (281621940, 218338735),
    (281410829, 218502530), (281195079, 218670179), (281129348, 218721306),
    (281071181, 218766570), (281031445, 218797502), (281023081, 218804014),
    (280692342, 219061830), (280558531, 219166311), (280466963, 219237865),
    (280349791, 219329495), (280342972, 219334830), (280192601, 219452541),
    (280043907, 219569063), (279991173, 219610417), (279778239, 219777558),
    (279625983, 219897227), (279625409, 219897678), (279599028, 219918426),
    (279260567, 220184965), (279218339, 220218265), (279155818, 220267586),
    (279059938, 220343266), (279009030, 220383470), (278992987, 220396143),
    (278912053, 220460097), (278818978, 220533690), (278736298, 220599106),
    (277991213, 221190366), (277973218, 221204685), (277821374, 221325585),
    (277801199, 221341659), (277759166, 221375154), (277542919, 221547638),
    (277239417, 221790173), (277193884, 221826605), (277167732, 221847535),
    (277089910, 221909842), (276871233, 222085110), (276755563, 222177930),
    (276452922, 222421155), (276432347, 222437710), (276232047, 222599003),
    (276024976, 222765994), (275919229, 222851370), (275852353, 222905397),
    (275802232, 222945905), (275768507, 222973170), (275698780, 223029562),
    (275620544, 223092870), (275210835, 223424990), (275147873, 223476117),
    (275090943, 223522365), (275064990, 223543455), (275043867, 223560623),
    (275016056, 223583230), (275007372, 223590290), (275000243, 223596087),
    (274975239, 223616419), (274916656, 223664070), (274319424, 224151018),
    (274173174, 224270585), (274103224, 224327818), (274035607, 224383170),
    (274019447, 224396403), (273904969, 224490189), (273825511, 224555331),
    (273254963, 225024195), (273148161, 225112181), (273122493, 225133337),
    (273031350, 225208490), (273029356, 225210135), (272968221, 225260574),
    (272741969, 225447438), (272674330, 225503362), (272595229, 225568798),
    (272529829, 225622929), (272481346, 225663074), (272074708, 226000346),
    (272004369, 226058789), (271934038, 226117255), (271911605, 226135910),
    (271854952, 226183035), (271821909, 226210530), (271637751, 226363891),
    (271623410, 226375842), (271299651, 226645991), (271232725, 226701915),
    (271207136, 226723305), (271126713, 226790557), (271071668, 226836610),
    (270709110, 227140410), (270658133, 227183190), (270512957, 227305113),
    (270347996, 227443810), (270305116, 227479890), (270048607, 227695965),
    (269871001, 227845815), (269756277, 227942715), (269630575, 228048982),
    (269613121, 228063745), (269461951, 228191691), (269355286, 228282055),
    (269261467, 228361595), (269210764, 228404605), (268947413, 228628257),
    (268927396, 228645274), (268812687, 228742843), (268772014, 228777458),
    (268629581, 228898761), (268428209, 229070478), (268321953, 229161190),
    (268154147, 229304595), (268138548, 229317935), (267998103, 229438110),
    (267955901, 229474245), (267939903, 229487947), (267813825, 229595982),
    (267805870, 229602802), (267739048, 229660106), (267467783, 229893027),
    (267160387, 230157543), (267018609, 230279749), (267000033, 230295770),
    (266872749, 230405609), (266732966, 230526354), (266729559, 230529299),
    (266619576, 230624394), (266271703, 230925695), (266130520, 231048202),
    (266064043, 231105930), (265960051, 231196294), (265875738, 231269610),
    (265848940, 231292922), (265809397, 231327330), (265771819, 231360038),
    (265682681, 231437661), (265528074, 231572418), (265306587, 231765743),
    (265218053, 231843110), (265195749, 231862609), (265105307, 231941710),
    (264949341, 232078245), (264899450, 232121955), (264840135, 232173942),
    (264700874, 232296090), (264553944, 232425105), (264413549, 232548515),
    (264301145, 232647415), (264043222, 232874670), (263255292, 233571670),
    (263071549, 233734809), (263053461, 233750881), (263050530, 233753485),
    (263022011, 233778831), (262974221, 233821315), (262942065, 233849910),
    (262856269, 233926238), (262716971, 234050271), (262296015, 234425895),
    (262256329, 234461370), (262210431, 234502411), (262185693, 234524537),
    (262175639, 234533530), (262115659, 234587199), (262042473, 234652717),
    (261585597, 235062553), (261560381, 235085214), (261243756, 235370135),
    (261008447, 235582330), (260862101, 235714494), (260722136, 235841034),
    (260545430, 236000985), (260468169, 236070989), (260332218, 236194270),
    (260153878, 236356185), (260142109, 236366878), (260089361, 236414815),
    (260056296, 236444874), (259991803, 236503526), (259878541, 236606601),
    (259813697, 236665653), (259404117, 237039330), (259353003, 237086047),
    (259285943, 237147365), (259264553, 237166930), (259140563, 237280407),
    (258989763, 237418566), (258617249, 237760545), (258593735, 237782165),
    (258216913, 238129166), (258117988, 238220430), (258055427, 238278183),
    (257976990, 238350630), (257773670, 238538630), (257455298, 238833610),
    (257318861, 238960245), (257234901, 239038241), (257213680, 239057962),
    (257203446, 239067474), (257128833, 239136846), (257125969, 239139510),
    (256928837, 239322993), (256737678, 239501185), (256597434, 239632085),
    (256483996, 239738070), (256419145, 239798702), (256340773, 239872017),
    (256162137, 240039293), (256148613, 240051966), (255967325, 240221982),
    (255828027, 240352783), (255803366, 240375954), (255525699, 240637159),
    (255453187, 240705465), (255397876, 240757594), (255357368, 240795786),
    (255334150, 240817682), (255310156, 240840314), (255286069, 240863038),
    (255174857, 240968013), (255027421, 241107321), (254884882, 241242155),
    (254581427, 241529710), (254496041, 241610745), (254460063, 241644907),
    (254422214, 241680855), (254368920, 241731490), (254315923, 241781865),
    (253688971, 242379390), (253644573, 242421817), (253613743, 242451286),
    (253606195, 242458502), (253578989, 242484515), (253471799, 242587059),
    (253446169, 242611590), (253325347, 242727303), (253307723, 242744190),
    (253272932, 242777535), (252906189, 243129590), (252882329, 243152530),
    (252709477, 243318845), (252626116, 243399135), (252482801, 243537294),
    (252436741, 243581730), (252235054, 243776498), (252077309, 243929049),
    (251977525, 244025645), (251921104, 244080298), (251788637, 244208710),
    (251701121, 244293621), (251655203, 244338195), (251617127, 244375170),
    (251595967, 244395723), (251110260, 244868442), (251010860, 244965410),
    (250870119, 245102838), (250853880, 245118705), (250839287, 245132965),
    (250835663, 245136507), (250775290, 245195522), (250698643, 245270487),
    (250630396, 245337274), (250465561, 245498734), (250191669, 245767489),
    (250035624, 245920870), (250014597, 245941553), (249981423, 245974190),
    (249924233, 246030477), (249901509, 246052849), (249854451, 246099191),
    (249736883, 246215046), (249469612, 246478830), (249395635, 246551942),
    (249144231, 246800730), (249092884, 246851605), (249000280, 246943410),
    (248906157, 247036790), (248831583, 247110827), (248801338, 247140866),
    (248728980, 247212762), (248388485, 247551645), (248229381, 247710315),
    (248210319, 247729339), (248185221, 247754390), (248135550, 247803985),
    (248125677, 247813845), (248053698, 247885755), (248003983, 247935446),
    (248001738, 247937690), (247992181, 247947245), (247731148, 248208506),
    (247729339, 248210319), (247623399, 248316510), (247361446, 248579474),
    (247300426, 248640810), (247110827, 248831583), (247108074, 248834355),
    (246801488, 249143466), (246566119, 249381295), (246299209, 249651545),
    (246099191, 249854451), (246052849, 249901509), (246030477, 249924233),
    (245978060, 249977490), (245941553, 250014597), (245897800, 250059082),
    (245823728, 250134430), (245767489, 250191669), (245332518, 250635255),
    (245270487, 250698643), (245250253, 250719326), (245240495, 250729302),
    (245189753, 250781190), (245136507, 250835663), (244662670, 251321455),
    (244655388, 251328935), (244554508, 251432610), (244395723, 251595967),
    (244293621, 251701121), (244234724, 251761818), (244032288, 251970666),
    (243929049, 252077309), (243702401, 252311745), (243610282, 252407155),
    (243571643, 252447195), (243553337, 252466170), (243481114, 252541058),
    (243458143, 252564886), (243435265, 252588622), (243325153, 252702926),
    (243309402, 252719285), (243029771, 253010065), (242727303, 253325347),
    (242659016, 253396635), (242587059, 253471799), (242537808, 253523270),
    (242421817, 253644573), (242300549, 253771518), (242240091, 253834854),
    (241910268, 254180935), (241851946, 254242230), (241810558, 254285746),
    (241644907, 254460063), (241571458, 254537430), (241525969, 254585370),
    (241143111, 254989570), (241107321, 255027421), (241082942, 255053210),
    (240968013, 255174857), (240918155, 255227665), (240637159, 255525699),
    (240619249, 255544718), (240593436, 255572135), (240537196, 255631890),
    (240352783, 255828027), (240293976, 255890635), (240172608, 256019946),
    (240077537, 256121330), (240039293, 256162137), (239936641, 256271730),
    (239914005, 256295910), (239872017, 256340773), (239842861, 256371934),
    (239750017, 256471215), (239622896, 256607274), (239322993, 256928837),
    (239299923, 256953606), (239038241, 257234901), (238987696, 257289305),
    (238860979, 257425798), (238816000, 257474282), (238371351, 257954565),
    (238311873, 258018945), (238278183, 258055427), (238192836, 258147890),
    (237864841, 258503854), (237829461, 258542310), (237795838, 258578866),
    (237556127, 258839790), (237318199, 259099295), (237300363, 259118770),
    (237280407, 259140563), (237219054, 259207585), (237199485, 259228970),
    (237086047, 259353003), (236948081, 259504014), (236706160, 259769235),
    (236665653, 259813697), (236606601, 259878541), (236468914, 260029858),
    (236249198, 260271690), (236208769, 260316238), (236150500, 260380470),
    (236070989, 260468169), (235953517, 260597845), (235798080, 260769630),
    (235544208, 261050690), (235540805, 261054462), (235419384, 261189105),
    (235366670, 261247602), (235285830, 261337362), (235126364, 261514605),
    (235062553, 261585597), (234887663, 261780365), (234762391, 261920054),
    (234684950, 262006482), (234652717, 262042473), (234596239, 262105558),
    (234587199, 262115659), (234524537, 262185693), (234502411, 262210431),
    (234460693, 262257086), (234050271, 262716971), (233921703, 262861365),
    (233904293, 262880930), (233778831, 263022011), (233750881, 263053461),
    (233734809, 263071549), (233722469, 263085438), (233624826, 263195394),
    (233559595, 263268902), (233070410, 263821470), (232935745, 263973990),
    (232847696, 264073810), (232769259, 264162795), (232717139, 264221958),
    (232698546, 264243070), (232681949, 264261918), (232625019, 264326590),
    (232214582, 264793785), (232156411, 264860134), (232126805, 264893915),
    (232098421, 264926310), (232040508, 264992430), (232007704, 265029898),
    (231992686, 265047055), (231876283, 265180110), (231862609, 265195749),
    (231765743, 265306587), (231690100, 265393205), (231437661, 265682681),
    (231402643, 265722886), (231360429, 265771370), (231215738, 265937685),
    (231165617, 265995345), (230994903, 266191926), (230973110, 266217042),
    (230658628, 266580005), (230529299, 266729559), (230481010, 266785442),
    (230411582, 266865830), (230405609, 266872749), (230335576, 266953890),
    (230279749, 267018609), (230157543, 267160387), (229893027, 267467783),
    (229835193, 267535086), (229744214, 267641030), (229712659, 267677795),
    (229504613, 267920445), (229487947, 267939903), (229427656, 268010314),
    (228898761, 268629581), (228776797, 268772790), (228755996, 268797230),
    (228742843, 268812687), (228719714, 268839870), (228706409, 268855510),
    (228628257, 268947413), (228563378, 269023755), (228477645, 269124702),
    (228456871, 269149174), (228210882, 269439290), (228191691, 269461951),
    (228054894, 269623585), (227979666, 269712555), (227893489, 269814545),
    (227836626, 269881885), (227808766, 269914890), (227751166, 269983154),
    (227626756, 270130714), (227305113, 270512957), (227249040, 270579705),
    (227227600, 270605235), (227180003, 270661930), (227114100, 270740470),
    (227103476, 270753135), (226886464, 271012105), (226790557, 271126713),
    (226767625, 271154130), (226645991, 271299651), (226611698, 271340706),
    (226363891, 271637751), (226309408, 271703146), (226263137, 271758710),
    (226058789, 272004369), (225622929, 272529829), (225187363, 273056966),
    (225133337, 273122493), (225131113, 273125190), (225112181, 273148161),
    (224791139, 273538265), (224677601, 273676494), (224622630, 273743470),
    (224588664, 273784870), (224555331, 273825511), (224503593, 273888615),
    (224490189, 273904969), (224462738, 273938466), (224396403, 274019447),
    (224384556, 274033914), (224377891, 274042054), (224342303, 274085526),
    (223927204, 274593605), (223853337, 274684215), (223843210, 274696642),
    (223616419, 274975239), (223596087, 275000243), (223560623, 275043867),
    (223476117, 275147873), (223448790, 275181522), (222936914, 275813355),
    (222918523, 275836110), (222905397, 275852353), (222842142, 275930655),
    (222738301, 276059294), (222599003, 276232047), (222510888, 276341435),
    (222346386, 276545885), (222229926, 276690810), (222007185, 276968415),
    (221942782, 277048785), (221896292, 277106830), (221893086, 277110834),
    (221840925, 277175990), (221790173, 277239417), (221341659, 277801199),
    (221323399, 277824118), (221268802, 277892670), (221247926, 277918890),
    (221230936, 277940234), (220565244, 278779090), (220461518, 278910255),
    (220460097, 278912053), (220396143, 278992987), (220393687, 278996095),
    (220344624, 279058218), (220250954, 279176898), (220120246, 279342674),
    (219897227, 279625983), (219843425, 279694415), (219792036, 279759810),
    (219760963, 279799366), (219728275, 279840990), (219706129, 279869198),
    (219610417, 279991173), (219569063, 280043907), (219495791, 280137390),
    (219452541, 280192601), (219208775, 280504182), (219166311, 280558531),
    (219145184, 280585578), (218902189, 280897045), (218829980, 280989735),
    (218670179, 281195079), (218595604, 281291010), (218491234, 281425378),
    (218252307, 281733463), (218116182, 281909290), (218103641, 281925501),
    (217932523, 282146865), (217830970, 282278402), (217703130, 282444162),
    (217616954, 282556010), (217447690, 282775955), (217338585, 282917910),
    (217239574, 283046855), (217213010, 283081470), (217120906, 283201555),
    (217070153, 283267770), (217039465, 283307822), (216903731, 283485111),
    (216741134, 283697778), (216679317, 283778715), (216540524, 283960605),
    (216469869, 284053289), (216343900, 284218682), (216208601, 284396541),
    (216142884, 284483010), (216105895, 284531702), (216071619, 284576838),
    (215783389, 284956958), (215727603, 285030647), (215705790, 285059470),
    (215671823, 285104365), (215656441, 285124701), (215546319, 285270370),
    (215494779, 285338598), (215115609, 285841545), (215031531, 285953311),
    (214900003, 286128326), (214771999, 286298859), (214700328, 286394430),
    (214682273, 286418517), (214659899, 286448370), (214622331, 286498511),
    (214596244, 286533338), (214544759, 286602099), (214379920, 286822470),
    (214175066, 287096810), (214131099, 287155759), (214110897, 287182853),
    (213997545, 287334970), (213948065, 287401422), (213831195, 287558502),
    (213831096, 287558635), (213717718, 287711186), (213552198, 287934185),
    (213511985, 287988415), (213398776, 288141194), (213226413, 288374115),
    (213196269, 288414889), (213164011, 288458534), (213119906, 288518230),
    (213111427, 288529710), (212640267, 289169023), (212567755, 289267665),
    (212550219, 289291530), (212480866, 289385954), (212451639, 289425765),
    (212404068, 289490586), (212248627, 289702595), (212245561, 289706781),
    (212129621, 289865121), (211971793, 290080945), (211759769, 290371389),
    (211708801, 290441294), (211700643, 290452487), (211544133, 290667377),
    (211522743, 290696770), (211474351, 290763291), (211315824, 290981418),
    (211116305, 291256415), (211069033, 291321646), (210977230, 291448410),
    (210945917, 291491673), (210814349, 291673590), (210796621, 291698121),
    (210591231, 291982614), (210327663, 292348507), (210306396, 292378070),
    (210206139, 292517519), (210174872, 292561035), (210162646, 292578055),
    (210130847, 292622330), (210019490, 292777485), (209981271, 292830774),
    (209901898, 292941506), (209849524, 293014618), (209707297, 293213345),
    (209618149, 293338045), (209569150, 293406630), (209507005, 293493662),
    (209480287, 293531095), (209395979, 293649279), (209254206, 293848230),
    (209170533, 293965777), (209091447, 294076965), (209032739, 294159558),
    (208858377, 294405133), (208788680, 294503410), (208760003, 294543865),
    (208536682, 294859290), (208455175, 294974582), (208368088, 295097866),
    (208237777, 295282533), (208155347, 295399465), (207959997, 295676953),
    (207932403, 295716190), (207927013, 295723857), (207889081, 295777815),
    (207863813, 295813770), (207785240, 295925630), (207577403, 296221926),
    (207468253, 296377770), (207464439, 296383219), (207301668, 296615935),
    (207098879, 296906379), (207044470, 296984402), (207022259, 297016265),
    (207006699, 297038590), (206973867, 297085710), (206779625, 297364782),
    (206660151, 297536694), (206401503, 297909547), (206174740, 298237205),
    (206152387, 298269543), (206089726, 298360230), (206083593, 298369110),
    (206059139, 298404519), (206022481, 298457614), (205693761, 298934581),
    (205659978, 298983685), (205640575, 299011895), (205531540, 299170522),
    (205471766, 299257554), (205384641, 299384501), (205249341, 299581854),
    (205110232, 299785035), (205059054, 299859855), (204981541, 299973245),
    (204956627, 300009710), (204792724, 300249818), (204714266, 300364890),
    (204664649, 300437709), (204643954, 300468090), (204534187, 300629343),
    (204492661, 300690390), (204188684, 301138030), (204171513, 301163357),
    (204044171, 301351310), (204013887, 301396043), (203885558, 301585746),
    (203879490, 301594722), (203853823, 301632695), (203777359, 301745878),
    (203619538, 301979755), (203316740, 302429490), (203308905, 302441145),
    (203266319, 302504510), (203207352, 302592290), (203199267, 302604330),
    (203169109, 302649249), (203110171, 302737071), (203008568, 302888586),
    (202757835, 303263142), (202600803, 303498195), (202598035, 303502342),
    (202570167, 303544095), (202524809, 303612078), (202504071, 303643171),
    (202487365, 303668222), (202418316, 303771810), (202263127, 304004883),
    (202112640, 304231235), (201892119, 304563539), (201861880, 304609162),
    (201698835, 304855395), (201673569, 304893589), (201591890, 305017122),
    (201435091, 305254551), (201158529, 305674229), (201134479, 305710779),
    (201027997, 305872710), (201009031, 305901570), (201007735, 305903542),
    (200871636, 306110805), (200775729, 306257029), (200765129, 306273198),
    (200548957, 306603330), (200513859, 306656999), (200494530, 306686562),
    (200357319, 306896590), (200289828, 307000005), (200244980, 307068762),
    (200089081, 307308014), (199774637, 307791715), (199737018, 307849685),
    (199587290, 308080630), (199541629, 308151129), (199521452, 308182290),
    (199469870, 308261985), (199441671, 308305571), (199385074, 308393085),
    (199292164, 308536858), (199156413, 308747166), (199077578, 308869430),
    (198953077, 309062715), (198941503, 309080695), (198891864, 309157835),
    (198837302, 309242670), (198772423, 309343606), (198751099, 309376795),
    (198645100, 309541882), (198552299, 309686559), (198443839, 309855819),
    (198287439, 310100219), (198261129, 310141370), (198054362, 310465155),
    (198042537, 310483693), (197789207, 310881363), (197765166, 310919154),
    (197682545, 311049102), (197466373, 311389617), (197451676, 311412794),
    (197347850, 311576630), (197336503, 311594547), (197213424, 311789010),
    (196997764, 312130335), (196836555, 312385970), (196692814, 312614258),
    (196627931, 312717414), (196579168, 312794986), (196493531, 312931311),
    (196474993, 312960837), (196440040, 313016522), (196390971, 313094730),
    (196134820, 313503630), (196096173, 313565417), (196094398, 313568255),
    (196045469, 313646515), (196030734, 313670090), (195947400, 313803490),
    (195888693, 313897537), (195831867, 313988623), (195739719, 314136438),
    (195601676, 314358135), (195539871, 314457495), (195340752, 314778035),
    (195237178, 314945026), (195182117, 315033873), (195162381, 315065730),
    (195145363, 315093207), (195022393, 315291886), (195020969, 315294189),
    (194963646, 315386890), (194558163, 316044195), (194543223, 316068467),
    (194524869, 316098289), (194517410, 316110410), (194476882, 316176285),
    (194460839, 316202370), (194372250, 316346485), (194182109, 316656249),
    (193934149, 317061118), (193877890, 317153122), (193737661, 317382681),
    (193719383, 317412627), (193683567, 317471323), (193679301, 317478315),
    (193520807, 317738330), (193439004, 317872698), (193327238, 318056466),
    (193177510, 318302985), (193105711, 318421334), (193085277, 318455033),
    (193075083, 318471846), (193069348, 318481306), (192969526, 318646055),
    (192765001, 318984141), (192396633, 319594877), (192293403, 319766447),
    (192287649, 319776015), (192278950, 319790482), (192229233, 319873190),
    (192215523, 319896006), (191859868, 320489005), (191829437, 320539845),
    (191813612, 320566290), (191756926, 320661055), (191733478, 320700270),
    (191677857, 320793330), (191658538, 320825666), (191649409, 320840949),
    (191538677, 321026433), (191427216, 321213354), (191203712, 321588830),
    (191187633, 321615877), (191073019, 321808795), (191009990, 321914985),
    (190770880, 322318470), (190714309, 322414078), (190482793, 322805945),
    (190340003, 323048110), (190231097, 323233053), (190192202, 323299155),
    (190045745, 323548302), (189911241, 323777454), (189863855, 323858262),
    (189807891, 323953751), (189788699, 323986510), (189658973, 324208115),
    (189641080, 324238705), (189529784, 324429105), (189527194, 324433538),
    (189441466, 324580354), (189423664, 324610858), (189405793, 324641486),
    (189359069, 324721590), (189213893, 324970737), (189072053, 325214526),
    (188967103, 325395147), (188866821, 325567921), (188623365, 325988130),
    (188607503, 326015547), (188393173, 326386445), (188338522, 326481155),
    (188187909, 326742449), (188168880, 326775490), (188158061, 326794281),
    (188140953, 326823997), (188139250, 326826955), (188040706, 326998230),
    (188039494, 327000338), (187912175, 327221895), (187607219, 327753795),
    (187544311, 327863734), (187513509, 327917590), (187354297, 328196253),
    (187348721, 328206021), (187325949, 328245918), (187291776, 328305810),
    (187227448, 328418610), (187012270, 328796490), (186913026, 328971070),
    (186810924, 329150870), (186710691, 329327570), (186606003, 329512326),
    (186434605, 329815262), (186290215, 330070895), (186156379, 330308198),
    (186103879, 330401379), (186060131, 330479065), (186039959, 330514899),
    (186006020, 330575205), (185983411, 330615390), (185977876, 330625230),
    (185951584, 330671978), (185913110, 330740410), (185824199, 330898659),
    (185626077, 331251833), (185494701, 331486441), (185470088, 331530430),
    (185448417, 331569173), (185425740, 331609722), (185355649, 331735118),
    (185288655, 331855062), (185028613, 332321457), (184983342, 332402785),
    (184913956, 332527514), (184742143, 332836770), (184726607, 332864763),
    (184709811, 332895031), (184675029, 332957729), (184672310, 332962630),
    (184288231, 333656565), (184150084, 333906870), (184137422, 333929830),
    (184124050, 333954082), (184016651, 334148991), (184002955, 334173862),
    (183994199, 334189765), (183901879, 334357530), (183896641, 334367054),
    (183799187, 334544343), (183754217, 334626215), (183661406, 334795314),
    (183480961, 335124570), (183473890, 335137485), (183404537, 335264215),
    (183382245, 335304970), (183344037, 335374845), (183338248, 335385435),
    (183305633, 335445110), (183202854, 335633298), (183060223, 335894806),
    (182936153, 336122615), (182832373, 336313406), (182738123, 336486865),
    (182735483, 336491727), (182538741, 336854401), (182418491, 337076454),
    (182385347, 337137710), (182327718, 337244270), (182185902, 337506785),
    (182020900, 337812735), (181914978, 338009430), (181869587, 338093790),
    (181843876, 338141594), (181838464, 338151658), (181782887, 338255043),
    (181730153, 338353197), (181654231, 338494611), (181398394, 338972010),
    (181387841, 338991730), (181383139, 339000519), (181274403, 339203865),
    (181206408, 339331146), (181187853, 339365897), (181032978, 339656226),
    (180979617, 339756373), (180934088, 339841866), (180837625, 340023145),
    (180714445, 340254915), (180698014, 340285855), (180647278, 340381426),
    (180630235, 340413542), (180613261, 340445534), (180578977, 340510170),
    (180568195, 340530502), (180231997, 341165715), (179983947, 341635903),
    (179850185, 341889990), (179849026, 341892194), (179753717, 342073473),
    (179726519, 342125238), (179630700, 342307735), (179438541, 342674310),
    (179407137, 342734293), (179390211, 342766631), (179360748, 342822935),
    (179293471, 342951574), (179284931, 342967911), (179181343, 343166187),
    (178942323, 343624567), (178881302, 343741785), (178867989, 343767370),
    (178791951, 343913570), (178745728, 344002505), (178596874, 344289218),
    (178552817, 344374170), (178537247, 344404203), (178519194, 344439030),
    (178492699, 344490159), (178209759, 345037099), (178192580, 345070362),
    (178122044, 345207010), (178060002, 345327290), (178000022, 345443655),
    (177969561, 345502781), (177960165, 345521022), (177926654, 345586098),
    (177829931, 345774065), (177420347, 346572303), (177406171, 346599995),
    (177377644, 346655738), (177327742, 346753290), (177306701, 346794441),
    (177275158, 346856146), (177239679, 346925579), (177232627, 346939383),
    (177181213, 347040057), (176873856, 347643114), (176812035, 347764665),
    (176736871, 347912565), (176726319, 347933339), (176643161, 348097134),
    (176643079, 348097295), (176454116, 348470070), (176379466, 348617555),
    (176118657, 349133813), (176055575, 349258910), (176002827, 349363583),
    (175942803, 349482770), (175930254, 349507698), (175928007, 349512163),
    (175584964, 350195010), (175546833, 350271077), (175510511, 350343565),
    (175503528, 350357505), (175489050, 350386410), (175444678, 350475026),
    (175409104, 350546105), (175237513, 350889357), (175135538, 351093666),
    (174946963, 351472110), (174931056, 351504070), (174783759, 351800295),
    (174756081, 351856014), (174753849, 351860509), (174681791, 352005654),
    (174566906, 352237314), (174400426, 352573555), (174271492, 352834405),
    (174048567, 353286323), (174005631, 353373495), (173966669, 353452638),
    (173821557, 353747713), (173554812, 354291405), (173520028, 354362426),
    (173501413, 354400445), (173469691, 354465254), (173462789, 354479358),
    (173428073, 354550317), (173410537, 354586170), (173397220, 354613402),
    (173327869, 354755289), (173286151, 354840694), (173048933, 355327115),
    (172977578, 355473690), (172843035, 355750395), (172793049, 355853309),
    (172760511, 355920331), (172751390, 355939122), (172535181, 356385161),
    (172518549, 356419518), (172309711, 356851495), (172293455, 356885165),
    (172269433, 356934930), (172245079, 356985398), (172202101, 357074494),
    (172159087, 357163710), (172144609, 357193749), (172037242, 357416670),
    (171994577, 357505330), (171899106, 357703885), (171849113, 357807945),
    (171812283, 357884646), (171770246, 357972230), (171636865, 358250415),
    (171583093, 358362686), (171571986, 358385885), (171483955, 358569862),
    (171475787, 358586943), (171383315, 358780422), (171367146, 358814274),
    (171331689, 358888530), (171077006, 359422810), (171062619, 359453039),
    (171036736, 359507434), (171018388, 359546005), (171005534, 359573030),
    (170946097, 359698053), (170817951, 359967894), (170431973, 360783115),
    (170304213, 361053770), (170265251, 361136391), (170248035, 361172910),
    (170222767, 361226523), (170206771, 361260471), (170190713, 361294557),
    (169920933, 361868177), (169878186, 361959234), (169828113, 362065957),
    (169810941, 362102570), (169720951, 362294565), (169695271, 362349390),
    (169685400, 362370470), (169682948, 362375706), (169665573, 362412817),
    (169579280, 362597235), (169500259, 362766278), (169247305, 363308462),
    (169176598, 363460306), (169127521, 363565774), (169075829, 363676929),
    (169070797, 363687753), (169040077, 363753845), (169019407, 363798330),
    (168928720, 363993630), (168677609, 364535510), (168604126, 364694385),
    (168588219, 364728795), (168538227, 364836983), (168427200, 365077482),
    (168335118, 365277185), (168246948, 365468610), (168245863, 365470966),
    (168156703, 365664747), (168115560, 365754235), (168027505, 365945910),
    (167947403, 366120447), (167866943, 366295930), (167859091, 366313065),
    (167816649, 366405709), (167775245, 366496130), (167759417, 366530710),
    (167397657, 367322813), (167395792, 367326905), (167347231, 367433495),
    (167340573, 367448115), (167326768, 367478430), (167272171, 367598374),
    (167183527, 367793283), (167086931, 368005911), (167074495, 368033302),
    (166977041, 368248101), (166794728, 368650610), (166690416, 368881305),
    (166680719, 368902765), (166655499, 368958590), (166654282, 368961285),
    (166478864, 369350058), (166447515, 369419622), (166432381, 369453214),
    (166263757, 369827913), (166160728, 370057226), (165960232, 370504290),
    (165937438, 370555185), (165927531, 370577311), (165867559, 370711299),
    (165804861, 370851481), (165784586, 370896834), (165743220, 370989402),
    (165625916, 371252154), (165511411, 371508995), (165456814, 371631585),
    (165449329, 371648398), (165335989, 371903169), (165334492, 371906535),
    (165257449, 372079918), (165200689, 372207758), (165154099, 372312759),
    (165088723, 372460195), (165000145, 372660145), (164907631, 372869211),
    (164756163, 373212007), (164591654, 373585030), (164543787, 373693710),
    (164411668, 373994005), (164342981, 374150315), (164295306, 374258885),
    (164256901, 374346390), (164167175, 374550990), (164151687, 374586330),
    (164122959, 374651899), (164103010, 374697442), (164098126, 374708594),
    (163931867, 375088623), (163882485, 375201645), (163780932, 375434290),
    (163645181, 375745730), (163517897, 376038215), (163500169, 376078989),
    (163411998, 376281906), (163397140, 376316122), (163371224, 376375818),
    (163007773, 377215006), (162974046, 377293070), (162783960, 377733642),
    (162697573, 377934206), (162607263, 378144107), (162485368, 378427786),
    (162320743, 378811587), (162307774, 378841855), (162305429, 378847329),
    (162303826, 378851070), (162290177, 378882933), (162236020, 379009410),
    (162216769, 379054389), (161976875, 379615782), (161929131, 379727711),
    (161888727, 379822483), (161774151, 380091491), (161691872, 380284905),
    (161677170, 380319485), (161616526, 380462194), (161570663, 380570190),
    (161368447, 381047095), (161207039, 381428619), (161177748, 381497935),
    (161158039, 381544590), (161056925, 381784130), (160807938, 382375266),
    (160762074, 382484355), (160721961, 382579815), (160688295, 382659970),
    (160641562, 382771290), (160606677, 382854433), (160513216, 383077354),
    (160480669, 383155045), (160420474, 383298818), (160412833, 383317077),
    (160296232, 383595905), (160051691, 384181995), (160039779, 384210590),
    (159971745, 384373990), (159948003, 384431047), (159895241, 384557901),
    (159883223, 384586806), (159797438, 384793266), (159492070, 385530002),
    (159409608, 385729435), (159316844, 385954030), (159240653, 386138697),
    (159235923, 386150167), (159227516, 386170554), (159210667, 386211423),
    (159028233, 386654477), (158936349, 386878009), (158904081, 386956570),
    (158795224, 387221835), (158735661, 387367134), (158706313, 387438766),
    (158691340, 387475322), (158652193, 387570930), (158576561, 387755781),
    (158530559, 387868299), (158454723, 388053930), (158328124, 388364218),
    (158241152, 388577670), (158200242, 388678155), (158132990, 388843455),
    (158049144, 389049738), (158034233, 389086446), (157842929, 389558015),
    (157813206, 389631385), (157647094, 390041938), (157645943, 390044787),
    (157630182, 390083785), (157593335, 390174990), (157546603, 390290726),
    (157516936, 390364234), (157472513, 390474357), (157269395, 390978665),
    (157068219, 391479439), (157029472, 391576035), (156994311, 391663734),
    (156948768, 391777386), (156936228, 391808690), (156782708, 392192346),
    (156531493, 392821770), (156517260, 392857490), (156508261, 392880081),
    (156492436, 392919810), (156480418, 392949986), (156465655, 392987062),
    (156433281, 393068390), (156397493, 393158337), (156358707, 393255863),
    (156307129, 393385629), (156033777, 394074790), (155936195, 394321395),
    (155927124, 394344335), (155888218, 394442755), (155819302, 394617210),
    (155797273, 394673006), (155706397, 394903353), (155694808, 394932746),
    (155524551, 395365091), (155484337, 395467345), (155459577, 395530333),
    (155440681, 395578414), (155393858, 395697610), (155253121, 396056310),
    (155241846, 396085074), (155231797, 396110715), (155132364, 396364605),
    (155083346, 396489885), (155050109, 396574878), (154927909, 396887678),
    (154843279, 397104598), (154833256, 397130305), (154783957, 397256790),
    (154770941, 397290201), (154671803, 397544847), (154616402, 397687290),
    (154373583, 398312827), (154322067, 398445790), (154277300, 398561410),
    (154268429, 398584329), (154240286, 398657055), (154157302, 398871655),
    (154152785, 398883342), (154075564, 399083258), (153928058, 399465690),
    (153804463, 399786695), (153727291, 399987390), (153689168, 400086610),
    (153654007, 400178163), (153638470, 400218630), (153607721, 400298745),
    (153580395, 400369970), (153534381, 400489961), (153482019, 400626590),
    (153343281, 400989061), (153328499, 401027718), (153214421, 401326310),
    (153162809, 401461545), (153136599, 401530259), (153128514, 401551458),
    (153104914, 401613355), (153016452, 401845535), (152951771, 402015471),
    (152855389, 402268958), (152837114, 402317058), (152627275, 402870182),
    (152508561, 403183781), (152503997, 403195845), (152470939, 403283265),
    (152446794, 403347138), (152304581, 403723761), (152281769, 403784238),
    (152140588, 404158935), (152083079, 404311765), (152002441, 404526254),
    (151995208, 404545505), (151834111, 404974731), (151832611, 404978730),
    (151821585, 405008142), (151806039, 405049619), (151751171, 405196071),
    (151631571, 405515671), (151489680, 405895490), (151453335, 405992895),
    (151444293, 406017137), (151409400, 406110705), (151368535, 406220342),
    (151324624, 406338218), (151246385, 406548415), (151146750, 406816410),
    (151020672, 407156035), (150957580, 407326205), (150872939, 407554719),
    (150842091, 407638065), (150797361, 407758981), (150792873, 407771117),
    (150698021, 408027774), (150666156, 408114070), (150581678, 408343026),
    (150522071, 408504730), (150501397, 408560845), (150419185, 408784145),
    (150340399, 408998370), (150314671, 409068374), (150277591, 409169310),
    (150218854, 409329298), (150181331, 409431570), (150124909, 409585449),
    (149954539, 410050795), (149842130, 410358410), (149790927, 410498683),
    (149748420, 410615205), (149725776, 410677305), (149692250, 410769282),
    (149628777, 410943533), (149585261, 411063081), (149467290, 411387522),
    (149237388, 412021270), (149228807, 412044963), (149202259, 412118278),
    (149134771, 412304774), (148954773, 412803006), (148768347, 413320303),
    (148682391, 413559251), (148637603, 413683865), (148571892, 413866830),
    (148492201, 414088941), (148490734, 414093030), (148453189, 414197758),
    (148266496, 414719305), (148231838, 414816270), (148191609, 414928878),
    (148110963, 415154807), (148080893, 415239110), (148032045, 415376130),
    (147930861, 415660245), (147893950, 415763985), (147861928, 415854026),
    (147838476, 415919994), (147659514, 416424085), (147641266, 416475554),
    (147631709, 416502515), (147564931, 416690995), (147548933, 416736177),
    (147487291, 416910351), (147460493, 416986115), (147424942, 417086670),
    (147202566, 417716754), (147144297, 417882170), (147079779, 418065479),
    (147043496, 418168635), (146982888, 418341066), (146824639, 418791958),
    (146746831, 419014011), (146577185, 419498970), (146540834, 419603030),
    (146507309, 419699049), (146470753, 419803797), (146419373, 419951110),
    (146415387, 419962543), (146258759, 420412278), (146174253, 420655326),
    (145991307, 421182463), (145849060, 421593242), (145766443, 421832190),
    (145745836, 421891834), (145660823, 422138067), (145490709, 422631649),
    (145453090, 422740955), (145410788, 422863935), (145381645, 422948702),
    (145380329, 422952530), (145344054, 423058090), (145333688, 423088266),
    (145226243, 423401286), (145220647, 423417603), (145185694, 423519538),
    (145077969, 423834015), (144986944, 424100105), (144969215, 424151970),
    (144932560, 424259242), (144853390, 424491122), (144797896, 424653810),
    (144745293, 424808137), (144692977, 424961733), (144584511, 425280534),
    (144382295, 425876165), (144241397, 426292170), (144229267, 426328023),
    (144211669, 426380045), (144207444, 426392538), (144103565, 426699910),
    (144070597, 426797553), (144023575, 426936895), (143855593, 427435437),
    (143803860, 427589205), (143779251, 427662391), (143773737, 427678790),
    (143700711, 427896131), (143697546, 427905555), (143591426, 428221794),
    (143579954, 428256010), (143577879, 428262198), (143422944, 428724835),
    (143301049, 429089518), (143266669, 429192489), (143249255, 429244662),
    (143209258, 429364546), (143173930, 429470490), (143149429, 429543998),
    (143064163, 429800007), (142976655, 430063062), (142783377, 430645215),
    (142669299, 430989559), (142665030, 431002455), (142562350, 431312882),
    (142515323, 431455206), (142478479, 431566779), (142288419, 432143239),
    (142265851, 432211791), (142251628, 432255005), (142218376, 432356070),
    (142198270, 432417202), (142177119, 432481530), (142168848, 432506690),
    (142109341, 432687801), (142079937, 432777345), (142026644, 432939738),
    (141848889, 433482269), (141742555, 433807462), (141653911, 434078931),
    (141642593, 434113615), (141610855, 434210910), (141584188, 434292690),
    (141534874, 434444010), (141324483, 435090770), (141222081, 435406261),
    (141220002, 435412670), (141171498, 435562270), (141139201, 435661941),
    (141037531, 435975995), (141015162, 436045155), (141004563, 436077930),
    (140962750, 436207282), (140866731, 436504614), (140810970, 436677470),
    (140791630, 436737455), (140714722, 436976155), (140712689, 436982469),
    (140701446, 437017385), (140597539, 437340358), (140292789, 438290369),
    (140279265, 438332622), (140252091, 438417551), (140250528, 438422435),
    (140233481, 438475730), (140204264, 438567105), (140174895, 438658990),
    (140096300, 438905082), (140087231, 438933495), (140021953, 439138126),
    (139995586, 439220834), (139934599, 439412259), (139899683, 439521927),
    (139812991, 439794454), (139671337, 440240493), (139630283, 440369930),
    (139609169, 440436530), (139588449, 440501909), (139529109, 440689249),
    (139496493, 440792286), (139456026, 440920194), (139192453, 441755115),
    (139117565, 441992915), (139059445, 442177645), (138986609, 442409370),
    (138970117, 442461873), (138912059, 442646799), (138910687, 442651170),
    (138900599, 442683318), (138621602, 443574285), (138619708, 443580346),
    (138596942, 443653210), (138583866, 443695070), (138555417, 443786173),
    (138523493, 443888445), (138317579, 444549265), (138243365, 444787915),
    (138226461, 444842310), (138167849, 445031015), (138116023, 445198006),
    (138029647, 445476603), (138004466, 445557885), (137926176, 445810794),
    (137901116, 445891810), (137692768, 446566505), (137590761, 446897581),
    (137573936, 446952234), (137545471, 447044730), (137532495, 447086910),
    (137521933, 447121246), (137500121, 447192174), (137487619, 447232838),
    (137348321, 447686421), (137245705, 448021145), (137086587, 448541170),
    (137042763, 448684607), (137021027, 448755783), (137016957, 448769113),
    (137009723, 448792806), (136969233, 448925477), (136952484, 448980378),
    (136912755, 449110662), (136838247, 449355203), (136637751, 450014565),
    (136627481, 450048390), (136574080, 450224362), (136561246, 450266674),
    (136528483, 450374727), (136514678, 450420270), (136264914, 451245858),
    (136125789, 451707045), (136074334, 451877855), (136029447, 452026965),
    (136002184, 452117578), (135987594, 452166085), (135967019, 452234510),
    (135927476, 452366070), (135851573, 452618817), (135818875, 452727782),
    (135818334, 452729585), (135670353, 453223397), (135649825, 453291982),
    (135635273, 453340615), (135616362, 453403830), (135603568, 453446610),
    (135563356, 453581114), (135510879, 453756765), (135471568, 453888435),
    (135256478, 454610226), (135080002, 455204155), (135067308, 455246935),
    (135065357, 455253513), (135024303, 455391930), (134991577, 455502333),
    (134935500, 455691630), (134878138, 455885430), (134806560, 456127490),
    (134730975, 456383382), (134677643, 456564110), (134630733, 456723190),
    (134605382, 456809210), (134574587, 456913743), (134562351, 456955291),
    (134473706, 457256514), (134406343, 457485686), (134314790, 457797522),
    (134169851, 458292065), (134136373, 458406445), (134077073, 458609190),
    (134069274, 458635870), (134005157, 458855313), (133977950, 458948490),
    (133969951, 458975894), (133767543, 459670387), (133733891, 459786054),
    (133580193, 460315086), (133571546, 460344885), (133559401, 460386745),
    (133509304, 460559498), (133436374, 460811218), (133392721, 460962021),
    (133364779, 461058598), (133135851, 461851390), (133108521, 461946221),
    (133095963, 461989807), (133074103, 462065695), (133058193, 462120945),
    (132861443, 462805287), (132841340, 462875322), (132718385, 463304145),
    (132653293, 463531486), (132597874, 463725218), (132514949, 464015409),
    (132474670, 464156490), (132449725, 464243910), (132430067, 464312823),
    (132276972, 464850210), (132206774, 465097030), (132174086, 465212055),
    (132150572, 465294830), (132130959, 465363899), (132110979, 465434279),
    (131938336, 466043305), (131766250, 466651955), (131741437, 466739845),
    (131634451, 467119191), (131597697, 467249653), (131565233, 467364945),
    (131542719, 467444939), (131535774, 467469618), (131526730, 467501762),
    (131525265, 467506970), (131511005, 467557662), (131487110, 467642630),
    (131358485, 468100542), (131224370, 468578955), (131202107, 468658465),
    (131148007, 468851790), (131128543, 468921387), (131105215, 469004822),
    (131092846, 469049074), (131057829, 469174398), (131052779, 469192479),
    (131021236, 469305434), (131003241, 469369901), (130960027, 469524783),
    (130862184, 469875835), (130792798, 470125106), (130687156, 470505135),
    (130668681, 470571661), (130631600, 470705235), (130623801, 470733341),
    (130621878, 470740270), (130527231, 471081611), (130272715, 472001970),
    (130234084, 472141978), (130158119, 472417539), (130142238, 472475185),
    (130076939, 472712370), (130044680, 472829630), (130014929, 472937829),
    (129975764, 473080335), (129939270, 473213202), (129906848, 473331306),
    (129752007, 473896163), (129725160, 473994235), (129678273, 474165615),
    (129676501, 474172094), (129642971, 474294730), (129570281, 474560814),
    (129393864, 475207835), (129308624, 475521090), (129296867, 475564330),
    (129289433, 475591677), (129251927, 475729683), (129027713, 476556366),
    (129013871, 476607495), (128863199, 477164765), (128809363, 477364195),
    (128737141, 477632001), (128726855, 477670165), (128712899, 477721959),
    (128659430, 477920490), (128617450, 478076482), (128476803, 478599847),
    (128464418, 478645986), (128368839, 479002370), (128303637, 479245793),
    (128298717, 479264170), (128185967, 479685723), (128170386, 479744034),
    (128152822, 479809785), (128081068, 480078586), (128009973, 480345217),
    (127914013, 480705566), (127772359, 481238499), (127762849, 481274318),
    (127726593, 481410930), (127587428, 481936026), (127513710, 482214642),
    (127469141, 482383245), (127442441, 482484310), (127347336, 482844635),
    (127277772, 483108535), (127248020, 483221490), (127230031, 483289814),
    (127211107, 483361710), (127157961, 483563730), (127142873, 483621117),
    (127055861, 483952315), (126917427, 484480183), (126893335, 484572165),
    (126885759, 484601099), (126884610, 484605485), (126822286, 484843634),
    (126789494, 484969030), (126735899, 485174118), (126662673, 485454606),
    (126636466, 485555070), (126567550, 485819455), (126525799, 485979765),
    (126477972, 486163535), (126354738, 486637690), (126351463, 486650307),
    (126313058, 486798270), (126294311, 486870531), (126282443, 486916287),
    (126270529, 486962229), (126038654, 487858098), (125988762, 488051290),
    (125985333, 488064577), (125880909, 488469449), (125850560, 488587242),
    (125827601, 488676390), (125797983, 488791446), (125637587, 489415465),
    (125445920, 490163235), (125426940, 490237410), (125419643, 490265930),
    (125417831, 490273014), (125364651, 490480991), (125359663, 490500507),
    (125349321, 490540974), (125095834, 491534978), (125029541, 491795601),
    (125009006, 491876385), (125007298, 491883106), (124962116, 492060954),
    (124950754, 492105698), (124942666, 492137555), (124927225, 492198382),
    (124756207, 492873095), (124608684, 493456605), (124571733, 493602977),
    (124546442, 493703210), (124540616, 493726305), (124473794, 493991355),
    (124415791, 494221654), (124289737, 494722893), (124259327, 494843965),
    (124194242, 495103290), (124114690, 495420630), (124105159, 495458678),
    (124104253, 495462297), (124067775, 495607970), (124062838, 495627690),
    (124026849, 495771510), (123996090, 495894490), (123967723, 496007967),
    (123942073, 496110615), (123864669, 496420638), (123691432, 497115905),
    (123646725, 497295645), (123635483, 497340865), (123606381, 497457961),
    (123570433, 497602677), (123555413, 497663166), (123554037, 497668710),
    (123283059, 498762590), (123275971, 498791271), (123149604, 499303090),
    (123114873, 499443945), (123107523, 499473767), (123049595, 499708902),
    (123026424, 499803018), (123015238, 499848466), (122970776, 500029194),
    (122883744, 500383338), (122798789, 500729515), (122758281, 500894745),
    (122749367, 500931123), (122720512, 501048905), (122668637, 501260793),
    (122666259, 501270510), (122635243, 501397286), (122597761, 501550581),
    (122568253, 501671326), (122551419, 501740239), (122434221, 502220521),
    (122331335, 502642910), (122327694, 502657870), (122254830, 502957455),
    (122203755, 503167665), (122197861, 503191934), (122146810, 503402242),
    (122040149, 503842209), (121964524, 504154618), (121901465, 504415415),
    (121888249, 504470109), (121866102, 504561785), (121851200, 504623490),
    (121805141, 504814310), (121785821, 504894390), (121768647, 504965603),
    (121654701, 505438570), (121590231, 505706565), (121551812, 505866405),
    (121514885, 506020130), (121363651, 506650694), (121357876, 506674805),
    (121329508, 506793270), (121293529, 506943598), (121229251, 507212391),
    (121225643, 507227487), (121210908, 507289146), (120955134, 508361870),
    (120925227, 508487595), (120861054, 508757585), (120822453, 508920126),
    (120680687, 509517965), (120553660, 510054842), (120484006, 510349714),
    (120459077, 510455330), (120431519, 510572139), (120420157, 510620313),
    (120408841, 510668301), (120397893, 510714737), (120378797, 510795753),
    (120318579, 511051398), (120296718, 511144270), (120187977, 511606733),
    (120176391, 511656054), (120146988, 511781270), (120110991, 511934651),
    (120025983, 512297227), (120019646, 512324274), (119936008, 512681546),
    (119899351, 512838291), (119875008, 512942430), (119724977, 513585215),
    (119661496, 513857674), (119568423, 514257667), (119533737, 514406893),
    (119528981, 514427361), (119519120, 514469802), (119493848, 514578610),
    (119245326, 515651055), (119194634, 515870355), (119185675, 515909130),
    (119155936, 516037890), (119139091, 516110854), (119131379, 516144265),
    (119066303, 516426365), (119064583, 516433827), (118748029, 517810515),
    (118709283, 517979527), (118706668, 517990935), (118673524, 518135605),
    (118659099, 518198590), (118640203, 518281126), (118609527, 518415170),
    (118543023, 518706006), (118479823, 518982695), (118401901, 519324245),
    (118353080, 519538470), (118332826, 519627394), (118303300, 519757082),
    (118251763, 519983607), (118222437, 520112593), (118183439, 520284219),
    (118035494, 520936338), (117976758, 521195690), (117920517, 521444273),
    (117896118, 521552185), (117884995, 521601395), (117857247, 521724203),
    (117709692, 522378210), (117563182, 523029210), (117542607, 523120763),
    (117531276, 523171194), (117443831, 523560730), (117370383, 523888365),
    (117326358, 524084946), (117295202, 524224155), (117293599, 524231318),
    (117262268, 524371386), (117251205, 524420862), (117109270, 525056455),
    (117087217, 525155345), (117025135, 525433942), (117012581, 525490315),
    (116963119, 525712539), (116960851, 525722730), (116889415, 526044022),
    (116875440, 526106922), (116867404, 526143098), (116620704, 527256105),
    (116509265, 527760415), (116384629, 528325590), (116242596, 528971135),
    (116231629, 529021045), (116107291, 529587570), (116086971, 529680271),
    (116063402, 529787830), (115996343, 530094110), (115931304, 530391498),
    (115882871, 530613174), (115845050, 530786410), (115786209, 531056149),
    (115718830, 531365362), (115680019, 531543639), (115659000, 531640235),
    (115646461, 531697881), (115607869, 531875370), (115598147, 531920103),
    (115582808, 531990690), (115524101, 532261041), (115329314, 533160010),
    (115312197, 533239153), (115264649, 533459118), (115263177, 533465933),
    (115202804, 533745498), (115139874, 534037218), (115078771, 534320774),
    (114989645, 534734915), (114946513, 534935566), (114923206, 535044055),
    (114856329, 535355590), (114830053, 535478097), (114801401, 535611741),
    (114797991, 535627651), (114752306, 535840890), (114743973, 535879806),
    (114663051, 536257995), (114535239, 536856419), (114513497, 536958345),
    (114449380, 537259162), (114388729, 537544029), (114371421, 537625374),
    (114322637, 537854793), (114314128, 537894826), (114281689, 538047510),
    (114138658, 538721755), (114095845, 538923902), (114051337, 539134215),
    (114027447, 539247170), (114024491, 539261151), (114003689, 539359545),
    (113989833, 539425110), (113946744, 539629090), (113918313, 539763770),
    (113652556, 541025914), (113624520, 541159410), (113613800, 541210470),
    (113551738, 541506270), (113536142, 541580655), (113528335, 541617895),
    (113443232, 542024210), (113395278, 542253426), (113380261, 542325245),
    (113322995, 542599302), (113207294, 543153855), (113187921, 543246821),
    (113181945, 543275502), (113164501, 543359245), (113123600, 543555705),
    (113029394, 544008738), (113000173, 544149417), (112894836, 544657135),
    (112831537, 544962693), (112811464, 545059658), (112784399, 545190459),
    (112751681, 545348661), (112723719, 545483939), (112630287, 545936443),
    (112566668, 546244986), (112556090, 546296322), (112451739, 546803265),
    (112412578, 546993755), (112409232, 547010035), (112395569, 547076530),
    (112277665, 547651022), (112251796, 547777230), (112245094, 547809938),
    (112198201, 548038894), (112163909, 548206449), (112075509, 548638849),
    (111963602, 549187210), (111926668, 549368430), (111911295, 549443895),
    (111850163, 549744195), (111839611, 549796065), (111808209, 549950478),
    (111798043, 550000486), (111780311, 550087734), (111738058, 550295746),
    (111662327, 550668965), (111623975, 550858165), (111514781, 551397561),
    (111494519, 551497765), (111468457, 551626710), (111452698, 551704706),
    (111421071, 551861310), (111382997, 552049953), (111299501, 552464094),
    (111255444, 552682870), (111196485, 552975915), (111173193, 553091770),
    (111103666, 553437885), (111017167, 553869095), (111003592, 553936830),
    (110971391, 554097570), (110954921, 554179821), (110895086, 554478834),
    (110835964, 554774605), (110773819, 555085839), (110687577, 555518333),
    (110670829, 555602398), (110595183, 555982427), (110409990, 556914985),
    (110299553, 557472597), (110279512, 557573905), (110230759, 557820510),
    (110230048, 557824106), (110198071, 557985974), (110196843, 557992190),
    (110171633, 558119877), (110133793, 558311637), (109959213, 559198057),
    (109948839, 559250819), (109948613, 559251966), (109921712, 559388830),
    (109888779, 559556479), (109805208, 559982346), (109784531, 560087814),
    (109727769, 560377545), (109726270, 560385202), (109641289, 560819545),
    (109583155, 561117062), (109451094, 561794090), (109414990, 561979470),
    (109402007, 562046163), (109398751, 562062891), (109360653, 562258697),
    (109335089, 562390158), (109187288, 563151435), (109126153, 563466926),
    (109096787, 563618595), (109069732, 563758405), (109051820, 563851002),
    (109038091, 563921995), (108992538, 564157685), (108966261, 564293730),
    (108931427, 564474183), (108829883, 565000865), (108723845, 565551910),
    (108711141, 565618001), (108671849, 565822509), (108649364, 565939605),
    (108630771, 566036471), (108619787, 566093710), (108560453, 566403110),
    (108465049, 566901309), (108451865, 566970222), (108339658, 567557430),
    (108323579, 567641679), (108316131, 567680711), (108270262, 567921210),
    (108234934, 568106578), (108104300, 568793082), (107871909, 570018449),
    (107863801, 570061294), (107852230, 570122455), (107835911, 570208730),
    (107828220, 570249402), (107826843, 570256687), (107744351, 570693291),
    (107570958, 571613185), (107557804, 571683090), (107515765, 571906622),
    (107508805, 571943645), (107391669, 572567489), (107385999, 572597718),
    (107371283, 572676195), (107341136, 572837034), (107311165, 572997022),
    (107272379, 573204198), (107251599, 573315259), (107125530, 573989955),
    (107122348, 574007005), (107095619, 574150265), (107065549, 574311518),
    (107055448, 574365706), (107008811, 574616031), (106946983, 574948227),
    (106915548, 575117270), (106776099, 575868370), (106755992, 575976830),
    (106693186, 576315885), (106647830, 576560985), (106613206, 576748230),
    (106598134, 576829778), (106452208, 577620505), (106384020, 577990735),
    (106339576, 578232305), (106328047, 578295003), (106320133, 578338046),
    (106308727, 578400095), (106283877, 578535330), (106225819, 578851530),
    (106211229, 578931045), (106124313, 579405190), (106122780, 579413562),
    (106064810, 579730242), (105985896, 580161890), (105936054, 580434855),
    (105879884, 580742778), (105850321, 580904974), (105804209, 581158149),
    (105794227, 581212983), (105772066, 581334754), (105737175, 581526582),
    (105558152, 582512830), (105552083, 582546327), (105472958, 582983346),
    (105451221, 583103521), (105398310, 583396242), (105163831, 584697014),
    (105142507, 584815595), (105103069, 585035038), (105098063, 585062907),
    (105087436, 585122070), (105081323, 585156110), (105031069, 585436089),
    (105011291, 585546351), (105009745, 585554970), (104853648, 586426690),
    (104844831, 586476011), (104809074, 586676090), (104777673, 586851917),
    (104740143, 587062190), (104697989, 587298558), (104624152, 587713035),
    (104585266, 587931554), (104545723, 588153930), (104429188, 588810266),
    (104380001, 589087730), (104344840, 589286235), (104320279, 589424979),
    (104310437, 589480593), (104288854, 589602585), (104118888, 590565066),
    (104077673, 590798930), (104056843, 590917195), (104022518, 591112185),
    (103996721, 591258815), (103979998, 591353906), (103963506, 591447714),
    (103944540, 591555630), (103864849, 592009509), (103796539, 592399119),
    (103732219, 592766438), (103650834, 593231870), (103627121, 593367621),
    (103598187, 593533343), (103595905, 593546415), (103562103, 593740147),
    (103549439, 593812758), (103511129, 594032530), (103286765, 595322915),
    (103285273, 595331517), (103228853, 595656897), (103200751, 595819094),
    (103174071, 595973171), (103130211, 596226631), (103087370, 596474410),
    (103076193, 596539086), (103029569, 596809038), (102885472, 597644905),
    (102881378, 597668685), (102851533, 597842115), (102846880, 597869162),
    (102829989, 597967370), (102820287, 598023790), (102717043, 598624887),
    (102692320, 598769002), (102567658, 599496755), (102555116, 599570070),
    (102529527, 599719710), (102490770, 599946490), (102459445, 600129915),
    (102386930, 600554955), (102332324, 600875418), (102321346, 600939885),
    (102267093, 601258686), (102159150, 601893985), (102142947, 601989465),
    (102133660, 602044205), (102124062, 602100785), (102114427, 602157595),
    (102085756, 602326714), (102006943, 602792086), (101926911, 603265390),
    (101903593, 603403437), (101809769, 603959510), (101751517, 604305273),
    (101697519, 604626139), (101654452, 604882290), (101584554, 605298498),
    (101555085, 605474142), (101445497, 606128215), (101442478, 606146255),
    (101334961, 606789381), (101300401, 606996390), (101285083, 607088190),
    (101252035, 607286342), (101173281, 607759061), (101141313, 607951157),
    (101131563, 608009766), (101056320, 608462470), (100993120, 608843235),
    (100946059, 609127078), (100912357, 609330513), (100894021, 609441245),
    (100883083, 609507327), (100849417, 609710790), (100836784, 609787178),
    (100768441, 610200745), (100717545, 610509102), (100633533, 611018777),
    (100591491, 611274151), (100579264, 611348458), (100567239, 611421558),
    (100444104, 612171105), (100435818, 612221610), (100387864, 612514058),
    (100348047, 612757095), (100310116, 612988805), (100256929, 613313998),
    (100252158, 613343185), (100209781, 613602561), (100186224, 613746835),
    (100178949, 613791409), (100145903, 613993947), (100144914, 614000010),
    (998947534,615537615), (998887890,615574369), (998873187,615583430),
    (998685093,615699370), (997708145,616302258), (997582542,616379855),
    (997349353,616523970), (997208355,616611142), (996925373,616786170),
    (995205354,617852165), (994915922,618031905), (994765387,618125430),
    (994707519,618161390), (994681730,618177417), (994591290,618233629),
    (994459323,618315670), (994231810,618457161), (993755499,618753590),
    (992761495,619373118), (992221230,619710367), (992219195,619711638),
    (992015934,619838615), (991437195,620200438), (990924594,620521265),
    (990271811,620930310), (990212685,620967386), (989687930,621296637),
    (989445786,621448685), (988946035,621762726), (987982710,622368971),
    (987452610,622703081), (987331865,622779234), (987205954,622858665),
    (986913210,623043421), (986682515,623189094), (985746190,623781039),
    (984988823,624260670), (984275110,624713331), (983752770,625045033),
    (983591202,625147705), (982467655,625862622), (982374965,625921674),
    (981001014,626798315), (980961982,626823255), (980480865,627130834),
    (980471991,627136510), (980326470,627229603), (980227347,627293030),
    (979443465,627795074), (979159335,627977246), (978830930,628187937),
    (978008383,628716270), (977699359,628914990), (976938898,629404545),
    (976703763,629556070), (976129154,629926665), (975910585,630067746),
    (975726815,630186414), (975104845,630588378), (973924458,631352645),
    (973832574,631412215), (973741062,631471555), (973300614,631757315),
    (972790819,632088390), (972716115,632136934), (972624345,632196578),
    (972384413,632352570), (972327070,632389863), (971959530,632628997),
    (971861253,632692970), (971638910,632837751), (970910545,633312498),
    (969210970,634423053), (969202198,634428795), (969144330,634466677),
    (968960366,634587135), (968688305,634765362), (968596915,634825254),
    (968417835,634942646), (968396507,634956630), (967904630,635279307),
    (967242234,635714365), (966217070,636388863), (965887553,636605970),
    (965689270,636736683), (965426385,636910066), (964847631,637292110),
    (964766490,637345709), (963825005,637968282), (962476998,638861795),
    (961983165,639189754), (961467015,639532894), (961438247,639552030),
    (960690434,640049865), (959619570,640764113), (959371446,640929835),
    (959299341,640978010), (959147189,641079690), (958784631,641322110),
    (958491586,641518185), (958247045,641681898), (957693385,642052866),
    (957199694,642384015), (955938165,643231754), (955443918,643564495),
    (955365099,643617590), (955340330,643634277), (955264002,643685705),
    (955049953,643829970), (954728390,644046819), (954329530,644315997),
    (953214990,645069359), (952413969,645611890), (951459366,646259635),
    (951183354,646447165), (951155485,646466106), (950961011,646598310),
    (950415670,646969323), (949039455,647907502), (948331230,648391367),
    (948294867,648416230), (948205401,648477410), (947988470,648625803),
    (947792326,648760035), (947648921,648858210), (946160670,649878823),
    (946069465,649941474), (945875658,650074645), (944950370,650711193),
    (944835515,650790294), (944835078,650790595), (944334105,651135842),
    (943037515,652031094), (942163222,652636155), (941965869,652772890),
    (941692611,652962310), (941466682,653119005), (941410470,653158003),
    (941143322,653343405), (941010270,653435783), (940939545,653484898),
    (940790305,653588562), (940704765,653647994), (940696251,653653910),
    (939751670,654310923), (939560879,654443790), (939049566,654800135),
    (938739802,655016205), (938384958,655263895), (938036099,655507590),
    (937842774,655642715), (937316930,656010537), (937157910,656121851),
    (936771485,656392506), (936743605,656412042), (934889878,657713595),
    (934729890,657826169), (934499306,657988485), (934238382,658172255),
    (933479690,658707189), (933303910,658831251), (932086610,659691681),
    (931451079,660141790), (930868558,660554895), (930727798,660654795),
    (930519395,660802758), (930424110,660870431), (930300657,660958130),
    (930199795,661029798), (930030101,661150410), (929120995,661797318),
    (928625646,662150335), (928130385,662503666), (928030818,662574745),
    (927473505,662972882), (927242085,663138346), (926608290,663591929),
    (925610574,664307215), (925143065,664642914), (924916713,664805570),
    (924241890,665290969), (924131390,665370519), (923979614,665479815),
    (923892442,665542605), (923633035,665729526), (923549055,665790062),
    (923375145,665915458), (921924042,666963605), (921441157,667313130),
    (920773490,667797009), (920689770,667857733), (920083255,668297982),
    (919970997,668379530), (919340774,668837715), (918995935,669088686),
    (918771087,669252430), (917710626,670025785), (917369453,670274970),
    (917022687,670528430), (916812890,670681869), (916720189,670749690),
    (916691243,670770870), (916584130,670849257), (914680767,672245230),
    (913910582,672811755), (913827486,672872935), (913690617,672973730),
    (913677415,672983454), (912693705,673708802), (911004666,674957885),
    (910929513,675013570), (910507026,675326785), (910493870,675336543),
    (910408310,675400011), (910104503,675625470), (908914435,676510086),
    (908650765,676706394), (908271155,676989222), (907776870,677357843),
    (907513530,677554397), (906915695,678001038), (906681230,678176367),
    (906446794,678351765), (906372017,678407730), (905939265,678731794),
    (905459170,679091673), (905237634,679257865), (904898085,679512746),
    (904332170,679937973), (904188129,680046290), (904053930,680147237),
    (903755710,680371671), (903572227,680509830), (903490071,680571710),
    (903414090,680628949), (901159987,682331430), (900749454,682642415),
    (900029130,683188757), (899919735,683271806), (898768585,684146946),
    (898710406,684191235), (898153503,684615470), (897850954,684846165),
    (897538226,685084785), (897511566,685105135), (897369214,685213815),
    (897035685,685468586), (896951055,685533262), (896803743,685645870),
    (896424655,685935822), (896042290,686228529), (895906715,686332374),
    (895372842,686741605), (894711615,687249134), (894406513,687483570),
    (893795162,687953805), (893728641,688005010), (893133010,688463841),
    (892686235,688808406), (892463495,688980318), (891115770,690022333),
    (891048795,690074198), (890953206,690148235), (890062030,690839247),
    (890000111,690887310), (889847805,691005562), (889575830,691216827),
    (889149657,691548130), (889098530,691587897), (887776890,692617469),
    (887572346,692777085), (887148570,693108013), (887101735,693144606),
    (887030859,693199990), (886533505,693588882), (886198395,693851158),
    (886163135,693878766), (885906065,694080114), (885293598,694560295),
    (884923746,694850585), (884355290,695297229), (884060177,695529330),
    (883985830,695587827), (883684357,695825130), (883631595,695866678),
    (883510230,695962267), (883215399,696194590), (881897331,697235110),
    (881378498,697645545), (881003818,697942245), (880593285,698267626),
    (880480986,698356685), (880014135,698727166), (879640035,699024326),
    (879043854,699498415), (878824518,699672995), (877866990,700436159),
    (877734165,700542154), (877552557,700687130), (877517641,700715010),
    (877134210,701021321), (877045521,701092210), (876844870,701252643),
    (876835102,701260455), (876580738,701463945), (876187565,701778714),
    (874034770,703507233), (873964938,703563445), (873952310,703573611),
    (873918799,703600590), (873769245,703721018), (873474910,703958151),
    (872090310,705075811), (872002131,705147110), (871951990,705187659),
    (871357461,705668810), (871323882,705696005), (870812522,706110405),
    (870242835,706572646), (870028159,706746990), (869107785,707495426),
    (868227230,708212967), (868157862,708269555), (867774061,708582810),
    (867507069,708800890), (867140365,709100634), (866964538,709244445),
    (866639345,709510578), (865554690,710399689), (865375602,710546705),
    (865244667,710654230), (864510010,711258141), (864423582,711329255),
    (864286478,711442095), (864215179,711500790), (863965245,711706618),
    (863802555,711840662), (863133558,712392395), (862675905,712770322),
    (862004910,713325151), (861979118,713346495), (861548559,713702990),
    (861467277,713770330), (861290430,713916887), (860723045,714387498),
    (859600014,715320815), (859495533,715407770), (859245569,715615890),
    (858384978,716333345), (858184327,716500830), (857859933,716771770),
    (857449670,717114723), (857378935,717173886), (855811110,718487731),
    (855792262,718503555), (855324782,718896255), (855313095,718906078),
    (855178410,719019301), (855091941,719092010), (854870874,719277965),
    (854730485,719396106), (853873790,720117879), (853595106,720352985),
    (852760090,721058349), (852656046,721146335), (852159867,721566230),
    (851752330,721911477), (851326255,722272782), (851113835,722453046),
    (851033855,722520942), (850953565,722589114), (849923466,723464885),
    (849616274,723726465), (849604665,723736354), (849140565,724131914),
    (848604757,724589130), (848327865,724825634), (848200210,724934721),
    (847896403,725194470), (847668030,725389847), (846835206,726103235),
    (845727870,727053943), (845481910,727265451), (845379145,727353858),
    (845353985,727375506), (845263298,727453545), (845200389,727507690),
    (844276134,728304115), (843020633,729388770), (842941099,729457590),
    (842691135,729673966), (842364926,729956535), (841675593,730554370),
    (840783515,731329494), (840577803,731508470), (839925086,732076935),
    (839737015,732240894), (839607594,732353765), (839398098,732536545),
    (839295457,732626130), (839083245,732811418), (838028022,733734155),
    (836988285,734645626), (836978961,734653810), (836736159,734866990),
    (836702867,734896230), (836337270,735217483), (836130958,735398895),
    (835917635,735586566), (835434655,736011822), (834885205,736496202),
    (833972230,737302467), (833820702,737436455), (833472354,737744665),
    (833452081,737762610), (833403597,737805530), (833381990,737824659),
    (833271413,737922570), (833005030,738158547), (832848170,738297573),
    (831527970,739469753), (831320490,739654309), (831318785,739655826),
    (830309614,740554815), (829687193,741110370), (829637655,741154622),
    (829438610,741332481), (829337795,741422598), (829024305,741702962),
    (828177882,742461005), (827557059,743017990), (827367730,743188017),
    (827284073,743263170), (827118502,743411955), (826679945,743806338),
    (826672463,743813070), (826640606,743841735), (825770495,744625518),
    (825443619,744920390), (825000729,745320290), (824538155,745738422),
    (824089926,746144035), (823780815,746424014), (822126162,747926305),
    (822058341,747988010), (821887066,748143885), (821714907,748300630),
    (821476533,748517770), (821354610,748628881), (821230410,748742101),
    (820997366,748954635), (820614795,749303798), (820101590,749772699),
    (819659335,750177246), (819412429,750403290), (819170898,750624545),
    (817589487,752076430), (817568290,752095929), (817500845,752157978),
    (817121690,752506989), (815542234,753964365), (815517962,753986805),
    (815276130,754210457), (815109438,754364695), (814652410,754787901),
    (814312070,755103363), (813096830,756231927), (813036315,756288214),
    (812221410,757047001), (812034274,757221465), (811985790,757266679),
    (811603715,757623174), (811538871,757683710), (811527145,757694658),
    (811450885,757765866), (811083845,758108778), (811031342,758157855),
    (810392142,758755855), (810099238,759030195), (809949462,759170555),
    (809645655,759455422), (809443635,759644966), (809091010,759976041),
    (808870755,760182982), (808623530,760415397), (808459361,760569810),
    (808385853,760638970), (808317870,760702943), (807447522,761522905),
    (806842239,762094190), (806566530,762354697), (806391690,762519989),
    (806367562,762542805), (806035195,762857238), (805888743,762995870),
    (804030942,764758855), (803810371,764968710), (803691070,765082263),
    (803609807,765159630), (803226710,765524571), (803060518,765682995),
    (803033385,765708866), (802923090,765814049), (802403349,766310090),
    (802064165,766634154), (801978122,766716405), (801481161,767191810),
    (800979922,767671905), (800597490,768038609), (800356326,768270035),
    (800258459,768363990), (799740015,768862094), (799573390,769022319),
    (799476205,769115802), (797743310,770786511), (797314110,771201431),
    (797168658,771342145), (797048043,771458870), (796625654,771867915),
    (796203265,772277394), (796179615,772300334), (796053335,772422846),
    (795141165,773308954), (795089694,773359015), (794681745,773756018),
    (794580402,773854705), (794260610,774166281), (793976123,774443670),
    (792979770,775416733), (792882805,775511562), (792729210,775661821),
    (792652795,775736598), (792221430,776158987), (791060666,777297885),
    (791001211,777356310), (790934690,777421689), (790730182,777622755),
    (790664951,777686910), (789806706,778531985), (789214647,779116030),
    (789066033,779262770), (788885510,779441091), (788688670,779635623),
    (788642790,779680979), (788229715,780089574), (788150913,780167570),
    (787362565,780948714), (786771258,781535645), (786511726,781793535),
    (786346977,781957330), (786316674,781987465), (785760162,782541305),
    (785341095,782958878), (785147363,783152070) ] }

extern crate bex;
extern crate hashbrown;
use bex::{swap::SwapSolver, find_factors, int::{X32, X64}};
use bex::reg::Reg;
use hashbrown::HashSet;

/// The real challenge: factor the 64-bit product of the first 15 primes.
#[cfg(not(test))]
pub fn main() {
  find_factors!(SwapSolver, X32, X64, K as usize, factors()); }