# Seeds for failure cases proptest has generated in the past. It is
# automatically read and these particular cases re-run before any
# novel cases are generated.
#
# It is recommended to check this file in to source control so that
# everyone who runs the test benefits from these saved cases.
cc a5a81b58c7d40d53f85868fc478bea1df015f674b3734f6f868bf687a3c8fc74 # shrinks to entities = [(182861791921025984694243607050717012, 0), (238879957003700546320528103070476771, 1), (823841784202407851711045064114091516, 2), (1446427375719569338856740434766508083, 3), (1484076865652467928958046465830964939, 4), (1537828107851569460617435153369540155, 5), (1954265158503058568742109263902222199, 6), (2100658608388299601346336834128975930, 7), (2133891685978816137710543505710474585, 8), (2262591586381134448367723867518103429, 9), (2362457692063900212609758186824095988, 10), (2377212781685796745625252237024862257, 11), (2500516925117237048867521946288689671, 12), (2904213727146898261761229298463079387, 13), (3562031810097679815201916050982221260, 14), (3720957092783717318547084548286670847, 15), (3997223739807804736150547048910778379, 16), (4318807638511192292662012535960160066, 17), (4369912646818800585142078316640953510, 18), (4630004365106089858563994849879793187, 19), (5127940073168358457424944166829564313, 20), (5607445314906773410470986274967225625, 21), (5941188219535766843994681655063770857, 22), (5970381434429808960250467105666142898, 23), (7076282387307312168683847524671048137, 24), (7187273415113592086690105494324749068, 25), (7421338418223715107908980506158437102, 26), (7529450978880750219574883997027090765, 27), (9078044113663909771783950761027173511, 28), (9495497724365455681016419751710005154, 29), (9824711651621124000134986875455883739, 30), (10020493591913612428883467613559470932, 31), (10162732175971015827631255777893610780, 32), (10303565204620631295428476963961172173, 33), (10321152986233809097051988367112335605, 34), (10999477804638569316611975942904962221, 35), (11278471672415838427223734701783718855, 36), (11288307270054057618965270277185525487, 37), (11434608115960444739430323873873250780, 38), (11522694171842891340451913453852895515, 39), (11718221754555922543752465824200463066, 40), (11798377549769836139500883410222640161, 41), (11810494258770839359869226809114876225, 42), (12063813571598262387141282886599869563, 43), (12430853860176610693693368528881485758, 44), (12783107538214403909788580321100962872, 45), (12977752332913910325809824996951404629, 46), (13074241554239836248160338812842411622, 47), (13360862488492517853299940386564778132, 48), (13715080303628236142026907981380199296, 49), (13821431904518200057932733624252753586, 50), (14855071734710604171558512015748489903, 51), (15194372870675209616313045921003434771, 52), (15366493573237556745464764145908926894, 53), (15662545312307196968528174330329802340, 54), (15838726247347163827005696892996368784, 55), (16078785308385629704456982525268015607, 56), (16180019617653124016477532925576583221, 57), (17018610537519069817702276495000268355, 58), (17022781132306460760807115076742656857, 59), (17091986078611776119208432270502437122, 60), (17599690047319896088100890844694958594, 61), (17995069387701405270298253872093165363, 62), (18782108225051300896753292536618085180, 63), (18872521525159613812786913019325082290, 64), (19145149639589530708722331163713829506, 65), (19383990784846190835383095487417767286, 66), (19440576530573744441018867581868637922, 67), (19664465907319774654988764162587651424, 68), (19667757802321587417354864604096798321, 69), (20206884179421315789396930237806540923, 70), (20303857124055192836207023117448325707, 71), (20767373428122176773057653451746296774, 72), (20874748445621536006905605357657556029, 73), (21221455537896821458262547154039329295, 74), (21280419079459667321651356108425278589, 75), (21465570459605966856918578848223863406, 76), (21585560469936816848262115963844896542, 77), (21860984884213614637723667328322274589, 78), (21926924774503003401454546638759338943, 79), (21978723867415979879676799881428373111, 80), (22376773213388227110978873654532910158, 81), (22439375492109735767452147256290210011, 82), (22786050309098112869135498935933965128, 83), (22891064341888932511065178954071672297, 84), (22989831965361395243483010801032301473, 85), (23028711621205263894976710219418592626, 86), (23485412775277237106424579983819993509, 87), (23613234544179515788951562147251362538, 88), (23979463755270096196770844856674514100, 89), (24164008874438702020288565436774026602, 90), (24923418644364741590942140522813141687, 91), (24971966364035790031459733776311260641, 92), (25575663030836409916915722302867771849, 93), (25791017607273359280730985688642849930, 94), (25802494337729341174583247002035884704, 95), (26538599074736801062072648200473321386, 96), (26894129163381651090457361588798541855, 97), (26973934670497174673004177377914769085, 98), (27096446191770225852373187328335896536, 99), (27319691979511852180657411199757003322, 100), (27331474480397361526306801005846033282, 101), (27419630474262792949878134909678400312, 102), (27427024441646525414413576033191228296, 103), (27525323591254508678936953433442768198, 104), (27551951903255520554363061306380126354, 105), (28169326408134995657227912403586671336, 106), (29174738054374822704733089410446936986, 107), (29824472696128239284521252318536937405, 108), (29985305676750460220105584032038286643, 109), (30036534352457273847100625338712029014, 110), (30332745905563670522117197367824681603, 111), (30389958414202982155166201680185828486, 112), (30855432805894693101115877069532911800, 113), (31008185765513445303128034250237566361, 114), (31120473597120020351082076384255620696, 115), (31205267779768638732204345878398920206, 116), (31228235349141723177765441122817750951, 117), (31379794769150265940968648558777752889, 118), (31485567715254259094377436843296905640, 119), (31856791791833998457824858207072725450, 120), (32577158031452475286318124936658738543, 121), (32777972524756617773879711775541390021, 122), (32829219689973467407542907153979253503, 123), (33512802256462871294366016571238181253, 124), (33746560844592680783044125720961861577, 125), (33804204708736248835707678910469578635, 126), (34089107365643593116372136122341759590, 127), (34341915324052613059972924652857050605, 128), (34438980972325204879938785692616084868, 129), (34446017662343262845716177508424998338, 130), (34531786216712860982788133172042464555, 131), (35228603397683689522656478690484898527, 132), (35673324576630264960702375487409348248, 133), (36135989634284702953920443203653099258, 134), (36183524531471890171616746805714930888, 135), (36381906670662044574734122862435271491, 136), (37207783911716737089705806429436688238, 137), (37484149321300153032121314275945040020, 138), (37746203991584203744942534502193717171, 139), (37803651880452622914905126600632667758, 140), (37902173047509597681906069468086849051, 141), (38271847635053827555087540546693944328, 142), (38303356721572080628814082406981622118, 143), (38517991983480797272837771727155590963, 144), (38652483853678619002993690456064741751, 145), (38789402203529774122400752329974295856, 146), (39185375250088549805408753306625441388, 147), (39444539222116146298327786262346443325, 148), (39661391414928374057722436559114382213, 149), (39752852591570781348225343813830795051, 150), (40002904613828848567815586999906895736, 151), (40096977441534437901996823342474475015, 152), (40606942628782366788937420989811191917, 153), (41128678453443907584366450851572329844, 154), (41499262084185121324285868181514278774, 155), (41510854408698885227362295749506453102, 156), (41513021642966210221845683666084876023, 157), (41912738911328079067088196066338408578, 158), (42100934502089468756628899750027156855, 159), (42255612523259340165415018984044111655, 160), (42535880912263715488717146810601850156, 161), (42614953421033713208040183761890263502, 162), (42617387183891271461084653956285640363, 163), (42687156627981198478553025686901740047, 164), (43169783387450310469861081054865241805, 165), (43556639456641643936031878039070074848, 166), (43621288898331984316174126368818308654, 167), (43731448884571131079248418112052297730, 168), (43979545883427950965622691074898538537, 169), (44305716261377696900991525255661893306, 170), (44578676449742220022656150038711601593, 171), (44876363236291278495787936134314755728, 172), (44885175160503891780099796255450394067, 173), (45128893357679594762043911467125529171, 174), (45667816819691150282202741115809782057, 175), (45686693594334994111140618636535505876, 176), (45813442137940146764509967508687925584, 177), (45847831671584305736064090799431603252, 178), (45909940702813930170432548678728224231, 179), (46835934826449393833304927316871308341, 180), (47287204984940179487233720623829551956, 181), (47818166737107150516179099472354364931, 182), (47891589762238002753205641159490280037, 183), (48660726348322643012716283060416681769, 184), (48717729210427728394970364402244804409, 185), (48724565353665429850254023908381018221, 186), (49272556467932430315266996801128107551, 187), (49336073549548586919023980688024321785, 188), (49583622782307762423860188496586899246, 189), (50041049408652996314250354540793267186, 190), (50113452166323835180614114013537649314, 191), (50154207869908476759514620136010503182, 192), (50406633558764654758070507525478135745, 193), (50530677567058533727164461003626079422, 194), (50628253044601046559742692754365047809, 195), (50726135500352603316372926781792541027, 196), (50728138110456835619535871780688383198, 197), (51274376866332653111257367924328078591, 198), (51957622085486324848992174430650101455, 199), (51975069293814212424996959612483767902, 200), (52462586728511240840217753905278365995, 201), (52515756557391257618677415889054804710, 202), (53097014019826573698483202741305631791, 203), (53229004967888387821539584851040157665, 204), (53468069999046282974168846401358483617, 205), (53903096466388463891749619383360246272, 206), (54143580880729285575031265981315132199, 207), (54185871824227404189262573729942829856, 208), (54866267411377703783217624459788911130, 209), (55141827656684800572707837638190305202, 210), (55618160194109875141680243263288418904, 211), (56125885299983039277035915298256651285, 212), (56581467011681396123436842911927811799, 213), (56993407326522022928203485924275837455, 214), (57013470374323116733602166080022332857, 215), (57898223050433261436380056586635801824, 216), (57926437350962153477019693086201419847, 217), (58169300816139115442803732061258399440, 218), (58363765235983148817982878886669561043, 219), (59014609306668408892846408658231367626, 220), (59070140162186864544398954067534175674, 221), (59763264830943685337274387766341010566, 222), (59804155508283437453896097115117884067, 223), (60314359657563747227048328551938493864, 224), (60568453403699508154866180256257399995, 225), (61350861332488350629433788125353294286, 226), (61569373054114112080835004022468566593, 227), (61575459168055293393731935903311957423, 228), (61583382910114139568423727932559910196, 229), (62222035963207941123613867282407899828, 230), (62416242914174944902950663547141692780, 231), (62493969979700645150898531092634621661, 232), (62607485660580551135690695643361692719, 233), (62829411483771595518099433240073951876, 234), (62981102084941154610987147629271018948, 235), (63012599370599074719556804505143071989, 236), (63032919760593284026295554105626624540, 237), (63212163252182326457174866697834867411, 238), (64021993496429814624773201395428642274, 239), (64073251849766167866698514541886937201, 240), (64179507796733677262132668582980825327, 241), (64201490869692468827882491311989579737, 242), (64625010476637226521275816505870584780, 243), (64836395915216155052486760389390452396, 244), (64892402899943704642943929996475943596, 245), (65052779512222456432477771758357319121, 246), (65341256508292616012500582474769582517, 247), (65507534524642981069091301470357760791, 248), (65533633167728141584504473591067172193, 249), (65601810149802280681890755939284662191, 250), (65619687055465287773401284160628717817, 251), (65746031618858058520861605185974002123, 252), (65747263984823565556029858290543339499, 253), (65805343541334546465779277148956954337, 254), (66098783366409857681396219665765152386, 255), (66856100944872241644797515480545511075, 256), (67112026180467002454710364058919983127, 257), (67342195421952846044433592962972385070, 258), (67828939453893537885553665798039596008, 259), (67980386039463462717048032162827208747, 260), (68056612320696212516912429034452876562, 261), (68097063099535740837988036864501716989, 262), (68165111961315738933620510436740332827, 263), (69246949549808120019329868715783870959, 264), (69376112509829198401399037315857704570, 265), (70225417507355410923886804712351968363, 266), (70234833421148569494010309655401406027, 267), (70504817100634891112208046402856179095, 268), (71184475438350598149698635805102935468, 269), (71499136830314358721853800131424595914, 270), (73742860314568984245248142490746089314, 271), (74232017572587057078181387731193389430, 272), (74393456893441667901838907981666891581, 273), (74795772882336429698867293841750734981, 274), (75080201160918054128207069682551701696, 275), (75507396711237099994680584532905169476, 276), (75599903182181090152402573404782592863, 277), (75745499225811480826773817154085562534, 278), (75988911633791882515797721014232903241, 279), (76030482801560916483801179185274968889, 280), (76241280272606528895158295110690864922, 281), (76304099923358315181576416064398174849, 282), (76727028175342273421590293909686142854, 283), (76935996384759347486733117515557011043, 284), (76969134831177865269395709827448330968, 285), (77277243104824023481804211287275384596, 286), (77298115750018220118787128474084886133, 287), (77439300523835188936330434968183382960, 288), (77940621113222901549647510787622112809, 289), (77972356556947627402170593566822046352, 290), (77984598446507449280970298895212872846, 291), (78293334653866220319533445152737455236, 292), (78303215499534218099740671186157059130, 293), (78551808085624716273969493723435350332, 294), (78593648913257832375063074127486217024, 295), (78667344475902120669026008324478523797, 296), (78722223707959907711907552343355331157, 297), (78750116974196557128789980047311399163, 298), (78755972116367691750009002360406492159, 299), (79180599475306757661615527206874256695, 300), (79367666277890261132144935590932993720, 301), (79386491141376867873691185839519061340, 302), (79876079354292289031125013994145642290, 303), (79876491250026505458038685766433742255, 304), (79982173971030305901383642925342911692, 305), (80251662828459292432971279807821660821, 306), (80479822224120506644471253748910770943, 307), (80741278309466522470555142110773604211, 308), (81029909831235185905938564902466483245, 309), (81276496752885744389459360139412114440, 310), (81459816738242767544306200082630157528, 311), (81768101031070683874339366012492491586, 312), (82132187514183234164883431576389932486, 313), (82402345667784368532398463318066647066, 314), (82445332700792376336192627611416165618, 315), (82470614627723036104192617328546350366, 316), (82844212593054252522878762255108151707, 317), (84383892946750816866063944992813978700, 318), (84436603838406429869879041887833223941, 319), (84637850702944320315178660965732509601, 320), (85051387436535210944708369200949303230, 321), (85417272480385745558613774578001070805, 322), (85530339141036412211268128297965773248, 323), (86106820528099215622171287220777550789, 324), (86141484473690145594038710662217951040, 325), (86816429805238748381799918441558915800, 326), (86954695703443601043586270640023747962, 327), (86987464365675003530601580429193578623, 328), (87058472710900092918374457537187648775, 329), (87097639802810251646501583353410399094, 330), (87261553838681999783982117786836627620, 331), (87350345484529789596698847589730051002, 332), (87717561829290996190981618864570157207, 333), (87915752717067616077601835424855579475, 334), (88156167572183090303395206592902125389, 335), (88200377597448380537785304506966960094, 336), (88797488659094357373871906107559837460, 337), (88856690700630828694895971155247985708, 338), (89247522364641009726058790558135388939, 339), (90062895201516397705045961974816756801, 340), (90472669012738114676800505736550329075, 341), (90547424808306302852151014232444301156, 342), (90938813511333424224562457388371722363, 343), (92385432186499483569202476932771407751, 344), (92821104620867162284958042036413790303, 345), (93070251487276090511614074306308215510, 346), (94141112543919072608996751021283327224, 347), (94244518885744523086646906921443699132, 348), (94310943376581499836405718702617221329, 349), (94357662164311630975138724904347017981, 350), (94570588246388425150901602146369970973, 351), (94617018546488496774782022161705567177, 352), (94789952484375968167318063208126950529, 353), (94959199518390289448133413588298209506, 354), (95171461803693022051681832169767802131, 355), (95205599729456733555046622595728991610, 356), (95399903385274703115994711302064845210, 357), (96427864095501476795863340805962543435, 358), (96646796686758859967919273740440075194, 359), (97145664225177704377305393153945926049, 360), (97293351600238057478338992104519373956, 361), (97704337325803290925732974949226917343, 362), (97795302146916127879221929472688825975, 363), (97869590085668194148578646441614440140, 364), (98002000284647523878957902901396641502, 365), (98519836237306136578569029843411245217, 366), (98663777582196723500657572242185498721, 367), (98919617499702938959976253402151686804, 368), (99059794229494975620688761936405150708, 369), (99088750057539255296694264964996617581, 370), (99189167826139494662620941302363363194, 371), (99459283780284482519389163908151530191, 372), (99792651247874777557264687210480338846, 373), (100105093460919234416962299500325084001, 374), (100169182888606940445503139651416173131, 375), (100554602097212217110782819130832922498, 376), (100685369998316549499268332533839125881, 377), (100974140282926038153898307604669246483, 378), (101380638797843023298609606824980543791, 379), (102439497818109465540147026626936251781, 380), (102518844529915898333567645961581163724, 381), (102698817157766385983909267582208123343, 382), (102907823514143318705492853621690195842, 383), (103401935325121196782088690238763377028, 384), (104136115982559106382400985462253704190, 385), (104394630862523182574296227145871660265, 386), (104686072618328413982820104042617479810, 387), (104713836391818178963269154281258502906, 388), (104737405178482477100058175940281369558, 389), (104878941635471226426274306586203191535, 390), (104944489394286206937502227657019398853, 391), (105021160852250000948285425855570264288, 392), (105060762374779156591270342102257749963, 393), (105310917148701521446008211259569446923, 394), (105482915552079437784812773851798574474, 395), (105715965801564313880679595434682086314, 396), (106548817689697750315326386758948237114, 397), (107485905777091908975398922353357741759, 398), (107840075830358914693442564224146573914, 399), (108000887272157894387943906874639986067, 400), (108218113922743535521893733590219988748, 401), (108611894951451952897425748379151237334, 402), (108634499914089175460336250312191087730, 403), (108711690070405180249266367201686054632, 404), (109027899480002233540794603162491084551, 405), (109331581096733656228215679137225238449, 406), (109368364508985999856331585918577299106, 407), (109633141634660512325058759015686869719, 408), (109676768125656739376809792777447997332, 409), (109776756589181575561394929889132491169, 410), (110341872213780759013783491281405813126, 411), (110552951808835617200164000830660918636, 412), (110644792462036894393157849800497074040, 413), (110916393670529835181381121878342610502, 414), (111263962911202489115499064178948552282, 415), (111270355150449844665551247140686020469, 416), (111404763062221973024345618786516292825, 417), (111455985851796591535257879347371446503, 418), (111756946403543227087914439574986225567, 419), (111921210004830064826971183903203045845, 420), (112054143742852580444486818899503919591, 421), (112337460502551170245580132068881489177, 422), (113583973307113705573371048679481570082, 423), (113644451362577563882377608010578889190, 424), (113885114052779850807750443475909978828, 425), (114629689782686836480133615995183995585, 426), (115520221163757851230653261277798056634, 427), (115941705639652347317661164820286449534, 428), (116006193992134858836099228223751223897, 429), (116121550518585463706816841688271212201, 430), (116167855394686667597129698080644558869, 431), (116457738581496567928504601802201297205, 432), (117387683453845354349687158759990399721, 433), (117490524786076583067747951705307159548, 434), (117685311507016265673303316155242150681, 435), (117743040108145459904429696750605594547, 436), (117834008932243399862457799522632612480, 437), (117849156234570072708876783606196082000, 438), (118375540336035440081159715269424929236, 439), (118378807404018967114323999372082460304, 440), (118715388446466557424194938430214948851, 441), (118811440734156450637290272429325491867, 442), (119030815919432482293324105214202670874, 443), (119225269532040220040337177060631230739, 444), (119229072803858755028496586093659797604, 445), (119647397657253115802671341340913639626, 446), (119664197546407465544677530778632772752, 447), (119866469523060086818137808726043121963, 448), (120170487792181959632016519366924757268, 449), (121333156992661674263818983106505501678, 450), (121358951991161908540955820701136567234, 451), (121494546463733704760446745673277825152, 452), (121658422192408686027358982773752941204, 453), (121864748285296760017449200492624185876, 454), (121904663391481788728188706422936139395, 455), (122795722547441589628811917010665177762, 456), (123002768677175924435237337613144570674, 457), (123132101040362090708960249054829396938, 458), (123227031101336283583754017803518312842, 459), (123240087654600520658275376943309082591, 460), (123478898505045043400297764527080788416, 461), (123713492073665845248651445755480564131, 462), (123842757431430175506401666165504143608, 463), (123973139989280618611489401680228956401, 464), (125336050893768189101364891408295770556, 465), (125578985933001944861700086061508821382, 466), (125916612263021835213963636510615087645, 467), (125983847960667200667874062444928598089, 468), (126131498911649828115397912949920934156, 469), (126641230901153535022822781567852659016, 470), (126677596019643273985442225215682849050, 471), (126852372039231369836870653627069404200, 472), (127377763654122378277008130308430356467, 473), (127472495079178201767697078819368970924, 474), (127583076430068444743402788448782088470, 475), (127722582155409507162995040897204377818, 476), (128305948243778939978475844260600144160, 477), (128381070936313333559390410940150570085, 478), (128586704597857044966876140085878738344, 479), (128801977933067529333908980386757581998, 480), (128916355490282835155948223571331191964, 481), (129187006755491957548554247698325520635, 482), (130056799898304405633738168347187811269, 483), (130230303142402448681476478350245526732, 484), (130247218067825223415176029763776271382, 485), (130277407369027853531534563763194702992, 486), (130497725546085915504085880366161286428, 487), (130796721170804564889986285984451475878, 488), (131168057061067002099773391504293179853, 489), (131197671799402890556245092963403379006, 490), (131210465378244227758010674232583729127, 491), (131241369193315663504916774797032144723, 492), (131299155873795411466222082352231341094, 493), (131369079165639647255671263718004520388, 494), (131981141354318745865608393217301327972, 495), (132140627853891225708756624691886314681, 496), (132158000464568367366689265820809004465, 497), (132270184528213200996935337792450927002, 498), (132590161974544622937119111832572974901, 499), (133106403508156709158920930626785750484, 500), (133213414353105881071343881642247327745, 501), (133339862392593542752483501384979509747, 502), (133475551551946889999101602218992286130, 503), (133530974997104543308187289451785667857, 504), (133809587126481074350847356931898732842, 505), (134439603812881498374978962549293517911, 506), (134478605819361007807971823038917675994, 507), (134755376223517273220600107660157418962, 508), (135037504701483359084082734684147032598, 509), (135613390480218539510690235147597456816, 510), (135997650757758017895554720471319913340, 511), (136165264075967568567267534351426128144, 512), (136857818790515861867674233099905750026, 513), (137146134040263711660728850254159793043, 514), (137264587364974288812137135362266708670, 515), (137391265220055379693452805016331395339, 516), (137486437528272633718157733393503663243, 517), (138256073482960574223066135007062471242, 518), (138549258828950582617898042787440735842, 519), (138602706328929169410505347195622987514, 520), (138725824699873420414373814608619017878, 521), (138876261148506702094454594919667507837, 522), (139005837492909698446451954945127468020, 523), (139245461857299575432239492942902923950, 524), (139459355461945524121099198605945297209, 525), (139945047822521257012065991662923163139, 526), (140111544900357337461548616430492139529, 527), (140560456953084383580482645454743412348, 528), (140746171584848164668913853900476203206, 529), (141090384204657007131030781478253924278, 530), (141103064391162735527559908755777478991, 531), (141525046048930669507853774525998735351, 532), (141655418118969716032717124619170305276, 533), (141689856757204879947006937547248411122, 534), (141738157312989889380986241728713576513, 535), (141961485948475557915408426415105836516, 536), (142226252705832271020248569739130935802, 537), (142437050818923594393475019534180025930, 538), (142499829436021357399007022280315165226, 539), (142760760406412302280216796241358920699, 540), (143016112826636154130086379163715808031, 541), (143024408901683301223369730147523857856, 542), (143267631709819858092747382366940352951, 543), (143326307132886315961834252410059926375, 544), (143420389072012366656016871367581617211, 545), (143457074548386103353000315484973597054, 546), (143463890486885602328666177425425550796, 547), (143501473253330622789462926106268956374, 548), (143728711034928368608269275645848117694, 549), (143752852563458093679638263611175834048, 550), (143849179669393940360831909503454650289, 551), (143913518982604601781568724747986634460, 552), (144006345021717420164691703540878203593, 553), (144367120249723446815946208073029874789, 554), (144553253391056578160435581428775468297, 555), (144592355255873793222012992865816141796, 556), (145310265170439673537481271235471887223, 557), (145338263509534630377803609001553050166, 558), (145812398864490854693541698045594289245, 559), (145928503286426344430575193450156349219, 560), (146232024893851496900718323860998343576, 561), (146590736735903116837280300615337534222, 562), (146707869131453340407951149248724650545, 563), (146804641309230041067698952021955645651, 564), (146821588552837839221994454807745867722, 565), (147364842724611904160571928502541538012, 566), (147398708301611015201392480804135470458, 567), (147478348824040148304890564546237207481, 568), (147835554602452258442247325485931221457, 569), (148204049041536406105744786530310498074, 570), (148384139095061964233710477732075420640, 571), (148443204446022361031805884595532918609, 572), (148451084568336802707026322979050032353, 573), (148907480861046053524425500412293841242, 574), (149602772807297617977643083585038257638, 575), (149696522604633311419201187338059136262, 576), (149747709381352024655138374080646623009, 577), (150624428349044659823379692314320376118, 578), (150664421626674882519664707321958093940, 579), (151105722669267415634567768405300330642, 580), (151228389537816727848065804500513891884, 581), (151455012474858801224820038480490666624, 582), (151455566322852115032747082522969138853, 583), (151545705734287771574657904153045692286, 584), (151661012147802159391476534248206623694, 585), (152634554781277455351190053599305243296, 586), (152898284607508288967878565712554199872, 587), (153002697087058884695801318209979445760, 588), (153257168244465035493225809097402430955, 589), (153768436233291990885361514138449138020, 590), (154014039773743983704799402245770550193, 591), (154519185571539025326009015816980924332, 592), (154845156872733205965737827170227596175, 593), (155890705608627389939214226273958463751, 594), (155961336660555318968597070893441885788, 595), (156212451242553505095522258603034594453, 596), (156415432560052963132167235794049292431, 597), (156699121118478969123308290094637462758, 598), (156701902347708064455718097564172439333, 599), (156761275758184529570666823236434182078, 600), (157282784252366132179784814511371428743, 601), (157711061117041771814254109072643782484, 602), (157987784216033692907561821356710924295, 603), (158238041407946425391226136946537342905, 604), (158822312952828694621370778362278832576, 605), (159693213935254847022515264378560359324, 606), (160080003110978106716848923329613214622, 607), (160459874243564212707047866996261209595, 608), (160489303208179615041746957499905362745, 609), (160606826944045358895163073770189129408, 610), (160779111277586837360394990393014397928, 611), (161100345353394781790970568731103046302, 612), (161226429569446911133072778748856856055, 613), (161242969613562810160061150212415613032, 614), (161569907635187105518536096709264258572, 615), (162962014245308476424292177250191947225, 616), (163310230951106023729895076232351060796, 617), (163388215078336241557319291808235526511, 618), (163831497276938001660673415288941363640, 619), (163860554694616261497959726096229888369, 620), (163972868143234646972439471482009815143, 621), (164003315416277135756732964937953467307, 622), (164361608462867861044962796585189255118, 623), (164989480449794001375810555139443330289, 624), (165162386092731709993434021900369643093, 625), (165795381612253061154614225034724712974, 626), (167662054718243554992324440302019925027, 627), (167934982614138889134570659496915102728, 628), (168948339090482944149700026800205906830, 629), (169442855836830174164784290353519551037, 630), (169579439913694566474943266208159221937, 631), (169948528871807544364242241762388106062, 632), (170285997942426607320837436279072861121, 633), (170386506662927682369632200239187958753, 634), (170465799797904483245770463611540866058, 635), (171215404100234722159953442892801282667, 636), (171368022901334765603027234420946181871, 637), (171451570458281634122193470610987698793, 638), (171532569388631477294382037837749933752, 639), (171646555376828405954479765822232399249, 640), (171720933998153810982274107834188564265, 641), (171890518012752485272170108589229820365, 642), (171978897991066805821839320542469572596, 643), (172053188666054330596797819264958476566, 644), (172193124089797471867804418870421569220, 645), (172298590894036949840862079621767884495, 646), (172494789849268881208355429866178727914, 647), (174437338165338898457861106896340987791, 648), (174611585769615419366159257519629656985, 649), (174648634492209571622797480137455472134, 650), (174712424685991103222239205912070560020, 651), (175265238294494775804048772330142989045, 652), (175510228996433119299150825431285751904, 653), (175515409539603403660794623376147363235, 654), (176540188266455356298904772672003227366, 655), (176606268498244591578557903787143338736, 656), (176998771894334995566593091707185675526, 657), (177424187445407226770270571241550995491, 658), (177439517054543734323225751216435149132, 659), (177852017834660134292705918226800961335, 660), (177981686601624891353563559059074431067, 661), (178226212997348548675315815844546560306, 662), (178447420017740020384310224057951791942, 663), (178456305512598420951738467416169832776, 664), (178769589244051314959638496234384852094, 665), (179160750444140644168753630192089956658, 666), (179672781803297756307652245222785979053, 667), (179680861914464189789349692755610362222, 668), (179784788811949307515211459135771468513, 669), (180017085864355811509079796496560606461, 670), (180307798286677640385488947049577549458, 671), (180387676193510147175053654962364208708, 672), (180469778424168190954099231505946583438, 673), (180540478821361234087705811776249297520, 674), (180546344967631805469736168893322127120, 675), (180729814062769827376700381479899913814, 676), (180910479962726615033843021966277030773, 677), (181084777880901906540916171532313082762, 678), (181631323456248377697952073788149753159, 679), (181808878357048052997564911006875981709, 680), (181871661821193948738213685881692509070, 681), (182346663269351873220541915625193373748, 682), (182369600742899262993103649343862138620, 683), (183307573969775109127077035796592922047, 684), (183687292064183712497009016746805384128, 685), (184135152697954384930877477638160399646, 686), (184473136562170328327560931697324962208, 687), (184936763567914152577671366587897669720, 688), (185506743088675624879105349135119784758, 689), (186043811863195777716631693162777244256, 690), (186476896023803951438920413249920630876, 691), (186537111349319967592714077244038229425, 692), (187367781106802492524286636303282502400, 693), (188081932592873798839377697309574724938, 694), (188312324370569669051535173037762561607, 695), (188644559219904041363757781829590968626, 696), (188889231071254617427961306834635162589, 697), (189060122382569540713682286324058700138, 698), (189134867247242130811679784407729873714, 699), (189711203722044060247279708769750805541, 700), (189753772779897409790914082315711246135, 701), (189913752677407421857409564054014020112, 702), (190141630179461941750625923737034708970, 703), (190247617437231165507915575968246050803, 704), (190291840792240656476453193756875581902, 705), (190879219797197320018410524735039071115, 706), (191061360780838698222884555659225161215, 707), (191430125561679702695979554837152922179, 708), (191448397699690012943504994951987605844, 709), (192057317385592015262020387462960964792, 710), (192059868859825445266961145073087161690, 711), (192221354337849095968551352141253515755, 712), (192408797026425186102085676085915233953, 713), (192637153371900535728498048617957084405, 714), (192637297980757523364294265903699198932, 715), (192826226704350305661427861825380820679, 716), (193268865061354897442513763269998641075, 717), (193396654470571786192484939008316022164, 718), (193981749298514063910949443968736820234, 719), (194084518806460438067060285085220459342, 720), (194566775547967121388931832588307663588, 721), (194632308458508981292630870793701428727, 722), (195130290742806271181437200653229530547, 723), (195170231631112532805858678246646805856, 724), (195398822884912517832748994124809249490, 725), (195604982527299494958572344956678720222, 726), (195606517868704768669993165541452023032, 727), (195688854036200488410176216866472022385, 728), (195987338935959862332760379627658473029, 729), (196160863890570887842336430236565437084, 730), (196401457898726695447486826936896661026, 731), (196628455579524757515436157156455710253, 732), (196670101107009198378820580948290458907, 733), (196960709330085151154768697561475574920, 734), (197007671662124473512324870426787444444, 735), (197362519029326455557618602035849179621, 736), (197514106847167743333717410484581541389, 737), (197562130687003052252010133071367635130, 738), (197640438954777280890000774540807823446, 739), (197900057418291668434040239984255863730, 740), (198229402320892806397212215346433525959, 741), (198336405355530430362676582040793338865, 742), (198733313444612170305460053964343848162, 743), (199022713151610739757461555277979323837, 744), (199638279105918409015059815464095701470, 745), (200068504961523386356589002648695436231, 746), (200295064848788226593969986661048514444, 747), (200391864368352048827898091319976543571, 748), (200525350647649406579524461192298921388, 749), (200628390957749569592275403034481777165, 750), (200864859662317981403881560606736857552, 751), (201030211829544761307031642701451968787, 752), (201120384088878878047257711316960983203, 753), (201529835852079945366722321521937874700, 754), (202037828932783235051349096952964914701, 755), (202499639251361943455714769806234773061, 756), (202845477021191753873079054410839925245, 757), (202880192602065948829729524517527229192, 758), (203471890102993419881337799302806970777, 759), (203762709299731485581976830241343185058, 760), (203891384067574372697177695758559288188, 761), (204366966053027252087989850868905222016, 762), (204723723574253552184516157732800579202, 763), (204759127898602683986744200262210168599, 764), (204890017935407630392700034107524283775, 765), (204944543484659515529038412935464839325, 766), (205021592789624531841352296116819658321, 767), (205536048376424252274762056179223941704, 768), (205965681081559844536724757404109737969, 769), (206059158881617735659199798059350178568, 770), (206345371756448648687088987147550906780, 771), (206669546420807087027596601281611100142, 772), (206934192374448169756183442496183960886, 773), (206956509993563406907722361519345433250, 774), (207023151811702246147443036506257389274, 775), (207148465955494780446781428121360767107, 776), (207169193014574067406962272252615862503, 777), (207214293893785155915917821510565166536, 778), (207231865539431065281243915796582259794, 779), (207282465211418939565197502166563004635, 780), (207335189750608535793567884710927439514, 781), (207422616698663629964675455207366827536, 782), (207779156436233710434447126572261283834, 783), (208055691383255041608457803767427621946, 784), (208127521098142424462785902569416407660, 785), (208196096207106080686670602863788646590, 786), (208337248844900042959129651178683570575, 787), (208370561576414507081756431953901916563, 788), (208413658661387109912065903308747642350, 789), (209385635239731680231522375761013511940, 790), (210002532278346179969704536854498817191, 791), (210161823096146273554279044097448477252, 792), (210210698553345373511146640397719018738, 793), (210336169757648417601889525641763692803, 794), (210604758604842640130787409294401137557, 795), (210930577721872015586327458843337453239, 796), (211315040098821000989879450971324376083, 797), (211330930089876406473389619186601015829, 798), (211458916043718632503279654275311402129, 799), (211589833952788207222712380103579336100, 800), (211780030628467430622292783925391306085, 801), (212079752021327240516117801259103721656, 802), (212170748862303991392719761012163030465, 803), (212294387197888268747074637747504833239, 804), (212319313364035261094075981068842587604, 805), (212511027445031357009094021481748621174, 806), (213387033265098827570309109219920387841, 807), (213393611993795647264670212609607796124, 808), (213756722071546935593514149748980059319, 809), (213787299973693183573397738524210554753, 810), (213805352923298732773445489146982353658, 811), (213976957226507285713288344987255075299, 812), (214011037495683992019966443022060368790, 813), (214225396389151194161576886586826756729, 814), (214295960247286480910670581283760842796, 815), (214705440196301808179340266487740774097, 816), (215392479404974760724007290721922097167, 817), (216002255643196701043713366995476477399, 818), (216004295242953188924447624338780500475, 819), (216202799007552465996481700181987015318, 820), (216244705008457587076057934068027815075, 821), (216579846047953335019268952666255224949, 822), (217199415920240635665158505992323743934, 823), (218058431222656259645518775693988265452, 824), (218423460273151296301059870631971757209, 825), (218529542702282658295441105295553591652, 826), (218551911309209868129001532456400930907, 827), (218888033256262735028027037914348244857, 828), (218922484964067602525346305237892806103, 829), (219228957202792015170936396848249378370, 830), (219254076506954802084703863410220343270, 831), (219293014473934508023310043812468093990, 832), (219547927153421721085959714081563426695, 833), (219747703975822802251310611752504186265, 834), (220126637560799951172504016533878033097, 835), (220676148316316277937476749557284928695, 836), (220849822891144174460916508927993201318, 837), (220866896534633741136955174598986125745, 838), (220881174758370013237735593545156066469, 839), (220961422906133552229273209219153250022, 840), (221718563212479332830658735964598415672, 841), (221974104608730174294122926215422109278, 842), (222481498383403773869836761155661113683, 843), (223561416662763971075644793567883926503, 844), (223856625439621692409936742016433403153, 845), (223879757260255336869618507952486625344, 846), (223907723070456475900838466005500977303, 847), (223971077147655958356881874895456094757, 848), (224575064008513498204150927839893314338, 849), (224975068114119867330872996108986313485, 850), (225050677982069312692859447835828973981, 851), (225566295217051496900859555103057232246, 852), (226569281355050704277349214924662676557, 853), (226862562715670568619246004091210229556, 854), (227152357043453138319349417221274273599, 855), (227492002615484811105685943280855322526, 856), (227573024237824320095019697097658521597, 857), (227786679027306228777382498389059565322, 858), (227824492016528521054151220319551594690, 859), (228097118404786349297914625425627097538, 860), (228158784315933207685600406867583853299, 861), (228325943092667833543790481393580386207, 862), (228556000162353470427766654334050270126, 863), (228767804811325600635819377044358636618, 864), (229221838454182775721018701527074591245, 865), (229310254480003288404509443392813502285, 866), (229503627910160961776250562578086775614, 867), (229965748205986426347764913525056055404, 868), (229987232191234074600673955336881188966, 869), (230971887408458682662748996003104290743, 870), (231118284156352093542283750005168324487, 871), (231410746276494446565891933888259773039, 872), (231815206719191516315078523093370076660, 873), (232012991679893989689586807076367496562, 874), (232101906513162529001807419666093555783, 875), (232613136383816600945941155862831713906, 876), (233013269250487387400649997503725093981, 877), (233414334710877346398033311627697924357, 878), (233470345972099975051276180755340519799, 879), (233998692495480929997133889040444138614, 880), (234564122125202232593710463235984914522, 881), (235078996772265151981486999615017501649, 882), (235232277216659839140153307321423434827, 883), (235406878503937427507712590384586215182, 884), (236352342028144473490599365437218140272, 885), (236791257257452227937231046361574509041, 886), (237231560483478312621395912410050480595, 887), (237651743676232603807016897398658520700, 888), (237664701744165189752635424765623337326, 889), (237750933286261506785531231852982244955, 890), (238651472071064229184645959378981155860, 891), (238787734849883439535512358749902813821, 892), (238957150469278285757854584701455662373, 893), (239474360742407749410895312622747478149, 894), (239919414358607408156773850774093690008, 895), (240060543743334938143437018879553415718, 896), (240157558011934538667204608377966496807, 897), (240839643619631056796809498726446989667, 898), (241007784649161567843725133705600136149, 899), (241028071414275493038216849083086208528, 900), (241071561092147483152093629540728152296, 901), (241155279183486683370166225440980963849, 902), (241634991437285732079567852308787137625, 903), (242849947054604180989376863567916038101, 904), (243120814234812923303374350294167730762, 905), (243190504548097112014185643917269115848, 906), (243950209081972281873978333634650732607, 907), (244320685012087295463543254292562613845, 908), (244891303054470118894702518585648136251, 909), (244957324381860679005741533326193732434, 910), (246113800159689500144604420228381012788, 911), (246134401602228138680760426687058622809, 912), (246542844546550909003057722848555296605, 913), (246958386472652383442369343302930004178, 914), (247056839607580665123765446624817650755, 915), (247298266349659781612167284305865423043, 916), (247383475005829488909111927388157958366, 917), (247664042164161842609125847074634057781, 918), (247938964232665450177270088007516270712, 919), (247997729747003532225353992433427921928, 920), (249023723821866804473500621583209246462, 921), (249063080914980907325940922594825240529, 922), (249100803478686777862625920517546864865, 923), (249568214027194457891244075159318135923, 924), (250062022425591019088478168220016687578, 925), (250879081723093030478057518983355100566, 926), (250957242148965326354648550668544048325, 927), (251250477048494669632081978499199211986, 928), (251960698373880993213891918730316799252, 929), (252351417566227728421925040300886418233, 930), (252470951262757075969197614334059160723, 931), (252479444017457045156016289137870869944, 932), (252634664157921159998222716005436922028, 933), (252807286780374317485843114378173099881, 934), (253078514711577076754236421980249337866, 935), (253506406712112256545470743182407508165, 936), (253599214287335241527281940799972968952, 937), (254667284839734760907166316999631192587, 938), (255213209292864989053215943446381959004, 939), (255650906804600652678943077309109379963, 940), (255794637995592791115401696524387173599, 941), (256267508962055261365071043912401394324, 942), (256584937223255164107187092979106218887, 943), (256956810753729091379866603364862741560, 944), (257204125961396731399254909728444645495, 945), (257235092194476622610023491818995990065, 946), (257640707758816172180218854013201736697, 947), (258174446554570272768354444723838796636, 948), (258656613785465667045807543539106332088, 949), (258781030986431809065604158875369827777, 950), (259425568080733482153676956864242735652, 951), (259576987560791464406731712326922886327, 952), (259792220565390274175531152445009875907, 953), (259896774781581154262467630302619887569, 954), (260328321066613969558050020572225230882, 955), (260630971322041765543764239048171065541, 956), (261039685245418269756078163333014237389, 957), (261486337239787322023263316834814001791, 958), (261704201862516616364272075663525712153, 959), (262304835492200396006965473155249596484, 960), (262585032487475342489376871626978036342, 961), (263024365229634314945369191627597392878, 962), (263031385985070090282814390537197666611, 963), (263289085517377256275809318715525426017, 964), (263434121303303196583038179217547382643, 965), (263504906544783054689041900916441329080, 966), (263605210132343449355033255361427711279, 967), (263660796659334239169854586460526247223, 968), (263703647016360482181324148147051066061, 969), (263708028308088220430633019280881153970, 970), (263761915738806632547134271478336958599, 971), (264840346216416853373953249505057452695, 972), (264963787330465102723297165425172602988, 973), (264996908410921344683837322412171129797, 974), (265340293742727829964780848489109908757, 975), (265663776215930802448544681205750872319, 976), (265706118312660399860553045206059516893, 977), (265924589324350693222771563040368663814, 978), (265951508237663468257377179115588213793, 979), (265994096667884684105087796436005245334, 980), (266142950647848001369366878218364542625, 981), (266995091063196909039900465919907555013, 982), (267795004082015620639331799803086168493, 983), (267993585568444971226321988208879995313, 984), (268023690595097728805923776094519224979, 985), (268329062138687356389755236904894931070, 986), (268368607353724096343540417424073492930, 987), (268638938623217342826202646713034024233, 988), (268672883452754982706654315930401760654, 989), (268929249525427149601138692583294921974, 990), (269264970567966660068422480808076584525, 991), (269557644568247036524186410164824937501, 992), (269667475394481797275064166775664959246, 993), (269975472872119272489018322855723781688, 994), (270405421342414435642354264839666390408, 995), (270704377641235384716389772055152536674, 996), (271133193168062172324961377026187404656, 997), (271319692028836069946226769829800863884, 998), (271348009094320163836137256510058234471, 999), (271731968410984537954289813447140171299, 1000), (271841553102401327289089048948980107621, 1001), (272114860846490701627377781315367621368, 1002), (272245780540549984349986550078175945338, 1003), (272412755172171471819959563088970740745, 1004), (272715228693287988393149144575716936472, 1005), (273004651660978667633813504518879946890, 1006), (273208056332933367868751056623244671154, 1007), (273361920726058277827629139697034264873, 1008), (273671954339125738640901387279762137055, 1009), (273860430260351277316216923397932481188, 1010), (274371109103630441567190170886832707103, 1011), (274994246015349247356598295578623589612, 1012), (275341707282205032746437060409582130159, 1013), (275357787281572827632437291620253339621, 1014), (275661317470842283964248237440674866014, 1015), (275667518401081586762172047932927006036, 1016), (275845827686581905498544944369090915460, 1017), (275893228195955503421987780788863415304, 1018), (275938607819371635018953516195356366109, 1019), (276028379571282378528973379482703734254, 1020), (276380391525420305684029006664262935910, 1021), (276645544894701889481714551929301592169, 1022), (276770182008277426519612826273385813045, 1023), (276852535041057992219729865767504977123, 1024), (276911410714629944013718135435697978665, 1025), (276948414592029507381066400517432830775, 1026), (276988609023057784914822568204017149189, 1027), (277058027999004283594256416464969243868, 1028), (277475493265137111773962771794523596971, 1029), (277524531040968739218754182428974570875, 1030), (277752955318136512222751831201315064049, 1031), (278471166605058099979538214852748737616, 1032), (278728964232370558856094758717080730796, 1033), (278846435420640356805467743128993346599, 1034), (279148710886928076611640116611286499427, 1035), (279156045177364430477090920918963601210, 1036), (279981565243928436904498598740078293349, 1037), (280044441893659588774432197024808708088, 1038), (280264985585243541897296911831747029746, 1039), (280545170217305498196143247250560136971, 1040), (280592493403472536341958567659466190434, 1041), (280700663113149729028762161339974256948, 1042), (280747666895652802423493667530879327558, 1043), (281047538653819612092896872917184025675, 1044), (281112919005396802710467828127839325941, 1045), (281159371744660859825682028058058498054, 1046), (281567510564298196140149477337982788924, 1047), (282097722289652065718419379922692002150, 1048), (282267748928183707524871539564173145144, 1049), (282317566238961956703095143013623271110, 1050), (282525499862824631764639421838073640085, 1051), (282846856799080320391358417627907755885, 1052), (283557082648746370525123945023050498647, 1053), (284287839524880137753574206192799610622, 1054), (284908485471538967525120446363723888721, 1055), (285162746681553074709332419515169768936, 1056), (285493354315481456648634805060903021808, 1057), (285626806994326851284165360905942909176, 1058), (285798264120512975505497637238403326108, 1059), (285994645765820853460236866533721783503, 1060), (286189393470065301432584275174763633157, 1061), (286218085691634088390738880071014787629, 1062), (286721739085466944943452143808264045783, 1063), (286907949861841740315650167396814179171, 1064), (287501326527867360954633120423964327912, 1065), (288984630291500651547843559970652224497, 1066), (289271970389178655520123797703226720904, 1067), (289282550854914274708753320586136057868, 1068), (290003703741598249969950652126916246552, 1069), (290490325939290915539920942153979621613, 1070), (290599697687117078077079883519991249729, 1071), (290848930272345084668733544075266398203, 1072), (290897609318834791822700982167590500527, 1073), (291015938445241174650751920124203157009, 1074), (291694907522489974285637198609472791622, 1075), (291878266523536392210330463799032126706, 1076), (292127227788669607827566423229926690464, 1077), (292270702689093849232982552071509597261, 1078), (292880639352386114871311772409462878537, 1079), (292995523340201765560027745672908945118, 1080), (293221010423876037576889678749643111272, 1081), (293249788628248119065877629176745003751, 1082), (293326222353894797118515226696510537841, 1083), (293595614965428027106480955031803918278, 1084), (293634526382758335227758943085963708922, 1085), (293698657939486362915164765946434911460, 1086), (294209264130157341687814439351623070727, 1087), (294340874945588222132149198804372622943, 1088), (294717212726113354329634852289390385806, 1089), (294741518237236227165521248748283423229, 1090), (294900499995916193243080034000784911103, 1091), (295289666195845692568798790845418436986, 1092), (295843581115172673729047868952187270495, 1093), (295968877543691562634652607048130249889, 1094), (296219473456384992116258746314948378537, 1095), (296236435529475609973917656425399147462, 1096), (296285990005575890412173913550582186068, 1097), (296505721461619370842785832575971208594, 1098), (296531673349977124518561871979787629058, 1099), (296592687174687124449002509180607992211, 1100), (297255971531061897585790728081803027195, 1101), (297259103389414573837682508279050482352, 1102), (297638026612145184892253479532873700931, 1103), (297671052128646068885505815717920468406, 1104), (297694107205269557620831922064639277103, 1105), (297978339849814613916215862611786840452, 1106), (298065640497733213360680997376080155093, 1107), (298188568371482467368447550446548877604, 1108), (298384063429745914804185662553427017620, 1109), (298403531420786810745575580140670887691, 1110), (298561861750289491082862393112766806532, 1111), (298586169351010006404731304268174230608, 1112), (299115720457342463837607769655775277097, 1113), (299152453960179836616357139946271425908, 1114), (299233929111478939633574487427188135303, 1115), (299242964853474249877358156531676736909, 1116), (299290825576302608603479714578367242556, 1117), (299315778822012531450107688487031326958, 1118), (299905880398159563488427076229658390436, 1119), (299962517039775581471412640000290596132, 1120), (300168098083374753701775571602335915628, 1121), (300251234616065896360329563183886185304, 1122), (300273327580315036511792839758115865278, 1123), (300705582009673569424318243626230381313, 1124), (300776929712712521332620248231965562199, 1125), (300859409318181705886945141713245321566, 1126), (300860246524409441203300775660941265745, 1127), (300985519646198799634409642203655634984, 1128), (301330525855843930603070655206947375154, 1129), (301439981036725001929471151774534802190, 1130), (301598439117206155379723687373985565238, 1131), (302010277023593193852625537686787001515, 1132), (302065191285628908907887814429948564931, 1133), (302411062045491170831046991580275282912, 1134), (303178932750132983119164880293179873161, 1135), (303305374283682030505572537973531417228, 1136), (303571498253955639283951568828575986512, 1137), (303581824092172014834222535474251622199, 1138), (303628685055671719444696058535688593385, 1139), (303940175299446095896325564488819589568, 1140), (304758774102483401931500895498199590269, 1141), (304838554517765443159461816222403893750, 1142), (306248830216316659123741381924894639581, 1143), (306686975217695761978917457858276124923, 1144), (306728336841918717445942479278629908531, 1145), (307240841234320592466859585225579333735, 1146), (307299561270590628533695714120792889090, 1147), (307566289724243431067674761331217951941, 1148), (307641244280407967688229111428463467754, 1149), (308514774093589583987404168234104848131, 1150), (308605537509716160787829654168902026552, 1151), (308916692156622535910005639495896262260, 1152), (309239363645747323923974969570897163311, 1153), (309379576289126023945625011187270237212, 1154), (309917194231813109919344421224000951121, 1155), (310329273713074550257194737404413868675, 1156), (310460218139680686198561438776223126916, 1157), (310482660038129144951778173624750605851, 1158), (310572724820703539158380112585520576537, 1159), (310963410014965567210235828630351681410, 1160), (311749774356749019971555877846784449142, 1161), (311803617130912605526622359925586500007, 1162), (312010008190322043433695229691320163493, 1163), (312051604852874240423049707175684417752, 1164), (312370291488396588504939230820903468172, 1165), (312486958623182711735189769163487086790, 1166), (312667257402458950677717686276865749922, 1167), (312684074238552744217863304824478016141, 1168), (312784121649327128785569519759442778132, 1169), (313168383410534700356713436471846108551, 1170), (313221999509846117240566444605493847357, 1171), (313589233313470676383360552374782978588, 1172), (313702907334878972763897881099500101051, 1173), (313916025683613115049824153718105587751, 1174), (314169378068212994673593100422012387422, 1175), (314921550218063396836261236168522526362, 1176), (315070106282546461292197045838083523208, 1177), (315377856818674014800912035614177641964, 1178), (315581142386207976986230344583623834630, 1179), (315870296626323001388306611399031681777, 1180), (316428500232873607311936534326830248677, 1181), (316517030333634002784751536245539324870, 1182), (316893476999456618382160472234101917352, 1183), (317180347023597897535812560276420084088, 1184), (317255870777156518900280546943838285672, 1185), (317528709690160307968026934251344061392, 1186), (317636531022707196123282664336696434513, 1187), (317956669412832270023729638088341683588, 1188), (318002389260585779528561113026487339660, 1189), (318162625084734258422320841946093973518, 1190), (318386206657613260199755193047174028957, 1191), (318484131303332915593329796383197509362, 1192), (318638304426585262565629460704815912108, 1193), (319416128266826498759528511017932589463, 1194), (319678936730835101643692560628369977379, 1195), (319723535252236149845868829170713288553, 1196), (320234395096999407887826574604370684972, 1197), (320924310645641296238911336792735571508, 1198), (321114582368202994420482209151820941452, 1199), (321282068322956258648767586251324403824, 1200), (322137346569190212443650119309966382294, 1201), (322275959979935934235475070375001257084, 1202), (322724631245950658638061133323115224045, 1203), (322909793359083879892665115649305474756, 1204), (323072674168018330123826948412625011634, 1205), (323400079499004439078297059155545961810, 1206), (323453702004776827254390483104011747236, 1207), (323581161220209274844834092265254005194, 1208), (323854983348110146362689702214398549407, 1209), (323857860104628550488646687561611289965, 1210), (323885975226683757670515788663940562365, 1211), (324136268207852431412647348137390929422, 1212), (324402143554933173571677231499134487675, 1213), (324530430836450365609613422974055523449, 1214), (324553322162484066427548851125926290586, 1215), (324553664938763639917965112366058556460, 1216), (324850758072200031672355197637963617180, 1217), (324957361311646441768397567989516391775, 1218), (325064572588466579210405351458581121536, 1219), (325321329613053386563494057414342748631, 1220), (326810407027479278638392935754474570673, 1221), (327065528284406717604005418784226824450, 1222), (327392809678421378258624686965104272594, 1223), (327413151632098066866301759629223898316, 1224), (327572462162362459557442298822230855357, 1225), (327601390870995889121637096570893154092, 1226), (328121345790612507119564637951567544711, 1227), (328134627160810882540148983657612718776, 1228), (328453948310549380693690586777989534845, 1229), (329099924106499593160498660496152343811, 1230), (329114569268219188012227375809825433867, 1231), (329250038876779734611461432868847121295, 1232), (329314413275006738470399068739867936358, 1233), (329444335153276432366000920518409223721, 1234), (329540225070064468493670805073842587698, 1235), (329557571776231750797833275860617313183, 1236), (329827454163806658756838866722128210629, 1237), (330379717033737509498853332521476799629, 1238), (330443618735767902350884997122319979026, 1239), (331071568380387431324812347850149643951, 1240), (331581823610503059151090514614764377311, 1241), (332358115038404376348085784978410240929, 1242), (332420234031205213851164482536921180832, 1243), (332443552836084278290313568187691083723, 1244), (332953319590244703722542497961811734996, 1245), (333169567210699261065387926710138162160, 1246), (333295420807233555596673872318151684422, 1247), (333599685143232401393992235129363760178, 1248), (333852036357758140649141785498772033634, 1249), (334215588656985789124162513961489041144, 1250), (334227135040813940748177359244823270235, 1251), (334677271053751078025683937140317071702, 1252), (334903595095728454956358737583848613708, 1253), (334954598612686747461120155356277828200, 1254), (335182210067145000002967936075720349975, 1255), (335474626364818922312532602008144649539, 1256), (336092017061116528138066926437456558546, 1257), (336265796030465049092733591599634724755, 1258), (336378693539280238497235263372066153695, 1259), (336647382488904072687511717680965215688, 1260), (336835307820889881322731134366384298213, 1261), (337385950577568419900149795784173039487, 1262), (337476755644501960291119682674731820415, 1263), (337963790447752752004354764608691349995, 1264), (338138222456827404075080813832406598482, 1265), (338264782329977687170958699839450552096, 1266), (339594807813001075953509530458313117036, 1267), (339684387791204403366561119928721048505, 1268), (339878973812157678282311437362834343328, 1269), (339897710402582650530805392711916917090, 1270), (339942552838912229037506679985856391827, 1271)]