let data = [
(mk_real_int64 593577076514247969L),(mk_real_int64 428680505437969320L);(* 17, 17 *)
(mk_real_int64 115148850047821254L),(mk_real_int64 400625175641427675L);(* 17, 17 *)
(mk_real_int64 267559796243890150L),(mk_real_int64 136412146185955315L);(* 17, 17 *)
(mk_real_int64 297040999931329479L),(mk_real_int64 29825072577377098L);(* 17, 16 *)
(mk_real_int64 858357628464932527L),(mk_real_int64 213035687964967841L);(* 17, 17 *)
(mk_real_int64 692780235444750948L),(mk_real_int64 32361101103141920L);(* 17, 16 *)
(mk_real_int64 368368415358674470L),(mk_real_int64 642250206775142145L);(* 17, 17 *)
(mk_real_int64 44352225921124639L),(mk_real_int64 84828703199977545L);(* 16, 16 *)
(mk_real_int64 293767468923358080L),(mk_real_int64 490354811484381388L);(* 17, 17 *)
(mk_real_int64 11580401050568952L),(mk_real_int64 328542995430032790L);(* 16, 17 *)
(mk_real_int64 361658680742465480L),(mk_real_int64 32529200157013252L);(* 17, 16 *)
(mk_real_int64 720930266342781826L),(mk_real_int64 154152718338301010L);(* 17, 17 *)
(mk_real_int64 32494575670377125L),(mk_real_int64 294730722590458680L);(* 16, 17 *)
(mk_real_int64 302457425920251063L),(mk_real_int64 171171393669591983L);(* 17, 17 *)
(mk_real_int64 607014172489591917L),(mk_real_int64 583373694158955503L);(* 17, 17 *)
(mk_real_int64 136475059390012953L),(mk_real_int64 802638546348782037L);(* 17, 17 *)
(mk_real_int64 72604157973643010L),(mk_real_int64 109591660960474693L);(* 16, 17 *)
(mk_real_int64 181227586211215124L),(mk_real_int64 481352555272347506L);(* 17, 17 *)
(mk_real_int64 469409098050003981L),(mk_real_int64 81703500828888114L);(* 17, 16 *)
(mk_real_int64 523818167442188320L),(mk_real_int64 113624381071366665L);(* 17, 17 *)
(mk_real_int64 90176144567500932L),(mk_real_int64 176029278330009456L);(* 16, 17 *)
(mk_real_int64 314312111378233182L),(mk_real_int64 674468900005789776L);(* 17, 17 *)
(mk_real_int64 606735181438351267L),(mk_real_int64 276571488323597520L);(* 17, 17 *)
(mk_real_int64 346812068985741636L),(mk_real_int64 95360777077860000L);(* 17, 16 *)
(mk_real_int64 182600518690968273L),(mk_real_int64 12804250058753183L);(* 17, 16 *)
(mk_real_int64 432891753125152496L),(mk_real_int64 584777428468571058L);(* 17, 17 *)
(mk_real_int64 205562116747747041L),(mk_real_int64 59876458977379590L);(* 17, 16 *)
(mk_real_int64 63764679139133024L),(mk_real_int64 15949346321153958L);(* 16, 16 *)
(mk_real_int64 581232493658172982L),(mk_real_int64 72640184426663042L);(* 17, 16 *)
(mk_real_int64 386144941881660951L),(mk_real_int64 139340247736797800L);(* 17, 17 *)
(mk_real_int64 1834399628878245L),(mk_real_int64 52992453560315558L);(* 15, 16 *)
(mk_real_int64 198554588400482100L),(mk_real_int64 947856141299473804L);(* 17, 17 *)
(mk_real_int64 202372079351488772L),(mk_real_int64 142006166408538738L);(* 17, 17 *)
(mk_real_int64 30304525036039896L),(mk_real_int64 139176746068147216L);(* 16, 17 *)
(mk_real_int64 518986357192159120L),(mk_real_int64 77320061352118746L);(* 17, 16 *)
(mk_real_int64 375108279078092640L),(mk_real_int64 91443459108583337L);(* 17, 16 *)
(mk_real_int64 511138638300269448L),(mk_real_int64 390345752646113160L);(* 17, 17 *)
(mk_real_int64 31881316669604122L),(mk_real_int64 152733592195099581L);(* 16, 17 *)
(mk_real_int64 567048714070888293L),(mk_real_int64 16727242942719006L);(* 17, 16 *)
(mk_real_int64 478646606294174545L),(mk_real_int64 333567474600622906L);(* 17, 17 *)
(mk_real_int64 75387897831759795L),(mk_real_int64 79902574033969975L);(* 16, 16 *)
(mk_real_int64 522789246229386240L),(mk_real_int64 318113105262331938L);(* 17, 17 *)
(mk_real_int64 668821765419722550L),(mk_real_int64 19441889042953960L);(* 17, 16 *)
(mk_real_int64 224969149043018168L),(mk_real_int64 15506915245560675L);(* 17, 16 *)
(mk_real_int64 34727842856539638L),(mk_real_int64 201587350012327084L);(* 16, 17 *)
(mk_real_int64 7718212768683318L),(mk_real_int64 165334157732744532L);(* 15, 17 *)
(mk_real_int64 27022496088630661L),(mk_real_int64 490555087105277608L);(* 16, 17 *)
(mk_real_int64 16761546396004295L),(mk_real_int64 181893596499823404L);(* 16, 17 *)
(mk_real_int64 568493999054889740L),(mk_real_int64 250322347468258725L);(* 17, 17 *)
(mk_real_int64 409886520928385886L),(mk_real_int64 861977709480663750L);(* 17, 17 *)
(mk_real_int64 33750615705282585L),(mk_real_int64 159909611686283128L);(* 16, 17 *)
(mk_real_int64 480873536374793258L),(mk_real_int64 403545250580123214L);(* 17, 17 *)
(mk_real_int64 349475323501652400L),(mk_real_int64 23133548472456150L);(* 17, 16 *)
(mk_real_int64 23620501525765480L),(mk_real_int64 288620016849006140L);(* 16, 17 *)
(mk_real_int64 81211034886982776L),(mk_real_int64 189853068631257952L);(* 16, 17 *)
(mk_real_int64 81499790593513080L),(mk_real_int64 366681427710683904L);(* 16, 17 *)
(mk_real_int64 7949818594636644L),(mk_real_int64 85408420777383152L);(* 15, 16 *)
(mk_real_int64 634197005289549405L),(mk_real_int64 166272832722748360L);(* 17, 17 *)
(mk_real_int64 125534262847858460L),(mk_real_int64 173882194745925094L);(* 17, 17 *)
(mk_real_int64 313544292480479458L),(mk_real_int64 117964910018325792L);(* 17, 17 *)
(mk_real_int64 243412030980796347L),(mk_real_int64 1114044407758268L);(* 17, 15 *)
(mk_real_int64 945851299305824814L),(mk_real_int64 121355180105389626L);(* 17, 17 *)
(mk_real_int64 17425681026832232L),(mk_real_int64 6879176136108735L);(* 16, 15 *)
(mk_real_int64 74689563565062600L),(mk_real_int64 539732462100269320L);(* 16, 17 *)
(mk_real_int64 138450201815611932L),(mk_real_int64 719635337454146616L);(* 17, 17 *)
(mk_real_int64 405826054742195052L),(mk_real_int64 369653802612391780L);(* 17, 17 *)
(mk_real_int64 264941710677584820L),(mk_real_int64 276274772473447181L);(* 17, 17 *)
(mk_real_int64 608326901916297575L),(mk_real_int64 55961604681412362L);(* 17, 16 *)
(mk_real_int64 865000774650459200L),(mk_real_int64 74262523934704434L);(* 17, 16 *)
(mk_real_int64 1113644835197622L),(mk_real_int64 254920014998145330L);(* 15, 17 *)
(mk_real_int64 281529665999463664L),(mk_real_int64 409018730295274792L);(* 17, 17 *)
(mk_real_int64 449001186656439960L),(mk_real_int64 85121853080698102L);(* 17, 16 *)
(mk_real_int64 350852999189380512L),(mk_real_int64 78636991734309096L);(* 17, 16 *)
(mk_real_int64 368395200123333808L),(mk_real_int64 310945489396631454L);(* 17, 17 *)
(mk_real_int64 28888194000980283L),(mk_real_int64 135767904078146136L);(* 16, 17 *)
(mk_real_int64 272781364443450000L),(mk_real_int64 372972681985485166L);(* 17, 17 *)
(mk_real_int64 44395895538852856L),(mk_real_int64 102649825639854575L);(* 16, 17 *)
(mk_real_int64 394896429705037512L),(mk_real_int64 9936393940485474L);(* 17, 15 *)
(mk_real_int64 260779687734248416L),(mk_real_int64 121536563662906003L);(* 17, 17 *)
(mk_real_int64 34126573183279535L),(mk_real_int64 504032628076773540L);(* 16, 17 *)
(mk_real_int64 67481169086988228L),(mk_real_int64 5789790942269693L);(* 16, 15 *)
(mk_real_int64 247158371534520459L),(mk_real_int64 436729323378602020L);(* 17, 17 *)
(mk_real_int64 192355602867232522L),(mk_real_int64 805220047814808805L);(* 17, 17 *)
(mk_real_int64 418400998477857558L),(mk_real_int64 300752070718209408L);(* 17, 17 *)
(mk_real_int64 167901300044116480L),(mk_real_int64 163721723802592360L);(* 17, 17 *)
(mk_real_int64 279595990657022535L),(mk_real_int64 559691791891692600L);(* 17, 17 *)
(mk_real_int64 272947776810709350L),(mk_real_int64 233192394156385458L);(* 17, 17 *)
(mk_real_int64 373028763761464980L),(mk_real_int64 197169279973814285L);(* 17, 17 *)
(mk_real_int64 447973625558312610L),(mk_real_int64 257275865559752575L);(* 17, 17 *)
(mk_real_int64 162751268632080996L),(mk_real_int64 49158816079191705L);(* 17, 16 *)
(mk_real_int64 362434068641894216L),(mk_real_int64 327116761013379216L);(* 17, 17 *)
(mk_real_int64 597068501739285535L),(mk_real_int64 12241898397071550L);(* 17, 16 *)
(mk_real_int64 391006093467659481L),(mk_real_int64 465699562690802953L);(* 17, 17 *)
(mk_real_int64 207152321072355911L),(mk_real_int64 223755720965302032L);(* 17, 17 *)
(mk_real_int64 53733848653588300L),(mk_real_int64 530662923876621125L);(* 16, 17 *)
(mk_real_int64 76523313269231895L),(mk_real_int64 9717215647913124L);(* 16, 15 *)
(mk_real_int64 35807129585941770L),(mk_real_int64 11311388289769568L);(* 16, 16 *)
(mk_real_int64 296596702614925752L),(mk_real_int64 192721070270345436L);(* 17, 17 *)
(mk_real_int64 18289220989301220L),(mk_real_int64 645933272672277888L);(* 16, 17 *)
(mk_real_int64 181377626984399430L),(mk_real_int64 21658451652450692L);(* 17, 16 *)
(mk_real_int64 103869686343254018L),(mk_real_int64 604754777331707829L);(* 17, 17 *)
(mk_real_int64 91635169822009996L),(mk_real_int64 12485624993411737L);(* 16, 16 *)
(mk_real_int64 172953434924303243L),(mk_real_int64 252696236796920210L);(* 17, 17 *)
(mk_real_int64 153134968640597414L),(mk_real_int64 13789298656558605L);(* 17, 16 *)
(mk_real_int64 396845123478383840L),(mk_real_int64 270159836959960593L);(* 17, 17 *)
(mk_real_int64 38980695007353333L),(mk_real_int64 23522944404051840L);(* 16, 16 *)
(mk_real_int64 269394527747421920L),(mk_real_int64 494966004413881960L);(* 17, 17 *)
(mk_real_int64 252749377141810745L),(mk_real_int64 354581938043061988L);(* 17, 17 *)
(mk_real_int64 371001846228785592L),(mk_real_int64 474034906819971389L);(* 17, 17 *)
(mk_real_int64 176070144108119300L),(mk_real_int64 539906586098534991L);(* 17, 17 *)
(mk_real_int64 51632118105881364L),(mk_real_int64 88091229914334960L);(* 16, 16 *)
(mk_real_int64 428143100748513234L),(mk_real_int64 397120188117104316L);(* 17, 17 *)
(mk_real_int64 35292113095600632L),(mk_real_int64 307514352857007765L);(* 16, 17 *)
(mk_real_int64 393491271648668697L),(mk_real_int64 62937123177410860L);(* 17, 16 *)
(mk_real_int64 683812585302996812L),(mk_real_int64 45449088773707160L);(* 17, 16 *)
(mk_real_int64 236455448093063344L),(mk_real_int64 766942110506460591L);(* 17, 17 *)
(mk_real_int64 95646258873971960L),(mk_real_int64 196263107194503972L);(* 16, 17 *)
(mk_real_int64 196544078903723040L),(mk_real_int64 111499757545873270L);(* 17, 17 *)
(mk_real_int64 657753565991728392L),(mk_real_int64 294974608343260340L);(* 17, 17 *)
(mk_real_int64 227725097514624255L),(mk_real_int64 24845876191717988L);(* 17, 16 *)
(mk_real_int64 711427827948594624L),(mk_real_int64 536975540302481448L);(* 17, 17 *)
(mk_real_int64 198634711104299430L),(mk_real_int64 251619941516349532L);(* 17, 17 *)
(mk_real_int64 535658038560687174L),(mk_real_int64 36855341637391728L);(* 17, 16 *)
(mk_real_int64 7527954595002825L),(mk_real_int64 578297599242777180L);(* 15, 17 *)
(mk_real_int64 143935275495457800L),(mk_real_int64 501315176991445116L);(* 17, 17 *)
(mk_real_int64 42312215579068512L),(mk_real_int64 291745732504001760L);(* 16, 17 *)
(mk_real_int64 4376044718667753L),(mk_real_int64 12498334937909835L);(* 15, 16 *)
(mk_real_int64 190202776130624240L),(mk_real_int64 317076479065475838L);(* 17, 17 *)
(mk_real_int64 440538805958922063L),(mk_real_int64 893034731045406807L);(* 17, 17 *)
(mk_real_int64 680165557303656460L),(mk_real_int64 478236709963851762L);(* 17, 17 *)
(mk_real_int64 37049082325054749L),(mk_real_int64 421176144561881446L);(* 16, 17 *)
(mk_real_int64 299105370770375661L),(mk_real_int64 85425107536710292L);(* 17, 16 *)
(mk_real_int64 67433391948385890L),(mk_real_int64 156219513133267969L);(* 16, 17 *)
(mk_real_int64 229251953226132586L),(mk_real_int64 349874996308937495L);(* 17, 17 *)
(mk_real_int64 27152596689423411L),(mk_real_int64 124458308343775314L);(* 16, 17 *)
(mk_real_int64 324550243136308488L),(mk_real_int64 348621898431194546L);(* 17, 17 *)
(mk_real_int64 3404623470361015L),(mk_real_int64 208778859696372669L);(* 15, 17 *)
(mk_real_int64 71955317877020544L),(mk_real_int64 236172215821516624L);(* 16, 17 *)
(mk_real_int64 871185625987423034L),(mk_real_int64 135650618364233520L);(* 17, 17 *)
(mk_real_int64 359102803375130388L),(mk_real_int64 563540458036194819L);(* 17, 17 *)
(mk_real_int64 341715459547967820L),(mk_real_int64 109658830457248992L);(* 17, 17 *)
(mk_real_int64 59006283293639610L),(mk_real_int64 252538158661749100L);(* 16, 17 *)
(mk_real_int64 30020057115869704L),(mk_real_int64 393812864292377852L);(* 16, 17 *)
(mk_real_int64 205986414112689444L),(mk_real_int64 1159244375316120L);(* 17, 15 *)
(mk_real_int64 53799437234710998L),(mk_real_int64 449872350498821358L);(* 16, 17 *)
(mk_real_int64 560319387270645308L),(mk_real_int64 678094921304502912L);(* 17, 17 *)
(mk_real_int64 97505848669525961L),(mk_real_int64 16464827738268584L);(* 16, 16 *)
(mk_real_int64 72482493056156928L),(mk_real_int64 159053078429255120L);(* 16, 17 *)
(mk_real_int64 325101240400510274L),(mk_real_int64 92009505566696716L);(* 17, 16 *)
(mk_real_int64 23085921324146800L),(mk_real_int64 205509583682664066L);(* 16, 17 *)
(mk_real_int64 29818640585443872L),(mk_real_int64 148008669567525104L);(* 16, 17 *)
(mk_real_int64 106612038859912470L),(mk_real_int64 345760306683501828L);(* 17, 17 *)
(mk_real_int64 11184785044380255L),(mk_real_int64 130876791833643255L);(* 16, 17 *)
(mk_real_int64 273687032090948400L),(mk_real_int64 16959732329964152L);(* 17, 16 *)
(mk_real_int64 145972708563073340L),(mk_real_int64 91999379160339312L);(* 17, 16 *)
(mk_real_int64 588703340234359992L),(mk_real_int64 145457586545942504L);(* 17, 17 *)
(mk_real_int64 222088761109606600L),(mk_real_int64 40920521901355395L);(* 17, 16 *)
(mk_real_int64 122950554769918735L),(mk_real_int64 216120054808213164L);(* 17, 17 *)
(mk_real_int64 745110061683934584L),(mk_real_int64 503809707130100304L);(* 17, 17 *)
(mk_real_int64 361418581471626432L),(mk_real_int64 479760028542834996L);(* 17, 17 *)
(mk_real_int64 64047583705729632L),(mk_real_int64 109159068275009612L);(* 16, 17 *)
(mk_real_int64 222251373766624006L),(mk_real_int64 779288998712127207L);(* 17, 17 *)
(mk_real_int64 24738894062152611L),(mk_real_int64 59472745302516150L);(* 16, 16 *)
(mk_real_int64 115488616195994680L),(mk_real_int64 252784105965486576L);(* 17, 17 *)
(mk_real_int64 342500018982039072L),(mk_real_int64 320764335449866614L);(* 17, 17 *)
(mk_real_int64 7536670133451927L),(mk_real_int64 60339530795479360L);(* 15, 16 *)
(mk_real_int64 51036410965356257L),(mk_real_int64 203102254067186208L);(* 16, 17 *)
(mk_real_int64 5073267793058696L),(mk_real_int64 716946310451578680L);(* 15, 17 *)
(mk_real_int64 454545788414598181L),(mk_real_int64 921283123522146L);(* 17, 14 *)
(mk_real_int64 5469369972227032L),(mk_real_int64 321992199206833638L);(* 15, 17 *)
(mk_real_int64 92531941442587572L),(mk_real_int64 29628958330353021L);(* 16, 16 *)
(mk_real_int64 55766593837271040L),(mk_real_int64 406733957429677280L);(* 16, 17 *)
(mk_real_int64 18030480689736120L),(mk_real_int64 102280659071464965L);(* 16, 17 *)
(mk_real_int64 295968148353485055L),(mk_real_int64 30333286834670495L);(* 17, 16 *)
(mk_real_int64 217914640067007856L),(mk_real_int64 668426766942359089L);(* 17, 17 *)
(mk_real_int64 386169873414707930L),(mk_real_int64 202363639892105652L);(* 17, 17 *)
(mk_real_int64 190564133398151841L),(mk_real_int64 379284879307229328L);(* 17, 17 *)
(mk_real_int64 142611111947983833L),(mk_real_int64 161347081704455680L);(* 17, 17 *)
(mk_real_int64 535995834008423700L),(mk_real_int64 62399799331398523L);(* 17, 16 *)
(mk_real_int64 95952315379167546L),(mk_real_int64 74005856147147176L);(* 16, 16 *)
(mk_real_int64 498776542144479936L),(mk_real_int64 239307031709724860L);(* 17, 17 *)
(mk_real_int64 331507016234909159L),(mk_real_int64 415088128288339002L);(* 17, 17 *)
(mk_real_int64 476480090139910838L),(mk_real_int64 310198958983844690L);(* 17, 17 *)
(mk_real_int64 10483790480830320L),(mk_real_int64 581633437425680750L);(* 16, 17 *)
(mk_real_int64 407793212755189440L),(mk_real_int64 313029237083503200L);(* 17, 17 *)
(mk_real_int64 8857688605585647L),(mk_real_int64 56349810741436078L);(* 15, 16 *)
(mk_real_int64 199741859949628314L),(mk_real_int64 244869802544418540L);(* 17, 17 *)
(mk_real_int64 61436800723215897L),(mk_real_int64 66351149466140982L);(* 16, 16 *)
(mk_real_int64 229074624892492624L),(mk_real_int64 137747323125799403L);(* 17, 17 *)
(mk_real_int64 23680724168227016L),(mk_real_int64 457064614716083922L);(* 16, 17 *)
(mk_real_int64 135922210174223886L),(mk_real_int64 35828964697400160L);(* 17, 16 *)
(mk_real_int64 168856535922700990L),(mk_real_int64 363491046369203558L);(* 17, 17 *)
(mk_real_int64 182009255609432160L),(mk_real_int64 575055304886640270L);(* 17, 17 *)
(mk_real_int64 208212541926871524L),(mk_real_int64 132146049980955479L);(* 17, 17 *)
(mk_real_int64 127332952851360306L),(mk_real_int64 235031200652394190L);(* 17, 17 *)
(mk_real_int64 9029153171294760L),(mk_real_int64 130059053128835080L);(* 15, 17 *)
(mk_real_int64 301466824069340755L),(mk_real_int64 983249445501630L);(* 17, 14 *)
(mk_real_int64 746180663030933360L),(mk_real_int64 173520366663593952L);(* 17, 17 *)
(mk_real_int64 58486989805413218L),(mk_real_int64 75514031476451645L);(* 16, 16 *)
(mk_real_int64 182438406328915145L),(mk_real_int64 451297356761033568L);(* 17, 17 *)
(mk_real_int64 13819262630206200L),(mk_real_int64 89006413325831939L);(* 16, 16 *)
(mk_real_int64 251197757828780732L),(mk_real_int64 638363789773816834L);(* 17, 17 *)
(mk_real_int64 152736915466691248L),(mk_real_int64 283619989933277007L);(* 17, 17 *)
(mk_real_int64 121130032250304168L),(mk_real_int64 37152797043406563L);(* 17, 16 *)
(mk_real_int64 263994620405030685L),(mk_real_int64 397038399465778000L);(* 17, 17 *)
(mk_real_int64 103106446127621405L),(mk_real_int64 272272732440987798L);(* 17, 17 *)
(mk_real_int64 400673537413237970L),(mk_real_int64 9263736331827680L);(* 17, 15 *)
(mk_real_int64 531614303185912005L),(mk_real_int64 195839139748123744L);(* 17, 17 *)
(mk_real_int64 305876508529382800L),(mk_real_int64 133228306938368L);(* 17, 14 *)
(mk_real_int64 812168617662155990L),(mk_real_int64 147413738255595240L);(* 17, 17 *)
(mk_real_int64 162297956943142118L),(mk_real_int64 101708348125687810L);(* 17, 17 *)
(mk_real_int64 433496891151348882L),(mk_real_int64 37694441514423550L);(* 17, 16 *)
(mk_real_int64 85473914484837970L),(mk_real_int64 106100201076501060L);(* 16, 17 *)
(mk_real_int64 81656765262615060L),(mk_real_int64 11732945262301840L);(* 16, 16 *)
(mk_real_int64 343287849250124700L),(mk_real_int64 31038832199918213L);(* 17, 16 *)
(mk_real_int64 864273540846398592L),(mk_real_int64 17528389391613380L);(* 17, 16 *)
(mk_real_int64 444581262464597L),(mk_real_int64 478513787820283827L);(* 14, 17 *)
(mk_real_int64 384798851493251446L),(mk_real_int64 44621943606777114L);(* 17, 16 *)
(mk_real_int64 60193580767447120L),(mk_real_int64 119081512917922030L);(* 16, 17 *)
(mk_real_int64 217592667270940910L),(mk_real_int64 12918587421730662L);(* 17, 16 *)
(mk_real_int64 25543856085636600L),(mk_real_int64 149411224244210577L);(* 16, 17 *)
(mk_real_int64 548685113327138700L),(mk_real_int64 132439015597735979L);(* 17, 17 *)
(mk_real_int64 50702202434371113L),(mk_real_int64 153259410432667140L);(* 16, 17 *)
(mk_real_int64 212670612297368L),(mk_real_int64 152646018772595282L);(* 14, 17 *)
(mk_real_int64 9398550639602350L),(mk_real_int64 109285038251745408L);(* 15, 17 *)
(mk_real_int64 195735175389224220L),(mk_real_int64 65909645514966045L);(* 17, 16 *)
(mk_real_int64 13050466242967296L),(mk_real_int64 294695140372941680L);(* 16, 17 *)
(mk_real_int64 322536050414181578L),(mk_real_int64 65587528251929095L);(* 17, 16 *)
(mk_real_int64 567228631900235625L),(mk_real_int64 418535050108566352L);(* 17, 17 *)
(mk_real_int64 359716527290209680L),(mk_real_int64 178680639115499444L);(* 17, 17 *)
(mk_real_int64 134675447156571436L),(mk_real_int64 239468991290438280L);(* 17, 17 *)
(mk_real_int64 52640661601250412L),(mk_real_int64 221611620347699462L);(* 16, 17 *)
(mk_real_int64 8593585849344808L),(mk_real_int64 60382316014617380L);(* 15, 16 *)
(mk_real_int64 29526377923331844L),(mk_real_int64 289346592082006684L);(* 16, 17 *)
(mk_real_int64 14900514608590758L),(mk_real_int64 38060565166686860L);(* 16, 16 *)
(mk_real_int64 2500846013626656L),(mk_real_int64 306266011514444802L);(* 15, 17 *)
(mk_real_int64 31754513352044415L),(mk_real_int64 64453635938894880L);(* 16, 16 *)
(mk_real_int64 619306183693446318L),(mk_real_int64 647265304374681980L);(* 17, 17 *)
(mk_real_int64 399783260600307683L),(mk_real_int64 1590711591338816L);(* 17, 15 *)
(mk_real_int64 38271444177252440L),(mk_real_int64 28470986909003709L);(* 16, 16 *)
(mk_real_int64 49234943667239070L),(mk_real_int64 3045316701912904L);(* 16, 15 *)
(mk_real_int64 174434346505389492L),(mk_real_int64 14214848254723970L);(* 17, 16 *)
(mk_real_int64 162102288946819670L),(mk_real_int64 158806596271052835L);(* 17, 17 *)
(mk_real_int64 44188349701310145L),(mk_real_int64 69874761950848848L);(* 16, 16 *)
(mk_real_int64 41753283518651936L),(mk_real_int64 140189930041789140L);(* 16, 17 *)
(mk_real_int64 21492823394400190L),(mk_real_int64 114357455324274742L);(* 16, 17 *)
(mk_real_int64 317122132163156460L),(mk_real_int64 32864027802422875L);(* 17, 16 *)
(mk_real_int64 269459489144852370L),(mk_real_int64 53731832959018116L);(* 17, 16 *)
(mk_real_int64 1755495090541608L),(mk_real_int64 680348411229582366L);(* 15, 17 *)
(mk_real_int64 325450714537315080L),(mk_real_int64 240701242117938732L);(* 17, 17 *)
(mk_real_int64 11675168942651088L),(mk_real_int64 180837447858264092L);(* 16, 17 *)
(mk_real_int64 199586973565389740L),(mk_real_int64 584827043267803955L);(* 17, 17 *)
(mk_real_int64 519757143929621952L),(mk_real_int64 115215000505827792L);(* 17, 17 *)
(mk_real_int64 228901291121299536L),(mk_real_int64 166107144289808995L);(* 17, 17 *)
(mk_real_int64 110256899984893960L),(mk_real_int64 94250039733365111L);(* 17, 16 *)
(mk_real_int64 20881595075859840L),(mk_real_int64 456116293043596820L);(* 16, 17 *)
(mk_real_int64 170199638014602180L),(mk_real_int64 445452794101254632L);(* 17, 17 *)
(mk_real_int64 325123249773875927L),(mk_real_int64 221694834071874800L);(* 17, 17 *)
(mk_real_int64 363111962916667852L),(mk_real_int64 356416423234506750L);(* 17, 17 *)
(mk_real_int64 326981312664076720L),(mk_real_int64 324301112702375263L);(* 17, 17 *)
(mk_real_int64 276875940729903200L),(mk_real_int64 328684337227569319L);(* 17, 17 *)
(mk_real_int64 618503564531835L),(mk_real_int64 140964281311281630L);(* 14, 17 *)
(mk_real_int64 31719442074907275L),(mk_real_int64 191497833873471395L);(* 16, 17 *)
(mk_real_int64 137156963954724970L),(mk_real_int64 330971357509405888L);(* 17, 17 *)
(mk_real_int64 72966112399229232L),(mk_real_int64 166121922852055396L);(* 16, 17 *)
(mk_real_int64 662179135599193896L),(mk_real_int64 40061468175331140L);(* 17, 16 *)
(mk_real_int64 215383144596181548L),(mk_real_int64 26648831051211425L);(* 17, 16 *)
(mk_real_int64 322173735589951960L),(mk_real_int64 242941596763714090L);(* 17, 17 *)
(mk_real_int64 363578889618560302L),(mk_real_int64 234960520082923068L);(* 17, 17 *)
(mk_real_int64 523238402390966400L),(mk_real_int64 337491466628723620L);(* 17, 17 *)
(mk_real_int64 31519314667009180L),(mk_real_int64 579841056333224751L);(* 16, 17 *)
(mk_real_int64 109017346836836304L),(mk_real_int64 32885159804207640L);(* 17, 16 *)
(mk_real_int64 185651726506320966L),(mk_real_int64 233841680895092230L);(* 17, 17 *)
(mk_real_int64 10960671338035380L),(mk_real_int64 650358741227734184L);(* 16, 17 *)
(mk_real_int64 47263468351578128L),(mk_real_int64 282792510460582857L);(* 16, 17 *)
(mk_real_int64 793549667027214839L),(mk_real_int64 88040219740318170L);(* 17, 16 *)
(mk_real_int64 335398728970647900L),(mk_real_int64 663685179874661331L);(* 17, 17 *)
(mk_real_int64 75674486248624386L),(mk_real_int64 76179155741421720L);(* 16, 16 *)
(mk_real_int64 359541162114242832L),(mk_real_int64 20546505576975352L);(* 17, 16 *)
(mk_real_int64 502159561777520892L),(mk_real_int64 23916740460208200L);(* 17, 16 *)
(mk_real_int64 464267909803572770L),(mk_real_int64 62155301715071390L);(* 17, 16 *)
(mk_real_int64 249764117659684661L),(mk_real_int64 356337950803418475L);(* 17, 17 *)
(mk_real_int64 304323019404668770L),(mk_real_int64 247135260325725250L);(* 17, 17 *)
(mk_real_int64 317142706086137318L),(mk_real_int64 146424868516807220L);(* 17, 17 *)
(mk_real_int64 246637813304621530L),(mk_real_int64 635318301473187380L);(* 17, 17 *)
(mk_real_int64 36493606281527064L),(mk_real_int64 50121185194755196L);(* 16, 16 *)
(mk_real_int64 56660129567743824L),(mk_real_int64 56737312115843232L);(* 16, 16 *)
(mk_real_int64 620408719927368558L),(mk_real_int64 617406520259732433L);(* 17, 17 *)
(mk_real_int64 11163115822194906L),(mk_real_int64 8157877628814816L);(* 16, 15 *)
(mk_real_int64 600037644342656306L),(mk_real_int64 87486818799947280L);(* 17, 16 *)
(mk_real_int64 271009067929780368L),(mk_real_int64 747585271145609402L);(* 17, 17 *)
(mk_real_int64 771840699546069900L),(mk_real_int64 588341334039643140L);(* 17, 17 *)
(mk_real_int64 106578562655071752L),(mk_real_int64 252527556390580188L);(* 17, 17 *)
(mk_real_int64 225289348505247612L),(mk_real_int64 45458350309807560L);(* 17, 16 *)
(mk_real_int64 327517597885524536L),(mk_real_int64 295769811303097549L);(* 17, 17 *)
(mk_real_int64 224947959761813248L),(mk_real_int64 81531223308189244L);(* 17, 16 *)
(mk_real_int64 9879288157918288L),(mk_real_int64 57109329090843700L);(* 15, 16 *)
(mk_real_int64 489684519570241311L),(mk_real_int64 275340445109356200L);(* 17, 17 *)
(mk_real_int64 632394256346331012L),(mk_real_int64 4109162784837390L);(* 17, 15 *)
(mk_real_int64 119116823842730074L),(mk_real_int64 585102241508406346L);(* 17, 17 *)
(mk_real_int64 124733913253405728L),(mk_real_int64 295261908438735054L);(* 17, 17 *)
(mk_real_int64 9402516412382304L),(mk_real_int64 98562126947697075L);(* 15, 16 *)
(mk_real_int64 762447903651976154L),(mk_real_int64 88954522809503782L);(* 17, 16 *)
(mk_real_int64 471644751757414580L),(mk_real_int64 50361805537691571L);(* 17, 16 *)
(mk_real_int64 754305307490470050L),(mk_real_int64 286070872467533500L);(* 17, 17 *)
(mk_real_int64 382339139599808820L),(mk_real_int64 9087528998115040L);(* 17, 15 *)
(mk_real_int64 676895764060895754L),(mk_real_int64 438302030974332110L);(* 17, 17 *)
(mk_real_int64 250734033511892091L),(mk_real_int64 379719080052221610L);(* 17, 17 *)
(mk_real_int64 135948236040499820L),(mk_real_int64 66424862932572960L);(* 17, 16 *)
(mk_real_int64 129871176710817185L),(mk_real_int64 139767848415195639L);(* 17, 17 *)
(mk_real_int64 347255803217270220L),(mk_real_int64 381062465965689541L);(* 17, 17 *)
(mk_real_int64 52478169947878215L),(mk_real_int64 131436405010956474L);(* 16, 17 *)
(mk_real_int64 180531012721495744L),(mk_real_int64 443608448341991328L);(* 17, 17 *)
(mk_real_int64 72245903238289074L),(mk_real_int64 672261464428338582L);(* 16, 17 *)
(mk_real_int64 78701102536979250L),(mk_real_int64 3310952884532885L);(* 16, 15 *)
(mk_real_int64 421245902344450932L),(mk_real_int64 69440209438615656L);(* 17, 16 *)
(mk_real_int64 156630693464266545L),(mk_real_int64 502568160881995045L);(* 17, 17 *)
(mk_real_int64 366481174077495750L),(mk_real_int64 299511852435647412L);(* 17, 17 *)
(mk_real_int64 296434880915962880L),(mk_real_int64 349324011158639472L);(* 17, 17 *)
(mk_real_int64 347788600716983184L),(mk_real_int64 391712416764112605L);(* 17, 17 *)
(mk_real_int64 130558000080487650L),(mk_real_int64 214177563933272335L);(* 17, 17 *)
(mk_real_int64 116633318688157126L),(mk_real_int64 259482392938442640L);(* 17, 17 *)
(mk_real_int64 115798391914472000L),(mk_real_int64 15911217431489028L);(* 17, 16 *)
(mk_real_int64 62865805432806312L),(mk_real_int64 11684680772064144L);(* 16, 16 *)
(mk_real_int64 12701693110122529L),(mk_real_int64 341948864526628720L);(* 16, 17 *)
(mk_real_int64 34672340426360490L),(mk_real_int64 281634089042179272L);(* 16, 17 *)
(mk_real_int64 25774146398909950L),(mk_real_int64 3733728996040600L);(* 16, 15 *)
(mk_real_int64 86985518108563089L),(mk_real_int64 64561483497787515L);(* 16, 16 *)
(mk_real_int64 290594092303558290L),(mk_real_int64 256552414995652362L);(* 17, 17 *)
(mk_real_int64 48374153671476608L),(mk_real_int64 22016447217828486L);(* 16, 16 *)
(mk_real_int64 68858913199392255L),(mk_real_int64 37337040380932204L);(* 16, 16 *)
(mk_real_int64 292733808455942300L),(mk_real_int64 432247011448038549L);(* 17, 17 *)
(mk_real_int64 225799538014044908L),(mk_real_int64 199756931403223223L);(* 17, 17 *)
(mk_real_int64 867052349059168325L),(mk_real_int64 36585750957279200L);(* 17, 16 *)
(mk_real_int64 37909515109507080L),(mk_real_int64 221731287228613719L);(* 16, 17 *)
(mk_real_int64 13429066143364650L),(mk_real_int64 245248258702886610L);(* 16, 17 *)
(mk_real_int64 184593801636927360L),(mk_real_int64 469255574233047232L);(* 17, 17 *)
(mk_real_int64 258111718919554358L),(mk_real_int64 58707802620411476L);(* 17, 16 *)
(mk_real_int64 23157823586872410L),(mk_real_int64 501770041902910566L);(* 16, 17 *)
(mk_real_int64 487638582633736487L),(mk_real_int64 9158748958960500L);(* 17, 15 *)
(mk_real_int64 242485647513638950L),(mk_real_int64 6009335672906784L);(* 17, 15 *)
(mk_real_int64 39022830127389810L),(mk_real_int64 95266812491246794L);(* 16, 16 *)
(mk_real_int64 210907209845871422L),(mk_real_int64 4505705938886544L);(* 17, 15 *)
(mk_real_int64 347388785593813725L),(mk_real_int64 92329020210157200L);(* 17, 16 *)
(mk_real_int64 19405205110530058L),(mk_real_int64 626825034770971256L);(* 16, 17 *)
(mk_real_int64 10027279149285741L),(mk_real_int64 84053163187888972L);(* 16, 16 *)
(mk_real_int64 28816660288789191L),(mk_real_int64 251663084776003450L);(* 16, 17 *)
(mk_real_int64 125366116255098600L),(mk_real_int64 65625056548741812L);(* 17, 16 *)
(mk_real_int64 1747807045623320L),(mk_real_int64 42875789802173660L);(* 15, 16 *)
(mk_real_int64 62166212445147426L),(mk_real_int64 174772598523477474L);(* 16, 17 *)
(mk_real_int64 4634504272791316L),(mk_real_int64 389218161147703956L);(* 15, 17 *)
(mk_real_int64 53118155463315404L),(mk_real_int64 204684784150231890L);(* 16, 17 *)
(mk_real_int64 188598633989126425L),(mk_real_int64 391239494720695832L);(* 17, 17 *)
(mk_real_int64 49042499816042048L),(mk_real_int64 411543903154483706L);(* 16, 17 *)
(mk_real_int64 105948106070871059L),(mk_real_int64 494971127467061028L);(* 17, 17 *)
(mk_real_int64 510411998636942381L),(mk_real_int64 4094714141895354L);(* 17, 15 *)
(mk_real_int64 102800962709287268L),(mk_real_int64 279079732365018740L);(* 17, 17 *)
(mk_real_int64 246267718419420048L),(mk_real_int64 425257460757118404L);(* 17, 17 *)
(mk_real_int64 277777553279745408L),(mk_real_int64 203886464930639937L);(* 17, 17 *)
(mk_real_int64 187762349581660620L),(mk_real_int64 489466117031376375L);(* 17, 17 *)
(mk_real_int64 104972444463237032L),(mk_real_int64 1520363773240480L);(* 17, 15 *)
(mk_real_int64 300977754901383936L),(mk_real_int64 256688257412093871L);(* 17, 17 *)
(mk_real_int64 131520776355337380L),(mk_real_int64 155728212297871099L);(* 17, 17 *)
(mk_real_int64 81226700792260128L),(mk_real_int64 253200981232851974L);(* 16, 17 *)
(mk_real_int64 439742937600173704L),(mk_real_int64 357566547063273975L);(* 17, 17 *)
(mk_real_int64 149434602909944930L),(mk_real_int64 61049175436478463L);(* 17, 16 *)
(mk_real_int64 212104290296339773L),(mk_real_int64 391710468618109840L);(* 17, 17 *)
(mk_real_int64 179478716247689800L),(mk_real_int64 44214260580503509L);(* 17, 16 *)
(mk_real_int64 452992986808639542L),(mk_real_int64 262759542547948578L);(* 17, 17 *)
(mk_real_int64 14461562773966394L),(mk_real_int64 312052038103269540L);(* 16, 17 *)
(mk_real_int64 2166951230704338L),(mk_real_int64 4242598754495763L);(* 15, 15 *)
(mk_real_int64 25483256874681012L),(mk_real_int64 312957282989132600L);(* 16, 17 *)
(mk_real_int64 266270925102595950L),(mk_real_int64 16700160707790920L);(* 17, 16 *)
(mk_real_int64 711670373430384024L),(mk_real_int64 9026168794509348L);(* 17, 15 *)
(mk_real_int64 601059720946448883L),(mk_real_int64 519743191546926731L);(* 17, 17 *)
(mk_real_int64 133699211141907465L),(mk_real_int64 347952807432327589L);(* 17, 17 *)
(mk_real_int64 99864889578374400L),(mk_real_int64 78020592391040075L);(* 16, 16 *)
(mk_real_int64 364074224072180L),(mk_real_int64 786806229974465040L);(* 14, 17 *)
(mk_real_int64 731942186003430150L),(mk_real_int64 233428789336079412L);(* 17, 17 *)
(mk_real_int64 192343093131202230L),(mk_real_int64 247411404511450864L);(* 17, 17 *)
(mk_real_int64 136851384183953712L),(mk_real_int64 650630476336004108L);(* 17, 17 *)
(mk_real_int64 355397561005550416L),(mk_real_int64 100815433997218248L);(* 17, 17 *)
(mk_real_int64 99766375486658910L),(mk_real_int64 626732031538528095L);(* 16, 17 *)
(mk_real_int64 353917875141915748L),(mk_real_int64 84092423658133878L);(* 17, 16 *)
(mk_real_int64 194495292154321126L),(mk_real_int64 9813152945288304L);(* 17, 15 *)
(mk_real_int64 860828654578504899L),(mk_real_int64 686628945523857600L);(* 17, 17 *)
(mk_real_int64 166325255123767740L),(mk_real_int64 303052090130874405L);(* 17, 17 *)
(mk_real_int64 181092365537175081L),(mk_real_int64 77965632368170866L);(* 17, 16 *)
(mk_real_int64 359699913048241872L),(mk_real_int64 308831817723027572L);(* 17, 17 *)
(mk_real_int64 15741948481811244L),(mk_real_int64 67779715077021522L);(* 16, 16 *)
(mk_real_int64 6796682935031584L),(mk_real_int64 161201192421263900L);(* 15, 17 *)
(mk_real_int64 15632966247819424L),(mk_real_int64 455350778392759451L);(* 16, 17 *)
(mk_real_int64 326891916932835888L),(mk_real_int64 755266648992100002L);(* 17, 17 *)
(mk_real_int64 186012666572402056L),(mk_real_int64 90204203006729952L);(* 17, 16 *)
(mk_real_int64 745545065773481921L),(mk_real_int64 28261683130750848L);(* 17, 16 *)
(mk_real_int64 91683597967971680L),(mk_real_int64 14758852351053330L);(* 16, 16 *)
(mk_real_int64 628044769387649985L),(mk_real_int64 24489397147014960L);(* 17, 16 *)
(mk_real_int64 195458693032701900L),(mk_real_int64 188082605425813862L);(* 17, 17 *)
(mk_real_int64 223727976987860070L),(mk_real_int64 4360332914249166L);(* 17, 15 *)
(mk_real_int64 49401604364971117L),(mk_real_int64 258748626842429085L);(* 16, 17 *)
(mk_real_int64 393278439209933820L),(mk_real_int64 100742743980640125L);(* 17, 17 *)
(mk_real_int64 191110218283001160L),(mk_real_int64 77308921537454863L);(* 17, 16 *)
(mk_real_int64 22693878678601600L),(mk_real_int64 117942525828599121L);(* 16, 17 *)
(mk_real_int64 5093296744366008L),(mk_real_int64 295810800009685701L);(* 15, 17 *)
(mk_real_int64 75456914080229280L),(mk_real_int64 341287088725970022L);(* 16, 17 *)
(mk_real_int64 193638807054800310L),(mk_real_int64 581097421202856802L);(* 17, 17 *)
(mk_real_int64 41352409989390720L),(mk_real_int64 210691788830722620L);(* 16, 17 *)
(mk_real_int64 544311083696580612L),(mk_real_int64 544257755160116340L);(* 17, 17 *)
(mk_real_int64 10268168936144398L),(mk_real_int64 12118926933488816L);(* 16, 16 *)
(mk_real_int64 371267116859843730L),(mk_real_int64 774390458911136606L);(* 17, 17 *)
(mk_real_int64 538406272662200506L),(mk_real_int64 897462746811145650L);(* 17, 17 *)
(mk_real_int64 22291454001651575L),(mk_real_int64 146072925944970990L);(* 16, 17 *)
(mk_real_int64 14654718776377708L),(mk_real_int64 148939423919324220L);(* 16, 17 *)
(mk_real_int64 70432538555545418L),(mk_real_int64 297717274758711500L);(* 16, 17 *)
(mk_real_int64 166697116771735692L),(mk_real_int64 365281182465954700L);(* 17, 17 *)
(mk_real_int64 90222334039348506L),(mk_real_int64 85208738269727616L);(* 16, 16 *)
(mk_real_int64 496111698942030003L),(mk_real_int64 18655030212288016L);(* 17, 16 *)
(mk_real_int64 230518753381871790L),(mk_real_int64 849253246116793920L);(* 17, 17 *)
(mk_real_int64 371059785357853590L),(mk_real_int64 411838448864260128L);(* 17, 17 *)
(mk_real_int64 354259460966857307L),(mk_real_int64 802128091797661893L);(* 17, 17 *)
(mk_real_int64 71337939285542040L),(mk_real_int64 498931544933022914L);(* 16, 17 *)
(mk_real_int64 53678803283507898L),(mk_real_int64 468155478728409885L);(* 16, 17 *)
(mk_real_int64 148819745765631962L),(mk_real_int64 119453894386003500L);(* 17, 17 *)
(mk_real_int64 904760984587626069L),(mk_real_int64 256027712066025540L);(* 17, 17 *)
(mk_real_int64 232065928115177948L),(mk_real_int64 114287366167416310L);(* 17, 17 *)
(mk_real_int64 152672205429483272L),(mk_real_int64 568246829396111752L);(* 17, 17 *)
(mk_real_int64 100995865086032465L),(mk_real_int64 11310524696533719L);(* 17, 16 *)
(mk_real_int64 186389799194979448L),(mk_real_int64 190753739422509921L);(* 17, 17 *)
(mk_real_int64 168829396007173080L),(mk_real_int64 595689573012885931L);(* 17, 17 *)
(mk_real_int64 210943999499709564L),(mk_real_int64 93154816133918112L);(* 17, 16 *)
(mk_real_int64 36456230028725676L),(mk_real_int64 826982409627260712L);(* 16, 17 *)
(mk_real_int64 9089121208105666L),(mk_real_int64 21226501340240667L);(* 15, 16 *)
(mk_real_int64 459161880645325198L),(mk_real_int64 12203201503937752L);(* 17, 16 *)
(mk_real_int64 142727185040516497L),(mk_real_int64 931152520204456435L);(* 17, 17 *)
(mk_real_int64 66245316686005776L),(mk_real_int64 422573665432328262L);(* 16, 17 *)
(mk_real_int64 52229806412610450L),(mk_real_int64 880120471149534330L);(* 16, 17 *)
(mk_real_int64 157169173152858810L),(mk_real_int64 207461523809505060L);(* 17, 17 *)
(mk_real_int64 130425446679672484L),(mk_real_int64 5710202329867816L);(* 17, 15 *)
(mk_real_int64 234590577474221280L),(mk_real_int64 218645118178581056L);(* 17, 17 *)
(mk_real_int64 146116789517563680L),(mk_real_int64 148724655234246813L);(* 17, 17 *)
(mk_real_int64 177210195386899408L),(mk_real_int64 707418746897103104L);(* 17, 17 *)
(mk_real_int64 696273371928173520L),(mk_real_int64 13111998616981799L);(* 17, 16 *)
(mk_real_int64 369144905073156179L),(mk_real_int64 447871769170193121L);(* 17, 17 *)
(mk_real_int64 261556580390938302L),(mk_real_int64 248652283714420680L);(* 17, 17 *)
(mk_real_int64 29129004534852180L),(mk_real_int64 165904299320848704L);(* 16, 17 *)
(mk_real_int64 356821541154757536L),(mk_real_int64 206833497379075210L);(* 17, 17 *)
(mk_real_int64 163738327735650690L),(mk_real_int64 469535868143783624L);(* 17, 17 *)
(mk_real_int64 390650133026481985L),(mk_real_int64 155080393089333915L);(* 17, 17 *)
(mk_real_int64 50404703987358414L),(mk_real_int64 356118081793979610L);(* 16, 17 *)
(mk_real_int64 32568769546106409L),(mk_real_int64 434661770518349732L);(* 16, 17 *)
(mk_real_int64 20332203202549910L),(mk_real_int64 8918688988766223L);(* 16, 15 *)
(mk_real_int64 488967417474265277L),(mk_real_int64 1965813342753946L);(* 17, 15 *)
(mk_real_int64 263663509550159264L),(mk_real_int64 16600888116415890L);(* 17, 16 *)
(mk_real_int64 84300216206278378L),(mk_real_int64 439803583284153896L);(* 16, 17 *)
(mk_real_int64 312848116933632523L),(mk_real_int64 152356748937403824L);(* 17, 17 *)
(mk_real_int64 209540559484061415L),(mk_real_int64 1551108060821646L);(* 17, 15 *)
(mk_real_int64 17386666711985491L),(mk_real_int64 294602829982765544L);(* 16, 17 *)
(mk_real_int64 484492416858935484L),(mk_real_int64 85794693728147514L);(* 17, 16 *)
(mk_real_int64 24372545287642674L),(mk_real_int64 43075206256836746L);(* 16, 16 *)
(mk_real_int64 432094512993548445L),(mk_real_int64 11551911778098185L);(* 17, 16 *)
(mk_real_int64 131418918284629968L),(mk_real_int64 76473628247266480L);(* 17, 16 *)
(mk_real_int64 152519938871818544L),(mk_real_int64 814803367645219824L);(* 17, 17 *)
(mk_real_int64 559770470213342646L),(mk_real_int64 137676242235612114L);(* 17, 17 *)
(mk_real_int64 182252539223136690L),(mk_real_int64 401793393661529955L);(* 17, 17 *)
(mk_real_int64 374666662939408515L),(mk_real_int64 122804154075680544L);(* 17, 17 *)
(mk_real_int64 56544640550303950L),(mk_real_int64 272784156676652502L);(* 16, 17 *)
(mk_real_int64 291495160776037608L),(mk_real_int64 6869634395566059L);(* 17, 15 *)
(mk_real_int64 76035179482527328L),(mk_real_int64 109154862425922936L);(* 16, 17 *)
(mk_real_int64 73507590599888720L),(mk_real_int64 151415412000890160L);(* 16, 17 *)
(mk_real_int64 12976671050689476L),(mk_real_int64 304761843656700040L);(* 16, 17 *)
(mk_real_int64 306336033537339608L),(mk_real_int64 92908961156132248L);(* 17, 16 *)
(mk_real_int64 296802536444184320L),(mk_real_int64 471595376275064076L);(* 17, 17 *)
(mk_real_int64 265248536227550008L),(mk_real_int64 485474214446145529L);(* 17, 17 *)
(mk_real_int64 317196419626351915L),(mk_real_int64 816253754302619732L);(* 17, 17 *)
(mk_real_int64 153527692971084520L),(mk_real_int64 11557641893607440L);(* 17, 16 *)
(mk_real_int64 676888268015492361L),(mk_real_int64 151831926674149920L);(* 17, 17 *)
(mk_real_int64 434172341809240414L),(mk_real_int64 725355431554870674L);(* 17, 17 *)
(mk_real_int64 136394095741712550L),(mk_real_int64 621432715517875044L);(* 17, 17 *)
(mk_real_int64 3449962333007127L),(mk_real_int64 480369999672100969L);(* 15, 17 *)
(mk_real_int64 112755219806006910L),(mk_real_int64 108458061553200753L);(* 17, 17 *)
(mk_real_int64 20425420295104110L),(mk_real_int64 235855246958106344L);(* 16, 17 *)
(mk_real_int64 336769516810671791L),(mk_real_int64 170049482258806570L);(* 17, 17 *)
(mk_real_int64 120015193102019478L),(mk_real_int64 500363097909504156L);(* 17, 17 *)
(mk_real_int64 242531186920431465L),(mk_real_int64 374889727587607920L);(* 17, 17 *)
(mk_real_int64 830990516216339322L),(mk_real_int64 44870434498250946L);(* 17, 16 *)
(mk_real_int64 437337966777932430L),(mk_real_int64 123617647681404149L);(* 17, 17 *)
(mk_real_int64 32010075175130853L),(mk_real_int64 175238622667784988L);(* 16, 17 *)
(mk_real_int64 6401180336291811L),(mk_real_int64 469413146181597156L);(* 15, 17 *)
(mk_real_int64 72225885730934367L),(mk_real_int64 100902841783165630L);(* 16, 17 *)
(mk_real_int64 555947721932368422L),(mk_real_int64 71884411384828716L);(* 17, 16 *)
(mk_real_int64 11310082851412980L),(mk_real_int64 5840806486672276L);(* 16, 15 *)
(mk_real_int64 69094491382961484L),(mk_real_int64 115089316787779656L);(* 16, 17 *)
(mk_real_int64 77474187408421716L),(mk_real_int64 198790402562268054L);(* 16, 17 *)
(mk_real_int64 114052136099710176L),(mk_real_int64 133655234207060784L);(* 17, 17 *)
(mk_real_int64 640642861755418382L),(mk_real_int64 140328667680253455L);(* 17, 17 *)
(mk_real_int64 99426032717989264L),(mk_real_int64 811459517714491071L);(* 16, 17 *)
(mk_real_int64 299388146280726874L),(mk_real_int64 56023948078244003L);(* 17, 16 *)
(mk_real_int64 14681460631173710L),(mk_real_int64 126598047592659600L);(* 16, 17 *)
(mk_real_int64 190594738453607418L),(mk_real_int64 273520413046779600L);(* 17, 17 *)
(mk_real_int64 45130834913067726L),(mk_real_int64 72922927355163648L);(* 16, 16 *)
(mk_real_int64 682524197809864560L),(mk_real_int64 11501134039783259L);(* 17, 16 *)
(mk_real_int64 261147710188142596L),(mk_real_int64 10795719052521864L);(* 17, 16 *)
(mk_real_int64 612242647351633425L),(mk_real_int64 724753581578167707L);(* 17, 17 *)
(mk_real_int64 89447031723680592L),(mk_real_int64 613575854361825712L);(* 16, 17 *)
(mk_real_int64 75221044130221610L),(mk_real_int64 62437493767215000L);(* 16, 16 *)
(mk_real_int64 122980369081653920L),(mk_real_int64 139350098640226264L);(* 17, 17 *)
(mk_real_int64 191753108742459732L),(mk_real_int64 59765304065246994L);(* 17, 16 *)
(mk_real_int64 496248375998034660L),(mk_real_int64 185976720605796741L);(* 17, 17 *)
(mk_real_int64 11663449119405014L),(mk_real_int64 220112113481034950L);(* 16, 17 *)
(mk_real_int64 90019979931442324L),(mk_real_int64 138680103047713833L);(* 16, 17 *)
(mk_real_int64 246972887627693676L),(mk_real_int64 279748763615295912L);(* 17, 17 *)
(mk_real_int64 263299358734156679L),(mk_real_int64 18700083552569724L);(* 17, 16 *)
(mk_real_int64 842713184656371184L),(mk_real_int64 222686162228646900L);(* 17, 17 *)
(mk_real_int64 60076245168859232L),(mk_real_int64 13001979270207723L);(* 16, 16 *)
(mk_real_int64 206156636493363892L),(mk_real_int64 39450170112980375L);(* 17, 16 *)
(mk_real_int64 132664093425110379L),(mk_real_int64 101833372337589640L);(* 17, 17 *)
(mk_real_int64 59624200077623463L),(mk_real_int64 225283324310008170L);(* 16, 17 *)
(mk_real_int64 350506842258682381L),(mk_real_int64 823524378783026698L);(* 17, 17 *)
(mk_real_int64 229009312730583112L),(mk_real_int64 139679788568211472L);(* 17, 17 *)
(mk_real_int64 238586586148697472L),(mk_real_int64 3438075068066610L);(* 17, 15 *)
(mk_real_int64 55181926868040362L),(mk_real_int64 564285090785712988L);(* 16, 17 *)
(mk_real_int64 228373092961359570L),(mk_real_int64 45324711403960979L);(* 17, 16 *)
(mk_real_int64 433450039566505800L),(mk_real_int64 5779814058999612L);(* 17, 15 *)
(mk_real_int64 119040428754426073L),(mk_real_int64 162608716447001550L);(* 17, 17 *)
(mk_real_int64 126543423111601348L),(mk_real_int64 26028028310115306L);(* 17, 16 *)
(mk_real_int64 63540787532674749L),(mk_real_int64 156740157883775536L);(* 16, 17 *)
(mk_real_int64 23324021500639024L),(mk_real_int64 58648466211657553L);(* 16, 16 *)
(mk_real_int64 633331026360422811L),(mk_real_int64 341101435007020383L);(* 17, 17 *)
(mk_real_int64 1600055299487659L),(mk_real_int64 51028019134901524L);(* 15, 16 *)
(mk_real_int64 485820496143072944L),(mk_real_int64 516150123043777665L);(* 17, 17 *)
(mk_real_int64 255448667625962832L),(mk_real_int64 55722623811698980L);(* 17, 16 *)
(mk_real_int64 409828665334907158L),(mk_real_int64 78246103581519040L);(* 17, 16 *)
(mk_real_int64 284837621710441948L),(mk_real_int64 752003815325565722L);(* 17, 17 *)
(mk_real_int64 602905320343796525L),(mk_real_int64 742811965071900480L);(* 17, 17 *)
(mk_real_int64 215551282196246976L),(mk_real_int64 642773295888196992L);(* 17, 17 *)
(mk_real_int64 583074379399228680L),(mk_real_int64 22867696506149583L);(* 17, 16 *)
(mk_real_int64 400906498646797560L),(mk_real_int64 243223929420077568L);(* 17, 17 *)
(mk_real_int64 908723312675275350L),(mk_real_int64 118569180727903016L);(* 17, 17 *)
(mk_real_int64 240227407007770092L),(mk_real_int64 44300934657485926L);(* 17, 16 *)
(mk_real_int64 211964822498530245L),(mk_real_int64 240061121885985300L);(* 17, 17 *)
(mk_real_int64 94930428544323606L),(mk_real_int64 234767838130868694L);(* 16, 17 *)
(mk_real_int64 99474907863353302L),(mk_real_int64 584524170084483909L);(* 16, 17 *)
(mk_real_int64 12650320854337824L),(mk_real_int64 229605112793307713L);(* 16, 17 *)
(mk_real_int64 59702192440211952L),(mk_real_int64 764342185901862036L);(* 16, 17 *)
(mk_real_int64 486763512203189298L),(mk_real_int64 444232265802732874L);(* 17, 17 *)
(mk_real_int64 253148755480914656L),(mk_real_int64 110885433291927504L);(* 17, 17 *)
(mk_real_int64 3017282624126673L),(mk_real_int64 12284946223335636L);(* 15, 16 *)
(mk_real_int64 423072048903281050L),(mk_real_int64 42369065159124920L);(* 17, 16 *)
(mk_real_int64 258213374964468434L),(mk_real_int64 622676329793374780L);(* 17, 17 *)
(mk_real_int64 261269463129805152L),(mk_real_int64 652165415334478031L);(* 17, 17 *)
(mk_real_int64 528239585152350773L),(mk_real_int64 359626150072275007L);(* 17, 17 *)
(mk_real_int64 200102652952194438L),(mk_real_int64 248047961710365531L);(* 17, 17 *)
(mk_real_int64 409254169132740096L),(mk_real_int64 10684881587668145L);(* 17, 16 *)
(mk_real_int64 789948491613588496L),(mk_real_int64 417663227448475960L);(* 17, 17 *)
(mk_real_int64 490366800409409040L),(mk_real_int64 31212308763091533L);(* 17, 16 *)
(mk_real_int64 191075942182785996L),(mk_real_int64 55867299018160917L);(* 17, 16 *)
(mk_real_int64 107100682253722719L),(mk_real_int64 373085966097961255L);(* 17, 17 *)
(mk_real_int64 8804800651476300L),(mk_real_int64 157231485025656188L);(* 15, 17 *)
(mk_real_int64 454861192419900800L),(mk_real_int64 745146441904545450L);(* 17, 17 *)
(mk_real_int64 11496795608306112L),(mk_real_int64 159249453772591225L);(* 16, 17 *)
(mk_real_int64 57932613414425664L),(mk_real_int64 223851113048079618L);(* 16, 17 *)
(mk_real_int64 76590884363125301L),(mk_real_int64 243665443228419730L);(* 16, 17 *)
(mk_real_int64 152179147779991700L),(mk_real_int64 183308423333938188L);(* 17, 17 *)
(mk_real_int64 128683737848599622L),(mk_real_int64 117916588465090106L);(* 17, 17 *)
(mk_real_int64 98077062191483520L),(mk_real_int64 257526207710618346L);(* 16, 17 *)
(mk_real_int64 16442619629007052L),(mk_real_int64 746325585172341104L);(* 16, 17 *)
(mk_real_int64 133734742264750684L),(mk_real_int64 10259442198451440L);(* 17, 16 *)
(mk_real_int64 3543874476514560L),(mk_real_int64 399903439010291508L);(* 15, 17 *)
(mk_real_int64 292528609951499060L),(mk_real_int64 886240262048344980L);(* 17, 17 *)
(mk_real_int64 165300999540805296L),(mk_real_int64 59214302982243489L);(* 17, 16 *)
(mk_real_int64 8367875217369317L),(mk_real_int64 34987378643976330L);(* 15, 16 *)
(mk_real_int64 413136279301505408L),(mk_real_int64 267461272795659440L);(* 17, 17 *)
(mk_real_int64 249549638557193175L),(mk_real_int64 347615490772393128L);(* 17, 17 *)
(mk_real_int64 145330460084736683L),(mk_real_int64 653803041793988880L);(* 17, 17 *)
(mk_real_int64 158384809891715638L),(mk_real_int64 96599431220847322L);(* 17, 16 *)
(mk_real_int64 205608112902088339L),(mk_real_int64 273006455558363813L);(* 17, 17 *)
(mk_real_int64 275135580389051676L),(mk_real_int64 104253466269589164L);(* 17, 17 *)
(mk_real_int64 414344819195654844L),(mk_real_int64 702422930092998582L);(* 17, 17 *)
(mk_real_int64 6036873136353720L),(mk_real_int64 676613953513603858L);(* 15, 17 *)
(mk_real_int64 359011770037510932L),(mk_real_int64 680586248165284398L);(* 17, 17 *)
(mk_real_int64 182707943046567704L),(mk_real_int64 272463312987014540L);(* 17, 17 *)
(mk_real_int64 388775585384215848L),(mk_real_int64 122104942625027043L);(* 17, 17 *)
(mk_real_int64 54045314469805320L),(mk_real_int64 615953249067435796L);(* 16, 17 *)
(mk_real_int64 189093503288281000L),(mk_real_int64 398650271000471392L);(* 17, 17 *)
(mk_real_int64 261956794725602670L),(mk_real_int64 87759452300160704L);(* 17, 16 *)
(mk_real_int64 258629958248844171L),(mk_real_int64 761223369252198420L);(* 17, 17 *)
(mk_real_int64 604169305404880610L),(mk_real_int64 92481445687557094L);(* 17, 16 *)
(mk_real_int64 562261910286786663L),(mk_real_int64 184627938299588868L);(* 17, 17 *)
(mk_real_int64 24878503874262038L),(mk_real_int64 675572774177415203L);(* 16, 17 *)
(mk_real_int64 106541340017109198L),(mk_real_int64 22258850839292304L);(* 17, 16 *)
(mk_real_int64 724184692892950590L),(mk_real_int64 825359130951253326L);(* 17, 17 *)
(mk_real_int64 693075996996144197L),(mk_real_int64 172959712008462016L);(* 17, 17 *)
(mk_real_int64 13949939963043000L),(mk_real_int64 351869023743482795L);(* 16, 17 *)
(mk_real_int64 382082364816605928L),(mk_real_int64 171988161800618340L);(* 17, 17 *)
(mk_real_int64 27341423225829112L),(mk_real_int64 445596123978428785L);(* 16, 17 *)
(mk_real_int64 138531555168270588L),(mk_real_int64 477921774802602864L);(* 17, 17 *)
(mk_real_int64 137036365154310114L),(mk_real_int64 278018435167329375L);(* 17, 17 *)
(mk_real_int64 329287979720347207L),(mk_real_int64 367924564473646964L);(* 17, 17 *)
(mk_real_int64 110196892117470774L),(mk_real_int64 302235801544384800L);(* 17, 17 *)
(mk_real_int64 678413313744607340L),(mk_real_int64 130160199267019103L);(* 17, 17 *)
(mk_real_int64 434476267930486350L),(mk_real_int64 356434436091543276L);(* 17, 17 *)
(mk_real_int64 260625674650198410L),(mk_real_int64 635233329583232982L);(* 17, 17 *)
(mk_real_int64 278867035391393680L),(mk_real_int64 92057441784679717L);(* 17, 16 *)
(mk_real_int64 169867260130126056L),(mk_real_int64 238579286587064794L);(* 17, 17 *)
(mk_real_int64 46580907943251968L),(mk_real_int64 139836477448303564L);(* 16, 17 *)
(mk_real_int64 229816383142221948L),(mk_real_int64 257664827952003873L);(* 17, 17 *)
(mk_real_int64 705083541903912L),(mk_real_int64 214662654938848147L);(* 14, 17 *)
(mk_real_int64 730184990273655828L),(mk_real_int64 80838698975170020L);(* 17, 16 *)
(mk_real_int64 370797272500143933L),(mk_real_int64 57499855574062876L);(* 17, 16 *)
(mk_real_int64 743103586250010000L),(mk_real_int64 12560479554589880L);(* 17, 16 *)
(mk_real_int64 295994821633703896L),(mk_real_int64 12521729801254695L);(* 17, 16 *)
(mk_real_int64 96691874039859280L),(mk_real_int64 90100502189072994L);(* 16, 16 *)
(mk_real_int64 178725656364342637L),(mk_real_int64 42085643324748171L);(* 17, 16 *)
(mk_real_int64 380008250683731870L),(mk_real_int64 515283790742670989L);(* 17, 17 *)
(mk_real_int64 353348734281330611L),(mk_real_int64 249461239753401336L);(* 17, 17 *)
(mk_real_int64 20569010317601772L),(mk_real_int64 139049406702602612L);(* 16, 17 *)
(mk_real_int64 351300270231794506L),(mk_real_int64 445205625043864884L);(* 17, 17 *)
(mk_real_int64 275253948407168514L),(mk_real_int64 273163011986949064L);(* 17, 17 *)
(mk_real_int64 144067194933109305L),(mk_real_int64 20473084461446706L);(* 17, 16 *)
(mk_real_int64 256504003116280920L),(mk_real_int64 177139517580898552L);(* 17, 17 *)
(mk_real_int64 22956760304090834L),(mk_real_int64 473704949375808384L);(* 16, 17 *)
(mk_real_int64 169948356632419706L),(mk_real_int64 371727527717719440L);(* 17, 17 *)
(mk_real_int64 37736475700250000L),(mk_real_int64 7058251797180480L);(* 16, 15 *)
(mk_real_int64 338072901759894938L),(mk_real_int64 395966005163576203L);(* 17, 17 *)
(mk_real_int64 2872003702204068L),(mk_real_int64 222573971856406985L);(* 15, 17 *)
(mk_real_int64 42508564456494585L),(mk_real_int64 547725863948010690L);(* 16, 17 *)
(mk_real_int64 413056527906494574L),(mk_real_int64 446735681900480421L);(* 17, 17 *)
(mk_real_int64 389529928452339592L),(mk_real_int64 4422461108880258L);(* 17, 15 *)
(mk_real_int64 19007411974911500L),(mk_real_int64 312522463711735584L);(* 16, 17 *)
(mk_real_int64 160351674415701444L),(mk_real_int64 4380781863364179L);(* 17, 15 *)
(mk_real_int64 144499830580439316L),(mk_real_int64 26127883629905232L);(* 17, 16 *)
(mk_real_int64 473931903797856896L),(mk_real_int64 76677814264616800L);(* 17, 16 *)
(mk_real_int64 190617069775577328L),(mk_real_int64 405514137331460556L);(* 17, 17 *)
(mk_real_int64 147895553238175778L),(mk_real_int64 68877141636610044L);(* 17, 16 *)
(mk_real_int64 96279929034063373L),(mk_real_int64 175992526856146494L);(* 16, 17 *)
(mk_real_int64 293890934178484870L),(mk_real_int64 178245899053238982L);(* 17, 17 *)
(mk_real_int64 192668268002044769L),(mk_real_int64 40014834374693010L);(* 17, 16 *)
(mk_real_int64 6539761442928800L),(mk_real_int64 144412941763248549L);(* 15, 17 *)
(mk_real_int64 50295279025946584L),(mk_real_int64 150444706863997483L);(* 16, 17 *)
(mk_real_int64 549059853896400132L),(mk_real_int64 98092221765344876L);(* 17, 16 *)
(mk_real_int64 60398071684593004L),(mk_real_int64 165228893375945106L);(* 16, 17 *)
(mk_real_int64 53751846841125246L),(mk_real_int64 259931237188116098L);(* 16, 17 *)
(mk_real_int64 122131336718759264L),(mk_real_int64 23376654691930832L);(* 17, 16 *)
(mk_real_int64 598276947867716280L),(mk_real_int64 14457658984269984L);(* 17, 16 *)
(mk_real_int64 31101592548212400L),(mk_real_int64 779705450302531332L);(* 16, 17 *)
(mk_real_int64 33471294181001516L),(mk_real_int64 51258014550354447L);(* 16, 16 *)
(mk_real_int64 279478945543446735L),(mk_real_int64 690497977979321044L);(* 17, 17 *)
(mk_real_int64 512323710977707455L),(mk_real_int64 83304258517403220L);(* 17, 16 *)
(mk_real_int64 298783632546375743L),(mk_real_int64 148930285464602965L);(* 17, 17 *)
(mk_real_int64 352958353099748693L),(mk_real_int64 1197070644155433L);(* 17, 15 *)
(mk_real_int64 70319404633186656L),(mk_real_int64 49320859492526344L);(* 16, 16 *)
(mk_real_int64 87805654610749690L),(mk_real_int64 182321097758949612L);(* 16, 17 *)
(mk_real_int64 6905168065513406L),(mk_real_int64 144634561278775281L);(* 15, 17 *)
(mk_real_int64 809344036204263712L),(mk_real_int64 263617285775156811L);(* 17, 17 *)
(mk_real_int64 814707898359841615L),(mk_real_int64 297374110102353753L);(* 17, 17 *)
(mk_real_int64 166039500111485424L),(mk_real_int64 20257935411515040L);(* 17, 16 *)
(mk_real_int64 263783361757101924L),(mk_real_int64 657599387703695746L);(* 17, 17 *)
(mk_real_int64 107418119566871335L),(mk_real_int64 465859416597984720L);(* 17, 17 *)
(mk_real_int64 6919830365244285L),(mk_real_int64 115142390660589080L);(* 15, 17 *)
(mk_real_int64 23992960654117708L),(mk_real_int64 155448572416898144L);(* 16, 17 *)
(mk_real_int64 506405480277386320L),(mk_real_int64 724218551032667724L);(* 17, 17 *)
(mk_real_int64 184130386813404252L),(mk_real_int64 417058108112373410L);(* 17, 17 *)
(mk_real_int64 40907074836978840L),(mk_real_int64 220897212370868430L);(* 16, 17 *)
(mk_real_int64 560727410304792750L),(mk_real_int64 125738889241979724L);(* 17, 17 *)
(mk_real_int64 13559768894492252L),(mk_real_int64 22649478162101400L);(* 16, 16 *)
(mk_real_int64 4018272354494754L),(mk_real_int64 9948615410592795L);(* 15, 15 *)
(mk_real_int64 175044982773215969L),(mk_real_int64 48970811819748000L);(* 17, 16 *)
(mk_real_int64 85768313635517605L),(mk_real_int64 179453265141700386L);(* 16, 17 *)
(mk_real_int64 62378902283841374L),(mk_real_int64 520137487404553641L);(* 16, 17 *)
(mk_real_int64 95196278856083274L),(mk_real_int64 253469679982741233L);(* 16, 17 *)
(mk_real_int64 127898254137345237L),(mk_real_int64 720421350860148400L);(* 17, 17 *)
(mk_real_int64 440649642567663672L),(mk_real_int64 326897213832856725L);(* 17, 17 *)
(mk_real_int64 12873265363929250L),(mk_real_int64 24347550958829808L);(* 16, 16 *)
(mk_real_int64 290885035486985346L),(mk_real_int64 592869385156681598L);(* 17, 17 *)
(mk_real_int64 379869156569487508L),(mk_real_int64 454380729218279235L);(* 17, 17 *)
(mk_real_int64 688979527108774992L),(mk_real_int64 37949922989679275L);(* 17, 16 *)
(mk_real_int64 6892645217251739L),(mk_real_int64 390312507314801376L);(* 15, 17 *)
(mk_real_int64 823268783092292689L),(mk_real_int64 505311355874309421L);(* 17, 17 *)
(mk_real_int64 665818615368411344L),(mk_real_int64 67611582294459555L);(* 17, 16 *)
(mk_real_int64 31833332963680245L),(mk_real_int64 348262340038993125L);(* 16, 17 *)
(mk_real_int64 121929772878457635L),(mk_real_int64 491735590348504050L);(* 17, 17 *)
(mk_real_int64 109395874076045700L),(mk_real_int64 221013617050208528L);(* 17, 17 *)
(mk_real_int64 555645964202062272L),(mk_real_int64 1251323835469176L);(* 17, 15 *)
(mk_real_int64 268655574457902072L),(mk_real_int64 83331374977281032L);(* 17, 16 *)
(mk_real_int64 194339498503644029L),(mk_real_int64 150538320271112478L);(* 17, 17 *)
(mk_real_int64 24728638166275685L),(mk_real_int64 125212371087329127L);(* 16, 17 *)
(mk_real_int64 229078069940799898L),(mk_real_int64 121132576807714157L);(* 17, 17 *)
(mk_real_int64 191899689974393028L),(mk_real_int64 248614128793710527L);(* 17, 17 *)
(mk_real_int64 19335421454942824L),(mk_real_int64 110523712674094430L);(* 16, 17 *)
(mk_real_int64 291539245693503030L),(mk_real_int64 233488069926128432L);(* 17, 17 *)
(mk_real_int64 122366897955991668L),(mk_real_int64 7487780422235004L);(* 17, 15 *)
(mk_real_int64 448642491013006926L),(mk_real_int64 146513571733996290L);(* 17, 17 *)
(mk_real_int64 107139608798366326L),(mk_real_int64 20993173960042410L);(* 17, 16 *)
(mk_real_int64 117174904940548008L),(mk_real_int64 213438507760869604L);(* 17, 17 *)
(mk_real_int64 427266686183988168L),(mk_real_int64 6683230458510552L);(* 17, 15 *)
(mk_real_int64 665377191480758010L),(mk_real_int64 14491050422204223L);(* 17, 16 *)
(mk_real_int64 273488086759997865L),(mk_real_int64 624360148264280560L);(* 17, 17 *)
(mk_real_int64 50881747603036632L),(mk_real_int64 239692135032472428L);(* 16, 17 *)
(mk_real_int64 5392570685914020L),(mk_real_int64 173497425593500920L);(* 15, 17 *)
(mk_real_int64 142009248163947850L),(mk_real_int64 389405872099749076L);(* 17, 17 *)
(mk_real_int64 81135789824832518L),(mk_real_int64 253938024272531709L);(* 16, 17 *)
(mk_real_int64 41040677633273240L),(mk_real_int64 106077318662935300L);(* 16, 17 *)
(mk_real_int64 350501205384717248L),(mk_real_int64 21100257914671170L);(* 17, 16 *)
(mk_real_int64 310017645108957258L),(mk_real_int64 279377902539486580L);(* 17, 17 *)
(mk_real_int64 889859221165683735L),(mk_real_int64 87821791390148772L);(* 17, 16 *)
(mk_real_int64 374796768845337930L),(mk_real_int64 96445585303862872L);(* 17, 16 *)
(mk_real_int64 123721359722623385L),(mk_real_int64 243984998537948889L);(* 17, 17 *)
(mk_real_int64 128183134240081518L),(mk_real_int64 539191902400704L);(* 17, 14 *)
(mk_real_int64 7432427777665280L),(mk_real_int64 58569398040162939L);(* 15, 16 *)
(mk_real_int64 657619674768234675L),(mk_real_int64 216415837373855430L);(* 17, 17 *)
(mk_real_int64 198796664853296016L),(mk_real_int64 69572846670067730L);(* 17, 16 *)
(mk_real_int64 3634661912794563L),(mk_real_int64 319187171508271164L);(* 15, 17 *)
(mk_real_int64 92944899629007679L),(mk_real_int64 318640920553105125L);(* 16, 17 *)
(mk_real_int64 32567485615317754L),(mk_real_int64 190133256236867102L);(* 16, 17 *)
(mk_real_int64 165322080139398850L),(mk_real_int64 113738615973366186L);(* 17, 17 *)
(mk_real_int64 117856642879233051L),(mk_real_int64 13283396370650560L);(* 17, 16 *)
(mk_real_int64 57952217319737964L),(mk_real_int64 270650634099323403L);(* 16, 17 *)
(mk_real_int64 451648154099218301L),(mk_real_int64 66321310463737569L);(* 17, 16 *)
(mk_real_int64 36728674297155661L),(mk_real_int64 86580401011932834L);(* 16, 16 *)
(mk_real_int64 307555587490145421L),(mk_real_int64 451111610895042920L);(* 17, 17 *)
(mk_real_int64 235020814043246386L),(mk_real_int64 58083905635139604L);(* 17, 16 *)
(mk_real_int64 439032608939671200L),(mk_real_int64 55091318812432512L);(* 17, 16 *)
(mk_real_int64 463352733900576846L),(mk_real_int64 325984018786893456L);(* 17, 17 *)
(mk_real_int64 183824622200934468L),(mk_real_int64 103385296222218528L);(* 17, 17 *)
(mk_real_int64 7820198683476111L),(mk_real_int64 172059693574856292L);(* 15, 17 *)
(mk_real_int64 60169547546833020L),(mk_real_int64 397864005974938572L);(* 16, 17 *)
(mk_real_int64 280875578320387834L),(mk_real_int64 96030962571192532L);(* 17, 16 *)
(mk_real_int64 165651466887694615L),(mk_real_int64 25821329868928485L);(* 17, 16 *)
(mk_real_int64 453480154188053896L),(mk_real_int64 506242593165416596L);(* 17, 17 *)
(mk_real_int64 710581541711202564L),(mk_real_int64 289511114251656276L);(* 17, 17 *)
(mk_real_int64 233271177390337114L),(mk_real_int64 655289791406641380L);(* 17, 17 *)
(mk_real_int64 76645042306484868L),(mk_real_int64 544213064303056096L);(* 16, 17 *)
(mk_real_int64 161784229567887822L),(mk_real_int64 3416518397036514L);(* 17, 15 *)
(mk_real_int64 234783246854951280L),(mk_real_int64 165142279215827528L);(* 17, 17 *)
(mk_real_int64 374305475472972930L),(mk_real_int64 49638554171065090L);(* 17, 16 *)
(mk_real_int64 710048097451578160L),(mk_real_int64 138368208049183274L);(* 17, 17 *)
(mk_real_int64 645032304724825656L),(mk_real_int64 620334463872975000L);(* 17, 17 *)
(mk_real_int64 330029614147215908L),(mk_real_int64 162256397899255205L);(* 17, 17 *)
(mk_real_int64 340283912255138016L),(mk_real_int64 254756445463584534L);(* 17, 17 *)
(mk_real_int64 510999965172915750L),(mk_real_int64 123240687146453484L);(* 17, 17 *)
(mk_real_int64 59423632882065298L),(mk_real_int64 4942354507281306L);(* 16, 15 *)
(mk_real_int64 105166487413569624L),(mk_real_int64 4169229747669826L);(* 17, 15 *)
(mk_real_int64 46581618440128792L),(mk_real_int64 18041786959126777L);(* 16, 16 *)
(mk_real_int64 793896091622760282L),(mk_real_int64 291747218574375984L);(* 17, 17 *)
(mk_real_int64 122966836148459667L),(mk_real_int64 258372999180339360L);(* 17, 17 *)
(mk_real_int64 269321520054520296L),(mk_real_int64 62276945455656756L);(* 17, 16 *)
(mk_real_int64 327861143929499224L),(mk_real_int64 9876116528656470L);(* 17, 15 *)
(mk_real_int64 9283271001840040L),(mk_real_int64 456553441651470916L);(* 15, 17 *)
(mk_real_int64 140172681802374828L),(mk_real_int64 210377704821887273L);(* 17, 17 *)
(mk_real_int64 189204871918513824L),(mk_real_int64 590557570376391020L);(* 17, 17 *)
(mk_real_int64 740578497478932042L),(mk_real_int64 208381914920982120L);(* 17, 17 *)
(mk_real_int64 197673975191962875L),(mk_real_int64 210222514456692322L);(* 17, 17 *)
(mk_real_int64 157919681039601L),(mk_real_int64 7013976546028011L);(* 14, 15 *)
(mk_real_int64 8660283088717464L),(mk_real_int64 333350816310440100L);(* 15, 17 *)
(mk_real_int64 78568388580078632L),(mk_real_int64 490633124255592659L);(* 16, 17 *)
(mk_real_int64 11685071470329242L),(mk_real_int64 4637653878752424L);(* 16, 15 *)
(mk_real_int64 357266922560543700L),(mk_real_int64 915604545922068503L);(* 17, 17 *)
(mk_real_int64 77544405516974140L),(mk_real_int64 16849530487435360L);(* 16, 16 *)
(mk_real_int64 163199827468618176L),(mk_real_int64 168365728255787700L);(* 17, 17 *)
(mk_real_int64 132546524093757508L),(mk_real_int64 148606604601560560L);(* 17, 17 *)
(mk_real_int64 191235677777320920L),(mk_real_int64 587209958339248408L);(* 17, 17 *)
(mk_real_int64 703613079796670046L),(mk_real_int64 507082967833159190L);(* 17, 17 *)
(mk_real_int64 19683672627344228L),(mk_real_int64 130696099532675325L);(* 16, 17 *)
(mk_real_int64 118274577131884446L),(mk_real_int64 307639710454062546L);(* 17, 17 *)
(mk_real_int64 574210892346098850L),(mk_real_int64 498411953426871824L);(* 17, 17 *)
(mk_real_int64 299725400493044072L),(mk_real_int64 814463464567806915L);(* 17, 17 *)
(mk_real_int64 80282015006414592L),(mk_real_int64 358989457644404496L);(* 16, 17 *)
(mk_real_int64 343240417218675114L),(mk_real_int64 65847620304719592L);(* 17, 16 *)
(mk_real_int64 48880795796606160L),(mk_real_int64 115395610321739202L);(* 16, 17 *)
(mk_real_int64 10257882923411224L),(mk_real_int64 47395373091219684L);(* 16, 16 *)
(mk_real_int64 524077236617636L),(mk_real_int64 29116893943284840L);(* 14, 16 *)
(mk_real_int64 187612596843716416L),(mk_real_int64 123407823106743189L);(* 17, 17 *)
(mk_real_int64 351237459002698650L),(mk_real_int64 341391307778962264L);(* 17, 17 *)
(mk_real_int64 62852914686887248L),(mk_real_int64 66412532437748332L);(* 16, 16 *)
(mk_real_int64 433159175983670136L),(mk_real_int64 242357699754983280L);(* 17, 17 *)
(mk_real_int64 207272034879086200L),(mk_real_int64 550049714742216412L);(* 17, 17 *)
(mk_real_int64 56226380193261252L),(mk_real_int64 1015550363672625L);(* 16, 15 *)
(mk_real_int64 127351329399566820L),(mk_real_int64 448512907072586691L);(* 17, 17 *)
(mk_real_int64 518498419624574906L),(mk_real_int64 470871911210692875L);(* 17, 17 *)
(mk_real_int64 138468892180627957L),(mk_real_int64 46666680598928610L);(* 17, 16 *)
(mk_real_int64 126632132059167468L),(mk_real_int64 446955457730116294L);(* 17, 17 *)
(mk_real_int64 469424389389248850L),(mk_real_int64 166400285479642030L);(* 17, 17 *)
(mk_real_int64 14576018859788694L),(mk_real_int64 161949995937481108L);(* 16, 17 *)
(mk_real_int64 173422191673189725L),(mk_real_int64 145495390776482160L);(* 17, 17 *)
(mk_real_int64 10490681218720953L),(mk_real_int64 497223415630387524L);(* 16, 17 *)
(mk_real_int64 143685196090929688L),(mk_real_int64 419272989328472688L);(* 17, 17 *)
(mk_real_int64 739182443681562920L),(mk_real_int64 264288903209167296L);(* 17, 17 *)
(mk_real_int64 299203096051222548L),(mk_real_int64 107813319077050686L);(* 17, 17 *)
(mk_real_int64 618528069533712330L),(mk_real_int64 388859241688819594L);(* 17, 17 *)
(mk_real_int64 7156092663611112L),(mk_real_int64 85973839319757765L);(* 15, 16 *)
(mk_real_int64 135481002442061087L),(mk_real_int64 5090686761320640L);(* 17, 15 *)
(mk_real_int64 224510509483173864L),(mk_real_int64 31051784724899826L);(* 17, 16 *)
(mk_real_int64 92536072472813864L),(mk_real_int64 586285053997561722L);(* 16, 17 *)
(mk_real_int64 291949804926934478L),(mk_real_int64 79652793687890297L);(* 17, 16 *)
(mk_real_int64 128667269174756844L),(mk_real_int64 557825939213274608L);(* 17, 17 *)
(mk_real_int64 780462449872516308L),(mk_real_int64 45785044427610279L);(* 17, 16 *)
(mk_real_int64 51521165456357440L),(mk_real_int64 737855891778078324L);(* 16, 17 *)
(mk_real_int64 549589368559853400L),(mk_real_int64 132271987593624482L);(* 17, 17 *)
(mk_real_int64 384259306325462280L),(mk_real_int64 74202904977827430L);(* 17, 16 *)
(mk_real_int64 429766829770096802L),(mk_real_int64 189645633148436765L);(* 17, 17 *)
(mk_real_int64 371248243711292948L),(mk_real_int64 36399899495312380L);(* 17, 16 *)
(mk_real_int64 506522979701785083L),(mk_real_int64 101156369051498700L);(* 17, 17 *)
(mk_real_int64 497619114810863184L),(mk_real_int64 382066475022846012L);(* 17, 17 *)
(mk_real_int64 115312647922151400L),(mk_real_int64 207160080362094211L);(* 17, 17 *)
(mk_real_int64 32794320918543432L),(mk_real_int64 71854364743961760L);(* 16, 16 *)
(mk_real_int64 2630110581817725L),(mk_real_int64 308519632016436978L);(* 15, 17 *)
(mk_real_int64 15404249291611914L),(mk_real_int64 280658980088209846L);(* 16, 17 *)
(mk_real_int64 1666085223959040L),(mk_real_int64 175755115472855464L);(* 15, 17 *)
(mk_real_int64 94770900606789904L),(mk_real_int64 396582995083982000L);(* 16, 17 *)
(mk_real_int64 561150930549842824L),(mk_real_int64 867294576472654304L);(* 17, 17 *)
(mk_real_int64 404072306023940801L),(mk_real_int64 226523082932498976L);(* 17, 17 *)
(mk_real_int64 58882677993157982L),(mk_real_int64 388653047904339228L);(* 16, 17 *)
(mk_real_int64 355051677322317412L),(mk_real_int64 531006800188200L);(* 17, 14 *)
(mk_real_int64 26539786357709184L),(mk_real_int64 450652423590012721L);(* 16, 17 *)
(mk_real_int64 494739044272459800L),(mk_real_int64 74043522864770718L);(* 17, 16 *)
(mk_real_int64 249201136656102826L),(mk_real_int64 429095069595859224L);(* 17, 17 *)
(mk_real_int64 354913159176479L),(mk_real_int64 442496149398184478L);(* 14, 17 *)
(mk_real_int64 210472506754160628L),(mk_real_int64 79581119381824520L);(* 17, 16 *)
(mk_real_int64 229758403056206164L),(mk_real_int64 149502082993191096L);(* 17, 17 *)
(mk_real_int64 121885361476901120L),(mk_real_int64 300065640458675176L);(* 17, 17 *)
(mk_real_int64 115008996345505605L),(mk_real_int64 460815598154100618L);(* 17, 17 *)
(mk_real_int64 171819785560068464L),(mk_real_int64 5839394762112185L);(* 17, 15 *)
(mk_real_int64 22653870015726144L),(mk_real_int64 118290442108972700L);(* 16, 17 *)
(mk_real_int64 210182587784577732L),(mk_real_int64 425834901779389229L);(* 17, 17 *)
(mk_real_int64 18388064577089341L),(mk_real_int64 107677872137251552L);(* 16, 17 *)
(mk_real_int64 171366834562569784L),(mk_real_int64 95138790011576892L);(* 17, 16 *)
(mk_real_int64 371951431215785390L),(mk_real_int64 570539735983729160L);(* 17, 17 *)
(mk_real_int64 274572186851220780L),(mk_real_int64 86378080215768000L);(* 17, 16 *)
(mk_real_int64 55544369931079412L),(mk_real_int64 280232037384432806L);(* 16, 17 *)
(mk_real_int64 41848810557034088L),(mk_real_int64 77949689489972982L);(* 16, 16 *)
(mk_real_int64 446023715973708836L),(mk_real_int64 629364959738620802L);(* 17, 17 *)
(mk_real_int64 1659860815619514L),(mk_real_int64 23098009218234864L);(* 15, 16 *)
(mk_real_int64 107517481744419242L),(mk_real_int64 300772932346479903L);(* 17, 17 *)
(mk_real_int64 109744272721043037L),(mk_real_int64 712426655342965748L);(* 17, 17 *)
(mk_real_int64 624010191478381422L),(mk_real_int64 106022302962512400L);(* 17, 17 *)
(mk_real_int64 184379721115291800L),(mk_real_int64 263070742701816475L);(* 17, 17 *)
(mk_real_int64 1968060468328722L),(mk_real_int64 14764922547597084L);(* 15, 16 *)
(mk_real_int64 756443004474658290L),(mk_real_int64 553845033121683466L);(* 17, 17 *)
(mk_real_int64 191566706784999549L),(mk_real_int64 119682523209090924L);(* 17, 17 *)
(mk_real_int64 113951674623144924L),(mk_real_int64 270249508853490048L);(* 17, 17 *)
(mk_real_int64 654470961193540788L),(mk_real_int64 447847400945278422L);(* 17, 17 *)
(mk_real_int64 532332225241003125L),(mk_real_int64 173070319279127250L);(* 17, 17 *)
(mk_real_int64 377495332182269596L),(mk_real_int64 175829142341763080L);(* 17, 17 *)
(mk_real_int64 163976487125827728L),(mk_real_int64 235804133841310435L);(* 17, 17 *)
(mk_real_int64 231620414743149025L),(mk_real_int64 136060152681048096L);(* 17, 17 *)
(mk_real_int64 525515028768702813L),(mk_real_int64 49148139903864422L);(* 17, 16 *)
(mk_real_int64 276360055437806824L),(mk_real_int64 41895692752209384L);(* 17, 16 *)
(mk_real_int64 5128579272023900L),(mk_real_int64 231338296950936370L);(* 15, 17 *)
(mk_real_int64 273424096675798791L),(mk_real_int64 314614293521831902L);(* 17, 17 *)
(mk_real_int64 707292147617436815L),(mk_real_int64 301443519069825713L);(* 17, 17 *)
(mk_real_int64 213019146422093220L),(mk_real_int64 139270493820204615L);(* 17, 17 *)
(mk_real_int64 63808718833548992L),(mk_real_int64 221304093026843178L);(* 16, 17 *)
(mk_real_int64 193919741062213704L),(mk_real_int64 102339429138180432L);(* 17, 17 *)
(mk_real_int64 147859250000980584L),(mk_real_int64 205347642781108275L);(* 17, 17 *)
(mk_real_int64 182295949824552096L),(mk_real_int64 275780402695777674L);(* 17, 17 *)
(mk_real_int64 576541331914549586L),(mk_real_int64 245801525908535010L);(* 17, 17 *)
(mk_real_int64 31404509514450802L),(mk_real_int64 511965901452799528L);(* 16, 17 *)
(mk_real_int64 532574376520588L),(mk_real_int64 81410173493047931L);(* 14, 16 *)
(mk_real_int64 135223815423703986L),(mk_real_int64 264918864708798750L);(* 17, 17 *)
(mk_real_int64 41898895942064364L),(mk_real_int64 25132929952228176L);(* 16, 16 *)
(mk_real_int64 11189686376143366L),(mk_real_int64 11859768678774720L);(* 16, 16 *)
(mk_real_int64 201278394715701469L),(mk_real_int64 100738272787649543L);(* 17, 17 *)
(mk_real_int64 11988769347048120L),(mk_real_int64 64302279973561665L);(* 16, 16 *)
(mk_real_int64 462857929676491200L),(mk_real_int64 19156546165428792L);(* 17, 16 *)
(mk_real_int64 99558975960270398L),(mk_real_int64 131470614204830216L);(* 16, 17 *)
(mk_real_int64 565640182911810039L),(mk_real_int64 119873845965604687L);(* 17, 17 *)
(mk_real_int64 116113171745810400L),(mk_real_int64 172837592245430094L);(* 17, 17 *)
(mk_real_int64 858927598293632368L),(mk_real_int64 166981368042027549L);(* 17, 17 *)
(mk_real_int64 146796810763834184L),(mk_real_int64 99677355156230893L);(* 17, 16 *)
(mk_real_int64 385514215156884898L),(mk_real_int64 315121954012951682L);(* 17, 17 *)
(mk_real_int64 255593180124225760L),(mk_real_int64 460793643361493768L);(* 17, 17 *)
(mk_real_int64 842726796875314650L),(mk_real_int64 274245243061579272L);(* 17, 17 *)
(mk_real_int64 266732566875944779L),(mk_real_int64 159072893105265999L);(* 17, 17 *)
(mk_real_int64 276734851149681784L),(mk_real_int64 119150330445378135L);(* 17, 17 *)
(mk_real_int64 52455887967785984L),(mk_real_int64 394912449102918530L);(* 16, 17 *)
(mk_real_int64 276908697434380440L),(mk_real_int64 21746679088327311L);(* 17, 16 *)
(mk_real_int64 450266605045071004L),(mk_real_int64 28251048432871824L);(* 17, 16 *)
(mk_real_int64 63037226969930180L),(mk_real_int64 373620555830229271L);(* 16, 17 *)
(mk_real_int64 237621098998615824L),(mk_real_int64 35641528284130827L);(* 17, 16 *)
(mk_real_int64 134395053316622355L),(mk_real_int64 149613456100834899L);(* 17, 17 *)
(mk_real_int64 895552409557569157L),(mk_real_int64 243467275621622307L);(* 17, 17 *)
(mk_real_int64 347730102107935700L),(mk_real_int64 698613085669645160L);(* 17, 17 *)
(mk_real_int64 391353711916315168L),(mk_real_int64 311469670087907766L);(* 17, 17 *)
(mk_real_int64 127506035067772360L),(mk_real_int64 309990171882536952L);(* 17, 17 *)
(mk_real_int64 221722270910587094L),(mk_real_int64 392016290355693960L);(* 17, 17 *)
(mk_real_int64 135321079752243567L),(mk_real_int64 293076709112869485L);(* 17, 17 *)
(mk_real_int64 397831144030928280L),(mk_real_int64 475907001773383368L);(* 17, 17 *)
(mk_real_int64 253683678292556838L),(mk_real_int64 144956972675040894L);(* 17, 17 *)
(mk_real_int64 793788504332261802L),(mk_real_int64 312410896046190375L);(* 17, 17 *)
(mk_real_int64 200940126244604148L),(mk_real_int64 135073441454723136L);(* 17, 17 *)
(mk_real_int64 348568683417709476L),(mk_real_int64 231559093334273821L);(* 17, 17 *)
(mk_real_int64 40700985550552460L),(mk_real_int64 117936152231015652L);(* 16, 17 *)
(mk_real_int64 636974990510621448L),(mk_real_int64 415766678174080380L);(* 17, 17 *)
(mk_real_int64 743598920867412838L),(mk_real_int64 1970197989130872L);(* 17, 15 *)
(mk_real_int64 382717594438405276L),(mk_real_int64 211956078260422395L);(* 17, 17 *)
(mk_real_int64 165752217268235424L),(mk_real_int64 133748123574746320L);(* 17, 17 *)
(mk_real_int64 665529040758255056L),(mk_real_int64 143903850677551420L);(* 17, 17 *)
(mk_real_int64 113673918320665638L),(mk_real_int64 243959520104901354L);(* 17, 17 *)
(mk_real_int64 72725505924838897L),(mk_real_int64 36162897910769800L);(* 16, 16 *)
(mk_real_int64 137031057438899519L),(mk_real_int64 760294558447754970L);(* 17, 17 *)
(mk_real_int64 709939843753034888L),(mk_real_int64 57676979978558325L);(* 17, 16 *)
(mk_real_int64 317876766055665642L),(mk_real_int64 921980601061499210L);(* 17, 17 *)
(mk_real_int64 124511460390176262L),(mk_real_int64 294759419208697004L);(* 17, 17 *)
(mk_real_int64 65953054089804120L),(mk_real_int64 300268147932220380L);(* 16, 17 *)
(mk_real_int64 317463022073811584L),(mk_real_int64 377215986989877504L);(* 17, 17 *)
(mk_real_int64 133230609351783750L),(mk_real_int64 247864715813073359L);(* 17, 17 *)
(mk_real_int64 426045677492551170L),(mk_real_int64 194442740742505504L);(* 17, 17 *)
(mk_real_int64 115160680748029283L),(mk_real_int64 15439324090340844L);(* 17, 16 *)
(mk_real_int64 881092378878251104L),(mk_real_int64 269316157549801572L);(* 17, 17 *)
(mk_real_int64 513427355524044745L),(mk_real_int64 132912183568687302L);(* 17, 17 *)
(mk_real_int64 609250328704311100L),(mk_real_int64 184868778372047040L);(* 17, 17 *)
(mk_real_int64 2380701428626628L),(mk_real_int64 111161332815330168L);(* 15, 17 *)
(mk_real_int64 237781656084123954L),(mk_real_int64 29204260009601010L);(* 17, 16 *)
(mk_real_int64 226572202799640585L),(mk_real_int64 204580954007556060L);(* 17, 17 *)
(mk_real_int64 41743697216086104L),(mk_real_int64 488871133196409504L);(* 16, 17 *)
(mk_real_int64 547133832837154132L),(mk_real_int64 10536181013841112L);(* 17, 16 *)
(mk_real_int64 23270181032347800L),(mk_real_int64 54955384365944986L);(* 16, 16 *)
(mk_real_int64 162342977721316524L),(mk_real_int64 545848594498042430L);(* 17, 17 *)
(mk_real_int64 17464584477790112L),(mk_real_int64 562814369441690436L);(* 16, 17 *)
(mk_real_int64 15901002821257168L),(mk_real_int64 244700399962528020L);(* 16, 17 *)
(mk_real_int64 36028217879185776L),(mk_real_int64 539684247993252024L);(* 16, 17 *)
(mk_real_int64 17276742210111612L),(mk_real_int64 332066502994913014L);(* 16, 17 *)
(mk_real_int64 411861232643791700L),(mk_real_int64 183268351507142560L);(* 17, 17 *)
(mk_real_int64 154562124489353560L),(mk_real_int64 126420759130043840L);(* 17, 17 *)
(mk_real_int64 207392420809125334L),(mk_real_int64 197501180868631836L);(* 17, 17 *)
(mk_real_int64 380410031190093222L),(mk_real_int64 156071122965120045L);(* 17, 17 *)
(mk_real_int64 468703627490825733L),(mk_real_int64 3881380531815340L);(* 17, 15 *)
(mk_real_int64 333263575399151025L),(mk_real_int64 404431614334041525L);(* 17, 17 *)
(mk_real_int64 17850406233849963L),(mk_real_int64 364998319528309880L);(* 16, 17 *)
(mk_real_int64 126976874877096972L),(mk_real_int64 482107703879974740L);(* 17, 17 *)
(mk_real_int64 214443810147758400L),(mk_real_int64 541202758843736344L);(* 17, 17 *)
(mk_real_int64 161674218961402748L),(mk_real_int64 261656286006718218L);(* 17, 17 *)
(mk_real_int64 353770294415700264L),(mk_real_int64 758852310241553063L);(* 17, 17 *)
(mk_real_int64 7681799209976340L),(mk_real_int64 443315678914358892L);(* 15, 17 *)
(mk_real_int64 436883833381497336L),(mk_real_int64 848554393123349056L);(* 17, 17 *)
(mk_real_int64 3949055269001832L),(mk_real_int64 61824642967060480L);(* 15, 16 *)
(mk_real_int64 64161742453752595L),(mk_real_int64 214958175606024563L);(* 16, 17 *)
(mk_real_int64 719504767141180296L),(mk_real_int64 305992066135500675L);(* 17, 17 *)
(mk_real_int64 516515755698751896L),(mk_real_int64 64038827307927006L);(* 17, 16 *)
(mk_real_int64 615099697516901520L),(mk_real_int64 214570171543079696L);(* 17, 17 *)
(mk_real_int64 53172839478065324L),(mk_real_int64 113466688109732400L);(* 16, 17 *)
(mk_real_int64 450042466989577968L),(mk_real_int64 279434226229034500L);(* 17, 17 *)
(mk_real_int64 59247174988456000L),(mk_real_int64 197081463270400527L);(* 16, 17 *)
(mk_real_int64 122343633331464879L),(mk_real_int64 135107495831644492L);(* 17, 17 *)
(mk_real_int64 369070577119551582L),(mk_real_int64 142499420784079793L);(* 17, 17 *)
(mk_real_int64 87068063759834970L),(mk_real_int64 698592279886825831L);(* 16, 17 *)
(mk_real_int64 301623726610970226L),(mk_real_int64 371732134830124158L);(* 17, 17 *)
(mk_real_int64 152139855421718528L),(mk_real_int64 127971173280527455L);(* 17, 17 *)
(mk_real_int64 46108528365681000L),(mk_real_int64 407418689319883098L);(* 16, 17 *)
(mk_real_int64 545832346315037886L),(mk_real_int64 121032785667250876L);(* 17, 17 *)
(mk_real_int64 50751303543158560L),(mk_real_int64 9720152323395381L);(* 16, 15 *)
(mk_real_int64 46199641318565998L),(mk_real_int64 85171122976843332L);(* 16, 16 *)
(mk_real_int64 578812927050840789L),(mk_real_int64 143575671668458866L);(* 17, 17 *)
(mk_real_int64 173007109679410659L),(mk_real_int64 207434525539963545L);(* 17, 17 *)
(mk_real_int64 389312500157236432L),(mk_real_int64 63656378468524644L);(* 17, 16 *)
(mk_real_int64 192796647732118885L),(mk_real_int64 130892409247257888L);(* 17, 17 *)
(mk_real_int64 231533110015678328L),(mk_real_int64 182572312942703025L);(* 17, 17 *)
(mk_real_int64 363547090596094308L),(mk_real_int64 365145568172045856L);(* 17, 17 *)
(mk_real_int64 5489458260594330L),(mk_real_int64 45692268604238840L);(* 15, 16 *)
(mk_real_int64 68766190462115756L),(mk_real_int64 432180490461756096L);(* 16, 17 *)
(mk_real_int64 703055171030543604L),(mk_real_int64 255212878557116304L);(* 17, 17 *)
(mk_real_int64 93970746832775914L),(mk_real_int64 294235315543082016L);(* 16, 17 *)
(mk_real_int64 117050018256574724L),(mk_real_int64 176428910215525640L);(* 17, 17 *)
(mk_real_int64 139863280367853955L),(mk_real_int64 324199919509673761L);(* 17, 17 *)
(mk_real_int64 65158803933103712L),(mk_real_int64 13821663810399426L);(* 16, 16 *)
(mk_real_int64 554687522356083282L),(mk_real_int64 94148870902433000L);(* 17, 16 *)
(mk_real_int64 201822139227044916L),(mk_real_int64 110096388460402124L);(* 17, 17 *)
(mk_real_int64 46302230478061424L),(mk_real_int64 277607508704007200L);(* 16, 17 *)
(mk_real_int64 495673479025596876L),(mk_real_int64 17931209052999808L);(* 17, 16 *)
(mk_real_int64 484090893934579380L),(mk_real_int64 55402876818758979L);(* 17, 16 *)
(mk_real_int64 17478150331965120L),(mk_real_int64 589239857585307560L);(* 16, 17 *)
(mk_real_int64 109581539444833200L),(mk_real_int64 355880822933535285L);(* 17, 17 *)
(mk_real_int64 29712032115734024L),(mk_real_int64 591375581400199224L);(* 16, 17 *)
(mk_real_int64 205448206201777448L),(mk_real_int64 229410595119248190L);(* 17, 17 *)
(mk_real_int64 180715357660899024L),(mk_real_int64 820394344313280954L);(* 17, 17 *)
(mk_real_int64 3208513901620940L),(mk_real_int64 630308329531850220L);(* 15, 17 *)
(mk_real_int64 108239696293847472L),(mk_real_int64 217696934850047166L);(* 17, 17 *)
(mk_real_int64 3278646456054860L),(mk_real_int64 87230369675115500L);(* 15, 16 *)
(mk_real_int64 190658228364689165L),(mk_real_int64 583771138523183016L);(* 17, 17 *)
(mk_real_int64 522441559935677431L),(mk_real_int64 151881200544040829L);(* 17, 17 *)
(mk_real_int64 632112321944825842L),(mk_real_int64 702550956543485L);(* 17, 14 *)
(mk_real_int64 430393736487154041L),(mk_real_int64 35699556543230259L);(* 17, 16 *)
(mk_real_int64 48659693605499419L),(mk_real_int64 69209942882719290L);(* 16, 16 *)
(mk_real_int64 275760265815429915L),(mk_real_int64 22808169388131530L);(* 17, 16 *)
(mk_real_int64 462937606973496754L),(mk_real_int64 184070636852543280L);(* 17, 17 *)
(mk_real_int64 574842697987773960L),(mk_real_int64 595010128197365239L);(* 17, 17 *)
(mk_real_int64 442296715147222500L),(mk_real_int64 325935069106206400L);(* 17, 17 *)
(mk_real_int64 172005190044720840L),(mk_real_int64 290996261740193775L);(* 17, 17 *)
(mk_real_int64 591492781147993832L),(mk_real_int64 234319844823734325L);(* 17, 17 *)
(mk_real_int64 698087689456918596L),(mk_real_int64 159884434995535044L);(* 17, 17 *)
(mk_real_int64 158778992549916840L),(mk_real_int64 304105039337086650L);(* 17, 17 *)
(mk_real_int64 166863446198837475L),(mk_real_int64 18108059250851009L);(* 17, 16 *)
(mk_real_int64 126463954150142685L),(mk_real_int64 101730449428039208L);(* 17, 17 *)
(mk_real_int64 15913350915986160L),(mk_real_int64 109001895371971846L);(* 16, 17 *)
(mk_real_int64 5940942356202987L),(mk_real_int64 213057784576916136L);(* 15, 17 *)
(mk_real_int64 100625553784011648L),(mk_real_int64 249172447774652180L);(* 17, 17 *)
(mk_real_int64 597283421606798304L),(mk_real_int64 58733029901475297L);(* 17, 16 *)
(mk_real_int64 52036769592637940L),(mk_real_int64 113989812766825788L);(* 16, 17 *)
(mk_real_int64 553919213993684436L),(mk_real_int64 33105454005133150L);(* 17, 16 *)
(mk_real_int64 218110100398360212L),(mk_real_int64 131254967377563600L)(* 17, 17 *)
];;