let data = [
(mk_real_int (num_of_string "122296604108918879616753777")),(mk_real_int (num_of_string "239583034835457602457170160"));(* 26, 26 *)
(mk_real_int (num_of_string "116945034742723939605374625")),(mk_real_int (num_of_string "125034640094443853206382950"));(* 26, 26 *)
(mk_real_int (num_of_string "256159296716627591337252993")),(mk_real_int (num_of_string "29686298930505441130550938"));(* 26, 25 *)
(mk_real_int (num_of_string "211310562458108613257922016")),(mk_real_int (num_of_string "22602159551554455880029660"));(* 26, 25 *)
(mk_real_int (num_of_string "201429551492824537118121130")),(mk_real_int (num_of_string "52092940603790257161777945"));(* 26, 25 *)
(mk_real_int (num_of_string "54519196153497193827457860")),(mk_real_int (num_of_string "224133888884095562962826880"));(* 25, 26 *)
(mk_real_int (num_of_string "5849599436337919403873424")),(mk_real_int (num_of_string "235227762937248968939586600"));(* 24, 26 *)
(mk_real_int (num_of_string "10967558299264651634687060")),(mk_real_int (num_of_string "329615692237334853724105492"));(* 25, 26 *)
(mk_real_int (num_of_string "20141123268528643579807125")),(mk_real_int (num_of_string "143819191598285367979484040"));(* 25, 26 *)
(mk_real_int (num_of_string "146902580132601563038105243")),(mk_real_int (num_of_string "412617302837237033041285431"));(* 26, 26 *)
(mk_real_int (num_of_string "11816007093635777330403222")),(mk_real_int (num_of_string "673075921862048121915357255"));(* 25, 26 *)
(mk_real_int (num_of_string "109588668779355489159457021")),(mk_real_int (num_of_string "87236743533416743592416552"));(* 26, 25 *)
(mk_real_int (num_of_string "342243394955806544573536461")),(mk_real_int (num_of_string "58699938997035262302742080"));(* 26, 25 *)
(mk_real_int (num_of_string "61447529885311484152274520")),(mk_real_int (num_of_string "29352403770943713801710184"));(* 25, 25 *)
(mk_real_int (num_of_string "249447635048403630529305066")),(mk_real_int (num_of_string "515635526938046418542763984"));(* 26, 26 *)
(mk_real_int (num_of_string "91984661280919854644641920")),(mk_real_int (num_of_string "99438823449764306228010000"));(* 25, 25 *)
(mk_real_int (num_of_string "114056446535802862628551308")),(mk_real_int (num_of_string "8873922455091604177476908"));(* 26, 24 *)
(mk_real_int (num_of_string "38900382230806030194676962")),(mk_real_int (num_of_string "185027347257370294393846710"));(* 25, 26 *)
(mk_real_int (num_of_string "38888182784457895443259744")),(mk_real_int (num_of_string "15200410026967886428789476"));(* 25, 25 *)
(mk_real_int (num_of_string "16373330744761859255164820")),(mk_real_int (num_of_string "238707921968378468710053180"));(* 25, 26 *)
(mk_real_int (num_of_string "516653761295347857092340")),(mk_real_int (num_of_string "37358403966703003792941150"));(* 23, 25 *)
(mk_real_int (num_of_string "265708146265094666098978776")),(mk_real_int (num_of_string "102516874289417821378184644"));(* 26, 26 *)
(mk_real_int (num_of_string "25650219831860326736947584")),(mk_real_int (num_of_string "85337322043862134194142480"));(* 25, 25 *)
(mk_real_int (num_of_string "10105610394265413219412542")),(mk_real_int (num_of_string "262445381834386046609943840"));(* 25, 26 *)
(mk_real_int (num_of_string "88308250498239930013115736")),(mk_real_int (num_of_string "72031612659799292252853360"));(* 25, 25 *)
(mk_real_int (num_of_string "9688922093748114564603426")),(mk_real_int (num_of_string "149521565948861149253524623"));(* 24, 26 *)
(mk_real_int (num_of_string "464348133595924675245309415")),(mk_real_int (num_of_string "25921289950470066579882210"));(* 26, 25 *)
(mk_real_int (num_of_string "45975417098065808839903950")),(mk_real_int (num_of_string "289030250219264603957007360"));(* 25, 26 *)
(mk_real_int (num_of_string "311472398931595271142697200")),(mk_real_int (num_of_string "9391873965493630587272120"));(* 26, 24 *)
(mk_real_int (num_of_string "6930039198194761258206675")),(mk_real_int (num_of_string "15665014657933557411415752"));(* 24, 25 *)
(mk_real_int (num_of_string "7051585105275031454201178")),(mk_real_int (num_of_string "4890103428669738702716412"));(* 24, 24 *)
(mk_real_int (num_of_string "320586921822317611308714384")),(mk_real_int (num_of_string "4665234470258224233623410"));(* 26, 24 *)
(mk_real_int (num_of_string "239009267491273723119988620")),(mk_real_int (num_of_string "244047522691363527842116950"));(* 26, 26 *)
(mk_real_int (num_of_string "773412347805877673800530000")),(mk_real_int (num_of_string "6015077155519403838909345"));(* 26, 24 *)
(mk_real_int (num_of_string "169451911826965369400274450")),(mk_real_int (num_of_string "400214814225619489601757984"));(* 26, 26 *)
(mk_real_int (num_of_string "11486196825068175613232850")),(mk_real_int (num_of_string "13730348576841391955840800"));(* 25, 25 *)
(mk_real_int (num_of_string "10805944849879881845595456")),(mk_real_int (num_of_string "116285726927571637536507360"));(* 25, 26 *)
(mk_real_int (num_of_string "35672973776438726812750848")),(mk_real_int (num_of_string "6979229980509338537479824"));(* 25, 24 *)
(mk_real_int (num_of_string "167956383021033967532182890")),(mk_real_int (num_of_string "78815429387373319861721200"));(* 26, 25 *)
(mk_real_int (num_of_string "55592270499273006069003004")),(mk_real_int (num_of_string "115689099802068224390875296"));(* 25, 26 *)
(mk_real_int (num_of_string "239377923715190559271364439")),(mk_real_int (num_of_string "1071478132300090860323496"));(* 26, 24 *)
(mk_real_int (num_of_string "7585018042065708905106006")),(mk_real_int (num_of_string "1917908528926199082346920"));(* 24, 24 *)
(mk_real_int (num_of_string "42795227065171440418528200")),(mk_real_int (num_of_string "130417754766803596489348320"));(* 25, 26 *)
(mk_real_int (num_of_string "577988343855988237130322384")),(mk_real_int (num_of_string "186779197477012548344362440"));(* 26, 26 *)
(mk_real_int (num_of_string "264678339276426421225228140")),(mk_real_int (num_of_string "168232611913624945346307725"));(* 26, 26 *)
(mk_real_int (num_of_string "30193748763728812301288706")),(mk_real_int (num_of_string "119058203192438357720745600"));(* 25, 26 *)
(mk_real_int (num_of_string "964603332521121539295504")),(mk_real_int (num_of_string "82856398064672208460860660"));(* 23, 25 *)
(mk_real_int (num_of_string "213716681894556831842914832")),(mk_real_int (num_of_string "73146463180354547841908520"));(* 26, 25 *)
(mk_real_int (num_of_string "280903518840595529637599808")),(mk_real_int (num_of_string "36183357905839146617833152"));(* 26, 25 *)
(mk_real_int (num_of_string "205641314336110954224319632")),(mk_real_int (num_of_string "5930501169851541784159311"));(* 26, 24 *)
(mk_real_int (num_of_string "27607540673294163577200000")),(mk_real_int (num_of_string "163608860944099539066640646"));(* 25, 26 *)
(mk_real_int (num_of_string "65764990937679944781780525")),(mk_real_int (num_of_string "6124567987017197694936624"));(* 25, 24 *)
(mk_real_int (num_of_string "31423914558922212661979680")),(mk_real_int (num_of_string "34420177802591330729427251"));(* 25, 25 *)
(mk_real_int (num_of_string "6546495229193988932848980")),(mk_real_int (num_of_string "30081208215835147716322692"));(* 24, 25 *)
(mk_real_int (num_of_string "235186824270729261295613586")),(mk_real_int (num_of_string "88283497639442829956624860"));(* 26, 25 *)
(mk_real_int (num_of_string "679879289035623425822645920")),(mk_real_int (num_of_string "149033570404548009950170056"));(* 26, 26 *)
(mk_real_int (num_of_string "70819284950622441494899200")),(mk_real_int (num_of_string "108527492648313858039168440"));(* 25, 26 *)
(mk_real_int (num_of_string "380875336309314936818341200")),(mk_real_int (num_of_string "93531958806085761208141650"));(* 26, 25 *)
(mk_real_int (num_of_string "193845850035680127763097100")),(mk_real_int (num_of_string "169972048797193342777184630"));(* 26, 26 *)
(mk_real_int (num_of_string "48373371773342715081888475")),(mk_real_int (num_of_string "42551853821775032790271860"));(* 25, 25 *)
(mk_real_int (num_of_string "274290436949962761853372936")),(mk_real_int (num_of_string "258074625667727298015429360"));(* 26, 26 *)
(mk_real_int (num_of_string "6984792919539593522620650")),(mk_real_int (num_of_string "319142462240555824876094691"));(* 24, 26 *)
(mk_real_int (num_of_string "137436429614148856052824900")),(mk_real_int (num_of_string "18122163124518259529480784"));(* 26, 25 *)
(mk_real_int (num_of_string "33856855454038965363529125")),(mk_real_int (num_of_string "11654878023885061460206140"));(* 25, 25 *)
(mk_real_int (num_of_string "18520676608993509653080560")),(mk_real_int (num_of_string "6486267997167307423986912"));(* 25, 24 *)
(mk_real_int (num_of_string "149459752858712606316542736")),(mk_real_int (num_of_string "15233082797907839615775360"));(* 26, 25 *)
(mk_real_int (num_of_string "32596301636061327721582740")),(mk_real_int (num_of_string "12517903918470482054187292"));(* 25, 25 *)
(mk_real_int (num_of_string "26964931195905096342972603")),(mk_real_int (num_of_string "25659752736978568289826836"));(* 25, 25 *)
(mk_real_int (num_of_string "137371439903019016490168779")),(mk_real_int (num_of_string "48719844056903214770967980"));(* 26, 25 *)
(mk_real_int (num_of_string "5170760341507459021209615")),(mk_real_int (num_of_string "285910168967261127184174240"));(* 24, 26 *)
(mk_real_int (num_of_string "30326942514639785867733660")),(mk_real_int (num_of_string "8145193420627196408048640"));(* 25, 24 *)
(mk_real_int (num_of_string "414751282640045513467056920")),(mk_real_int (num_of_string "106953336452550372369574780"));(* 26, 26 *)
(mk_real_int (num_of_string "278800810580715558302832600")),(mk_real_int (num_of_string "111065220126607028432625284"));(* 26, 26 *)
(mk_real_int (num_of_string "296673180910697285946316485")),(mk_real_int (num_of_string "8277381122126293975961664"));(* 26, 24 *)
(mk_real_int (num_of_string "23587019090014470423090492")),(mk_real_int (num_of_string "254399069989333800236141424"));(* 25, 26 *)
(mk_real_int (num_of_string "205040832735555207694113510")),(mk_real_int (num_of_string "37142148734658265092449130"));(* 26, 25 *)
(mk_real_int (num_of_string "479182093798690489170020252")),(mk_real_int (num_of_string "15335961652195726447514240"));(* 26, 25 *)
(mk_real_int (num_of_string "391291462717706087293628988")),(mk_real_int (num_of_string "36793310848265802287142840"));(* 26, 25 *)
(mk_real_int (num_of_string "163554931019212560730838880")),(mk_real_int (num_of_string "88131965722697304757320720"));(* 26, 25 *)
(mk_real_int (num_of_string "21892085081322067791687640")),(mk_real_int (num_of_string "76236459557918426484061890"));(* 25, 25 *)
(mk_real_int (num_of_string "168452709915087795183456960")),(mk_real_int (num_of_string "450466494317901078761194416"));(* 26, 26 *)
(mk_real_int (num_of_string "148107148078634853734210256")),(mk_real_int (num_of_string "33539540299555915477678584"));(* 26, 25 *)
(mk_real_int (num_of_string "1777727230405376624032500")),(mk_real_int (num_of_string "352476769077679752975470040"));(* 24, 26 *)
(mk_real_int (num_of_string "273806574280534970304870276")),(mk_real_int (num_of_string "22601499843669729020881920"));(* 26, 25 *)
(mk_real_int (num_of_string "3177165815192737814394621")),(mk_real_int (num_of_string "3274242796491171245437200"));(* 24, 24 *)
(mk_real_int (num_of_string "306356941048511609779406202")),(mk_real_int (num_of_string "407182235348746786554812979"));(* 26, 26 *)
(mk_real_int (num_of_string "426089330439666827408413020")),(mk_real_int (num_of_string "28283577559211813428556274"));(* 26, 25 *)
(mk_real_int (num_of_string "45487144490236685427975002")),(mk_real_int (num_of_string "236583708919837816320407676"));(* 25, 26 *)
(mk_real_int (num_of_string "52844727384797157888661170")),(mk_real_int (num_of_string "45700575411275219201452378"));(* 25, 25 *)
(mk_real_int (num_of_string "198142286574291102622697085")),(mk_real_int (num_of_string "5967205562600088616678338"));(* 26, 24 *)
(mk_real_int (num_of_string "52758260168618325324972696")),(mk_real_int (num_of_string "7301552728728367975178570"));(* 25, 24 *)
(mk_real_int (num_of_string "202297732544125539523288944")),(mk_real_int (num_of_string "17538288369944641688777856"));(* 26, 25 *)
(mk_real_int (num_of_string "351512252394655059153856936")),(mk_real_int (num_of_string "120728778635979249240259440"));(* 26, 26 *)
(mk_real_int (num_of_string "94830911181927748425538656")),(mk_real_int (num_of_string "222681128727303434175159060"));(* 25, 26 *)
(mk_real_int (num_of_string "18586076205336951289408560")),(mk_real_int (num_of_string "24068502512141965762490900"));(* 25, 25 *)
(mk_real_int (num_of_string "3181526704162247758424856")),(mk_real_int (num_of_string "29557513766521654550747760"));(* 24, 25 *)
(mk_real_int (num_of_string "46959178587563069038963368")),(mk_real_int (num_of_string "288790027821147791750074254"));(* 25, 26 *)
(mk_real_int (num_of_string "13575613573968363115898112")),(mk_real_int (num_of_string "80189754192456666015806324"));(* 25, 25 *)
(mk_real_int (num_of_string "37405442283405685594460928")),(mk_real_int (num_of_string "100197995659768405914262880"));(* 25, 26 *)
(mk_real_int (num_of_string "35655023341524545254275108")),(mk_real_int (num_of_string "12243096216892745827677600"));(* 25, 25 *)
(mk_real_int (num_of_string "7917958776144735309696480")),(mk_real_int (num_of_string "59424838177718067061998432"));(* 24, 25 *)
(mk_real_int (num_of_string "186629399414377955116382484")),(mk_real_int (num_of_string "2711972984221348107107925"));(* 26, 24 *)
(mk_real_int (num_of_string "180616296329587638628430400")),(mk_real_int (num_of_string "3751353127992333167608280"));(* 26, 24 *)
(mk_real_int (num_of_string "17001106507386701740652496")),(mk_real_int (num_of_string "463383521709868689942674496"));(* 25, 26 *)
(mk_real_int (num_of_string "38351551619723864678373800")),(mk_real_int (num_of_string "29135018552152178721431025"));(* 25, 25 *)
(mk_real_int (num_of_string "145760287695241769690288904")),(mk_real_int (num_of_string "556599499095128133823565376"));(* 26, 26 *)
(mk_real_int (num_of_string "38764141869006054397795392")),(mk_real_int (num_of_string "286488447731058847244522112"));(* 25, 26 *)
(mk_real_int (num_of_string "103037027003207435398754348")),(mk_real_int (num_of_string "183488774591362279029739098"));(* 26, 26 *)
(mk_real_int (num_of_string "13040587597488257446325004")),(mk_real_int (num_of_string "13029876036871373976400500"));(* 25, 25 *)
(mk_real_int (num_of_string "88923590459786533250887776")),(mk_real_int (num_of_string "312305367666090840527632608"));(* 25, 26 *)
(mk_real_int (num_of_string "1378621545674061638029899")),(mk_real_int (num_of_string "16835131013553370128016960"));(* 24, 25 *)
(mk_real_int (num_of_string "157651619354455521985757760")),(mk_real_int (num_of_string "4685875316911634091501024"));(* 26, 24 *)
(mk_real_int (num_of_string "41983181291678131184428511")),(mk_real_int (num_of_string "54554767774872291130512"));(* 25, 22 *)
(mk_real_int (num_of_string "73948104126967151252655918")),(mk_real_int (num_of_string "11937856765363411200549492"));(* 25, 25 *)
(mk_real_int (num_of_string "2519336180493844902297600")),(mk_real_int (num_of_string "162332595602835222812713440"));(* 24, 26 *)
(mk_real_int (num_of_string "36190062254479271100341925")),(mk_real_int (num_of_string "25372813951963902310685505"));(* 25, 25 *)
(mk_real_int (num_of_string "164735298270801827011478560")),(mk_real_int (num_of_string "341453810953050156673488827"));(* 26, 26 *)
(mk_real_int (num_of_string "112078046223133398245013516")),(mk_real_int (num_of_string "130502437785361915166995056"));(* 26, 26 *)
(mk_real_int (num_of_string "80563919988599768472620715")),(mk_real_int (num_of_string "153085940093280942460979200"));(* 25, 26 *)
(mk_real_int (num_of_string "10317190683828147549033898")),(mk_real_int (num_of_string "42948033370534452404223096"));(* 25, 25 *)
(mk_real_int (num_of_string "254651577115191268844484288")),(mk_real_int (num_of_string "155384549986315862060215780"));(* 26, 26 *)
(mk_real_int (num_of_string "277319039435137429054579548")),(mk_real_int (num_of_string "221230866080980092766290530"));(* 26, 26 *)
(mk_real_int (num_of_string "4363842981461224343337600")),(mk_real_int (num_of_string "569821164924757584189846000"));(* 24, 26 *)
(mk_real_int (num_of_string "124113784226014765047403200")),(mk_real_int (num_of_string "1258860931580921878349841"));(* 26, 24 *)
(mk_real_int (num_of_string "53460451206916873643632626")),(mk_real_int (num_of_string "56208279601058221102301820"));(* 25, 25 *)
(mk_real_int (num_of_string "10862370499164598507832538")),(mk_real_int (num_of_string "192745386228048481691803408"));(* 25, 26 *)
(mk_real_int (num_of_string "4106008388722064473339152")),(mk_real_int (num_of_string "358297002439618415107600686"));(* 24, 26 *)
(mk_real_int (num_of_string "27419318980412410993175520")),(mk_real_int (num_of_string "80202736827797959263657860"));(* 25, 25 *)
(mk_real_int (num_of_string "47251968512513000135215680")),(mk_real_int (num_of_string "461200816990601812603354260"));(* 25, 26 *)
(mk_real_int (num_of_string "52960240373937217529946206")),(mk_real_int (num_of_string "74674198190313753938790510"));(* 25, 25 *)
(mk_real_int (num_of_string "6154112385062118049435800")),(mk_real_int (num_of_string "57525673380509137850275880"));(* 24, 25 *)
(mk_real_int (num_of_string "763025564928732901778520")),(mk_real_int (num_of_string "166847255806675895511511680"));(* 23, 26 *)
(mk_real_int (num_of_string "49857994615030998639694346")),(mk_real_int (num_of_string "16161005939868816690103825"));(* 25, 25 *)
(mk_real_int (num_of_string "60445721406002507261075808")),(mk_real_int (num_of_string "9183397773792697297117800"));(* 25, 24 *)
(mk_real_int (num_of_string "57509791427373035664640672")),(mk_real_int (num_of_string "425879000513212834765050692"));(* 25, 26 *)
(mk_real_int (num_of_string "150551420299712970337985349")),(mk_real_int (num_of_string "8478037403407779336059112"));(* 26, 24 *)
(mk_real_int (num_of_string "189305705647007063646320115")),(mk_real_int (num_of_string "57088640728074251334710000"));(* 26, 25 *)
(mk_real_int (num_of_string "155713151419371690239361240")),(mk_real_int (num_of_string "6490164450620716838423920"));(* 26, 24 *)
(mk_real_int (num_of_string "180018318707772001422729000")),(mk_real_int (num_of_string "176899079454530524596941504"));(* 26, 26 *)
(mk_real_int (num_of_string "98246598880664439805952")),(mk_real_int (num_of_string "162354057912724717118940900"));(* 22, 26 *)
(mk_real_int (num_of_string "78269683850821904971838308")),(mk_real_int (num_of_string "91424387897791188356264070"));(* 25, 25 *)
(mk_real_int (num_of_string "4370672755263901487913000")),(mk_real_int (num_of_string "78212978187652211045612470"));(* 24, 25 *)
(mk_real_int (num_of_string "43953439624864637470298640")),(mk_real_int (num_of_string "7482811090223673532142000"));(* 25, 24 *)
(mk_real_int (num_of_string "1509625066426809753652154")),(mk_real_int (num_of_string "311479525686656890468389120"));(* 24, 26 *)
(mk_real_int (num_of_string "322471838912406458930353")),(mk_real_int (num_of_string "253856088308010623186800458"));(* 23, 26 *)
(mk_real_int (num_of_string "14124195143826836015806956")),(mk_real_int (num_of_string "22645363516293571358488400"));(* 25, 25 *)
(mk_real_int (num_of_string "11469795158684644106211120")),(mk_real_int (num_of_string "6260226998742971166776850"));(* 25, 24 *)
(mk_real_int (num_of_string "88291840844021735205647637")),(mk_real_int (num_of_string "122970736417675351892613300"));(* 25, 26 *)
(mk_real_int (num_of_string "15396027982411394689128")),(mk_real_int (num_of_string "107337818640332974871667420"));(* 22, 26 *)
(mk_real_int (num_of_string "36033211321296681894326496")),(mk_real_int (num_of_string "4351150522892935100979600"));(* 25, 24 *)
(mk_real_int (num_of_string "3800780938063746562578720")),(mk_real_int (num_of_string "44296666340457172906012320"));(* 24, 25 *)
(mk_real_int (num_of_string "77741643353314463368173200")),(mk_real_int (num_of_string "80189736288510531327928634"));(* 25, 25 *)
(mk_real_int (num_of_string "366643880037271847021293125")),(mk_real_int (num_of_string "232919543426390416887066880"));(* 26, 26 *)
(mk_real_int (num_of_string "136815839344522518087569816")),(mk_real_int (num_of_string "42119075414490876883248720"));(* 26, 25 *)
(mk_real_int (num_of_string "572342331264280064522736")),(mk_real_int (num_of_string "175158984991518519343893932"));(* 23, 26 *)
(mk_real_int (num_of_string "34286452610024448880160240")),(mk_real_int (num_of_string "15045816425518525880718852"));(* 25, 25 *)
(mk_real_int (num_of_string "208398612216264949978758")),(mk_real_int (num_of_string "6805634625186026783180160"));(* 23, 24 *)
(mk_real_int (num_of_string "216792870879872789809700160")),(mk_real_int (num_of_string "2891390097587707455885315"));(* 26, 24 *)
(mk_real_int (num_of_string "262811192980022937188137062")),(mk_real_int (num_of_string "609773424102286131460604260"));(* 26, 26 *)
(mk_real_int (num_of_string "180730531540424393494848")),(mk_real_int (num_of_string "9590412607608888532027320"));(* 23, 24 *)
(mk_real_int (num_of_string "15765996527362898796203640")),(mk_real_int (num_of_string "1658885785061453439964584"));(* 25, 24 *)
(mk_real_int (num_of_string "4300993303195663068441930")),(mk_real_int (num_of_string "85080718024042001923089050"));(* 24, 25 *)
(mk_real_int (num_of_string "39250293845039188865664480")),(mk_real_int (num_of_string "3284549760329707201962672"));(* 25, 24 *)
(mk_real_int (num_of_string "109852745347167805114094280")),(mk_real_int (num_of_string "3136634082216472570747490"));(* 26, 24 *)
(mk_real_int (num_of_string "163751154760696731539842440")),(mk_real_int (num_of_string "17149697061479497135220625"));(* 26, 25 *)
(mk_real_int (num_of_string "45779475364243424158384008")),(mk_real_int (num_of_string "1401818666829818844925656"));(* 25, 24 *)
(mk_real_int (num_of_string "5984018026900435301109120")),(mk_real_int (num_of_string "152838878148709767757750644"));(* 24, 26 *)
(mk_real_int (num_of_string "117891681923283702680747620")),(mk_real_int (num_of_string "179046091585070123094076220"));(* 26, 26 *)
(mk_real_int (num_of_string "460126616801207493606944256")),(mk_real_int (num_of_string "29790677442619849644815904"));(* 26, 25 *)
(mk_real_int (num_of_string "16107058132958316719507585")),(mk_real_int (num_of_string "107166588389414656364129320"));(* 25, 26 *)
(mk_real_int (num_of_string "15507656966133368596156800")),(mk_real_int (num_of_string "104532587906982917431004880"));(* 25, 26 *)
(mk_real_int (num_of_string "210251612714981675572099904")),(mk_real_int (num_of_string "152709463817527667365508050"));(* 26, 26 *)
(mk_real_int (num_of_string "218913858876466893783425560")),(mk_real_int (num_of_string "193307160392015588979762000"));(* 26, 26 *)
(mk_real_int (num_of_string "145751565881074124064958501")),(mk_real_int (num_of_string "202488068529689306930770400"));(* 26, 26 *)
(mk_real_int (num_of_string "20101164833626164653625")),(mk_real_int (num_of_string "137580094437379198216966590"));(* 22, 26 *)
(mk_real_int (num_of_string "67795873951403450803411120")),(mk_real_int (num_of_string "128223868897406025168213560"));(* 25, 26 *)
(mk_real_int (num_of_string "61142133965299536252144576")),(mk_real_int (num_of_string "131275311523099442986659912"));(* 25, 26 *)
(mk_real_int (num_of_string "3281123380326310477786500")),(mk_real_int (num_of_string "70080013474875475894847724"));(* 24, 25 *)
(mk_real_int (num_of_string "216415387485639539038630360")),(mk_real_int (num_of_string "131492970594504376642115980"));(* 26, 26 *)
(mk_real_int (num_of_string "107021157667215831922896804")),(mk_real_int (num_of_string "387692730323519063269056000"));(* 26, 26 *)
(mk_real_int (num_of_string "3617979646569187774526520")),(mk_real_int (num_of_string "550700179191680802652509336"));(* 24, 26 *)
(mk_real_int (num_of_string "11428994137080772970709840")),(mk_real_int (num_of_string "124914502676296451522136030"));(* 25, 26 *)
(mk_real_int (num_of_string "1927127090232028554147720")),(mk_real_int (num_of_string "174825737576319399990841408"));(* 24, 26 *)
(mk_real_int (num_of_string "92596174146436261599280710")),(mk_real_int (num_of_string "213368395739247296427956321"));(* 25, 26 *)
(mk_real_int (num_of_string "50597744458836280633079400")),(mk_real_int (num_of_string "332921510413679088567401481"));(* 25, 26 *)
(mk_real_int (num_of_string "22253673914077713692423280")),(mk_real_int (num_of_string "25288380849397262496659136"));(* 25, 25 *)
(mk_real_int (num_of_string "271128881527516233196415244")),(mk_real_int (num_of_string "20565373958952286285602000"));(* 26, 25 *)
(mk_real_int (num_of_string "52565824824333345395540250")),(mk_real_int (num_of_string "105236602650401585076682221"));(* 25, 26 *)
(mk_real_int (num_of_string "123827650708729353651421420")),(mk_real_int (num_of_string "192622321039696560539083250"));(* 26, 26 *)
(mk_real_int (num_of_string "145900747289070391812334900")),(mk_real_int (num_of_string "157256408866753391334542920"));(* 26, 26 *)
(mk_real_int (num_of_string "21932979102830743406596224")),(mk_real_int (num_of_string "4725176688961768698352644"));(* 25, 24 *)
(mk_real_int (num_of_string "53619267341506189699951776")),(mk_real_int (num_of_string "405319022905367495796409998"));(* 25, 26 *)
(mk_real_int (num_of_string "8296879628962431522164316")),(mk_real_int (num_of_string "6586069741133150432312736"));(* 24, 24 *)
(mk_real_int (num_of_string "83710899686235730987977360")),(mk_real_int (num_of_string "211741104597082483904615328"));(* 25, 26 *)
(mk_real_int (num_of_string "722819963655752067020386800")),(mk_real_int (num_of_string "66957118629737374421720040"));(* 26, 25 *)
(mk_real_int (num_of_string "66684917472312841126254432")),(mk_real_int (num_of_string "38782472071178353533595980"));(* 25, 25 *)
(mk_real_int (num_of_string "131659265559061397213579264")),(mk_real_int (num_of_string "165508047285526878888372373"));(* 26, 26 *)
(mk_real_int (num_of_string "13231585070318138540816372")),(mk_real_int (num_of_string "3476520514842629755371200"));(* 25, 24 *)
(mk_real_int (num_of_string "346455904580011363146375357")),(mk_real_int (num_of_string "246108341931215986754431200"));(* 26, 26 *)
(mk_real_int (num_of_string "3612775780717498603528740")),(mk_real_int (num_of_string "79271523347332962718180894"));(* 24, 25 *)
(mk_real_int (num_of_string "2154701515362019853271552")),(mk_real_int (num_of_string "160712239582408695464826324"));(* 24, 26 *)
(mk_real_int (num_of_string "26731969409821149565203450")),(mk_real_int (num_of_string "250067539160766843716806898"));(* 25, 26 *)
(mk_real_int (num_of_string "455654757548654366039556660")),(mk_real_int (num_of_string "39321271453864735847046150"));(* 26, 25 *)
(mk_real_int (num_of_string "14833308545689636392511000")),(mk_real_int (num_of_string "67008543496344317900260800"));(* 25, 25 *)
(mk_real_int (num_of_string "285717395376322978177623438")),(mk_real_int (num_of_string "260358573951865796592994830"));(* 26, 26 *)
(mk_real_int (num_of_string "28061646315274832856122700")),(mk_real_int (num_of_string "122195022953189660793712960"));(* 25, 26 *)
(mk_real_int (num_of_string "116371628285855245795403275")),(mk_real_int (num_of_string "54165462576192638720945532"));(* 26, 25 *)
(mk_real_int (num_of_string "283750387415357891016428649")),(mk_real_int (num_of_string "9263051188667075197328190"));(* 26, 24 *)
(mk_real_int (num_of_string "168447238167298273265238464")),(mk_real_int (num_of_string "34347960697304086007579712"));(* 26, 25 *)
(mk_real_int (num_of_string "111414721398094193336331606")),(mk_real_int (num_of_string "1572278427812878224716250"));(* 26, 24 *)
(mk_real_int (num_of_string "85424345748758887909684884")),(mk_real_int (num_of_string "53634214036552931078913960"));(* 25, 25 *)
(mk_real_int (num_of_string "433186206909109143113603370")),(mk_real_int (num_of_string "127346213092884213449521500"));(* 26, 26 *)
(mk_real_int (num_of_string "276721457988623553175029760")),(mk_real_int (num_of_string "130145827557924193888669824"));(* 26, 26 *)
(mk_real_int (num_of_string "171970508473947028860509985")),(mk_real_int (num_of_string "63692871133755993015735750"));(* 26, 25 *)
(mk_real_int (num_of_string "42144108424800663673151000")),(mk_real_int (num_of_string "83156496837150767474254080"));(* 25, 25 *)
(mk_real_int (num_of_string "463524504251353022442096")),(mk_real_int (num_of_string "25215178586886634091083104"));(* 23, 25 *)
(mk_real_int (num_of_string "4003282888450251105743603")),(mk_real_int (num_of_string "37617476574130415722490400"));(* 24, 25 *)
(mk_real_int (num_of_string "2303641521195402675183960")),(mk_real_int (num_of_string "11765148318925111873654000"));(* 24, 25 *)
(mk_real_int (num_of_string "42547756127261226763218921")),(mk_real_int (num_of_string "38355758482606505161824150"));(* 25, 25 *)
(mk_real_int (num_of_string "78722930494039920296960772")),(mk_real_int (num_of_string "3470847025527210439774848"));(* 25, 24 *)
(mk_real_int (num_of_string "24391976623918082149024335")),(mk_real_int (num_of_string "30855027740775287834747600"));(* 25, 25 *)
(mk_real_int (num_of_string "151631936507900577369097779")),(mk_real_int (num_of_string "128577869325022238111183404"));(* 26, 26 *)
(mk_real_int (num_of_string "691302673454697863781844025")),(mk_real_int (num_of_string "1739551481345983869408000"));(* 26, 24 *)
(mk_real_int (num_of_string "63619378184111182872159330")),(mk_real_int (num_of_string "11478610084878288820876950"));(* 25, 25 *)
(mk_real_int (num_of_string "68576922562396998506008320")),(mk_real_int (num_of_string "326029040147256049160961088"));(* 25, 26 *)
(mk_real_int (num_of_string "30001128650415805819381704")),(mk_real_int (num_of_string "22738441862746931392302390"));(* 25, 25 *)
(mk_real_int (num_of_string "225226436764705216915893550")),(mk_real_int (num_of_string "4808403312323680157761500"));(* 26, 24 *)
(mk_real_int (num_of_string "1097741458398821296367904")),(mk_real_int (num_of_string "20351048773537304534729940"));(* 24, 25 *)
(mk_real_int (num_of_string "94750343053496362421391306")),(mk_real_int (num_of_string "3484089270790262759746800"));(* 25, 24 *)
(mk_real_int (num_of_string "58729188008825051913637200")),(mk_real_int (num_of_string "19122681934976314969249648"));(* 25, 25 *)
(mk_real_int (num_of_string "1598985800722621254955557")),(mk_real_int (num_of_string "15189245690779641936007476"));(* 24, 25 *)
(mk_real_int (num_of_string "76991596567790840390736600")),(mk_real_int (num_of_string "26892182672299755250049400"));(* 25, 25 *)
(mk_real_int (num_of_string "175296844217553885759240")),(mk_real_int (num_of_string "26575774453688179812147880"));(* 23, 25 *)
(mk_real_int (num_of_string "91082232355656771919992978")),(mk_real_int (num_of_string "3461274640635699378135568"));(* 25, 24 *)
(mk_real_int (num_of_string "24214326817518827356436300")),(mk_real_int (num_of_string "84682698359061687457974210"));(* 25, 25 *)
(mk_real_int (num_of_string "377912587222655343107226064")),(mk_real_int (num_of_string "20894890682750963084452544"));(* 26, 25 *)
(mk_real_int (num_of_string "78219383748166702140049909")),(mk_real_int (num_of_string "342199640740501754251467468"));(* 25, 26 *)
(mk_real_int (num_of_string "4086878836774696827899982")),(mk_real_int (num_of_string "28744668571745563398621040"));(* 24, 25 *)
(mk_real_int (num_of_string "177200847300307408024107648")),(mk_real_int (num_of_string "164168860046010066023850432"));(* 26, 26 *)
(mk_real_int (num_of_string "121303223829489625017449805")),(mk_real_int (num_of_string "154471085166320669731198500"));(* 26, 26 *)
(mk_real_int (num_of_string "35590152858302158415051016")),(mk_real_int (num_of_string "1349669297084661854658560"));(* 25, 24 *)
(mk_real_int (num_of_string "47363745829771085777088663")),(mk_real_int (num_of_string "110999653145149068226554540"));(* 25, 26 *)
(mk_real_int (num_of_string "77975968263017087885457024")),(mk_real_int (num_of_string "115985125060170324694017212"));(* 25, 26 *)
(mk_real_int (num_of_string "208249764501878112237403725")),(mk_real_int (num_of_string "15664023934107852486149690"));(* 26, 25 *)
(mk_real_int (num_of_string "53552105000798735149125245")),(mk_real_int (num_of_string "278452447516437925743132800"));(* 25, 26 *)
(mk_real_int (num_of_string "22779138548031551024450627")),(mk_real_int (num_of_string "231033547040116719085437492"));(* 25, 26 *)
(mk_real_int (num_of_string "791619192697104965254002")),(mk_real_int (num_of_string "12353074842850356526390440"));(* 23, 25 *)
(mk_real_int (num_of_string "1333568832869776768514085")),(mk_real_int (num_of_string "25372106043505578336339360"));(* 24, 25 *)
(mk_real_int (num_of_string "249414648449310915026785200")),(mk_real_int (num_of_string "12688238331846734635853880"));(* 26, 25 *)
(mk_real_int (num_of_string "5651800028501052252435372")),(mk_real_int (num_of_string "498911021239689979613598507"));(* 24, 26 *)
(mk_real_int (num_of_string "98171376453633918494315160")),(mk_real_int (num_of_string "47323530346518173138498400"));(* 25, 25 *)
(mk_real_int (num_of_string "65449480750502003933183000")),(mk_real_int (num_of_string "341476452272297833907880"));(* 25, 23 *)
(mk_real_int (num_of_string "267384734993032433105631750")),(mk_real_int (num_of_string "122905461646875268972411128"));(* 26, 26 *)
(mk_real_int (num_of_string "169817166557896873358471968")),(mk_real_int (num_of_string "129724415081091996050147808"));(* 26, 26 *)
(mk_real_int (num_of_string "71406102302013206715930288")),(mk_real_int (num_of_string "50059941053029300015151760"));(* 25, 25 *)
(mk_real_int (num_of_string "151621345139690071605441495")),(mk_real_int (num_of_string "123021470460189010451960664"));(* 26, 26 *)
(mk_real_int (num_of_string "188745223417810876360558574")),(mk_real_int (num_of_string "8704792166624098781967504"));(* 26, 24 *)
(mk_real_int (num_of_string "221469637524313904512459200")),(mk_real_int (num_of_string "156272800370585974114139100"));(* 26, 26 *)
(mk_real_int (num_of_string "179704454814092155313007576")),(mk_real_int (num_of_string "28260825086168456538872412"));(* 26, 25 *)
(mk_real_int (num_of_string "23801195988064436464882412")),(mk_real_int (num_of_string "13844634115737389333053608"));(* 25, 25 *)
(mk_real_int (num_of_string "935120269076416413354784")),(mk_real_int (num_of_string "18316360396740791736713600"));(* 23, 25 *)
(mk_real_int (num_of_string "439654553378026094034892027")),(mk_real_int (num_of_string "255704868816712216625505888"));(* 26, 26 *)
(mk_real_int (num_of_string "170404271361384502816640216")),(mk_real_int (num_of_string "73411266382865898175987872"));(* 26, 25 *)
(mk_real_int (num_of_string "26065271881196103498543360")),(mk_real_int (num_of_string "1467168518470828200661920"));(* 25, 24 *)
(mk_real_int (num_of_string "162404008667094195684949875")),(mk_real_int (num_of_string "18510874775408758976498880"));(* 26, 25 *)
(mk_real_int (num_of_string "1189523359785213273244726")),(mk_real_int (num_of_string "154246600767929003216789940"));(* 24, 26 *)
(mk_real_int (num_of_string "40268440420822140964377731")),(mk_real_int (num_of_string "124840193958411678611982900"));(* 25, 26 *)
(mk_real_int (num_of_string "92121917085434649446294625")),(mk_real_int (num_of_string "16157134192707421607505240"));(* 25, 25 *)
(mk_real_int (num_of_string "6260336821748596523443200")),(mk_real_int (num_of_string "2177611657464423180133809"));(* 24, 24 *)
(mk_real_int (num_of_string "257044154829655968933778737")),(mk_real_int (num_of_string "29636382569978256264895680"));(* 26, 25 *)
(mk_real_int (num_of_string "20528658019508908153513860")),(mk_real_int (num_of_string "226663510943498071387738240"));(* 25, 26 *)
(mk_real_int (num_of_string "136298832643894768365980700")),(mk_real_int (num_of_string "457938627400910750660040528"));(* 26, 26 *)
(mk_real_int (num_of_string "10143974755162581720659732")),(mk_real_int (num_of_string "4554445379489824344437520"));(* 25, 24 *)
(mk_real_int (num_of_string "746650975691005541523960670")),(mk_real_int (num_of_string "501151342154405894561416020"));(* 26, 26 *)
(mk_real_int (num_of_string "2115861390084372281731900")),(mk_real_int (num_of_string "22552692617060839203075210"));(* 24, 25 *)
(mk_real_int (num_of_string "144672288423576808472284980")),(mk_real_int (num_of_string "21587467418466837298873000"));(* 26, 25 *)
(mk_real_int (num_of_string "99166177913705792373794652")),(mk_real_int (num_of_string "55399503361171845399042200"));(* 25, 25 *)
(mk_real_int (num_of_string "10911266770556496368686848")),(mk_real_int (num_of_string "72274381800635561911205016"));(* 25, 25 *)
(mk_real_int (num_of_string "95374392421696729129429740")),(mk_real_int (num_of_string "761650238758906968522148800"));(* 25, 26 *)
(mk_real_int (num_of_string "334999670911003697998173984")),(mk_real_int (num_of_string "349339498842019834350095167"));(* 26, 26 *)
(mk_real_int (num_of_string "19481096934649073534768280")),(mk_real_int (num_of_string "98073334298427664291684596"));(* 25, 25 *)
(mk_real_int (num_of_string "69652099561113619786767825")),(mk_real_int (num_of_string "119485930323691975659768600"));(* 25, 26 *)
(mk_real_int (num_of_string "420981325085031885278769918")),(mk_real_int (num_of_string "127693676481245208704544360"));(* 26, 26 *)
(mk_real_int (num_of_string "81437072843007058251475280")),(mk_real_int (num_of_string "121751149311661223091165688"));(* 25, 26 *)
(mk_real_int (num_of_string "78760344153797936422399010")),(mk_real_int (num_of_string "2703341311232480654359908"));(* 25, 24 *)
(mk_real_int (num_of_string "140942827957367191008626331")),(mk_real_int (num_of_string "136112541803246350083214680"));(* 26, 26 *)
(mk_real_int (num_of_string "19649311627766235054472008")),(mk_real_int (num_of_string "36458341150648949365893696"));(* 25, 25 *)
(mk_real_int (num_of_string "39319054812981361158571656")),(mk_real_int (num_of_string "4057826883759355326568494"));(* 25, 24 *)
(mk_real_int (num_of_string "184005991725426191335324442")),(mk_real_int (num_of_string "4346246400214419458185736"));(* 26, 24 *)
(mk_real_int (num_of_string "425264509091035464498833670")),(mk_real_int (num_of_string "61294187492407534331751216"));(* 26, 25 *)
(mk_real_int (num_of_string "9136612004415326565897750")),(mk_real_int (num_of_string "790756416411378886044558540"));(* 24, 26 *)
(mk_real_int (num_of_string "40438454575867964385525720")),(mk_real_int (num_of_string "3820822329411379636508912"));(* 25, 24 *)
(mk_real_int (num_of_string "39193934531001001806038400")),(mk_real_int (num_of_string "191219248836906452092545536"));(* 25, 26 *)
(mk_real_int (num_of_string "117394682102034495701396907")),(mk_real_int (num_of_string "158818034054787697000460288"));(* 26, 26 *)
(mk_real_int (num_of_string "320342393622039548044025520")),(mk_real_int (num_of_string "10520373134587455374725171"));(* 26, 25 *)
(mk_real_int (num_of_string "145264321348928067731492034")),(mk_real_int (num_of_string "200517754192029576532950840"));(* 26, 26 *)
(mk_real_int (num_of_string "18346476416812155570336840")),(mk_real_int (num_of_string "93990006905369016566412288"));(* 25, 25 *)
(mk_real_int (num_of_string "152911132188658357813764220")),(mk_real_int (num_of_string "103992231165969389263309080"));(* 26, 26 *)
(mk_real_int (num_of_string "86561079185188032007360410")),(mk_real_int (num_of_string "35277132477074026079450385"));(* 25, 25 *)
(mk_real_int (num_of_string "337546437647847779195434380")),(mk_real_int (num_of_string "14935277363350575767175486"));(* 26, 25 *)
(mk_real_int (num_of_string "17097273813574070605285790")),(mk_real_int (num_of_string "5186071674784879537728159"));(* 25, 24 *)
(mk_real_int (num_of_string "326217160548104840752710")),(mk_real_int (num_of_string "26376479325071786217967296"));(* 23, 25 *)
(mk_real_int (num_of_string "31370224784078854121798618")),(mk_real_int (num_of_string "369745899635051925198466168"));(* 25, 26 *)
(mk_real_int (num_of_string "3564672876792062656476768")),(mk_real_int (num_of_string "13891596789897271990316745"));(* 24, 25 *)
(mk_real_int (num_of_string "11164020823659326911944693")),(mk_real_int (num_of_string "222289827913999541367765152"));(* 25, 26 *)
(mk_real_int (num_of_string "17271825516153737279675892")),(mk_real_int (num_of_string "5214953471104995358866618"));(* 25, 24 *)
(mk_real_int (num_of_string "81124162052337625180795965")),(mk_real_int (num_of_string "8086121808049655052405840"));(* 25, 24 *)
(mk_real_int (num_of_string "75712761224488613894822080")),(mk_real_int (num_of_string "125522635234897448796246336"));(* 25, 26 *)
(mk_real_int (num_of_string "477552136999459785314721516")),(mk_real_int (num_of_string "29411812112998008351030210"));(* 26, 25 *)
(mk_real_int (num_of_string "157974988577192674706009445")),(mk_real_int (num_of_string "117023361523828427452955040"));(* 26, 26 *)
(mk_real_int (num_of_string "20810079278373046877771600")),(mk_real_int (num_of_string "216056932110716206477114602"));(* 25, 26 *)
(mk_real_int (num_of_string "1292491457655875927926164")),(mk_real_int (num_of_string "44112696403192072503008448"));(* 24, 25 *)
(mk_real_int (num_of_string "1516877205992956064422880")),(mk_real_int (num_of_string "95217141823572502529195040"));(* 24, 25 *)
(mk_real_int (num_of_string "37710120286683621591354280")),(mk_real_int (num_of_string "230016167686626746599752512"));(* 25, 26 *)
(mk_real_int (num_of_string "214580541914610775879162880")),(mk_real_int (num_of_string "173021393182665467590047912"));(* 26, 26 *)
(mk_real_int (num_of_string "445467144208472460078841859")),(mk_real_int (num_of_string "282165529982023916213308180"));(* 26, 26 *)
(mk_real_int (num_of_string "105713255339627861325205080")),(mk_real_int (num_of_string "11361704716721795431774960"));(* 26, 25 *)
(mk_real_int (num_of_string "146290073345265655177843680")),(mk_real_int (num_of_string "326859616544183386840635684"));(* 26, 26 *)
(mk_real_int (num_of_string "15846606073752848148387150")),(mk_real_int (num_of_string "18453033720278342116175916"));(* 25, 25 *)
(mk_real_int (num_of_string "62392299697841215049339991")),(mk_real_int (num_of_string "94154997760457158280985570"));(* 25, 25 *)
(mk_real_int (num_of_string "11518501323220754877003990")),(mk_real_int (num_of_string "140848861635951052924017656"));(* 25, 26 *)
(mk_real_int (num_of_string "165680608711598373058618540")),(mk_real_int (num_of_string "61634678288421361465050444"));(* 26, 25 *)
(mk_real_int (num_of_string "228742323184818619056656370")),(mk_real_int (num_of_string "330309201657711001582741680"));(* 26, 26 *)
(mk_real_int (num_of_string "10697050156758197420854926")),(mk_real_int (num_of_string "226774333678351045561580970"));(* 25, 26 *)
(mk_real_int (num_of_string "690311643675450478697997")),(mk_real_int (num_of_string "52015333674707430556206132"));(* 23, 25 *)
(mk_real_int (num_of_string "77234443717434484637176020")),(mk_real_int (num_of_string "44293551043235280063842538"));(* 25, 25 *)
(mk_real_int (num_of_string "242472910763615187923188452")),(mk_real_int (num_of_string "1864108712563719808173480"));(* 26, 24 *)
(mk_real_int (num_of_string "942103325629802927449488")),(mk_real_int (num_of_string "49300658157335196910860408"));(* 23, 25 *)
(mk_real_int (num_of_string "46374679458841357569034848")),(mk_real_int (num_of_string "37876945221723903933658968"));(* 25, 25 *)
(mk_real_int (num_of_string "37062505693713928808927664")),(mk_real_int (num_of_string "324200430512423294767344610"));(* 25, 26 *)
(mk_real_int (num_of_string "93639502936705784554146448")),(mk_real_int (num_of_string "257954121166422304657386822"));(* 25, 26 *)
(mk_real_int (num_of_string "47981232447334968948004410")),(mk_real_int (num_of_string "2170194130972064662902800"));(* 25, 24 *)
(mk_real_int (num_of_string "37701257987237233768201074")),(mk_real_int (num_of_string "62404826098990127372287200"));(* 25, 25 *)
(mk_real_int (num_of_string "1044206513366559862588416")),(mk_real_int (num_of_string "548196697119478237799199120"));(* 24, 26 *)
(mk_real_int (num_of_string "241805263151559174231373300")),(mk_real_int (num_of_string "7138313623290211552321704"));(* 26, 24 *)
(mk_real_int (num_of_string "712800486017009844617829762")),(mk_real_int (num_of_string "55802875308599007685858944"));(* 26, 25 *)
(mk_real_int (num_of_string "12326854624523596756478800")),(mk_real_int (num_of_string "46856337327344504871660000"));(* 25, 25 *)
(mk_real_int (num_of_string "12681548201848464583101744")),(mk_real_int (num_of_string "125929230807405539544401748"));(* 25, 26 *)
(mk_real_int (num_of_string "236757855657257697175232820")),(mk_real_int (num_of_string "4546532345724820863537462"));(* 26, 24 *)
(mk_real_int (num_of_string "58696109356911132970874850")),(mk_real_int (num_of_string "46815287641478058188291164"));(* 25, 25 *)
(mk_real_int (num_of_string "70458738777466860495943092")),(mk_real_int (num_of_string "258185823191162241457762344"));(* 25, 26 *)
(mk_real_int (num_of_string "8108901148828954208157360")),(mk_real_int (num_of_string "432767421835645881808502640"));(* 24, 26 *)
(mk_real_int (num_of_string "17172960672183813025258016")),(mk_real_int (num_of_string "9377010339069090234236532"));(* 25, 24 *)
(mk_real_int (num_of_string "19698417214895854122264500")),(mk_real_int (num_of_string "27055842893427770715896130"));(* 25, 25 *)
(mk_real_int (num_of_string "33579846911335080073430373")),(mk_real_int (num_of_string "140206904157377063075766870"));(* 25, 26 *)
(mk_real_int (num_of_string "537095540591315084330744744")),(mk_real_int (num_of_string "49046907102801217572723488"));(* 26, 25 *)
(mk_real_int (num_of_string "214730568448749804732317568")),(mk_real_int (num_of_string "210796970734683889491780"));(* 26, 23 *)
(mk_real_int (num_of_string "253383394034219437924554692")),(mk_real_int (num_of_string "23051564592863538282742170"));(* 26, 25 *)
(mk_real_int (num_of_string "291086146850790076927602600")),(mk_real_int (num_of_string "1024532782023627253922508"));(* 26, 24 *)
(mk_real_int (num_of_string "35968699119771247594673700")),(mk_real_int (num_of_string "14890179717600964569590572"));(* 25, 25 *)
(mk_real_int (num_of_string "3395151517223597839009368")),(mk_real_int (num_of_string "68419066694950303505347552"));(* 24, 25 *)
(mk_real_int (num_of_string "51645033105520629515418909")),(mk_real_int (num_of_string "245325340010740860849740121"));(* 25, 26 *)
(mk_real_int (num_of_string "1124413745646916304466677")),(mk_real_int (num_of_string "35277141684253427180364352"));(* 24, 25 *)
(mk_real_int (num_of_string "288069788577609165073544985")),(mk_real_int (num_of_string "25504306623150632821535040"));(* 26, 25 *)
(mk_real_int (num_of_string "147159869796821702223459428")),(mk_real_int (num_of_string "62068751243067132294197120"));(* 26, 25 *)
(mk_real_int (num_of_string "731337872139962875698676704")),(mk_real_int (num_of_string "460500373895977321519563500"));(* 26, 26 *)
(mk_real_int (num_of_string "150030336561310312412788224")),(mk_real_int (num_of_string "538459832052505837006957440"));(* 26, 26 *)
(mk_real_int (num_of_string "8309963420508920610021879")),(mk_real_int (num_of_string "268332146214667289959772160"));(* 24, 26 *)
(mk_real_int (num_of_string "332037149910460866854314200")),(mk_real_int (num_of_string "77954172357456525010089656"));(* 26, 25 *)
(mk_real_int (num_of_string "34950316089502298470625892")),(mk_real_int (num_of_string "64498171738333647439851750"));(* 25, 25 *)
(mk_real_int (num_of_string "10539095770917829696025718")),(mk_real_int (num_of_string "210355676802423500912031396"));(* 25, 26 *)
(mk_real_int (num_of_string "394330280489378760154036311")),(mk_real_int (num_of_string "4305518321857677045541728"));(* 26, 24 *)
(mk_real_int (num_of_string "58419518358344713148989872")),(mk_real_int (num_of_string "380222798477226517903752648"));(* 25, 26 *)
(mk_real_int (num_of_string "112157811845994856227470266")),(mk_real_int (num_of_string "111181074282757465077966336"));(* 26, 26 *)
(mk_real_int (num_of_string "1481730029543749993686042")),(mk_real_int (num_of_string "10583626440892741357895700"));(* 24, 25 *)
(mk_real_int (num_of_string "31391084034545216057045200")),(mk_real_int (num_of_string "217011954920433723681241492"));(* 25, 26 *)
(mk_real_int (num_of_string "255490200110427891734705184")),(mk_real_int (num_of_string "352292269852551577203926089"));(* 26, 26 *)
(mk_real_int (num_of_string "295715612811411589343228253")),(mk_real_int (num_of_string "60362263729144459012408182"));(* 26, 25 *)
(mk_real_int (num_of_string "347695316019600314679631872")),(mk_real_int (num_of_string "9934883068880393495091935"));(* 26, 24 *)
(mk_real_int (num_of_string "122656019138052796688249720")),(mk_real_int (num_of_string "52117590409862367365735760"));(* 26, 25 *)
(mk_real_int (num_of_string "45836340858678849280376148")),(mk_real_int (num_of_string "24942844662987217389322221"));(* 25, 25 *)
(mk_real_int (num_of_string "110211132991861942719215620")),(mk_real_int (num_of_string "4686433835251682918693100"));(* 26, 24 *)
(mk_real_int (num_of_string "7576721132155850324172800")),(mk_real_int (num_of_string "514299408786744648830913150"));(* 24, 26 *)
(mk_real_int (num_of_string "36642193007117882681259925")),(mk_real_int (num_of_string "56361023618576146516128384"));(* 25, 25 *)
(mk_real_int (num_of_string "40726505783044174366510900")),(mk_real_int (num_of_string "69734713831369495866048490"));(* 25, 25 *)
(mk_real_int (num_of_string "75140823590890665506461992")),(mk_real_int (num_of_string "37017326042354118651444098"));(* 25, 25 *)
(mk_real_int (num_of_string "4802457511906381443617280")),(mk_real_int (num_of_string "86476152754917874360831878"));(* 24, 25 *)
(mk_real_int (num_of_string "397669900752986420278870080")),(mk_real_int (num_of_string "2574978476889632156990448"));(* 26, 24 *)
(mk_real_int (num_of_string "2194103287561156190726400")),(mk_real_int (num_of_string "188949065814306436899939792"));(* 24, 26 *)
(mk_real_int (num_of_string "389229653553062755568094540")),(mk_real_int (num_of_string "22286797021531824690475728"));(* 26, 25 *)
(mk_real_int (num_of_string "6610248532466324018495846")),(mk_real_int (num_of_string "18297937757199578406065280"));(* 24, 25 *)
(mk_real_int (num_of_string "170506339146915199807005360")),(mk_real_int (num_of_string "136074404952098101431000600"));(* 26, 26 *)
(mk_real_int (num_of_string "49224159005558221435508954")),(mk_real_int (num_of_string "305730529113553789674044880"));(* 25, 26 *)
(mk_real_int (num_of_string "57484706087237935092434194")),(mk_real_int (num_of_string "94326868703862147735959291"));(* 25, 25 *)
(mk_real_int (num_of_string "252994567865116642350187752")),(mk_real_int (num_of_string "46977291842183887558927608"));(* 26, 25 *)
(mk_real_int (num_of_string "513403404777299332612783116")),(mk_real_int (num_of_string "5588470143167318788574520"));(* 26, 24 *)
(mk_real_int (num_of_string "79183075223088612569844216")),(mk_real_int (num_of_string "563789418331208780684259384"));(* 25, 26 *)
(mk_real_int (num_of_string "148522939457520260837103460")),(mk_real_int (num_of_string "87085675531155640009133736"));(* 26, 25 *)
(mk_real_int (num_of_string "32923554361302501510210000")),(mk_real_int (num_of_string "191194630734396919302563792"));(* 25, 26 *)
(mk_real_int (num_of_string "75147196995590745308679872")),(mk_real_int (num_of_string "121955909595204787844508480"));(* 25, 26 *)
(mk_real_int (num_of_string "198122316974864748640001355")),(mk_real_int (num_of_string "600366154826616561404643240"));(* 26, 26 *)
(mk_real_int (num_of_string "43060198254172946733214888")),(mk_real_int (num_of_string "222953692233281193721136817"));(* 25, 26 *)
(mk_real_int (num_of_string "18919460679275378178088132")),(mk_real_int (num_of_string "94646770810742731930162071"));(* 25, 25 *)
(mk_real_int (num_of_string "21809900657924136963672048")),(mk_real_int (num_of_string "610016178006845361454949820"));(* 25, 26 *)
(mk_real_int (num_of_string "433146958272100815211340550")),(mk_real_int (num_of_string "3860671782877522520779520"));(* 26, 24 *)
(mk_real_int (num_of_string "116160069688816578012200030")),(mk_real_int (num_of_string "199058038407708637747355280"));(* 26, 26 *)
(mk_real_int (num_of_string "10380839470045391956809944")),(mk_real_int (num_of_string "162584356533029501365091340"));(* 25, 26 *)
(mk_real_int (num_of_string "237721906265041046244266160")),(mk_real_int (num_of_string "76594403627978679279825750"));(* 26, 25 *)
(mk_real_int (num_of_string "155648256498492206001546406")),(mk_real_int (num_of_string "85774806706361720608706892"));(* 26, 25 *)
(mk_real_int (num_of_string "42253850464768963308554400")),(mk_real_int (num_of_string "631614634086967590682690340"));(* 25, 26 *)
(mk_real_int (num_of_string "195051269231122850993246850")),(mk_real_int (num_of_string "206925556039680778148628360"));(* 26, 26 *)
(mk_real_int (num_of_string "444897981453577826580919926")),(mk_real_int (num_of_string "36654637014112696977779920"));(* 26, 25 *)
(mk_real_int (num_of_string "62768415013884423999307776")),(mk_real_int (num_of_string "30075247130978033861959852"));(* 25, 25 *)
(mk_real_int (num_of_string "44692550502575316249803276")),(mk_real_int (num_of_string "185276979189362673496557756"));(* 25, 26 *)
(mk_real_int (num_of_string "578655588763458816680016")),(mk_real_int (num_of_string "190989645760408606651040062"));(* 23, 26 *)
(mk_real_int (num_of_string "7900278260016279019958280")),(mk_real_int (num_of_string "218162555413382699525526822"));(* 24, 26 *)
(mk_real_int (num_of_string "431902629861550302145680000")),(mk_real_int (num_of_string "6396668476820794499396360"));(* 26, 24 *)
(mk_real_int (num_of_string "11731640531119597739953470")),(mk_real_int (num_of_string "9298711424991592730227920"));(* 25, 24 *)
(mk_real_int (num_of_string "127215754227974748037467205")),(mk_real_int (num_of_string "22468444127591182314372378"));(* 26, 25 *)
(mk_real_int (num_of_string "292520544144964860703101448")),(mk_real_int (num_of_string "155273279152835983519472553"));(* 26, 26 *)
(mk_real_int (num_of_string "12053671468049721729536772")),(mk_real_int (num_of_string "83356922016152546249539672"));(* 25, 25 *)
(mk_real_int (num_of_string "269272502338718802994721796")),(mk_real_int (num_of_string "124315158164937884127368784"));(* 26, 26 *)
(mk_real_int (num_of_string "121288123499008749730729425")),(mk_real_int (num_of_string "6237696625913226883357872"));(* 26, 24 *)
(mk_real_int (num_of_string "152890256985450620570686464")),(mk_real_int (num_of_string "12599524895768493129585658"));(* 26, 25 *)
(mk_real_int (num_of_string "27960753374948852129650000")),(mk_real_int (num_of_string "85261734185283257796122400"));(* 25, 25 *)
(mk_real_int (num_of_string "6090336880186080907794240")),(mk_real_int (num_of_string "155140109962527646088228278"));(* 24, 26 *)
(mk_real_int (num_of_string "501034702227103642943340")),(mk_real_int (num_of_string "54233546279641893660689995"));(* 23, 25 *)
(mk_real_int (num_of_string "477870670389637455243811110")),(mk_real_int (num_of_string "211501282391312674906852866"));(* 26, 26 *)
(mk_real_int (num_of_string "23872766252823644945875280")),(mk_real_int (num_of_string "1371592481091729084726300"));(* 25, 24 *)
(mk_real_int (num_of_string "3617522210332166489604576")),(mk_real_int (num_of_string "60686928973162689836049684"));(* 24, 25 *)
(mk_real_int (num_of_string "125813799008471991322070316")),(mk_real_int (num_of_string "14221953028013748277327872"));(* 26, 25 *)
(mk_real_int (num_of_string "37305987350708659431945600")),(mk_real_int (num_of_string "158876247857947338885111504"));(* 25, 26 *)
(mk_real_int (num_of_string "73775028549188016926089102")),(mk_real_int (num_of_string "13294028558506907140142868"));(* 25, 25 *)
(mk_real_int (num_of_string "78527112059205094459659186")),(mk_real_int (num_of_string "117403308807273241153036860"));(* 25, 26 *)
(mk_real_int (num_of_string "115325042501303813106762790")),(mk_real_int (num_of_string "437189275630895925496800"));(* 26, 23 *)
(mk_real_int (num_of_string "44557626407419271516614683")),(mk_real_int (num_of_string "24523824602155246195372216"));(* 25, 25 *)
(mk_real_int (num_of_string "284303677716466832767316688")),(mk_real_int (num_of_string "11441813301122703234909556"));(* 26, 25 *)
(mk_real_int (num_of_string "48126056857922662342745484")),(mk_real_int (num_of_string "47968659139828088108113722"));(* 25, 25 *)
(mk_real_int (num_of_string "89986287554911571021530176")),(mk_real_int (num_of_string "18981713168114654609957440"));(* 25, 25 *)
(mk_real_int (num_of_string "12238822571029758759581568")),(mk_real_int (num_of_string "28646497865886531456128400"));(* 25, 25 *)
(mk_real_int (num_of_string "12255092860366083731309012")),(mk_real_int (num_of_string "39126119274624433207915935"));(* 25, 25 *)
(mk_real_int (num_of_string "78703170822464274267359464")),(mk_real_int (num_of_string "374439658583495220850333350"));(* 25, 26 *)
(mk_real_int (num_of_string "209718111929700748354250699")),(mk_real_int (num_of_string "74890606920747045715014965"));(* 26, 25 *)
(mk_real_int (num_of_string "973212366944342449265556")),(mk_real_int (num_of_string "4265971827130042992073152"));(* 23, 24 *)
(mk_real_int (num_of_string "621716103397291979766170")),(mk_real_int (num_of_string "177804009058908861763777704"));(* 23, 26 *)
(mk_real_int (num_of_string "83541660086248562780757819")),(mk_real_int (num_of_string "369382262123136567545134368"));(* 25, 26 *)
(mk_real_int (num_of_string "290309861211395105221733180")),(mk_real_int (num_of_string "138565371719005595319834396"));(* 26, 26 *)
(mk_real_int (num_of_string "13625536847921226235242720")),(mk_real_int (num_of_string "257899415892981967139498328"));(* 25, 26 *)
(mk_real_int (num_of_string "888460745261690722223085")),(mk_real_int (num_of_string "389753144661993032184865200"));(* 23, 26 *)
(mk_real_int (num_of_string "76931847611206051675680320")),(mk_real_int (num_of_string "5582126312059516314851888"));(* 25, 24 *)
(mk_real_int (num_of_string "176512498732970388628080480")),(mk_real_int (num_of_string "382576284179291796602438232"));(* 26, 26 *)
(mk_real_int (num_of_string "108039730766854934921718850")),(mk_real_int (num_of_string "34882028785593450981187920"));(* 26, 25 *)
(mk_real_int (num_of_string "41905896843294270205705500")),(mk_real_int (num_of_string "22813848547608640369313064"));(* 25, 25 *)
(mk_real_int (num_of_string "1237069085010263454693000")),(mk_real_int (num_of_string "731924455848031480630914"));(* 24, 23 *)
(mk_real_int (num_of_string "107764797346267429218661555")),(mk_real_int (num_of_string "6822396023351999859132000"));(* 26, 24 *)
(mk_real_int (num_of_string "132489497019626539882674606")),(mk_real_int (num_of_string "43946652207354345927401154"));(* 26, 25 *)
(mk_real_int (num_of_string "77377188918391936417586106")),(mk_real_int (num_of_string "39883903547026942412756109"));(* 25, 25 *)
(mk_real_int (num_of_string "585090339142390239068641200")),(mk_real_int (num_of_string "177365149541759003780069400"));(* 26, 26 *)
(mk_real_int (num_of_string "5919681659901647759929500")),(mk_real_int (num_of_string "15401642284413831304846992"));(* 24, 25 *)
(mk_real_int (num_of_string "320918218594434710837544278")),(mk_real_int (num_of_string "318873617381461035721253580"));(* 26, 26 *)
(mk_real_int (num_of_string "11984672790803680080016464")),(mk_real_int (num_of_string "15037545677536283989436425"));(* 25, 25 *)
(mk_real_int (num_of_string "212584865166215772454082592")),(mk_real_int (num_of_string "763802072583511992156246907"));(* 26, 26 *)
(mk_real_int (num_of_string "141503047299863776042281136")),(mk_real_int (num_of_string "10127292467669633438372025"));(* 26, 25 *)
(mk_real_int (num_of_string "314039627257264385635968750")),(mk_real_int (num_of_string "66491092343301177028578465"));(* 26, 25 *)
(mk_real_int (num_of_string "62658266091551147482264800")),(mk_real_int (num_of_string "214407398037061183382972544"));(* 25, 26 *)
(mk_real_int (num_of_string "1182312152201293273512912")),(mk_real_int (num_of_string "23694195523145136885343392"));(* 24, 25 *)
(mk_real_int (num_of_string "20800526741589669865745245")),(mk_real_int (num_of_string "34780354999224433570285206"));(* 25, 25 *)
(mk_real_int (num_of_string "21102005965096044408483567")),(mk_real_int (num_of_string "164652363615239470399986466"));(* 25, 26 *)
(mk_real_int (num_of_string "3800990166069478301196816")),(mk_real_int (num_of_string "242692846807198373972177734"));(* 24, 26 *)
(mk_real_int (num_of_string "29446186425087260880673360")),(mk_real_int (num_of_string "255498367072574459394115980"));(* 25, 26 *)
(mk_real_int (num_of_string "103001590650579842725775208")),(mk_real_int (num_of_string "3990924599328120336651684"));(* 26, 24 *)
(mk_real_int (num_of_string "6708131940087465507445950")),(mk_real_int (num_of_string "49125210082525720157663012"));(* 24, 25 *)
(mk_real_int (num_of_string "74980155936334998671767512")),(mk_real_int (num_of_string "142514836483615351634631648"));(* 25, 26 *)
(mk_real_int (num_of_string "926639854402640757011928")),(mk_real_int (num_of_string "69541369523498579174048070"));(* 23, 25 *)
(mk_real_int (num_of_string "82351706010892860076814790")),(mk_real_int (num_of_string "105502562214386976500931520"));(* 25, 26 *)
(mk_real_int (num_of_string "42269131793083894614083088")),(mk_real_int (num_of_string "5305414718197019848535400"));(* 25, 24 *)
(mk_real_int (num_of_string "16145086665356766842213650")),(mk_real_int (num_of_string "277901705440033756866668312"));(* 25, 26 *)
(mk_real_int (num_of_string "46996608529295963609388075")),(mk_real_int (num_of_string "23523301451171565747003040"));(* 25, 25 *)
(mk_real_int (num_of_string "117288016118692425716387904")),(mk_real_int (num_of_string "19548347575813718324075820"));(* 26, 25 *)
(mk_real_int (num_of_string "134914259709688444434218220")),(mk_real_int (num_of_string "161829538122298663667449380"));(* 26, 26 *)
(mk_real_int (num_of_string "325792745339171630767187850")),(mk_real_int (num_of_string "13727184353294772844047256"));(* 26, 25 *)
(mk_real_int (num_of_string "59347858194135012077947098")),(mk_real_int (num_of_string "284139964542229978668096"));(* 25, 23 *)
(mk_real_int (num_of_string "5661081071480485679491840")),(mk_real_int (num_of_string "50568128613214758613993275"));(* 24, 25 *)
(mk_real_int (num_of_string "24105907847739911547433980")),(mk_real_int (num_of_string "124169352085343311680956880"));(* 25, 26 *)
(mk_real_int (num_of_string "389527876651343498175597")),(mk_real_int (num_of_string "276819364685320409651715324"));(* 23, 26 *)
(mk_real_int (num_of_string "143877798588087872203126125")),(mk_real_int (num_of_string "13713555858745767004989292"));(* 26, 25 *)
(mk_real_int (num_of_string "20866024341070779843659550")),(mk_real_int (num_of_string "106207003716456391955641842"));(* 25, 26 *)
(mk_real_int (num_of_string "11686079766019203668347840")),(mk_real_int (num_of_string "17828688281153725672519428"));(* 25, 25 *)
(mk_real_int (num_of_string "100167944436384044043590237")),(mk_real_int (num_of_string "10983223719949271177418957"));(* 26, 25 *)
(mk_real_int (num_of_string "51450552219630827128974480")),(mk_real_int (num_of_string "233473277136582475673664081"));(* 25, 26 *)
(mk_real_int (num_of_string "111622927871440256800894776")),(mk_real_int (num_of_string "53691496139980203894232800"));(* 26, 25 *)
(mk_real_int (num_of_string "38505218740837331314132992")),(mk_real_int (num_of_string "216108382782518591705635086"));(* 25, 26 *)
(mk_real_int (num_of_string "21287407981881218221189548")),(mk_real_int (num_of_string "6981640172860580083616928"));(* 25, 24 *)
(mk_real_int (num_of_string "148137688603796002279081776")),(mk_real_int (num_of_string "27805133073817477166077980"));(* 26, 25 *)
(mk_real_int (num_of_string "141385445104534314726706790")),(mk_real_int (num_of_string "31602092819039866737967028"));(* 26, 25 *)
(mk_real_int (num_of_string "18246136963668841354085820")),(mk_real_int (num_of_string "324881246697903737256832568"));(* 25, 26 *)
(mk_real_int (num_of_string "203448657630316118319060216")),(mk_real_int (num_of_string "235876902173578904587764156"));(* 26, 26 *)
(mk_real_int (num_of_string "434966758436857676820922560")),(mk_real_int (num_of_string "62839159229331738066965544"));(* 26, 25 *)
(mk_real_int (num_of_string "54653294824336409761239120")),(mk_real_int (num_of_string "2374491963600258300804852"));(* 25, 24 *)
(mk_real_int (num_of_string "13735436423873469310151272")),(mk_real_int (num_of_string "223388655671318972326341300"));(* 25, 26 *)
(mk_real_int (num_of_string "685440047874114802252993680")),(mk_real_int (num_of_string "92456207551611531721946128"));(* 26, 25 *)
(mk_real_int (num_of_string "466100634781773880357875000")),(mk_real_int (num_of_string "71269047989071759429364164"));(* 26, 25 *)
(mk_real_int (num_of_string "180005000253306119609256000")),(mk_real_int (num_of_string "246095061832061335384831278"));(* 26, 26 *)
(mk_real_int (num_of_string "1805491102059375407925048")),(mk_real_int (num_of_string "20047113588112443671808354"));(* 24, 25 *)
(mk_real_int (num_of_string "12423957516906840908560536")),(mk_real_int (num_of_string "1643947001624459374737328"));(* 25, 24 *)
(mk_real_int (num_of_string "12297170150303451576309377")),(mk_real_int (num_of_string "339816729888375652310213088"));(* 25, 26 *)
(mk_real_int (num_of_string "38811814433651561501453436")),(mk_real_int (num_of_string "220466311533420262623424320"));(* 25, 26 *)
(mk_real_int (num_of_string "938486788930201380514920")),(mk_real_int (num_of_string "214869758239043659378799304"));(* 23, 26 *)
(mk_real_int (num_of_string "1541175343349128838736480")),(mk_real_int (num_of_string "385481890202462242751956404"));(* 24, 26 *)
(mk_real_int (num_of_string "194375386555655635214113262")),(mk_real_int (num_of_string "120935275650995725078585920"));(* 26, 26 *)
(mk_real_int (num_of_string "227419307429334568906399650")),(mk_real_int (num_of_string "134138450795216373440544600"));(* 26, 26 *)
(mk_real_int (num_of_string "34166656548633088199297266")),(mk_real_int (num_of_string "6815179701989167241187"));(* 25, 21 *)
(mk_real_int (num_of_string "1321715032472183388447216")),(mk_real_int (num_of_string "171610409643865924020742800"));(* 24, 26 *)
(mk_real_int (num_of_string "453319891793170097383378449")),(mk_real_int (num_of_string "58651860777027072026928"));(* 26, 22 *)
(mk_real_int (num_of_string "210663848519499481247178000")),(mk_real_int (num_of_string "120409625690224084897198493"));(* 26, 26 *)
(mk_real_int (num_of_string "5099889347962974125246400")),(mk_real_int (num_of_string "90782144763050004527556480"));(* 24, 25 *)
(mk_real_int (num_of_string "51883782085773756731031160")),(mk_real_int (num_of_string "72601191378568507251629760"));(* 25, 25 *)
(mk_real_int (num_of_string "320880601048122206390860976")),(mk_real_int (num_of_string "652924367842204658900782170"));(* 26, 26 *)
(mk_real_int (num_of_string "5935834910143644937732028")),(mk_real_int (num_of_string "51259970330262429497937450"));(* 24, 25 *)
(mk_real_int (num_of_string "212275073739085688700861786")),(mk_real_int (num_of_string "414766115668143677438186400"));(* 26, 26 *)
(mk_real_int (num_of_string "179981544056667510830689072")),(mk_real_int (num_of_string "108889360594299401835703680"));(* 26, 26 *)
(mk_real_int (num_of_string "71849560163540743050300288")),(mk_real_int (num_of_string "112926556863862768311977646"));(* 25, 26 *)
(mk_real_int (num_of_string "18723623906084971838816160")),(mk_real_int (num_of_string "3090262595227727029540248"));(* 25, 24 *)
(mk_real_int (num_of_string "2428371137573353690478640")),(mk_real_int (num_of_string "297825051080529404557944"));(* 24, 23 *)
(mk_real_int (num_of_string "180552200128586362674134400")),(mk_real_int (num_of_string "45040450735529572047158679"));(* 26, 25 *)
(mk_real_int (num_of_string "23506560630338462458852048")),(mk_real_int (num_of_string "60623196601962767358818848"));(* 25, 25 *)
(mk_real_int (num_of_string "112154798819841553432264608")),(mk_real_int (num_of_string "194011373909565036111612000"));(* 26, 26 *)
(mk_real_int (num_of_string "3729556535788409417708388")),(mk_real_int (num_of_string "8421439631098663013773500"));(* 24, 24 *)
(mk_real_int (num_of_string "80601527714781592214182440")),(mk_real_int (num_of_string "367436750665368892154572563"));(* 25, 26 *)
(mk_real_int (num_of_string "63711417649873130379757125")),(mk_real_int (num_of_string "47757836447074352186246230"));(* 25, 25 *)
(mk_real_int (num_of_string "81817422580447388931510900")),(mk_real_int (num_of_string "324734192536899491528679988"));(* 25, 26 *)
(mk_real_int (num_of_string "45073604778773565752324920")),(mk_real_int (num_of_string "8714683875328460169704718"));(* 25, 24 *)
(mk_real_int (num_of_string "3660067204419660506207925")),(mk_real_int (num_of_string "72321685029542931012002160"));(* 24, 25 *)
(mk_real_int (num_of_string "456336113628278051177850048")),(mk_real_int (num_of_string "65641068685341194382255672"));(* 26, 25 *)
(mk_real_int (num_of_string "581311906601481199148075760")),(mk_real_int (num_of_string "100551241413575796657553536"));(* 26, 26 *)
(mk_real_int (num_of_string "44254345905048853180474164")),(mk_real_int (num_of_string "585960482851696116748660230"));(* 25, 26 *)
(mk_real_int (num_of_string "6247768455005254804117608")),(mk_real_int (num_of_string "13341226342684665279424395"));(* 24, 25 *)
(mk_real_int (num_of_string "399810717659463279073920")),(mk_real_int (num_of_string "88765700571757363629944088"));(* 23, 25 *)
(mk_real_int (num_of_string "57513545553267063281655248")),(mk_real_int (num_of_string "275396193758837131531813638"));(* 25, 26 *)
(mk_real_int (num_of_string "60543559109698565030786138")),(mk_real_int (num_of_string "94427796132810224514413088"));(* 25, 25 *)
(mk_real_int (num_of_string "458066842028017227425828064")),(mk_real_int (num_of_string "4019133903774696286167720"));(* 26, 24 *)
(mk_real_int (num_of_string "162950057099087054982423516")),(mk_real_int (num_of_string "329172264402670689953773200"));(* 26, 26 *)
(mk_real_int (num_of_string "196219960140586391035188840")),(mk_real_int (num_of_string "62450369439298975138498620"));(* 26, 25 *)
(mk_real_int (num_of_string "20290915857301971523584955")),(mk_real_int (num_of_string "126300709225852021472531920"));(* 25, 26 *)
(mk_real_int (num_of_string "433427112476069884507406028")),(mk_real_int (num_of_string "58826548095419747283058800"));(* 26, 25 *)
(mk_real_int (num_of_string "79783632137147809770958044")),(mk_real_int (num_of_string "114395290028809460518894200"));(* 25, 26 *)
(mk_real_int (num_of_string "287297435924177812227720")),(mk_real_int (num_of_string "21572180974544997993357600"));(* 23, 25 *)
(mk_real_int (num_of_string "89345577158757673817252814")),(mk_real_int (num_of_string "14928948745847840318847588"));(* 25, 25 *)
(mk_real_int (num_of_string "174172879197552385489920")),(mk_real_int (num_of_string "159330773217139569015169472"));(* 23, 26 *)
(mk_real_int (num_of_string "392339804504372325004768000")),(mk_real_int (num_of_string "491946681162167933117275504"));(* 26, 26 *)
(mk_real_int (num_of_string "44839904203549016710910801")),(mk_real_int (num_of_string "120197221142061248862186432"));(* 25, 26 *)
(mk_real_int (num_of_string "1410976130091158646151128")),(mk_real_int (num_of_string "51931882119722881888368400"));(* 24, 25 *)
(mk_real_int (num_of_string "23275444388294351900908800")),(mk_real_int (num_of_string "254224462495198112998755444"));(* 25, 26 *)
(mk_real_int (num_of_string "37236945163620975500466522")),(mk_real_int (num_of_string "212626099145259591851999056"));(* 25, 26 *)
(mk_real_int (num_of_string "97229497367560694898117")),(mk_real_int (num_of_string "339960869090268669455585608"));(* 22, 26 *)
(mk_real_int (num_of_string "49392368399685415565609120")),(mk_real_int (num_of_string "55343782751267735702215224"));(* 25, 25 *)
(mk_real_int (num_of_string "16024983331013252271468800")),(mk_real_int (num_of_string "262483522332586076754622152"));(* 25, 26 *)
(mk_real_int (num_of_string "92075742081176133811317930")),(mk_real_int (num_of_string "5021378422481407198559984"));(* 25, 24 *)
(mk_real_int (num_of_string "13822115459059717262286912")),(mk_real_int (num_of_string "40748748750272896438786800"));(* 25, 25 *)
(mk_real_int (num_of_string "418283080904328469945751192")),(mk_real_int (num_of_string "2015735017576779880312084"));(* 26, 24 *)
(mk_real_int (num_of_string "99812057905158457089839408")),(mk_real_int (num_of_string "60755783047763071696342740"));(* 25, 25 *)
(mk_real_int (num_of_string "88923495967806850470318000")),(mk_real_int (num_of_string "152170146461991262237564800"));(* 25, 26 *)
(mk_real_int (num_of_string "3712375617386268555743816")),(mk_real_int (num_of_string "175464408301990139969923096"));(* 24, 26 *)
(mk_real_int (num_of_string "54077809340673237458929986")),(mk_real_int (num_of_string "404627886478599524647341464"));(* 25, 26 *)
(mk_real_int (num_of_string "259826168365109665092282")),(mk_real_int (num_of_string "15865085538163581166106976"));(* 23, 25 *)
(mk_real_int (num_of_string "225527392440741415623029076")),(mk_real_int (num_of_string "104270504843540394621850203"));(* 26, 26 *)
(mk_real_int (num_of_string "250124391889262030189199150")),(mk_real_int (num_of_string "48769244093182534981257600"));(* 26, 25 *)
(mk_real_int (num_of_string "20435180607480395109912700")),(mk_real_int (num_of_string "374079304100051945323254"));(* 25, 23 *)
(mk_real_int (num_of_string "162630705034695670976285130")),(mk_real_int (num_of_string "493494100043871922492303722"));(* 26, 26 *)
(mk_real_int (num_of_string "56315352116211051442588596")),(mk_real_int (num_of_string "65446971984974764184421888"));(* 25, 25 *)
(mk_real_int (num_of_string "411009808851297344678962500")),(mk_real_int (num_of_string "379621683432864746936870742"));(* 26, 26 *)
(mk_real_int (num_of_string "140538101679159770894034000")),(mk_real_int (num_of_string "81739307761916093185769420"));(* 26, 25 *)
(mk_real_int (num_of_string "161007951089381840163231600")),(mk_real_int (num_of_string "55624036857928082102088445"));(* 26, 25 *)
(mk_real_int (num_of_string "27138834800112406479987264")),(mk_real_int (num_of_string "129488733457453574515097679"));(* 25, 26 *)
(mk_real_int (num_of_string "3922302267813546856155400")),(mk_real_int (num_of_string "15139121024050207838386656"));(* 24, 25 *)
(mk_real_int (num_of_string "110235428057686904403229630")),(mk_real_int (num_of_string "180526755450816241512801918"));(* 26, 26 *)
(mk_real_int (num_of_string "562757895512841075999505050")),(mk_real_int (num_of_string "80705258129891822285930918"));(* 26, 25 *)
(mk_real_int (num_of_string "42758368255672577143298190")),(mk_real_int (num_of_string "45994665347830962798568896"));(* 25, 25 *)
(mk_real_int (num_of_string "104215341186038258038983648")),(mk_real_int (num_of_string "28156706700335340677171424"));(* 26, 25 *)
(mk_real_int (num_of_string "194649275777298014515780350")),(mk_real_int (num_of_string "53036804648675501566432416"));(* 26, 25 *)
(mk_real_int (num_of_string "58057746139733726268625574")),(mk_real_int (num_of_string "76656125485101384447348780"));(* 25, 25 *)
(mk_real_int (num_of_string "237983350324677612773686792")),(mk_real_int (num_of_string "93272455505308924506452"));(* 26, 22 *)
(mk_real_int (num_of_string "6082058366563777550375976")),(mk_real_int (num_of_string "246784606526569428200351250"));(* 24, 26 *)
(mk_real_int (num_of_string "6254623975487582093997312")),(mk_real_int (num_of_string "533256365322670818697960"));(* 24, 23 *)
(mk_real_int (num_of_string "15310887600253659072603428")),(mk_real_int (num_of_string "15876906859216627925781930"));(* 25, 25 *)
(mk_real_int (num_of_string "39146852972705255866808055")),(mk_real_int (num_of_string "14564461649782030459891200"));(* 25, 25 *)
(mk_real_int (num_of_string "81007535400855092786085186")),(mk_real_int (num_of_string "91395317853124287391093832"));(* 25, 25 *)
(mk_real_int (num_of_string "101374659683891432689014186")),(mk_real_int (num_of_string "23730928234740902470159200"));(* 26, 25 *)
(mk_real_int (num_of_string "161977342956762049401100672")),(mk_real_int (num_of_string "129983109453922583417589729"));(* 26, 26 *)
(mk_real_int (num_of_string "35297170667004073626754534")),(mk_real_int (num_of_string "343064411829741347852955422"));(* 25, 26 *)
(mk_real_int (num_of_string "232855023467246710919603520")),(mk_real_int (num_of_string "426242679351307175146740600"));(* 26, 26 *)
(mk_real_int (num_of_string "52305934901807530374383736")),(mk_real_int (num_of_string "222464315885855985697233867"));(* 25, 26 *)
(mk_real_int (num_of_string "185197949390888877018482432")),(mk_real_int (num_of_string "9339361304502717918730080"));(* 26, 24 *)
(mk_real_int (num_of_string "90538754766552392814366090")),(mk_real_int (num_of_string "26266115513585603113166280"));(* 25, 25 *)
(mk_real_int (num_of_string "125188436931903197595282220")),(mk_real_int (num_of_string "6405266304700037789577024"));(* 26, 24 *)
(mk_real_int (num_of_string "163321232178000139755926151")),(mk_real_int (num_of_string "19374452227465774117100208"));(* 26, 25 *)
(mk_real_int (num_of_string "122993954448462886196187915")),(mk_real_int (num_of_string "146406777281401199433757191"));(* 26, 26 *)
(mk_real_int (num_of_string "205789675113909350664499110")),(mk_real_int (num_of_string "287406124623481673455504400"));(* 26, 26 *)
(mk_real_int (num_of_string "79108299595235583172055872")),(mk_real_int (num_of_string "196468944397738290526120440"));(* 25, 26 *)
(mk_real_int (num_of_string "302667905192145734428138272")),(mk_real_int (num_of_string "89021516160050518405580340"));(* 26, 25 *)
(mk_real_int (num_of_string "115313649039806138402738985")),(mk_real_int (num_of_string "136824800644850609816762760"));(* 26, 26 *)
(mk_real_int (num_of_string "83505953892076184950754544")),(mk_real_int (num_of_string "209573462955675258028867734"));(* 25, 26 *)
(mk_real_int (num_of_string "220864140503623854545329476")),(mk_real_int (num_of_string "225617321411703843189744750"));(* 26, 26 *)
(mk_real_int (num_of_string "88852852462691733253736256")),(mk_real_int (num_of_string "122701196300643633986163876"));(* 25, 26 *)
(mk_real_int (num_of_string "30630452949097413245884680")),(mk_real_int (num_of_string "99820753076223364234894512"));(* 25, 25 *)
(mk_real_int (num_of_string "1205819824574169488648160")),(mk_real_int (num_of_string "505144794834641913830391098"));(* 24, 26 *)
(mk_real_int (num_of_string "177078467482167849527175556")),(mk_real_int (num_of_string "75930785998504989108418080"));(* 26, 25 *)
(mk_real_int (num_of_string "82656148440635895999030800")),(mk_real_int (num_of_string "154971543830121949324201408"));(* 25, 26 *)
(mk_real_int (num_of_string "15522071581182159231822714")),(mk_real_int (num_of_string "129931864325830521430082646"));(* 25, 26 *)
(mk_real_int (num_of_string "35570993072445572535287600")),(mk_real_int (num_of_string "105917598816148894084505265"));(* 25, 26 *)
(mk_real_int (num_of_string "493837504100854051158366696")),(mk_real_int (num_of_string "26357170133223084242691450"));(* 26, 25 *)
(mk_real_int (num_of_string "919288126360529696873049640")),(mk_real_int (num_of_string "36808417961342232143811522"));(* 26, 25 *)
(mk_real_int (num_of_string "41097350074266897265866720")),(mk_real_int (num_of_string "152976071149820537114728320"));(* 25, 26 *)
(mk_real_int (num_of_string "152181923865252399403735296")),(mk_real_int (num_of_string "81855099896495137931696250"));(* 26, 25 *)
(mk_real_int (num_of_string "51437748496104563332193310")),(mk_real_int (num_of_string "185468504568960127862981024"));(* 25, 26 *)
(mk_real_int (num_of_string "5843841633358273702621368")),(mk_real_int (num_of_string "626922273503837653661882304"));(* 24, 26 *)
(mk_real_int (num_of_string "476114009112223549531961630")),(mk_real_int (num_of_string "87322992260996170998840300"));(* 26, 25 *)
(mk_real_int (num_of_string "131892123848377349218325760")),(mk_real_int (num_of_string "370939760741317827756616"));(* 26, 23 *)
(mk_real_int (num_of_string "151134283355799158119369170")),(mk_real_int (num_of_string "10410418530516484133068770"));(* 26, 25 *)
(mk_real_int (num_of_string "111420946257554473743630240")),(mk_real_int (num_of_string "37469997365103083529465504"));(* 26, 25 *)
(mk_real_int (num_of_string "15073461590194664809329784")),(mk_real_int (num_of_string "8899457992989890754472800"));(* 25, 24 *)
(mk_real_int (num_of_string "37493323018895142840451934")),(mk_real_int (num_of_string "129885903658182101033708280"));(* 25, 26 *)
(mk_real_int (num_of_string "391318657753585621208032")),(mk_real_int (num_of_string "399408583388762870751826368"));(* 23, 26 *)
(mk_real_int (num_of_string "191509684135162933370856480")),(mk_real_int (num_of_string "24844282677419432555312976"));(* 26, 25 *)
(mk_real_int (num_of_string "9851979938916257771280432")),(mk_real_int (num_of_string "239835969875946884990764550"));(* 24, 26 *)
(mk_real_int (num_of_string "76703581724178666493491200")),(mk_real_int (num_of_string "46686713370348825010134520"));(* 25, 25 *)
(mk_real_int (num_of_string "149371169661300093669686978")),(mk_real_int (num_of_string "104315238740603731035368376"));(* 26, 26 *)
(mk_real_int (num_of_string "1848504819687652161779550")),(mk_real_int (num_of_string "153598334255104926365048778"));(* 24, 26 *)
(mk_real_int (num_of_string "215544271788775201795421175")),(mk_real_int (num_of_string "11162065447903187990628225"));(* 26, 25 *)
(mk_real_int (num_of_string "176884056276390261184109920")),(mk_real_int (num_of_string "126319640668079994916473420"));(* 26, 26 *)
(mk_real_int (num_of_string "194235377319432026424950400")),(mk_real_int (num_of_string "96601963709296847285353552"));(* 26, 25 *)
(mk_real_int (num_of_string "258379519070518606593734286")),(mk_real_int (num_of_string "271864005181549990760982216"));(* 26, 26 *)
(mk_real_int (num_of_string "6702762673279553259980280")),(mk_real_int (num_of_string "221966878363476076898484336"));(* 24, 26 *)
(mk_real_int (num_of_string "836577470444500759502389888")),(mk_real_int (num_of_string "247644308145840324280320"));(* 26, 23 *)
(mk_real_int (num_of_string "47611142838804804449089290")),(mk_real_int (num_of_string "208427580283401968925097364"));(* 25, 26 *)
(mk_real_int (num_of_string "296388340210114339280261175")),(mk_real_int (num_of_string "34148843128840905244352016"));(* 26, 25 *)
(mk_real_int (num_of_string "64100113366254090668318160")),(mk_real_int (num_of_string "109482805304517490684541888"));(* 25, 26 *)
(mk_real_int (num_of_string "67469525207135444024970000")),(mk_real_int (num_of_string "211491939841106873835712320"));(* 25, 26 *)
(mk_real_int (num_of_string "12442827507922255594696000")),(mk_real_int (num_of_string "114808943014281239379141213"));(* 25, 26 *)
(mk_real_int (num_of_string "106947485384438604137752156")),(mk_real_int (num_of_string "66440270197420812686982582"));(* 26, 25 *)
(mk_real_int (num_of_string "81701223659312628942197820")),(mk_real_int (num_of_string "224553386410805517921197901"));(* 25, 26 *)
(mk_real_int (num_of_string "239103092192003256239937990")),(mk_real_int (num_of_string "30269138748821841095671808"));(* 26, 25 *)
(mk_real_int (num_of_string "34616667592444946434803000")),(mk_real_int (num_of_string "296207615011023441203548356"));(* 25, 26 *)
(mk_real_int (num_of_string "2423941874508669048534276")),(mk_real_int (num_of_string "24632080771267810827787360"));(* 24, 25 *)
(mk_real_int (num_of_string "32222194536256444559446974")),(mk_real_int (num_of_string "70682855137792579621506996"));(* 25, 25 *)
(mk_real_int (num_of_string "35736235504977816545038902")),(mk_real_int (num_of_string "144183992856381938461445865"));(* 25, 26 *)
(mk_real_int (num_of_string "337225097976511751668676560")),(mk_real_int (num_of_string "14168369171765512052441268"));(* 26, 25 *)
(mk_real_int (num_of_string "28457648935994868261731424")),(mk_real_int (num_of_string "194430085420515136520871400"));(* 25, 26 *)
(mk_real_int (num_of_string "3510217663290780111970452")),(mk_real_int (num_of_string "207597513442531604715385920"));(* 24, 26 *)
(mk_real_int (num_of_string "24056225908930196757289560")),(mk_real_int (num_of_string "56448882848301562868856064"));(* 25, 25 *)
(mk_real_int (num_of_string "233979627977952373968017112")),(mk_real_int (num_of_string "72062052074237987253919152"));(* 26, 25 *)
(mk_real_int (num_of_string "223604101565786779181818560")),(mk_real_int (num_of_string "27174168836620901745525296"));(* 26, 25 *)
(mk_real_int (num_of_string "17528767858895634858349580")),(mk_real_int (num_of_string "168553714182939137274183832"));(* 25, 26 *)
(mk_real_int (num_of_string "5557452594460879804501500")),(mk_real_int (num_of_string "129881731890993342759814104"));(* 24, 26 *)
(mk_real_int (num_of_string "29718579635560371213007776")),(mk_real_int (num_of_string "34619097468125662931666216"));(* 25, 25 *)
(mk_real_int (num_of_string "92501436685299682083816800")),(mk_real_int (num_of_string "26673990192443188865413632"));(* 25, 25 *)
(mk_real_int (num_of_string "29273588247113948416936320")),(mk_real_int (num_of_string "16013222575628895408791070"));(* 25, 25 *)
(mk_real_int (num_of_string "315040416116980756015176200")),(mk_real_int (num_of_string "72940347307005234229335600"));(* 26, 25 *)
(mk_real_int (num_of_string "11954403209145829317385864")),(mk_real_int (num_of_string "301974449031713965064279232"));(* 25, 26 *)
(mk_real_int (num_of_string "214817512100409264655520190")),(mk_real_int (num_of_string "158329378990034833719864096"));(* 26, 26 *)
(mk_real_int (num_of_string "1225157583243680344019520")),(mk_real_int (num_of_string "178669978118523169288819980"));(* 24, 26 *)
(mk_real_int (num_of_string "78492915678000431196543000")),(mk_real_int (num_of_string "793202645313817690917460"));(* 25, 23 *)
(mk_real_int (num_of_string "171189407989735922812223695")),(mk_real_int (num_of_string "339671414999752448280445512"));(* 26, 26 *)
(mk_real_int (num_of_string "15459685919194836062864435")),(mk_real_int (num_of_string "4362901825183060499242358"));(* 25, 24 *)
(mk_real_int (num_of_string "249109406572574126693288979")),(mk_real_int (num_of_string "3001290313934159001567459"));(* 26, 24 *)
(mk_real_int (num_of_string "27681436456084491374864100")),(mk_real_int (num_of_string "15725410332619531640329155"));(* 25, 25 *)
(mk_real_int (num_of_string "423941217418327598030201490")),(mk_real_int (num_of_string "115544786296081286853636480"));(* 26, 26 *)
(mk_real_int (num_of_string "225085000972283878373955520")),(mk_real_int (num_of_string "381085660566471666598987500"));(* 26, 26 *)
(mk_real_int (num_of_string "156462001420151346990414840")),(mk_real_int (num_of_string "189221085098721902383765800"));(* 26, 26 *)
(mk_real_int (num_of_string "70672431861320763907696950")),(mk_real_int (num_of_string "370062604667052890680568184"));(* 25, 26 *)
(mk_real_int (num_of_string "104717361470572415859939000")),(mk_real_int (num_of_string "76941239216532554666140650"));(* 26, 25 *)
(mk_real_int (num_of_string "1867504685079455023214206")),(mk_real_int (num_of_string "124746372828024556911116220"));(* 24, 26 *)
(mk_real_int (num_of_string "489574575110683448109360")),(mk_real_int (num_of_string "21049034132684449748198762"));(* 23, 25 *)
(mk_real_int (num_of_string "197343428569747890629181840")),(mk_real_int (num_of_string "27069674876858914322163456"));(* 26, 25 *)
(mk_real_int (num_of_string "201336853027726432183379520")),(mk_real_int (num_of_string "9066714030593720214426486"));(* 26, 24 *)
(mk_real_int (num_of_string "24002555599269227455979400")),(mk_real_int (num_of_string "87087241416958248314261268"));(* 25, 25 *)
(mk_real_int (num_of_string "59387013338043309759435336")),(mk_real_int (num_of_string "41593128302500330158835200"));(* 25, 25 *)
(mk_real_int (num_of_string "324343298568684881593760279")),(mk_real_int (num_of_string "60217938003608513048504106"));(* 26, 25 *)
(mk_real_int (num_of_string "101032577656534567469611008")),(mk_real_int (num_of_string "55329529869567275553483660"));(* 26, 25 *)
(mk_real_int (num_of_string "10952778080002163151368034")),(mk_real_int (num_of_string "41557989373215707862653820"));(* 25, 25 *)
(mk_real_int (num_of_string "40857843254004830718989604")),(mk_real_int (num_of_string "263961421753559446217915244"));(* 25, 26 *)
(mk_real_int (num_of_string "88101501887986104160841055")),(mk_real_int (num_of_string "58092991468720491774032100"));(* 25, 25 *)
(mk_real_int (num_of_string "325052362518574024852277760")),(mk_real_int (num_of_string "28078134237065376892114554"));(* 26, 25 *)
(mk_real_int (num_of_string "387315940431876946743834")),(mk_real_int (num_of_string "35167828013175547269005088"));(* 23, 25 *)
(mk_real_int (num_of_string "357510364981792796689130248")),(mk_real_int (num_of_string "9826128219242835832000575"));(* 26, 24 *)
(mk_real_int (num_of_string "36851702874561639826901958")),(mk_real_int (num_of_string "59252849985174880329949646"));(* 25, 25 *)
(mk_real_int (num_of_string "430105201101521896085477925")),(mk_real_int (num_of_string "344125827283953466950836544"));(* 26, 26 *)
(mk_real_int (num_of_string "45835099031954985077768346")),(mk_real_int (num_of_string "513680913630338840235622080"));(* 25, 26 *)
(mk_real_int (num_of_string "625931768461956277572343080")),(mk_real_int (num_of_string "234844862820799929218211852"));(* 26, 26 *)
(mk_real_int (num_of_string "21955442028250641696228704")),(mk_real_int (num_of_string "13666771406323490563032000"));(* 25, 25 *)
(mk_real_int (num_of_string "21149480630457706299086580")),(mk_real_int (num_of_string "198646969462570115316050520"));(* 25, 26 *)
(mk_real_int (num_of_string "233745587089712599953090312")),(mk_real_int (num_of_string "67824330357750649635898816"));(* 26, 25 *)
(mk_real_int (num_of_string "40083135819359798668474335")),(mk_real_int (num_of_string "245439689266869552302587740"));(* 25, 26 *)
(mk_real_int (num_of_string "183775453512228896441627")),(mk_real_int (num_of_string "220562746138963393485883500"));(* 23, 26 *)
(mk_real_int (num_of_string "372773006063123272745365980")),(mk_real_int (num_of_string "140784232457612271119514160"));(* 26, 26 *)
(mk_real_int (num_of_string "104526856572439195338827760")),(mk_real_int (num_of_string "364462793239150003721070496"));(* 26, 26 *)
(mk_real_int (num_of_string "2011960288023567983000944")),(mk_real_int (num_of_string "36637992090961055086843320"));(* 24, 25 *)
(mk_real_int (num_of_string "39241722175943450568028624")),(mk_real_int (num_of_string "193939260844567392818849604"));(* 25, 26 *)
(mk_real_int (num_of_string "529568345942011100308038")),(mk_real_int (num_of_string "93827845560247795676148"));(* 23, 22 *)
(mk_real_int (num_of_string "506175990082900559831841300")),(mk_real_int (num_of_string "31722872773422984009617700"));(* 26, 25 *)
(mk_real_int (num_of_string "3049716832778815791467322")),(mk_real_int (num_of_string "6461017593636757357676680"));(* 24, 24 *)
(mk_real_int (num_of_string "31574976438298846544762784")),(mk_real_int (num_of_string "86055977734520335688065200"));(* 25, 25 *)
(mk_real_int (num_of_string "56472059911647542989096170")),(mk_real_int (num_of_string "98026795544543331108296220"));(* 25, 25 *)
(mk_real_int (num_of_string "154894452239136501733917672")),(mk_real_int (num_of_string "171772573378834831967057516"));(* 26, 26 *)
(mk_real_int (num_of_string "651989861955465525861341")),(mk_real_int (num_of_string "276817830797404350712403040"));(* 23, 26 *)
(mk_real_int (num_of_string "70193860662897867420065178")),(mk_real_int (num_of_string "1015995820619200056772608"));(* 25, 24 *)
(mk_real_int (num_of_string "52399284296481652596355392")),(mk_real_int (num_of_string "30901533288632851463260224"));(* 25, 25 *)
(mk_real_int (num_of_string "48158272484948890791414855")),(mk_real_int (num_of_string "339499205102682626875756116"));(* 25, 26 *)
(mk_real_int (num_of_string "17392187250010657930299108")),(mk_real_int (num_of_string "697961322658792828435878"));(* 25, 23 *)
(mk_real_int (num_of_string "16555068608390807269632086")),(mk_real_int (num_of_string "128829852310473828873695180"));(* 25, 26 *)
(mk_real_int (num_of_string "49950518864426740806337392")),(mk_real_int (num_of_string "546428817889031820982456217"));(* 25, 26 *)
(mk_real_int (num_of_string "3184130815158350804429298")),(mk_real_int (num_of_string "289932399367074108704658960"));(* 24, 26 *)
(mk_real_int (num_of_string "2884586439158754749202080")),(mk_real_int (num_of_string "8077727174506373940211110"));(* 24, 24 *)
(mk_real_int (num_of_string "99987080859695139980143014")),(mk_real_int (num_of_string "1081007835405515495659550"));(* 25, 24 *)
(mk_real_int (num_of_string "310790965284331802270545920")),(mk_real_int (num_of_string "64159949797885460180457270"));(* 26, 25 *)
(mk_real_int (num_of_string "42358201704572085007353900")),(mk_real_int (num_of_string "46350985715909345074347360"));(* 25, 25 *)
(mk_real_int (num_of_string "263224308699445906107357480")),(mk_real_int (num_of_string "161460745986574256496550848"));(* 26, 26 *)
(mk_real_int (num_of_string "23556848919920223557717676")),(mk_real_int (num_of_string "24084205759686842449431078"));(* 25, 25 *)
(mk_real_int (num_of_string "342058631035689241215785500")),(mk_real_int (num_of_string "338729860635207964243944480"));(* 26, 26 *)
(mk_real_int (num_of_string "54336434373872746832363520")),(mk_real_int (num_of_string "236806815467050791653376640"));(* 25, 26 *)
(mk_real_int (num_of_string "70337103563345810247991584")),(mk_real_int (num_of_string "72748760878790310529406364"));(* 25, 25 *)
(mk_real_int (num_of_string "14689592282635906574549688")),(mk_real_int (num_of_string "2514247363771813385362449"));(* 25, 24 *)
(mk_real_int (num_of_string "180769928510978610143365728")),(mk_real_int (num_of_string "89916018811245517937616787"));(* 26, 25 *)
(mk_real_int (num_of_string "31461821622840042314232240")),(mk_real_int (num_of_string "188205699575212123793126104"));(* 25, 26 *)
(mk_real_int (num_of_string "261914254095670799572649781")),(mk_real_int (num_of_string "99056818252880461389098760"));(* 26, 25 *)
(mk_real_int (num_of_string "95911184412986891886637560")),(mk_real_int (num_of_string "134492114565066113802922680"));(* 25, 26 *)
(mk_real_int (num_of_string "145640879225955854822599128")),(mk_real_int (num_of_string "93886447145216447118307680"));(* 26, 25 *)
(mk_real_int (num_of_string "18265120473568607486780904")),(mk_real_int (num_of_string "20741643808530812043914400"));(* 25, 25 *)
(mk_real_int (num_of_string "42606667311748741258064370")),(mk_real_int (num_of_string "386996284735105375277153024"));(* 25, 26 *)
(mk_real_int (num_of_string "432762475821531753115024884")),(mk_real_int (num_of_string "60428984573049714105562944"));(* 26, 25 *)
(mk_real_int (num_of_string "227487149919928968358463616")),(mk_real_int (num_of_string "39844097904376052531519925"));(* 26, 25 *)
(mk_real_int (num_of_string "21100052167651158360764490")),(mk_real_int (num_of_string "2474538988937193138272250"));(* 25, 24 *)
(mk_real_int (num_of_string "59764375291679061912090000")),(mk_real_int (num_of_string "408757199628628865277362440"));(* 25, 26 *)
(mk_real_int (num_of_string "293375022403204497761621460")),(mk_real_int (num_of_string "218871167083916918168840"));(* 26, 23 *)
(mk_real_int (num_of_string "151813371483942071832299520")),(mk_real_int (num_of_string "116534404670309244919692216"));(* 26, 26 *)
(mk_real_int (num_of_string "17484780749475556318345821")),(mk_real_int (num_of_string "18174514982691974501658150"));(* 25, 25 *)
(mk_real_int (num_of_string "102294880353299775508448562")),(mk_real_int (num_of_string "42774094864858770210839130"));(* 26, 25 *)
(mk_real_int (num_of_string "180377116446286949609332000")),(mk_real_int (num_of_string "14832330275625175576817754"));(* 26, 25 *)
(mk_real_int (num_of_string "116597010652143178040561132")),(mk_real_int (num_of_string "31217787630465852473844252"));(* 26, 25 *)
(mk_real_int (num_of_string "127069017656524001777891484")),(mk_real_int (num_of_string "38475100647452593157685344"));(* 26, 25 *)
(mk_real_int (num_of_string "22175770998075528819117968")),(mk_real_int (num_of_string "6548475115429724533445065"));(* 25, 24 *)
(mk_real_int (num_of_string "37855920529179272699621910")),(mk_real_int (num_of_string "38155856770033747757052824"));(* 25, 25 *)
(mk_real_int (num_of_string "57843151422402117415122600")),(mk_real_int (num_of_string "50485350541793385229687825"));(* 25, 25 *)
(mk_real_int (num_of_string "144830598434319012455122455")),(mk_real_int (num_of_string "2317615381936096966451284"));(* 26, 24 *)
(mk_real_int (num_of_string "6440933838341110674529656")),(mk_real_int (num_of_string "36678142026905685251458816"));(* 24, 25 *)
(mk_real_int (num_of_string "433307679629248635678879664")),(mk_real_int (num_of_string "11819933827402188445898889"));(* 26, 25 *)
(mk_real_int (num_of_string "413552813457591378440417172")),(mk_real_int (num_of_string "2370114655023672844352415"));(* 26, 24 *)
(mk_real_int (num_of_string "381592807026891004210530024")),(mk_real_int (num_of_string "23918209491624178001286306"));(* 26, 25 *)
(mk_real_int (num_of_string "2880682738242672558327570")),(mk_real_int (num_of_string "13091558997555007487124750"));(* 24, 25 *)
(mk_real_int (num_of_string "68415054245365993307612856")),(mk_real_int (num_of_string "27335270311783553810661150"));(* 25, 25 *)
(mk_real_int (num_of_string "68824075509518787369288000")),(mk_real_int (num_of_string "130699038071193197542916024"));(* 25, 26 *)
(mk_real_int (num_of_string "149692501146787462640247084")),(mk_real_int (num_of_string "240702242348489251145947578"));(* 26, 26 *)
(mk_real_int (num_of_string "630202859455058775168716562")),(mk_real_int (num_of_string "9364327023497089028228424"));(* 26, 24 *)
(mk_real_int (num_of_string "8194282447954401886601940")),(mk_real_int (num_of_string "5907856506213803820357528"));(* 24, 24 *)
(mk_real_int (num_of_string "273697355872961074797417360")),(mk_real_int (num_of_string "150803123434928559675282864"));(* 26, 26 *)
(mk_real_int (num_of_string "68107303220672968529882640")),(mk_real_int (num_of_string "28003487427337142001839760"));(* 25, 25 *)
(mk_real_int (num_of_string "1207440584204555237241936")),(mk_real_int (num_of_string "32972864614840263913609995"));(* 24, 25 *)
(mk_real_int (num_of_string "54066665157718384858899040")),(mk_real_int (num_of_string "29959620313042408507793820"));(* 25, 25 *)
(mk_real_int (num_of_string "7233159082053229457781600")),(mk_real_int (num_of_string "11156557785799733017366040"));(* 24, 25 *)
(mk_real_int (num_of_string "138966653174705067826470240")),(mk_real_int (num_of_string "9291664960599268652165376"));(* 26, 24 *)
(mk_real_int (num_of_string "169972300361500924594042389")),(mk_real_int (num_of_string "4413079524608170346764530"));(* 26, 24 *)
(mk_real_int (num_of_string "84541915116590126922255865")),(mk_real_int (num_of_string "64210651997581348429214590"));(* 25, 25 *)
(mk_real_int (num_of_string "341558248172906490485760000")),(mk_real_int (num_of_string "439592092466087084593200"));(* 26, 23 *)
(mk_real_int (num_of_string "42126038393653776780718092")),(mk_real_int (num_of_string "270826520340126533036428560"));(* 25, 26 *)
(mk_real_int (num_of_string "90930720798220387537223424")),(mk_real_int (num_of_string "8773292440491244974039780"));(* 25, 24 *)
(mk_real_int (num_of_string "284133809286685816779976749")),(mk_real_int (num_of_string "6700657656298225520425536"));(* 26, 24 *)
(mk_real_int (num_of_string "54144075442858450273924884")),(mk_real_int (num_of_string "180923677764729133123196160"));(* 25, 26 *)
(mk_real_int (num_of_string "15676132970032719869814232")),(mk_real_int (num_of_string "28904759958888678466749750"));(* 25, 25 *)
(mk_real_int (num_of_string "137394936322327291185903996")),(mk_real_int (num_of_string "18863776467047311971806568"));(* 26, 25 *)
(mk_real_int (num_of_string "13086061688448502773379800")),(mk_real_int (num_of_string "123851340106619139880898460"));(* 25, 26 *)
(mk_real_int (num_of_string "85944825088247334931481042")),(mk_real_int (num_of_string "189767266075150625243516316"));(* 25, 26 *)
(mk_real_int (num_of_string "163664221180260231209025540")),(mk_real_int (num_of_string "583851214597978383351589222"));(* 26, 26 *)
(mk_real_int (num_of_string "37860780007495792760952960")),(mk_real_int (num_of_string "12778131621039471728533360"));(* 25, 25 *)
(mk_real_int (num_of_string "136817600367802836798965376")),(mk_real_int (num_of_string "521845340550023270457086256"));(* 26, 26 *)
(mk_real_int (num_of_string "142943303921608096692725760")),(mk_real_int (num_of_string "527129409690096035300231552"));(* 26, 26 *)
(mk_real_int (num_of_string "228192482314268172630910400")),(mk_real_int (num_of_string "1013184771008012182383480"));(* 26, 24 *)
(mk_real_int (num_of_string "284966383659304188432234872")),(mk_real_int (num_of_string "139862027335054289986974682"));(* 26, 26 *)
(mk_real_int (num_of_string "71979681018288710690766720")),(mk_real_int (num_of_string "131118939488925032042497085"));(* 25, 26 *)
(mk_real_int (num_of_string "3698845606957178920011888")),(mk_real_int (num_of_string "163085472877520936807863376"));(* 24, 26 *)
(mk_real_int (num_of_string "8905425850527301146493785")),(mk_real_int (num_of_string "636587027411585395340994336"));(* 24, 26 *)
(mk_real_int (num_of_string "89142201410580866361271032")),(mk_real_int (num_of_string "3094359649636480460202033"));(* 25, 24 *)
(mk_real_int (num_of_string "15968438653457955002150650")),(mk_real_int (num_of_string "264373093500393728602313730"));(* 25, 26 *)
(mk_real_int (num_of_string "39828055776355211157821000")),(mk_real_int (num_of_string "124398766489224912927855956"));(* 25, 26 *)
(mk_real_int (num_of_string "8299838641638307056156864")),(mk_real_int (num_of_string "186379865255583232029023760"));(* 24, 26 *)
(mk_real_int (num_of_string "1183930684103930299403328")),(mk_real_int (num_of_string "564163247888081401933762438"));(* 24, 26 *)
(mk_real_int (num_of_string "153348617940843081052099200")),(mk_real_int (num_of_string "441122041075546542065560470"));(* 26, 26 *)
(mk_real_int (num_of_string "48304733207115523885478352")),(mk_real_int (num_of_string "76880188932365475224283888"));(* 25, 25 *)
(mk_real_int (num_of_string "18702787100091352779881184")),(mk_real_int (num_of_string "51504501207002436545700384"));(* 25, 25 *)
(mk_real_int (num_of_string "406128143542930114952435776")),(mk_real_int (num_of_string "235445646626131469338850436"));(* 26, 26 *)
(mk_real_int (num_of_string "2518794099870168961723968")),(mk_real_int (num_of_string "7006499916484090399935925"));(* 24, 24 *)
(mk_real_int (num_of_string "56935896013938897775248000")),(mk_real_int (num_of_string "4945952316545763910868295"));(* 25, 24 *)
(mk_real_int (num_of_string "14295198370185450197895690")),(mk_real_int (num_of_string "44886840142202859220172280"));(* 25, 25 *)
(mk_real_int (num_of_string "34048000668778865054869306")),(mk_real_int (num_of_string "10343997920679684100803162"));(* 25, 25 *)
(mk_real_int (num_of_string "4998688624991694952344560")),(mk_real_int (num_of_string "143450095820117659757697966"));(* 24, 26 *)
(mk_real_int (num_of_string "134809209719333955482376805")),(mk_real_int (num_of_string "62817370689153077903586496"));(* 26, 25 *)
(mk_real_int (num_of_string "46545002518935663461515734")),(mk_real_int (num_of_string "22136807729153903782598"));(* 25, 22 *)
(mk_real_int (num_of_string "231320380305338995733056470")),(mk_real_int (num_of_string "40762457382983352092941800"));(* 26, 25 *)
(mk_real_int (num_of_string "5243608931912070341868320")),(mk_real_int (num_of_string "328496367160679863378662636"));(* 24, 26 *)
(mk_real_int (num_of_string "78335175346971017245822656")),(mk_real_int (num_of_string "4037335805335132206892224"));(* 25, 24 *)
(mk_real_int (num_of_string "76851310403192888508389384")),(mk_real_int (num_of_string "417603323590561704097796820"));(* 25, 26 *)
(mk_real_int (num_of_string "309765547622742071732140720")),(mk_real_int (num_of_string "2140281490297082509880584"));(* 26, 24 *)
(mk_real_int (num_of_string "14587406451071071593458112")),(mk_real_int (num_of_string "13567606530506878728033480"));(* 25, 25 *)
(mk_real_int (num_of_string "30909143867698486689818280")),(mk_real_int (num_of_string "171948683472085390025830350"));(* 25, 26 *)
(mk_real_int (num_of_string "329350562655522352548479239")),(mk_real_int (num_of_string "198915807602938493551929375"));(* 26, 26 *)
(mk_real_int (num_of_string "283398362508097483533241875")),(mk_real_int (num_of_string "106947705437480099228607920"));(* 26, 26 *)
(mk_real_int (num_of_string "28825668235183994805198720")),(mk_real_int (num_of_string "30578934153823237165140300"));(* 25, 25 *)
(mk_real_int (num_of_string "99641329072448545880630272")),(mk_real_int (num_of_string "177398751432818387009057975"));(* 25, 26 *)
(mk_real_int (num_of_string "136631921650144573041101570")),(mk_real_int (num_of_string "169990813732200406015243920"));(* 26, 26 *)
(mk_real_int (num_of_string "547651661083809285597087780")),(mk_real_int (num_of_string "33650947287541384842179448"));(* 26, 25 *)
(mk_real_int (num_of_string "87628013456926484529321264")),(mk_real_int (num_of_string "879845852002806031829040"));(* 25, 23 *)
(mk_real_int (num_of_string "4908676645804887990181278")),(mk_real_int (num_of_string "441846058335908737321860865"));(* 24, 26 *)
(mk_real_int (num_of_string "84450065805438253006400864")),(mk_real_int (num_of_string "8569044747690184954598220"));(* 25, 24 *)
(mk_real_int (num_of_string "13606674698615042865589002")),(mk_real_int (num_of_string "1432263432315605152073580"));(* 25, 24 *)
(mk_real_int (num_of_string "12062232294905013060919248")),(mk_real_int (num_of_string "34664785030711497887141308"));(* 25, 25 *)
(mk_real_int (num_of_string "247594656506620624251330726")),(mk_real_int (num_of_string "107993444103317404537012251"));(* 26, 26 *)
(mk_real_int (num_of_string "113216758697900474822183706")),(mk_real_int (num_of_string "112466879803293619913439984"));(* 26, 26 *)
(mk_real_int (num_of_string "4825686946305259779196560")),(mk_real_int (num_of_string "7136289067183337748952640"));(* 24, 24 *)
(mk_real_int (num_of_string "1010676748972984487852130")),(mk_real_int (num_of_string "92284413749865758640841632"));(* 24, 25 *)
(mk_real_int (num_of_string "459061040556543175374093210")),(mk_real_int (num_of_string "173996819588173280251383792"));(* 26, 26 *)
(mk_real_int (num_of_string "537902419795523366748652416")),(mk_real_int (num_of_string "22560293066854997080245300"));(* 26, 25 *)
(mk_real_int (num_of_string "482322932502981711219346360")),(mk_real_int (num_of_string "307590494254998475638843916"));(* 26, 26 *)
(mk_real_int (num_of_string "8587526681855000025123960")),(mk_real_int (num_of_string "253747057535852581222375464"));(* 24, 26 *)
(mk_real_int (num_of_string "311101646642991021722059638")),(mk_real_int (num_of_string "17565704386223597494534904"));(* 26, 25 *)
(mk_real_int (num_of_string "491995824996186989063536860")),(mk_real_int (num_of_string "86754176544338465800871406"));(* 26, 25 *)
(mk_real_int (num_of_string "94749468619620781232730750")),(mk_real_int (num_of_string "100374696723335749379379540"));(* 25, 26 *)
(mk_real_int (num_of_string "655795296167781814929696")),(mk_real_int (num_of_string "185835236435789341822567758"));(* 23, 26 *)
(mk_real_int (num_of_string "92063819930097855967633350")),(mk_real_int (num_of_string "28205824513991777773317648"));(* 25, 25 *)
(mk_real_int (num_of_string "4314308765234760753611654")),(mk_real_int (num_of_string "309142043906615848157007636"));(* 24, 26 *)
(mk_real_int (num_of_string "9343889322909695200241520")),(mk_real_int (num_of_string "183573158621721618091118469"));(* 24, 26 *)
(mk_real_int (num_of_string "40082659138319946062164320")),(mk_real_int (num_of_string "38425284035766453385888560"));(* 25, 25 *)
(mk_real_int (num_of_string "32026393844255312517338568")),(mk_real_int (num_of_string "3175078668445839083467320"));(* 25, 24 *)
(mk_real_int (num_of_string "40866589119655878995554666")),(mk_real_int (num_of_string "181026690893665978064473350"));(* 25, 26 *)
(mk_real_int (num_of_string "165410107973990174679726342")),(mk_real_int (num_of_string "182794793727053519475224874"));(* 26, 26 *)
(mk_real_int (num_of_string "828148912536367165002846104")),(mk_real_int (num_of_string "33973982175637031011398306"));(* 26, 25 *)
(mk_real_int (num_of_string "109827339909185901762960520")),(mk_real_int (num_of_string "408347416592048593365101760"));(* 26, 26 *)
(mk_real_int (num_of_string "16805713054520384908568800")),(mk_real_int (num_of_string "35752691877220840724394016"));(* 25, 25 *)
(mk_real_int (num_of_string "337556867222368121357319000")),(mk_real_int (num_of_string "135958404980427250277403738"));(* 26, 26 *)
(mk_real_int (num_of_string "44068982235389203342335939")),(mk_real_int (num_of_string "38866582043422555012045110"));(* 25, 25 *)
(mk_real_int (num_of_string "66821470063256317008532988")),(mk_real_int (num_of_string "15678887987997917382100032"));(* 25, 25 *)
(mk_real_int (num_of_string "215850018019396246498114197")),(mk_real_int (num_of_string "18815320840448603266168324"));(* 26, 25 *)
(mk_real_int (num_of_string "15759833257011943660822840")),(mk_real_int (num_of_string "58626289552216347744293994"));(* 25, 25 *)
(mk_real_int (num_of_string "3409969265701152644768118")),(mk_real_int (num_of_string "343142654659530429339503658"));(* 24, 26 *)
(mk_real_int (num_of_string "6452259642856377638631720")),(mk_real_int (num_of_string "139775217074171069226279906"));(* 24, 26 *)
(mk_real_int (num_of_string "191525159925802318908085380")),(mk_real_int (num_of_string "12023967098364570752980500"));(* 26, 25 *)
(mk_real_int (num_of_string "73621746440650219693193949")),(mk_real_int (num_of_string "45043560960865503257456928"));(* 25, 25 *)
(mk_real_int (num_of_string "98701174745674834537799595")),(mk_real_int (num_of_string "50816854226398908283859520"));(* 25, 25 *)
(mk_real_int (num_of_string "23067094995968067383621350")),(mk_real_int (num_of_string "56266157940314801963163240"));(* 25, 25 *)
(mk_real_int (num_of_string "183213940892020927024657248")),(mk_real_int (num_of_string "97050236525127603028248200"));(* 26, 25 *)
(mk_real_int (num_of_string "89626869402248472001400734")),(mk_real_int (num_of_string "1566643635132717218313509"));(* 25, 24 *)
(mk_real_int (num_of_string "72242836100364229799337552")),(mk_real_int (num_of_string "95861015548805388645878620"));(* 25, 25 *)
(mk_real_int (num_of_string "39597942981151349107233030")),(mk_real_int (num_of_string "45039604931841096080868078"));(* 25, 25 *)
(mk_real_int (num_of_string "43687422537843389185938750")),(mk_real_int (num_of_string "84049920160236379670484240"));(* 25, 25 *)
(mk_real_int (num_of_string "411565037771379264101097755")),(mk_real_int (num_of_string "165494732185952810852321980"));(* 26, 26 *)
(mk_real_int (num_of_string "94564659648540560101982832")),(mk_real_int (num_of_string "112980673902305644571540999"));(* 25, 26 *)
(mk_real_int (num_of_string "27814519827804493060896444")),(mk_real_int (num_of_string "86490087066532327313744163"));(* 25, 25 *)
(mk_real_int (num_of_string "283144251629266347748626")),(mk_real_int (num_of_string "15209429071971594291899284"));(* 23, 25 *)
(mk_real_int (num_of_string "82149830468462742526021068")),(mk_real_int (num_of_string "224494625182459051309505"));(* 25, 23 *)
(mk_real_int (num_of_string "299881512253452746774592486")),(mk_real_int (num_of_string "9860371895115123743625921"));(* 26, 24 *)
(mk_real_int (num_of_string "206818428412442944307351643")),(mk_real_int (num_of_string "204190025922701357103292054"));(* 26, 26 *)
(mk_real_int (num_of_string "87449772093639243055590420")),(mk_real_int (num_of_string "39786801256794767123858850"));(* 25, 25 *)
(mk_real_int (num_of_string "47587109693748658601305320")),(mk_real_int (num_of_string "68325587245626600656371248"));(* 25, 25 *)
(mk_real_int (num_of_string "116400388691467979008951887")),(mk_real_int (num_of_string "74086503954898207401365800"));(* 26, 25 *)
(mk_real_int (num_of_string "1743461910739837051340800")),(mk_real_int (num_of_string "316154385624651453365830920"));(* 24, 26 *)
(mk_real_int (num_of_string "34822079958796102509727320")),(mk_real_int (num_of_string "680973349518754190312937720"));(* 25, 26 *)
(mk_real_int (num_of_string "227844683016571821439892672")),(mk_real_int (num_of_string "56319719397273660320370840"));(* 26, 25 *)
(mk_real_int (num_of_string "162396539567128686983284500")),(mk_real_int (num_of_string "27090726872164554117045923"));(* 26, 25 *)
(mk_real_int (num_of_string "23896359646767419199897060")),(mk_real_int (num_of_string "67812918734516816387612700"));(* 25, 25 *)
(mk_real_int (num_of_string "271158207804428091830585400")),(mk_real_int (num_of_string "28493892205342331219639040"));(* 26, 25 *)
(mk_real_int (num_of_string "5956840078688659504383072")),(mk_real_int (num_of_string "24811891938949034457921078"));(* 24, 25 *)
(mk_real_int (num_of_string "3163031144871036604935000")),(mk_real_int (num_of_string "742272817957385845081907970"));(* 24, 26 *)
(mk_real_int (num_of_string "191829790885820607747431424")),(mk_real_int (num_of_string "267244401906419504639056748"));(* 26, 26 *)
(mk_real_int (num_of_string "226519296543724826563612800")),(mk_real_int (num_of_string "89497633470742680920554944"));(* 26, 25 *)
(mk_real_int (num_of_string "16455032487236828809574712")),(mk_real_int (num_of_string "14197396101095672012604888"));(* 25, 25 *)
(mk_real_int (num_of_string "134990402598945387865843290")),(mk_real_int (num_of_string "143835377063621682181514775"));(* 26, 26 *)
(mk_real_int (num_of_string "37722759133300884188434872")),(mk_real_int (num_of_string "33448200553702272780779226"));(* 25, 25 *)
(mk_real_int (num_of_string "191878103529698068666248120")),(mk_real_int (num_of_string "175596066951032342102319104"));(* 26, 26 *)
(mk_real_int (num_of_string "203372649411301168358031912")),(mk_real_int (num_of_string "23927478274089051116434668"));(* 26, 25 *)
(mk_real_int (num_of_string "8983788064413857175782400")),(mk_real_int (num_of_string "9264303679062958904971593"));(* 24, 24 *)
(mk_real_int (num_of_string "85100232319660509537721120")),(mk_real_int (num_of_string "45365340136835023531096200"));(* 25, 25 *)
(mk_real_int (num_of_string "73667920350501717096054891")),(mk_real_int (num_of_string "1539729172024025445302112"));(* 25, 24 *)
(mk_real_int (num_of_string "57535101050574909644701770")),(mk_real_int (num_of_string "469893668842766525287656500"));(* 25, 26 *)
(mk_real_int (num_of_string "246847915628602615268224948")),(mk_real_int (num_of_string "271376277076841497105990592"));(* 26, 26 *)
(mk_real_int (num_of_string "141423626885762883645658480")),(mk_real_int (num_of_string "428426319578461487027555292"));(* 26, 26 *)
(mk_real_int (num_of_string "116985306865956530171964024")),(mk_real_int (num_of_string "212376781502879493829014448"));(* 26, 26 *)
(mk_real_int (num_of_string "766091453676938418163236")),(mk_real_int (num_of_string "474121605480538873992152352"));(* 23, 26 *)
(mk_real_int (num_of_string "62032387050305848371495784")),(mk_real_int (num_of_string "34401892369026212515468494"));(* 25, 25 *)
(mk_real_int (num_of_string "4546012157562503974185840")),(mk_real_int (num_of_string "14928746929885255903248786"));(* 24, 25 *)
(mk_real_int (num_of_string "94910417363135133424373220")),(mk_real_int (num_of_string "220506010009543483512964600"));(* 25, 26 *)
(mk_real_int (num_of_string "93209032129864465047468960")),(mk_real_int (num_of_string "7557159214165560245035920"));(* 25, 24 *)
(mk_real_int (num_of_string "51115413616554966190864638")),(mk_real_int (num_of_string "480071230107948759091146864"));(* 25, 26 *)
(mk_real_int (num_of_string "78494778688317133570804344")),(mk_real_int (num_of_string "279200207771399157718709420"));(* 25, 26 *)
(mk_real_int (num_of_string "20795325633069015680028032")),(mk_real_int (num_of_string "7702315779652881337335591"));(* 25, 24 *)
(mk_real_int (num_of_string "346685094670933649514656")),(mk_real_int (num_of_string "3617096870785930016576000"));(* 23, 24 *)
(mk_real_int (num_of_string "736802279408600622213647196")),(mk_real_int (num_of_string "2771246625256818916912185"));(* 26, 24 *)
(mk_real_int (num_of_string "9996890352759373330266480")),(mk_real_int (num_of_string "19163675861627686170314512"));(* 24, 25 *)
(mk_real_int (num_of_string "7437773420711573654314180")),(mk_real_int (num_of_string "132870661467350131995510435"));(* 24, 26 *)
(mk_real_int (num_of_string "330254818492807679142247992")),(mk_real_int (num_of_string "18319151886846357898020000"));(* 26, 25 *)
(mk_real_int (num_of_string "187232044748904179245742160")),(mk_real_int (num_of_string "1626592629177686269559670"));(* 26, 24 *)
(mk_real_int (num_of_string "27188703849642811969160195")),(mk_real_int (num_of_string "146909056403366349661081344"));(* 25, 26 *)
(mk_real_int (num_of_string "344931949533824518830114384")),(mk_real_int (num_of_string "294446460739381647455230252"));(* 26, 26 *)
(mk_real_int (num_of_string "14269048229523221417898912")),(mk_real_int (num_of_string "5657498906931867438372657"));(* 25, 24 *)
(mk_real_int (num_of_string "66762609144321115387855197")),(mk_real_int (num_of_string "49191141034222668393307992"));(* 25, 25 *)
(mk_real_int (num_of_string "305039429558344054605756404")),(mk_real_int (num_of_string "84591372551688183439940192"));(* 26, 25 *)
(mk_real_int (num_of_string "97515874953651444002865152")),(mk_real_int (num_of_string "691673499981880613023704440"));(* 25, 26 *)
(mk_real_int (num_of_string "29193100209236239547618853")),(mk_real_int (num_of_string "70521355040509474901701800"));(* 25, 25 *)
(mk_real_int (num_of_string "7513807692770715060631368")),(mk_real_int (num_of_string "55616442020934041820861816"));(* 24, 25 *)
(mk_real_int (num_of_string "205457625967141352646225642")),(mk_real_int (num_of_string "132515117147444878942936158"));(* 26, 26 *)
(mk_real_int (num_of_string "2973338307145599568749495")),(mk_real_int (num_of_string "92638886888151184120929108"));(* 24, 25 *)
(mk_real_int (num_of_string "86518290223536728695440120")),(mk_real_int (num_of_string "35593212083793255633227086"));(* 25, 25 *)
(mk_real_int (num_of_string "6157307775193447072415280")),(mk_real_int (num_of_string "16082239463539779536364848"));(* 24, 25 *)
(mk_real_int (num_of_string "13420898736213601671340400")),(mk_real_int (num_of_string "82450648926482427213525000"));(* 25, 25 *)
(mk_real_int (num_of_string "99880834288730851673858400")),(mk_real_int (num_of_string "5741253896300511748696800"));(* 25, 24 *)
(mk_real_int (num_of_string "2146462596215413627049868")),(mk_real_int (num_of_string "645168839682234316675215"));(* 24, 23 *)
(mk_real_int (num_of_string "44093965822174619804977200")),(mk_real_int (num_of_string "308822880869809893193894416"));(* 25, 26 *)
(mk_real_int (num_of_string "5892845797658658963336576")),(mk_real_int (num_of_string "36014886084378441527849820"));(* 24, 25 *)
(mk_real_int (num_of_string "415864868921156209509985940")),(mk_real_int (num_of_string "52587340634428081205369772"));(* 26, 25 *)
(mk_real_int (num_of_string "11746692427581616073269140")),(mk_real_int (num_of_string "452764829553174823722320"));(* 25, 23 *)
(mk_real_int (num_of_string "85945724873576799471637600")),(mk_real_int (num_of_string "9261455435860466089152000"));(* 25, 24 *)
(mk_real_int (num_of_string "114552630894373987509331912")),(mk_real_int (num_of_string "108697081925857447766794380"));(* 26, 26 *)
(mk_real_int (num_of_string "65771426224612534605414012")),(mk_real_int (num_of_string "389280266590187169727232296"));(* 25, 26 *)
(mk_real_int (num_of_string "64881020471859832650818589")),(mk_real_int (num_of_string "1568335636534885330810368"));(* 25, 24 *)
(mk_real_int (num_of_string "50259031211335890622802004")),(mk_real_int (num_of_string "94948675787790649525339290"));(* 25, 25 *)
(mk_real_int (num_of_string "790190233716089598559808")),(mk_real_int (num_of_string "524421817064509565073259992"));(* 23, 26 *)
(mk_real_int (num_of_string "73650563171999770916568609")),(mk_real_int (num_of_string "151806905852700479420063376"));(* 25, 26 *)
(mk_real_int (num_of_string "350166527476784211587639784")),(mk_real_int (num_of_string "219753780282997951788344232"));(* 26, 26 *)
(mk_real_int (num_of_string "4245001554147357653832270")),(mk_real_int (num_of_string "2885160683483009403878400"));(* 24, 24 *)
(mk_real_int (num_of_string "237510981757850421510457260")),(mk_real_int (num_of_string "3374762674704642792779370"));(* 26, 24 *)
(mk_real_int (num_of_string "67492576532860916816586240")),(mk_real_int (num_of_string "33239155246689652756908048"));(* 25, 25 *)
(mk_real_int (num_of_string "242118077416687146010806080")),(mk_real_int (num_of_string "151813349260759445946757330"));(* 26, 26 *)
(mk_real_int (num_of_string "7468515125860164831692412")),(mk_real_int (num_of_string "46102906513687678293051486"));(* 24, 25 *)
(mk_real_int (num_of_string "121454008074660255105623810")),(mk_real_int (num_of_string "31561260882577397678847384"));(* 26, 25 *)
(mk_real_int (num_of_string "15200017655157476666233570")),(mk_real_int (num_of_string "6503985635860530075357600"));(* 25, 24 *)
(mk_real_int (num_of_string "648324969256675815602262150")),(mk_real_int (num_of_string "21777313269829092051129480"));(* 26, 25 *)
(mk_real_int (num_of_string "30756207353423144579068500")),(mk_real_int (num_of_string "155731081504024968238354568"));(* 25, 26 *)
(mk_real_int (num_of_string "479081794171155796836742302")),(mk_real_int (num_of_string "151753809174650640323491840"));(* 26, 26 *)
(mk_real_int (num_of_string "11078051882191222004813415")),(mk_real_int (num_of_string "519619608171787236569919000"));(* 25, 26 *)
(mk_real_int (num_of_string "66352522069723354505562570")),(mk_real_int (num_of_string "14423653822341810361771412"));(* 25, 25 *)
(mk_real_int (num_of_string "3673768608245325848010368")),(mk_real_int (num_of_string "66772662607545392321311824"));(* 24, 25 *)
(mk_real_int (num_of_string "30077521700719583707846320")),(mk_real_int (num_of_string "21705893618607616899782070"));(* 25, 25 *)
(mk_real_int (num_of_string "95642237542137967801731520")),(mk_real_int (num_of_string "178672124964119436708997050"));(* 25, 26 *)
(mk_real_int (num_of_string "45369040420819630960896165")),(mk_real_int (num_of_string "92037728831035290876409980"));(* 25, 25 *)
(mk_real_int (num_of_string "34677444316335721837565000")),(mk_real_int (num_of_string "187222367965936608198593370"));(* 25, 26 *)
(mk_real_int (num_of_string "2709515955176139369580672")),(mk_real_int (num_of_string "9161798408105298036475782"));(* 24, 24 *)
(mk_real_int (num_of_string "44693267602288459053572020")),(mk_real_int (num_of_string "615357360379781255177417217"));(* 25, 26 *)
(mk_real_int (num_of_string "214175265710793927902654250")),(mk_real_int (num_of_string "23821232986579606655612238"));(* 26, 25 *)
(mk_real_int (num_of_string "199458987571580038333543295")),(mk_real_int (num_of_string "310615928569618167757051800"));(* 26, 26 *)
(mk_real_int (num_of_string "181110399388169266742474727")),(mk_real_int (num_of_string "9614395742898676279662882"));(* 26, 24 *)
(mk_real_int (num_of_string "23513121951469005953325120")),(mk_real_int (num_of_string "132156691181845140516367536"));(* 25, 26 *)
(mk_real_int (num_of_string "57084948980178074963258367")),(mk_real_int (num_of_string "9306533557766076735781455"));(* 25, 24 *)
(mk_real_int (num_of_string "110186075325816552267975468")),(mk_real_int (num_of_string "373779926075700375570000000"));(* 26, 26 *)
(mk_real_int (num_of_string "59356836087430550483121912")),(mk_real_int (num_of_string "84912410498754265576003008"));(* 25, 25 *)
(mk_real_int (num_of_string "16137589430467035463230774")),(mk_real_int (num_of_string "130172207477002210633048320"));(* 25, 26 *)
(mk_real_int (num_of_string "72073790395213864881139040")),(mk_real_int (num_of_string "16297986355403817143871000"));(* 25, 25 *)
(mk_real_int (num_of_string "36144887168704655803747446")),(mk_real_int (num_of_string "99777291684275949636786600"));(* 25, 25 *)
(mk_real_int (num_of_string "322809309325110308440741474")),(mk_real_int (num_of_string "47748371847639645180450816"));(* 26, 25 *)
(mk_real_int (num_of_string "95462093067891793274315680")),(mk_real_int (num_of_string "23996920508724788662801920"));(* 25, 25 *)
(mk_real_int (num_of_string "17523931379594670358777680")),(mk_real_int (num_of_string "103231477535224497815535300"));(* 25, 26 *)
(mk_real_int (num_of_string "224935664588137217579543040")),(mk_real_int (num_of_string "940015791620835233081085"));(* 26, 23 *)
(mk_real_int (num_of_string "58788947982575409123778600")),(mk_real_int (num_of_string "11485999042076404832742000"));(* 25, 25 *)
(mk_real_int (num_of_string "88937334091851478030034640")),(mk_real_int (num_of_string "20408764400562625224153660"));(* 25, 25 *)
(mk_real_int (num_of_string "1351169393377393176823808")),(mk_real_int (num_of_string "42038643409854598695912812"));(* 24, 25 *)
(mk_real_int (num_of_string "93025556167144210440138840")),(mk_real_int (num_of_string "470146802486038291505640000"));(* 25, 26 *)
(mk_real_int (num_of_string "32919471526449773889662958")),(mk_real_int (num_of_string "15337179591731762467177280"));(* 25, 25 *)
(mk_real_int (num_of_string "255960058165114659612296898")),(mk_real_int (num_of_string "31895676634714912760544344"));(* 26, 25 *)
(mk_real_int (num_of_string "7652127059184302113950180")),(mk_real_int (num_of_string "3167982572272008158306880"));(* 24, 24 *)
(mk_real_int (num_of_string "121943388238227706297960488")),(mk_real_int (num_of_string "116752430660455551636510920"));(* 26, 26 *)
(mk_real_int (num_of_string "91141287274092517721823270")),(mk_real_int (num_of_string "79015733961557027161214922"));(* 25, 25 *)
(mk_real_int (num_of_string "103212324289841072748962940")),(mk_real_int (num_of_string "23502581069283562153293760"));(* 26, 25 *)
(mk_real_int (num_of_string "61614558847678542748661124")),(mk_real_int (num_of_string "30080373129063928545001335"));(* 25, 25 *)
(mk_real_int (num_of_string "67348570429438607390372760")),(mk_real_int (num_of_string "252253949451085013543273880"));(* 25, 26 *)
(mk_real_int (num_of_string "5950181556420393069816192")),(mk_real_int (num_of_string "115096599793294399632965184"));(* 24, 26 *)
(mk_real_int (num_of_string "197289115083308089086645368")),(mk_real_int (num_of_string "262985948481156523157561528"));(* 26, 26 *)
(mk_real_int (num_of_string "326688936905310894901958400")),(mk_real_int (num_of_string "128478388908257244413502960"));(* 26, 26 *)
(mk_real_int (num_of_string "13435497654971261923470508")),(mk_real_int (num_of_string "244760622394318696657811688"));(* 25, 26 *)
(mk_real_int (num_of_string "53693401818520230944999040")),(mk_real_int (num_of_string "272454686606824072235110590"));(* 25, 26 *)
(mk_real_int (num_of_string "164225008028941516988763110")),(mk_real_int (num_of_string "44076863789195264272202283"));(* 26, 25 *)
(mk_real_int (num_of_string "111781556599484113990738200")),(mk_real_int (num_of_string "487589044616521629260928"));(* 26, 23 *)
(mk_real_int (num_of_string "36350761507453325764481760")),(mk_real_int (num_of_string "347374166095670267300651520"));(* 25, 26 *)
(mk_real_int (num_of_string "4404942392921450910539208")),(mk_real_int (num_of_string "16444722093731286642870604"));(* 24, 25 *)
(mk_real_int (num_of_string "34998542391989350171813324")),(mk_real_int (num_of_string "84819422723869175977829376"));(* 25, 25 *)
(mk_real_int (num_of_string "142508624656563484960180176")),(mk_real_int (num_of_string "130849540384544543867467760"));(* 26, 26 *)
(mk_real_int (num_of_string "43986798679684733492603976")),(mk_real_int (num_of_string "76796829600524767256418600"));(* 25, 25 *)
(mk_real_int (num_of_string "4640303951091638102707632")),(mk_real_int (num_of_string "95288029738926444070197300"));(* 24, 25 *)
(mk_real_int (num_of_string "51686196587942632748001868")),(mk_real_int (num_of_string "287668623895644101033490255"));(* 25, 26 *)
(mk_real_int (num_of_string "15011398046653417983945774")),(mk_real_int (num_of_string "63028631677435065516125384"));(* 25, 25 *)
(mk_real_int (num_of_string "63216540212824961625516768")),(mk_real_int (num_of_string "219251594828186673098220"));(* 25, 23 *)
(mk_real_int (num_of_string "42379870300474368690480488")),(mk_real_int (num_of_string "7627042596971518427619720"));(* 25, 24 *)
(mk_real_int (num_of_string "5503946748109005467824722")),(mk_real_int (num_of_string "320500583033903645465503488"));(* 24, 26 *)
(mk_real_int (num_of_string "66499538008604918794833828")),(mk_real_int (num_of_string "17140735203194607391207382"));(* 25, 25 *)
(mk_real_int (num_of_string "72397763758837572475412478")),(mk_real_int (num_of_string "334939552279180111362131970"));(* 25, 26 *)
(mk_real_int (num_of_string "12405146054091027622802040")),(mk_real_int (num_of_string "71841725875555855637450640"));(* 25, 25 *)
(mk_real_int (num_of_string "11534060791051108128203690")),(mk_real_int (num_of_string "60325163633529506262456360"));(* 25, 25 *)
(mk_real_int (num_of_string "299487775163966216348847228")),(mk_real_int (num_of_string "68812516903112439267275028"));(* 26, 25 *)
(mk_real_int (num_of_string "506849656895603265992374620")),(mk_real_int (num_of_string "46981860287044964395885056"));(* 26, 25 *)
(mk_real_int (num_of_string "3919145778705146796555840")),(mk_real_int (num_of_string "118464359635823539696419428"));(* 24, 26 *)
(mk_real_int (num_of_string "120999185201390185748233392")),(mk_real_int (num_of_string "1870967514738423738074454"));(* 26, 24 *)
(mk_real_int (num_of_string "120361650250624166252690724")),(mk_real_int (num_of_string "5984929271431735341528140"));(* 26, 24 *)
(mk_real_int (num_of_string "298195614557485690435380120")),(mk_real_int (num_of_string "40339061872612185698121015"));(* 26, 25 *)
(mk_real_int (num_of_string "206624463534576852523649088")),(mk_real_int (num_of_string "263583275731972832083619535"));(* 26, 26 *)
(mk_real_int (num_of_string "25759813401567234659878416")),(mk_real_int (num_of_string "1381377187766198724764370"));(* 25, 24 *)
(mk_real_int (num_of_string "14643926876456204547436500")),(mk_real_int (num_of_string "66035463286993257658481160"));(* 25, 25 *)
(mk_real_int (num_of_string "10239878780474324527028064")),(mk_real_int (num_of_string "123110027275150929706348275"));(* 25, 26 *)
(mk_real_int (num_of_string "52288380076897156628171883")),(mk_real_int (num_of_string "107640065587742738219248408"));(* 25, 26 *)
(mk_real_int (num_of_string "150187153762447331713114140")),(mk_real_int (num_of_string "216450251278049686422048"));(* 26, 23 *)
(mk_real_int (num_of_string "294469113902292273392121366")),(mk_real_int (num_of_string "2790586443249668493421200"));(* 26, 24 *)
(mk_real_int (num_of_string "130627031809654148720219120")),(mk_real_int (num_of_string "165611796432171376193818002"));(* 26, 26 *)
(mk_real_int (num_of_string "71316892944530455853281860")),(mk_real_int (num_of_string "74510409395918279108435544"));(* 25, 25 *)
(mk_real_int (num_of_string "150682336540333536496157600")),(mk_real_int (num_of_string "34877581958730675888086076"));(* 26, 25 *)
(mk_real_int (num_of_string "111334749782228031387393120")),(mk_real_int (num_of_string "239950072590491713719656560"));(* 26, 26 *)
(mk_real_int (num_of_string "22784254051740592329078160")),(mk_real_int (num_of_string "70950618239978846841850072"))(* 25, 25 *)
];;