let data = [ (mk_real_int (num_of_string "33572409929580833751")),(mk_real_int (num_of_string "31148544303953368259"));(* 19, 19 *) (mk_real_int (num_of_string "25286050174190807804")),(mk_real_int (num_of_string "24730080721092594782"));(* 19, 19 *) (mk_real_int (num_of_string "28102898481056826372")),(mk_real_int (num_of_string "20558178005327796900"));(* 19, 19 *) (mk_real_int (num_of_string "35597949478152789376")),(mk_real_int (num_of_string "16655501835545179420"));(* 19, 19 *) (mk_real_int (num_of_string "34358853243790303767")),(mk_real_int (num_of_string "28853735865560168563"));(* 19, 19 *) (mk_real_int (num_of_string "39810130950918898900")),(mk_real_int (num_of_string "20991793221680908374"));(* 19, 19 *) (mk_real_int (num_of_string "36164914639034706954")),(mk_real_int (num_of_string "28333668815475848484"));(* 19, 19 *) (mk_real_int (num_of_string "20198888744582626276")),(mk_real_int (num_of_string "17283271267412299215"));(* 19, 19 *) (mk_real_int (num_of_string "23439470377235278080")),(mk_real_int (num_of_string "38563033030730109572"));(* 19, 19 *) (mk_real_int (num_of_string "15223622583443498928")),(mk_real_int (num_of_string "29735798434737708390"));(* 19, 19 *) (mk_real_int (num_of_string "18525935614021875028")),(mk_real_int (num_of_string "24037285142129988256"));(* 19, 19 *) (mk_real_int (num_of_string "28051053154610255550")),(mk_real_int (num_of_string "28768830119973522601"));(* 19, 19 *) (mk_real_int (num_of_string "17788180790513167760")),(mk_real_int (num_of_string "23090170534600145328"));(* 19, 19 *) (mk_real_int (num_of_string "21291126661160206268")),(mk_real_int (num_of_string "30741578193770457992"));(* 19, 19 *) (mk_real_int (num_of_string "37312400635530845968")),(mk_real_int (num_of_string "32065354411190445411"));(* 19, 19 *) (mk_real_int (num_of_string "33876812647503135915")),(mk_real_int (num_of_string "25416986314790221239"));(* 19, 19 *) (mk_real_int (num_of_string "13985990300271092642")),(mk_real_int (num_of_string "33251196154616671077"));(* 19, 19 *) (mk_real_int (num_of_string "40189368257349303135")),(mk_real_int (num_of_string "19866689936242500384"));(* 19, 19 *) (mk_real_int (num_of_string "32885639039242757680")),(mk_real_int (num_of_string "20826379267161536948"));(* 19, 19 *) (mk_real_int (num_of_string "21407567181068817584")),(mk_real_int (num_of_string "36013468503693282789"));(* 19, 19 *) (mk_real_int (num_of_string "20154159275924798586")),(mk_real_int (num_of_string "21532637598082055214"));(* 19, 19 *) (mk_real_int (num_of_string "33702246114925956370")),(mk_real_int (num_of_string "29222938712195650763"));(* 19, 19 *) (mk_real_int (num_of_string "38227543832118719848")),(mk_real_int (num_of_string "25135325679368858646"));(* 19, 19 *) (mk_real_int (num_of_string "22321716812668731381")),(mk_real_int (num_of_string "23543573531048464927"));(* 19, 19 *) (mk_real_int (num_of_string "23769134273467183997")),(mk_real_int (num_of_string "14369117920579248750"));(* 19, 19 *) (mk_real_int (num_of_string "29136534010572339318")),(mk_real_int (num_of_string "35899345969306125625"));(* 19, 19 *) (mk_real_int (num_of_string "14328464291121391796")),(mk_real_int (num_of_string "40312202315066193600"));(* 19, 19 *) (mk_real_int (num_of_string "21216429602204626944")),(mk_real_int (num_of_string "13321039568452832480"));(* 19, 19 *) (mk_real_int (num_of_string "26396844807676863696")),(mk_real_int (num_of_string "24664233439087612568"));(* 19, 19 *) (mk_real_int (num_of_string "22613254802828210532")),(mk_real_int (num_of_string "27943544635047532128"));(* 19, 19 *) (mk_real_int (num_of_string "20458784280731690817")),(mk_real_int (num_of_string "15903106777293095789"));(* 19, 19 *) (mk_real_int (num_of_string "27612300487446391420")),(mk_real_int (num_of_string "37299649274712282535"));(* 19, 19 *) (mk_real_int (num_of_string "19535852241344569009")),(mk_real_int (num_of_string "25235363567080868608"));(* 19, 19 *) (mk_real_int (num_of_string "21573960810733653630")),(mk_real_int (num_of_string "17395045895945547819"));(* 19, 19 *) (mk_real_int (num_of_string "22426091998882023936")),(mk_real_int (num_of_string "30917169703164305462"));(* 19, 19 *) (mk_real_int (num_of_string "17436089345828729895")),(mk_real_int (num_of_string "36147047013286273911"));(* 19, 19 *) (mk_real_int (num_of_string "29943846419256650397")),(mk_real_int (num_of_string "31608722356773399101"));(* 19, 19 *) (mk_real_int (num_of_string "20758244686394967125")),(mk_real_int (num_of_string "16297076128134636120"));(* 19, 19 *) (mk_real_int (num_of_string "23361855748705720224")),(mk_real_int (num_of_string "21805600907356868899"));(* 19, 19 *) (mk_real_int (num_of_string "33361192690924017876")),(mk_real_int (num_of_string "26155717117492121390"));(* 19, 19 *) (mk_real_int (num_of_string "32788120729712350904")),(mk_real_int (num_of_string "13701368012601836952"));(* 19, 19 *) (mk_real_int (num_of_string "31429381722792545800")),(mk_real_int (num_of_string "28056695270325970336"));(* 19, 19 *) (mk_real_int (num_of_string "23946781337003799175")),(mk_real_int (num_of_string "23354125263327730300"));(* 19, 19 *) (mk_real_int (num_of_string "19610178037329369996")),(mk_real_int (num_of_string "17483345854794771820"));(* 19, 19 *) (mk_real_int (num_of_string "19580385825437237680")),(mk_real_int (num_of_string "18369444402307520511"));(* 19, 19 *) (mk_real_int (num_of_string "20373012670885241488")),(mk_real_int (num_of_string "18372444575150410888"));(* 19, 19 *) (mk_real_int (num_of_string "31774043202253507155")),(mk_real_int (num_of_string "22230406098202282156"));(* 19, 19 *) (mk_real_int (num_of_string "36260488950256746285")),(mk_real_int (num_of_string "14298842877484343112"));(* 19, 19 *) (mk_real_int (num_of_string "38348399502295316544")),(mk_real_int (num_of_string "23127526008428915304"));(* 19, 19 *) (mk_real_int (num_of_string "29468135840364033120")),(mk_real_int (num_of_string "42859521857231658832"));(* 19, 19 *) (mk_real_int (num_of_string "26195223730935481574")),(mk_real_int (num_of_string "14674640879141308450"));(* 19, 19 *) (mk_real_int (num_of_string "36971521144248970323")),(mk_real_int (num_of_string "25725412717362572071"));(* 19, 19 *) (mk_real_int (num_of_string "15373724279892883047")),(mk_real_int (num_of_string "37064424717555453504"));(* 19, 19 *) (mk_real_int (num_of_string "18456612225491964304")),(mk_real_int (num_of_string "20784497229636632470"));(* 19, 19 *) (mk_real_int (num_of_string "17238747478973240132")),(mk_real_int (num_of_string "25715658083515545574"));(* 19, 19 *) (mk_real_int (num_of_string "19434461103584416241")),(mk_real_int (num_of_string "29366615813009873244"));(* 19, 19 *) (mk_real_int (num_of_string "16186400016474915612")),(mk_real_int (num_of_string "21138557277456953576"));(* 19, 19 *) (mk_real_int (num_of_string "31076127393825322842")),(mk_real_int (num_of_string "26127382992901047440"));(* 19, 19 *) (mk_real_int (num_of_string "16638819785499599952")),(mk_real_int (num_of_string "30605559054078364356"));(* 19, 19 *) (mk_real_int (num_of_string "21653085879670267638")),(mk_real_int (num_of_string "24663482055635505478"));(* 19, 19 *) (mk_real_int (num_of_string "22047586830857827668")),(mk_real_int (num_of_string "21989678249953775823"));(* 19, 19 *) (mk_real_int (num_of_string "25246202619247689365")),(mk_real_int (num_of_string "38244780124493141826"));(* 19, 19 *) (mk_real_int (num_of_string "12754315174605904086")),(mk_real_int (num_of_string "14541853045744529648"));(* 19, 19 *) (mk_real_int (num_of_string "35068518276916323738")),(mk_real_int (num_of_string "19911078974382448424"));(* 19, 19 *) (mk_real_int (num_of_string "31788444163659174552")),(mk_real_int (num_of_string "25398105397820760000"));(* 19, 19 *) (mk_real_int (num_of_string "28708395192612575154")),(mk_real_int (num_of_string "30633710003636824128"));(* 19, 19 *) (mk_real_int (num_of_string "21039999747285910666")),(mk_real_int (num_of_string "32217872110426500168"));(* 19, 19 *) (mk_real_int (num_of_string "23961590926169909859")),(mk_real_int (num_of_string "28739147203340671306"));(* 19, 19 *) (mk_real_int (num_of_string "33711641417643357883")),(mk_real_int (num_of_string "23440835558663189216"));(* 19, 19 *) (mk_real_int (num_of_string "18430860997436289534")),(mk_real_int (num_of_string "23629245698406122170"));(* 19, 19 *) (mk_real_int (num_of_string "36675765814115269974")),(mk_real_int (num_of_string "22153900897071146280"));(* 19, 19 *) (mk_real_int (num_of_string "30642052708947370746")),(mk_real_int (num_of_string "19715061005550366852"));(* 19, 19 *) (mk_real_int (num_of_string "23631480399362961103")),(mk_real_int (num_of_string "21356124255862188133"));(* 19, 19 *) (mk_real_int (num_of_string "38061016225101124332")),(mk_real_int (num_of_string "21480531385150581876"));(* 19, 19 *) (mk_real_int (num_of_string "21788126356522731348")),(mk_real_int (num_of_string "15250407105622096408"));(* 19, 19 *) (mk_real_int (num_of_string "29939331877831765862")),(mk_real_int (num_of_string "24621235745368217571"));(* 19, 19 *) (mk_real_int (num_of_string "13559743163737887402")),(mk_real_int (num_of_string "29429210272328063175"));(* 19, 19 *) (mk_real_int (num_of_string "28196902181228285934")),(mk_real_int (num_of_string "19014462787109404824"));(* 19, 19 *) (mk_real_int (num_of_string "34413995495155206920")),(mk_real_int (num_of_string "17999593615355747120"));(* 19, 19 *) (mk_real_int (num_of_string "20098053603131429233")),(mk_real_int (num_of_string "25397368874886828820"));(* 19, 19 *) (mk_real_int (num_of_string "13991262173392155564")),(mk_real_int (num_of_string "20101775826597660624"));(* 19, 19 *) (mk_real_int (num_of_string "25958041019478922926")),(mk_real_int (num_of_string "30973577744291784525"));(* 19, 19 *) (mk_real_int (num_of_string "41762004568998584211")),(mk_real_int (num_of_string "24486642710242001344"));(* 19, 19 *) (mk_real_int (num_of_string "38468053625130677284")),(mk_real_int (num_of_string "21883488378665367740"));(* 19, 19 *) (mk_real_int (num_of_string "24217476494071001625")),(mk_real_int (num_of_string "19956600491408230034"));(* 19, 19 *) (mk_real_int (num_of_string "25031801718319605693")),(mk_real_int (num_of_string "35339430150394906635"));(* 19, 19 *) (mk_real_int (num_of_string "35354835249533769530")),(mk_real_int (num_of_string "19186948927433489202"));(* 19, 19 *) (mk_real_int (num_of_string "19633304667574387845")),(mk_real_int (num_of_string "37783496757986652992"));(* 19, 19 *) (mk_real_int (num_of_string "32591004179898436580")),(mk_real_int (num_of_string "26031672488743456128"));(* 19, 19 *) (mk_real_int (num_of_string "19562909602060384076")),(mk_real_int (num_of_string "18420082240032456225"));(* 19, 19 *) (mk_real_int (num_of_string "33906326894153724824")),(mk_real_int (num_of_string "23773891695716936565"));(* 19, 19 *) (mk_real_int (num_of_string "21631917102787719552")),(mk_real_int (num_of_string "21696134640674596080"));(* 19, 19 *) (mk_real_int (num_of_string "27877186561900804480")),(mk_real_int (num_of_string "32708760906440572536"));(* 19, 19 *) (mk_real_int (num_of_string "28250948698268387168")),(mk_real_int (num_of_string "21718640730902267944"));(* 19, 19 *) (mk_real_int (num_of_string "28054715173237417192")),(mk_real_int (num_of_string "23724974246612918125"));(* 19, 19 *) (mk_real_int (num_of_string "13565268300577577980")),(mk_real_int (num_of_string "18766332146987952351"));(* 19, 19 *) (mk_real_int (num_of_string "29089666539115063112")),(mk_real_int (num_of_string "11788072578080417476"));(* 19, 19 *) (mk_real_int (num_of_string "31029529641606442320")),(mk_real_int (num_of_string "21189804410527311174"));(* 19, 19 *) (mk_real_int (num_of_string "21801602489769337686")),(mk_real_int (num_of_string "23333346236694607520"));(* 19, 19 *) (mk_real_int (num_of_string "22684686870294067696")),(mk_real_int (num_of_string "15329888225567164194"));(* 19, 19 *) (mk_real_int (num_of_string "22437730893159525592")),(mk_real_int (num_of_string "31755887733435638916"));(* 19, 19 *) (mk_real_int (num_of_string "14118269694795938672")),(mk_real_int (num_of_string "19722019532976082278"));(* 19, 19 *) (mk_real_int (num_of_string "26250225002606078045")),(mk_real_int (num_of_string "21135249282229087676"));(* 19, 19 *) (mk_real_int (num_of_string "21754225347515547458")),(mk_real_int (num_of_string "14890978077204913948"));(* 19, 19 *) (mk_real_int (num_of_string "23066719611694210881")),(mk_real_int (num_of_string "33227912427853816728"));(* 19, 19 *) (mk_real_int (num_of_string "25405180212497008000")),(mk_real_int (num_of_string "12418361347178457440"));(* 19, 19 *) (mk_real_int (num_of_string "33247375512579506300")),(mk_real_int (num_of_string "25281151297831080333"));(* 19, 19 *) (mk_real_int (num_of_string "29600381494511770954")),(mk_real_int (num_of_string "24180176992314040940"));(* 19, 19 *) (mk_real_int (num_of_string "38059796897847382064")),(mk_real_int (num_of_string "24518423044570037440"));(* 19, 19 *) (mk_real_int (num_of_string "37060845735857157500")),(mk_real_int (num_of_string "21514010489270917365"));(* 19, 19 *) (mk_real_int (num_of_string "33948244403495950000")),(mk_real_int (num_of_string "13427941318582173240"));(* 19, 19 *) (mk_real_int (num_of_string "30925399411668710520")),(mk_real_int (num_of_string "30536000935575507064"));(* 19, 19 *) (mk_real_int (num_of_string "15178435189357299200")),(mk_real_int (num_of_string "36076146656034140480"));(* 19, 19 *) (mk_real_int (num_of_string "34199486308027151958")),(mk_real_int (num_of_string "17512585691833478400"));(* 19, 19 *) (mk_real_int (num_of_string "23048226430814991780")),(mk_real_int (num_of_string "34970883248279429220"));(* 19, 19 *) (mk_real_int (num_of_string "33972533374485277440")),(mk_real_int (num_of_string "28540529182512238078"));(* 19, 19 *) (mk_real_int (num_of_string "25233560957627367884")),(mk_real_int (num_of_string "18038597906312433296"));(* 19, 19 *) (mk_real_int (num_of_string "20959328223742049152")),(mk_real_int (num_of_string "21595284432295804230"));(* 19, 19 *) (mk_real_int (num_of_string "34839745554275565860")),(mk_real_int (num_of_string "27666930136205473575"));(* 19, 19 *) (mk_real_int (num_of_string "18148005270634314735")),(mk_real_int (num_of_string "20922461477993382736"));(* 19, 19 *) (mk_real_int (num_of_string "34823205431082330526")),(mk_real_int (num_of_string "35633283730567513870"));(* 19, 19 *) (mk_real_int (num_of_string "21193870188627553032")),(mk_real_int (num_of_string "29351738040767819600"));(* 19, 19 *) (mk_real_int (num_of_string "30455341615295874068")),(mk_real_int (num_of_string "20117684297361308196"));(* 19, 19 *) (mk_real_int (num_of_string "24509729858501569539")),(mk_real_int (num_of_string "18946984426713251370"));(* 19, 19 *) (mk_real_int (num_of_string "22318280476914474624")),(mk_real_int (num_of_string "31543831574588562669"));(* 19, 19 *) (mk_real_int (num_of_string "32876829237972386205")),(mk_real_int (num_of_string "17641064336296436992"));(* 19, 19 *) (mk_real_int (num_of_string "16136845849044126976")),(mk_real_int (num_of_string "12024977431884627056"));(* 19, 19 *) (mk_real_int (num_of_string "29591382097243846726")),(mk_real_int (num_of_string "21761958033105990414"));(* 19, 19 *) (mk_real_int (num_of_string "34921852586595252300")),(mk_real_int (num_of_string "36338215165810686975"));(* 19, 19 *) (mk_real_int (num_of_string "31575698644415464759")),(mk_real_int (num_of_string "36821630712231475000"));(* 19, 19 *) (mk_real_int (num_of_string "29374461955377970200")),(mk_real_int (num_of_string "19295396972157570858"));(* 19, 19 *) (mk_real_int (num_of_string "23551080882586423254")),(mk_real_int (num_of_string "26021043057968355045"));(* 19, 19 *) (mk_real_int (num_of_string "24509669884122627930")),(mk_real_int (num_of_string "22765660249132309080"));(* 19, 19 *) (mk_real_int (num_of_string "27502589129746076940")),(mk_real_int (num_of_string "26600162897418547866"));(* 19, 19 *) (mk_real_int (num_of_string "21197378314893792000")),(mk_real_int (num_of_string "14999401956071515400"));(* 19, 19 *) (mk_real_int (num_of_string "31726683382172574686")),(mk_real_int (num_of_string "24156318532958805215"));(* 19, 19 *) (mk_real_int (num_of_string "18516751632574286861")),(mk_real_int (num_of_string "16464444229019918560"));(* 19, 19 *) (mk_real_int (num_of_string "23282705218191493228")),(mk_real_int (num_of_string "26808540544890302352"));(* 19, 19 *) (mk_real_int (num_of_string "24224375458191889167")),(mk_real_int (num_of_string "40426735523114963660"));(* 19, 19 *) (mk_real_int (num_of_string "24729832065754451845")),(mk_real_int (num_of_string "40256825431310309338"));(* 19, 19 *) (mk_real_int (num_of_string "24532845531534315261")),(mk_real_int (num_of_string "24997986586900784424"));(* 19, 19 *) (mk_real_int (num_of_string "21455661113055105255")),(mk_real_int (num_of_string "23737870065937842496"));(* 19, 19 *) (mk_real_int (num_of_string "24503286503879146700")),(mk_real_int (num_of_string "18885353652616094226"));(* 19, 19 *) (mk_real_int (num_of_string "15813703053057549222")),(mk_real_int (num_of_string "18659272566817945920"));(* 19, 19 *) (mk_real_int (num_of_string "21919386273746184256")),(mk_real_int (num_of_string "24410507728974085290"));(* 19, 19 *) (mk_real_int (num_of_string "35351640769827902388")),(mk_real_int (num_of_string "35166919009549550091"));(* 19, 19 *) (mk_real_int (num_of_string "12403084155904289056")),(mk_real_int (num_of_string "38587630402981230956"));(* 19, 19 *) (mk_real_int (num_of_string "18357829687152643930")),(mk_real_int (num_of_string "22525579055020439794"));(* 19, 19 *) (mk_real_int (num_of_string "21858957799970582577")),(mk_real_int (num_of_string "23238374947547825384"));(* 19, 19 *) (mk_real_int (num_of_string "20065513266972118044")),(mk_real_int (num_of_string "18068565091568894045"));(* 19, 19 *) (mk_real_int (num_of_string "15661850298963786720")),(mk_real_int (num_of_string "24517170026531564250"));(* 19, 19 *) (mk_real_int (num_of_string "25303340338657447968")),(mk_real_int (num_of_string "21935617186639158288"));(* 19, 19 *) (mk_real_int (num_of_string "33081651678310792722")),(mk_real_int (num_of_string "13827540706109639894"));(* 19, 19 *) (mk_real_int (num_of_string "16335537411557237610")),(mk_real_int (num_of_string "23561533332977778831"));(* 19, 19 *) (mk_real_int (num_of_string "28233169332902303880")),(mk_real_int (num_of_string "15695575969530806712"));(* 19, 19 *) (mk_real_int (num_of_string "21011542803365853618")),(mk_real_int (num_of_string "38561936241481526720"));(* 19, 19 *) (mk_real_int (num_of_string "18827391882792107560")),(mk_real_int (num_of_string "26745459634561440762"));(* 19, 19 *) (mk_real_int (num_of_string "23590842498659226450")),(mk_real_int (num_of_string "23742472686542216068"));(* 19, 19 *) (mk_real_int (num_of_string "32665890285705956389")),(mk_real_int (num_of_string "37728670265050820880"));(* 19, 19 *) (mk_real_int (num_of_string "27576476991159319850")),(mk_real_int (num_of_string "32543750898982323880"));(* 19, 19 *) (mk_real_int (num_of_string "22766986312687886698")),(mk_real_int (num_of_string "19774910912344837843"));(* 19, 19 *) (mk_real_int (num_of_string "42511566901090363692")),(mk_real_int (num_of_string "24598422411097651215"));(* 19, 19 *) (mk_real_int (num_of_string "28192701133435584702")),(mk_real_int (num_of_string "12553678556632687936"));(* 19, 19 *) (mk_real_int (num_of_string "32221328176975547940")),(mk_real_int (num_of_string "17102144059749226368"));(* 19, 19 *) (mk_real_int (num_of_string "28862640072739190773")),(mk_real_int (num_of_string "28684249091778024250"));(* 19, 19 *) (mk_real_int (num_of_string "18566567717553172680")),(mk_real_int (num_of_string "13946885838781744420"));(* 19, 19 *) (mk_real_int (num_of_string "19114401628089157500")),(mk_real_int (num_of_string "20162167293220081591"));(* 19, 19 *) (mk_real_int (num_of_string "19851583929739884124")),(mk_real_int (num_of_string "27857155807442616160"));(* 19, 19 *) (mk_real_int (num_of_string "17972046906509828649")),(mk_real_int (num_of_string "20570599301922216767"));(* 19, 19 *) (mk_real_int (num_of_string "21617151726877793163")),(mk_real_int (num_of_string "16346621830867942108"));(* 19, 19 *) (mk_real_int (num_of_string "19069024794172757888")),(mk_real_int (num_of_string "15223494796378903056"));(* 19, 19 *) (mk_real_int (num_of_string "20516178072197899047")),(mk_real_int (num_of_string "29671516061196220134"));(* 19, 19 *) (mk_real_int (num_of_string "20762847548821657125")),(mk_real_int (num_of_string "17343373910494965080"));(* 19, 19 *) (mk_real_int (num_of_string "20618467076378920320")),(mk_real_int (num_of_string "21135634926579888000"));(* 19, 19 *) (mk_real_int (num_of_string "28783602679901071002")),(mk_real_int (num_of_string "30607469559621331036"));(* 19, 19 *) (mk_real_int (num_of_string "34952750589763145172")),(mk_real_int (num_of_string "20773387779415296718"));(* 19, 19 *) (mk_real_int (num_of_string "21663700659878912052")),(mk_real_int (num_of_string "31738022168048514120"));(* 19, 19 *) (mk_real_int (num_of_string "15067586704074398450")),(mk_real_int (num_of_string "39393741347756167548"));(* 19, 19 *) (mk_real_int (num_of_string "25856646965954567103")),(mk_real_int (num_of_string "24101111445972077902"));(* 19, 19 *) (mk_real_int (num_of_string "22969508248904385861")),(mk_real_int (num_of_string "17853062093770904110"));(* 19, 19 *) (mk_real_int (num_of_string "23593250100320878131")),(mk_real_int (num_of_string "34052417430591296880"));(* 19, 19 *) (mk_real_int (num_of_string "25574140422098661888")),(mk_real_int (num_of_string "32110910233566469272"));(* 19, 19 *) (mk_real_int (num_of_string "27312149886651808101")),(mk_real_int (num_of_string "31819075231891378706"));(* 19, 19 *) (mk_real_int (num_of_string "20228868063451733400")),(mk_real_int (num_of_string "22767237113306329688"));(* 19, 19 *) (mk_real_int (num_of_string "29000691323467414012")),(mk_real_int (num_of_string "29688670921350339184"));(* 19, 19 *) (mk_real_int (num_of_string "18149199099000179925")),(mk_real_int (num_of_string "13176519098165803292"));(* 19, 19 *) (mk_real_int (num_of_string "20895657111240075120")),(mk_real_int (num_of_string "30387247130400193110"));(* 19, 19 *) (mk_real_int (num_of_string "18041726745700697028")),(mk_real_int (num_of_string "16578817088051910560"));(* 19, 19 *) (mk_real_int (num_of_string "18724010569156142976")),(mk_real_int (num_of_string "30283190447828916290"));(* 19, 19 *) (mk_real_int (num_of_string "21485532037632035230")),(mk_real_int (num_of_string "21228585073275008000"));(* 19, 19 *) (mk_real_int (num_of_string "15441576730070721120")),(mk_real_int (num_of_string "23203789204405517796"));(* 19, 19 *) (mk_real_int (num_of_string "23980580918626336290")),(mk_real_int (num_of_string "27884855142978774336"));(* 19, 19 *) (mk_real_int (num_of_string "24458494418868606734")),(mk_real_int (num_of_string "31956362945544922500"));(* 19, 19 *) (mk_real_int (num_of_string "17543007688597081064")),(mk_real_int (num_of_string "29665170852355203858"));(* 19, 19 *) (mk_real_int (num_of_string "23391008316914182692")),(mk_real_int (num_of_string "21740149625097397395"));(* 19, 19 *) (mk_real_int (num_of_string "17968200652006529540")),(mk_real_int (num_of_string "15280161176449006882"));(* 19, 19 *) (mk_real_int (num_of_string "18526668902915813145")),(mk_real_int (num_of_string "25725618717964397320"));(* 19, 19 *) (mk_real_int (num_of_string "37631433263277548343")),(mk_real_int (num_of_string "24302775082118358980"));(* 19, 19 *) (mk_real_int (num_of_string "16234385580921780712")),(mk_real_int (num_of_string "19115360328189971538"));(* 19, 19 *) (mk_real_int (num_of_string "38862409563677772864")),(mk_real_int (num_of_string "19997602817828134268"));(* 19, 19 *) (mk_real_int (num_of_string "14454331638446689220")),(mk_real_int (num_of_string "19903070754044856356"));(* 19, 19 *) (mk_real_int (num_of_string "32907022481777039255")),(mk_real_int (num_of_string "27067046447658850864"));(* 19, 19 *) (mk_real_int (num_of_string "17889493514926932547")),(mk_real_int (num_of_string "34423976486808398336"));(* 19, 19 *) (mk_real_int (num_of_string "30173428453947449220")),(mk_real_int (num_of_string "13570298312770941324"));(* 19, 19 *) (mk_real_int (num_of_string "21159384420414011585")),(mk_real_int (num_of_string "38204222449892118620"));(* 19, 19 *) (mk_real_int (num_of_string "29252463947900339168")),(mk_real_int (num_of_string "18824370595084099045"));(* 19, 19 *) (mk_real_int (num_of_string "31592010113233650476")),(mk_real_int (num_of_string "16593326100162570330"));(* 19, 19 *) (mk_real_int (num_of_string "29154597430593861512")),(mk_real_int (num_of_string "26803434626433084312"));(* 19, 19 *) (mk_real_int (num_of_string "21021652073815640951")),(mk_real_int (num_of_string "20942684826217401632"));(* 19, 19 *) (mk_real_int (num_of_string "37639824290981401104")),(mk_real_int (num_of_string "24256345483251875620"));(* 19, 19 *) (mk_real_int (num_of_string "22611435485892780296")),(mk_real_int (num_of_string "18571118204886449664"));(* 19, 19 *) (mk_real_int (num_of_string "23344095849474622365")),(mk_real_int (num_of_string "22711490771468691291"));(* 19, 19 *) (mk_real_int (num_of_string "21022861777868756025")),(mk_real_int (num_of_string "23592319748734711491"));(* 19, 19 *) (mk_real_int (num_of_string "33550375893316112226")),(mk_real_int (num_of_string "12443890794364870566"));(* 19, 19 *) (mk_real_int (num_of_string "31091426703633150426")),(mk_real_int (num_of_string "18683078954341495485"));(* 19, 19 *) (mk_real_int (num_of_string "22029307894570906215")),(mk_real_int (num_of_string "29180187263806709438"));(* 19, 19 *) (mk_real_int (num_of_string "17313467714242277160")),(mk_real_int (num_of_string "21175391909182828900"));(* 19, 19 *) (mk_real_int (num_of_string "20886644587278159228")),(mk_real_int (num_of_string "24308394289659303439"));(* 19, 19 *) (mk_real_int (num_of_string "17377934872656963000")),(mk_real_int (num_of_string "19694851222645694865"));(* 19, 19 *) (mk_real_int (num_of_string "19531645594108771200")),(mk_real_int (num_of_string "27353687880319154079"));(* 19, 19 *) (mk_real_int (num_of_string "15095517418017230084")),(mk_real_int (num_of_string "24367145327645102598"));(* 19, 19 *) (mk_real_int (num_of_string "30670896409691227140")),(mk_real_int (num_of_string "23282256849070081995"));(* 19, 19 *) (mk_real_int (num_of_string "18058765456197825546")),(mk_real_int (num_of_string "20692670312869565230"));(* 19, 19 *) (mk_real_int (num_of_string "14195656193932143700")),(mk_real_int (num_of_string "28545033381349941060"));(* 19, 19 *) (mk_real_int (num_of_string "17570057243762665488")),(mk_real_int (num_of_string "16610104346969969561"));(* 19, 19 *) (mk_real_int (num_of_string "20380752462050320626")),(mk_real_int (num_of_string "20065344591096659624"));(* 19, 19 *) (mk_real_int (num_of_string "19232092477610461636")),(mk_real_int (num_of_string "25973000999163902464"));(* 19, 19 *) (mk_real_int (num_of_string "24995182068165660692")),(mk_real_int (num_of_string "19286366253170364854"));(* 19, 19 *) (mk_real_int (num_of_string "35445021594672206286")),(mk_real_int (num_of_string "29931442569965248026"));(* 19, 19 *) (mk_real_int (num_of_string "29117447130800545495")),(mk_real_int (num_of_string "22155053961808404120"));(* 19, 19 *) (mk_real_int (num_of_string "27742764056591265990")),(mk_real_int (num_of_string "18980076482308156908"));(* 19, 19 *) (mk_real_int (num_of_string "16966438935537374250")),(mk_real_int (num_of_string "29178181123590289703"));(* 19, 19 *) (mk_real_int (num_of_string "12053340226144389282")),(mk_real_int (num_of_string "33855812770349013290"));(* 19, 19 *) (mk_real_int (num_of_string "18170280513695587585")),(mk_real_int (num_of_string "25754112139586535408"));(* 19, 19 *) (mk_real_int (num_of_string "18186168554789042808")),(mk_real_int (num_of_string "13330016601258737358"));(* 19, 19 *) (mk_real_int (num_of_string "15906969118515146595")),(mk_real_int (num_of_string "22286164457235329244"));(* 19, 19 *) (mk_real_int (num_of_string "21581669523223757508")),(mk_real_int (num_of_string "14562959639504134320"));(* 19, 19 *) (mk_real_int (num_of_string "35482774215702490710")),(mk_real_int (num_of_string "35607133211609937384"));(* 19, 19 *) (mk_real_int (num_of_string "16209989142320107772")),(mk_real_int (num_of_string "22345207211109852927"));(* 19, 19 *) (mk_real_int (num_of_string "21773240177061127744")),(mk_real_int (num_of_string "14433677298971087520"));(* 19, 19 *) (mk_real_int (num_of_string "18936034135085987348")),(mk_real_int (num_of_string "13471466844063717500"));(* 19, 19 *) (mk_real_int (num_of_string "17354745485231552640")),(mk_real_int (num_of_string "18230529179626830000"));(* 19, 19 *) (mk_real_int (num_of_string "19220326678110420720")),(mk_real_int (num_of_string "24737122565887447254"));(* 19, 19 *) (mk_real_int (num_of_string "15259900645808649996")),(mk_real_int (num_of_string "20992671308236571416"));(* 19, 19 *) (mk_real_int (num_of_string "24176218476796561989")),(mk_real_int (num_of_string "21364738248703094784"));(* 19, 19 *) (mk_real_int (num_of_string "20815812501351657768")),(mk_real_int (num_of_string "17048832156482749480"));(* 19, 19 *) (mk_real_int (num_of_string "27210633864901937978")),(mk_real_int (num_of_string "16484565937387436020"));(* 19, 19 *) (mk_real_int (num_of_string "28892013642217754930")),(mk_real_int (num_of_string "17968794754260957508"));(* 19, 19 *) (mk_real_int (num_of_string "20532996895144585137")),(mk_real_int (num_of_string "24178200931553138613"));(* 19, 19 *) (mk_real_int (num_of_string "27344628599778361927")),(mk_real_int (num_of_string "25029824984976538980"));(* 19, 19 *) (mk_real_int (num_of_string "19599776763403286714")),(mk_real_int (num_of_string "22323268951505419260"));(* 19, 19 *) (mk_real_int (num_of_string "28389907471848568800")),(mk_real_int (num_of_string "28274088091656918170"));(* 19, 19 *) (mk_real_int (num_of_string "21166750325965741112")),(mk_real_int (num_of_string "33977726365574968878"));(* 19, 19 *) (mk_real_int (num_of_string "24670303706391574110")),(mk_real_int (num_of_string "25971856095244184576"));(* 19, 19 *) (mk_real_int (num_of_string "17277683789911756959")),(mk_real_int (num_of_string "27229795019899182700"));(* 19, 19 *) (mk_real_int (num_of_string "21402593447934487734")),(mk_real_int (num_of_string "21687111141911205408"));(* 19, 19 *) (mk_real_int (num_of_string "29078686775718432160")),(mk_real_int (num_of_string "25171811110690446323"));(* 19, 19 *) (mk_real_int (num_of_string "27126072922588956756")),(mk_real_int (num_of_string "23950321867875466360"));(* 19, 19 *) (mk_real_int (num_of_string "33305771987516661017")),(mk_real_int (num_of_string "24468524500330552290"));(* 19, 19 *) (mk_real_int (num_of_string "27921131753019252990")),(mk_real_int (num_of_string "26394242937943914528"));(* 19, 19 *) (mk_real_int (num_of_string "27045834098608407148")),(mk_real_int (num_of_string "26617239134096634870"));(* 19, 19 *) (mk_real_int (num_of_string "17827874715790694522")),(mk_real_int (num_of_string "19275397617563667855"));(* 19, 19 *) (mk_real_int (num_of_string "15522028285332619974")),(mk_real_int (num_of_string "33087542953825461387"));(* 19, 19 *) (mk_real_int (num_of_string "19684113097994867522")),(mk_real_int (num_of_string "30361068119675378052"));(* 19, 19 *) (mk_real_int (num_of_string "17777766080187911952")),(mk_real_int (num_of_string "28304071546000928832"));(* 19, 19 *) (mk_real_int (num_of_string "24701740819723327976")),(mk_real_int (num_of_string "23249426930623449963"));(* 19, 19 *) (mk_real_int (num_of_string "15626383485965048225")),(mk_real_int (num_of_string "24610090203093475916"));(* 19, 19 *) (mk_real_int (num_of_string "19912840531332936836")),(mk_real_int (num_of_string "36655821249221511260"));(* 19, 19 *) (mk_real_int (num_of_string "23457936080048044960")),(mk_real_int (num_of_string "31405259545579645440"));(* 19, 19 *) (mk_real_int (num_of_string "26162251126555051728")),(mk_real_int (num_of_string "34953126054172656682"));(* 19, 19 *) (mk_real_int (num_of_string "20947243755607552460")),(mk_real_int (num_of_string "33040622577818480108"));(* 19, 19 *) (mk_real_int (num_of_string "14078893498675132050")),(mk_real_int (num_of_string "26209061871934627576"));(* 19, 19 *) (mk_real_int (num_of_string "17874561660889509378")),(mk_real_int (num_of_string "34995431734586687364"));(* 19, 19 *) (mk_real_int (num_of_string "19722509821913233335")),(mk_real_int (num_of_string "26216971740241668540"));(* 19, 19 *) (mk_real_int (num_of_string "18344244271878932440")),(mk_real_int (num_of_string "23392767028792280273"));(* 19, 19 *) (mk_real_int (num_of_string "28032454510825810122")),(mk_real_int (num_of_string "25999562749903501528"));(* 19, 19 *) (mk_real_int (num_of_string "34663056879982884584")),(mk_real_int (num_of_string "28928679338965278510"));(* 19, 19 *) (mk_real_int (num_of_string "16467213935942451990")),(mk_real_int (num_of_string "20701325711559050712"));(* 19, 19 *) (mk_real_int (num_of_string "20958348605371005444")),(mk_real_int (num_of_string "20693907454225623640"));(* 19, 19 *) (mk_real_int (num_of_string "22991639050824817560")),(mk_real_int (num_of_string "22831987758755124345"));(* 19, 19 *) (mk_real_int (num_of_string "18963489141520879307")),(mk_real_int (num_of_string "31099308534703877160"));(* 19, 19 *) (mk_real_int (num_of_string "28750492385478360200")),(mk_real_int (num_of_string "25020044018647608777"));(* 19, 19 *) (mk_real_int (num_of_string "33629559216526149096")),(mk_real_int (num_of_string "20567895169536088396"));(* 19, 19 *) (mk_real_int (num_of_string "28183874476069732794")),(mk_real_int (num_of_string "23063923513337985905"));(* 19, 19 *) (mk_real_int (num_of_string "31627307797642771830")),(mk_real_int (num_of_string "28106774188626583241"));(* 19, 19 *) (mk_real_int (num_of_string "12952044016828521220")),(mk_real_int (num_of_string "25641346373459661163"));(* 19, 19 *) (mk_real_int (num_of_string "21103192133019558144")),(mk_real_int (num_of_string "15481220670131773128"));(* 19, 19 *) (mk_real_int (num_of_string "41898102151306065214")),(mk_real_int (num_of_string "29960774778839900248"));(* 19, 19 *) (mk_real_int (num_of_string "15034303370302387325")),(mk_real_int (num_of_string "12300353092863620928"));(* 19, 19 *) (mk_real_int (num_of_string "35528629318596256700")),(mk_real_int (num_of_string "21920093424238797216"));(* 19, 19 *) (mk_real_int (num_of_string "35117743435591618131")),(mk_real_int (num_of_string "28003743443031332900"));(* 19, 19 *) (mk_real_int (num_of_string "37066810033626111365")),(mk_real_int (num_of_string "36090507772144342506"));(* 19, 19 *) (mk_real_int (num_of_string "34724490290216914275")),(mk_real_int (num_of_string "17161689223016674028"));(* 19, 19 *) (mk_real_int (num_of_string "21219950840232526800")),(mk_real_int (num_of_string "18415045991539750058"));(* 19, 19 *) (mk_real_int (num_of_string "37759705646207842143")),(mk_real_int (num_of_string "20577665293957461459"));(* 19, 19 *) (mk_real_int (num_of_string "22563412948386039015")),(mk_real_int (num_of_string "20175884350710156552"));(* 19, 19 *) (mk_real_int (num_of_string "18212580186806832640")),(mk_real_int (num_of_string "15216977162738800735"));(* 19, 19 *) (mk_real_int (num_of_string "25940566047008574940")),(mk_real_int (num_of_string "31634171328449180634"));(* 19, 19 *) (mk_real_int (num_of_string "18897775995233865620")),(mk_real_int (num_of_string "34790823789921925902"));(* 19, 19 *) (mk_real_int (num_of_string "29165832446308109530")),(mk_real_int (num_of_string "23630863338677843270"));(* 19, 19 *) (mk_real_int (num_of_string "18526482687065515173")),(mk_real_int (num_of_string "30497661154671633351"));(* 19, 19 *) (mk_real_int (num_of_string "12613587919218559196")),(mk_real_int (num_of_string "30148283770248797120"));(* 19, 19 *) (mk_real_int (num_of_string "25043255540874981223")),(mk_real_int (num_of_string "28689590854105105210"));(* 19, 19 *) (mk_real_int (num_of_string "35322221600815909474")),(mk_real_int (num_of_string "18051552726004570256"));(* 19, 19 *) (mk_real_int (num_of_string "29343576262735977704")),(mk_real_int (num_of_string "35294058361966766736"));(* 19, 19 *) (mk_real_int (num_of_string "20516884598322759438")),(mk_real_int (num_of_string "19320319006336470122"));(* 19, 19 *) (mk_real_int (num_of_string "31267282633928547844")),(mk_real_int (num_of_string "35861154558309369366"));(* 19, 19 *) (mk_real_int (num_of_string "27550689559525622094")),(mk_real_int (num_of_string "26280923396917494393"));(* 19, 19 *) (mk_real_int (num_of_string "18145348381422887130")),(mk_real_int (num_of_string "26184297950690421630"));(* 19, 19 *) (mk_real_int (num_of_string "15422719373259310684")),(mk_real_int (num_of_string "33476564191573589009"));(* 19, 19 *) (mk_real_int (num_of_string "32556607704984662112")),(mk_real_int (num_of_string "25630833834504104877"));(* 19, 19 *) (mk_real_int (num_of_string "28594665725854332522")),(mk_real_int (num_of_string "14327634629606891549"));(* 19, 19 *) (mk_real_int (num_of_string "22365449743008243344")),(mk_real_int (num_of_string "34684581374063387745"));(* 19, 19 *) (mk_real_int (num_of_string "40236644587287275886")),(mk_real_int (num_of_string "20781153690060239586"));(* 19, 19 *) (mk_real_int (num_of_string "18610141729705037325")),(mk_real_int (num_of_string "13176319433599394314"));(* 19, 19 *) (mk_real_int (num_of_string "27542384672833362156")),(mk_real_int (num_of_string "19682637014151234816"));(* 19, 19 *) (mk_real_int (num_of_string "23708318483042944718")),(mk_real_int (num_of_string "31868852818940076324"));(* 19, 19 *) (mk_real_int (num_of_string "29843340901941755540")),(mk_real_int (num_of_string "26706282763966833720"));(* 19, 19 *) (mk_real_int (num_of_string "34001500222865547427")),(mk_real_int (num_of_string "22507086852821019548"));(* 19, 19 *) (mk_real_int (num_of_string "35842699595817676980")),(mk_real_int (num_of_string "23728872105232017020"));(* 19, 19 *) (mk_real_int (num_of_string "19828772840263304225")),(mk_real_int (num_of_string "24823180329320899372"));(* 19, 19 *) (mk_real_int (num_of_string "32553484226000737560")),(mk_real_int (num_of_string "18147481397960764157"));(* 19, 19 *) (mk_real_int (num_of_string "21676364112776796632")),(mk_real_int (num_of_string "15041594447000182116"));(* 19, 19 *) (mk_real_int (num_of_string "16447285630014439695")),(mk_real_int (num_of_string "17551431940450573440"));(* 19, 19 *) (mk_real_int (num_of_string "16808111208105559936")),(mk_real_int (num_of_string "25772541405183852125"));(* 19, 19 *) (mk_real_int (num_of_string "24874720927323956766")),(mk_real_int (num_of_string "16990049119982136396"));(* 19, 19 *) (mk_real_int (num_of_string "11891814757647978065")),(mk_real_int (num_of_string "21732289830190325375"));(* 19, 19 *) (mk_real_int (num_of_string "23456784257886497078")),(mk_real_int (num_of_string "17877286236876984665"));(* 19, 19 *) (mk_real_int (num_of_string "28949427753858318278")),(mk_real_int (num_of_string "23397956039203959213"));(* 19, 19 *) (mk_real_int (num_of_string "15179451784142189390")),(mk_real_int (num_of_string "21984582213447723562"));(* 19, 19 *) (mk_real_int (num_of_string "16899841421205218575")),(mk_real_int (num_of_string "16669908767746994760"));(* 19, 19 *) (mk_real_int (num_of_string "28223003585259342288")),(mk_real_int (num_of_string "29797405189398803880"));(* 19, 19 *) (mk_real_int (num_of_string "21507545708574622752")),(mk_real_int (num_of_string "25975447924780473350"));(* 19, 19 *) (mk_real_int (num_of_string "26205609252560085095")),(mk_real_int (num_of_string "24731479066832761608"));(* 19, 19 *) (mk_real_int (num_of_string "27985839086539151840")),(mk_real_int (num_of_string "17671559399794983980"));(* 19, 19 *) (mk_real_int (num_of_string "15895356965370990107")),(mk_real_int (num_of_string "22632390546596123590"));(* 19, 19 *) (mk_real_int (num_of_string "25525045286361632286")),(mk_real_int (num_of_string "27987171825415936826"));(* 19, 19 *) (mk_real_int (num_of_string "20293758261542977629")),(mk_real_int (num_of_string "21813473539208521940"));(* 19, 19 *) (mk_real_int (num_of_string "17572261936650012042")),(mk_real_int (num_of_string "30624608353547807962"));(* 19, 19 *) (mk_real_int (num_of_string "20956472842282125555")),(mk_real_int (num_of_string "21692216994371491480"));(* 19, 19 *) (mk_real_int (num_of_string "16225444592257846308")),(mk_real_int (num_of_string "27965542798181046135"));(* 19, 19 *) (mk_real_int (num_of_string "15036010767021545180")),(mk_real_int (num_of_string "20929192536310667202"));(* 19, 19 *) (mk_real_int (num_of_string "22616206252016347080")),(mk_real_int (num_of_string "18021113039004339000"));(* 19, 19 *) (mk_real_int (num_of_string "31068739159544436900")),(mk_real_int (num_of_string "21403839397870847225"));(* 19, 19 *) (mk_real_int (num_of_string "18831386543112750915")),(mk_real_int (num_of_string "30980340403688096080"));(* 19, 19 *) (mk_real_int (num_of_string "15652020837335436840")),(mk_real_int (num_of_string "19970010932973331923"));(* 19, 19 *) (mk_real_int (num_of_string "19286980805687969286")),(mk_real_int (num_of_string "19368977873383819989"));(* 19, 19 *) (mk_real_int (num_of_string "20924342284695386394")),(mk_real_int (num_of_string "17027708934231526300"));(* 19, 19 *) (mk_real_int (num_of_string "11910339418519621937")),(mk_real_int (num_of_string "20557989760266093520"));(* 19, 19 *) (mk_real_int (num_of_string "20563150893831517356")),(mk_real_int (num_of_string "22273400428480720640"));(* 19, 19 *) (mk_real_int (num_of_string "19846853780140487683")),(mk_real_int (num_of_string "19693815906448338072"));(* 19, 19 *) (mk_real_int (num_of_string "21914899759078112226")),(mk_real_int (num_of_string "18879844193693089464"));(* 19, 19 *) (mk_real_int (num_of_string "30996332483375752196")),(mk_real_int (num_of_string "22054403955108551818"));(* 19, 19 *) (mk_real_int (num_of_string "42098132858377824140")),(mk_real_int (num_of_string "16499240709793965860"));(* 19, 19 *) (mk_real_int (num_of_string "23438588359708245625")),(mk_real_int (num_of_string "27294632478354169841"));(* 19, 19 *) (mk_real_int (num_of_string "20362447198571333625")),(mk_real_int (num_of_string "19778322300291670500"));(* 19, 19 *) (mk_real_int (num_of_string "28984118193464681808")),(mk_real_int (num_of_string "18615777827849879292"));(* 19, 19 *) (mk_real_int (num_of_string "37377977572124788555")),(mk_real_int (num_of_string "21200286739730208957"));(* 19, 19 *) (mk_real_int (num_of_string "34034199364359205396")),(mk_real_int (num_of_string "19135486806945622036"));(* 19, 19 *) (mk_real_int (num_of_string "26574092226113406975")),(mk_real_int (num_of_string "27364197794452862959"));(* 19, 19 *) (mk_real_int (num_of_string "16628062295952432512")),(mk_real_int (num_of_string "14090157723953142975"));(* 19, 19 *) (mk_real_int (num_of_string "18674051343439457273")),(mk_real_int (num_of_string "40668265006554954780"));(* 19, 19 *) (mk_real_int (num_of_string "15683851921081656312")),(mk_real_int (num_of_string "33380019479297179854"));(* 19, 19 *) (mk_real_int (num_of_string "18495271454633589242")),(mk_real_int (num_of_string "28345198646120300208"));(* 19, 19 *) (mk_real_int (num_of_string "30790102737490098464")),(mk_real_int (num_of_string "29434253824397078316"));(* 19, 19 *) (mk_real_int (num_of_string "23301763729611442768")),(mk_real_int (num_of_string "17515245159724128817"));(* 19, 19 *) (mk_real_int (num_of_string "26471663763843548250")),(mk_real_int (num_of_string "25905254090861207216"));(* 19, 19 *) (mk_real_int (num_of_string "26333740460139536160")),(mk_real_int (num_of_string "19732481027856899896"));(* 19, 19 *) (mk_real_int (num_of_string "27690365539057347720")),(mk_real_int (num_of_string "27986997261805128096"));(* 19, 19 *) (mk_real_int (num_of_string "31402837346152004964")),(mk_real_int (num_of_string "16087997506814935504"));(* 19, 19 *) (mk_real_int (num_of_string "12482908031899925334")),(mk_real_int (num_of_string "12074534421506609580"));(* 19, 19 *) (mk_real_int (num_of_string "16865054989510033130")),(mk_real_int (num_of_string "25311479139287101200"));(* 19, 19 *) (mk_real_int (num_of_string "26701144789330873466")),(mk_real_int (num_of_string "15162250273970036160"));(* 19, 19 *) (mk_real_int (num_of_string "31614871463289433440")),(mk_real_int (num_of_string "19718429491535357275"));(* 19, 19 *) (mk_real_int (num_of_string "29440626033317497394")),(mk_real_int (num_of_string "38864899869119902688"));(* 19, 19 *) (mk_real_int (num_of_string "22314351305843742420")),(mk_real_int (num_of_string "28033308342251155515"));(* 19, 19 *) (mk_real_int (num_of_string "22560438337513844581")),(mk_real_int (num_of_string "17835311046174804644"));(* 19, 19 *) (mk_real_int (num_of_string "24449292854132620232")),(mk_real_int (num_of_string "21354423440548669900"));(* 19, 19 *) (mk_real_int (num_of_string "33961168769518178694")),(mk_real_int (num_of_string "28539147237330071100"));(* 19, 19 *) (mk_real_int (num_of_string "29110217637976409176")),(mk_real_int (num_of_string "21219378231222655198"));(* 19, 19 *) (mk_real_int (num_of_string "22161141551634969510")),(mk_real_int (num_of_string "36490836787647976811"));(* 19, 19 *) (mk_real_int (num_of_string "17314846198769732030")),(mk_real_int (num_of_string "38797942951815097776"));(* 19, 19 *) (mk_real_int (num_of_string "24625748700107882800")),(mk_real_int (num_of_string "28401162576451413760"));(* 19, 19 *) (mk_real_int (num_of_string "19069497830518416490")),(mk_real_int (num_of_string "28075529187933913015"));(* 19, 19 *) (mk_real_int (num_of_string "19387086820405057468")),(mk_real_int (num_of_string "17945187196181865180"));(* 19, 19 *) (mk_real_int (num_of_string "38731339272095791002")),(mk_real_int (num_of_string "38869445422362906780"));(* 19, 19 *) (mk_real_int (num_of_string "21322779799938168904")),(mk_real_int (num_of_string "28955320941001624609"));(* 19, 19 *) (mk_real_int (num_of_string "35997371074004079740")),(mk_real_int (num_of_string "14589487651792161460"));(* 19, 19 *) (mk_real_int (num_of_string "35840710489786105024")),(mk_real_int (num_of_string "22271823002327442720"));(* 19, 19 *) (mk_real_int (num_of_string "12093770197792685226")),(mk_real_int (num_of_string "36347297260764411240"));(* 19, 19 *) (mk_real_int (num_of_string "13816202228225201772")),(mk_real_int (num_of_string "24125978880493300008"));(* 19, 19 *) (mk_real_int (num_of_string "19296203926430636205")),(mk_real_int (num_of_string "22540604625533767256"));(* 19, 19 *) (mk_real_int (num_of_string "37949082883945744170")),(mk_real_int (num_of_string "28090341039491342304"));(* 19, 19 *) (mk_real_int (num_of_string "17140609291250961516")),(mk_real_int (num_of_string "27441105323877719639"));(* 19, 19 *) (mk_real_int (num_of_string "31241110974541698846")),(mk_real_int (num_of_string "21121476357610481204"));(* 19, 19 *) (mk_real_int (num_of_string "32399604181929621714")),(mk_real_int (num_of_string "13101169717074505297"));(* 19, 19 *) (mk_real_int (num_of_string "35135381590831089304")),(mk_real_int (num_of_string "19834393913906561957"));(* 19, 19 *) (mk_real_int (num_of_string "18369289023529407678")),(mk_real_int (num_of_string "30429545112624550860"));(* 19, 19 *) (mk_real_int (num_of_string "16670874718441946772")),(mk_real_int (num_of_string "26800501647391853634"));(* 19, 19 *) (mk_real_int (num_of_string "31693625340511240414")),(mk_real_int (num_of_string "15984710443303034400"));(* 19, 19 *) (mk_real_int (num_of_string "23647195846585175656")),(mk_real_int (num_of_string "25218671587136807472"));(* 19, 19 *) (mk_real_int (num_of_string "25678706922013782384")),(mk_real_int (num_of_string "22322294403582285816"));(* 19, 19 *) (mk_real_int (num_of_string "18465224703401519076")),(mk_real_int (num_of_string "17627942862200919127"));(* 19, 19 *) (mk_real_int (num_of_string "18907559590609795248")),(mk_real_int (num_of_string "20747360802181123198"));(* 19, 19 *) (mk_real_int (num_of_string "27933037182226617408")),(mk_real_int (num_of_string "18543035784393141395"));(* 19, 19 *) (mk_real_int (num_of_string "24019258243865272080")),(mk_real_int (num_of_string "33178761195927571323"));(* 19, 19 *) (mk_real_int (num_of_string "15526718194575053422")),(mk_real_int (num_of_string "26953857246622990783"));(* 19, 19 *) (mk_real_int (num_of_string "34447034474573944047")),(mk_real_int (num_of_string "32484264642048457392"));(* 19, 19 *) (mk_real_int (num_of_string "14757200260959769910")),(mk_real_int (num_of_string "13050745606135584468"));(* 19, 19 *) (mk_real_int (num_of_string "39286505752254599839")),(mk_real_int (num_of_string "29845651254317409797"));(* 19, 19 *) (mk_real_int (num_of_string "39547531196479139460")),(mk_real_int (num_of_string "35009514400119365799"));(* 19, 19 *) (mk_real_int (num_of_string "16953430526985040110")),(mk_real_int (num_of_string "18324985039305335369"));(* 19, 19 *) (mk_real_int (num_of_string "16027361749560866298")),(mk_real_int (num_of_string "18416945279451047175"));(* 19, 19 *) (mk_real_int (num_of_string "26148109550447514784")),(mk_real_int (num_of_string "19289372172792584016"));(* 19, 19 *) (mk_real_int (num_of_string "30121263740432215296")),(mk_real_int (num_of_string "23845559370533947464"));(* 19, 19 *) (mk_real_int (num_of_string "20755604343228731625")),(mk_real_int (num_of_string "18564483599982367707"));(* 19, 19 *) (mk_real_int (num_of_string "20857226330656349887")),(mk_real_int (num_of_string "21785221658085316970"));(* 19, 19 *) (mk_real_int (num_of_string "36394745648335822165")),(mk_real_int (num_of_string "28299888218909212587"));(* 19, 19 *) (mk_real_int (num_of_string "24296453070147447552")),(mk_real_int (num_of_string "36145798268757190156"));(* 19, 19 *) (mk_real_int (num_of_string "30808120739474498035")),(mk_real_int (num_of_string "36062740403311556880"));(* 19, 19 *) (mk_real_int (num_of_string "20005790813286604612")),(mk_real_int (num_of_string "34374435669861218162"));(* 19, 19 *) (mk_real_int (num_of_string "22903292103178501872")),(mk_real_int (num_of_string "22858582701377320359"));(* 19, 19 *) (mk_real_int (num_of_string "14643627693160703600")),(mk_real_int (num_of_string "38413837964106063360"));(* 19, 19 *) (mk_real_int (num_of_string "29319377725551576960")),(mk_real_int (num_of_string "36328152133226218496"));(* 19, 19 *) (mk_real_int (num_of_string "20146761151355475648")),(mk_real_int (num_of_string "24024887138121953028"));(* 19, 19 *) (mk_real_int (num_of_string "37522875010188929405")),(mk_real_int (num_of_string "22815604137021047352"));(* 19, 19 *) (mk_real_int (num_of_string "14713629418630219550")),(mk_real_int (num_of_string "19406934189903902400"));(* 19, 19 *) (mk_real_int (num_of_string "34497818175869545948")),(mk_real_int (num_of_string "17040707895650386112"));(* 19, 19 *) (mk_real_int (num_of_string "26235226395971030130")),(mk_real_int (num_of_string "28895402157789258982"));(* 19, 19 *) (mk_real_int (num_of_string "19461468255659542112")),(mk_real_int (num_of_string "23446073393084060268"));(* 19, 19 *) (mk_real_int (num_of_string "23891196715991283591")),(mk_real_int (num_of_string "28130785491678816705"));(* 19, 19 *) (mk_real_int (num_of_string "13236126403087653516")),(mk_real_int (num_of_string "16883664536085428312"));(* 19, 19 *) (mk_real_int (num_of_string "21179869037384128566")),(mk_real_int (num_of_string "21666713728407223905"));(* 19, 19 *) (mk_real_int (num_of_string "30727938578510315406")),(mk_real_int (num_of_string "28888551296934550650"));(* 19, 19 *) (mk_real_int (num_of_string "17243366571928325763")),(mk_real_int (num_of_string "39610641731888216385"));(* 19, 19 *) (mk_real_int (num_of_string "24968455904351066426")),(mk_real_int (num_of_string "28013375780368531014"));(* 19, 19 *) (mk_real_int (num_of_string "18498472021224497984")),(mk_real_int (num_of_string "30928160069849654304"));(* 19, 19 *) (mk_real_int (num_of_string "16146451863124230318")),(mk_real_int (num_of_string "17787234799872446656"));(* 19, 19 *) (mk_real_int (num_of_string "19602965929204599040")),(mk_real_int (num_of_string "31084352144430113144"));(* 19, 19 *) (mk_real_int (num_of_string "21166945185366868096")),(mk_real_int (num_of_string "25347005849926191805"));(* 19, 19 *) (mk_real_int (num_of_string "25593028666691249236")),(mk_real_int (num_of_string "33168047080363214118"));(* 19, 19 *) (mk_real_int (num_of_string "40120278827846512900")),(mk_real_int (num_of_string "19171281054163002919"));(* 19, 19 *) (mk_real_int (num_of_string "27786996889090894774")),(mk_real_int (num_of_string "31987698754000069509"));(* 19, 19 *) (mk_real_int (num_of_string "28833901254188249274")),(mk_real_int (num_of_string "24623248113726045663"));(* 19, 19 *) (mk_real_int (num_of_string "26242963290992346668")),(mk_real_int (num_of_string "14674162647648763688"));(* 19, 19 *) (mk_real_int (num_of_string "21837116817758393184")),(mk_real_int (num_of_string "33578587160158710450"));(* 19, 19 *) (mk_real_int (num_of_string "32308720031395484028")),(mk_real_int (num_of_string "22262431374078419304"));(* 19, 19 *) (mk_real_int (num_of_string "38772958076956140532")),(mk_real_int (num_of_string "18421681569409950656"));(* 19, 19 *) (mk_real_int (num_of_string "21835573189556921619")),(mk_real_int (num_of_string "21195853794395582302"));(* 19, 19 *) (mk_real_int (num_of_string "32936034992967092745")),(mk_real_int (num_of_string "17017105877426655000"));(* 19, 19 *) (mk_real_int (num_of_string "11779314930266035515")),(mk_real_int (num_of_string "22210367086454507697"));(* 19, 19 *) (mk_real_int (num_of_string "21262392262367283566")),(mk_real_int (num_of_string "18080247469344774021"));(* 19, 19 *) (mk_real_int (num_of_string "18485080201259915496")),(mk_real_int (num_of_string "19330266469721050228"));(* 19, 19 *) (mk_real_int (num_of_string "21314275633080189760")),(mk_real_int (num_of_string "26672783404801383366"));(* 19, 19 *) (mk_real_int (num_of_string "18225376473803493478")),(mk_real_int (num_of_string "35114088523317972168"));(* 19, 19 *) (mk_real_int (num_of_string "22256469025376193696")),(mk_real_int (num_of_string "14244710412207347160"));(* 19, 19 *) (mk_real_int (num_of_string "15814028600098804460")),(mk_real_int (num_of_string "29455255415320130242"));(* 19, 19 *) (mk_real_int (num_of_string "22207852932166681417")),(mk_real_int (num_of_string "26516227258443784004"));(* 19, 19 *) (mk_real_int (num_of_string "14789447783886017682")),(mk_real_int (num_of_string "16084367232224943916"));(* 19, 19 *) (mk_real_int (num_of_string "18833328680591237472")),(mk_real_int (num_of_string "21825090411736568528"));(* 19, 19 *) (mk_real_int (num_of_string "15597572379087638544")),(mk_real_int (num_of_string "26077792023578054298"));(* 19, 19 *) (mk_real_int (num_of_string "26878119204936958530")),(mk_real_int (num_of_string "33476608253746618444"));(* 19, 19 *) (mk_real_int (num_of_string "21449072397693693841")),(mk_real_int (num_of_string "35292704961684409316"));(* 19, 19 *) (mk_real_int (num_of_string "30199759622256795340")),(mk_real_int (num_of_string "24489522504759870954"));(* 19, 19 *) (mk_real_int (num_of_string "21339496126239382542")),(mk_real_int (num_of_string "28216628392467036797"));(* 19, 19 *) (mk_real_int (num_of_string "18283805257051816746")),(mk_real_int (num_of_string "24086808184522759500"));(* 19, 19 *) (mk_real_int (num_of_string "29808506556312959475")),(mk_real_int (num_of_string "19850537876095504710"));(* 19, 19 *) (mk_real_int (num_of_string "15647902267586078160")),(mk_real_int (num_of_string "24081196614941322120"));(* 19, 19 *) (mk_real_int (num_of_string "29479869033054686829")),(mk_real_int (num_of_string "15456675031417026000"));(* 19, 19 *) (mk_real_int (num_of_string "20640313180694555700")),(mk_real_int (num_of_string "24429910974973387752"));(* 19, 19 *) (mk_real_int (num_of_string "19017622319184472610")),(mk_real_int (num_of_string "30215491581640326115"));(* 19, 19 *) (mk_real_int (num_of_string "26044108791274477200")),(mk_real_int (num_of_string "32133176543618161968"));(* 19, 19 *) (mk_real_int (num_of_string "34522332525723352640")),(mk_real_int (num_of_string "23921287334186517968"));(* 19, 19 *) (mk_real_int (num_of_string "29505364164285463575")),(mk_real_int (num_of_string "37317681774104336748"));(* 19, 19 *) (mk_real_int (num_of_string "14710512227849318100")),(mk_real_int (num_of_string "23802448655388557264"));(* 19, 19 *) (mk_real_int (num_of_string "30196352118354653616")),(mk_real_int (num_of_string "27106624139908863077"));(* 19, 19 *) (mk_real_int (num_of_string "36784290814305071400")),(mk_real_int (num_of_string "31187606612894238969"));(* 19, 19 *) (mk_real_int (num_of_string "33262687821254277474")),(mk_real_int (num_of_string "23365975397006060500"));(* 19, 19 *) (mk_real_int (num_of_string "21779146247504967035")),(mk_real_int (num_of_string "18357828649500301566"));(* 19, 19 *) (mk_real_int (num_of_string "14596900574194861560")),(mk_real_int (num_of_string "33232277302903407795"));(* 19, 19 *) (mk_real_int (num_of_string "17955737100058116722")),(mk_real_int (num_of_string "21650341275797518515"));(* 19, 19 *) (mk_real_int (num_of_string "20323424466540095120")),(mk_real_int (num_of_string "34041169657965394958"));(* 19, 19 *) (mk_real_int (num_of_string "25685066141358506883")),(mk_real_int (num_of_string "27586149979933496292"));(* 19, 19 *) (mk_real_int (num_of_string "29521436359943206800")),(mk_real_int (num_of_string "23999532044905642192"));(* 19, 19 *) (mk_real_int (num_of_string "22395619896118559992")),(mk_real_int (num_of_string "40128807183259944380"));(* 19, 19 *) (mk_real_int (num_of_string "21380197764028746852")),(mk_real_int (num_of_string "29531541010963108887"));(* 19, 19 *) (mk_real_int (num_of_string "25195124945782994400")),(mk_real_int (num_of_string "15931637546605504317"));(* 19, 19 *) (mk_real_int (num_of_string "19273086397990407136")),(mk_real_int (num_of_string "23628956380354304595"));(* 19, 19 *) (mk_real_int (num_of_string "17641688134558872428")),(mk_real_int (num_of_string "21143921627181894750"));(* 19, 19 *) (mk_real_int (num_of_string "31373974749750652096")),(mk_real_int (num_of_string "21840199146188831551"));(* 19, 19 *) (mk_real_int (num_of_string "24804374934459121540")),(mk_real_int (num_of_string "11400862432903300148"));(* 19, 19 *) (mk_real_int (num_of_string "15714037058937398720")),(mk_real_int (num_of_string "24507889619577658008"));(* 19, 19 *) (mk_real_int (num_of_string "25000780992104284774")),(mk_real_int (num_of_string "17333849398852842108"));(* 19, 19 *) (mk_real_int (num_of_string "22253922015024750336")),(mk_real_int (num_of_string "19687298941090487014"));(* 19, 19 *) (mk_real_int (num_of_string "25808962862689204704")),(mk_real_int (num_of_string "29248275235162252500"));(* 19, 19 *) (mk_real_int (num_of_string "23655817116327309408")),(mk_real_int (num_of_string "37594936717336802870"));(* 19, 19 *) (mk_real_int (num_of_string "24272488042654248540")),(mk_real_int (num_of_string "20452705544156415816"));(* 19, 19 *) (mk_real_int (num_of_string "25283537823142476944")),(mk_real_int (num_of_string "13404457723972847840"));(* 19, 19 *) (mk_real_int (num_of_string "19881318870777807630")),(mk_real_int (num_of_string "32971053158189425675"));(* 19, 19 *) (mk_real_int (num_of_string "16975830808340138900")),(mk_real_int (num_of_string "16925656200290432265"));(* 19, 19 *) (mk_real_int (num_of_string "21161092370452799292")),(mk_real_int (num_of_string "34934643910763005332"));(* 19, 19 *) (mk_real_int (num_of_string "18841409901378752688")),(mk_real_int (num_of_string "18558385525761954224"));(* 19, 19 *) (mk_real_int (num_of_string "37632767767193286688")),(mk_real_int (num_of_string "35331980382329536422"));(* 19, 19 *) (mk_real_int (num_of_string "33121220549861720672")),(mk_real_int (num_of_string "20946802877876600120"));(* 19, 19 *) (mk_real_int (num_of_string "13044865963920872147")),(mk_real_int (num_of_string "35428033112795346276"));(* 19, 19 *) (mk_real_int (num_of_string "18889016228299739808")),(mk_real_int (num_of_string "24898998758022348729"));(* 19, 19 *) (mk_real_int (num_of_string "16344640111860894735")),(mk_real_int (num_of_string "27879078405385841425"));(* 19, 19 *) (mk_real_int (num_of_string "24231112031053786980")),(mk_real_int (num_of_string "30472672804489195764"));(* 19, 19 *) (mk_real_int (num_of_string "26150856558496395264")),(mk_real_int (num_of_string "15338673653532911484"));(* 19, 19 *) (mk_real_int (num_of_string "25051521140390473443")),(mk_real_int (num_of_string "18606893513954745219"));(* 19, 19 *) (mk_real_int (num_of_string "20581729693959774362")),(mk_real_int (num_of_string "33819525307256244402"));(* 19, 19 *) (mk_real_int (num_of_string "23042274063944186370")),(mk_real_int (num_of_string "21780182013103100169"));(* 19, 19 *) (mk_real_int (num_of_string "30883007964058191084")),(mk_real_int (num_of_string "31289003924588312760"));(* 19, 19 *) (mk_real_int (num_of_string "13891883593180453608")),(mk_real_int (num_of_string "17349750538845126402"));(* 19, 19 *) (mk_real_int (num_of_string "20385676494129768228")),(mk_real_int (num_of_string "20625889638236156032"));(* 19, 19 *) (mk_real_int (num_of_string "21947337678461729424")),(mk_real_int (num_of_string "18555426993793533690"));(* 19, 19 *) (mk_real_int (num_of_string "21719375807209157055")),(mk_real_int (num_of_string "19183305589395548172"));(* 19, 19 *) (mk_real_int (num_of_string "31396646920272046776")),(mk_real_int (num_of_string "35640418074086180971"));(* 19, 19 *) (mk_real_int (num_of_string "25763672516441210758")),(mk_real_int (num_of_string "20680085336517726735"));(* 19, 19 *) (mk_real_int (num_of_string "14029958728229911038")),(mk_real_int (num_of_string "30051566983801046596"));(* 19, 19 *) (mk_real_int (num_of_string "35496281454137761763")),(mk_real_int (num_of_string "21107324411363064380"));(* 19, 19 *) (mk_real_int (num_of_string "20535679195437347392")),(mk_real_int (num_of_string "21701303937929182985"));(* 19, 19 *) (mk_real_int (num_of_string "22893236960604226502")),(mk_real_int (num_of_string "17332455990826841480"));(* 19, 19 *) (mk_real_int (num_of_string "21868039566218851720")),(mk_real_int (num_of_string "24073034895901006092"));(* 19, 19 *) (mk_real_int (num_of_string "19483225121903585383")),(mk_real_int (num_of_string "15748691116098277656"));(* 19, 19 *) (mk_real_int (num_of_string "23656772980901958084")),(mk_real_int (num_of_string "16697614051956951828"));(* 19, 19 *) (mk_real_int (num_of_string "12699454851053170420")),(mk_real_int (num_of_string "25461510562697376750"));(* 19, 19 *) (mk_real_int (num_of_string "35662732873196498289")),(mk_real_int (num_of_string "28611306826766293080"));(* 19, 19 *) (mk_real_int (num_of_string "22416539791459745470")),(mk_real_int (num_of_string "13995037989450860188"));(* 19, 19 *) (mk_real_int (num_of_string "35878978645130975244")),(mk_real_int (num_of_string "29092793441652213240"));(* 19, 19 *) (mk_real_int (num_of_string "29455260321262238100")),(mk_real_int (num_of_string "16399031271517392300"));(* 19, 19 *) (mk_real_int (num_of_string "22557952450292566879")),(mk_real_int (num_of_string "23864941981560058786"));(* 19, 19 *) (mk_real_int (num_of_string "26368360885501374432")),(mk_real_int (num_of_string "39147149669121170259"));(* 19, 19 *) (mk_real_int (num_of_string "36393515656323289035")),(mk_real_int (num_of_string "36672604880094858664"));(* 19, 19 *) (mk_real_int (num_of_string "30780162470002874346")),(mk_real_int (num_of_string "27752257689340888704"));(* 19, 19 *) (mk_real_int (num_of_string "25689258876340596834")),(mk_real_int (num_of_string "21441108621776803443"));(* 19, 19 *) (mk_real_int (num_of_string "23737226118466944545")),(mk_real_int (num_of_string "30994701259082878317"));(* 19, 19 *) (mk_real_int (num_of_string "25282242824740556688")),(mk_real_int (num_of_string "37148939628436148062"));(* 19, 19 *) (mk_real_int (num_of_string "21013194624316808529")),(mk_real_int (num_of_string "20255913077961248688"));(* 19, 19 *) (mk_real_int (num_of_string "31054139089427845787")),(mk_real_int (num_of_string "19607683804071960960"));(* 19, 19 *) (mk_real_int (num_of_string "15303024613317648944")),(mk_real_int (num_of_string "39408872501785937942"));(* 19, 19 *) (mk_real_int (num_of_string "20898994338157062336")),(mk_real_int (num_of_string "38025069964956110300"));(* 19, 19 *) (mk_real_int (num_of_string "18968333228354927186")),(mk_real_int (num_of_string "21018674954106317466"));(* 19, 19 *) (mk_real_int (num_of_string "39790487940152314750")),(mk_real_int (num_of_string "22008196746171716509"));(* 19, 19 *) (mk_real_int (num_of_string "33017162701071351726")),(mk_real_int (num_of_string "30623384819158111552"));(* 19, 19 *) (mk_real_int (num_of_string "19091830859217444592")),(mk_real_int (num_of_string "26220236181304455400"));(* 19, 19 *) (mk_real_int (num_of_string "29157386168392844560")),(mk_real_int (num_of_string "11271378385086514992"));(* 19, 19 *) (mk_real_int (num_of_string "19447811743626438887")),(mk_real_int (num_of_string "25148407602027456648"));(* 19, 19 *) (mk_real_int (num_of_string "30131465927424366604")),(mk_real_int (num_of_string "29360540495144766292"));(* 19, 19 *) (mk_real_int (num_of_string "34002073485636530164")),(mk_real_int (num_of_string "26834180965871892888"));(* 19, 19 *) (mk_real_int (num_of_string "35672024606187267584")),(mk_real_int (num_of_string "26468202097817481771"));(* 19, 19 *) (mk_real_int (num_of_string "24961548100229544705")),(mk_real_int (num_of_string "25999859467693733600"));(* 19, 19 *) (mk_real_int (num_of_string "22295613667897276278")),(mk_real_int (num_of_string "18047102405916751200"));(* 19, 19 *) (mk_real_int (num_of_string "39033376394649241264")),(mk_real_int (num_of_string "30880326766048636008"));(* 19, 19 *) (mk_real_int (num_of_string "22813007803174618502")),(mk_real_int (num_of_string "22063227488563837180"));(* 19, 19 *) (mk_real_int (num_of_string "18709905187338992352")),(mk_real_int (num_of_string "21719877799596511920"));(* 19, 19 *) (mk_real_int (num_of_string "24098182147414487970")),(mk_real_int (num_of_string "23651738249051735592"));(* 19, 19 *) (mk_real_int (num_of_string "18849676051484033052")),(mk_real_int (num_of_string "17314533458455923580"));(* 19, 19 *) (mk_real_int (num_of_string "32029828035309675615")),(mk_real_int (num_of_string "37157871809647249782"));(* 19, 19 *) (mk_real_int (num_of_string "13351949757625652712")),(mk_real_int (num_of_string "33859823103015458340"));(* 19, 19 *) (mk_real_int (num_of_string "15999759484967973792")),(mk_real_int (num_of_string "28592403385028861884"));(* 19, 19 *) (mk_real_int (num_of_string "26219308464093530412")),(mk_real_int (num_of_string "19979634390551284020"));(* 19, 19 *) (mk_real_int (num_of_string "20847752193707676655")),(mk_real_int (num_of_string "25076325914072886035"));(* 19, 19 *) (mk_real_int (num_of_string "17875505079745949350")),(mk_real_int (num_of_string "26109848057034145536"));(* 19, 19 *) (mk_real_int (num_of_string "17572875153060997770")),(mk_real_int (num_of_string "29113855434106231217"));(* 19, 19 *) (mk_real_int (num_of_string "22832872037954766425")),(mk_real_int (num_of_string "25897357592381159016"));(* 19, 19 *) (mk_real_int (num_of_string "20617963579715412438")),(mk_real_int (num_of_string "17941483848787653352"));(* 19, 19 *) (mk_real_int (num_of_string "16586772811067563368")),(mk_real_int (num_of_string "22577575012573999880"));(* 19, 19 *) (mk_real_int (num_of_string "34264192210874287629")),(mk_real_int (num_of_string "31735607411072497867"));(* 19, 19 *) (mk_real_int (num_of_string "23115416111143986663")),(mk_real_int (num_of_string "16967646085217465088"));(* 19, 19 *) (mk_real_int (num_of_string "22962185970251136180")),(mk_real_int (num_of_string "12808457799981573070"));(* 19, 19 *) (mk_real_int (num_of_string "27165110514303590796")),(mk_real_int (num_of_string "28554387401526071184"));(* 19, 19 *) (mk_real_int (num_of_string "25585191232850450421")),(mk_real_int (num_of_string "27087811082981623546"));(* 19, 19 *) (mk_real_int (num_of_string "26664612388681030170")),(mk_real_int (num_of_string "28339469831309891870"));(* 19, 19 *) (mk_real_int (num_of_string "25771062593658789044")),(mk_real_int (num_of_string "18222926787001930752"));(* 19, 19 *) (mk_real_int (num_of_string "27586091301364074292")),(mk_real_int (num_of_string "21812202620855555205"));(* 19, 19 *) (mk_real_int (num_of_string "23445910158224676408")),(mk_real_int (num_of_string "24476303740024606250"));(* 19, 19 *) (mk_real_int (num_of_string "38588034485550390192")),(mk_real_int (num_of_string "29500904736758084784"));(* 19, 19 *) (mk_real_int (num_of_string "19652744433819514743")),(mk_real_int (num_of_string "25156141770392809319"));(* 19, 19 *) (mk_real_int (num_of_string "29965525190581326566")),(mk_real_int (num_of_string "36314785139233560531"));(* 19, 19 *) (mk_real_int (num_of_string "21466258262340035760")),(mk_real_int (num_of_string "29263041789177721140"));(* 19, 19 *) (mk_real_int (num_of_string "24397602931801015532")),(mk_real_int (num_of_string "25484236670011121640"));(* 19, 19 *) (mk_real_int (num_of_string "30310047782521318625")),(mk_real_int (num_of_string "23609134994805415132"));(* 19, 19 *) (mk_real_int (num_of_string "27659667981760402500")),(mk_real_int (num_of_string "24628272363884320857"));(* 19, 19 *) (mk_real_int (num_of_string "19978469335455279330")),(mk_real_int (num_of_string "24116883763569872715"));(* 19, 19 *) (mk_real_int (num_of_string "26892789155560700680")),(mk_real_int (num_of_string "36826219781739975433"));(* 19, 19 *) (mk_real_int (num_of_string "29394132354177563764")),(mk_real_int (num_of_string "23221912176679400800"));(* 19, 19 *) (mk_real_int (num_of_string "26830089923470820415")),(mk_real_int (num_of_string "28365564961988932458"));(* 19, 19 *) (mk_real_int (num_of_string "31382923082882636408")),(mk_real_int (num_of_string "20146078635041420985"));(* 19, 19 *) (mk_real_int (num_of_string "19816396770725025900")),(mk_real_int (num_of_string "24522489899722746998"));(* 19, 19 *) (mk_real_int (num_of_string "38749541586950688120")),(mk_real_int (num_of_string "39098718085652716854"));(* 19, 19 *) (mk_real_int (num_of_string "24953776264020954592")),(mk_real_int (num_of_string "34754678475782026300"));(* 19, 19 *) (mk_real_int (num_of_string "24980861439510874920")),(mk_real_int (num_of_string "21198569882617308060"));(* 19, 19 *) (mk_real_int (num_of_string "25658580097839459056")),(mk_real_int (num_of_string "25212675872485860660"));(* 19, 19 *) (mk_real_int (num_of_string "19385852360280688326")),(mk_real_int (num_of_string "29509350922069688131"));(* 19, 19 *) (mk_real_int (num_of_string "23671836189729585000")),(mk_real_int (num_of_string "27831702775237992180"));(* 19, 19 *) (mk_real_int (num_of_string "26544931026881917848")),(mk_real_int (num_of_string "20990756168224711517"));(* 19, 19 *) (mk_real_int (num_of_string "30047478145078388302")),(mk_real_int (num_of_string "27770176135212062695"));(* 19, 19 *) (mk_real_int (num_of_string "27316732758493825845")),(mk_real_int (num_of_string "19538268693513719952"));(* 19, 19 *) (mk_real_int (num_of_string "21561909110929122507")),(mk_real_int (num_of_string "41262572341482248504"));(* 19, 19 *) (mk_real_int (num_of_string "26501376724912212651")),(mk_real_int (num_of_string "32352759210287208726"));(* 19, 19 *) (mk_real_int (num_of_string "26184337037668596160")),(mk_real_int (num_of_string "34565717092174178768"));(* 19, 19 *) (mk_real_int (num_of_string "32173352765971071116")),(mk_real_int (num_of_string "17265475475387274520"));(* 19, 19 *) (mk_real_int (num_of_string "25152477836196229431")),(mk_real_int (num_of_string "21416597443651344726"));(* 19, 19 *) (mk_real_int (num_of_string "18541278738854842047")),(mk_real_int (num_of_string "19892101781340409995"));(* 19, 19 *) (mk_real_int (num_of_string "19416448921216784822")),(mk_real_int (num_of_string "33392288363839030483"));(* 19, 19 *) (mk_real_int (num_of_string "16689221150454470772")),(mk_real_int (num_of_string "16884844507537379868"));(* 19, 19 *) (mk_real_int (num_of_string "36074432973524338800")),(mk_real_int (num_of_string "22884161377122256860"));(* 19, 19 *) (mk_real_int (num_of_string "17982463638819408520")),(mk_real_int (num_of_string "30714353454772618697"));(* 19, 19 *) (mk_real_int (num_of_string "27963961335826272867")),(mk_real_int (num_of_string "21751183914121743763"));(* 19, 19 *) (mk_real_int (num_of_string "31983056409192838334")),(mk_real_int (num_of_string "16849795793906519444"));(* 19, 19 *) (mk_real_int (num_of_string "23828508717964552888")),(mk_real_int (num_of_string "21905102686851911670"));(* 19, 19 *) (mk_real_int (num_of_string "19524189968843721876")),(mk_real_int (num_of_string "22296291538003493120"));(* 19, 19 *) (mk_real_int (num_of_string "30003230312244243912")),(mk_real_int (num_of_string "31524168070512828480"));(* 19, 19 *) (mk_real_int (num_of_string "25378970707150727260")),(mk_real_int (num_of_string "27694584206296789474"));(* 19, 19 *) (mk_real_int (num_of_string "15001396544174109960")),(mk_real_int (num_of_string "22597302615363537556"));(* 19, 19 *) (mk_real_int (num_of_string "28650239001671556258")),(mk_real_int (num_of_string "29791235497066187848"));(* 19, 19 *) (mk_real_int (num_of_string "22574500911615728460")),(mk_real_int (num_of_string "31733840856116244780"));(* 19, 19 *) (mk_real_int (num_of_string "19401400630377382584")),(mk_real_int (num_of_string "24129285810268778700"));(* 19, 19 *) (mk_real_int (num_of_string "34196034285619615695")),(mk_real_int (num_of_string "18047615096119075896"));(* 19, 19 *) (mk_real_int (num_of_string "21982009838094264464")),(mk_real_int (num_of_string "22424652782690362512"));(* 19, 19 *) (mk_real_int (num_of_string "27791903869775971464")),(mk_real_int (num_of_string "25973068407781352880"));(* 19, 19 *) (mk_real_int (num_of_string "14304069474463657152")),(mk_real_int (num_of_string "14341256874380659014"));(* 19, 19 *) (mk_real_int (num_of_string "27667441193806736949")),(mk_real_int (num_of_string "31540493569147746843"));(* 19, 19 *) (mk_real_int (num_of_string "21090871618263748576")),(mk_real_int (num_of_string "16848512912294645010"));(* 19, 19 *) (mk_real_int (num_of_string "23478791800103107072")),(mk_real_int (num_of_string "22847439476393054952"));(* 19, 19 *) (mk_real_int (num_of_string "34335901118600926548")),(mk_real_int (num_of_string "26932079655173527560"));(* 19, 19 *) (mk_real_int (num_of_string "17040284624562954293")),(mk_real_int (num_of_string "22658477257343206466"));(* 19, 19 *) (mk_real_int (num_of_string "15956634778338900844")),(mk_real_int (num_of_string "26689382937164893638"));(* 19, 19 *) (mk_real_int (num_of_string "14011671230034854200")),(mk_real_int (num_of_string "24543107305284487458"));(* 19, 19 *) (mk_real_int (num_of_string "20353518960608955187")),(mk_real_int (num_of_string "19472405224360089386"));(* 19, 19 *) (mk_real_int (num_of_string "22665117812763391680")),(mk_real_int (num_of_string "29827041475339497543"));(* 19, 19 *) (mk_real_int (num_of_string "21860523829262727026")),(mk_real_int (num_of_string "31579961924409641127"));(* 19, 19 *) (mk_real_int (num_of_string "22347825113359737090")),(mk_real_int (num_of_string "23515764525675482753"));(* 19, 19 *) (mk_real_int (num_of_string "31025699041969103186")),(mk_real_int (num_of_string "15742238779906783914"));(* 19, 19 *) (mk_real_int (num_of_string "21238761019553983312")),(mk_real_int (num_of_string "28895960507926675504"));(* 19, 19 *) (mk_real_int (num_of_string "26453246915869727492")),(mk_real_int (num_of_string "22304668791543107046"));(* 19, 19 *) (mk_real_int (num_of_string "21095515470598270790")),(mk_real_int (num_of_string "19162429559220454969"));(* 19, 19 *) (mk_real_int (num_of_string "28742273211849664478")),(mk_real_int (num_of_string "17189194323445028742"));(* 19, 19 *) (mk_real_int (num_of_string "33944953713377163886")),(mk_real_int (num_of_string "21833964167745880876"));(* 19, 19 *) (mk_real_int (num_of_string "19620133336135880064")),(mk_real_int (num_of_string "23870181030677562944"));(* 19, 19 *) (mk_real_int (num_of_string "18159998781406997988")),(mk_real_int (num_of_string "24833946036411722408"));(* 19, 19 *) (mk_real_int (num_of_string "18263686907120302648")),(mk_real_int (num_of_string "18036860900769570453"));(* 19, 19 *) (mk_real_int (num_of_string "19933458841347060460")),(mk_real_int (num_of_string "26575623380299331338"));(* 19, 19 *) (mk_real_int (num_of_string "25200099264514284770")),(mk_real_int (num_of_string "23862600305112480769"));(* 19, 19 *) (mk_real_int (num_of_string "19668776568490331887")),(mk_real_int (num_of_string "15481177495656699200"));(* 19, 19 *) (mk_real_int (num_of_string "27600383229493630325")),(mk_real_int (num_of_string "35404523088447292824"));(* 19, 19 *) (mk_real_int (num_of_string "22796120663121608187")),(mk_real_int (num_of_string "30377444381526688501"));(* 19, 19 *) (mk_real_int (num_of_string "25781006763175331316")),(mk_real_int (num_of_string "23577069805680829977"));(* 19, 19 *) (mk_real_int (num_of_string "20985501502835422344")),(mk_real_int (num_of_string "16695021197303776096"));(* 19, 19 *) (mk_real_int (num_of_string "33072455242031449530")),(mk_real_int (num_of_string "12913517912579789780"));(* 19, 19 *) (mk_real_int (num_of_string "36224161914498238153")),(mk_real_int (num_of_string "14772829702133894787"));(* 19, 19 *) (mk_real_int (num_of_string "13813400700338909901")),(mk_real_int (num_of_string "34453671596238453240"));(* 19, 19 *) (mk_real_int (num_of_string "33343972111168420856")),(mk_real_int (num_of_string "30091839935821648050"));(* 19, 19 *) (mk_real_int (num_of_string "33993906187652787552")),(mk_real_int (num_of_string "30820853625105027000"));(* 19, 19 *) (mk_real_int (num_of_string "15398262358260039060")),(mk_real_int (num_of_string "26309820863576217121"));(* 19, 19 *) (mk_real_int (num_of_string "26198210986492520184")),(mk_real_int (num_of_string "35291341456130224080"));(* 19, 19 *) (mk_real_int (num_of_string "20282304095836622532")),(mk_real_int (num_of_string "34885133775451950892"));(* 19, 19 *) (mk_real_int (num_of_string "14004673892884099953")),(mk_real_int (num_of_string "29057703638847203056"));(* 19, 19 *) (mk_real_int (num_of_string "22907801178625159390")),(mk_real_int (num_of_string "14868861612268124956"));(* 19, 19 *) (mk_real_int (num_of_string "35538939861605280100")),(mk_real_int (num_of_string "34252561611460523375"));(* 19, 19 *) (mk_real_int (num_of_string "26841326791092839146")),(mk_real_int (num_of_string "25472680586614535340"));(* 19, 19 *) (mk_real_int (num_of_string "16363271346712834830")),(mk_real_int (num_of_string "24973121537740975951"));(* 19, 19 *) (mk_real_int (num_of_string "35026051287526630650")),(mk_real_int (num_of_string "21061660193237446585"));(* 19, 19 *) (mk_real_int (num_of_string "19349716319279206476")),(mk_real_int (num_of_string "13458090771119812752"));(* 19, 19 *) (mk_real_int (num_of_string "16947350985084926692")),(mk_real_int (num_of_string "13117012462162467870"));(* 19, 19 *) (mk_real_int (num_of_string "23317740640386032764")),(mk_real_int (num_of_string "18008229442063096071"));(* 19, 19 *) (mk_real_int (num_of_string "21468421073837433168")),(mk_real_int (num_of_string "23345546932891421568"));(* 19, 19 *) (mk_real_int (num_of_string "22583095457927525455")),(mk_real_int (num_of_string "25209712123444250358"));(* 19, 19 *) (mk_real_int (num_of_string "23254470779552887292")),(mk_real_int (num_of_string "23916875771977117479"));(* 19, 19 *) (mk_real_int (num_of_string "35817883931216821500")),(mk_real_int (num_of_string "24250161146652353770"));(* 19, 19 *) (mk_real_int (num_of_string "31213699324173896508")),(mk_real_int (num_of_string "27441032356296400050"));(* 19, 19 *) (mk_real_int (num_of_string "17745025504298030246")),(mk_real_int (num_of_string "12561974162522840484"));(* 19, 19 *) (mk_real_int (num_of_string "28451704245600251000")),(mk_real_int (num_of_string "31753646719707495418"));(* 19, 19 *) (mk_real_int (num_of_string "27079462488720831860")),(mk_real_int (num_of_string "33103930501167051999"));(* 19, 19 *) (mk_real_int (num_of_string "40763611124460240940")),(mk_real_int (num_of_string "19771122417175555635"));(* 19, 19 *) (mk_real_int (num_of_string "18708193082788002486")),(mk_real_int (num_of_string "24283826884383442684"));(* 19, 19 *) (mk_real_int (num_of_string "31730479417294456480")),(mk_real_int (num_of_string "41330439387262982528"));(* 19, 19 *) (mk_real_int (num_of_string "25534576776676283272")),(mk_real_int (num_of_string "24965013034087710430"));(* 19, 19 *) (mk_real_int (num_of_string "21557433898333368640")),(mk_real_int (num_of_string "19795009624311561750"));(* 19, 19 *) (mk_real_int (num_of_string "35499214825031756700")),(mk_real_int (num_of_string "19972281333562377512"));(* 19, 19 *) (mk_real_int (num_of_string "27404570400407320032")),(mk_real_int (num_of_string "19435177175271893805"));(* 19, 19 *) (mk_real_int (num_of_string "19156846007767209027")),(mk_real_int (num_of_string "21923918239967151815"));(* 19, 19 *) (mk_real_int (num_of_string "34350656859968979486")),(mk_real_int (num_of_string "17279712264357716800"));(* 19, 19 *) (mk_real_int (num_of_string "26112985511247953230")),(mk_real_int (num_of_string "22567007898443664832"));(* 19, 19 *) (mk_real_int (num_of_string "18692729353472770200")),(mk_real_int (num_of_string "16710457357447345800"));(* 19, 19 *) (mk_real_int (num_of_string "19610630158063286760")),(mk_real_int (num_of_string "27145524445597080402"));(* 19, 19 *) (mk_real_int (num_of_string "24125241853056887752")),(mk_real_int (num_of_string "23376959364467089249"));(* 19, 19 *) (mk_real_int (num_of_string "12815874200850731296")),(mk_real_int (num_of_string "38603926498953215763"));(* 19, 19 *) (mk_real_int (num_of_string "25394056643949092616")),(mk_real_int (num_of_string "27952693788759455694"));(* 19, 19 *) (mk_real_int (num_of_string "22109091123482872872")),(mk_real_int (num_of_string "23442113221904340964"));(* 19, 19 *) (mk_real_int (num_of_string "26784603512782114230")),(mk_real_int (num_of_string "24533406266317859592"));(* 19, 19 *) (mk_real_int (num_of_string "20663208626305111680")),(mk_real_int (num_of_string "18202478751545590656"));(* 19, 19 *) (mk_real_int (num_of_string "20246697089444257091")),(mk_real_int (num_of_string "23327500277984659680"));(* 19, 19 *) (mk_real_int (num_of_string "18393501891872553402")),(mk_real_int (num_of_string "24581544571835771520"));(* 19, 19 *) (mk_real_int (num_of_string "24705736347753684091")),(mk_real_int (num_of_string "20462461784791727470"));(* 19, 19 *) (mk_real_int (num_of_string "30991127112516016611")),(mk_real_int (num_of_string "29752372313983413754"));(* 19, 19 *) (mk_real_int (num_of_string "18109415153526238080")),(mk_real_int (num_of_string "24476035812284447028"));(* 19, 19 *) (mk_real_int (num_of_string "19249085474578925262")),(mk_real_int (num_of_string "22063561655134422104"));(* 19, 19 *) (mk_real_int (num_of_string "18725681245967196490")),(mk_real_int (num_of_string "35897033449780160350"));(* 19, 19 *) (mk_real_int (num_of_string "23552106614514505500")),(mk_real_int (num_of_string "24038981472989649034"));(* 19, 19 *) (mk_real_int (num_of_string "18542971626674708862")),(mk_real_int (num_of_string "18985958452095117450"));(* 19, 19 *) (mk_real_int (num_of_string "18969731775635593920")),(mk_real_int (num_of_string "21303396667310437515"));(* 19, 19 *) (mk_real_int (num_of_string "27950853924636269902")),(mk_real_int (num_of_string "27740744599373815548"));(* 19, 19 *) (mk_real_int (num_of_string "32371868675867677011")),(mk_real_int (num_of_string "24750658371458880124"));(* 19, 19 *) (mk_real_int (num_of_string "19559092727748063897")),(mk_real_int (num_of_string "30297393325237576956"));(* 19, 19 *) (mk_real_int (num_of_string "40525825037409130408")),(mk_real_int (num_of_string "15723254263122848871"));(* 19, 19 *) (mk_real_int (num_of_string "17372071073042919662")),(mk_real_int (num_of_string "16252631542319883480"));(* 19, 19 *) (mk_real_int (num_of_string "17204409311432310132")),(mk_real_int (num_of_string "14220816779884022154"));(* 19, 19 *) (mk_real_int (num_of_string "32595387439053013806")),(mk_real_int (num_of_string "27001122572747090856"));(* 19, 19 *) (mk_real_int (num_of_string "18029968363269057382")),(mk_real_int (num_of_string "25352806340877438753"));(* 19, 19 *) (mk_real_int (num_of_string "17826631682711419260")),(mk_real_int (num_of_string "19063618754807575476"));(* 19, 19 *) (mk_real_int (num_of_string "24349160455233169875")),(mk_real_int (num_of_string "27089364767111193261"));(* 19, 19 *) (mk_real_int (num_of_string "18438142935199058082")),(mk_real_int (num_of_string "18921160730005941220"));(* 19, 19 *) (mk_real_int (num_of_string "24125576091154548494")),(mk_real_int (num_of_string "18239369601915679855"));(* 19, 19 *) (mk_real_int (num_of_string "16140557084423002770")),(mk_real_int (num_of_string "22204497050438990100"));(* 19, 19 *) (mk_real_int (num_of_string "29636046329509796847")),(mk_real_int (num_of_string "16308049534152817936"));(* 19, 19 *) (mk_real_int (num_of_string "28939435029772785034")),(mk_real_int (num_of_string "20287995266292043653"));(* 19, 19 *) (mk_real_int (num_of_string "22942044862974291593")),(mk_real_int (num_of_string "14391726373990748970"));(* 19, 19 *) (mk_real_int (num_of_string "27729528689185688409")),(mk_real_int (num_of_string "29589692474685879613"));(* 19, 19 *) (mk_real_int (num_of_string "19803067057916920316")),(mk_real_int (num_of_string "21757789760907289320"));(* 19, 19 *) (mk_real_int (num_of_string "29973731599962358296")),(mk_real_int (num_of_string "22544276048750317972"));(* 19, 19 *) (mk_real_int (num_of_string "29442429349135566984")),(mk_real_int (num_of_string "29118657870363305464"));(* 19, 19 *) (mk_real_int (num_of_string "19094520257069123152")),(mk_real_int (num_of_string "23764276951741156402"));(* 19, 19 *) (mk_real_int (num_of_string "14622269779899103245")),(mk_real_int (num_of_string "22302554145334720884"));(* 19, 19 *) (mk_real_int (num_of_string "25186566031316655405")),(mk_real_int (num_of_string "20283868484641519692"));(* 19, 19 *) (mk_real_int (num_of_string "15927858921062204974")),(mk_real_int (num_of_string "41095293506851279696"));(* 19, 19 *) (mk_real_int (num_of_string "30425953718752171734")),(mk_real_int (num_of_string "15069390144141249972"));(* 19, 19 *) (mk_real_int (num_of_string "31933138638792957643")),(mk_real_int (num_of_string "31094188475962731405"));(* 19, 19 *) (mk_real_int (num_of_string "30885956505287588375")),(mk_real_int (num_of_string "31533388056578563584"));(* 19, 19 *) (mk_real_int (num_of_string "24509598869442237309")),(mk_real_int (num_of_string "37827610630008496000"));(* 19, 19 *) (mk_real_int (num_of_string "35617073287735853243")),(mk_real_int (num_of_string "21640293701026126280"));(* 19, 19 *) (mk_real_int (num_of_string "21864141896494592552")),(mk_real_int (num_of_string "19414858669469493274"));(* 19, 19 *) (mk_real_int (num_of_string "22497046821796996680")),(mk_real_int (num_of_string "24468361849494163755"));(* 19, 19 *) (mk_real_int (num_of_string "18454160315433307575")),(mk_real_int (num_of_string "29544262229545937390"));(* 19, 19 *) (mk_real_int (num_of_string "31389254625076667462")),(mk_real_int (num_of_string "25477028738146954496"));(* 19, 19 *) (mk_real_int (num_of_string "38165379396797212593")),(mk_real_int (num_of_string "33222660668557097199"));(* 19, 19 *) (mk_real_int (num_of_string "32659689786159888100")),(mk_real_int (num_of_string "19724349117170828790"));(* 19, 19 *) (mk_real_int (num_of_string "26588996672188922136")),(mk_real_int (num_of_string "26199019831970324064"));(* 19, 19 *) (mk_real_int (num_of_string "25497183208097766484")),(mk_real_int (num_of_string "26791236689114765362"));(* 19, 19 *) (mk_real_int (num_of_string "13553688060939942542")),(mk_real_int (num_of_string "18788975757545615578"));(* 19, 19 *) (mk_real_int (num_of_string "24626605995958018888")),(mk_real_int (num_of_string "14675606037815959225"));(* 19, 19 *) (mk_real_int (num_of_string "14360744317476348330")),(mk_real_int (num_of_string "16988500655803533120"));(* 19, 19 *) (mk_real_int (num_of_string "33604134480727498490")),(mk_real_int (num_of_string "30978531819722722235"));(* 19, 19 *) (mk_real_int (num_of_string "26598261395929266120")),(mk_real_int (num_of_string "20886689752436495647"));(* 19, 19 *) (mk_real_int (num_of_string "16274997882728650560")),(mk_real_int (num_of_string "30576091956785224531"));(* 19, 19 *) (mk_real_int (num_of_string "15795590437661664058")),(mk_real_int (num_of_string "32607007828032847671"));(* 19, 19 *) (mk_real_int (num_of_string "21226657063041387199")),(mk_real_int (num_of_string "19380600379037717160"));(* 19, 19 *) (mk_real_int (num_of_string "17731492421475320840")),(mk_real_int (num_of_string "31447565893156133292"));(* 19, 19 *) (mk_real_int (num_of_string "39017189815494029304")),(mk_real_int (num_of_string "22074840229465576014"));(* 19, 19 *) (mk_real_int (num_of_string "36771261272764828953")),(mk_real_int (num_of_string "25177793280198373298"));(* 19, 19 *) (mk_real_int (num_of_string "20118517852716865615")),(mk_real_int (num_of_string "27600852437538170120"));(* 19, 19 *) (mk_real_int (num_of_string "12798707362650958133")),(mk_real_int (num_of_string "13596375121038965541"));(* 19, 19 *) (mk_real_int (num_of_string "21924971892685498406")),(mk_real_int (num_of_string "18535986363171178440"));(* 19, 19 *) (mk_real_int (num_of_string "24377705425187318611")),(mk_real_int (num_of_string "25522947763916285980"));(* 19, 19 *) (mk_real_int (num_of_string "27747326026551073932")),(mk_real_int (num_of_string "11470453796212064390"));(* 19, 19 *) (mk_real_int (num_of_string "34407010449780647976")),(mk_real_int (num_of_string "34382739334333531504"));(* 19, 19 *) (mk_real_int (num_of_string "27705310311230639406")),(mk_real_int (num_of_string "12805445347440959092"));(* 19, 19 *) (mk_real_int (num_of_string "22380991783605488880")),(mk_real_int (num_of_string "22091018206208962956"));(* 19, 19 *) (mk_real_int (num_of_string "15231881672406607626")),(mk_real_int (num_of_string "35524479484320363779"));(* 19, 19 *) (mk_real_int (num_of_string "25323696262052730850")),(mk_real_int (num_of_string "31064262492329038368"));(* 19, 19 *) (mk_real_int (num_of_string "33181388727825713562")),(mk_real_int (num_of_string "36905068628580972160"));(* 19, 19 *) (mk_real_int (num_of_string "29531663516820563615")),(mk_real_int (num_of_string "14929396566819381856"));(* 19, 19 *) (mk_real_int (num_of_string "19014337390570743540")),(mk_real_int (num_of_string "29674481741532370512"));(* 19, 19 *) (mk_real_int (num_of_string "34120619231727276490")),(mk_real_int (num_of_string "31967514887679298224"));(* 19, 19 *) (mk_real_int (num_of_string "36263673891684893676")),(mk_real_int (num_of_string "29341339085540926532"));(* 19, 19 *) (mk_real_int (num_of_string "26078170459254886236")),(mk_real_int (num_of_string "21772899228906584836"));(* 19, 19 *) (mk_real_int (num_of_string "25550138063915180232")),(mk_real_int (num_of_string "19983476906423455392"));(* 19, 19 *) (mk_real_int (num_of_string "16582615836984859992")),(mk_real_int (num_of_string "23091038345673222408"));(* 19, 19 *) (mk_real_int (num_of_string "16041562952460098152")),(mk_real_int (num_of_string "21129650129457407010"));(* 19, 19 *) (mk_real_int (num_of_string "12006603173605852130")),(mk_real_int (num_of_string "17487121410700070283"));(* 19, 19 *) (mk_real_int (num_of_string "32946725289700714239")),(mk_real_int (num_of_string "16155093850487430916"));(* 19, 19 *) (mk_real_int (num_of_string "37146289981551417216")),(mk_real_int (num_of_string "22125607319717363044"));(* 19, 19 *) (mk_real_int (num_of_string "13328250983295056754")),(mk_real_int (num_of_string "31775852003226558942"));(* 19, 19 *) (mk_real_int (num_of_string "22132328423998996830")),(mk_real_int (num_of_string "35678121467210738780"));(* 19, 19 *) (mk_real_int (num_of_string "27593476222192887644")),(mk_real_int (num_of_string "30781287604773253020"));(* 19, 19 *) (mk_real_int (num_of_string "20169312843359152000")),(mk_real_int (num_of_string "13513481699418255170"));(* 19, 19 *) (mk_real_int (num_of_string "21409277147739266038")),(mk_real_int (num_of_string "29952470206552291002"));(* 19, 19 *) (mk_real_int (num_of_string "30248208034708693370")),(mk_real_int (num_of_string "33787441562769576000"));(* 19, 19 *) (mk_real_int (num_of_string "17179944701068635860")),(mk_real_int (num_of_string "20246696732625708224"));(* 19, 19 *) (mk_real_int (num_of_string "27592950045860018336")),(mk_real_int (num_of_string "22656866243372258887"));(* 19, 19 *) (mk_real_int (num_of_string "21645206055816802305")),(mk_real_int (num_of_string "35165670323329428960"));(* 19, 19 *) (mk_real_int (num_of_string "15138933888302827702")),(mk_real_int (num_of_string "20666020761463043736"));(* 19, 19 *) (mk_real_int (num_of_string "30675362596463602776")),(mk_real_int (num_of_string "16849906652436225258"));(* 19, 19 *) (mk_real_int (num_of_string "19623236605051973850")),(mk_real_int (num_of_string "27428330004651971846"));(* 19, 19 *) (mk_real_int (num_of_string "26344184171233972824")),(mk_real_int (num_of_string "25279693627925442915"));(* 19, 19 *) (mk_real_int (num_of_string "36654593024610957968")),(mk_real_int (num_of_string "27646920664560662993"));(* 19, 19 *) (mk_real_int (num_of_string "31221939749053570627")),(mk_real_int (num_of_string "17965315047249648144"));(* 19, 19 *) (mk_real_int (num_of_string "25597944237540268110")),(mk_real_int (num_of_string "41808751982371823790"));(* 19, 19 *) (mk_real_int (num_of_string "21344451558004133020")),(mk_real_int (num_of_string "17124918083033992440"));(* 19, 19 *) (mk_real_int (num_of_string "21981096408346541829")),(mk_real_int (num_of_string "13674620900120828725"));(* 19, 19 *) (mk_real_int (num_of_string "14647819175183465040")),(mk_real_int (num_of_string "30034774506045728100"));(* 19, 19 *) (mk_real_int (num_of_string "22143544139323588267")),(mk_real_int (num_of_string "29885638079817176338"));(* 19, 19 *) (mk_real_int (num_of_string "19550733879651497985")),(mk_real_int (num_of_string "29568402713350133952"));(* 19, 19 *) (mk_real_int (num_of_string "26985541859353609290")),(mk_real_int (num_of_string "25304391139247949300"));(* 19, 19 *) (mk_real_int (num_of_string "22096491556805736378")),(mk_real_int (num_of_string "35226266126172145332"));(* 19, 19 *) (mk_real_int (num_of_string "34004720482896220838")),(mk_real_int (num_of_string "21278642233425501309"));(* 19, 19 *) (mk_real_int (num_of_string "24536086935723931953")),(mk_real_int (num_of_string "29275992463371021390"));(* 19, 19 *) (mk_real_int (num_of_string "31331396467788170204")),(mk_real_int (num_of_string "19878039994797111710"));(* 19, 19 *) (mk_real_int (num_of_string "20309178453818646700")),(mk_real_int (num_of_string "37548673291733307418"));(* 19, 19 *) (mk_real_int (num_of_string "22328525158439225726")),(mk_real_int (num_of_string "21307219565831411454"));(* 19, 19 *) (mk_real_int (num_of_string "29427492048601420400")),(mk_real_int (num_of_string "22201442719323778284"));(* 19, 19 *) (mk_real_int (num_of_string "31711775010073139124")),(mk_real_int (num_of_string "29404749415651586790"));(* 19, 19 *) (mk_real_int (num_of_string "22100592600805206708")),(mk_real_int (num_of_string "25728987974184227656"));(* 19, 19 *) (mk_real_int (num_of_string "17855939735664750775")),(mk_real_int (num_of_string "17212428397568501350"));(* 19, 19 *) (mk_real_int (num_of_string "17402582047553443158")),(mk_real_int (num_of_string "22066766222533077705"));(* 19, 19 *) (mk_real_int (num_of_string "17382638054358948800")),(mk_real_int (num_of_string "23141063801553832530"));(* 19, 19 *) (mk_real_int (num_of_string "24321715574161737996")),(mk_real_int (num_of_string "17116106132371068900"));(* 19, 19 *) (mk_real_int (num_of_string "23087526006034420502")),(mk_real_int (num_of_string "30211104660413350905"));(* 19, 19 *) (mk_real_int (num_of_string "38819900249420230908")),(mk_real_int (num_of_string "35609313341546045992"));(* 19, 19 *) (mk_real_int (num_of_string "32277773000740037936")),(mk_real_int (num_of_string "24221259742153765500"));(* 19, 19 *) (mk_real_int (num_of_string "23669881335897108312")),(mk_real_int (num_of_string "23821386511061026195"));(* 19, 19 *) (mk_real_int (num_of_string "15936801526316245542")),(mk_real_int (num_of_string "22701857823789760044"));(* 19, 19 *) (mk_real_int (num_of_string "27443341459799324796")),(mk_real_int (num_of_string "18138408851798046768"));(* 19, 19 *) (mk_real_int (num_of_string "23017878989135860214")),(mk_real_int (num_of_string "28299754207163618080"));(* 19, 19 *) (mk_real_int (num_of_string "23486112054204467041")),(mk_real_int (num_of_string "32462369300386538667"));(* 19, 19 *) (mk_real_int (num_of_string "22034346603138198384")),(mk_real_int (num_of_string "19336747127471395369"));(* 19, 19 *) (mk_real_int (num_of_string "17068604785795454100")),(mk_real_int (num_of_string "26551280941354186281"));(* 19, 19 *) (mk_real_int (num_of_string "24513793605909128268")),(mk_real_int (num_of_string "22010906713199306760"));(* 19, 19 *) (mk_real_int (num_of_string "21698337868319856744")),(mk_real_int (num_of_string "24659990850858277530"));(* 19, 19 *) (mk_real_int (num_of_string "18987790856881628936")),(mk_real_int (num_of_string "38703222585351931750"));(* 19, 19 *) (mk_real_int (num_of_string "26380381640729697570")),(mk_real_int (num_of_string "13269001234986019512"));(* 19, 19 *) (mk_real_int (num_of_string "18261258302314984044")),(mk_real_int (num_of_string "18190213142655771525"));(* 19, 19 *) (mk_real_int (num_of_string "25788522625823421530")),(mk_real_int (num_of_string "28599443352100219170"));(* 19, 19 *) (mk_real_int (num_of_string "27582711707211597090")),(mk_real_int (num_of_string "13052864770226574524"));(* 19, 19 *) (mk_real_int (num_of_string "24408460288856776506")),(mk_real_int (num_of_string "21770068987618583632"));(* 19, 19 *) (mk_real_int (num_of_string "30830903962137692160")),(mk_real_int (num_of_string "31359588218548448166"));(* 19, 19 *) (mk_real_int (num_of_string "18495207171285569956")),(mk_real_int (num_of_string "27420822346202658945"));(* 19, 19 *) (mk_real_int (num_of_string "18847940188537546625")),(mk_real_int (num_of_string "24148041476039731712"));(* 19, 19 *) (mk_real_int (num_of_string "21761763003063494125")),(mk_real_int (num_of_string "19519470799177735760"));(* 19, 19 *) (mk_real_int (num_of_string "33564953961711504464")),(mk_real_int (num_of_string "32653099097339940065"));(* 19, 19 *) (mk_real_int (num_of_string "23255989360125834312")),(mk_real_int (num_of_string "11428483616948489850"));(* 19, 19 *) (mk_real_int (num_of_string "25137192059546909056")),(mk_real_int (num_of_string "24274242678058871927"));(* 19, 19 *) (mk_real_int (num_of_string "25802598736174967575")),(mk_real_int (num_of_string "28364616950519037606"));(* 19, 19 *) (mk_real_int (num_of_string "24685943665311845972")),(mk_real_int (num_of_string "27685215255504302012"));(* 19, 19 *) (mk_real_int (num_of_string "24262716995383439870")),(mk_real_int (num_of_string "23413108019946708470"));(* 19, 19 *) (mk_real_int (num_of_string "14354642629640124471")),(mk_real_int (num_of_string "13212980882165527540"));(* 19, 19 *) (mk_real_int (num_of_string "37605209795841517247")),(mk_real_int (num_of_string "34434325806805453320"));(* 19, 19 *) (mk_real_int (num_of_string "17482455975190084076")),(mk_real_int (num_of_string "28882137203104564236"));(* 19, 19 *) (mk_real_int (num_of_string "24063328203927668392")),(mk_real_int (num_of_string "21364869037106819070"));(* 19, 19 *) (mk_real_int (num_of_string "32807061770042118185")),(mk_real_int (num_of_string "33847185911901104600"));(* 19, 19 *) (mk_real_int (num_of_string "21734625173406995520")),(mk_real_int (num_of_string "36785867593029564636"));(* 19, 19 *) (mk_real_int (num_of_string "33291805040098432586")),(mk_real_int (num_of_string "20918779597896747886"));(* 19, 19 *) (mk_real_int (num_of_string "24764382238421506725")),(mk_real_int (num_of_string "22049541964017668463"));(* 19, 19 *) (mk_real_int (num_of_string "36980452711734625335")),(mk_real_int (num_of_string "16251343302261158520"));(* 19, 19 *) (mk_real_int (num_of_string "25470220787897428620")),(mk_real_int (num_of_string "21454231125193216240"));(* 19, 19 *) (mk_real_int (num_of_string "21884788984906964743")),(mk_real_int (num_of_string "21318765634307187442"));(* 19, 19 *) (mk_real_int (num_of_string "16316068658335596612")),(mk_real_int (num_of_string "22464820172853730320"));(* 19, 19 *) (mk_real_int (num_of_string "22409649905876649427")),(mk_real_int (num_of_string "31411461082596577136"));(* 19, 19 *) (mk_real_int (num_of_string "37775162746432655280")),(mk_real_int (num_of_string "27093678766252889725"));(* 19, 19 *) (mk_real_int (num_of_string "30019980116289418750")),(mk_real_int (num_of_string "17681088934580252126"));(* 19, 19 *) (mk_real_int (num_of_string "15787621091768439738")),(mk_real_int (num_of_string "31241006724121256205"));(* 19, 19 *) (mk_real_int (num_of_string "18576616934182214193")),(mk_real_int (num_of_string "27076865338594659071"));(* 19, 19 *) (mk_real_int (num_of_string "27801119379245204014")),(mk_real_int (num_of_string "18499554587128490810"));(* 19, 19 *) (mk_real_int (num_of_string "33021601686411958334")),(mk_real_int (num_of_string "18984143019924845950"));(* 19, 19 *) (mk_real_int (num_of_string "34656284071577674605")),(mk_real_int (num_of_string "25400363181131315520"));(* 19, 19 *) (mk_real_int (num_of_string "22238992111205128006")),(mk_real_int (num_of_string "23259623118620891211"));(* 19, 19 *) (mk_real_int (num_of_string "16397842823556602760")),(mk_real_int (num_of_string "13316280665147741270"));(* 19, 19 *) (mk_real_int (num_of_string "21649143791556018155")),(mk_real_int (num_of_string "24380830033197971872"));(* 19, 19 *) (mk_real_int (num_of_string "13199435846426084860")),(mk_real_int (num_of_string "24847810947692768288"));(* 19, 19 *) (mk_real_int (num_of_string "14150269988641140200")),(mk_real_int (num_of_string "15815660819655009225"));(* 19, 19 *) (mk_real_int (num_of_string "42204146720928205860")),(mk_real_int (num_of_string "14712568422015628340"));(* 19, 19 *) (mk_real_int (num_of_string "13246708761339822153")),(mk_real_int (num_of_string "19607589261722560725"));(* 19, 19 *) (mk_real_int (num_of_string "32895760411454747488")),(mk_real_int (num_of_string "17460796088764225758"));(* 19, 19 *) (mk_real_int (num_of_string "18899167984289012288")),(mk_real_int (num_of_string "23793384144659539696"));(* 19, 19 *) (mk_real_int (num_of_string "33978551778860244732")),(mk_real_int (num_of_string "21825851399025562240"));(* 19, 19 *) (mk_real_int (num_of_string "30488087759588800825")),(mk_real_int (num_of_string "16314329673313065548"));(* 19, 19 *) (mk_real_int (num_of_string "26280004180894450800")),(mk_real_int (num_of_string "35078125034309500308"));(* 19, 19 *) (mk_real_int (num_of_string "16485356594170991197")),(mk_real_int (num_of_string "27036995653100044381"));(* 19, 19 *) (mk_real_int (num_of_string "22571128837490441362")),(mk_real_int (num_of_string "36340873507586687512"));(* 19, 19 *) (mk_real_int (num_of_string "22791167115233475530")),(mk_real_int (num_of_string "35440417913455324737"));(* 19, 19 *) (mk_real_int (num_of_string "27669954355559036653")),(mk_real_int (num_of_string "39536455825803336840"));(* 19, 19 *) (mk_real_int (num_of_string "22584127379549514086")),(mk_real_int (num_of_string "27604438056215103776"));(* 19, 19 *) (mk_real_int (num_of_string "26313087740355472749")),(mk_real_int (num_of_string "19999933290240356684"));(* 19, 19 *) (mk_real_int (num_of_string "28386135969361328235")),(mk_real_int (num_of_string "20442551843693814120"));(* 19, 19 *) (mk_real_int (num_of_string "18459196260535502472")),(mk_real_int (num_of_string "21176814170883095296"));(* 19, 19 *) (mk_real_int (num_of_string "27998349573677267400")),(mk_real_int (num_of_string "17940473647285109778"));(* 19, 19 *) (mk_real_int (num_of_string "21314466750214810535")),(mk_real_int (num_of_string "23261891940621234582"));(* 19, 19 *) (mk_real_int (num_of_string "29353566625665142960")),(mk_real_int (num_of_string "15196203556960611900"));(* 19, 19 *) (mk_real_int (num_of_string "16062224144359705169")),(mk_real_int (num_of_string "31965756049675649124"));(* 19, 19 *) (mk_real_int (num_of_string "31181753387861102400")),(mk_real_int (num_of_string "32800476488473214466"));(* 19, 19 *) (mk_real_int (num_of_string "36342765802472223600")),(mk_real_int (num_of_string "28929950600399156616"));(* 19, 19 *) (mk_real_int (num_of_string "26803964775091217714")),(mk_real_int (num_of_string "30443294620546244096"));(* 19, 19 *) (mk_real_int (num_of_string "20162640799716389700")),(mk_real_int (num_of_string "28535526671688838439"));(* 19, 19 *) (mk_real_int (num_of_string "32672562169071981464")),(mk_real_int (num_of_string "22213898848408890150"));(* 19, 19 *) (mk_real_int (num_of_string "27509399082047618208")),(mk_real_int (num_of_string "20357649146563834875"));(* 19, 19 *) (mk_real_int (num_of_string "40282882683633784766")),(mk_real_int (num_of_string "23993493380779388268"));(* 19, 19 *) (mk_real_int (num_of_string "24889592076979535664")),(mk_real_int (num_of_string "25596758577025945936"));(* 19, 19 *) (mk_real_int (num_of_string "36178449801387946074")),(mk_real_int (num_of_string "30036016885453005438"));(* 19, 19 *) (mk_real_int (num_of_string "18340256349106495056")),(mk_real_int (num_of_string "27351018742769488338"));(* 19, 19 *) (mk_real_int (num_of_string "30349903186600500239")),(mk_real_int (num_of_string "22675907052739393024"));(* 19, 19 *) (mk_real_int (num_of_string "25340956861049952980")),(mk_real_int (num_of_string "14554696132468375488"));(* 19, 19 *) (mk_real_int (num_of_string "30434053486901543094")),(mk_real_int (num_of_string "34903111318344978753"));(* 19, 19 *) (mk_real_int (num_of_string "20593526293144207260")),(mk_real_int (num_of_string "34320938490381856533"));(* 19, 19 *) (mk_real_int (num_of_string "25294599512835352095")),(mk_real_int (num_of_string "28866778122270999988"));(* 19, 19 *) (mk_real_int (num_of_string "30595768371252037250")),(mk_real_int (num_of_string "17157010495496446080"));(* 19, 19 *) (mk_real_int (num_of_string "31156269790789924440")),(mk_real_int (num_of_string "25586580972559089637"));(* 19, 19 *) (mk_real_int (num_of_string "26313869294074956352")),(mk_real_int (num_of_string "22294258113680253547"));(* 19, 19 *) (mk_real_int (num_of_string "21718643998109387472")),(mk_real_int (num_of_string "17685530933316988665"));(* 19, 19 *) (mk_real_int (num_of_string "34432579086991905820")),(mk_real_int (num_of_string "24125740438134501320"));(* 19, 19 *) (mk_real_int (num_of_string "37110643144701792380")),(mk_real_int (num_of_string "20775493568154656958"));(* 19, 19 *) (mk_real_int (num_of_string "36545974624960336690")),(mk_real_int (num_of_string "31428508005398278412"));(* 19, 19 *) (mk_real_int (num_of_string "43197310567402523400")),(mk_real_int (num_of_string "16088091250951015186"));(* 19, 19 *) (mk_real_int (num_of_string "23257535950489181033")),(mk_real_int (num_of_string "28456451544992664303"));(* 19, 19 *) (mk_real_int (num_of_string "28593229202225308368")),(mk_real_int (num_of_string "27017600688668787890"));(* 19, 19 *) (mk_real_int (num_of_string "22557743372387916000")),(mk_real_int (num_of_string "22888176977370647888"));(* 19, 19 *) (mk_real_int (num_of_string "26691937052873753958")),(mk_real_int (num_of_string "26386172792557327420"));(* 19, 19 *) (mk_real_int (num_of_string "13576802810000164405")),(mk_real_int (num_of_string "24768228216581841453"));(* 19, 19 *) (mk_real_int (num_of_string "30311697775602001440")),(mk_real_int (num_of_string "35431818084121715168"));(* 19, 19 *) (mk_real_int (num_of_string "25948640898213573276")),(mk_real_int (num_of_string "25940834982073338239"));(* 19, 19 *) (mk_real_int (num_of_string "26849875634153504240")),(mk_real_int (num_of_string "30872325595819157450"));(* 19, 19 *) (mk_real_int (num_of_string "21507347672586141696")),(mk_real_int (num_of_string "12928425043997799292"));(* 19, 19 *) (mk_real_int (num_of_string "24335519952035172804")),(mk_real_int (num_of_string "16822125598636476228"));(* 19, 19 *) (mk_real_int (num_of_string "23600351176291570428")),(mk_real_int (num_of_string "24713184514508879466"));(* 19, 19 *) (mk_real_int (num_of_string "22899088229278768661")),(mk_real_int (num_of_string "23379690009005171688"));(* 19, 19 *) (mk_real_int (num_of_string "37956340093595272360")),(mk_real_int (num_of_string "18102109283614287954"));(* 19, 19 *) (mk_real_int (num_of_string "14655950813499902555")),(mk_real_int (num_of_string "24050402490225431628"));(* 19, 19 *) (mk_real_int (num_of_string "29648948809431069624")),(mk_real_int (num_of_string "25138431393115367250"));(* 19, 19 *) (mk_real_int (num_of_string "19758837791426189170")),(mk_real_int (num_of_string "25956783408841313215"));(* 19, 19 *) (mk_real_int (num_of_string "16569199130785328808")),(mk_real_int (num_of_string "28529726078769698783"));(* 19, 19 *) (mk_real_int (num_of_string "21266812450129096488")),(mk_real_int (num_of_string "26505103197560241760"));(* 19, 19 *) (mk_real_int (num_of_string "25493453905539500540")),(mk_real_int (num_of_string "18658959656612538670"));(* 19, 19 *) (mk_real_int (num_of_string "23556577019856893584")),(mk_real_int (num_of_string "28488314694106903537"));(* 19, 19 *) (mk_real_int (num_of_string "19948414148749771256")),(mk_real_int (num_of_string "22273438498791337506"));(* 19, 19 *) (mk_real_int (num_of_string "33297813638782113036")),(mk_real_int (num_of_string "17882231489399270444"));(* 19, 19 *) (mk_real_int (num_of_string "29397677932176682051")),(mk_real_int (num_of_string "21549186267093807487"));(* 19, 19 *) (mk_real_int (num_of_string "19465798849849673046")),(mk_real_int (num_of_string "23745245152315670665"));(* 19, 19 *) (mk_real_int (num_of_string "29773451615455176387")),(mk_real_int (num_of_string "27163788802998857394"));(* 19, 19 *) (mk_real_int (num_of_string "32842813070487631772")),(mk_real_int (num_of_string "16377913050783071436"));(* 19, 19 *) (mk_real_int (num_of_string "30091707703911362432")),(mk_real_int (num_of_string "25249656137020914060"));(* 19, 19 *) (mk_real_int (num_of_string "23589225235850488049")),(mk_real_int (num_of_string "34206879536826949920"));(* 19, 19 *) (mk_real_int (num_of_string "31898780065226162814")),(mk_real_int (num_of_string "19465926564544377632"));(* 19, 19 *) (mk_real_int (num_of_string "41305668996654499316")),(mk_real_int (num_of_string "27191351362377963486"));(* 19, 19 *) (mk_real_int (num_of_string "20623370293922374352")),(mk_real_int (num_of_string "20147453042584755140"));(* 19, 19 *) (mk_real_int (num_of_string "39974127750395204487")),(mk_real_int (num_of_string "31398746878691767652"));(* 19, 19 *) (mk_real_int (num_of_string "22300899890820961696")),(mk_real_int (num_of_string "13900499863132201506"));(* 19, 19 *) (mk_real_int (num_of_string "22232761782592376312")),(mk_real_int (num_of_string "23744723660532921728"));(* 19, 19 *) (mk_real_int (num_of_string "27966187428081714196")),(mk_real_int (num_of_string "36096106859875704950"));(* 19, 19 *) (mk_real_int (num_of_string "38314073399773546892")),(mk_real_int (num_of_string "19600899384345470488"));(* 19, 19 *) (mk_real_int (num_of_string "28961126991378701790")),(mk_real_int (num_of_string "28910525367378710682"));(* 19, 19 *) (mk_real_int (num_of_string "17470633936510449816")),(mk_real_int (num_of_string "20912864791058017569"));(* 19, 19 *) (mk_real_int (num_of_string "26663069926377673800")),(mk_real_int (num_of_string "30161730089727198171"));(* 19, 19 *) (mk_real_int (num_of_string "21342089120250327858")),(mk_real_int (num_of_string "18550588946773456452"));(* 19, 19 *) (mk_real_int (num_of_string "26273505029779571872")),(mk_real_int (num_of_string "19822877957026831687"));(* 19, 19 *) (mk_real_int (num_of_string "32876421336244952488")),(mk_real_int (num_of_string "20149284916234047233"));(* 19, 19 *) (mk_real_int (num_of_string "25577887599110607585")),(mk_real_int (num_of_string "26835929099437470375"));(* 19, 19 *) (mk_real_int (num_of_string "42626056963981528400")),(mk_real_int (num_of_string "19943764079993547695"));(* 19, 19 *) (mk_real_int (num_of_string "21838923264396913950")),(mk_real_int (num_of_string "22825133517720625575"));(* 19, 19 *) (mk_real_int (num_of_string "22239186334554632520")),(mk_real_int (num_of_string "22769737641242918997"));(* 19, 19 *) (mk_real_int (num_of_string "29709011451290931188")),(mk_real_int (num_of_string "23234555493455919525"));(* 19, 19 *) (mk_real_int (num_of_string "12691541633567538269")),(mk_real_int (num_of_string "22662773436066740680"));(* 19, 19 *) (mk_real_int (num_of_string "22314796872591389782")),(mk_real_int (num_of_string "14588080525587964571"));(* 19, 19 *) (mk_real_int (num_of_string "26101202929280956026")),(mk_real_int (num_of_string "27392355273695007288"));(* 19, 19 *) (mk_real_int (num_of_string "25855063617604744600")),(mk_real_int (num_of_string "24123189463932751346"));(* 19, 19 *) (mk_real_int (num_of_string "25429453413802726453")),(mk_real_int (num_of_string "20022582181469275716"));(* 19, 19 *) (mk_real_int (num_of_string "25900968320854327624")),(mk_real_int (num_of_string "20174118381402248692"));(* 19, 19 *) (mk_real_int (num_of_string "21607066735242664104")),(mk_real_int (num_of_string "27874902862578863575"));(* 19, 19 *) (mk_real_int (num_of_string "27247746728153494158")),(mk_real_int (num_of_string "31246197516952637901"));(* 19, 19 *) (mk_real_int (num_of_string "11649269097240563250")),(mk_real_int (num_of_string "33376888058324957916"));(* 19, 19 *) (mk_real_int (num_of_string "21002321600510230904")),(mk_real_int (num_of_string "25521918462486637950"));(* 19, 19 *) (mk_real_int (num_of_string "34361779077523253136")),(mk_real_int (num_of_string "27478709758417471884"));(* 19, 19 *) (mk_real_int (num_of_string "19307364164949234605")),(mk_real_int (num_of_string "27201664169583979185"));(* 19, 19 *) (mk_real_int (num_of_string "21708972060248583726")),(mk_real_int (num_of_string "26625792852522188424"));(* 19, 19 *) (mk_real_int (num_of_string "20992909644750678602")),(mk_real_int (num_of_string "28216581947324199880"));(* 19, 19 *) (mk_real_int (num_of_string "23171041241070068632")),(mk_real_int (num_of_string "16984018234806833672"));(* 19, 19 *) (mk_real_int (num_of_string "29304555834043072110")),(mk_real_int (num_of_string "21942018883209161000"));(* 19, 19 *) (mk_real_int (num_of_string "21431728051247383881")),(mk_real_int (num_of_string "21046630079900826060"));(* 19, 19 *) (mk_real_int (num_of_string "19972222957218643606")),(mk_real_int (num_of_string "21348324562632103905"));(* 19, 19 *) (mk_real_int (num_of_string "29215086405346809528")),(mk_real_int (num_of_string "17383389464387498332"));(* 19, 19 *) (mk_real_int (num_of_string "19876900009504031032")),(mk_real_int (num_of_string "27577444252954639362"));(* 19, 19 *) (mk_real_int (num_of_string "20045304743982062490")),(mk_real_int (num_of_string "25809624318970708326"));(* 19, 19 *) (mk_real_int (num_of_string "28754657356275651889")),(mk_real_int (num_of_string "21176415570809191000"));(* 19, 19 *) (mk_real_int (num_of_string "24113366001973459651")),(mk_real_int (num_of_string "21711858573018874227"));(* 19, 19 *) (mk_real_int (num_of_string "29630032496049242367")),(mk_real_int (num_of_string "20756856522358502887"));(* 19, 19 *) (mk_real_int (num_of_string "30040003158269082935")),(mk_real_int (num_of_string "29726820060748053936"));(* 19, 19 *) (mk_real_int (num_of_string "37836152937793969616")),(mk_real_int (num_of_string "19944601580631661890"));(* 19, 19 *) (mk_real_int (num_of_string "18848916771827463068")),(mk_real_int (num_of_string "26922325303954551042"));(* 19, 19 *) (mk_real_int (num_of_string "15128095960284562332")),(mk_real_int (num_of_string "17800846923923030275"));(* 19, 19 *) (mk_real_int (num_of_string "29093134335533733696")),(mk_real_int (num_of_string "27303960891980689840"));(* 19, 19 *) (mk_real_int (num_of_string "31958131407042904448")),(mk_real_int (num_of_string "22379320634918408205"));(* 19, 19 *) (mk_real_int (num_of_string "23294275063204857250")),(mk_real_int (num_of_string "18669256321770054000"));(* 19, 19 *) (mk_real_int (num_of_string "17786143591562317488")),(mk_real_int (num_of_string "30176673536329722622"));(* 19, 19 *) (mk_real_int (num_of_string "28542283896162267264")),(mk_real_int (num_of_string "13207308519643598250"));(* 19, 19 *) (mk_real_int (num_of_string "29983153526405863740")),(mk_real_int (num_of_string "15013036575285946362"));(* 19, 19 *) (mk_real_int (num_of_string "23858314977795409100")),(mk_real_int (num_of_string "29854780687499042484"));(* 19, 19 *) (mk_real_int (num_of_string "34872388448702151754")),(mk_real_int (num_of_string "34174775218509951102"));(* 19, 19 *) (mk_real_int (num_of_string "26983669734902155572")),(mk_real_int (num_of_string "32092615951770995082"));(* 19, 19 *) (mk_real_int (num_of_string "23116869093692308220")),(mk_real_int (num_of_string "26343594450116949159"));(* 19, 19 *) (mk_real_int (num_of_string "41047867128209699340")),(mk_real_int (num_of_string "22610949879326408292"));(* 19, 19 *) (mk_real_int (num_of_string "27227312429443226947")),(mk_real_int (num_of_string "29862366717098140841"));(* 19, 19 *) (mk_real_int (num_of_string "17667643772654073242")),(mk_real_int (num_of_string "37270985840329657196"));(* 19, 19 *) (mk_real_int (num_of_string "23638363667741175276")),(mk_real_int (num_of_string "14629372843573341084"));(* 19, 19 *) (mk_real_int (num_of_string "13842637499705193036")),(mk_real_int (num_of_string "41480226945249484590"));(* 19, 19 *) (mk_real_int (num_of_string "17236894653963564140")),(mk_real_int (num_of_string "15816420339603437631"));(* 19, 19 *) (mk_real_int (num_of_string "13913517528973566504")),(mk_real_int (num_of_string "25436130346155656842"));(* 19, 19 *) (mk_real_int (num_of_string "31220442655840998560")),(mk_real_int (num_of_string "16925990165385038595"));(* 19, 19 *) (mk_real_int (num_of_string "22833486705024467703")),(mk_real_int (num_of_string "25890454048049275146"));(* 19, 19 *) (mk_real_int (num_of_string "16993108282830367226")),(mk_real_int (num_of_string "22014373786659157453"));(* 19, 19 *) (mk_real_int (num_of_string "21437302216226175345")),(mk_real_int (num_of_string "24291181329271812560"));(* 19, 19 *) (mk_real_int (num_of_string "17857255840162203432")),(mk_real_int (num_of_string "29021998546870931778"))(* 19, 19 *) ];;