//! This file is auto-generated by HACL*. #![allow(non_snake_case)] #![allow(non_upper_case_globals)] #![allow(non_camel_case_types)] #![allow(unused_assignments)] #![allow(unreachable_patterns)] pub(crate) const precomp_basepoint_table_w4: [u64; 192] = [ 0u64, 0u64, 0u64, 0u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 0u64, 0u64, 0u64, 0u64, 8784043285714375740u64, 8483257759279461889u64, 8789745728267363600u64, 1770019616739251654u64, 15992936863339206154u64, 10037038012062884956u64, 15197544864945402661u64, 9615747158586711429u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 10634854829044225757u64, 351552716085025155u64, 10645315080955407736u64, 3609262091244858135u64, 15760741698986874125u64, 14936374388219697827u64, 15751360096993017895u64, 18012233706239762398u64, 1993877568177495041u64, 10345888787846536528u64, 7746511691117935375u64, 14517043990409914413u64, 14122549297570634151u64, 16934610359517083771u64, 5724511325497097418u64, 8983432969107448705u64, 2687429970334080245u64, 16525396802810050288u64, 7602596488871585854u64, 4813919589149203084u64, 7680395813780804519u64, 6687709583048023590u64, 18086445169104142027u64, 9637814708330203929u64, 14785108459960679090u64, 3838023279095023581u64, 3555615526157830307u64, 5177066488380472871u64, 18218186719108038403u64, 16281556341699656105u64, 1524227924561461191u64, 4148060517641909597u64, 2858290374115363433u64, 8942772026334130620u64, 3034451298319885113u64, 8447866036736640940u64, 11204933433076256578u64, 18333595740249588297u64, 8259597024804538246u64, 9539734295777539786u64, 9797290423046626413u64, 5777303437849646537u64, 8739356909899132020u64, 14815960973766782158u64, 15286581798204509801u64, 17597362577777019682u64, 13259283710820519742u64, 10501322996899164670u64, 1221138904338319642u64, 14586685489551951885u64, 895326705426031212u64, 14398171728560617847u64, 9592550823745097391u64, 17240998489162206026u64, 8085479283308189196u64, 14844657737893882826u64, 15923425394150618234u64, 2997808084773249525u64, 494323555453660587u64, 1215695327517794764u64, 9476207381098391690u64, 7480789678419122995u64, 15212230329321082489u64, 436189395349576388u64, 17377474396456660834u64, 15237013929655017939u64, 11444428846883781676u64, 5112749694521428575u64, 950829367509872073u64, 17665036182057559519u64, 17205133339690002313u64, 16233765170251334549u64, 10122775683257972591u64, 3352514236455632420u64, 9143148522359954691u64, 601191684005658860u64, 13398772186646349998u64, 15512696600132928431u64, 9128416073728948653u64, 11233051033546138578u64, 6769345682610122833u64, 10823233224575054288u64, 9997725227559980175u64, 6733425642852897415u64, 16302206918151466066u64, 1669330822143265921u64, 2661645605036546002u64, 17182558479745802165u64, 1165082692376932040u64, 9470595929011488359u64, 6142147329285324932u64, 4829075085998111287u64, 10231370681107338930u64, 9591876895322495239u64, 10316468561384076618u64, 11592503647238064235u64, 13395813606055179632u64, 511127033980815508u64, 12434976573147649880u64, 3425094795384359127u64, 6816971736303023445u64, 15444670609021139344u64, 9464349818322082360u64, 16178216413042376883u64, 9595540370774317348u64, 7229365182662875710u64, 4601177649460012843u64, 5455046447382487090u64, 10854066421606187521u64, 15913416821879788071u64, 2297365362023460173u64, 2603252216454941350u64, 6768791943870490934u64, 15705936687122754810u64, 9537096567546600694u64, 17580538144855035062u64, 4496542856965746638u64, 8444341625922124942u64, 12191263903636183168u64, 17427332907535974165u64, 14307569739254103736u64, 13900598742063266169u64, 7176996424355977650u64, 5709008170379717479u64, 14471312052264549092u64, 1464519909491759867u64, 3328154641049602121u64, 13020349337171136774u64, 2772166279972051938u64, 10854476939425975292u64, 1967189930534630940u64, 2802919076529341959u64, 14792226094833519208u64, 14675640928566522177u64, 14838974364643800837u64, 17631460696099549980u64, 17434186275364935469u64, 2665648200587705473u64, 13202122464492564051u64, 7576287350918073341u64, 2272206013910186424u64, 14558761641743937843u64, 5675729149929979729u64, 9043135187561613166u64, 11750149293830589225u64, 740555197954307911u64, 9871738005087190699u64, 17178667634283502053u64, 18046255991533013265u64, 4458222096988430430u64, 8452427758526311627u64, 13825286929656615266u64, 13956286357198391218u64, 15875692916799995079u64, 10634895319157013920u64, 13230116118036304207u64, 8795317393614625606u64, 7001710806858862020u64, 7949746088586183478u64, 14677556044923602317u64, 11184023437485843904u64, 11215864722023085094u64, 6444464081471519014u64, 1706241174022415217u64, 8243975633057550613u64, 15502902453836085864u64, 3799182188594003953u64, 3538840175098724094u64, ]; pub(crate) const precomp_g_pow2_64_table_w4: [u64; 192] = [ 0u64, 0u64, 0u64, 0u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 0u64, 0u64, 0u64, 0u64, 1499621593102562565u64, 16692369783039433128u64, 15337520135922861848u64, 5455737214495366228u64, 17827017231032529600u64, 12413621606240782649u64, 2290483008028286132u64, 15752017553340844820u64, 4846430910634234874u64, 10861682798464583253u64, 15404737222404363049u64, 363586619281562022u64, 9866710912401645115u64, 1162548847543228595u64, 7649967190445130486u64, 5212340432230915749u64, 7572620550182916491u64, 14876145112448665096u64, 2063227348838176167u64, 3519435548295415847u64, 8390400282019023103u64, 17666843593163037841u64, 9450204148816496323u64, 8483374507652916768u64, 6254661047265818424u64, 16382127809582285023u64, 125359443771153172u64, 1374336701588437897u64, 11362596098420127726u64, 2101654420738681387u64, 12772780342444840510u64, 12546934328908550060u64, 8331880412333790397u64, 11687262051473819904u64, 8926848496503457587u64, 9603974142010467857u64, 13199952163826973175u64, 2189856264898797734u64, 11356074861870267226u64, 2027714896422561895u64, 5261606367808050149u64, 153855954337762312u64, 6375919692894573986u64, 12364041207536146533u64, 1891896010455057160u64, 1568123795087313171u64, 18138710056556660101u64, 6004886947510047736u64, 4811859325589542932u64, 3618763430148954981u64, 11434521746258554122u64, 10086341535864049427u64, 8073421629570399570u64, 12680586148814729338u64, 9619958020761569612u64, 15827203580658384478u64, 12832694810937550406u64, 14977975484447400910u64, 5478002389061063653u64, 14731136312639060880u64, 4317867687275472033u64, 6642650962855259884u64, 2514254944289495285u64, 14231405641534478436u64, 4045448346091518946u64, 8985477013445972471u64, 8869039454457032149u64, 4356978486208692970u64, 10805288613335538577u64, 12832353127812502042u64, 4576590051676547490u64, 6728053735138655107u64, 17814206719173206184u64, 79790138573994940u64, 17920293215101822267u64, 13422026625585728864u64, 5018058010492547271u64, 110232326023384102u64, 10834264070056942976u64, 15222249086119088588u64, 15119439519142044997u64, 11655511970063167313u64, 1614477029450566107u64, 3619322817271059794u64, 9352862040415412867u64, 14017522553242747074u64, 13138513643674040327u64, 3610195242889455765u64, 8371069193996567291u64, 12670227996544662654u64, 1205961025092146303u64, 13106709934003962112u64, 4350113471327723407u64, 15060941403739680459u64, 13639127647823205030u64, 10790943339357725715u64, 498760574280648264u64, 17922071907832082887u64, 15122670976670152145u64, 6275027991110214322u64, 7250912847491816402u64, 15206617260142982380u64, 3385668313694152877u64, 17522479771766801905u64, 2965919117476170655u64, 1553238516603269404u64, 5820770015631050991u64, 4999445222232605348u64, 9245650860833717444u64, 1508811811724230728u64, 5190684913765614385u64, 15692927070934536166u64, 12981978499190500902u64, 5143491963193394698u64, 7705698092144084129u64, 581120653055084783u64, 13886552864486459714u64, 6290301270652587255u64, 8663431529954393128u64, 17033405846475472443u64, 5206780355442651635u64, 12580364474736467688u64, 17934601912005283310u64, 15119491731028933652u64, 17848231399859044858u64, 4427673319524919329u64, 2673607337074368008u64, 14034876464294699949u64, 10938948975420813697u64, 15202340615298669183u64, 5496603454069431071u64, 2486526142064906845u64, 4507882119510526802u64, 13888151172411390059u64, 15049027856908071726u64, 9667231543181973158u64, 6406671575277563202u64, 3395801050331215139u64, 9813607433539108308u64, 2681417728820980381u64, 18407064643927113994u64, 7707177692113485527u64, 14218149384635317074u64, 3658668346206375919u64, 15404713991002362166u64, 10152074687696195207u64, 10926946599582128139u64, 16907298600007085320u64, 16544287219664720279u64, 11007075933432813205u64, 8652245965145713599u64, 7857626748965990384u64, 5602306604520095870u64, 2525139243938658618u64, 14405696176872077447u64, 18432270482137885332u64, 9913880809120071177u64, 16896141737831216972u64, 7484791498211214829u64, 15635259968266497469u64, 8495118537612215624u64, 4915477980562575356u64, 16453519279754924350u64, 14462108244565406969u64, 14837837755237096687u64, 14130171078892575346u64, 15423793222528491497u64, 5460399262075036084u64, 16085440580308415349u64, 26873200736954488u64, 5603655807457499550u64, 3342202915871129617u64, 1604413932150236626u64, 9684226585089458974u64, 1213229904006618539u64, 6782978662408837236u64, 11197029877749307372u64, 14085968786551657744u64, 17352273610494009342u64, 7876582961192434984u64, ]; pub(crate) const precomp_g_pow2_128_table_w4: [u64; 192] = [ 0u64, 0u64, 0u64, 0u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 0u64, 0u64, 0u64, 0u64, 14619254753077084366u64, 13913835116514008593u64, 15060744674088488145u64, 17668414598203068685u64, 10761169236902342334u64, 15467027479157446221u64, 14989185522423469618u64, 14354539272510107003u64, 14298211796392133693u64, 13270323784253711450u64, 13380964971965046957u64, 8686204248456909699u64, 17434630286744937066u64, 1355903775279084720u64, 7554695053550308662u64, 11354971222741863570u64, 564601613420749879u64, 8466325837259054896u64, 10752965181772434263u64, 11405876547368426319u64, 13791894568738930940u64, 8230587134406354675u64, 12415514098722758608u64, 18414183046995786744u64, 15508000368227372870u64, 5781062464627999307u64, 15339429052219195590u64, 16038703753810741903u64, 9587718938298980714u64, 4822658817952386407u64, 1376351024833260660u64, 1120174910554766702u64, 1730170933262569274u64, 5187428548444533500u64, 16242053503368957131u64, 3036811119519868279u64, 1760267587958926638u64, 170244572981065185u64, 8063080791967388171u64, 4824892826607692737u64, 16286391083472040552u64, 11945158615253358747u64, 14096887760410224200u64, 1613720831904557039u64, 14316966673761197523u64, 17411006201485445341u64, 8112301506943158801u64, 2069889233927989984u64, 10082848378277483927u64, 3609691194454404430u64, 6110437205371933689u64, 9769135977342231601u64, 11977962151783386478u64, 18088718692559983573u64, 11741637975753055u64, 11110390325701582190u64, 1341402251566067019u64, 3028229550849726478u64, 10438984083997451310u64, 12730851885100145709u64, 11524169532089894189u64, 4523375903229602674u64, 2028602258037385622u64, 17082839063089388410u64, 6103921364634113167u64, 17066180888225306102u64, 11395680486707876195u64, 10952892272443345484u64, 8792831960605859401u64, 14194485427742325139u64, 15146020821144305250u64, 1654766014957123343u64, 7955526243090948551u64, 3989277566080493308u64, 12229385116397931231u64, 13430548930727025562u64, 3434892688179800602u64, 8431998794645622027u64, 12132530981596299272u64, 2289461608863966999u64, 18345870950201487179u64, 13517947207801901576u64, 5213113244172561159u64, 17632986594098340879u64, 4405251818133148856u64, 11783009269435447793u64, 9332138983770046035u64, 12863411548922539505u64, 3717030292816178224u64, 10026078446427137374u64, 11167295326594317220u64, 12425328773141588668u64, 5760335125172049352u64, 9016843701117277863u64, 5657892835694680172u64, 11025130589305387464u64, 1368484957977406173u64, 17361351345281258834u64, 1907113641956152700u64, 16439233413531427752u64, 5893322296986588932u64, 14000206906171746627u64, 14979266987545792900u64, 6926291766898221120u64, 7162023296083360752u64, 14762747553625382529u64, 12610831658612406849u64, 10462926899548715515u64, 4794017723140405312u64, 5234438200490163319u64, 8019519110339576320u64, 7194604241290530100u64, 12626770134810813246u64, 10793074474236419890u64, 11323224347913978783u64, 16831128015895380245u64, 18323094195124693378u64, 2361097165281567692u64, 15755578675014279498u64, 14289876470325854580u64, 12856787656093616839u64, 3578928531243900594u64, 3847532758790503699u64, 8377953190224748743u64, 3314546646092744596u64, 800810188859334358u64, 4626344124229343596u64, 6620381605850876621u64, 11422073570955989527u64, 12676813626484814469u64, 16725029886764122240u64, 16648497372773830008u64, 9135702594931291048u64, 16080949688826680333u64, 11528096561346602947u64, 2632498067099740984u64, 11583842699108800714u64, 8378404864573610526u64, 1076560261627788534u64, 13836015994325032828u64, 11234295937817067909u64, 5893659808396722708u64, 11277421142886984364u64, 8968549037166726491u64, 14841374331394032822u64, 9967344773947889341u64, 8799244393578496085u64, 5094686877301601410u64, 8780316747074726862u64, 9119697306829835718u64, 15381243327921855368u64, 2686250164449435196u64, 16466917280442198358u64, 13791704489163125216u64, 16955859337117924272u64, 17112836394923783642u64, 4639176427338618063u64, 16770029310141094964u64, 11049953922966416185u64, 12012669590884098968u64, 4859326885929417214u64, 896380084392586061u64, 7153028362977034008u64, 10540021163316263301u64, 9318277998512936585u64, 18344496977694796523u64, 11374737400567645494u64, 17158800051138212954u64, 18343197867863253153u64, 18204799297967861226u64, 15798973531606348828u64, 9870158263408310459u64, 17578869832774612627u64, 8395748875822696932u64, 15310679007370670872u64, 11205576736030808860u64, 10123429210002838967u64, 5910544144088393959u64, 14016615653353687369u64, 11191676704772957822u64, ]; pub(crate) const precomp_g_pow2_192_table_w4: [u64; 192] = [ 0u64, 0u64, 0u64, 0u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 0u64, 0u64, 0u64, 0u64, 7870395003430845958u64, 18001862936410067720u64, 8006461232116967215u64, 5921313779532424762u64, 10702113371959864307u64, 8070517410642379879u64, 7139806720777708306u64, 8253938546650739833u64, 17490482834545705718u64, 1065249776797037500u64, 5018258455937968775u64, 14100621120178668337u64, 8392845221328116213u64, 14630296398338540788u64, 4268947906723414372u64, 9231207002243517909u64, 14261219637616504262u64, 7786881626982345356u64, 11412720751765882139u64, 14119585051365330009u64, 15281626286521302128u64, 6350171933454266732u64, 16559468304937127866u64, 13200760478271693417u64, 6733381546280350776u64, 3801404890075189193u64, 2741036364686993903u64, 3218612940540174008u64, 10894914335165419505u64, 11862941430149998362u64, 4223151729402839584u64, 2913215088487087887u64, 14562168920104952953u64, 2170089393468287453u64, 10520900655016579352u64, 7040362608949989273u64, 8376510559381705307u64, 9142237200448131532u64, 5696859948123854080u64, 925422306716081180u64, 11155545953469186421u64, 1888208646862572812u64, 11151095998248845721u64, 15793503271680275267u64, 7729877044494854851u64, 6235134673193032913u64, 7364280682182401564u64, 5479679373325519985u64, 17966037684582301763u64, 14140891609330279185u64, 5814744449740463867u64, 5652588426712591652u64, 774745682988690912u64, 13228255573220500373u64, 11949122068786859397u64, 8021166392900770376u64, 7994323710948720063u64, 9924618472877849977u64, 17618517523141194266u64, 2750424097794401714u64, 15481749570715253207u64, 14646964509921760497u64, 1037442848094301355u64, 6295995947389299132u64, 16915049722317579514u64, 10493877400992990313u64, 18391008753060553521u64, 483942209623707598u64, 2017775662838016613u64, 5933251998459363553u64, 11789135019970707407u64, 5484123723153268336u64, 13246954648848484954u64, 4774374393926023505u64, 14863995618704457336u64, 13220153167104973625u64, 5988445485312390826u64, 17580359464028944682u64, 7297100131969874771u64, 379931507867989375u64, 10927113096513421444u64, 17688881974428340857u64, 4259872578781463333u64, 8573076295966784472u64, 16389829450727275032u64, 1667243868963568259u64, 17730726848925960919u64, 11408899874569778008u64, 3576527582023272268u64, 16492920640224231656u64, 7906130545972460130u64, 13878604278207681266u64, 41446695125652041u64, 8891615271337333503u64, 2594537723613594470u64, 7699579176995770924u64, 147458463055730655u64, 12120406862739088406u64, 12044892493010567063u64, 8554076749615475136u64, 1005097692260929999u64, 2687202654471188715u64, 9457588752176879209u64, 17472884880062444019u64, 9792097892056020166u64, 2525246678512797150u64, 15958903035313115662u64, 11336038170342247032u64, 11560342382835141123u64, 6212009033479929024u64, 8214308203775021229u64, 8475469210070503698u64, 13287024123485719563u64, 12956951963817520723u64, 10693035819908470465u64, 11375478788224786725u64, 16934625208487120398u64, 10094585729115874495u64, 2763884524395905776u64, 13535890148969964883u64, 13514657411765064358u64, 9903074440788027562u64, 17324720726421199990u64, 2273931039117368789u64, 3442641041506157854u64, 1119853641236409612u64, 12037070344296077989u64, 581736433335671746u64, 6019150647054369174u64, 14864096138068789375u64, 6652995210998318662u64, 12773883697029175304u64, 12751275631451845119u64, 11449095003038250478u64, 1025805267334366480u64, 2764432500300815015u64, 18274564429002844381u64, 10445634195592600351u64, 11814099592837202735u64, 5006796893679120289u64, 6908397253997261914u64, 13266696965302879279u64, 7768715053015037430u64, 3569923738654785686u64, 5844853453464857549u64, 1837340805629559110u64, 1034657624388283114u64, 711244516069456460u64, 12519286026957934814u64, 2613464944620837619u64, 10003023321338286213u64, 7291332092642881376u64, 9832199564117004897u64, 3280736694860799890u64, 6416452202849179874u64, 7326961381798642069u64, 8435688798040635029u64, 16630141263910982958u64, 17222635514422533318u64, 9482787389178881499u64, 836561194658263905u64, 3405319043337616649u64, 2786146577568026518u64, 7625483685691626321u64, 6728084875304656716u64, 1140997959232544268u64, 12847384827606303792u64, 1719121337754572070u64, 12863589482936438532u64, 3880712899640530862u64, 2748456882813671564u64, 4775988900044623019u64, 8937847374382191162u64, 3767367347172252295u64, 13468672401049388646u64, 14359032216842397576u64, 2002555958685443975u64, 16488678606651526810u64, 11826135409597474760u64, 15296495673182508601u64, ]; pub(crate) const precomp_basepoint_table_w5: [u64; 384] = [ 0u64, 0u64, 0u64, 0u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 0u64, 0u64, 0u64, 0u64, 8784043285714375740u64, 8483257759279461889u64, 8789745728267363600u64, 1770019616739251654u64, 15992936863339206154u64, 10037038012062884956u64, 15197544864945402661u64, 9615747158586711429u64, 1u64, 18446744069414584320u64, 18446744073709551615u64, 4294967294u64, 10634854829044225757u64, 351552716085025155u64, 10645315080955407736u64, 3609262091244858135u64, 15760741698986874125u64, 14936374388219697827u64, 15751360096993017895u64, 18012233706239762398u64, 1993877568177495041u64, 10345888787846536528u64, 7746511691117935375u64, 14517043990409914413u64, 14122549297570634151u64, 16934610359517083771u64, 5724511325497097418u64, 8983432969107448705u64, 2687429970334080245u64, 16525396802810050288u64, 7602596488871585854u64, 4813919589149203084u64, 7680395813780804519u64, 6687709583048023590u64, 18086445169104142027u64, 9637814708330203929u64, 14785108459960679090u64, 3838023279095023581u64, 3555615526157830307u64, 5177066488380472871u64, 18218186719108038403u64, 16281556341699656105u64, 1524227924561461191u64, 4148060517641909597u64, 2858290374115363433u64, 8942772026334130620u64, 3034451298319885113u64, 8447866036736640940u64, 11204933433076256578u64, 18333595740249588297u64, 8259597024804538246u64, 9539734295777539786u64, 9797290423046626413u64, 5777303437849646537u64, 8739356909899132020u64, 14815960973766782158u64, 15286581798204509801u64, 17597362577777019682u64, 13259283710820519742u64, 10501322996899164670u64, 1221138904338319642u64, 14586685489551951885u64, 895326705426031212u64, 14398171728560617847u64, 9592550823745097391u64, 17240998489162206026u64, 8085479283308189196u64, 14844657737893882826u64, 15923425394150618234u64, 2997808084773249525u64, 494323555453660587u64, 1215695327517794764u64, 9476207381098391690u64, 7480789678419122995u64, 15212230329321082489u64, 436189395349576388u64, 17377474396456660834u64, 15237013929655017939u64, 11444428846883781676u64, 5112749694521428575u64, 950829367509872073u64, 17665036182057559519u64, 17205133339690002313u64, 16233765170251334549u64, 10122775683257972591u64, 3352514236455632420u64, 9143148522359954691u64, 601191684005658860u64, 13398772186646349998u64, 15512696600132928431u64, 9128416073728948653u64, 11233051033546138578u64, 6769345682610122833u64, 10823233224575054288u64, 9997725227559980175u64, 6733425642852897415u64, 16302206918151466066u64, 1669330822143265921u64, 2661645605036546002u64, 17182558479745802165u64, 1165082692376932040u64, 9470595929011488359u64, 6142147329285324932u64, 4829075085998111287u64, 10231370681107338930u64, 9591876895322495239u64, 10316468561384076618u64, 11592503647238064235u64, 13395813606055179632u64, 511127033980815508u64, 12434976573147649880u64, 3425094795384359127u64, 6816971736303023445u64, 15444670609021139344u64, 9464349818322082360u64, 16178216413042376883u64, 9595540370774317348u64, 7229365182662875710u64, 4601177649460012843u64, 5455046447382487090u64, 10854066421606187521u64, 15913416821879788071u64, 2297365362023460173u64, 2603252216454941350u64, 6768791943870490934u64, 15705936687122754810u64, 9537096567546600694u64, 17580538144855035062u64, 4496542856965746638u64, 8444341625922124942u64, 12191263903636183168u64, 17427332907535974165u64, 14307569739254103736u64, 13900598742063266169u64, 7176996424355977650u64, 5709008170379717479u64, 14471312052264549092u64, 1464519909491759867u64, 3328154641049602121u64, 13020349337171136774u64, 2772166279972051938u64, 10854476939425975292u64, 1967189930534630940u64, 2802919076529341959u64, 14792226094833519208u64, 14675640928566522177u64, 14838974364643800837u64, 17631460696099549980u64, 17434186275364935469u64, 2665648200587705473u64, 13202122464492564051u64, 7576287350918073341u64, 2272206013910186424u64, 14558761641743937843u64, 5675729149929979729u64, 9043135187561613166u64, 11750149293830589225u64, 740555197954307911u64, 9871738005087190699u64, 17178667634283502053u64, 18046255991533013265u64, 4458222096988430430u64, 8452427758526311627u64, 13825286929656615266u64, 13956286357198391218u64, 15875692916799995079u64, 10634895319157013920u64, 13230116118036304207u64, 8795317393614625606u64, 7001710806858862020u64, 7949746088586183478u64, 14677556044923602317u64, 11184023437485843904u64, 11215864722023085094u64, 6444464081471519014u64, 1706241174022415217u64, 8243975633057550613u64, 15502902453836085864u64, 3799182188594003953u64, 3538840175098724094u64, 13240193491554624643u64, 12365034249541329920u64, 2924326828590977357u64, 5687195797140589099u64, 16880427227292834531u64, 9691471435758991112u64, 16642385273732487288u64, 12173806747523009914u64, 13142722756877876849u64, 8370377548305121979u64, 17988526053752025426u64, 4818750752684100334u64, 5669241919350361655u64, 4964810303238518540u64, 16709712747671533191u64, 4461414404267448242u64, 3971798785139504238u64, 6276818948740422136u64, 1426735892164275762u64, 7943622674892418919u64, 9864274225563929680u64, 57815533745003233u64, 10893588105168960233u64, 15739162732907069535u64, 3923866849462073470u64, 12279826158399226875u64, 1533015761334846582u64, 15860156818568437510u64, 8252625373831297988u64, 9666953804812706358u64, 8767785238646914634u64, 14382179044941403551u64, 10401039907264254245u64, 8584860003763157350u64, 3120462679504470266u64, 8670255778748340069u64, 5313789577940369984u64, 16977072364454789224u64, 12199578693972188324u64, 18211098771672599237u64, 12868831556008795030u64, 5310155061431048194u64, 18114153238435112606u64, 14482365809278304512u64, 12520721662723001511u64, 405943624021143002u64, 8146944101507657423u64, 181739317780393495u64, 81743892273670099u64, 14759561962550473930u64, 4592623849546992939u64, 6916440441743449719u64, 1304610503530809833u64, 5464930909232486441u64, 15414883617496224671u64, 8129283345256790u64, 18294252198413739489u64, 17394115281884857288u64, 7808348415224731235u64, 13195566655747230608u64, 8568194219353949094u64, 15329813048672122440u64, 9604275495885785744u64, 1577712551205219835u64, 15964209008022052790u64, 15087297920782098160u64, 3946031512438511898u64, 10050061168984440631u64, 11382452014533138316u64, 6313670788911952792u64, 12015989229696164014u64, 5946702628076168852u64, 5219995658774362841u64, 12230141881068377972u64, 12361195202673441956u64, 4732862275653856711u64, 17221430380805252370u64, 15397525953897375810u64, 16557437297239563045u64, 10101683801868971351u64, 1402611372245592868u64, 1931806383735563658u64, 10991705207471512479u64, 861333583207471392u64, 15207766844626322355u64, 9224628129811432393u64, 3497069567089055613u64, 11956632757898590316u64, 8733729372586312960u64, 18091521051714930927u64, 77582787724373283u64, 9922437373519669237u64, 3079321456325704615u64, 12171198408512478457u64, 17179130884012147596u64, 6839115479620367181u64, 4421032569964105406u64, 10353331468657256053u64, 17400988720335968824u64, 17138855889417480540u64, 4507980080381370611u64, 10703175719793781886u64, 12598516658725890426u64, 8353463412173898932u64, 17703029389228422404u64, 9313111267107226233u64, 5441322942995154196u64, 8952817660034465484u64, 17571113341183703118u64, 7375087953801067019u64, 13381466302076453648u64, 3218165271423914596u64, 16956372157249382685u64, 509080090049418841u64, 13374233893294084913u64, 2988537624204297086u64, 4979195832939384620u64, 3803931594068976394u64, 10731535883829627646u64, 12954845047607194278u64, 10494298062560667399u64, 4967351022190213065u64, 13391917938145756456u64, 951370484866918160u64, 13531334179067685307u64, 12868421357919390599u64, 15918857042998130258u64, 17769743831936974016u64, 7137921979260368809u64, 12461369180685892062u64, 827476514081935199u64, 15107282134224767230u64, 10084765752802805748u64, 3303739059392464407u64, 17859532612136591428u64, 10949414770405040164u64, 12838613589371008785u64, 5554397169231540728u64, 18375114572169624408u64, 15649286703242390139u64, 2957281557463706877u64, 14000350446219393213u64, 14355199721749620351u64, 2730856240099299695u64, 17528131000714705752u64, 2537498525883536360u64, 6121058967084509393u64, 16897667060435514221u64, 12367869599571112440u64, 3388831797050807508u64, 16791449724090982798u64, 2673426123453294928u64, 11369313542384405846u64, 15641960333586432634u64, 15080962589658958379u64, 7747943772340226569u64, 8075023376199159152u64, 8485093027378306528u64, 13503706844122243648u64, 8401961362938086226u64, 8125426002124226402u64, 9005399361407785203u64, 6847968030066906634u64, 11934937736309295197u64, 5116750888594772351u64, 2817039227179245227u64, 17724206901239332980u64, 4985702708254058578u64, 5786345435756642871u64, 17772527414940936938u64, 1201320251272957006u64, 15787430120324348129u64, 6305488781359965661u64, 12423900845502858433u64, 17485949424202277720u64, 2062237315546855852u64, 10353639467860902375u64, 2315398490451287299u64, 15394572894814882621u64, 232866113801165640u64, 7413443736109338926u64, 902719806551551191u64, 16568853118619045174u64, 14202214862428279177u64, 11719595395278861192u64, 5890053236389907647u64, 9996196494965833627u64, 12967056942364782577u64, 9034128755157395787u64, 17898204904710512655u64, 8229373445062993977u64, 13580036169519833644u64, ];