let data = [ (mk_real_int (num_of_string "3680857660418378333747253")),(mk_real_int (num_of_string "4414269758065822047732996"));(* 24, 24 *) (mk_real_int (num_of_string "4869533942069625706034388")),(mk_real_int (num_of_string "2695321389480405743094754"));(* 24, 24 *) (mk_real_int (num_of_string "6026959379057037304561920")),(mk_real_int (num_of_string "3021227783731778829105340"));(* 24, 24 *) (mk_real_int (num_of_string "6069890482189228444287384")),(mk_real_int (num_of_string "2508693981660739820982375"));(* 24, 24 *) (mk_real_int (num_of_string "5085493857943497294277410")),(mk_real_int (num_of_string "2784707669039116279880796"));(* 24, 24 *) (mk_real_int (num_of_string "2529596662834216166045470")),(mk_real_int (num_of_string "5094971413369308935456745"));(* 24, 24 *) (mk_real_int (num_of_string "2083046894126884554363792")),(mk_real_int (num_of_string "4638708864695794085582280"));(* 24, 24 *) (mk_real_int (num_of_string "2853448616036064779238000")),(mk_real_int (num_of_string "3330517235861434969162152"));(* 24, 24 *) (mk_real_int (num_of_string "2619438989990631321152800")),(mk_real_int (num_of_string "3123403170002537185764864"));(* 24, 24 *) (mk_real_int (num_of_string "4053189443833334918741056")),(mk_real_int (num_of_string "5474988659661997619311874"));(* 24, 24 *) (mk_real_int (num_of_string "3346348473610119083580435")),(mk_real_int (num_of_string "4248285207423699106852671"));(* 24, 24 *) (mk_real_int (num_of_string "4275207716371465895734440")),(mk_real_int (num_of_string "2969374045599498823638480"));(* 24, 24 *) (mk_real_int (num_of_string "5169305558992765167994720")),(mk_real_int (num_of_string "3253553768332158469844600"));(* 24, 24 *) (mk_real_int (num_of_string "2062186532980711479654480")),(mk_real_int (num_of_string "3729404660533155628084500"));(* 24, 24 *) (mk_real_int (num_of_string "5495396336283149374902100")),(mk_real_int (num_of_string "4687638315669344249960665"));(* 24, 24 *) (mk_real_int (num_of_string "3931747933635968205820844")),(mk_real_int (num_of_string "2771712931061171659900226"));(* 24, 24 *) (mk_real_int (num_of_string "3510532587420800309052194")),(mk_real_int (num_of_string "2211596659077008563631250"));(* 24, 24 *) (mk_real_int (num_of_string "2123730420742821853609902")),(mk_real_int (num_of_string "7064299598380154058384000"));(* 24, 24 *) (mk_real_int (num_of_string "3105063047609196616212480")),(mk_real_int (num_of_string "2365140887350023350218560"));(* 24, 24 *) (mk_real_int (num_of_string "3064353092092804040987784")),(mk_real_int (num_of_string "2916432603768504021011712"));(* 24, 24 *) (mk_real_int (num_of_string "2383721772458811758230509")),(mk_real_int (num_of_string "2464945407055935999350025"));(* 24, 24 *) (mk_real_int (num_of_string "3478411509903167804854575")),(mk_real_int (num_of_string "4562581799306809054901328"));(* 24, 24 *) (mk_real_int (num_of_string "3621316804577343551566950")),(mk_real_int (num_of_string "2550994550215075643914053"));(* 24, 24 *) (mk_real_int (num_of_string "1750200282008421731464920")),(mk_real_int (num_of_string "5725458041781646050077524"));(* 24, 24 *) (mk_real_int (num_of_string "3192468630324760374194409")),(mk_real_int (num_of_string "3403776646428500725809612"));(* 24, 24 *) (mk_real_int (num_of_string "3417435761634201385811744")),(mk_real_int (num_of_string "2479391179062576469550968"));(* 24, 24 *) (mk_real_int (num_of_string "5975071497508369324180932")),(mk_real_int (num_of_string "2562568339906846968281410"));(* 24, 24 *) (mk_real_int (num_of_string "4322874197996914489529226")),(mk_real_int (num_of_string "2947903435531652302048824"));(* 24, 24 *) (mk_real_int (num_of_string "3190806295090043587472275")),(mk_real_int (num_of_string "3148717815525864571540200"));(* 24, 24 *) (mk_real_int (num_of_string "2165066039022822385314720")),(mk_real_int (num_of_string "1789667065043536098768516"));(* 24, 24 *) (mk_real_int (num_of_string "3544217078579404889403632")),(mk_real_int (num_of_string "1719620726900459949129408"));(* 24, 24 *) (mk_real_int (num_of_string "4975798555669974494894850")),(mk_real_int (num_of_string "2551548992139386318128712"));(* 24, 24 *) (mk_real_int (num_of_string "4951911396640711363819200")),(mk_real_int (num_of_string "4152301302036776635279512"));(* 24, 24 *) (mk_real_int (num_of_string "4491288491237901426394272")),(mk_real_int (num_of_string "2631946141755769234538912"));(* 24, 24 *) (mk_real_int (num_of_string "4545423334511168657484519")),(mk_real_int (num_of_string "4658046691233522803154367"));(* 24, 24 *) (mk_real_int (num_of_string "1733986131733180992015552")),(mk_real_int (num_of_string "3196517734402713660976740"));(* 24, 24 *) (mk_real_int (num_of_string "1775683452707085499156708")),(mk_real_int (num_of_string "3769688709694824344064702"));(* 24, 24 *) (mk_real_int (num_of_string "2294479279699999024839990")),(mk_real_int (num_of_string "3181581126568371503429460"));(* 24, 24 *) (mk_real_int (num_of_string "3573282858174024051474126")),(mk_real_int (num_of_string "3501097823648368976284480"));(* 24, 24 *) (mk_real_int (num_of_string "2354093297820505361664576")),(mk_real_int (num_of_string "4232218889714137372079568"));(* 24, 24 *) (mk_real_int (num_of_string "3975432450689183427293688")),(mk_real_int (num_of_string "3921741171241369802325363"));(* 24, 24 *) (mk_real_int (num_of_string "1341687685141100305801884")),(mk_real_int (num_of_string "2342899857768319895491602"));(* 24, 24 *) (mk_real_int (num_of_string "5014715224374016128677892")),(mk_real_int (num_of_string "2247479330116216087862256"));(* 24, 24 *) (mk_real_int (num_of_string "4794805770310877151740544")),(mk_real_int (num_of_string "5178712808077970014705680"));(* 24, 24 *) (mk_real_int (num_of_string "3823551335893024713717030")),(mk_real_int (num_of_string "4712396855488429978936416"));(* 24, 24 *) (mk_real_int (num_of_string "3339610543556138013709239")),(mk_real_int (num_of_string "3460379483248658185637832"));(* 24, 24 *) (mk_real_int (num_of_string "3126824052272971648254198")),(mk_real_int (num_of_string "2846310197206151567879160"));(* 24, 24 *) (mk_real_int (num_of_string "4976921386354566978877020")),(mk_real_int (num_of_string "2724190822978858891102368"));(* 24, 24 *) (mk_real_int (num_of_string "3868322959227720786444990")),(mk_real_int (num_of_string "2834794460530573874620493"));(* 24, 24 *) (mk_real_int (num_of_string "3806186870542498909262796")),(mk_real_int (num_of_string "1854167532325130096813592"));(* 24, 24 *) (mk_real_int (num_of_string "2997218349017407762690494")),(mk_real_int (num_of_string "3220146512606107750810221"));(* 24, 24 *) (mk_real_int (num_of_string "2869447584142557930608694")),(mk_real_int (num_of_string "3214537679931159027199842"));(* 24, 24 *) (mk_real_int (num_of_string "3505531594393264927150280")),(mk_real_int (num_of_string "2099747502179401595487360"));(* 24, 24 *) (mk_real_int (num_of_string "2074023604438605921828216")),(mk_real_int (num_of_string "3288064708456254087507120"));(* 24, 24 *) (mk_real_int (num_of_string "4605341127827031387475758")),(mk_real_int (num_of_string "3384978417362671963599150"));(* 24, 24 *) (mk_real_int (num_of_string "6803202158448157216759396")),(mk_real_int (num_of_string "3683855794725939882005840"));(* 24, 24 *) (mk_real_int (num_of_string "3130199101998336679219125")),(mk_real_int (num_of_string "3016851995941040303113438"));(* 24, 24 *) (mk_real_int (num_of_string "5144222638325352643882421")),(mk_real_int (num_of_string "3369920402699560088045667"));(* 24, 24 *) (mk_real_int (num_of_string "2712346394363038291983435")),(mk_real_int (num_of_string "6395925068788489550630592"));(* 24, 24 *) (mk_real_int (num_of_string "3467376684543582559552020")),(mk_real_int (num_of_string "2128208492552431074493350"));(* 24, 24 *) (mk_real_int (num_of_string "5415148644331751251891200")),(mk_real_int (num_of_string "3866363135314615395252855"));(* 24, 24 *) (mk_real_int (num_of_string "2836846938576599847191508")),(mk_real_int (num_of_string "3278429679524453150052480"));(* 24, 24 *) (mk_real_int (num_of_string "4272198351534367270595040")),(mk_real_int (num_of_string "2134330313063458420434960"));(* 24, 24 *) (mk_real_int (num_of_string "1890763478558507244852000")),(mk_real_int (num_of_string "3403905409782445999494000"));(* 24, 24 *) (mk_real_int (num_of_string "4012348283800700333242928")),(mk_real_int (num_of_string "1686153041853083191675248"));(* 24, 24 *) (mk_real_int (num_of_string "3684897676763580922882164")),(mk_real_int (num_of_string "2596997901617597919418810"));(* 24, 24 *) (mk_real_int (num_of_string "2432860488289906006544240")),(mk_real_int (num_of_string "2199097551229251540807072"));(* 24, 24 *) (mk_real_int (num_of_string "2219207324705634782651496")),(mk_real_int (num_of_string "3280134834524258413318560"));(* 24, 24 *) (mk_real_int (num_of_string "4281812610452363858331460")),(mk_real_int (num_of_string "2291827655326688504622284"));(* 24, 24 *) (mk_real_int (num_of_string "2311301167426197506501838")),(mk_real_int (num_of_string "3428254847018049828189408"));(* 24, 24 *) (mk_real_int (num_of_string "4106396327950841384544000")),(mk_real_int (num_of_string "1519855021732655091405600"));(* 24, 24 *) (mk_real_int (num_of_string "4574436248720511522670200")),(mk_real_int (num_of_string "3752666330976676195227630"));(* 24, 24 *) (mk_real_int (num_of_string "6060088460967430248859520")),(mk_real_int (num_of_string "2751183273513060318370880"));(* 24, 24 *) (mk_real_int (num_of_string "5936652774963812405375000")),(mk_real_int (num_of_string "1934307048092504193486300"));(* 24, 24 *) (mk_real_int (num_of_string "2966282780968813768296120")),(mk_real_int (num_of_string "4554330723537599733523816"));(* 24, 24 *) (mk_real_int (num_of_string "4066034642911280512435200")),(mk_real_int (num_of_string "3182582607381827923268520"));(* 24, 24 *) (mk_real_int (num_of_string "3563570100200781569985000")),(mk_real_int (num_of_string "4251922123057236845557620"));(* 24, 24 *) (mk_real_int (num_of_string "4165625658592128432921520")),(mk_real_int (num_of_string "3181323461627667361337648"));(* 24, 24 *) (mk_real_int (num_of_string "3490972371192151507271296")),(mk_real_int (num_of_string "3514970213076356218280460"));(* 24, 24 *) (mk_real_int (num_of_string "2852044109793304237709040")),(mk_real_int (num_of_string "2671977203273762349360360"));(* 24, 24 *) (mk_real_int (num_of_string "3915334439659948711843346")),(mk_real_int (num_of_string "5956897025974722583452150"));(* 24, 24 *) (mk_real_int (num_of_string "4313158434068389266139968")),(mk_real_int (num_of_string "2653805462158669944348384"));(* 24, 24 *) (mk_real_int (num_of_string "2754336596780610471421350")),(mk_real_int (num_of_string "2772300369425996824797690"));(* 24, 24 *) (mk_real_int (num_of_string "4905620798835419319401472")),(mk_real_int (num_of_string "2857332698454377916692480"));(* 24, 24 *) (mk_real_int (num_of_string "2532069156823170882274560")),(mk_real_int (num_of_string "1379564442693197304033504"));(* 24, 24 *) (mk_real_int (num_of_string "4947971569340910625685632")),(mk_real_int (num_of_string "5178758091567081706175334"));(* 24, 24 *) (mk_real_int (num_of_string "4668751225864626203800981")),(mk_real_int (num_of_string "3545390797653050605725000"));(* 24, 24 *) (mk_real_int (num_of_string "3515238210071573298488000")),(mk_real_int (num_of_string "3917771747980800228227709"));(* 24, 24 *) (mk_real_int (num_of_string "3974260796924945298942540")),(mk_real_int (num_of_string "2675047863492134070751200"));(* 24, 24 *) (mk_real_int (num_of_string "2701212383544604571433000")),(mk_real_int (num_of_string "2551105824986287552061950"));(* 24, 24 *) (mk_real_int (num_of_string "3353097986611672900839282")),(mk_real_int (num_of_string "2242020391999505588419795"));(* 24, 24 *) (mk_real_int (num_of_string "3064771028334398285413588")),(mk_real_int (num_of_string "3572998177272916435359680"));(* 24, 24 *) (mk_real_int (num_of_string "3090781458062850904665939")),(mk_real_int (num_of_string "6946037168952791997500820"));(* 24, 24 *) (mk_real_int (num_of_string "3572522167547604940352036")),(mk_real_int (num_of_string "4400456166147890886739344"));(* 24, 24 *) (mk_real_int (num_of_string "2564895552099059502603720")),(mk_real_int (num_of_string "2363657410040192228447616"));(* 24, 24 *) (mk_real_int (num_of_string "2435295010923027695176050")),(mk_real_int (num_of_string "2658879763930517002525440"));(* 24, 24 *) (mk_real_int (num_of_string "3731986736282107605541376")),(mk_real_int (num_of_string "3643683257180774788982430"));(* 24, 24 *) (mk_real_int (num_of_string "1934859277092254036885040")),(mk_real_int (num_of_string "6830307149849087499930362"));(* 24, 24 *) (mk_real_int (num_of_string "2530144512121302228105430")),(mk_real_int (num_of_string "3337809587674217377166110"));(* 24, 24 *) (mk_real_int (num_of_string "2390987582050522765833864")),(mk_real_int (num_of_string "2128950082119999634279368"));(* 24, 24 *) (mk_real_int (num_of_string "1801877367436339432206240")),(mk_real_int (num_of_string "3123699200575804967141250"));(* 24, 24 *) (mk_real_int (num_of_string "5466441655140846553078560")),(mk_real_int (num_of_string "1788617313593277909631344"));(* 24, 24 *) (mk_real_int (num_of_string "2465087542211644211511870")),(mk_real_int (num_of_string "2615739313857496973491611"));(* 24, 24 *) (mk_real_int (num_of_string "2953522074969932903774700")),(mk_real_int (num_of_string "4096063849122441554820000"));(* 24, 24 *) (mk_real_int (num_of_string "2007145459097460241272600")),(mk_real_int (num_of_string "4162541767252076451830580"));(* 24, 24 *) (mk_real_int (num_of_string "5430888892585395778267350")),(mk_real_int (num_of_string "4324249558881214572718640"));(* 24, 24 *) (mk_real_int (num_of_string "2775835639167828427319250")),(mk_real_int (num_of_string "4725201745868974509328920"));(* 24, 24 *) (mk_real_int (num_of_string "7224027538697433660753492")),(mk_real_int (num_of_string "2517044131010981715888873"));(* 24, 24 *) (mk_real_int (num_of_string "3913987572409201599526896")),(mk_real_int (num_of_string "1391277403447889718473664"));(* 24, 24 *) (mk_real_int (num_of_string "5032898552919662361402720")),(mk_real_int (num_of_string "3325621987638880759116000"));(* 24, 24 *) (mk_real_int (num_of_string "1996616622819610598163480")),(mk_real_int (num_of_string "1621650060828807618513320"));(* 24, 24 *) (mk_real_int (num_of_string "2651027604103717379135625")),(mk_real_int (num_of_string "3629240399070136919377600"));(* 24, 24 *) (mk_real_int (num_of_string "1784725554808080858425358")),(mk_real_int (num_of_string "1980789758144140075714355"));(* 24, 24 *) (mk_real_int (num_of_string "3118705154749481776946467")),(mk_real_int (num_of_string "1941656404556598716235952"));(* 24, 24 *) (mk_real_int (num_of_string "1949365175707955575849752")),(mk_real_int (num_of_string "3773979470855669631283728"));(* 24, 24 *) (mk_real_int (num_of_string "3385073197846140097479000")),(mk_real_int (num_of_string "2165264053676023708262400"));(* 24, 24 *) (mk_real_int (num_of_string "4594810229909494948983084")),(mk_real_int (num_of_string "4203883076566568653677356"));(* 24, 24 *) (mk_real_int (num_of_string "3563798935728332031302304")),(mk_real_int (num_of_string "3606496318464501687608184"));(* 24, 24 *) (mk_real_int (num_of_string "2143597071358191602034000")),(mk_real_int (num_of_string "6979131304638593073200664"));(* 24, 24 *) (mk_real_int (num_of_string "3136507206814624511714340")),(mk_real_int (num_of_string "1824724051223353798551110"));(* 24, 24 *) (mk_real_int (num_of_string "3239893738685445736594392")),(mk_real_int (num_of_string "5105726599313502896104800"));(* 24, 24 *) (mk_real_int (num_of_string "3821515089222452989796352")),(mk_real_int (num_of_string "5119791707001722420914272"));(* 24, 24 *) (mk_real_int (num_of_string "2604459407217387601892400")),(mk_real_int (num_of_string "4097463128007138284215128"));(* 24, 24 *) (mk_real_int (num_of_string "3071435380663325913873240")),(mk_real_int (num_of_string "1633083507453268989198080"));(* 24, 24 *) (mk_real_int (num_of_string "2408028822735649773240240")),(mk_real_int (num_of_string "3396584272586694967004430"));(* 24, 24 *) (mk_real_int (num_of_string "2202383548466759613276480")),(mk_real_int (num_of_string "3374626785030251185529600"));(* 24, 24 *) (mk_real_int (num_of_string "2291900767057913983502700")),(mk_real_int (num_of_string "3442712976445079361024000"));(* 24, 24 *) (mk_real_int (num_of_string "2608094721815726160536415")),(mk_real_int (num_of_string "2997568460560585187836800"));(* 24, 24 *) (mk_real_int (num_of_string "2800746642903629405947928")),(mk_real_int (num_of_string "5235065231624031939922500"));(* 24, 24 *) (mk_real_int (num_of_string "2692342941442729015836360")),(mk_real_int (num_of_string "2957783908800553055719920"));(* 24, 24 *) (mk_real_int (num_of_string "2746818435345676723357480")),(mk_real_int (num_of_string "2003512507767009856539648"));(* 24, 24 *) (mk_real_int (num_of_string "3426450617089113528226680")),(mk_real_int (num_of_string "3582442592579029895321232"));(* 24, 24 *) (mk_real_int (num_of_string "2733962034727774885573904")),(mk_real_int (num_of_string "2109663267100626537887454"));(* 24, 24 *) (mk_real_int (num_of_string "2506066568383585307554944")),(mk_real_int (num_of_string "2709498947876642778115980"));(* 24, 24 *) (mk_real_int (num_of_string "3676438365709094379647110")),(mk_real_int (num_of_string "4102234807436038571659984"));(* 24, 24 *) (mk_real_int (num_of_string "3629991651433849053255420")),(mk_real_int (num_of_string "2315754679208992475234196"));(* 24, 24 *) (mk_real_int (num_of_string "3302943359998991947853035")),(mk_real_int (num_of_string "3972495889006573344354120"));(* 24, 24 *) (mk_real_int (num_of_string "4447984875021248628557184")),(mk_real_int (num_of_string "2256959201265717332757100"));(* 24, 24 *) (mk_real_int (num_of_string "3547915725957155260591000")),(mk_real_int (num_of_string "4637693516349085976448504"));(* 24, 24 *) (mk_real_int (num_of_string "4885058929587272510872080")),(mk_real_int (num_of_string "2205807580605573714657048"));(* 24, 24 *) (mk_real_int (num_of_string "3046909431989449693524424")),(mk_real_int (num_of_string "3205859539520201431193088"));(* 24, 24 *) (mk_real_int (num_of_string "2736270340853886359125425")),(mk_real_int (num_of_string "2332015519572934570163550"));(* 24, 24 *) (mk_real_int (num_of_string "4691776065946488723080820")),(mk_real_int (num_of_string "1852736962489000947106560"));(* 24, 24 *) (mk_real_int (num_of_string "3679791072298926681351060")),(mk_real_int (num_of_string "2751063087953713328195330"));(* 24, 24 *) (mk_real_int (num_of_string "2715598523559576544607280")),(mk_real_int (num_of_string "2946284354139227479719100"));(* 24, 24 *) (mk_real_int (num_of_string "1738629892567591488552000")),(mk_real_int (num_of_string "2585159385992904535904880"));(* 24, 24 *) (mk_real_int (num_of_string "1869199790605948431590400")),(mk_real_int (num_of_string "3691728317294819359467510"));(* 24, 24 *) (mk_real_int (num_of_string "3634789546718695326719572")),(mk_real_int (num_of_string "3158183305756271031892660"));(* 24, 24 *) (mk_real_int (num_of_string "1642203387466459407921858")),(mk_real_int (num_of_string "3198646640837524650170380"));(* 24, 24 *) (mk_real_int (num_of_string "2060683897536347475002100")),(mk_real_int (num_of_string "2304489361448693626937460"));(* 24, 24 *) (mk_real_int (num_of_string "1888771412055086518326822")),(mk_real_int (num_of_string "3050080131747772156432504"));(* 24, 24 *) (mk_real_int (num_of_string "3897131325410782390735516")),(mk_real_int (num_of_string "2475879597754217034629276"));(* 24, 24 *) (mk_real_int (num_of_string "5305078937997422088047802")),(mk_real_int (num_of_string "4235329055092652560927026"));(* 24, 24 *) (mk_real_int (num_of_string "4054974424515820472761500")),(mk_real_int (num_of_string "2232712380835275783080640"));(* 24, 24 *) (mk_real_int (num_of_string "1559172550876776052986000")),(mk_real_int (num_of_string "4749112378847404364589551"));(* 24, 24 *) (mk_real_int (num_of_string "1790552615612520240102972")),(mk_real_int (num_of_string "4024826997451796555365962"));(* 24, 24 *) (mk_real_int (num_of_string "1676409283820706142879080")),(mk_real_int (num_of_string "1428505169975437471362180"));(* 24, 24 *) (mk_real_int (num_of_string "2798048096194626424919160")),(mk_real_int (num_of_string "2275387859016418545818784"));(* 24, 24 *) (mk_real_int (num_of_string "4594577339109149706833430")),(mk_real_int (num_of_string "6286523530824598250451744"));(* 24, 24 *) (mk_real_int (num_of_string "2047856158161286275988976")),(mk_real_int (num_of_string "1372491351879079050281520"));(* 24, 24 *) (mk_real_int (num_of_string "2272701095435371557326292")),(mk_real_int (num_of_string "1891801762948279865902500"));(* 24, 24 *) (mk_real_int (num_of_string "2088080990826796594296000")),(mk_real_int (num_of_string "2412734355552828425497920"));(* 24, 24 *) (mk_real_int (num_of_string "2619499284958867049663364")),(mk_real_int (num_of_string "1998132074159230881089136"));(* 24, 24 *) (mk_real_int (num_of_string "2202606038617879807824696")),(mk_real_int (num_of_string "2875129356329763033213440"));(* 24, 24 *) (mk_real_int (num_of_string "3751025457380535643995268")),(mk_real_int (num_of_string "2280620215677807588215340"));(* 24, 24 *) (mk_real_int (num_of_string "3233260288564450132408962")),(mk_real_int (num_of_string "2359331533321344355832289"));(* 24, 24 *) (mk_real_int (num_of_string "2531580631019444262671802")),(mk_real_int (num_of_string "3720280731378367896886140"));(* 24, 24 *) (mk_real_int (num_of_string "4515613893682141131342720")),(mk_real_int (num_of_string "3190438265675381006404140"));(* 24, 24 *) (mk_real_int (num_of_string "3627734701866734970700224")),(mk_real_int (num_of_string "3887561562117260064176370"));(* 24, 24 *) (mk_real_int (num_of_string "1868530721231120446447830")),(mk_real_int (num_of_string "4643932256947155223048600"));(* 24, 24 *) (mk_real_int (num_of_string "3390651387660244658744718")),(mk_real_int (num_of_string "2423394689663933959290912"));(* 24, 24 *) (mk_real_int (num_of_string "3740820130346018563688040")),(mk_real_int (num_of_string "4053452359105539233073240"));(* 24, 24 *) (mk_real_int (num_of_string "4853202037717698240386454")),(mk_real_int (num_of_string "3430849713991211965605570"));(* 24, 24 *) (mk_real_int (num_of_string "3893553184531953148538328")),(mk_real_int (num_of_string "3764437614700390789885920"));(* 24, 24 *) (mk_real_int (num_of_string "1673387528743561482115498")),(mk_real_int (num_of_string "3462548317193169742921560"));(* 24, 24 *) (mk_real_int (num_of_string "2445619810118824006215114")),(mk_real_int (num_of_string "4201561844549768760127638"));(* 24, 24 *) (mk_real_int (num_of_string "2970425520237593922545664")),(mk_real_int (num_of_string "4606446474553038802420608"));(* 24, 24 *) (mk_real_int (num_of_string "1735666746975335174900700")),(mk_real_int (num_of_string "2641374039165613557831774"));(* 24, 24 *) (mk_real_int (num_of_string "3026272042331624287411860")),(mk_real_int (num_of_string "5135990406166036535818980"));(* 24, 24 *) (mk_real_int (num_of_string "3033974370556022474575575")),(mk_real_int (num_of_string "5886116732637780706944360"));(* 24, 24 *) (mk_real_int (num_of_string "2122881279758065543333960")),(mk_real_int (num_of_string "5856429326067594260110204"));(* 24, 24 *) (mk_real_int (num_of_string "1865635784241405149280300")),(mk_real_int (num_of_string "3887764710200833500348216"));(* 24, 24 *) (mk_real_int (num_of_string "2108194656482894539381185")),(mk_real_int (num_of_string "3024041889238453856991960"));(* 24, 24 *) (mk_real_int (num_of_string "3614379219401015912378130")),(mk_real_int (num_of_string "3961540502990981756890408"));(* 24, 24 *) (mk_real_int (num_of_string "3626568755889394780597552")),(mk_real_int (num_of_string "3949093464761248758416250"));(* 24, 24 *) (mk_real_int (num_of_string "2478390039500999658674640")),(mk_real_int (num_of_string "2357727475594350036125760"));(* 24, 24 *) (mk_real_int (num_of_string "3218672705940127925553000")),(mk_real_int (num_of_string "3860417960803560852809835"));(* 24, 24 *) (mk_real_int (num_of_string "2926026705208510992755130")),(mk_real_int (num_of_string "3457560015663836867346870"));(* 24, 24 *) (mk_real_int (num_of_string "4301205337630414230219720")),(mk_real_int (num_of_string "3327174911143264219419120"));(* 24, 24 *) (mk_real_int (num_of_string "5236192768636957219783760")),(mk_real_int (num_of_string "3010787240856020340604000"));(* 24, 24 *) (mk_real_int (num_of_string "1885120553390417918308160")),(mk_real_int (num_of_string "2550787151042836114498242"));(* 24, 24 *) (mk_real_int (num_of_string "4564186474411868104657152")),(mk_real_int (num_of_string "3503049259248220121164872"));(* 24, 24 *) (mk_real_int (num_of_string "2382581727931448516403000")),(mk_real_int (num_of_string "2020977086719348777938048"));(* 24, 24 *) (mk_real_int (num_of_string "5915103627656378999460600")),(mk_real_int (num_of_string "2806961531095398725277300"));(* 24, 24 *) (mk_real_int (num_of_string "6525402984399687376816920")),(mk_real_int (num_of_string "3654347645423727413567076"));(* 24, 24 *) (mk_real_int (num_of_string "3144703351003709087150280")),(mk_real_int (num_of_string "2344972170860439370339830"));(* 24, 24 *) (mk_real_int (num_of_string "4812615225330234437627883")),(mk_real_int (num_of_string "2917506997467823601328327"));(* 24, 24 *) (mk_real_int (num_of_string "2422397336199441953574144")),(mk_real_int (num_of_string "1626921422339370742417176"));(* 24, 24 *) (mk_real_int (num_of_string "4026702186345047070786320")),(mk_real_int (num_of_string "5446345995936324423495408"));(* 24, 24 *) (mk_real_int (num_of_string "2667697884083368771777450")),(mk_real_int (num_of_string "3587707657123288925963410"));(* 24, 24 *) (mk_real_int (num_of_string "1713319013545625898372582")),(mk_real_int (num_of_string "4281602692194806127168123"));(* 24, 24 *) (mk_real_int (num_of_string "2566290672711815464685234")),(mk_real_int (num_of_string "4628801339116994466175544"));(* 24, 24 *) (mk_real_int (num_of_string "6313355811154487015372998")),(mk_real_int (num_of_string "2922341255059162599784400"));(* 24, 24 *) (mk_real_int (num_of_string "2530659684551571264740328")),(mk_real_int (num_of_string "3164617218010839733177932"));(* 24, 24 *) (mk_real_int (num_of_string "4042288306038832178218596")),(mk_real_int (num_of_string "5196659467674369792664896"));(* 24, 24 *) (mk_real_int (num_of_string "2905240152738828329469000")),(mk_real_int (num_of_string "3567822275310227822653290"));(* 24, 24 *) (mk_real_int (num_of_string "2658391705322346278149176")),(mk_real_int (num_of_string "4222727720477057686033622"));(* 24, 24 *) (mk_real_int (num_of_string "4057774310915319912206418")),(mk_real_int (num_of_string "2187291211741654447444416"));(* 24, 24 *) (mk_real_int (num_of_string "3930351646133475447251760")),(mk_real_int (num_of_string "3397285376426760702847260"));(* 24, 24 *) (mk_real_int (num_of_string "3201396531435436973595075")),(mk_real_int (num_of_string "2100340161704413703517282"));(* 24, 24 *) (mk_real_int (num_of_string "3011607028932051530386644")),(mk_real_int (num_of_string "3171372046227668310177024"));(* 24, 24 *) (mk_real_int (num_of_string "4861531423666840288544350")),(mk_real_int (num_of_string "3968601892175320931232870"));(* 24, 24 *) (mk_real_int (num_of_string "5976530243446371838091786")),(mk_real_int (num_of_string "2808401559914129988625552"));(* 24, 24 *) (mk_real_int (num_of_string "3037856780650139925913800")),(mk_real_int (num_of_string "3546633262761072290008720"));(* 24, 24 *) (mk_real_int (num_of_string "4028754100841399278950480")),(mk_real_int (num_of_string "2178473160142295476944890"));(* 24, 24 *) (mk_real_int (num_of_string "2164356730123805226531194")),(mk_real_int (num_of_string "1652312733001554033643850"));(* 24, 24 *) (mk_real_int (num_of_string "2009603752212967818177152")),(mk_real_int (num_of_string "2600702467280483393597000"));(* 24, 24 *) (mk_real_int (num_of_string "1858816711761863447881149")),(mk_real_int (num_of_string "2749083947469050460183000"));(* 24, 24 *) (mk_real_int (num_of_string "3175485625695642428431328")),(mk_real_int (num_of_string "2590737316460059431503440"));(* 24, 24 *) (mk_real_int (num_of_string "2438800342808051710289830")),(mk_real_int (num_of_string "2666832628731302546500237"));(* 24, 24 *) (mk_real_int (num_of_string "2080571740698196759640075")),(mk_real_int (num_of_string "2767797394930381955155560"));(* 24, 24 *) (mk_real_int (num_of_string "3704382715070758242608112")),(mk_real_int (num_of_string "3502369547219471185004100"));(* 24, 24 *) (mk_real_int (num_of_string "4281763083713158732855790")),(mk_real_int (num_of_string "2355216972911223538561416"));(* 24, 24 *) (mk_real_int (num_of_string "2045511049684050795484400")),(mk_real_int (num_of_string "3155340364118630887209520"));(* 24, 24 *) (mk_real_int (num_of_string "3182511375935478640171026")),(mk_real_int (num_of_string "4312006461736963272548314"));(* 24, 24 *) (mk_real_int (num_of_string "2148860809769156082522768")),(mk_real_int (num_of_string "3257592881455191116306700"));(* 24, 24 *) (mk_real_int (num_of_string "2785059991856346651564855")),(mk_real_int (num_of_string "3007341915428953703268080"));(* 24, 24 *) (mk_real_int (num_of_string "1379222760901918934531520")),(mk_real_int (num_of_string "3171893051246254647846828"));(* 24, 24 *) (mk_real_int (num_of_string "2979687229721903911094280")),(mk_real_int (num_of_string "2905103357150715743589000"));(* 24, 24 *) (mk_real_int (num_of_string "3336388672393549661802375")),(mk_real_int (num_of_string "3090434288166512562368000"));(* 24, 24 *) (mk_real_int (num_of_string "1649812639647223418619720")),(mk_real_int (num_of_string "2143524694423637251043037"));(* 24, 24 *) (mk_real_int (num_of_string "2876560826294331046927452")),(mk_real_int (num_of_string "2308523552466662120534433"));(* 24, 24 *) (mk_real_int (num_of_string "1191353355500004310833765")),(mk_real_int (num_of_string "3027315373760144230235920"));(* 24, 24 *) (mk_real_int (num_of_string "3065396965211547677640492")),(mk_real_int (num_of_string "2238004268352446753204736"));(* 24, 24 *) (mk_real_int (num_of_string "2900450928959289384637062")),(mk_real_int (num_of_string "2426441008472380165747728"));(* 24, 24 *) (mk_real_int (num_of_string "7407449026844002623338880")),(mk_real_int (num_of_string "2127205942262211941701824"));(* 24, 24 *) (mk_real_int (num_of_string "3703893579446695382275000")),(mk_real_int (num_of_string "4196802839229934715355912"));(* 24, 24 *) (mk_real_int (num_of_string "2805981628673246534701344")),(mk_real_int (num_of_string "1799081531155596443082390"));(* 24, 24 *) (mk_real_int (num_of_string "5843010404023574503255225")),(mk_real_int (num_of_string "2671322857651759770345915"));(* 24, 24 *) (mk_real_int (num_of_string "4346850707619923500298178")),(mk_real_int (num_of_string "3122188681319209915024388"));(* 24, 24 *) (mk_real_int (num_of_string "2024152162990612466884864")),(mk_real_int (num_of_string "2418033742705899520797075"));(* 24, 24 *) (mk_real_int (num_of_string "1807637311253118257884062")),(mk_real_int (num_of_string "5943159214533643591925820"));(* 24, 24 *) (mk_real_int (num_of_string "3295485786398298873540538")),(mk_real_int (num_of_string "3757220501449259702343600"));(* 24, 24 *) (mk_real_int (num_of_string "3025261572744227085898496")),(mk_real_int (num_of_string "2922157373168618505237681"));(* 24, 24 *) (mk_real_int (num_of_string "3014109359934091224419250")),(mk_real_int (num_of_string "4029119529490816972725472"));(* 24, 24 *) (mk_real_int (num_of_string "4811548061896982993541888")),(mk_real_int (num_of_string "2667701466191417956564160"));(* 24, 24 *) (mk_real_int (num_of_string "3011072478149365414884036")),(mk_real_int (num_of_string "1520441543283610140078304"));(* 24, 24 *) (mk_real_int (num_of_string "1649578174700693390933040")),(mk_real_int (num_of_string "2429639618240216205072040"));(* 24, 24 *) (mk_real_int (num_of_string "4701088509797559635203170")),(mk_real_int (num_of_string "2425638879806675329379520"));(* 24, 24 *) (mk_real_int (num_of_string "3971840775495799053319056")),(mk_real_int (num_of_string "3599060596825347856564880"));(* 24, 24 *) (mk_real_int (num_of_string "3518100912653238833339400")),(mk_real_int (num_of_string "2895088949394456720074325"));(* 24, 24 *) (mk_real_int (num_of_string "2628521626683933352604166")),(mk_real_int (num_of_string "2770783135022712680713700"));(* 24, 24 *) (mk_real_int (num_of_string "4215223219124847774213432")),(mk_real_int (num_of_string "3960512374456688617792200"));(* 24, 24 *) (mk_real_int (num_of_string "3905001987762139435894500")),(mk_real_int (num_of_string "4192062835824792632903667"));(* 24, 24 *) (mk_real_int (num_of_string "1890337315212195368182140")),(mk_real_int (num_of_string "5278460138594444052424800"));(* 24, 24 *) (mk_real_int (num_of_string "3231688089598373660453600")),(mk_real_int (num_of_string "4403389468863279172421920"));(* 24, 24 *) (mk_real_int (num_of_string "3472817674451349037450780")),(mk_real_int (num_of_string "3078501757646961566683140"));(* 24, 24 *) (mk_real_int (num_of_string "3463845899848181254603152")),(mk_real_int (num_of_string "4929093222946325442909237"));(* 24, 24 *) (mk_real_int (num_of_string "6519892936247810746253900")),(mk_real_int (num_of_string "1807076487940984433594220"));(* 24, 24 *) (mk_real_int (num_of_string "1798002285636790737466688")),(mk_real_int (num_of_string "4910354225449337382747840"));(* 24, 24 *) (mk_real_int (num_of_string "1428826417781212539327168")),(mk_real_int (num_of_string "2442479009528224611646272"));(* 24, 24 *) (mk_real_int (num_of_string "5319906065106604303679165")),(mk_real_int (num_of_string "4698923998881181913686480"));(* 24, 24 *) (mk_real_int (num_of_string "2985721174205796690930084")),(mk_real_int (num_of_string "4524873621275492702153266"));(* 24, 24 *) (mk_real_int (num_of_string "4365811451604304886108463")),(mk_real_int (num_of_string "1260814541858732426406152"));(* 24, 24 *) (mk_real_int (num_of_string "4020081761352521578433104")),(mk_real_int (num_of_string "3166061522253896060283951"));(* 24, 24 *) (mk_real_int (num_of_string "2010861224094962044902096")),(mk_real_int (num_of_string "3838485308854525397125380"));(* 24, 24 *) (mk_real_int (num_of_string "5229805454779102249565576")),(mk_real_int (num_of_string "2154268145376919020470400"));(* 24, 24 *) (mk_real_int (num_of_string "2764782868627789208875944")),(mk_real_int (num_of_string "3138250561369443620084409"));(* 24, 24 *) (mk_real_int (num_of_string "2141731053643805648027760")),(mk_real_int (num_of_string "1632127961024157699712891"));(* 24, 24 *) (mk_real_int (num_of_string "3421094153011726233918528")),(mk_real_int (num_of_string "3121854631753091190354724"));(* 24, 24 *) (mk_real_int (num_of_string "2415059991508058990869200")),(mk_real_int (num_of_string "4192772906070206883710973"));(* 24, 24 *) (mk_real_int (num_of_string "3996546100300498874099580")),(mk_real_int (num_of_string "5205644676672384546184236"));(* 24, 24 *) (mk_real_int (num_of_string "2666899766142088222106240")),(mk_real_int (num_of_string "1632306583078964612553456"));(* 24, 24 *) (mk_real_int (num_of_string "6459242516486355883355640")),(mk_real_int (num_of_string "6276571472060575884175185"));(* 24, 24 *) (mk_real_int (num_of_string "1687509026574079923829170")),(mk_real_int (num_of_string "1923112223134436728420547"));(* 24, 24 *) (mk_real_int (num_of_string "3163262230947776642934139")),(mk_real_int (num_of_string "2543292912878765499873120"));(* 24, 24 *) (mk_real_int (num_of_string "4367276553131859544455168")),(mk_real_int (num_of_string "2496547690526169727662288"));(* 24, 24 *) (mk_real_int (num_of_string "2243242227009436100754125")),(mk_real_int (num_of_string "2902244669695548440427570"));(* 24, 24 *) (mk_real_int (num_of_string "4677512265762453505082070")),(mk_real_int (num_of_string "4880050733488480288001199"));(* 24, 24 *) (mk_real_int (num_of_string "4375760510193640653585216")),(mk_real_int (num_of_string "5679350324832156615321444"));(* 24, 24 *) (mk_real_int (num_of_string "2315362924942702171459052")),(mk_real_int (num_of_string "3739207362885741670111972"));(* 24, 24 *) (mk_real_int (num_of_string "2177231599956901628136870")),(mk_real_int (num_of_string "6064774723780636074099840"));(* 24, 24 *) (mk_real_int (num_of_string "3905594325851099814691200")),(mk_real_int (num_of_string "4949707425592787431332864"));(* 24, 24 *) (mk_real_int (num_of_string "4263740091149568585664080")),(mk_real_int (num_of_string "3022586806214784348753696"));(* 24, 24 *) (mk_real_int (num_of_string "2380714731233323097564850")),(mk_real_int (num_of_string "2185945903415184001502400"));(* 24, 24 *) (mk_real_int (num_of_string "4202529072886683880119706")),(mk_real_int (num_of_string "3284397421662576595245396"));(* 24, 24 *) (mk_real_int (num_of_string "1934025869291452072744608")),(mk_real_int (num_of_string "2965657588650504380660724"));(* 24, 24 *) (mk_real_int (num_of_string "2390748531039718716619890")),(mk_real_int (num_of_string "2821104894083978774737280"));(* 24, 24 *) (mk_real_int (num_of_string "2697050299548414218174958")),(mk_real_int (num_of_string "2671222165732893376555380"));(* 24, 24 *) (mk_real_int (num_of_string "3126161655981094216282902")),(mk_real_int (num_of_string "6973365209997825543172500"));(* 24, 24 *) (mk_real_int (num_of_string "2666926172336290770536380")),(mk_real_int (num_of_string "4834759765829616590402862"));(* 24, 24 *) (mk_real_int (num_of_string "2100947464183064996301360")),(mk_real_int (num_of_string "2394828487191656264297472"));(* 24, 24 *) (mk_real_int (num_of_string "2079826568717690819582720")),(mk_real_int (num_of_string "5297237044842862783242656"));(* 24, 24 *) (mk_real_int (num_of_string "3836154727066700872993904")),(mk_real_int (num_of_string "3706471411229943249872460"));(* 24, 24 *) (mk_real_int (num_of_string "5325350621021905854685900")),(mk_real_int (num_of_string "3141209172193411438368263"));(* 24, 24 *) (mk_real_int (num_of_string "4535053885364909492266974")),(mk_real_int (num_of_string "3611640051656072980748568"));(* 24, 24 *) (mk_real_int (num_of_string "3888336370488591939239980")),(mk_real_int (num_of_string "2089775516962169584447848"));(* 24, 24 *) (mk_real_int (num_of_string "3577550486188165157031840")),(mk_real_int (num_of_string "3943759759250199237584400"));(* 24, 24 *) (mk_real_int (num_of_string "4305849788505839642123784")),(mk_real_int (num_of_string "2055652000553913508311296"));(* 24, 24 *) (mk_real_int (num_of_string "4865502935017285132872735")),(mk_real_int (num_of_string "2428499045404614177525600"));(* 24, 24 *) (mk_real_int (num_of_string "1971317612533365792311040")),(mk_real_int (num_of_string "3193210724635212199652241"));(* 24, 24 *) (mk_real_int (num_of_string "1764488215405595470985040")),(mk_real_int (num_of_string "1826383701772883242024546"));(* 24, 24 *) (mk_real_int (num_of_string "2658713677549105034040000")),(mk_real_int (num_of_string "4463341131810757742736036"));(* 24, 24 *) (mk_real_int (num_of_string "2443168311218583662921328")),(mk_real_int (num_of_string "2245767819105194944232520"));(* 24, 24 *) (mk_real_int (num_of_string "2360749817479949727397720")),(mk_real_int (num_of_string "4698220348763252846799880"));(* 24, 24 *) (mk_real_int (num_of_string "1652999324424845565340785")),(mk_real_int (num_of_string "2008939231284937541199456"));(* 24, 24 *) (mk_real_int (num_of_string "2033564618823410903856192")),(mk_real_int (num_of_string "3372930820294031227527088"));(* 24, 24 *) (mk_real_int (num_of_string "2917069087635731282730300")),(mk_real_int (num_of_string "4244070806362014955710378"));(* 24, 24 *) (mk_real_int (num_of_string "3613429680971503238575251")),(mk_real_int (num_of_string "3893844138422640879834280"));(* 24, 24 *) (mk_real_int (num_of_string "2874075866860907186409540")),(mk_real_int (num_of_string "4705582682344355049640941"));(* 24, 24 *) (mk_real_int (num_of_string "2273888711090849073746694")),(mk_real_int (num_of_string "3924054181765156318423500"));(* 24, 24 *) (mk_real_int (num_of_string "2817834190824438230936400")),(mk_real_int (num_of_string "2204531181670965099956685"));(* 24, 24 *) (mk_real_int (num_of_string "2735289648231979117428765")),(mk_real_int (num_of_string "2288778068627138959002000"));(* 24, 24 *) (mk_real_int (num_of_string "3178456944443197491838000")),(mk_real_int (num_of_string "3745293109002685629188720"));(* 24, 24 *) (mk_real_int (num_of_string "4079392936412486461744800")),(mk_real_int (num_of_string "3992941547256682847420880"));(* 24, 24 *) (mk_real_int (num_of_string "4885812873662085989091000")),(mk_real_int (num_of_string "5397362548999139173774080"));(* 24, 24 *) (mk_real_int (num_of_string "2258145203451770220023100")),(mk_real_int (num_of_string "4291031872388514266195104"));(* 24, 24 *) (mk_real_int (num_of_string "5436440159669669069304000")),(mk_real_int (num_of_string "3523213160714169416462997"));(* 24, 24 *) (mk_real_int (num_of_string "3375201219791203812680388")),(mk_real_int (num_of_string "2187254970040432587317000"));(* 24, 24 *) (mk_real_int (num_of_string "2353860220383035041373055")),(mk_real_int (num_of_string "4896520136927559425413930"));(* 24, 24 *) (mk_real_int (num_of_string "2552863451559708220629158")),(mk_real_int (num_of_string "3143596093627464364940295"));(* 24, 24 *) (mk_real_int (num_of_string "2758512397510815559967808")),(mk_real_int (num_of_string "4859094233483659062596232"));(* 24, 24 *) (mk_real_int (num_of_string "5214950997916200229144800")),(mk_real_int (num_of_string "4104101067057021830132176"));(* 24, 24 *) (mk_real_int (num_of_string "2036497145970722836279704")),(mk_real_int (num_of_string "5206535027548412824214940"));(* 24, 24 *) (mk_real_int (num_of_string "2339859801385345879476000")),(mk_real_int (num_of_string "1878231441943334830535775"));(* 24, 24 *) (mk_real_int (num_of_string "2750676552087875353648832")),(mk_real_int (num_of_string "3183926732101107577250400"));(* 24, 24 *) (mk_real_int (num_of_string "4096137656275559159373248")),(mk_real_int (num_of_string "2036957940931695831086271"));(* 24, 24 *) (mk_real_int (num_of_string "2243017424363424509081120")),(mk_real_int (num_of_string "2250814318972608210950700"));(* 24, 24 *) (mk_real_int (num_of_string "3633254407265459251144588")),(mk_real_int (num_of_string "1876053551069278734975636"));(* 24, 24 *) (mk_real_int (num_of_string "2969317672686392492952864")),(mk_real_int (num_of_string "3997218538187092313865000"));(* 24, 24 *) (mk_real_int (num_of_string "4175896879680397218950400")),(mk_real_int (num_of_string "4504177595952207436140130"));(* 24, 24 *) (mk_real_int (num_of_string "2611932920231236676249955")),(mk_real_int (num_of_string "1719236338818801480217344"));(* 24, 24 *) (mk_real_int (num_of_string "2164909344906238563788640")),(mk_real_int (num_of_string "3681230074585725081859450"));(* 24, 24 *) (mk_real_int (num_of_string "2478542091668439822778950")),(mk_real_int (num_of_string "3978905051266610413580520"));(* 24, 24 *) (mk_real_int (num_of_string "3298843114016562174718656")),(mk_real_int (num_of_string "2802682320722699664557328"));(* 24, 24 *) (mk_real_int (num_of_string "5348671022568563591120256")),(mk_real_int (num_of_string "3681914645001209140307520"));(* 24, 24 *) (mk_real_int (num_of_string "1380234575353858286292498")),(mk_real_int (num_of_string "5637730544575066062197316"));(* 24, 24 *) (mk_real_int (num_of_string "2192262994114541017517952")),(mk_real_int (num_of_string "3277362809327049417746625"));(* 24, 24 *) (mk_real_int (num_of_string "3253786765955399407202100")),(mk_real_int (num_of_string "2837964342169794422149704"));(* 24, 24 *) (mk_real_int (num_of_string "3665438318965926387415608")),(mk_real_int (num_of_string "2302432169638013772478662"));(* 24, 24 *) (mk_real_int (num_of_string "2404860979692714948178238")),(mk_real_int (num_of_string "5912021963984470680499440"));(* 24, 24 *) (mk_real_int (num_of_string "4575711617443909547190872")),(mk_real_int (num_of_string "2928912702806271355164900"));(* 24, 24 *) (mk_real_int (num_of_string "1623900572914388421159456")),(mk_real_int (num_of_string "2714759629814468533897236"));(* 24, 24 *) (mk_real_int (num_of_string "2875610801697635613336984")),(mk_real_int (num_of_string "1837668339386052318899124"));(* 24, 24 *) (mk_real_int (num_of_string "3086502980677008129632955")),(mk_real_int (num_of_string "2829289935400052976475416"));(* 24, 24 *) (mk_real_int (num_of_string "4276548216949915461314142")),(mk_real_int (num_of_string "3754591819515012116144889"));(* 24, 24 *) (mk_real_int (num_of_string "2423370537562076500111038")),(mk_real_int (num_of_string "2899462605337441487717632"));(* 24, 24 *) (mk_real_int (num_of_string "3170664866702341194612794")),(mk_real_int (num_of_string "3566895356076005263489850"));(* 24, 24 *) (mk_real_int (num_of_string "3478847963719978039525192")),(mk_real_int (num_of_string "1854982467250982490976800"));(* 24, 24 *) (mk_real_int (num_of_string "2106512437488401248502690")),(mk_real_int (num_of_string "2661443305967140215239808"));(* 24, 24 *) (mk_real_int (num_of_string "2265527424983410137122208")),(mk_real_int (num_of_string "2180574814273162253122176"));(* 24, 24 *) (mk_real_int (num_of_string "3553100931280228466446260")),(mk_real_int (num_of_string "4191090088282233805338960"));(* 24, 24 *) (mk_real_int (num_of_string "3469945860479219840283180")),(mk_real_int (num_of_string "2151836328420176769095424"));(* 24, 24 *) (mk_real_int (num_of_string "5129447473921080656206080")),(mk_real_int (num_of_string "2331256968813334641805200"));(* 24, 24 *) (mk_real_int (num_of_string "2787088344030347329422164")),(mk_real_int (num_of_string "3890527928039325037999500"));(* 24, 24 *) (mk_real_int (num_of_string "5835494826267547490169120")),(mk_real_int (num_of_string "6616305967285876291574076"));(* 24, 24 *) (mk_real_int (num_of_string "4745825359454452270640580")),(mk_real_int (num_of_string "4636425885004701145717632"));(* 24, 24 *) (mk_real_int (num_of_string "2971408921128205779645165")),(mk_real_int (num_of_string "2988624839195305858086189"));(* 24, 24 *) (mk_real_int (num_of_string "3138188269635169019555904")),(mk_real_int (num_of_string "5597524548157172059854394"));(* 24, 24 *) (mk_real_int (num_of_string "3949751964390881547459063")),(mk_real_int (num_of_string "1980388452444045444437472"));(* 24, 24 *) (mk_real_int (num_of_string "1545631918442141910192176")),(mk_real_int (num_of_string "6792710308770333193372830"));(* 24, 24 *) (mk_real_int (num_of_string "2948815060007869983005768")),(mk_real_int (num_of_string "3483757325881289709884600"));(* 24, 24 *) (mk_real_int (num_of_string "7156916113355496092508750")),(mk_real_int (num_of_string "2996015837959530626036550"));(* 24, 24 *) (mk_real_int (num_of_string "2633069512650175327145200")),(mk_real_int (num_of_string "4431508930605363536722112"));(* 24, 24 *) (mk_real_int (num_of_string "3952363215269745696956800")),(mk_real_int (num_of_string "1907435895363707600842992"));(* 24, 24 *) (mk_real_int (num_of_string "3247912747275279510681824")),(mk_real_int (num_of_string "3278107922026658100639168"));(* 24, 24 *) (mk_real_int (num_of_string "6113820100524616389161120")),(mk_real_int (num_of_string "3757243955769481723943904"));(* 24, 24 *) (mk_real_int (num_of_string "3720607984463669914296630")),(mk_real_int (num_of_string "3692632293212261351117760"));(* 24, 24 *) (mk_real_int (num_of_string "3748869610826980004801436")),(mk_real_int (num_of_string "3166129504786817080274400"));(* 24, 24 *) (mk_real_int (num_of_string "3978864825874341989708144")),(mk_real_int (num_of_string "2917771410908374594382946"));(* 24, 24 *) (mk_real_int (num_of_string "2108920981200346048396320")),(mk_real_int (num_of_string "2856094821944851692214800"));(* 24, 24 *) (mk_real_int (num_of_string "3027758583067266375396960")),(mk_real_int (num_of_string "2339807066741573986719344"));(* 24, 24 *) (mk_real_int (num_of_string "2960304443717620807429005")),(mk_real_int (num_of_string "5709472524981270175844238"));(* 24, 24 *) (mk_real_int (num_of_string "1736592508195890840402656")),(mk_real_int (num_of_string "4733823858798612363524640"));(* 24, 24 *) (mk_real_int (num_of_string "3651014867890056752116080")),(mk_real_int (num_of_string "2336145996071195999425800"));(* 24, 24 *) (mk_real_int (num_of_string "2010697251103226943085180")),(mk_real_int (num_of_string "4207049022585141991667520"));(* 24, 24 *) (mk_real_int (num_of_string "1675758959800525689709620")),(mk_real_int (num_of_string "3535467501781993920773865"));(* 24, 24 *) (mk_real_int (num_of_string "3709020422542967078722200")),(mk_real_int (num_of_string "2874672380829338043540416"));(* 24, 24 *) (mk_real_int (num_of_string "2441459866156342594383000")),(mk_real_int (num_of_string "3022287556360458071572880"));(* 24, 24 *) (mk_real_int (num_of_string "4042742046820611849852813")),(mk_real_int (num_of_string "3022257715423923080509200"));(* 24, 24 *) (mk_real_int (num_of_string "3736479962580079314642900")),(mk_real_int (num_of_string "1773372900996612367598820"));(* 24, 24 *) (mk_real_int (num_of_string "3209020740197913519620964")),(mk_real_int (num_of_string "4197251716960041774040047"));(* 24, 24 *) (mk_real_int (num_of_string "3245093023925168164790880")),(mk_real_int (num_of_string "3781046912262487353315060"));(* 24, 24 *) (mk_real_int (num_of_string "4388864610962604827465236")),(mk_real_int (num_of_string "2238303777920595342792960"));(* 24, 24 *) (mk_real_int (num_of_string "4091366740216034564249328")),(mk_real_int (num_of_string "3227770278463830361262500"));(* 24, 24 *) (mk_real_int (num_of_string "3265097577786284452073112")),(mk_real_int (num_of_string "4228090225754337921657952"));(* 24, 24 *) (mk_real_int (num_of_string "3324969226869596617340348")),(mk_real_int (num_of_string "6036134641487984730781227"));(* 24, 24 *) (mk_real_int (num_of_string "3546168808297821873345864")),(mk_real_int (num_of_string "3370832045373977797778172"));(* 24, 24 *) (mk_real_int (num_of_string "4434040357351707780932000")),(mk_real_int (num_of_string "2812500448521181382784848"));(* 24, 24 *) (mk_real_int (num_of_string "2838034568798545493385000")),(mk_real_int (num_of_string "3745970426747710415973195"));(* 24, 24 *) (mk_real_int (num_of_string "4317625074930199784764600")),(mk_real_int (num_of_string "5988227902754687996125055"));(* 24, 24 *) (mk_real_int (num_of_string "3690585093281250715958160")),(mk_real_int (num_of_string "3043474610355426658979848"));(* 24, 24 *) (mk_real_int (num_of_string "5022620011946793313430672")),(mk_real_int (num_of_string "2088045814513950362014230"));(* 24, 24 *) (mk_real_int (num_of_string "3604758041405035976957600")),(mk_real_int (num_of_string "6950229436092558307545768"));(* 24, 24 *) (mk_real_int (num_of_string "3686269376301116585152736")),(mk_real_int (num_of_string "3230039786730905173549300"));(* 24, 24 *) (mk_real_int (num_of_string "3259949237302708436672160")),(mk_real_int (num_of_string "4320684199962535726074600"));(* 24, 24 *) (mk_real_int (num_of_string "2431468769937990762316884")),(mk_real_int (num_of_string "3661490753059484833606349"));(* 24, 24 *) (mk_real_int (num_of_string "3764015737305526406092896")),(mk_real_int (num_of_string "3537457307740137397922254"));(* 24, 24 *) (mk_real_int (num_of_string "4022759105652016905725242")),(mk_real_int (num_of_string "3113115006162744189377095"));(* 24, 24 *) (mk_real_int (num_of_string "3305382982588033545522636")),(mk_real_int (num_of_string "5403156422084203141636464"));(* 24, 24 *) (mk_real_int (num_of_string "3490795071230359265933094")),(mk_real_int (num_of_string "4648629736409543249219838"));(* 24, 24 *) (mk_real_int (num_of_string "4805114977717781375306680")),(mk_real_int (num_of_string "3120558578353297652872560"));(* 24, 24 *) (mk_real_int (num_of_string "3131515502850949359360594")),(mk_real_int (num_of_string "2192395663709144508255894"));(* 24, 24 *) (mk_real_int (num_of_string "2172487367325029181470890")),(mk_real_int (num_of_string "4875059458720272796560225"));(* 24, 24 *) (mk_real_int (num_of_string "2762354368765540944533880")),(mk_real_int (num_of_string "2900691952539911813343372"));(* 24, 24 *) (mk_real_int (num_of_string "2944603409799463342571520")),(mk_real_int (num_of_string "3073925764886803032519840"));(* 24, 24 *) (mk_real_int (num_of_string "4019727923606109475010958")),(mk_real_int (num_of_string "2984398872262055462494477"));(* 24, 24 *) (mk_real_int (num_of_string "3983277295427479818535536")),(mk_real_int (num_of_string "2021099250304136559710960"));(* 24, 24 *) (mk_real_int (num_of_string "3038306519939718291025788")),(mk_real_int (num_of_string "3109063807869415455086080"));(* 24, 24 *) (mk_real_int (num_of_string "3676251721183286510507840")),(mk_real_int (num_of_string "4703955550799097972681540"));(* 24, 24 *) (mk_real_int (num_of_string "2162943630402011301069960")),(mk_real_int (num_of_string "3285803927091928145083696"));(* 24, 24 *) (mk_real_int (num_of_string "3370192608950678210708988")),(mk_real_int (num_of_string "4884811314457597322339760"));(* 24, 24 *) (mk_real_int (num_of_string "3248649890916604120066440")),(mk_real_int (num_of_string "2861902202098549035270900"));(* 24, 24 *) (mk_real_int (num_of_string "3372834112175540618809840")),(mk_real_int (num_of_string "2563638804491408551068696"));(* 24, 24 *) (mk_real_int (num_of_string "2942212642004272126649376")),(mk_real_int (num_of_string "2902764292381866424061280"));(* 24, 24 *) (mk_real_int (num_of_string "2808628583243974957548144")),(mk_real_int (num_of_string "3040807813787578515090390"));(* 24, 24 *) (mk_real_int (num_of_string "2251841685050575688188864")),(mk_real_int (num_of_string "1904900528278992698760150"));(* 24, 24 *) (mk_real_int (num_of_string "5672865885193253316245824")),(mk_real_int (num_of_string "4089012423044369425963488"));(* 24, 24 *) (mk_real_int (num_of_string "1644054406161754086076955")),(mk_real_int (num_of_string "2698711155535467564161652"));(* 24, 24 *) (mk_real_int (num_of_string "1741058562240392628825250")),(mk_real_int (num_of_string "4132036228599560706844356"));(* 24, 24 *) (mk_real_int (num_of_string "3461363842118891156821628")),(mk_real_int (num_of_string "2733784076007615749144320"));(* 24, 24 *) (mk_real_int (num_of_string "2188933460101117565711040")),(mk_real_int (num_of_string "5040790855390880275924539"));(* 24, 24 *) (mk_real_int (num_of_string "3045055732952917100212890")),(mk_real_int (num_of_string "2550412930616009789014230"));(* 24, 24 *) (mk_real_int (num_of_string "3633391982921077946876190")),(mk_real_int (num_of_string "3151184976138836160550488"));(* 24, 24 *) (mk_real_int (num_of_string "3844298869323738424336724")),(mk_real_int (num_of_string "2049849754371883226407050"));(* 24, 24 *) (mk_real_int (num_of_string "3134691256834270451756121")),(mk_real_int (num_of_string "2692782485727581073822996"));(* 24, 24 *) (mk_real_int (num_of_string "4683786431469441758742800")),(mk_real_int (num_of_string "2216431204560387605365388"));(* 24, 24 *) (mk_real_int (num_of_string "1940069527678291356559872")),(mk_real_int (num_of_string "4387341911084707093011744"));(* 24, 24 *) (mk_real_int (num_of_string "2883668468781784956249432")),(mk_real_int (num_of_string "2971153066457187003946662"));(* 24, 24 *) (mk_real_int (num_of_string "2390285393972899165913600")),(mk_real_int (num_of_string "2892404223118619371138548"));(* 24, 24 *) (mk_real_int (num_of_string "2442749401358879684828229")),(mk_real_int (num_of_string "2481656678009898533022400"));(* 24, 24 *) (mk_real_int (num_of_string "3806240636616518540009500")),(mk_real_int (num_of_string "5040737852268912182365320"));(* 24, 24 *) (mk_real_int (num_of_string "3988804554208061401698936")),(mk_real_int (num_of_string "3221176438171479037810392"));(* 24, 24 *) (mk_real_int (num_of_string "3370268985701687170774140")),(mk_real_int (num_of_string "1185573170159663989345950"));(* 24, 24 *) (mk_real_int (num_of_string "3316420816441171425374840")),(mk_real_int (num_of_string "2652695252324338199705208"));(* 24, 24 *) (mk_real_int (num_of_string "3779796114539958969680280")),(mk_real_int (num_of_string "4337928600492365981913660"));(* 24, 24 *) (mk_real_int (num_of_string "4191559885721475568829952")),(mk_real_int (num_of_string "4107475549347258245091000"));(* 24, 24 *) (mk_real_int (num_of_string "2458049149716540150695760")),(mk_real_int (num_of_string "5234529485460594912695144"));(* 24, 24 *) (mk_real_int (num_of_string "1859094431882653763667240")),(mk_real_int (num_of_string "5824650274206897042788704"));(* 24, 24 *) (mk_real_int (num_of_string "2629624333948316763541395")),(mk_real_int (num_of_string "1944155964976901417010176"));(* 24, 24 *) (mk_real_int (num_of_string "4356941563711504993306900")),(mk_real_int (num_of_string "4758801800757332677552500"));(* 24, 24 *) (mk_real_int (num_of_string "2691648212198111546546220")),(mk_real_int (num_of_string "3440047602853354364169462"));(* 24, 24 *) (mk_real_int (num_of_string "3422153473131695078636100")),(mk_real_int (num_of_string "2262095063216187492589930"));(* 24, 24 *) (mk_real_int (num_of_string "2521676538180305189467056")),(mk_real_int (num_of_string "1234871169346058627005920"));(* 24, 24 *) (mk_real_int (num_of_string "3424824953475753634075360")),(mk_real_int (num_of_string "1865185993344010572739215"));(* 24, 24 *) (mk_real_int (num_of_string "2480009801217898715994540")),(mk_real_int (num_of_string "4269160290408644298588696"));(* 24, 24 *) (mk_real_int (num_of_string "3832372723197884225638324")),(mk_real_int (num_of_string "2516383644688498990130739"));(* 24, 24 *) (mk_real_int (num_of_string "5096895227786131244667000")),(mk_real_int (num_of_string "4751866955977617164098800"));(* 24, 24 *) (mk_real_int (num_of_string "2354995569751904488037398")),(mk_real_int (num_of_string "1864395673309687616393256"));(* 24, 24 *) (mk_real_int (num_of_string "4361708421884937163728448")),(mk_real_int (num_of_string "5321263274223395615948270"));(* 24, 24 *) (mk_real_int (num_of_string "3770241216032645670082760")),(mk_real_int (num_of_string "2509579123783101638972895"));(* 24, 24 *) (mk_real_int (num_of_string "4822068426927348395675520")),(mk_real_int (num_of_string "5940724329976471906937664"));(* 24, 24 *) (mk_real_int (num_of_string "2814662470142057608918048")),(mk_real_int (num_of_string "2609492952401052020406180"));(* 24, 24 *) (mk_real_int (num_of_string "5216024001225128661945760")),(mk_real_int (num_of_string "2841716015244338391405400"));(* 24, 24 *) (mk_real_int (num_of_string "3918270597306092645222592")),(mk_real_int (num_of_string "3480856133599794130206795"));(* 24, 24 *) (mk_real_int (num_of_string "3457876659846088215698994")),(mk_real_int (num_of_string "1589200961720500363361600"));(* 24, 24 *) (mk_real_int (num_of_string "2627989496682030264741830")),(mk_real_int (num_of_string "2525533348753835519192768"));(* 24, 24 *) (mk_real_int (num_of_string "2736645587340329112268500")),(mk_real_int (num_of_string "3045291596257757784421680"));(* 24, 24 *) (mk_real_int (num_of_string "2236644592585489593427624")),(mk_real_int (num_of_string "4199738755526481942387938"));(* 24, 24 *) (mk_real_int (num_of_string "2637405467599900952085504")),(mk_real_int (num_of_string "4512763710738522344088369"));(* 24, 24 *) (mk_real_int (num_of_string "3701751255730610611990536")),(mk_real_int (num_of_string "3266958962741850687158484"));(* 24, 24 *) (mk_real_int (num_of_string "2483521795963911716335224")),(mk_real_int (num_of_string "2407481677718593641936540"));(* 24, 24 *) (mk_real_int (num_of_string "3018412573662049796297619")),(mk_real_int (num_of_string "3536680196463410800933920"));(* 24, 24 *) (mk_real_int (num_of_string "2290126604428601248857738")),(mk_real_int (num_of_string "2492650216302678541782400"));(* 24, 24 *) (mk_real_int (num_of_string "3665731940375308133530716")),(mk_real_int (num_of_string "3161803539134853550900878"));(* 24, 24 *) (mk_real_int (num_of_string "2214179826636063440319480")),(mk_real_int (num_of_string "3817905654750086590860384"));(* 24, 24 *) (mk_real_int (num_of_string "1895873086074655187177100")),(mk_real_int (num_of_string "5592284623307547334961750"));(* 24, 24 *) (mk_real_int (num_of_string "3240852388016706225128755")),(mk_real_int (num_of_string "2201098956992486610970500"));(* 24, 24 *) (mk_real_int (num_of_string "2301595831816796097986880")),(mk_real_int (num_of_string "3730902591794562940979250"));(* 24, 24 *) (mk_real_int (num_of_string "5602948854544410602238462")),(mk_real_int (num_of_string "2945515984573044296479716"));(* 24, 24 *) (mk_real_int (num_of_string "3323713967312345107957377")),(mk_real_int (num_of_string "3146329210656240116740680"));(* 24, 24 *) (mk_real_int (num_of_string "3112648059165517352079532")),(mk_real_int (num_of_string "1848794444424010109463120"));(* 24, 24 *) (mk_real_int (num_of_string "2755322124081717462470076")),(mk_real_int (num_of_string "2408990848894048024863432"));(* 24, 24 *) (mk_real_int (num_of_string "2757020838395289348299916")),(mk_real_int (num_of_string "3036120054765644566554336"));(* 24, 24 *) (mk_real_int (num_of_string "1794282890922509278372200")),(mk_real_int (num_of_string "3236071813359841618731108"));(* 24, 24 *) (mk_real_int (num_of_string "3351206283629589357575625")),(mk_real_int (num_of_string "2268587798765717360624979"));(* 24, 24 *) (mk_real_int (num_of_string "2470051050174866243420156")),(mk_real_int (num_of_string "3206449671651100482334705"));(* 24, 24 *) (mk_real_int (num_of_string "3510202544555606514793500")),(mk_real_int (num_of_string "1547569031171232382921920"));(* 24, 24 *) (mk_real_int (num_of_string "3214337249907352965199602")),(mk_real_int (num_of_string "2149800819123782166745338"));(* 24, 24 *) (mk_real_int (num_of_string "4303233958425560131936527")),(mk_real_int (num_of_string "3019367868060442587877125"));(* 24, 24 *) (mk_real_int (num_of_string "2655319450364318518469444")),(mk_real_int (num_of_string "3806382904046840691549360"));(* 24, 24 *) (mk_real_int (num_of_string "4944836816092137703320264")),(mk_real_int (num_of_string "2819237965671427936451272"));(* 24, 24 *) (mk_real_int (num_of_string "1936882171988931068295264")),(mk_real_int (num_of_string "2306279870390203335802460"));(* 24, 24 *) (mk_real_int (num_of_string "2727789002819013958029630")),(mk_real_int (num_of_string "3502188757432913739884928"));(* 24, 24 *) (mk_real_int (num_of_string "2176864822703095479852482")),(mk_real_int (num_of_string "4965364989515719320083552"));(* 24, 24 *) (mk_real_int (num_of_string "5341132315796427937522470")),(mk_real_int (num_of_string "2913650664076008713248722"));(* 24, 24 *) (mk_real_int (num_of_string "3611725134929953488893000")),(mk_real_int (num_of_string "5202269428051954148686848"));(* 24, 24 *) (mk_real_int (num_of_string "5608700980127645569459807")),(mk_real_int (num_of_string "3727963641699022077072000"));(* 24, 24 *) (mk_real_int (num_of_string "2659106999205355757723080")),(mk_real_int (num_of_string "2991658517211527227991802"));(* 24, 24 *) (mk_real_int (num_of_string "2564708296146024263098500")),(mk_real_int (num_of_string "3524698733696466497872440"));(* 24, 24 *) (mk_real_int (num_of_string "5608241077510186623615406")),(mk_real_int (num_of_string "3863681735787329988520704"));(* 24, 24 *) (mk_real_int (num_of_string "5241525140825051938420055")),(mk_real_int (num_of_string "3246430986830744440315245"));(* 24, 24 *) (mk_real_int (num_of_string "3695831862530009720289984")),(mk_real_int (num_of_string "4682481744424862643649824"));(* 24, 24 *) (mk_real_int (num_of_string "1867932463971518007954800")),(mk_real_int (num_of_string "2116053413450871355164778"));(* 24, 24 *) (mk_real_int (num_of_string "2503263156536046855213888")),(mk_real_int (num_of_string "1860205109177358473750400"));(* 24, 24 *) (mk_real_int (num_of_string "3566887930501440915276900")),(mk_real_int (num_of_string "3119411074966404346699200"));(* 24, 24 *) (mk_real_int (num_of_string "3181219767618511684265760")),(mk_real_int (num_of_string "3519000882230365751967822"));(* 24, 24 *) (mk_real_int (num_of_string "1614871783756904729202168")),(mk_real_int (num_of_string "4445952826915852408628472"));(* 24, 24 *) (mk_real_int (num_of_string "2250056523819933285111744")),(mk_real_int (num_of_string "3249474790642784808154800"));(* 24, 24 *) (mk_real_int (num_of_string "4903556798118027093228600")),(mk_real_int (num_of_string "3110716740640195981598304"));(* 24, 24 *) (mk_real_int (num_of_string "4369371863471751902034009")),(mk_real_int (num_of_string "3762281027615271724286252"));(* 24, 24 *) (mk_real_int (num_of_string "1628071391357853844082366")),(mk_real_int (num_of_string "1886833276682065568885730"));(* 24, 24 *) (mk_real_int (num_of_string "2297372302548316465111682")),(mk_real_int (num_of_string "2552580571534286707784160"));(* 24, 24 *) (mk_real_int (num_of_string "4850014610271571666467516")),(mk_real_int (num_of_string "1597237298318378533271566"));(* 24, 24 *) (mk_real_int (num_of_string "4972291580229559672453848")),(mk_real_int (num_of_string "3536758601701187778638912"));(* 24, 24 *) (mk_real_int (num_of_string "3223697308727816459747712")),(mk_real_int (num_of_string "2066175160990542721473934"));(* 24, 24 *) (mk_real_int (num_of_string "1926747179135464118355108")),(mk_real_int (num_of_string "4807256530769740020161394"));(* 24, 24 *) (mk_real_int (num_of_string "4990823657572809255164100")),(mk_real_int (num_of_string "6365013144248103690824160"));(* 24, 24 *) (mk_real_int (num_of_string "3494296499874226327209365")),(mk_real_int (num_of_string "1889528218736537377781472"));(* 24, 24 *) (mk_real_int (num_of_string "4119531947388198344886660")),(mk_real_int (num_of_string "5631221184158669894381664"));(* 24, 24 *) (mk_real_int (num_of_string "5276324990868633828155808")),(mk_real_int (num_of_string "3024009097567566833069928"));(* 24, 24 *) (mk_real_int (num_of_string "3440584656232452265609422")),(mk_real_int (num_of_string "3171800142498697274826296"));(* 24, 24 *) (mk_real_int (num_of_string "2084956409352596606590512")),(mk_real_int (num_of_string "2155399387412000511896712"));(* 24, 24 *) (mk_real_int (num_of_string "1150918348693958324992656")),(mk_real_int (num_of_string "2974047148052004115648620"));(* 24, 24 *) (mk_real_int (num_of_string "5877596951506738318094883")),(mk_real_int (num_of_string "2004659160298866322934032"));(* 24, 24 *) (mk_real_int (num_of_string "2085081025936173120881280")),(mk_real_int (num_of_string "4256797579887852104656452"));(* 24, 24 *) (mk_real_int (num_of_string "2532988651290696826110660")),(mk_real_int (num_of_string "5839911686514219140473680"));(* 24, 24 *) (mk_real_int (num_of_string "3653532172822230240217600")),(mk_real_int (num_of_string "1909287915386385750385554"));(* 24, 24 *) (mk_real_int (num_of_string "3178121555473303086276948")),(mk_real_int (num_of_string "4953683839206976728767406"));(* 24, 24 *) (mk_real_int (num_of_string "2630114165742423484703400")),(mk_real_int (num_of_string "3107675010779355622573056"));(* 24, 24 *) (mk_real_int (num_of_string "4129167077212755796631328")),(mk_real_int (num_of_string "3556194949263240314961199"));(* 24, 24 *) (mk_real_int (num_of_string "1645183843027905440997660")),(mk_real_int (num_of_string "3478659530950478466466560"));(* 24, 24 *) (mk_real_int (num_of_string "2847521404427215513544064")),(mk_real_int (num_of_string "2293227872915395653019938"));(* 24, 24 *) (mk_real_int (num_of_string "4184075516104036111790160")),(mk_real_int (num_of_string "3827745060945879546144414"));(* 24, 24 *) (mk_real_int (num_of_string "5952789213090057326180400")),(mk_real_int (num_of_string "3469585495788977115877617"));(* 24, 24 *) (mk_real_int (num_of_string "3697382820702727461808674")),(mk_real_int (num_of_string "4496689087322095391856690"));(* 24, 24 *) (mk_real_int (num_of_string "3634511866845385766512580")),(mk_real_int (num_of_string "1798391954218632571351080"));(* 24, 24 *) (mk_real_int (num_of_string "1420635797229043442563560")),(mk_real_int (num_of_string "2938362848581987293022500"));(* 24, 24 *) (mk_real_int (num_of_string "3264210037319698314967925")),(mk_real_int (num_of_string "3993074441368154416295340"));(* 24, 24 *) (mk_real_int (num_of_string "2688963665404272897502197")),(mk_real_int (num_of_string "4207271144237165477486208"));(* 24, 24 *) (mk_real_int (num_of_string "3187754371986498977796966")),(mk_real_int (num_of_string "3483499838114526235775784"));(* 24, 24 *) (mk_real_int (num_of_string "4345149025834465402178618")),(mk_real_int (num_of_string "4732907567341784536261710"));(* 24, 24 *) (mk_real_int (num_of_string "4302780553244126599059216")),(mk_real_int (num_of_string "3327974227550752516265760"));(* 24, 24 *) (mk_real_int (num_of_string "2480872370051357527092925")),(mk_real_int (num_of_string "3590349469952819635412955"));(* 24, 24 *) (mk_real_int (num_of_string "4964391156333560892916000")),(mk_real_int (num_of_string "3192042701665393482479760"));(* 24, 24 *) (mk_real_int (num_of_string "3121284595348577967705612")),(mk_real_int (num_of_string "3953432402070988402932240"));(* 24, 24 *) (mk_real_int (num_of_string "1637487069795379453799000")),(mk_real_int (num_of_string "2034540331916956075027000"));(* 24, 24 *) (mk_real_int (num_of_string "2478311046899474389558800")),(mk_real_int (num_of_string "3245781975060315402462960"));(* 24, 24 *) (mk_real_int (num_of_string "2442209792753146007827440")),(mk_real_int (num_of_string "2966608639142357185475100"));(* 24, 24 *) (mk_real_int (num_of_string "6706019554075664843810400")),(mk_real_int (num_of_string "4663334530328018819812440"));(* 24, 24 *) (mk_real_int (num_of_string "3259964108441741745974544")),(mk_real_int (num_of_string "3370315629341470008028500"));(* 24, 24 *) (mk_real_int (num_of_string "2806140656860430163007510")),(mk_real_int (num_of_string "2919954165705914664749330"));(* 24, 24 *) (mk_real_int (num_of_string "4682834487580435676492436")),(mk_real_int (num_of_string "2579158067756238172818000"));(* 24, 24 *) (mk_real_int (num_of_string "2380270436024448448790782")),(mk_real_int (num_of_string "4854066969484715202089640"));(* 24, 24 *) (mk_real_int (num_of_string "2551881811251010373426688")),(mk_real_int (num_of_string "3108433079437999230154541"));(* 24, 24 *) (mk_real_int (num_of_string "2714374318357383772178424")),(mk_real_int (num_of_string "2731410788371849366341624"));(* 24, 24 *) (mk_real_int (num_of_string "2231920621777928173583400")),(mk_real_int (num_of_string "4202853802510828034018190"));(* 24, 24 *) (mk_real_int (num_of_string "3658682908886960285857680")),(mk_real_int (num_of_string "2263891110230682976352400"));(* 24, 24 *) (mk_real_int (num_of_string "2673021566060395941232572")),(mk_real_int (num_of_string "2223307069639802881812000"));(* 24, 24 *) (mk_real_int (num_of_string "3651011897855768760171375")),(mk_real_int (num_of_string "2294685867918222466732590"));(* 24, 24 *) (mk_real_int (num_of_string "3511370031841840959528516")),(mk_real_int (num_of_string "3242950619380072614361712"));(* 24, 24 *) (mk_real_int (num_of_string "2978041989443282952573504")),(mk_real_int (num_of_string "4337026344964206753702336"));(* 24, 24 *) (mk_real_int (num_of_string "1827969192634422008293500")),(mk_real_int (num_of_string "3569824728891433935129088"));(* 24, 24 *) (mk_real_int (num_of_string "5658442032093901065002208")),(mk_real_int (num_of_string "3239285228245969791696560"));(* 24, 24 *) (mk_real_int (num_of_string "2445122036238524696381328")),(mk_real_int (num_of_string "1752567313236555694534650"));(* 24, 24 *) (mk_real_int (num_of_string "4634854541328930158406400")),(mk_real_int (num_of_string "3373325437893915309809302"));(* 24, 24 *) (mk_real_int (num_of_string "3143716774773617193499516")),(mk_real_int (num_of_string "3674557947353065990409080"));(* 24, 24 *) (mk_real_int (num_of_string "2054753445316781088195978")),(mk_real_int (num_of_string "1751154660924626551114250"));(* 24, 24 *) (mk_real_int (num_of_string "4153642424134442960407661")),(mk_real_int (num_of_string "5919673818099539091147840"));(* 24, 24 *) (mk_real_int (num_of_string "2861531543974049689867096")),(mk_real_int (num_of_string "2696776428253698146471934"));(* 24, 24 *) (mk_real_int (num_of_string "4855454089346716230139505")),(mk_real_int (num_of_string "5685274893419215556638800"));(* 24, 24 *) (mk_real_int (num_of_string "3673234804128270216280720")),(mk_real_int (num_of_string "3441993612277086105715980"));(* 24, 24 *) (mk_real_int (num_of_string "4461857281890784590204600")),(mk_real_int (num_of_string "2477346219809981479703370"));(* 24, 24 *) (mk_real_int (num_of_string "3927699294086413032575850")),(mk_real_int (num_of_string "2331506434343814290440540"));(* 24, 24 *) (mk_real_int (num_of_string "2017761628198251307875696")),(mk_real_int (num_of_string "2638394930345032567140144"));(* 24, 24 *) (mk_real_int (num_of_string "2979508010771300437963422")),(mk_real_int (num_of_string "4283856959593876977786096"));(* 24, 24 *) (mk_real_int (num_of_string "6166455341890413080562480")),(mk_real_int (num_of_string "3122494753514819058016775"));(* 24, 24 *) (mk_real_int (num_of_string "2181320700175908750201840")),(mk_real_int (num_of_string "3600989971639653399674520"));(* 24, 24 *) (mk_real_int (num_of_string "2596359177022619513756082")),(mk_real_int (num_of_string "3138774845382018874654930"));(* 24, 24 *) (mk_real_int (num_of_string "4934963635463193755906494")),(mk_real_int (num_of_string "2276208158329438239542569"));(* 24, 24 *) (mk_real_int (num_of_string "3467830656481952260004445")),(mk_real_int (num_of_string "3029249622105646246307520"));(* 24, 24 *) (mk_real_int (num_of_string "2738088336027446828352180")),(mk_real_int (num_of_string "1951244921737135736706060"));(* 24, 24 *) (mk_real_int (num_of_string "2056623393806257562141585")),(mk_real_int (num_of_string "4281156282557585725040544"));(* 24, 24 *) (mk_real_int (num_of_string "1477159917565703194735800")),(mk_real_int (num_of_string "1681451055059772326541925"));(* 24, 24 *) (mk_real_int (num_of_string "4128593795790524783941680")),(mk_real_int (num_of_string "1548303888015218313138700"));(* 24, 24 *) (mk_real_int (num_of_string "3346745965832022223262628")),(mk_real_int (num_of_string "2444230731232107482996004"));(* 24, 24 *) (mk_real_int (num_of_string "3116065609444505717571904")),(mk_real_int (num_of_string "3666724887346125442155136"));(* 24, 24 *) (mk_real_int (num_of_string "4720551012815856513496575")),(mk_real_int (num_of_string "1735960717917516108157440"));(* 24, 24 *) (mk_real_int (num_of_string "2839626124484320575624000")),(mk_real_int (num_of_string "5671265431683361455795984"));(* 24, 24 *) (mk_real_int (num_of_string "2587244548362917119966538")),(mk_real_int (num_of_string "4565956295041404381643622"));(* 24, 24 *) (mk_real_int (num_of_string "3959523966399494125129510")),(mk_real_int (num_of_string "6202131128265812937688206"));(* 24, 24 *) (mk_real_int (num_of_string "2702444905307779008832798")),(mk_real_int (num_of_string "4685504284331908623097050"));(* 24, 24 *) (mk_real_int (num_of_string "3992951262126805818131775")),(mk_real_int (num_of_string "1960688005581452392873208"));(* 24, 24 *) (mk_real_int (num_of_string "2594289781723889092972986")),(mk_real_int (num_of_string "3317699810877781720983680"));(* 24, 24 *) (mk_real_int (num_of_string "3252978063999666521135400")),(mk_real_int (num_of_string "2000731406858133961593348"));(* 24, 24 *) (mk_real_int (num_of_string "4045836001217665907670050")),(mk_real_int (num_of_string "2381478103440811136204664"));(* 24, 24 *) (mk_real_int (num_of_string "2796531057080085769945293")),(mk_real_int (num_of_string "5749668916743868216788744"));(* 24, 24 *) (mk_real_int (num_of_string "4890195926793629600580000")),(mk_real_int (num_of_string "3963616003823920605887040"));(* 24, 24 *) (mk_real_int (num_of_string "2929283474066196042064360")),(mk_real_int (num_of_string "4513301454663127631534080"));(* 24, 24 *) (mk_real_int (num_of_string "4528873117987916629936200")),(mk_real_int (num_of_string "3212401643832141916888500"));(* 24, 24 *) (mk_real_int (num_of_string "4631952590092393815337344")),(mk_real_int (num_of_string "2714703617866549142673000"));(* 24, 24 *) (mk_real_int (num_of_string "4473802790379934473640944")),(mk_real_int (num_of_string "3460233422343005154791604"));(* 24, 24 *) (mk_real_int (num_of_string "4204067424920557108148160")),(mk_real_int (num_of_string "4702496145073303850747298"));(* 24, 24 *) (mk_real_int (num_of_string "3598857725271740641636632")),(mk_real_int (num_of_string "2976280255710714017532246"));(* 24, 24 *) (mk_real_int (num_of_string "4037441040716730744914960")),(mk_real_int (num_of_string "2443066610927734420685568"));(* 24, 24 *) (mk_real_int (num_of_string "2955486909446820734601000")),(mk_real_int (num_of_string "5361828111029821417247844"));(* 24, 24 *) (mk_real_int (num_of_string "3363459689366462710402470")),(mk_real_int (num_of_string "3564359543930647134700104"));(* 24, 24 *) (mk_real_int (num_of_string "5386044208881706199580000")),(mk_real_int (num_of_string "2671113496718970176526856"));(* 24, 24 *) (mk_real_int (num_of_string "2718818348391963415173568")),(mk_real_int (num_of_string "3106188046703253471351315"));(* 24, 24 *) (mk_real_int (num_of_string "5437868019183024213673248")),(mk_real_int (num_of_string "2300835052706981265150375"));(* 24, 24 *) (mk_real_int (num_of_string "5720450450793539815154320")),(mk_real_int (num_of_string "2751767006176621435032084"));(* 24, 24 *) (mk_real_int (num_of_string "7694601444603575866150500")),(mk_real_int (num_of_string "2868067773076146144624972"));(* 24, 24 *) (mk_real_int (num_of_string "3431818575210682219099390")),(mk_real_int (num_of_string "3904908106810073366314872"));(* 24, 24 *) (mk_real_int (num_of_string "3284127251668499789376000")),(mk_real_int (num_of_string "3385707756585382640069224"));(* 24, 24 *) (mk_real_int (num_of_string "2719500727012846183714296")),(mk_real_int (num_of_string "4686774378731542177296120"));(* 24, 24 *) (mk_real_int (num_of_string "3034730227396458322283832")),(mk_real_int (num_of_string "3712038681710629240658688"));(* 24, 24 *) (mk_real_int (num_of_string "4546494397318961536417584")),(mk_real_int (num_of_string "3907625976617325022000753"));(* 24, 24 *) (mk_real_int (num_of_string "2476217058926299755325440")),(mk_real_int (num_of_string "1990708634598351879168280"));(* 24, 24 *) (mk_real_int (num_of_string "3618472797188061879399564")),(mk_real_int (num_of_string "2074426535332438388410812"));(* 24, 24 *) (mk_real_int (num_of_string "2730699327880591581038770")),(mk_real_int (num_of_string "3520238383778503745826720"));(* 24, 24 *) (mk_real_int (num_of_string "3545636300621248047113240")),(mk_real_int (num_of_string "3035651318424981632733984"));(* 24, 24 *) (mk_real_int (num_of_string "3494902110003380883793500")),(mk_real_int (num_of_string "2708690141715156252001950"));(* 24, 24 *) (mk_real_int (num_of_string "1836504937361898578594820")),(mk_real_int (num_of_string "4034304744828169643190595"));(* 24, 24 *) (mk_real_int (num_of_string "2848360644278302317096096")),(mk_real_int (num_of_string "3655367912539289400286448"));(* 24, 24 *) (mk_real_int (num_of_string "3639178957082170275039300")),(mk_real_int (num_of_string "2921402780592750722680440"));(* 24, 24 *) (mk_real_int (num_of_string "2473247481671462767553984")),(mk_real_int (num_of_string "3044889058979910338402886"));(* 24, 24 *) (mk_real_int (num_of_string "5207275558826973585124584")),(mk_real_int (num_of_string "2484289009664793646432700"));(* 24, 24 *) (mk_real_int (num_of_string "2749235025453504762214782")),(mk_real_int (num_of_string "2767252244168037877236340"));(* 24, 24 *) (mk_real_int (num_of_string "4457269760898171809860656")),(mk_real_int (num_of_string "2537589291833892987201546"));(* 24, 24 *) (mk_real_int (num_of_string "4959859216799122796901216")),(mk_real_int (num_of_string "3325865242462439596381008"));(* 24, 24 *) (mk_real_int (num_of_string "4086861150286375786884217")),(mk_real_int (num_of_string "3664782026624849047183680"));(* 24, 24 *) (mk_real_int (num_of_string "5713854534033013226047152")),(mk_real_int (num_of_string "3711870296092911481680672"));(* 24, 24 *) (mk_real_int (num_of_string "3510755697023148728655632")),(mk_real_int (num_of_string "2748656576240710389484780"));(* 24, 24 *) (mk_real_int (num_of_string "3934433601959927763222240")),(mk_real_int (num_of_string "2403610319610875824225866"));(* 24, 24 *) (mk_real_int (num_of_string "3520958017985589451778816")),(mk_real_int (num_of_string "4251641715594108432816512"));(* 24, 24 *) (mk_real_int (num_of_string "5083300849858327757754356")),(mk_real_int (num_of_string "2968714349735339402126694"));(* 24, 24 *) (mk_real_int (num_of_string "2907196912286388754866900")),(mk_real_int (num_of_string "3969262695625523525255004"));(* 24, 24 *) (mk_real_int (num_of_string "3486432531035724611317600")),(mk_real_int (num_of_string "3451735845922941300130911"));(* 24, 24 *) (mk_real_int (num_of_string "2347658906076336405736170")),(mk_real_int (num_of_string "2668831071342872694620940"));(* 24, 24 *) (mk_real_int (num_of_string "5899649289890134801954512")),(mk_real_int (num_of_string "2085857302208791903149540"));(* 24, 24 *) (mk_real_int (num_of_string "4507195836964730665314600")),(mk_real_int (num_of_string "3223814800494932100223500"));(* 24, 24 *) (mk_real_int (num_of_string "3969048322980490158406855")),(mk_real_int (num_of_string "2847005566732199931224375"));(* 24, 24 *) (mk_real_int (num_of_string "3539596983984564240840480")),(mk_real_int (num_of_string "3574919188864211215187718"));(* 24, 24 *) (mk_real_int (num_of_string "1779874358523524105050326")),(mk_real_int (num_of_string "2519769086822114102463660"));(* 24, 24 *) (mk_real_int (num_of_string "3443487593214965231127710")),(mk_real_int (num_of_string "2426782895375382878614212"));(* 24, 24 *) (mk_real_int (num_of_string "3285656338990512429091275")),(mk_real_int (num_of_string "2984373445919228003273094"));(* 24, 24 *) (mk_real_int (num_of_string "4314236230687193720267938")),(mk_real_int (num_of_string "2225373491864527250771700"));(* 24, 24 *) (mk_real_int (num_of_string "2478372279428313787572144")),(mk_real_int (num_of_string "3801426829023353984025000"));(* 24, 24 *) (mk_real_int (num_of_string "2500983974801256013099590")),(mk_real_int (num_of_string "4455517448168933816797203"));(* 24, 24 *) (mk_real_int (num_of_string "2002660447950195390065100")),(mk_real_int (num_of_string "4488279614864399904105450"));(* 24, 24 *) (mk_real_int (num_of_string "4163410600149027442970304")),(mk_real_int (num_of_string "3203418022345839022287840"));(* 24, 24 *) (mk_real_int (num_of_string "2599024466111021067147595")),(mk_real_int (num_of_string "4667693580579038985578160"));(* 24, 24 *) (mk_real_int (num_of_string "2147626184708940627195714")),(mk_real_int (num_of_string "3898777472839066849346480"));(* 24, 24 *) (mk_real_int (num_of_string "4986732430512447935874972")),(mk_real_int (num_of_string "2026349844854417472196800"));(* 24, 24 *) (mk_real_int (num_of_string "2235233767138328400441921")),(mk_real_int (num_of_string "2514963234737734682616780"));(* 24, 24 *) (mk_real_int (num_of_string "4203291947432653538192286")),(mk_real_int (num_of_string "2333300927154146250669414"));(* 24, 24 *) (mk_real_int (num_of_string "1916261457270795390230552")),(mk_real_int (num_of_string "3231655283661329516916144"));(* 24, 24 *) (mk_real_int (num_of_string "4491965932549805600097685")),(mk_real_int (num_of_string "3504168050840627489641620"));(* 24, 24 *) (mk_real_int (num_of_string "3074107809630860486718422")),(mk_real_int (num_of_string "2981689537832681997593910"));(* 24, 24 *) (mk_real_int (num_of_string "5245568715873189191083868")),(mk_real_int (num_of_string "3375718636842147109854000"));(* 24, 24 *) (mk_real_int (num_of_string "4753063523302355267638320")),(mk_real_int (num_of_string "2327107102098530481453360"));(* 24, 24 *) (mk_real_int (num_of_string "1705397382417506318926560")),(mk_real_int (num_of_string "3085913616828201993917265"));(* 24, 24 *) (mk_real_int (num_of_string "5019586577411706882669696")),(mk_real_int (num_of_string "3926451060427808917112080"));(* 24, 24 *) (mk_real_int (num_of_string "3241713713511443485190260")),(mk_real_int (num_of_string "2182836938772685960004058"));(* 24, 24 *) (mk_real_int (num_of_string "2552786980499730679649952")),(mk_real_int (num_of_string "2973966043684451127530140"));(* 24, 24 *) (mk_real_int (num_of_string "4479763353915970040187396")),(mk_real_int (num_of_string "1511609643218873899237500"));(* 24, 24 *) (mk_real_int (num_of_string "4155170643346024211240300")),(mk_real_int (num_of_string "4417744887806841266637636"));(* 24, 24 *) (mk_real_int (num_of_string "4059338987780609857286076")),(mk_real_int (num_of_string "5568595794476263901754936"));(* 24, 24 *) (mk_real_int (num_of_string "4013162028339373727972700")),(mk_real_int (num_of_string "3952142675317672325776188"));(* 24, 24 *) (mk_real_int (num_of_string "4836813598681259947156020")),(mk_real_int (num_of_string "3381483203482708552498172"));(* 24, 24 *) (mk_real_int (num_of_string "2665430683910890637297352")),(mk_real_int (num_of_string "4245531220529071191258688"));(* 24, 24 *) (mk_real_int (num_of_string "1629556072161053646370124")),(mk_real_int (num_of_string "4002462676387666213400748"));(* 24, 24 *) (mk_real_int (num_of_string "1615197316463463566109360")),(mk_real_int (num_of_string "1715515091427536278015626"));(* 24, 24 *) (mk_real_int (num_of_string "3482818479233442171725760")),(mk_real_int (num_of_string "2982222781087759574832090"));(* 24, 24 *) (mk_real_int (num_of_string "2775487112541913677054651")),(mk_real_int (num_of_string "2717017211809153618142106"));(* 24, 24 *) (mk_real_int (num_of_string "2251632801889865424162030")),(mk_real_int (num_of_string "3828458778281338693676400"));(* 24, 24 *) (mk_real_int (num_of_string "2065401054824157092751048")),(mk_real_int (num_of_string "3474426600035747339666826"));(* 24, 24 *) (mk_real_int (num_of_string "3498756425256722232024688")),(mk_real_int (num_of_string "4067601972837753252059352"));(* 24, 24 *) (mk_real_int (num_of_string "2405500717993232347218088")),(mk_real_int (num_of_string "3866668251678339471814164"));(* 24, 24 *) (mk_real_int (num_of_string "2311588582476455589038150")),(mk_real_int (num_of_string "3900767452577121559274868"));(* 24, 24 *) (mk_real_int (num_of_string "3171032658989222245367760")),(mk_real_int (num_of_string "5435575394383580128572960"));(* 24, 24 *) (mk_real_int (num_of_string "5218063628817107909325600")),(mk_real_int (num_of_string "1952099170321457941801479"));(* 24, 24 *) (mk_real_int (num_of_string "4830555908515012273666320")),(mk_real_int (num_of_string "2496228456196981817168490"));(* 24, 24 *) (mk_real_int (num_of_string "1220810705236250691501456")),(mk_real_int (num_of_string "3210451479062445512812608"));(* 24, 24 *) (mk_real_int (num_of_string "4261279342148788250114460")),(mk_real_int (num_of_string "2188772775319654342086534"));(* 24, 24 *) (mk_real_int (num_of_string "2991344747479902137895186")),(mk_real_int (num_of_string "2220091707630399731868660"));(* 24, 24 *) (mk_real_int (num_of_string "6060340143176580413219816")),(mk_real_int (num_of_string "4619675419444584492567335"));(* 24, 24 *) (mk_real_int (num_of_string "5577827895551567509142784")),(mk_real_int (num_of_string "3766892451448798783631520"));(* 24, 24 *) (mk_real_int (num_of_string "5101963767420177424719640")),(mk_real_int (num_of_string "5422614303201216129006096"));(* 24, 24 *) (mk_real_int (num_of_string "3555860887498522886334528")),(mk_real_int (num_of_string "2247259234538002221485010"));(* 24, 24 *) (mk_real_int (num_of_string "3090363763848825329298992")),(mk_real_int (num_of_string "3343881543059550192321450"));(* 24, 24 *) (mk_real_int (num_of_string "3398474887607600118859695")),(mk_real_int (num_of_string "3764410772456867594814990"));(* 24, 24 *) (mk_real_int (num_of_string "2806701035896688342372280")),(mk_real_int (num_of_string "4014691964182037881999200"));(* 24, 24 *) (mk_real_int (num_of_string "2637060490992142385555400")),(mk_real_int (num_of_string "2686307811209691666513600"));(* 24, 24 *) (mk_real_int (num_of_string "3592051750103661055608320")),(mk_real_int (num_of_string "5465096901912289132587824"));(* 24, 24 *) (mk_real_int (num_of_string "3609269198041113223857240")),(mk_real_int (num_of_string "4645752364777824886061952"));(* 24, 24 *) (mk_real_int (num_of_string "1436831251554644449174776")),(mk_real_int (num_of_string "2837381902253721613220675"));(* 24, 24 *) (mk_real_int (num_of_string "2610632352807352705441480")),(mk_real_int (num_of_string "4043738007861746920457442"));(* 24, 24 *) (mk_real_int (num_of_string "1728684146659908804657688")),(mk_real_int (num_of_string "1087005085142325418071000"));(* 24, 24 *) (mk_real_int (num_of_string "5048393757113006650705264")),(mk_real_int (num_of_string "2972748841728811073527320"));(* 24, 24 *) (mk_real_int (num_of_string "3069177827362379181886248")),(mk_real_int (num_of_string "1525812459184099252778700"));(* 24, 24 *) (mk_real_int (num_of_string "2712298542392133298788100")),(mk_real_int (num_of_string "3408285432041219441099340"));(* 24, 24 *) (mk_real_int (num_of_string "5746168233059231419918344")),(mk_real_int (num_of_string "1994114488322539597862640"));(* 24, 24 *) (mk_real_int (num_of_string "3168847786392806493809358")),(mk_real_int (num_of_string "4780861202502421020033280"));(* 24, 24 *) (mk_real_int (num_of_string "2518346080772103067639920")),(mk_real_int (num_of_string "3811991482792838102175600"));(* 24, 24 *) (mk_real_int (num_of_string "2205723700259107942342880")),(mk_real_int (num_of_string "1862393619826874111532800"));(* 24, 24 *) (mk_real_int (num_of_string "2788057974655178048444940")),(mk_real_int (num_of_string "2334272927137485384348441"));(* 24, 24 *) (mk_real_int (num_of_string "2147390234014055247280000")),(mk_real_int (num_of_string "6943830955023672976315980"));(* 24, 24 *) (mk_real_int (num_of_string "2313492239846413917774320")),(mk_real_int (num_of_string "1575338375378015129792196"));(* 24, 24 *) (mk_real_int (num_of_string "4952985687992764823871600")),(mk_real_int (num_of_string "2275617485835052279466712"));(* 24, 24 *) (mk_real_int (num_of_string "3254798915686629647175672")),(mk_real_int (num_of_string "4883306706833673106230921"));(* 24, 24 *) (mk_real_int (num_of_string "1939162723280980781997864")),(mk_real_int (num_of_string "4695052903674560853618907"));(* 24, 24 *) (mk_real_int (num_of_string "1689109164030144643389180")),(mk_real_int (num_of_string "1882435458698167886660810"));(* 24, 24 *) (mk_real_int (num_of_string "1898880894184168019388836")),(mk_real_int (num_of_string "5227335360862736444312724"));(* 24, 24 *) (mk_real_int (num_of_string "4546330764450031715216940")),(mk_real_int (num_of_string "3211468738883724957346080"));(* 24, 24 *) (mk_real_int (num_of_string "3378869674935630536362989")),(mk_real_int (num_of_string "2069959299171637725128504"));(* 24, 24 *) (mk_real_int (num_of_string "5280175285500206726262784")),(mk_real_int (num_of_string "3195617278810402518024550"));(* 24, 24 *) (mk_real_int (num_of_string "1728727020143330602855840")),(mk_real_int (num_of_string "3254335369807155055564660"));(* 24, 24 *) (mk_real_int (num_of_string "5995645929201090102459200")),(mk_real_int (num_of_string "4253471431171762385696528"));(* 24, 24 *) (mk_real_int (num_of_string "3669359286980234535836420")),(mk_real_int (num_of_string "4762101775580533332544160"));(* 24, 24 *) (mk_real_int (num_of_string "2183867446903845982595264")),(mk_real_int (num_of_string "4669744339750872409352424"));(* 24, 24 *) (mk_real_int (num_of_string "2133624998435171614540456")),(mk_real_int (num_of_string "3067949171292532507532092"));(* 24, 24 *) (mk_real_int (num_of_string "4423048619794623598736828")),(mk_real_int (num_of_string "3146074707325709780410290"));(* 24, 24 *) (mk_real_int (num_of_string "4290702587887162550321316")),(mk_real_int (num_of_string "2807281905577256940249978"));(* 24, 24 *) (mk_real_int (num_of_string "3003655269995361360696000")),(mk_real_int (num_of_string "5126218504796917478998800"));(* 24, 24 *) (mk_real_int (num_of_string "2465164017460896470941644")),(mk_real_int (num_of_string "5005676407170062976165806"));(* 24, 24 *) (mk_real_int (num_of_string "3648483074723188565039072")),(mk_real_int (num_of_string "3656416951796210024164776"));(* 24, 24 *) (mk_real_int (num_of_string "2116870974808569356089752")),(mk_real_int (num_of_string "3882683032085684566613130"));(* 24, 24 *) (mk_real_int (num_of_string "3496365161102924665580460")),(mk_real_int (num_of_string "4554670163172702025345536"));(* 24, 24 *) (mk_real_int (num_of_string "3954468023887095899512800")),(mk_real_int (num_of_string "3930246037966805986259920"));(* 24, 24 *) (mk_real_int (num_of_string "3018346675219523287763760")),(mk_real_int (num_of_string "3782169658117946193270054"));(* 24, 24 *) (mk_real_int (num_of_string "2573650331408599873309440")),(mk_real_int (num_of_string "1886395854007188775216848"));(* 24, 24 *) (mk_real_int (num_of_string "2696165896360316776426492")),(mk_real_int (num_of_string "5573838865713805216774860"));(* 24, 24 *) (mk_real_int (num_of_string "2879490122979213294944562")),(mk_real_int (num_of_string "2055686761281629461304592"));(* 24, 24 *) (mk_real_int (num_of_string "3809911744693475538956832")),(mk_real_int (num_of_string "3400494787104971719539522"));(* 24, 24 *) (mk_real_int (num_of_string "2804925593497118988301340")),(mk_real_int (num_of_string "2346571721763204172960138"));(* 24, 24 *) (mk_real_int (num_of_string "2513547677852393863494044")),(mk_real_int (num_of_string "3538864702480318889520864"));(* 24, 24 *) (mk_real_int (num_of_string "2569339403409757642824972")),(mk_real_int (num_of_string "3397177476970212389203800"));(* 24, 24 *) (mk_real_int (num_of_string "3203444061211206763542780")),(mk_real_int (num_of_string "2913446612193826143526608"));(* 24, 24 *) (mk_real_int (num_of_string "2298258180308311529647965")),(mk_real_int (num_of_string "5874856716054410368397883"));(* 24, 24 *) (mk_real_int (num_of_string "3905424324315168629236668")),(mk_real_int (num_of_string "1312552778380132631355630"));(* 24, 24 *) (mk_real_int (num_of_string "2100401568808789500938130")),(mk_real_int (num_of_string "3624185475493973228350999"));(* 24, 24 *) (mk_real_int (num_of_string "2735564228922707339422382")),(mk_real_int (num_of_string "2848369989068442380880639"));(* 24, 24 *) (mk_real_int (num_of_string "5474346718199559347665760")),(mk_real_int (num_of_string "1434160534242763273148784"));(* 24, 24 *) (mk_real_int (num_of_string "4395654228223559568127686")),(mk_real_int (num_of_string "2059211346711145307357184"));(* 24, 24 *) (mk_real_int (num_of_string "3997773594622678229946496")),(mk_real_int (num_of_string "2735630886606255619122400"));(* 24, 24 *) (mk_real_int (num_of_string "5551069986141672573141372")),(mk_real_int (num_of_string "1764488920036674471696000"));(* 24, 24 *) (mk_real_int (num_of_string "3383080218107440062091776")),(mk_real_int (num_of_string "3854658659983760167134272"));(* 24, 24 *) (mk_real_int (num_of_string "2285029837604246420061648")),(mk_real_int (num_of_string "2006428793525331937972704"));(* 24, 24 *) (mk_real_int (num_of_string "2066528788331516455386534")),(mk_real_int (num_of_string "3357129845572650546502970"));(* 24, 24 *) (mk_real_int (num_of_string "4252224592197236768800410")),(mk_real_int (num_of_string "2847262293940670823525552"));(* 24, 24 *) (mk_real_int (num_of_string "3669156096680054599739454")),(mk_real_int (num_of_string "4560948525729991467338433"));(* 24, 24 *) (mk_real_int (num_of_string "4653299518019798026604220")),(mk_real_int (num_of_string "2771268569748152216184816"));(* 24, 24 *) (mk_real_int (num_of_string "2216089039727139625503252")),(mk_real_int (num_of_string "2035011323583548959960773"));(* 24, 24 *) (mk_real_int (num_of_string "4864408409177209450629498")),(mk_real_int (num_of_string "3675115473613313238144240"));(* 24, 24 *) (mk_real_int (num_of_string "2642135296420783466470036")),(mk_real_int (num_of_string "2601448092917950480235020"));(* 24, 24 *) (mk_real_int (num_of_string "1557370470602866884607500")),(mk_real_int (num_of_string "2536269125553467233628160"));(* 24, 24 *) (mk_real_int (num_of_string "4386194819425356158263680")),(mk_real_int (num_of_string "1707381307674273705062400"));(* 24, 24 *) (mk_real_int (num_of_string "5650036206681632812616544")),(mk_real_int (num_of_string "1317277097957760439183488"));(* 24, 24 *) (mk_real_int (num_of_string "2091632447013160221793233")),(mk_real_int (num_of_string "3546416136459480394323928"));(* 24, 24 *) (mk_real_int (num_of_string "3252501491099008866572610")),(mk_real_int (num_of_string "2219073850905812907806688"));(* 24, 24 *) (mk_real_int (num_of_string "2260513241487530712885888")),(mk_real_int (num_of_string "4637259398672364708216960"));(* 24, 24 *) (mk_real_int (num_of_string "3196356468385805267486592")),(mk_real_int (num_of_string "2352978380479574174062134"));(* 24, 24 *) (mk_real_int (num_of_string "3714057298480235143874038")),(mk_real_int (num_of_string "3571837133464168521598080"));(* 24, 24 *) (mk_real_int (num_of_string "4610918404935155548349616")),(mk_real_int (num_of_string "2120682899434171511243910"));(* 24, 24 *) (mk_real_int (num_of_string "4922899954384169263217170")),(mk_real_int (num_of_string "2210547168277235466418080"));(* 24, 24 *) (mk_real_int (num_of_string "2960626131797007955682674")),(mk_real_int (num_of_string "4277962918696360385898000"));(* 24, 24 *) (mk_real_int (num_of_string "4515490547648444411084695")),(mk_real_int (num_of_string "1569887925740428924873620"));(* 24, 24 *) (mk_real_int (num_of_string "2780763205535868959241050")),(mk_real_int (num_of_string "4056949241277091622381568"));(* 24, 24 *) (mk_real_int (num_of_string "3201767991034105671755280")),(mk_real_int (num_of_string "2350553743997253715117197"));(* 24, 24 *) (mk_real_int (num_of_string "3724987470309020360168472")),(mk_real_int (num_of_string "3429567734675220809454850"));(* 24, 24 *) (mk_real_int (num_of_string "3938698149785114837545440")),(mk_real_int (num_of_string "6131169302912038822972320"));(* 24, 24 *) (mk_real_int (num_of_string "3395710073615647174584356")),(mk_real_int (num_of_string "1678529113735920561129664"));(* 24, 24 *) (mk_real_int (num_of_string "7269519556215240259854704")),(mk_real_int (num_of_string "3537200463244173539446542"));(* 24, 24 *) (mk_real_int (num_of_string "4801317070771283122928748")),(mk_real_int (num_of_string "4478532737656770213917259"));(* 24, 24 *) (mk_real_int (num_of_string "3682003573644424252035630")),(mk_real_int (num_of_string "1950885564721030069055616"));(* 24, 24 *) (mk_real_int (num_of_string "5446965365946434393069490")),(mk_real_int (num_of_string "3065638380346793995642674"));(* 24, 24 *) (mk_real_int (num_of_string "3414262112322264079319040")),(mk_real_int (num_of_string "3000463633367199149754996"));(* 24, 24 *) (mk_real_int (num_of_string "3477210997651554728793548")),(mk_real_int (num_of_string "2238012569604837611287468"));(* 24, 24 *) (mk_real_int (num_of_string "2397940080265256872376850")),(mk_real_int (num_of_string "7164284672449448711229440"));(* 24, 24 *) (mk_real_int (num_of_string "1920225109538486329758288")),(mk_real_int (num_of_string "3782477993216083113543408"));(* 24, 24 *) (mk_real_int (num_of_string "3384707638379139460530792")),(mk_real_int (num_of_string "3431808747319441443432500"));(* 24, 24 *) (mk_real_int (num_of_string "2351301264311734801079126")),(mk_real_int (num_of_string "3621205301355428301129566"));(* 24, 24 *) (mk_real_int (num_of_string "3966665035633266460679640")),(mk_real_int (num_of_string "2403421476288006422304000"));(* 24, 24 *) (mk_real_int (num_of_string "3576887668698535447459740")),(mk_real_int (num_of_string "3581997969604934315876776"));(* 24, 24 *) (mk_real_int (num_of_string "3409910285149697296920984")),(mk_real_int (num_of_string "6770814009080962580277120"));(* 24, 24 *) (mk_real_int (num_of_string "2853513652481387858482800")),(mk_real_int (num_of_string "3226634307221175611848440"));(* 24, 24 *) (mk_real_int (num_of_string "2387804176228079537570625")),(mk_real_int (num_of_string "2944513954290027755615112"));(* 24, 24 *) (mk_real_int (num_of_string "5267300335689198610515075")),(mk_real_int (num_of_string "4604806741911951544187194"));(* 24, 24 *) (mk_real_int (num_of_string "1420848860925426826597968")),(mk_real_int (num_of_string "1835392191899974868181876"));(* 24, 24 *) (mk_real_int (num_of_string "1790041612902132482678016")),(mk_real_int (num_of_string "4552106763868225825287544"));(* 24, 24 *) (mk_real_int (num_of_string "2662666647277983358115700")),(mk_real_int (num_of_string "2220933142447482545655378"));(* 24, 24 *) (mk_real_int (num_of_string "1961018156393779549961568")),(mk_real_int (num_of_string "2372849960507874529038060"));(* 24, 24 *) (mk_real_int (num_of_string "3880727101280308691429850")),(mk_real_int (num_of_string "2234403290226715215444800"));(* 24, 24 *) (mk_real_int (num_of_string "2665926384817997919166038")),(mk_real_int (num_of_string "4670029254777132063838075"));(* 24, 24 *) (mk_real_int (num_of_string "2784893193130297123610383")),(mk_real_int (num_of_string "2150499599310185288615670"));(* 24, 24 *) (mk_real_int (num_of_string "4723188924824289143709276")),(mk_real_int (num_of_string "3294353411065339059335836"));(* 24, 24 *) (mk_real_int (num_of_string "2232051901288524666672310")),(mk_real_int (num_of_string "4145742036523115915560100"));(* 24, 24 *) (mk_real_int (num_of_string "1975679804277267924882144")),(mk_real_int (num_of_string "4105474903823749701919989"));(* 24, 24 *) (mk_real_int (num_of_string "3709535969545162547261610")),(mk_real_int (num_of_string "4198147955726582801071856"));(* 24, 24 *) (mk_real_int (num_of_string "3620705082268964290914852")),(mk_real_int (num_of_string "2103332314626327005886732"));(* 24, 24 *) (mk_real_int (num_of_string "1795163272996691139641904")),(mk_real_int (num_of_string "2707432087412693713392320"));(* 24, 24 *) (mk_real_int (num_of_string "2638306558357711860007368")),(mk_real_int (num_of_string "3343698657272575888420212"));(* 24, 24 *) (mk_real_int (num_of_string "5804236556798298673488401")),(mk_real_int (num_of_string "3808867612972287446542458"));(* 24, 24 *) (mk_real_int (num_of_string "4919864579444673212916000")),(mk_real_int (num_of_string "3934005128314766708376960"));(* 24, 24 *) (mk_real_int (num_of_string "1982713316904837075243978")),(mk_real_int (num_of_string "3926593049218002075459447"));(* 24, 24 *) (mk_real_int (num_of_string "3792959862968070379421784")),(mk_real_int (num_of_string "3362579390656969662430625"));(* 24, 24 *) (mk_real_int (num_of_string "3821041820420836219652850")),(mk_real_int (num_of_string "3743947815109494850338560"));(* 24, 24 *) (mk_real_int (num_of_string "3938038552485041028732216")),(mk_real_int (num_of_string "4045584137266871515820376"));(* 24, 24 *) (mk_real_int (num_of_string "2737146216075827246911660")),(mk_real_int (num_of_string "3297115613654613682927737"));(* 24, 24 *) (mk_real_int (num_of_string "2406995210541409216163248")),(mk_real_int (num_of_string "3878027943927971091008270"));(* 24, 24 *) (mk_real_int (num_of_string "4489826540173941094254054")),(mk_real_int (num_of_string "2119573062713007906694324"));(* 24, 24 *) (mk_real_int (num_of_string "1623531464117039382456474")),(mk_real_int (num_of_string "1962767340153793316646558"));(* 24, 24 *) (mk_real_int (num_of_string "2617541120905243237382400")),(mk_real_int (num_of_string "2181683350452092398682400"));(* 24, 24 *) (mk_real_int (num_of_string "4949813235338606008029006")),(mk_real_int (num_of_string "3329985822165158031421760"));(* 24, 24 *) (mk_real_int (num_of_string "4564657810786736028348495")),(mk_real_int (num_of_string "2572809218788399316267685"));(* 24, 24 *) (mk_real_int (num_of_string "1287104109305144498860482")),(mk_real_int (num_of_string "3936989626514460343082475"));(* 24, 24 *) (mk_real_int (num_of_string "2229132765122414895600630")),(mk_real_int (num_of_string "2185090593767888234720250"));(* 24, 24 *) (mk_real_int (num_of_string "5925072543326270369398024")),(mk_real_int (num_of_string "3701479351696411884047904"));(* 24, 24 *) (mk_real_int (num_of_string "3260603732088058521412720")),(mk_real_int (num_of_string "5717955526523948542766085"));(* 24, 24 *) (mk_real_int (num_of_string "6089704229847075956380782")),(mk_real_int (num_of_string "4515059664202322678349430"));(* 24, 24 *) (mk_real_int (num_of_string "2384502833749125551685482")),(mk_real_int (num_of_string "4108414419814259884453278"));(* 24, 24 *) (mk_real_int (num_of_string "5405368048938813037927320")),(mk_real_int (num_of_string "2456869728841812160987032"));(* 24, 24 *) (mk_real_int (num_of_string "5555709118721657037229971")),(mk_real_int (num_of_string "3409353028405206474259707"));(* 24, 24 *) (mk_real_int (num_of_string "4145770782252709682384456")),(mk_real_int (num_of_string "2576036451572432484543390"));(* 24, 24 *) (mk_real_int (num_of_string "2578735969457993120375296")),(mk_real_int (num_of_string "2214675284593388556653280"));(* 24, 24 *) (mk_real_int (num_of_string "2909464381868153215888320")),(mk_real_int (num_of_string "2783433524676189869221980"));(* 24, 24 *) (mk_real_int (num_of_string "3713258512286019278592120")),(mk_real_int (num_of_string "2977028998572790794990280"));(* 24, 24 *) (mk_real_int (num_of_string "3020180942228366640181248")),(mk_real_int (num_of_string "3028091668665965406411390"));(* 24, 24 *) (mk_real_int (num_of_string "2245423523762357206723245")),(mk_real_int (num_of_string "3269096807990197660458300"));(* 24, 24 *) (mk_real_int (num_of_string "2813162924485556091946560")),(mk_real_int (num_of_string "2544559305095499849311898"));(* 24, 24 *) (mk_real_int (num_of_string "2832427062392052684809138")),(mk_real_int (num_of_string "4039434510916601495094000"));(* 24, 24 *) (mk_real_int (num_of_string "4378371025102721431296000")),(mk_real_int (num_of_string "3657939048320779263212640"));(* 24, 24 *) (mk_real_int (num_of_string "4107360228511938043263024")),(mk_real_int (num_of_string "4955332387692102648026776"));(* 24, 24 *) (mk_real_int (num_of_string "5436711148146713044271760")),(mk_real_int (num_of_string "3462458821755521205760457"));(* 24, 24 *) (mk_real_int (num_of_string "1973674305815157563069984")),(mk_real_int (num_of_string "3381651016243346007010689"));(* 24, 24 *) (mk_real_int (num_of_string "5100495154128640720199453")),(mk_real_int (num_of_string "3482253801913287165790410"));(* 24, 24 *) (mk_real_int (num_of_string "1785590721531524554811824")),(mk_real_int (num_of_string "3961748467234839171830760"));(* 24, 24 *) (mk_real_int (num_of_string "2377270539951462159476760")),(mk_real_int (num_of_string "2490751406117841852125088"));(* 24, 24 *) (mk_real_int (num_of_string "5032033308425526566524416")),(mk_real_int (num_of_string "2074464511517629504599040"));(* 24, 24 *) (mk_real_int (num_of_string "2942469639515776623927102")),(mk_real_int (num_of_string "2733188181184590887199504"));(* 24, 24 *) (mk_real_int (num_of_string "4802475160397610089814000")),(mk_real_int (num_of_string "3254431376162523650352000"));(* 24, 24 *) (mk_real_int (num_of_string "2822599275376472475791796")),(mk_real_int (num_of_string "2473295846388528589497272"));(* 24, 24 *) (mk_real_int (num_of_string "2235523287368673855433088")),(mk_real_int (num_of_string "4366579838228373670874892"));(* 24, 24 *) (mk_real_int (num_of_string "2203413059461571553955415")),(mk_real_int (num_of_string "3499383296992796129060934"));(* 24, 24 *) (mk_real_int (num_of_string "3325808408886736395750606")),(mk_real_int (num_of_string "2624384765439873398004900"));(* 24, 24 *) (mk_real_int (num_of_string "3260509372546136138405628")),(mk_real_int (num_of_string "2358588018637629787499400"));(* 24, 24 *) (mk_real_int (num_of_string "4619173444075230071480496")),(mk_real_int (num_of_string "2798743023066958575904440"));(* 24, 24 *) (mk_real_int (num_of_string "2413757147346066310314139")),(mk_real_int (num_of_string "2828010538664101218235494"));(* 24, 24 *) (mk_real_int (num_of_string "2695484358347008110563632")),(mk_real_int (num_of_string "3928226440296002503853488"));(* 24, 24 *) (mk_real_int (num_of_string "2919630281131690269988101")),(mk_real_int (num_of_string "3225769195992502750565832"));(* 24, 24 *) (mk_real_int (num_of_string "2376149228976072780840608")),(mk_real_int (num_of_string "3715412531659976389224780"));(* 24, 24 *) (mk_real_int (num_of_string "3888077753530830891900204")),(mk_real_int (num_of_string "5885050913844627025051488"));(* 24, 24 *) (mk_real_int (num_of_string "2358614239305339825695860")),(mk_real_int (num_of_string "5975981997528600660191504"));(* 24, 24 *) (mk_real_int (num_of_string "2988172387270547212206900")),(mk_real_int (num_of_string "3023430170663008013906544"));(* 24, 24 *) (mk_real_int (num_of_string "2170836060399603291778560")),(mk_real_int (num_of_string "1692497197142932054277676"));(* 24, 24 *) (mk_real_int (num_of_string "1777433028479422333816170")),(mk_real_int (num_of_string "5231511312113085712034400"));(* 24, 24 *) (mk_real_int (num_of_string "4545540685863518124524544")),(mk_real_int (num_of_string "3033036670141677059892135"));(* 24, 24 *) (mk_real_int (num_of_string "5516472908525595456861200")),(mk_real_int (num_of_string "3248632421956873037497712"));(* 24, 24 *) (mk_real_int (num_of_string "3613327732914895907590176")),(mk_real_int (num_of_string "2592430014981547702579200"));(* 24, 24 *) (mk_real_int (num_of_string "3147164404436083703613669")),(mk_real_int (num_of_string "2822106430522611201489786"));(* 24, 24 *) (mk_real_int (num_of_string "5092693936725943601524688")),(mk_real_int (num_of_string "2706954925707508681911264"));(* 24, 24 *) (mk_real_int (num_of_string "3900216106407311605829369")),(mk_real_int (num_of_string "2663045715895949635736162"));(* 24, 24 *) (mk_real_int (num_of_string "3835290235059794911341220")),(mk_real_int (num_of_string "4740597369977702371556975"));(* 24, 24 *) (mk_real_int (num_of_string "3312020133057015667390272")),(mk_real_int (num_of_string "3524319196260443412215160"));(* 24, 24 *) (mk_real_int (num_of_string "3654327391145566869382693")),(mk_real_int (num_of_string "2480967920402895911422050"));(* 24, 24 *) (mk_real_int (num_of_string "3783318665094867715251116")),(mk_real_int (num_of_string "2272653547584035915986704"));(* 24, 24 *) (mk_real_int (num_of_string "2868066409669595479299016")),(mk_real_int (num_of_string "5818741035989499701039392"));(* 24, 24 *) (mk_real_int (num_of_string "4493180109061114521004800")),(mk_real_int (num_of_string "2201500662063176338248750"));(* 24, 24 *) (mk_real_int (num_of_string "3686697283809323160244917")),(mk_real_int (num_of_string "4271361656546144626656624"));(* 24, 24 *) (mk_real_int (num_of_string "4211812125317822019019200")),(mk_real_int (num_of_string "4422403566512232285695031"));(* 24, 24 *) (mk_real_int (num_of_string "3453197614954888233295680")),(mk_real_int (num_of_string "3981929378586757323208800"));(* 24, 24 *) (mk_real_int (num_of_string "2309247920202178729036044")),(mk_real_int (num_of_string "3208945197981154252165020"));(* 24, 24 *) (mk_real_int (num_of_string "3306996119702008268577990")),(mk_real_int (num_of_string "4043880307983849203623320"));(* 24, 24 *) (mk_real_int (num_of_string "2114883883410189511094202")),(mk_real_int (num_of_string "3184216904938045204263750"));(* 24, 24 *) (mk_real_int (num_of_string "2952919714331350069363200")),(mk_real_int (num_of_string "5876412699744818216031816"));(* 24, 24 *) (mk_real_int (num_of_string "3769437382174693707903152")),(mk_real_int (num_of_string "2565476447448203902466568"));(* 24, 24 *) (mk_real_int (num_of_string "1725307254792804728288880")),(mk_real_int (num_of_string "2586663881894774346726160"));(* 24, 24 *) (mk_real_int (num_of_string "2564718711812524173374118")),(mk_real_int (num_of_string "4058434081207693075361340"));(* 24, 24 *) (mk_real_int (num_of_string "2164528533204020104909200")),(mk_real_int (num_of_string "3554466067783606087782813"));(* 24, 24 *) (mk_real_int (num_of_string "3715414969648956770189664")),(mk_real_int (num_of_string "4244685581932290093498270"));(* 24, 24 *) (mk_real_int (num_of_string "3894983489637785283620856")),(mk_real_int (num_of_string "5156102771400354240360960"));(* 24, 24 *) (mk_real_int (num_of_string "4202972827934777774801550")),(mk_real_int (num_of_string "4780847702925393600007008"));(* 24, 24 *) (mk_real_int (num_of_string "3534273337045677653475600")),(mk_real_int (num_of_string "4358009326840387400100000"));(* 24, 24 *) (mk_real_int (num_of_string "2876651086186021980324230")),(mk_real_int (num_of_string "3243040372713434284988928"));(* 24, 24 *) (mk_real_int (num_of_string "2962649277866019737201310")),(mk_real_int (num_of_string "2779017685801357531021029"));(* 24, 24 *) (mk_real_int (num_of_string "2315102667320815921207020")),(mk_real_int (num_of_string "2320780188478351696079136"));(* 24, 24 *) (mk_real_int (num_of_string "4769419908213077485693920")),(mk_real_int (num_of_string "2981852984212469912663340"));(* 24, 24 *) (mk_real_int (num_of_string "2224859393974661825103210")),(mk_real_int (num_of_string "3440599874728666682929344"));(* 24, 24 *) (mk_real_int (num_of_string "5570579994531868141885878")),(mk_real_int (num_of_string "3266812861307218115114880"));(* 24, 24 *) (mk_real_int (num_of_string "3702867379759390156215762")),(mk_real_int (num_of_string "4583452938091837401961116"));(* 24, 24 *) (mk_real_int (num_of_string "4961769494404693175839944")),(mk_real_int (num_of_string "1530926530580760797685396"));(* 24, 24 *) (mk_real_int (num_of_string "5728049929213352197190729")),(mk_real_int (num_of_string "1674598136405635762453360"));(* 24, 24 *) (mk_real_int (num_of_string "4030621484894723831061348")),(mk_real_int (num_of_string "2596532216129821520493012"));(* 24, 24 *) (mk_real_int (num_of_string "1959873204216208801370634")),(mk_real_int (num_of_string "3597842466443105716862362"));(* 24, 24 *) (mk_real_int (num_of_string "3606904156095963174553056")),(mk_real_int (num_of_string "2238210053805009608920750"));(* 24, 24 *) (mk_real_int (num_of_string "3303581287385676756784584")),(mk_real_int (num_of_string "3710070051538617133078400"));(* 24, 24 *) (mk_real_int (num_of_string "3418027510405129534912656")),(mk_real_int (num_of_string "1688154262729905202044835"));(* 24, 24 *) (mk_real_int (num_of_string "3619520797540224475800720")),(mk_real_int (num_of_string "3672680730965811639295452"));(* 24, 24 *) (mk_real_int (num_of_string "5147246259164789444371168")),(mk_real_int (num_of_string "4721548755435949530244368"));(* 24, 24 *) (mk_real_int (num_of_string "1587840210917553115963960")),(mk_real_int (num_of_string "4134439520367555380790900"));(* 24, 24 *) (mk_real_int (num_of_string "2298913907225147087675904")),(mk_real_int (num_of_string "3702059809571200553981451"));(* 24, 24 *) (mk_real_int (num_of_string "5038129334873223844896480")),(mk_real_int (num_of_string "3167451495583167355735392"));(* 24, 24 *) (mk_real_int (num_of_string "3927939034696373890546500")),(mk_real_int (num_of_string "6707521950665622965364860"));(* 24, 24 *) (mk_real_int (num_of_string "1809267405475279111804125")),(mk_real_int (num_of_string "4609466476527470391867384"));(* 24, 24 *) (mk_real_int (num_of_string "4343752201291146716793264")),(mk_real_int (num_of_string "1678315295630693446162725"));(* 24, 24 *) (mk_real_int (num_of_string "4326453917791671479075766")),(mk_real_int (num_of_string "3386238587309411180302592"));(* 24, 24 *) (mk_real_int (num_of_string "3463794959208334625692950")),(mk_real_int (num_of_string "2287753439110638256405725"));(* 24, 24 *) (mk_real_int (num_of_string "3951828146691454281710120")),(mk_real_int (num_of_string "2062122695737615799021800"));(* 24, 24 *) (mk_real_int (num_of_string "3332828738831289645253376")),(mk_real_int (num_of_string "2648144126603704627173920"));(* 24, 24 *) (mk_real_int (num_of_string "2976001482854194300322520")),(mk_real_int (num_of_string "2887672701324693956534136"));(* 24, 24 *) (mk_real_int (num_of_string "2339574252864327339429036")),(mk_real_int (num_of_string "2716969298024328512570496"));(* 24, 24 *) (mk_real_int (num_of_string "1342205009418183992000645")),(mk_real_int (num_of_string "1767287736407958173765928"));(* 24, 24 *) (mk_real_int (num_of_string "2910934451193965633979360")),(mk_real_int (num_of_string "5545846909531323260812125"));(* 24, 24 *) (mk_real_int (num_of_string "2766460280062310813937150")),(mk_real_int (num_of_string "1823557519392735790550250"));(* 24, 24 *) (mk_real_int (num_of_string "4100883438249583081441710")),(mk_real_int (num_of_string "3776536579466850444434280"));(* 24, 24 *) (mk_real_int (num_of_string "2754484322605026848424000")),(mk_real_int (num_of_string "2749548253558153043748972"));(* 24, 24 *) (mk_real_int (num_of_string "5036176523451903716835180")),(mk_real_int (num_of_string "1699964541630268639030846"));(* 24, 24 *) (mk_real_int (num_of_string "2892457261261515275295072")),(mk_real_int (num_of_string "4737917348249117366382312"));(* 24, 24 *) (mk_real_int (num_of_string "2655694368730650145334590")),(mk_real_int (num_of_string "5696705810378435054007260"));(* 24, 24 *) (mk_real_int (num_of_string "2125567616064901984112280")),(mk_real_int (num_of_string "3123401016848598207609624"));(* 24, 24 *) (mk_real_int (num_of_string "3287532167806442593083696")),(mk_real_int (num_of_string "2851872329541967808088576"));(* 24, 24 *) (mk_real_int (num_of_string "2110665688856826063982782")),(mk_real_int (num_of_string "4359365146595490694185540"));(* 24, 24 *) (mk_real_int (num_of_string "2742026171037757323496686")),(mk_real_int (num_of_string "4362951065920148256473655"));(* 24, 24 *) (mk_real_int (num_of_string "4863996158579315945245404")),(mk_real_int (num_of_string "4661861974837787998583364"));(* 24, 24 *) (mk_real_int (num_of_string "3137416017688025588209824")),(mk_real_int (num_of_string "1668417247566880818800520"));(* 24, 24 *) (mk_real_int (num_of_string "2512930687725718356136740")),(mk_real_int (num_of_string "2747490826835787651045760"));(* 24, 24 *) (mk_real_int (num_of_string "3616727227753120896449790")),(mk_real_int (num_of_string "2138011821151658288097768"));(* 24, 24 *) (mk_real_int (num_of_string "4303695870465698777856430")),(mk_real_int (num_of_string "3694352795099709117822550"));(* 24, 24 *) (mk_real_int (num_of_string "2494545587403306610705536")),(mk_real_int (num_of_string "2127047713718586637502335"));(* 24, 24 *) (mk_real_int (num_of_string "3682937230425044571950100")),(mk_real_int (num_of_string "2787744343394529734604480"));(* 24, 24 *) (mk_real_int (num_of_string "2720270054035519760933676")),(mk_real_int (num_of_string "1537723295890870892974842"));(* 24, 24 *) (mk_real_int (num_of_string "4414287224158656730131960")),(mk_real_int (num_of_string "3338820563844857835947284"));(* 24, 24 *) (mk_real_int (num_of_string "2947712174379402686492152")),(mk_real_int (num_of_string "4278192782495224843027880"));(* 24, 24 *) (mk_real_int (num_of_string "4254423812842316074921620")),(mk_real_int (num_of_string "5219242672484446856517176"));(* 24, 24 *) (mk_real_int (num_of_string "2708337926429271288652500")),(mk_real_int (num_of_string "5602515023082664412274073"));(* 24, 24 *) (mk_real_int (num_of_string "2302230306760603549763640")),(mk_real_int (num_of_string "2616129890348013967167500"));(* 24, 24 *) (mk_real_int (num_of_string "1537358313649027006915704")),(mk_real_int (num_of_string "3372255058869903855117700"));(* 24, 24 *) (mk_real_int (num_of_string "2158655391931110381138900")),(mk_real_int (num_of_string "3901648623382268125529625"));(* 24, 24 *) (mk_real_int (num_of_string "4342147892965040556893040")),(mk_real_int (num_of_string "3233451713602589098425882"));(* 24, 24 *) (mk_real_int (num_of_string "3254852446790581775575104")),(mk_real_int (num_of_string "2677496538692408692259712"));(* 24, 24 *) (mk_real_int (num_of_string "2237469021625840187917212")),(mk_real_int (num_of_string "4513488210547085890888443"));(* 24, 24 *) (mk_real_int (num_of_string "1320275598306020347281600")),(mk_real_int (num_of_string "2744191177715610186507240"));(* 24, 24 *) (mk_real_int (num_of_string "4109151232557266907816274")),(mk_real_int (num_of_string "4078720687200976153502208"));(* 24, 24 *) (mk_real_int (num_of_string "4627556064035690169000640")),(mk_real_int (num_of_string "2295629471442102948430740"));(* 24, 24 *) (mk_real_int (num_of_string "5705707060863012855675640")),(mk_real_int (num_of_string "3600579587450037335729750"));(* 24, 24 *) (mk_real_int (num_of_string "2512009315950533338457262")),(mk_real_int (num_of_string "3856225045003292468481856"));(* 24, 24 *) (mk_real_int (num_of_string "2648739216290917247056260")),(mk_real_int (num_of_string "2936601590951541845798784"));(* 24, 24 *) (mk_real_int (num_of_string "2232576509693201100223613")),(mk_real_int (num_of_string "2144203956355167208472640"));(* 24, 24 *) (mk_real_int (num_of_string "3485290359254877392280516")),(mk_real_int (num_of_string "5164458804685245700298664"));(* 24, 24 *) (mk_real_int (num_of_string "4589346462453793817801760")),(mk_real_int (num_of_string "2570339389505226238620500"));(* 24, 24 *) (mk_real_int (num_of_string "3577299554424904964502000")),(mk_real_int (num_of_string "2453132876981940048243040"));(* 24, 24 *) (mk_real_int (num_of_string "2821415976668630024164800")),(mk_real_int (num_of_string "3420474992854736708683800"));(* 24, 24 *) (mk_real_int (num_of_string "2638281059685931705348992")),(mk_real_int (num_of_string "3685876682481139319385912"));(* 24, 24 *) (mk_real_int (num_of_string "3288519757711992769327512")),(mk_real_int (num_of_string "4788799194591744602098176"));(* 24, 24 *) (mk_real_int (num_of_string "3448817412865831747744094")),(mk_real_int (num_of_string "2124311349303453010783040"));(* 24, 24 *) (mk_real_int (num_of_string "2888779820320927016269344")),(mk_real_int (num_of_string "4128675689816007977969286"));(* 24, 24 *) (mk_real_int (num_of_string "3404877808696273119002760")),(mk_real_int (num_of_string "1906108502880491124119838"));(* 24, 24 *) (mk_real_int (num_of_string "2190451096354080482571936")),(mk_real_int (num_of_string "3576305198241671999417616"));(* 24, 24 *) (mk_real_int (num_of_string "2441200367118636213536160")),(mk_real_int (num_of_string "2672304135402470260824000"));(* 24, 24 *) (mk_real_int (num_of_string "3326727360510639992269440")),(mk_real_int (num_of_string "1961461577056323085459425"));(* 24, 24 *) (mk_real_int (num_of_string "4263600999060083935558530")),(mk_real_int (num_of_string "4378371892121763599484330"));(* 24, 24 *) (mk_real_int (num_of_string "3748153850584594227473130")),(mk_real_int (num_of_string "1557284326681534509318624"));(* 24, 24 *) (mk_real_int (num_of_string "2469809458998362194654824")),(mk_real_int (num_of_string "6912788990497862893419600"));(* 24, 24 *) (mk_real_int (num_of_string "2818097446806456188455488")),(mk_real_int (num_of_string "2167770862817991712100925"));(* 24, 24 *) (mk_real_int (num_of_string "3193419136316652676056816")),(mk_real_int (num_of_string "3911625964183102903830612"));(* 24, 24 *) (mk_real_int (num_of_string "2943657912454805692644960")),(mk_real_int (num_of_string "3160927903601250883354740"));(* 24, 24 *) (mk_real_int (num_of_string "3222906674062661871231600")),(mk_real_int (num_of_string "2332586263197962852507280"));(* 24, 24 *) (mk_real_int (num_of_string "4395367582168534571730720")),(mk_real_int (num_of_string "2075983426514422491067008"));(* 24, 24 *) (mk_real_int (num_of_string "2680310325131737754123008")),(mk_real_int (num_of_string "5313344674862935615826376"));(* 24, 24 *) (mk_real_int (num_of_string "2400783642560516195403008")),(mk_real_int (num_of_string "3797847089617501345976980"));(* 24, 24 *) (mk_real_int (num_of_string "4349134886787057589046400")),(mk_real_int (num_of_string "4586079373474017047798165"));(* 24, 24 *) (mk_real_int (num_of_string "4035209671948663295473170")),(mk_real_int (num_of_string "4356048796728341564364240"));(* 24, 24 *) (mk_real_int (num_of_string "3359158829624252194267245")),(mk_real_int (num_of_string "2929367238232639926426705"));(* 24, 24 *) (mk_real_int (num_of_string "2626290274520999296736960")),(mk_real_int (num_of_string "4945570001369515265328000"));(* 24, 24 *) (mk_real_int (num_of_string "3949980592347107785324032")),(mk_real_int (num_of_string "3285770590740332520317655"));(* 24, 24 *) (mk_real_int (num_of_string "2642773478317706561247162")),(mk_real_int (num_of_string "2357569242797715689704650"));(* 24, 24 *) (mk_real_int (num_of_string "3122646690974100178156224")),(mk_real_int (num_of_string "3864496600517377628878248"));(* 24, 24 *) (mk_real_int (num_of_string "2535202946841047191355985")),(mk_real_int (num_of_string "2477935283344861968563395"));(* 24, 24 *) (mk_real_int (num_of_string "3303395926186846593897398")),(mk_real_int (num_of_string "2458180965729213074954838"));(* 24, 24 *) (mk_real_int (num_of_string "3354108602123950392214192")),(mk_real_int (num_of_string "3824842894885232790649800"));(* 24, 24 *) (mk_real_int (num_of_string "2851106936796166829209552")),(mk_real_int (num_of_string "2718844796718048849545000"));(* 24, 24 *) (mk_real_int (num_of_string "1412301700970928036501408")),(mk_real_int (num_of_string "4571010725399186056084800"));(* 24, 24 *) (mk_real_int (num_of_string "2943008909352395049428200")),(mk_real_int (num_of_string "5339336864040083969300796"));(* 24, 24 *) (mk_real_int (num_of_string "3306884160074212578966688")),(mk_real_int (num_of_string "1872637144586289356949102"));(* 24, 24 *) (mk_real_int (num_of_string "3256048419850881635016465")),(mk_real_int (num_of_string "2144011085305109275574046"));(* 24, 24 *) (mk_real_int (num_of_string "2596680805310662290917536")),(mk_real_int (num_of_string "2450421608490904185046404"));(* 24, 24 *) (mk_real_int (num_of_string "3231793758224635065307064")),(mk_real_int (num_of_string "3958858457346781103547432"));(* 24, 24 *) (mk_real_int (num_of_string "2405283204226616686936782")),(mk_real_int (num_of_string "2808013476135148272769050"));(* 24, 24 *) (mk_real_int (num_of_string "3763338878733490155287088")),(mk_real_int (num_of_string "4229089053686137795765529"));(* 24, 24 *) (mk_real_int (num_of_string "4237755514000042767533712")),(mk_real_int (num_of_string "2119446998743577750160060"));(* 24, 24 *) (mk_real_int (num_of_string "3464368637930585367397272")),(mk_real_int (num_of_string "2381047749608364820766772"));(* 24, 24 *) (mk_real_int (num_of_string "4308206451438940458440200")),(mk_real_int (num_of_string "3486250458148780127868816"));(* 24, 24 *) (mk_real_int (num_of_string "4469654659212523366872060")),(mk_real_int (num_of_string "3840229627895342265878160"));(* 24, 24 *) (mk_real_int (num_of_string "3416200316785701597352704")),(mk_real_int (num_of_string "2538542568128120877270304"));(* 24, 24 *) (mk_real_int (num_of_string "3507661181366145790378624")),(mk_real_int (num_of_string "1985547392333058157459268"));(* 24, 24 *) (mk_real_int (num_of_string "2523240153211810712705720")),(mk_real_int (num_of_string "3186005370171745416754800"));(* 24, 24 *) (mk_real_int (num_of_string "5099310704830201900730400")),(mk_real_int (num_of_string "2354957348375111252550498"));(* 24, 24 *) (mk_real_int (num_of_string "5617590437227126220070912")),(mk_real_int (num_of_string "3463090614554593525898430"));(* 24, 24 *) (mk_real_int (num_of_string "1862730819885660183684836")),(mk_real_int (num_of_string "1829736289222505028470352"));(* 24, 24 *) (mk_real_int (num_of_string "4056516438924446098756200")),(mk_real_int (num_of_string "1757954110460545441766674"));(* 24, 24 *) (mk_real_int (num_of_string "2232607912150261722342084")),(mk_real_int (num_of_string "2821288893414261004574073"));(* 24, 24 *) (mk_real_int (num_of_string "2988962662354245548345400")),(mk_real_int (num_of_string "3712288679813144811733080"));(* 24, 24 *) (mk_real_int (num_of_string "3110427272209884951787827")),(mk_real_int (num_of_string "1756662262853453142346110"));(* 24, 24 *) (mk_real_int (num_of_string "2933081616472425876964928")),(mk_real_int (num_of_string "2417207810796129056501460"));(* 24, 24 *) (mk_real_int (num_of_string "4326377389804058370593904")),(mk_real_int (num_of_string "3559771865194749564087728"));(* 24, 24 *) (mk_real_int (num_of_string "3908363773138263442414530")),(mk_real_int (num_of_string "2973518378970102660971850"));(* 24, 24 *) (mk_real_int (num_of_string "3219859556143144901406900")),(mk_real_int (num_of_string "3114906364850162011899660"));(* 24, 24 *) (mk_real_int (num_of_string "5825462004324264073160545")),(mk_real_int (num_of_string "2870458302900478487665520"));(* 24, 24 *) (mk_real_int (num_of_string "1990027583394633358454016")),(mk_real_int (num_of_string "4495044219884939828842224"))(* 24, 24 *) ];;