(* Generated with the command below from commit cd13dd0e984a4eeadd82e0ac4ce792c275bd3b18
   [dune exec ./generate_ark.exe 8 56 3 52435875175126190479447740508185965837690552500527637822603658699938581184513 NomadicLabs] *)

let v =
  [|
    "51466596801245350172389236854912648222719187746298709105513845567941180611585";
    "21750751762978437653936573013155607200736969558902465208523342419237410586198";
    "12486517768781903523286807847370218034689963995541894791925792444351839473647";
    "20445718088460789875962943176961386089719184042145123661083866290956184640219";
    "27873160203424299876666416455237485949282512273439804047040763657322096149056";
    "41356063063918478660008355287283031045994439439052675999621074603564345282569";
    "39339901461669097862513996312696398098463519178491001542393778258774347097156";
    "9204042589329629203508256352213922752007565761246017599071231880772962888313";
    "44872792620396140616818721079703154415798612187578057809815607666928058754777";
    "15937726977018206908966109373834056579034465379649731865901151172854062328666";
    "23605712034497375740219228439343452998072299839093594319857450624289690266228";
    "6402638958817972947806346954920050102512724107777426591914400080844084499349";
    "3185239264644999224390913018332891687143438328474986546082170376396564918303";
    "8810128481422180179093610800905689707749830921384041843188605671660723745224";
    "23856254368860098877925830552890800356559853619873956523749705505858453741419";
    "24587049159258135725439557767222187037564112044982562605667614163816312730472";
    "22837536766890438293232796017074642678223630893636795777506185541273623237047";
    "9192015516308615812149895996678356120602200776491327365416854885711899134185";
    "4002652916865493677251257166117182479501804845054999793592382685603350748223";
    "33066348252219459468552045146523238597048287748451612668563453612283148717787";
    "22032405802641325275844419284045173476338377422793990841002770933934147271753";
    "40810499016480900907962993830032852958946905562531549979714594924288595159449";
    "11360048753112901991330610389408512769078774607723790648797196048769123341818";
    "31073120699274505130875191050788584204810084807427992815212547386082177411939";
    "38905424489726634595807315824887707754301482341060164517868666848234609856296";
    "16437589687938886598993201288686198745024640875414943299079721648754955896524";
    "9246415141807177921760679831767807305667023086044867913825908258624135672402";
    "43267134335847210508826260454424281515957785150826503791438907274325277067689";
    "47405994765042204778087426457971662098880376129631959037220571890293893837627";
    "51109501544539159334717344833663305202169784719089645141283241708762847921831";
    "28367352686904931835510258483164340654232741901091990185726515423922311395266";
    "49750106362878302307560487257360445042628424171940583005315598767946030678175";
    "45959469784902653889236043731939532829295000363517367441618551318205534438835";
    "27018375398598043392768159138944903620978890067620474698695220978535490993662";
    "37680060127197925845671480407334293104013784691230898581176604640776871595820";
    "10072365749347322273683640976003223868449058525371389769456254873788829510856";
    "5776958426313577264021166002700070711779258526703552908022966622941040975486";
    "2052552766687385987890760301444512953288614090851121718631539540584797743813";
    "29589973335212398499653074528975769763663217998670026908669929887809390254086";
    "47176517056998440790693968750261830775359488909857950144871025285282622331205";
    "4044841108655017183998683299702141262167457310115051178539772996106040315055";
    "23145769961882962007007503964681965122021931165884937363089732236563915279899";
    "7603705117156652453963281055927587143772971225944827219299824918233735396544";
    "678587461188445034628596985861476825212606316443632929982806452029635142763";
    "43358198653600383869329744766691886425670686115842008451706594321104589073353";
    "29783989749004381558893964246285207519677877370947641650381151227672399441258";
    "46788814117768703246098518443423934593855222525287642802070140820481989754464";
    "47667240567568953271881931068585333300960463653436442752666537199724542862209";
    "36185825409915459203448245743109969343193138020188742950229819419575178293681";
    "10268626031678681962519788038923114866365639923373751230918298280203944789089";
    "22423180878570467317830579782624040309181433514468470079452795926252301501451";
    "27854213599947523969400957712485981554578482677686500615005910306191690675548";
    "32552238758912415934584820719305968737837410579067602670579118065160652867044";
    "27524020150199858721583983985008046355789957344374031640804833804334599991125";
    "11598691035533751109698164453612171297192910953856758972631340412485692367245";
    "19240281692025919244580609351663678384250073443852130798436970816624877123792";
    "19081743524319516787728673230184684387616956386482784328031473187929184929813";
    "13482824733237717061443533817612030042881142888904695925365483772570662398419";
    "24557586779364722370887646696339785224219486745231704250023468368642112077961";
    "49132695885737549819731989839786719093658647324506783818463101428078920152339";
    "47598003338017334595631291432676651103981450315484662200923020856309789617505";
    "29657580775158274893108525946918168971159316368647847989798236676167226124425";
    "2089871173039090298283861039787654594553968107879556266696645874401027551594";
    "17062674176584193145991964541286296980632589397952567044305875706903816798918";
    "39759050960205479940159986279409353005846424612008117451162722701140967479478";
    "22533616828186323521649895181466155821530425549183373709986149684843468562921";
    "11710329771453525931280127059748492796905639784050357470339844149929022650252";
    "28382230089609321965313624834250197889691846195285335974753263997326737343307";
    "17483468269617424580234048407267881623433885539437967900597355348779845904370";
    "15393678108977111939937458813237466536883800502542016725609655847312425800060";
    "35335672469945182745009570081451366206953223954844817103347451918365408472583";
    "18485543557533557196522038987860777539645907448847172084578647917456309932838";
    "35453109551100805378496992884404555281031142908343718145992408005796255932067";
    "26162388899534531304185889785161995414351042512495564813598387581820788701274";
    "30513272868498004256565910019709317337704607470343755267516092336967857454429";
    "7482438077715696595671300257575441576458965352889636767368860652528296466835";
    "4420972756750713378268292139245553512010082345332818480344347760992140415579";
    "45443072118542869094106210430408632401658283491040846320908484790994846489479";
    "4587498519897850005501095589592009810295823998176500983502979737014704428427";
    "20140268669484747984769809200637802968551617462409085249909344252279198873265";
    "29246773006012167464394782413277073922652993569428539217341804135677142314734";
    "2090453766635748262896094182234431405487694916721156619151573559829565285658";
    "28154797511075990999067437210883725325588221412791352016549710458849851400443";
    "7437576051454980648324143413673447321627481635285743115910231258907952681902";
    "47849325109234284589063376275405356989691773872687047237532536232042052359483";
    "12480987611376364480590099596287568108053904335043512585655935306753098846056";
    "35282772152784155873872416038091486728018085424598473101796189937824691931982";
    "44644309599357388823648910637703362148932670809274055496007925095230623381923";
    "40669859985254288073391010054507859022800795198091698303895855303568474914724";
    "49443653278257139506363224578511517450965492260748531903735461532886298470324";
    "28151927370999705099548977210331844092002690574491843105417307465011218883372";
    "1645107825636563552234056692699842524648459238860722695243162269478817742307";
    "20451009040028965353495911802150535366781462589345362185312598771266505204706";
    "27819682514111647266735378995664843430901566567232355462928465778589146617300";
    "9554102125843498587844759244118187314040788045621020914785690475852459244712";
    "19166777550065260996957117606165528594010042113228133002376856047908024628860";
    "26933579719124735456146556120749918059938219375765953757687070745926421730690";
    "43664899352313137143462906778788854871017052765412139294077435721003011363428";
    "36173458814979531375880943417934798141032455281648386700864729797402421147643";
    "11182517313384645430276258135181995604973901045769946685233925860600679925400";
    "18957585496621103259998572202861039692818169581041076732942953590132787413185";
    "990272065387976234207571590743065697998566272630425704533408985373371347703";
    "4566865954002478217870742631824891308061027453183663472158387320791808636718";
    "13275080024861611833879690760787568594881779009163813547717517171800075477326";
    "18280289328587924651942995072338785526297904605272226018248763384856128538194";
    "37393719051038483957290231134622753224758957341736360150179478705995454183736";
    "35471769041551236267108986169916522221022951796087962631717489467967242728989";
    "18313615850921029128115249415256953514199920171298188893865360820700589880640";
    "8649505551495013773478550513798423370916587725243242103915932173300802613836";
    "29426595573001164623970767658482684730540336753851606403197168017465308935012";
    "15800050789941506886367343947552537811144738254935176866599264324633404561668";
    "2388599729796011963372654009792156200311446590133223685676648683498130023426";
    "39710359146943858258478963255479846071237665235335480449874571631729609456656";
    "12539354052138844839668649494440055311612800274194314682724519322900896888667";
    "34775703808689652205221353219074769424059692664878491357308664495453361798542";
    "16602078529355937689782643082006360605957411241022465529030420514355243740084";
    "20279850236027730246187137397861434992518721949131469477063849268012331913542";
    "20700406847766119075096991790226756382972208779794861885683190244345925948772";
    "10767548586122669600841175107605340206307369812479898137983203022752955229420";
    "33780485917217277294437000521052335973598541648381872358473220524753392579944";
    "26053477836690449767759260916263153231466698419416254714069016291032716493795";
    "51075719579296898046678332991810264442802867440545970415662411469944202971572";
    "44425065795172674272025431261784423304992373196100933574446818463450861237636";
    "21673427825228648696679367470878911746787913779734335379612724957949663438503";
    "39500036723407342733895180253912956707996173847799994738506003893694134507820";
    "18814390742264124557923083818518430926773544077233525827507879093955534745943";
    "33285136419882565391925060802949863649369447257963104257237128389534667335431";
    "7242824697084765204242498009056108554791055701454269759053340822841847843590";
    "31173248312673499793759274086904799638353536404479301039538892557122201869326";
    "31186133094427811821728441124091409602329280228993044467507339271468902426067";
    "25737910716320624211587760844165755540380223663083209047341376780006952817951";
    "41007486903540773766178646801963663835738017272207371664092100665995867447476";
    "33733614421653704619906981612465553433605639878071728634533669588152171336923";
    "44508002187727655261274038726582531821774653664912931880913651223618478524203";
    "29308206009053294442851242412693308913204908282227130202504576346803290538114";
    "37195044959073314994498067496758410674853446343706809704471573374824766240756";
    "27750290920151880266415654177442693344449343287594569254432923001134909857161";
    "15765188586172333129026261765507777427830002956246082548695725135386026089531";
    "1723567911352974656239983052419150859691079784042460780666277969900550546629";
    "32624380698163043349452348170080919066187676495607088889037247382764371823304";
    "42332347907545864823851740450059178607636354773434217763190376183475294814740";
    "32851187296571784166842016235453193261263026420621113443940941911613891853263";
    "46515450218610398244495734725817662625773300495752440637456039809680716524335";
    "48802434618714806701215020572358407402163910104929505500552346872970874445024";
    "15041030433764412988626541831537854311766371887970954109236962491586466599144";
    "24914207471851043784197436527940466212674042052967065649457499415892446136159";
    "9071888319763577380151443506898914744736366395870413605185856133895174517345";
    "14324407136483074978482942921602872905704673210914714962854893980450386451889";
    "29042406409942557018444189727617456411092110677398829954434968404039936168367";
    "45298132425441112218235385216467264374863717020516284112024948473015955374084";
    "5848266257013307529285399749765616739303579930676051972945621978827280728485";
    "50258542824814649118248459254788489871100732773736051031417014804244168803608";
    "2211331518382464997157173039326358398024782525487574099479995890254668498248";
    "25495625009683093041292487489064498029388757676050435379647316032736436019034";
    "1673456300079357795623609138015785582077169647352697470259283949067483430156";
    "732875001458000671533092091268384759392197266180901126140125986324726970217";
    "15937486314053418275659636264513684188072392679031027560851186610858143116536";
    "37523979262473761872442642124630377368104280370382009467506872860620420272028";
    "1463301537361190248611634113301833004506917120571380701549297040601288661632";
    "15388046866006485479772795262309796656931214897645470303116977773763549826647";
    "24820458677922696742762859449292673635627885851532245057181102097543570979209";
    "42204379350085294410776773079715228191662735656426212256162333812793552403993";
    "1195814176795714164840835333744966813414161441324551406851397366147530373686";
    "16761973517502055324144398018035682278752429331149035356778515867109688520079";
    "5794935406580257517632452299232288835369749493148532249516641371649010994761";
    "28489054235450115341655557856812811692903805568161190542887091508558194202484";
    "46027667092982098207528356294714952530753544394086856091550981466630371723227";
    "36549545461270844973100848885411892468389487357334958172813302441582453767995";
    "27730798985447029088568033769773024804917434212093202895074054132301610442265";
    "30053494660111523933577748614419372203999341521131288200082766152193752930915";
    "42669519840379176591693261573919152190190830699417113996773900230897690941207";
    "40491463463369636128381274334600090418795787105664137021554873372325496120497";
    "37855317198077808209359933009653152621140711928666934200968394018548493650684";
    "30289339203582770465154470558134566153982220926251521920946038335272057457401";
    "27778690140622310321003540914723670899734999136798303644913768708258653156597";
    "3973394156719142858738591330892034076809261304074876595400530436577715032673";
    "34101414891901169069858357639409485174940075127343413252072373211617833012486";
    "24763874711353584430968413634679742313122411936945926412259875031351381484206";
    "36482519855965638025925823411871352935082631497149119671124638993468289313858";
    "33663960240182462215313666658229034428117630528389633368925326911863733915779";
    "24156616496917756781377614606496469046971000527652456728186486373912788616012";
    "17862377433968409862537980143869608526991820954912158743675488121333401401128";
    "9883166492675772730546061809268489723031153354700278026721716994418744028520";
    "651720966810612228203754272949951577724164458606405611640617175537862475287";
    "45029571820041579599811835408905235857907197206303946042784264756752149312055";
    "15218138019507525985285504884751281493313515412230279354014712290617793064643";
    "7889502179901137713876340968057633612399550484642109442993286207350478652780";
    "51114781021375925510384757787309929484526957562759351412663650152039538436129";
    "49153605396638540179308253872425727518164881509781489770081628829948751933325";
    "39446436805473057234521273352946756590838723177719005850741347955181052035907";
    "32522116151199401996556140465344290516461661003004520182401454275644784968841";
    "35709586671485611381280332540710898003892567989895109778435218770617343891091";
  |]