formal_lp/old/arith/tests/arith_test_data15.hl

   1 let data = [\r
   2 (mk_real_int64 702941795326221L),(mk_real_int64 587475864851776L);(* 14, 14 *)\r
   3 (mk_real_int64 557681790741140L),(mk_real_int64 431609991799574L);(* 14, 14 *)\r
   4 (mk_real_int64 428657639559786L),(mk_real_int64 365457651324725L);(* 14, 14 *)\r
   5 (mk_real_int64 804672350225920L),(mk_real_int64 164799879070188L);(* 14, 14 *)\r
   6 (mk_real_int64 690700943383416L),(mk_real_int64 450621203384716L);(* 14, 14 *)\r
   7 (mk_real_int64 902567172378080L),(mk_real_int64 208922254068150L);(* 14, 14 *)\r
   8 (mk_real_int64 805104422742681L),(mk_real_int64 572429814888816L);(* 14, 14 *)\r
   9 (mk_real_int64 270459131819466L),(mk_real_int64 304148661952170L);(* 14, 14 *)\r
  10 (mk_real_int64 463191535210470L),(mk_real_int64 805728111094115L);(* 14, 14 *)\r
  11 (mk_real_int64 244467228142752L),(mk_real_int64 667000318316892L);(* 14, 14 *)\r
  12 (mk_real_int64 222131484494596L),(mk_real_int64 359290324562560L);(* 14, 14 *)\r
  13 (mk_real_int64 447908652928800L),(mk_real_int64 507708675244619L);(* 14, 14 *)\r
  14 (mk_real_int64 302795068486160L),(mk_real_int64 473247248215110L);(* 14, 14 *)\r
  15 (mk_real_int64 288273096314095L),(mk_real_int64 671484270634352L);(* 14, 14 *)\r
  16 (mk_real_int64 809186366965808L),(mk_real_int64 645392591505409L);(* 14, 14 *)\r
  17 (mk_real_int64 744422670553440L),(mk_real_int64 558730890514225L);(* 14, 14 *)\r
  18 (mk_real_int64 182607355397331L),(mk_real_int64 657560460440954L);(* 14, 14 *)\r
  19 (mk_real_int64 913387107541545L),(mk_real_int64 356668474352544L);(* 14, 14 *)\r
  20 (mk_real_int64 700179795938260L),(mk_real_int64 241404815137642L);(* 14, 14 *)\r
  21 (mk_real_int64 259727217701130L),(mk_real_int64 794044510790370L);(* 14, 14 *)\r
  22 (mk_real_int64 376141263117354L),(mk_real_int64 339961632304200L);(* 14, 14 *)\r
  23 (mk_real_int64 724223950704660L),(mk_real_int64 622132223304621L);(* 14, 14 *)\r
  24 (mk_real_int64 852003110535472L),(mk_real_int64 384658775936028L);(* 14, 14 *)\r
  25 (mk_real_int64 354862272152465L),(mk_real_int64 357110480531104L);(* 14, 14 *)\r
  26 (mk_real_int64 318147969036604L),(mk_real_int64 155757341270475L);(* 14, 14 *)\r
  27 (mk_real_int64 572122276941163L),(mk_real_int64 797515640627430L);(* 14, 14 *)\r
  28 (mk_real_int64 154631673126928L),(mk_real_int64 887284587732912L);(* 14, 14 *)\r
  29 (mk_real_int64 267953256539136L),(mk_real_int64 156206936375520L);(* 14, 14 *)\r
  30 (mk_real_int64 476924059192500L),(mk_real_int64 310967383408374L);(* 14, 14 *)\r
  31 (mk_real_int64 319016288248101L),(mk_real_int64 545169027562368L);(* 14, 14 *)\r
  32 (mk_real_int64 442430147544021L),(mk_real_int64 170012585320383L);(* 14, 14 *)\r
  33 (mk_real_int64 619589298196320L),(mk_real_int64 844856475393980L);(* 14, 14 *)\r
  34 (mk_real_int64 294253361839890L),(mk_real_int64 460826851897130L);(* 14, 14 *)\r
  35 (mk_real_int64 325033246271111L),(mk_real_int64 315444072925107L);(* 14, 14 *)\r
  36 (mk_real_int64 261568757276544L),(mk_real_int64 640312364909246L);(* 14, 14 *)\r
  37 (mk_real_int64 213476297484455L),(mk_real_int64 734418513415860L);(* 14, 14 *)\r
  38 (mk_real_int64 604243569249650L),(mk_real_int64 600235895745256L);(* 14, 14 *)\r
  39 (mk_real_int64 403014557725500L),(mk_real_int64 237260728296735L);(* 14, 14 *)\r
  40 (mk_real_int64 250386269932208L),(mk_real_int64 322323328798161L);(* 14, 14 *)\r
  41 (mk_real_int64 660366167449224L),(mk_real_int64 480690479307252L);(* 14, 14 *)\r
  42 (mk_real_int64 601255265294824L),(mk_real_int64 174918668116752L);(* 14, 14 *)\r
  43 (mk_real_int64 598790140086569L),(mk_real_int64 527485861651776L);(* 14, 14 *)\r
  44 (mk_real_int64 369044774046672L),(mk_real_int64 250876047027450L);(* 14, 14 *)\r
  45 (mk_real_int64 273385871939502L),(mk_real_int64 190834559174125L);(* 14, 14 *)\r
  46 (mk_real_int64 342940661716120L),(mk_real_int64 322729150591719L);(* 14, 14 *)\r
  47 (mk_real_int64 434881094309112L),(mk_real_int64 251436596098506L);(* 14, 14 *)\r
  48 (mk_real_int64 581329952031192L),(mk_real_int64 499504426524070L);(* 14, 14 *)\r
  49 (mk_real_int64 720490783645215L),(mk_real_int64 214896131146252L);(* 14, 14 *)\r
  50 (mk_real_int64 804335550437760L),(mk_real_int64 364661953912662L);(* 14, 14 *)\r
  51 (mk_real_int64 645439815446745L),(mk_real_int64 966046385975926L);(* 14, 14 *)\r
  52 (mk_real_int64 576000838272411L),(mk_real_int64 193943358331632L);(* 14, 14 *)\r
  53 (mk_real_int64 779551175501802L),(mk_real_int64 472071958808208L);(* 14, 14 *)\r
  54 (mk_real_int64 153329179657797L),(mk_real_int64 750271198524640L);(* 14, 14 *)\r
  55 (mk_real_int64 334792895382176L),(mk_real_int64 397325753023975L);(* 14, 14 *)\r
  56 (mk_real_int64 248363686553556L),(mk_real_int64 542005513043540L);(* 14, 14 *)\r
  57 (mk_real_int64 366789640924804L),(mk_real_int64 584124651722202L);(* 14, 14 *)\r
  58 (mk_real_int64 186287533864404L),(mk_real_int64 461681196343836L);(* 14, 14 *)\r
  59 (mk_real_int64 616778033652710L),(mk_real_int64 382444819990412L);(* 14, 14 *)\r
  60 (mk_real_int64 225596890128104L),(mk_real_int64 670724383606394L);(* 14, 14 *)\r
  61 (mk_real_int64 339908258377764L),(mk_real_int64 405505469971976L);(* 14, 14 *)\r
  62 (mk_real_int64 428370319478712L),(mk_real_int64 200996725344373L);(* 14, 14 *)\r
  63 (mk_real_int64 323014944067595L),(mk_real_int64 802180352622636L);(* 14, 14 *)\r
  64 (mk_real_int64 136410553525698L),(mk_real_int64 171519957847992L);(* 14, 14 *)\r
  65 (mk_real_int64 755378179208730L),(mk_real_int64 393461749199548L);(* 14, 14 *)\r
  66 (mk_real_int64 684050481212478L),(mk_real_int64 551076901488000L);(* 14, 14 *)\r
  67 (mk_real_int64 609729761645697L),(mk_real_int64 541811233513341L);(* 14, 14 *)\r
  68 (mk_real_int64 362945078194498L),(mk_real_int64 638117671427124L);(* 14, 14 *)\r
  69 (mk_real_int64 271626924366687L),(mk_real_int64 562379720565696L);(* 14, 14 *)\r
  70 (mk_real_int64 628681413918503L),(mk_real_int64 290443445260440L);(* 14, 14 *)\r
  71 (mk_real_int64 369612864115468L),(mk_real_int64 392004698904540L);(* 14, 14 *)\r
  72 (mk_real_int64 773812084651807L),(mk_real_int64 408087711517040L);(* 14, 14 *)\r
  73 (mk_real_int64 565364999209028L),(mk_real_int64 254549586225772L);(* 14, 14 *)\r
  74 (mk_real_int64 369070953701116L),(mk_real_int64 310615753918140L);(* 14, 14 *)\r
  75 (mk_real_int64 843847343488960L),(mk_real_int64 343069567108764L);(* 14, 14 *)\r
  76 (mk_real_int64 434618877871152L),(mk_real_int64 209481069955696L);(* 14, 14 *)\r
  77 (mk_real_int64 628233275793400L),(mk_real_int64 442326067536087L);(* 14, 14 *)\r
  78 (mk_real_int64 162718822961304L),(mk_real_int64 638554322626425L);(* 14, 14 *)\r
  79 (mk_real_int64 556627522455486L),(mk_real_int64 180777466429038L);(* 14, 14 *)\r
  80 (mk_real_int64 780585292039465L),(mk_real_int64 217142256943520L);(* 14, 14 *)\r
  81 (mk_real_int64 394688199427381L),(mk_real_int64 538577941316352L);(* 14, 14 *)\r
  82 (mk_real_int64 132085440106110L),(mk_real_int64 351777186362208L);(* 14, 14 *)\r
  83 (mk_real_int64 555631801860552L),(mk_real_int64 574384162934925L);(* 14, 14 *)\r
  84 (mk_real_int64 933147773762346L),(mk_real_int64 529778910083616L);(* 14, 14 *)\r
  85 (mk_real_int64 829999592257460L),(mk_real_int64 355692692428580L);(* 14, 14 *)\r
  86 (mk_real_int64 415102133340375L),(mk_real_int64 334405961088486L);(* 14, 14 *)\r
  87 (mk_real_int64 483708974303577L),(mk_real_int64 786205272080510L);(* 14, 14 *)\r
  88 (mk_real_int64 711860919923023L),(mk_real_int64 307976528266407L);(* 14, 14 *)\r
  89 (mk_real_int64 273921420533046L),(mk_real_int64 834166782560034L);(* 14, 14 *)\r
  90 (mk_real_int64 729230212944502L),(mk_real_int64 387986583219456L);(* 14, 14 *)\r
  91 (mk_real_int64 262283189492104L),(mk_real_int64 271577027329725L);(* 14, 14 *)\r
  92 (mk_real_int64 748320579670056L),(mk_real_int64 387837325862055L);(* 14, 14 *)\r
  93 (mk_real_int64 259574359587584L),(mk_real_int64 252268784271024L);(* 14, 14 *)\r
  94 (mk_real_int64 529629469693475L),(mk_real_int64 698244387448599L);(* 14, 14 *)\r
  95 (mk_real_int64 467969089544880L),(mk_real_int64 417877847845446L);(* 14, 14 *)\r
  96 (mk_real_int64 521134107523944L),(mk_real_int64 538428518195560L);(* 14, 14 *)\r
  97 (mk_real_int64 145508463152400L),(mk_real_int64 238249527243963L);(* 14, 14 *)\r
  98 (mk_real_int64 462229618103296L),(mk_real_int64 117753449871512L);(* 14, 14 *)\r
  99 (mk_real_int64 673175608756080L),(mk_real_int64 298509199253454L);(* 14, 14 *)\r
 100 (mk_real_int64 457904017658778L),(mk_real_int64 501294611820290L);(* 14, 14 *)\r
 101 (mk_real_int64 298454241997198L),(mk_real_int64 185361038600271L);(* 14, 14 *)\r
 102 (mk_real_int64 462002361828392L),(mk_real_int64 681368380154709L);(* 14, 14 *)\r
 103 (mk_real_int64 144783148181035L),(mk_real_int64 296957261215536L);(* 14, 14 *)\r
 104 (mk_real_int64 509181522064462L),(mk_real_int64 361478003577652L);(* 14, 14 *)\r
 105 (mk_real_int64 252781905558039L),(mk_real_int64 183649445379505L);(* 14, 14 *)\r
 106 (mk_real_int64 381261992115303L),(mk_real_int64 681558069096648L);(* 14, 14 *)\r
 107 (mk_real_int64 486767414899650L),(mk_real_int64 125978964147625L);(* 14, 14 *)\r
 108 (mk_real_int64 675595169265050L),(mk_real_int64 515434028588322L);(* 14, 14 *)\r
 109 (mk_real_int64 637143840347950L),(mk_real_int64 415900907551070L);(* 14, 14 *)\r
 110 (mk_real_int64 812253320086096L),(mk_real_int64 468701861485150L);(* 14, 14 *)\r
 111 (mk_real_int64 822222199619600L),(mk_real_int64 412038121629696L);(* 14, 14 *)\r
 112 (mk_real_int64 636953290225000L),(mk_real_int64 172669555938750L);(* 14, 14 *)\r
 113 (mk_real_int64 534768049107240L),(mk_real_int64 677432489728568L);(* 14, 14 *)\r
 114 (mk_real_int64 235415145947312L),(mk_real_int64 819676510474176L);(* 14, 14 *)\r
 115 (mk_real_int64 684023252882046L),(mk_real_int64 200398986010272L);(* 14, 14 *)\r
 116 (mk_real_int64 240317062183068L),(mk_real_int64 765007899782938L);(* 14, 14 *)\r
 117 (mk_real_int64 725138825407488L),(mk_real_int64 636606741195216L);(* 14, 14 *)\r
 118 (mk_real_int64 461888666812328L),(mk_real_int64 300659646917376L);(* 14, 14 *)\r
 119 (mk_real_int64 348969015873514L),(mk_real_int64 329003280879910L);(* 14, 14 *)\r
 120 (mk_real_int64 717253452670330L),(mk_real_int64 468942198628055L);(* 14, 14 *)\r
 121 (mk_real_int64 199176173959870L),(mk_real_int64 333318394782932L);(* 14, 14 *)\r
 122 (mk_real_int64 691427595574564L),(mk_real_int64 762813696952134L);(* 14, 14 *)\r
 123 (mk_real_int64 399650967537282L),(mk_real_int64 515666816995950L);(* 14, 14 *)\r
 124 (mk_real_int64 584619907378980L),(mk_real_int64 215216842431210L);(* 14, 14 *)\r
 125 (mk_real_int64 536423826564339L),(mk_real_int64 376626025721715L);(* 14, 14 *)\r
 126 (mk_real_int64 440728276506792L),(mk_real_int64 664195476119130L);(* 14, 14 *)\r
 127 (mk_real_int64 615611480344490L),(mk_real_int64 327888426524672L);(* 14, 14 *)\r
 128 (mk_real_int64 209640501275520L),(mk_real_int64 132166263337640L);(* 14, 14 *)\r
 129 (mk_real_int64 558237992229038L),(mk_real_int64 412751392690728L);(* 14, 14 *)\r
 130 (mk_real_int64 785490342963948L),(mk_real_int64 806368903933776L);(* 14, 14 *)\r
 131 (mk_real_int64 642596512049120L),(mk_real_int64 741244819991000L);(* 14, 14 *)\r
 132 (mk_real_int64 580226064753600L),(mk_real_int64 383907999627822L);(* 14, 14 *)\r
 133 (mk_real_int64 276707760318400L),(mk_real_int64 549973348743588L);(* 14, 14 *)\r
 134 (mk_real_int64 319275679911897L),(mk_real_int64 505527729671400L);(* 14, 14 *)\r
 135 (mk_real_int64 464996107696136L),(mk_real_int64 579515788972614L);(* 14, 14 *)\r
 136 (mk_real_int64 401725951162200L),(mk_real_int64 210061067264830L);(* 14, 14 *)\r
 137 (mk_real_int64 652094227735297L),(mk_real_int64 433523184430465L);(* 14, 14 *)\r
 138 (mk_real_int64 324568750483855L),(mk_real_int64 292423870305900L);(* 14, 14 *)\r
 139 (mk_real_int64 524145900463738L),(mk_real_int64 386996916791660L);(* 14, 14 *)\r
 140 (mk_real_int64 308993200647930L),(mk_real_int64 881687092434610L);(* 14, 14 *)\r
 141 (mk_real_int64 478219999325865L),(mk_real_int64 896883424272412L);(* 14, 14 *)\r
 142 (mk_real_int64 319397368414410L),(mk_real_int64 496241394700596L);(* 14, 14 *)\r
 143 (mk_real_int64 452205750244860L),(mk_real_int64 373524558180264L);(* 14, 14 *)\r
 144 (mk_real_int64 496532935594288L),(mk_real_int64 358147638142056L);(* 14, 14 *)\r
 145 (mk_real_int64 147216537711029L),(mk_real_int64 233486842289280L);(* 14, 14 *)\r
 146 (mk_real_int64 396831824282848L),(mk_real_int64 539349465184365L);(* 14, 14 *)\r
 147 (mk_real_int64 723656692628776L),(mk_real_int64 786215585628618L);(* 14, 14 *)\r
 148 (mk_real_int64 119394463335256L),(mk_real_int64 825713240570278L);(* 14, 14 *)\r
 149 (mk_real_int64 326362496734770L),(mk_real_int64 360753474294437L);(* 14, 14 *)\r
 150 (mk_real_int64 340052639982900L),(mk_real_int64 356041565761595L);(* 14, 14 *)\r
 151 (mk_real_int64 335249974420020L),(mk_real_int64 335028810981410L);(* 14, 14 *)\r
 152 (mk_real_int64 198442167102360L),(mk_real_int64 553776823015345L);(* 14, 14 *)\r
 153 (mk_real_int64 540460291862520L),(mk_real_int64 377209737210504L);(* 14, 14 *)\r
 154 (mk_real_int64 617018054416116L),(mk_real_int64 199298486037322L);(* 14, 14 *)\r
 155 (mk_real_int64 175105737246000L),(mk_real_int64 349641711638247L);(* 14, 14 *)\r
 156 (mk_real_int64 528678417495746L),(mk_real_int64 204389631628872L);(* 14, 14 *)\r
 157 (mk_real_int64 280392429043442L),(mk_real_int64 813770888392000L);(* 14, 14 *)\r
 158 (mk_real_int64 196258862678092L),(mk_real_int64 566453035021239L);(* 14, 14 *)\r
 159 (mk_real_int64 506041985601164L),(mk_real_int64 349764767744898L);(* 14, 14 *)\r
 160 (mk_real_int64 655798802064208L),(mk_real_int64 782963275501160L);(* 14, 14 *)\r
 161 (mk_real_int64 555522682226915L),(mk_real_int64 662518802409450L);(* 14, 14 *)\r
 162 (mk_real_int64 495712725106190L),(mk_real_int64 239941356168561L);(* 14, 14 *)\r
 163 (mk_real_int64 949445981245198L),(mk_real_int64 527008708559196L);(* 14, 14 *)\r
 164 (mk_real_int64 555249091031480L),(mk_real_int64 143395360604720L);(* 14, 14 *)\r
 165 (mk_real_int64 713544877485336L),(mk_real_int64 256168557082752L);(* 14, 14 *)\r
 166 (mk_real_int64 467231941918730L),(mk_real_int64 633877701237600L);(* 14, 14 *)\r
 167 (mk_real_int64 270119092698672L),(mk_real_int64 200700498213611L);(* 14, 14 *)\r
 168 (mk_real_int64 340191736121016L),(mk_real_int64 349466807332237L);(* 14, 14 *)\r
 169 (mk_real_int64 417066812290821L),(mk_real_int64 618037866309760L);(* 14, 14 *)\r
 170 (mk_real_int64 191634817098459L),(mk_real_int64 195328792461944L);(* 14, 14 *)\r
 171 (mk_real_int64 458368556437692L),(mk_real_int64 276657680509798L);(* 14, 14 *)\r
 172 (mk_real_int64 270484694390981L),(mk_real_int64 185838698248920L);(* 14, 14 *)\r
 173 (mk_real_int64 423290078720027L),(mk_real_int64 558366569976510L);(* 14, 14 *)\r
 174 (mk_real_int64 441459494248410L),(mk_real_int64 210934384721119L);(* 14, 14 *)\r
 175 (mk_real_int64 334405914589968L),(mk_real_int64 237655814054880L);(* 14, 14 *)\r
 176 (mk_real_int64 642586851795798L),(mk_real_int64 624579346128006L);(* 14, 14 *)\r
 177 (mk_real_int64 744219044666464L),(mk_real_int64 302145247152084L);(* 14, 14 *)\r
 178 (mk_real_int64 407533481554356L),(mk_real_int64 640355645688256L);(* 14, 14 *)\r
 179 (mk_real_int64 200535624042650L),(mk_real_int64 861581837619072L);(* 14, 14 *)\r
 180 (mk_real_int64 470765587636264L),(mk_real_int64 291762483604876L);(* 14, 14 *)\r
 181 (mk_real_int64 297694007494552L),(mk_real_int64 312850660690590L);(* 14, 14 *)\r
 182 (mk_real_int64 394323002617581L),(mk_real_int64 663902157462544L);(* 14, 14 *)\r
 183 (mk_real_int64 476802838904832L),(mk_real_int64 672875755825938L);(* 14, 14 *)\r
 184 (mk_real_int64 546625114912338L),(mk_real_int64 564423049949520L);(* 14, 14 *)\r
 185 (mk_real_int64 400627677455460L),(mk_real_int64 500915717800671L);(* 14, 14 *)\r
 186 (mk_real_int64 629695821813506L),(mk_real_int64 485679623259186L);(* 14, 14 *)\r
 187 (mk_real_int64 305527027108815L),(mk_real_int64 164503455378368L);(* 14, 14 *)\r
 188 (mk_real_int64 394997058713510L),(mk_real_int64 527758662637920L);(* 14, 14 *)\r
 189 (mk_real_int64 275767869678348L),(mk_real_int64 234003021915552L);(* 14, 14 *)\r
 190 (mk_real_int64 242056825321344L),(mk_real_int64 652688073050535L);(* 14, 14 *)\r
 191 (mk_real_int64 444414020817650L),(mk_real_int64 414154328932084L);(* 14, 14 *)\r
 192 (mk_real_int64 209494746669120L),(mk_real_int64 308600174486422L);(* 14, 14 *)\r
 193 (mk_real_int64 501532898275305L),(mk_real_int64 498395262003840L);(* 14, 14 *)\r
 194 (mk_real_int64 498864301758304L),(mk_real_int64 681115649847150L);(* 14, 14 *)\r
 195 (mk_real_int64 260043309321028L),(mk_real_int64 538129203997686L);(* 14, 14 *)\r
 196 (mk_real_int64 395163479535144L),(mk_real_int64 416814290794335L);(* 14, 14 *)\r
 197 (mk_real_int64 327191842372185L),(mk_real_int64 224622269666479L);(* 14, 14 *)\r
 198 (mk_real_int64 169221002391336L),(mk_real_int64 502784361254590L);(* 14, 14 *)\r
 199 (mk_real_int64 790543963829457L),(mk_real_int64 342054121502720L);(* 14, 14 *)\r
 200 (mk_real_int64 218257712167675L),(mk_real_int64 322079271090808L);(* 14, 14 *)\r
 201 (mk_real_int64 857438425700448L),(mk_real_int64 362981450501558L);(* 14, 14 *)\r
 202 (mk_real_int64 177965860744700L),(mk_real_int64 397644092902404L);(* 14, 14 *)\r
 203 (mk_real_int64 740166918080505L),(mk_real_int64 539751051095536L);(* 14, 14 *)\r
 204 (mk_real_int64 281843150621022L),(mk_real_int64 751637415644416L);(* 14, 14 *)\r
 205 (mk_real_int64 559652596638696L),(mk_real_int64 147575048807604L);(* 14, 14 *)\r
 206 (mk_real_int64 384944994467998L),(mk_real_int64 808019044103479L);(* 14, 14 *)\r
 207 (mk_real_int64 548600719167896L),(mk_real_int64 341385839953230L);(* 14, 14 *)\r
 208 (mk_real_int64 600673210227680L),(mk_real_int64 158061600512010L);(* 14, 14 *)\r
 209 (mk_real_int64 576544880969028L),(mk_real_int64 414105666520968L);(* 14, 14 *)\r
 210 (mk_real_int64 362835843555383L),(mk_real_int64 190564773269344L);(* 14, 14 *)\r
 211 (mk_real_int64 777882158637216L),(mk_real_int64 330721899229040L);(* 14, 14 *)\r
 212 (mk_real_int64 379396495399068L),(mk_real_int64 273051307857216L);(* 14, 14 *)\r
 213 (mk_real_int64 404197248976950L),(mk_real_int64 256205529026988L);(* 14, 14 *)\r
 214 (mk_real_int64 250687800785475L),(mk_real_int64 521917918571340L);(* 14, 14 *)\r
 215 (mk_real_int64 706078002255360L),(mk_real_int64 118152214795063L);(* 14, 14 *)\r
 216 (mk_real_int64 669115406447442L),(mk_real_int64 188055865373175L);(* 14, 14 *)\r
 217 (mk_real_int64 228130771126770L),(mk_real_int64 476101650918961L);(* 14, 14 *)\r
 218 (mk_real_int64 322669556969264L),(mk_real_int64 464223635275414L);(* 14, 14 *)\r
 219 (mk_real_int64 241911411325731L),(mk_real_int64 424788294384629L);(* 14, 14 *)\r
 220 (mk_real_int64 271930275661600L),(mk_real_int64 325877156885715L);(* 14, 14 *)\r
 221 (mk_real_int64 184872188619888L),(mk_real_int64 607784075874201L);(* 14, 14 *)\r
 222 (mk_real_int64 233113628329417L),(mk_real_int64 440700726437550L);(* 14, 14 *)\r
 223 (mk_real_int64 589524793880772L),(mk_real_int64 327910083154415L);(* 14, 14 *)\r
 224 (mk_real_int64 319816043947344L),(mk_real_int64 328682225331600L);(* 14, 14 *)\r
 225 (mk_real_int64 216114582970244L),(mk_real_int64 527890798290961L);(* 14, 14 *)\r
 226 (mk_real_int64 251239147254088L),(mk_real_int64 294354684052551L);(* 14, 14 *)\r
 227 (mk_real_int64 333003922482888L),(mk_real_int64 266705541890616L);(* 14, 14 *)\r
 228 (mk_real_int64 393522825190706L),(mk_real_int64 442847484547072L);(* 14, 14 *)\r
 229 (mk_real_int64 369521962372986L),(mk_real_int64 280063338470824L);(* 14, 14 *)\r
 230 (mk_real_int64 801756162834120L),(mk_real_int64 515640473908950L);(* 14, 14 *)\r
 231 (mk_real_int64 564901775975198L),(mk_real_int64 338684427678432L);(* 14, 14 *)\r
 232 (mk_real_int64 580317241750680L),(mk_real_int64 295865702326716L);(* 14, 14 *)\r
 233 (mk_real_int64 296419888316025L),(mk_real_int64 530374441251655L);(* 14, 14 *)\r
 234 (mk_real_int64 135041450276581L),(mk_real_int64 694004195994620L);(* 14, 14 *)\r
 235 (mk_real_int64 344660126730843L),(mk_real_int64 471224502771876L);(* 14, 14 *)\r
 236 (mk_real_int64 324528723453942L),(mk_real_int64 148271593003164L);(* 14, 14 *)\r
 237 (mk_real_int64 274238571381768L),(mk_real_int64 456761984781798L);(* 14, 14 *)\r
 238 (mk_real_int64 440150781069404L),(mk_real_int64 165535748272296L);(* 14, 14 *)\r
 239 (mk_real_int64 775477720878770L),(mk_real_int64 735322939451527L);(* 14, 14 *)\r
 240 (mk_real_int64 162143883456272L),(mk_real_int64 229928260815033L);(* 14, 14 *)\r
 241 (mk_real_int64 258521503478406L),(mk_real_int64 210092056448400L);(* 14, 14 *)\r
 242 (mk_real_int64 320027427319587L),(mk_real_int64 125234314739025L);(* 14, 14 *)\r
 243 (mk_real_int64 235014928587008L),(mk_real_int64 199506949581375L);(* 14, 14 *)\r
 244 (mk_real_int64 296492812021440L),(mk_real_int64 457097533597506L);(* 14, 14 *)\r
 245 (mk_real_int64 229763219483676L),(mk_real_int64 305184305616176L);(* 14, 14 *)\r
 246 (mk_real_int64 312660180536166L),(mk_real_int64 462797655770880L);(* 14, 14 *)\r
 247 (mk_real_int64 438646643738472L),(mk_real_int64 214203831432500L);(* 14, 14 *)\r
 248 (mk_real_int64 416290078764574L),(mk_real_int64 194963383241350L);(* 14, 14 *)\r
 249 (mk_real_int64 595707480652580L),(mk_real_int64 196858864427248L);(* 14, 14 *)\r
 250 (mk_real_int64 444282779519871L),(mk_real_int64 512571000331908L);(* 14, 14 *)\r
 251 (mk_real_int64 461080013276493L),(mk_real_int64 484608815603730L);(* 14, 14 *)\r
 252 (mk_real_int64 407202966771866L),(mk_real_int64 321262449505020L);(* 14, 14 *)\r
 253 (mk_real_int64 563650771041792L),(mk_real_int64 621676176592570L);(* 14, 14 *)\r
 254 (mk_real_int64 271073876509009L),(mk_real_int64 700042450267362L);(* 14, 14 *)\r
 255 (mk_real_int64 331519481127499L),(mk_real_int64 566860593086976L);(* 14, 14 *)\r
 256 (mk_real_int64 198722822828871L),(mk_real_int64 613580488719400L);(* 14, 14 *)\r
 257 (mk_real_int64 403267480068027L),(mk_real_int64 463566591530040L);(* 14, 14 *)\r
 258 (mk_real_int64 534611026120720L),(mk_real_int64 546584212563118L);(* 14, 14 *)\r
 259 (mk_real_int64 483817999775832L),(mk_real_int64 426480628544240L);(* 14, 14 *)\r
 260 (mk_real_int64 716558937058195L),(mk_real_int64 421793480570660L);(* 14, 14 *)\r
 261 (mk_real_int64 534449108640700L),(mk_real_int64 497080516821730L);(* 14, 14 *)\r
 262 (mk_real_int64 474586541052637L),(mk_real_int64 548611857419640L);(* 14, 14 *)\r
 263 (mk_real_int64 239054944946981L),(mk_real_int64 400412990171070L);(* 14, 14 *)\r
 264 (mk_real_int64 254686670905260L),(mk_real_int64 610384111359900L);(* 14, 14 *)\r
 265 (mk_real_int64 319309454589342L),(mk_real_int64 676086791747862L);(* 14, 14 *)\r
 266 (mk_real_int64 322927105851560L),(mk_real_int64 450226061594541L);(* 14, 14 *)\r
 267 (mk_real_int64 346858386741440L),(mk_real_int64 308362556543147L);(* 14, 14 *)\r
 268 (mk_real_int64 174319133977000L),(mk_real_int64 388500231425014L);(* 14, 14 *)\r
 269 (mk_real_int64 297531671619022L),(mk_real_int64 803851493944752L);(* 14, 14 *)\r
 270 (mk_real_int64 351493987577056L),(mk_real_int64 679632629934336L);(* 14, 14 *)\r
 271 (mk_real_int64 461128827565494L),(mk_real_int64 723465870410357L);(* 14, 14 *)\r
 272 (mk_real_int64 449399023526642L),(mk_real_int64 671190839522140L);(* 14, 14 *)\r
 273 (mk_real_int64 177522985924344L),(mk_real_int64 368132988069441L);(* 14, 14 *)\r
 274 (mk_real_int64 288223257219726L),(mk_real_int64 702022482682779L);(* 14, 14 *)\r
 275 (mk_real_int64 404049127270880L),(mk_real_int64 578225861031780L);(* 14, 14 *)\r
 276 (mk_real_int64 314316010228192L),(mk_real_int64 470001783295814L);(* 14, 14 *)\r
 277 (mk_real_int64 443421150296283L),(mk_real_int64 386614551796228L);(* 14, 14 *)\r
 278 (mk_real_int64 749612952040888L),(mk_real_int64 608795413661736L);(* 14, 14 *)\r
 279 (mk_real_int64 253550217757914L),(mk_real_int64 302287744860507L);(* 14, 14 *)\r
 280 (mk_real_int64 319755488352132L),(mk_real_int64 225213516540112L);(* 14, 14 *)\r
 281 (mk_real_int64 247745112357240L),(mk_real_int64 373499663825270L);(* 14, 14 *)\r
 282 (mk_real_int64 227602560011511L),(mk_real_int64 572921042132628L);(* 14, 14 *)\r
 283 (mk_real_int64 620647455959620L),(mk_real_int64 429734623718653L);(* 14, 14 *)\r
 284 (mk_real_int64 675844269012384L),(mk_real_int64 337057722320208L);(* 14, 14 *)\r
 285 (mk_real_int64 602798397514020L),(mk_real_int64 304861015600186L);(* 14, 14 *)\r
 286 (mk_real_int64 718028875754512L),(mk_real_int64 553971771137120L);(* 14, 14 *)\r
 287 (mk_real_int64 141215423835536L),(mk_real_int64 522077762747413L);(* 14, 14 *)\r
 288 (mk_real_int64 287084888668440L),(mk_real_int64 234670545423444L);(* 14, 14 *)\r
 289 (mk_real_int64 936085538917134L),(mk_real_int64 595253232679284L);(* 14, 14 *)\r
 290 (mk_real_int64 185806543261605L),(mk_real_int64 130786743585888L);(* 14, 14 *)\r
 291 (mk_real_int64 768976488474740L),(mk_real_int64 254896272054320L);(* 14, 14 *)\r
 292 (mk_real_int64 787568354309232L),(mk_real_int64 589565293992950L);(* 14, 14 *)\r
 293 (mk_real_int64 800369274634204L),(mk_real_int64 731727206172534L);(* 14, 14 *)\r
 294 (mk_real_int64 681762086600025L),(mk_real_int64 289919376203408L);(* 14, 14 *)\r
 295 (mk_real_int64 313805662108440L),(mk_real_int64 241168395509982L);(* 14, 14 *)\r
 296 (mk_real_int64 836467497798579L),(mk_real_int64 323699840048769L);(* 14, 14 *)\r
 297 (mk_real_int64 399889997038950L),(mk_real_int64 265792091781525L);(* 14, 14 *)\r
 298 (mk_real_int64 234922718349520L),(mk_real_int64 246361999063329L);(* 14, 14 *)\r
 299 (mk_real_int64 450308370528550L),(mk_real_int64 621963990492714L);(* 14, 14 *)\r
 300 (mk_real_int64 174937646293816L),(mk_real_int64 696970265178186L);(* 14, 14 *)\r
 301 (mk_real_int64 637292191841105L),(mk_real_int64 472344257630570L);(* 14, 14 *)\r
 302 (mk_real_int64 299319456130494L),(mk_real_int64 658057841993448L);(* 14, 14 *)\r
 303 (mk_real_int64 153493465191682L),(mk_real_int64 633008648900040L);(* 14, 14 *)\r
 304 (mk_real_int64 373384739133607L),(mk_real_int64 454057793033413L);(* 14, 14 *)\r
 305 (mk_real_int64 717975474751284L),(mk_real_int64 197120324640422L);(* 14, 14 *)\r
 306 (mk_real_int64 477209188519906L),(mk_real_int64 749186552904624L);(* 14, 14 *)\r
 307 (mk_real_int64 214099355294520L),(mk_real_int64 254214233384007L);(* 14, 14 *)\r
 308 (mk_real_int64 633371645531676L),(mk_real_int64 704851940502717L);(* 14, 14 *)\r
 309 (mk_real_int64 575212223410209L),(mk_real_int64 477463676314455L);(* 14, 14 *)\r
 310 (mk_real_int64 199012028826600L),(mk_real_int64 576073296128355L);(* 14, 14 *)\r
 311 (mk_real_int64 197844374404912L),(mk_real_int64 731744543961557L);(* 14, 14 *)\r
 312 (mk_real_int64 615059159620256L),(mk_real_int64 515767570368078L);(* 14, 14 *)\r
 313 (mk_real_int64 592801870638654L),(mk_real_int64 188875018438092L);(* 14, 14 *)\r
 314 (mk_real_int64 455317589985264L),(mk_real_int64 680981157665025L);(* 14, 14 *)\r
 315 (mk_real_int64 883229167772844L),(mk_real_int64 432449616649864L);(* 14, 14 *)\r
 316 (mk_real_int64 241340357015100L),(mk_real_int64 126823079865222L);(* 14, 14 *)\r
 317 (mk_real_int64 446219438497520L),(mk_real_int64 267243368587936L);(* 14, 14 *)\r
 318 (mk_real_int64 501283036978919L),(mk_real_int64 627153034024176L);(* 14, 14 *)\r
 319 (mk_real_int64 648083797686110L),(mk_real_int64 430608361075235L);(* 14, 14 *)\r
 320 (mk_real_int64 749821147709546L),(mk_real_int64 375461068521700L);(* 14, 14 *)\r
 321 (mk_real_int64 723319778661205L),(mk_real_int64 451097515880037L);(* 14, 14 *)\r
 322 (mk_real_int64 345245039645800L),(mk_real_int64 447644588507760L);(* 14, 14 *)\r
 323 (mk_real_int64 616743657064890L),(mk_real_int64 320595470429988L);(* 14, 14 *)\r
 324 (mk_real_int64 379829759705232L),(mk_real_int64 150825472859484L);(* 14, 14 *)\r
 325 (mk_real_int64 162217253302844L),(mk_real_int64 296590042061860L);(* 14, 14 *)\r
 326 (mk_real_int64 300736517861472L),(mk_real_int64 527962577170875L);(* 14, 14 *)\r
 327 (mk_real_int64 509980939317108L),(mk_real_int64 284817204434790L);(* 14, 14 *)\r
 328 (mk_real_int64 110737825109723L),(mk_real_int64 383322857894700L);(* 14, 14 *)\r
 329 (mk_real_int64 501459617356328L),(mk_real_int64 198107714351365L);(* 14, 14 *)\r
 330 (mk_real_int64 605965193127112L),(mk_real_int64 372605726134629L);(* 14, 14 *)\r
 331 (mk_real_int64 235198300213030L),(mk_real_int64 239997786964141L);(* 14, 14 *)\r
 332 (mk_real_int64 252557007276320L),(mk_real_int64 206191464147240L);(* 14, 14 *)\r
 333 (mk_real_int64 620021190631680L),(mk_real_int64 535624120842258L);(* 14, 14 *)\r
 334 (mk_real_int64 347852781872368L),(mk_real_int64 493174452056215L);(* 14, 14 *)\r
 335 (mk_real_int64 384111010952135L),(mk_real_int64 309040239119556L);(* 14, 14 *)\r
 336 (mk_real_int64 478475966695024L),(mk_real_int64 328337939393075L);(* 14, 14 *)\r
 337 (mk_real_int64 241154452963984L),(mk_real_int64 490204504789230L);(* 14, 14 *)\r
 338 (mk_real_int64 478020556073716L),(mk_real_int64 607077659783658L);(* 14, 14 *)\r
 339 (mk_real_int64 326503808969037L),(mk_real_int64 284782227576980L);(* 14, 14 *)\r
 340 (mk_real_int64 321825878741283L),(mk_real_int64 692197732501176L);(* 14, 14 *)\r
 341 (mk_real_int64 211034403160995L),(mk_real_int64 313969149858544L);(* 14, 14 *)\r
 342 (mk_real_int64 151454282960388L),(mk_real_int64 559425764930025L);(* 14, 14 *)\r
 343 (mk_real_int64 200029796122780L),(mk_real_int64 385911311390642L);(* 14, 14 *)\r
 344 (mk_real_int64 421115518794960L),(mk_real_int64 167915987663480L);(* 14, 14 *)\r
 345 (mk_real_int64 694995691825740L),(mk_real_int64 246341494942760L);(* 14, 14 *)\r
 346 (mk_real_int64 370867602134274L),(mk_real_int64 701000286926336L);(* 14, 14 *)\r
 347 (mk_real_int64 185171369917508L),(mk_real_int64 415437369735123L);(* 14, 14 *)\r
 348 (mk_real_int64 353505345990291L),(mk_real_int64 350112364813827L);(* 14, 14 *)\r
 349 (mk_real_int64 323905966911432L),(mk_real_int64 236818421167189L);(* 14, 14 *)\r
 350 (mk_real_int64 130011870002726L),(mk_real_int64 396671712594960L);(* 14, 14 *)\r
 351 (mk_real_int64 417662161716247L),(mk_real_int64 323992253306880L);(* 14, 14 *)\r
 352 (mk_real_int64 365867492581226L),(mk_real_int64 408667929660936L);(* 14, 14 *)\r
 353 (mk_real_int64 449586581704530L),(mk_real_int64 285508424761716L);(* 14, 14 *)\r
 354 (mk_real_int64 690380857728139L),(mk_real_int64 377861145080111L);(* 14, 14 *)\r
 355 (mk_real_int64 946827733646620L),(mk_real_int64 284430710888456L);(* 14, 14 *)\r
 356 (mk_real_int64 428311255088750L),(mk_real_int64 615634304102972L);(* 14, 14 *)\r
 357 (mk_real_int64 218967670786000L),(mk_real_int64 211804715915600L);(* 14, 14 *)\r
 358 (mk_real_int64 658350667242144L),(mk_real_int64 280173784789605L);(* 14, 14 *)\r
 359 (mk_real_int64 848734281032930L),(mk_real_int64 365607885313251L);(* 14, 14 *)\r
 360 (mk_real_int64 721743133316492L),(mk_real_int64 280021436018634L);(* 14, 14 *)\r
 361 (mk_real_int64 511928938049781L),(mk_real_int64 585613865311409L);(* 14, 14 *)\r
 362 (mk_real_int64 166694008918976L),(mk_real_int64 143889951701603L);(* 14, 14 *)\r
 363 (mk_real_int64 277342533758640L),(mk_real_int64 912525759796140L);(* 14, 14 *)\r
 364 (mk_real_int64 209211461740827L),(mk_real_int64 720120780147096L);(* 14, 14 *)\r
 365 (mk_real_int64 338892460331362L),(mk_real_int64 513560594673540L);(* 14, 14 *)\r
 366 (mk_real_int64 531644440460000L),(mk_real_int64 632912570827016L);(* 14, 14 *)\r
 367 (mk_real_int64 445731691968976L),(mk_real_int64 204549944638312L);(* 14, 14 *)\r
 368 (mk_real_int64 537591141477299L),(mk_real_int64 489311274090576L);(* 14, 14 *)\r
 369 (mk_real_int64 581845841754450L),(mk_real_int64 204285583619260L);(* 14, 14 *)\r
 370 (mk_real_int64 508510475575896L),(mk_real_int64 512229184659008L);(* 14, 14 *)\r
 371 (mk_real_int64 645153181647492L),(mk_real_int64 278402984479668L);(* 14, 14 *)\r
 372 (mk_real_int64 137501106965235L),(mk_real_int64 127197565397460L);(* 14, 14 *)\r
 373 (mk_real_int64 263319151634605L),(mk_real_int64 574506146499450L);(* 14, 14 *)\r
 374 (mk_real_int64 408663642726861L),(mk_real_int64 159987099067920L);(* 14, 14 *)\r
 375 (mk_real_int64 568621401716040L),(mk_real_int64 189102846648485L);(* 14, 14 *)\r
 376 (mk_real_int64 576810012457574L),(mk_real_int64 834075215493680L);(* 14, 14 *)\r
 377 (mk_real_int64 454709922624880L),(mk_real_int64 507249510583390L);(* 14, 14 *)\r
 378 (mk_real_int64 300098149496880L),(mk_real_int64 307754117792226L);(* 14, 14 *)\r
 379 (mk_real_int64 526451740573737L),(mk_real_int64 476000849647180L);(* 14, 14 *)\r
 380 (mk_real_int64 714737455873614L),(mk_real_int64 438646418654900L);(* 14, 14 *)\r
 381 (mk_real_int64 648959792972722L),(mk_real_int64 313656052407866L);(* 14, 14 *)\r
 382 (mk_real_int64 447460729631850L),(mk_real_int64 816032432921792L);(* 14, 14 *)\r
 383 (mk_real_int64 204899940724930L),(mk_real_int64 854395280929707L);(* 14, 14 *)\r
 384 (mk_real_int64 535205103241169L),(mk_real_int64 583804279832000L);(* 14, 14 *)\r
 385 (mk_real_int64 274668182827798L),(mk_real_int64 452734297586495L);(* 14, 14 *)\r
 386 (mk_real_int64 304914642986602L),(mk_real_int64 177627670110908L);(* 14, 14 *)\r
 387 (mk_real_int64 817279687758366L),(mk_real_int64 847317232316640L);(* 14, 14 *)\r
 388 (mk_real_int64 335667957851248L),(mk_real_int64 645770937150384L);(* 14, 14 *)\r
 389 (mk_real_int64 715199407112120L),(mk_real_int64 175051260725986L);(* 14, 14 *)\r
 390 (mk_real_int64 705597711583776L),(mk_real_int64 401140748617560L);(* 14, 14 *)\r
 391 (mk_real_int64 133543616636958L),(mk_real_int64 794289415029708L);(* 14, 14 *)\r
 392 (mk_real_int64 195150747200772L),(mk_real_int64 493008669386742L);(* 14, 14 *)\r
 393 (mk_real_int64 360403901482725L),(mk_real_int64 485570191147672L);(* 14, 14 *)\r
 394 (mk_real_int64 853402363119955L),(mk_real_int64 591611895914272L);(* 14, 14 *)\r
 395 (mk_real_int64 261822572293737L),(mk_real_int64 425519750756221L);(* 14, 14 *)\r
 396 (mk_real_int64 561213063977790L),(mk_real_int64 223903320452306L);(* 14, 14 *)\r
 397 (mk_real_int64 718492027247601L),(mk_real_int64 124728090216800L);(* 14, 14 *)\r
 398 (mk_real_int64 724685764625055L),(mk_real_int64 197802173302685L);(* 14, 14 *)\r
 399 (mk_real_int64 290397462208533L),(mk_real_int64 579766439571748L);(* 14, 14 *)\r
 400 (mk_real_int64 154409647820442L),(mk_real_int64 541920817609350L);(* 14, 14 *)\r
 401 (mk_real_int64 654285007939094L),(mk_real_int64 258829762930002L);(* 14, 14 *)\r
 402 (mk_real_int64 315359665303760L),(mk_real_int64 472299283076544L);(* 14, 14 *)\r
 403 (mk_real_int64 567953914662360L),(mk_real_int64 250386252869199L);(* 14, 14 *)\r
 404 (mk_real_int64 350691867941088L),(mk_real_int64 242681268803364L);(* 14, 14 *)\r
 405 (mk_real_int64 304788938412231L),(mk_real_int64 448910075254332L);(* 14, 14 *)\r
 406 (mk_real_int64 608132198936988L),(mk_real_int64 311185490457303L);(* 14, 14 *)\r
 407 (mk_real_int64 459214395553599L),(mk_real_int64 753911552065662L);(* 14, 14 *)\r
 408 (mk_real_int64 232802909947096L),(mk_real_int64 563120685306195L);(* 14, 14 *)\r
 409 (mk_real_int64 682178291741772L),(mk_real_int64 700104239364348L);(* 14, 14 *)\r
 410 (mk_real_int64 212961781558240L),(mk_real_int64 135518572797228L);(* 14, 14 *)\r
 411 (mk_real_int64 832228448580718L),(mk_real_int64 672552198631720L);(* 14, 14 *)\r
 412 (mk_real_int64 888971450466660L),(mk_real_int64 778561860539646L);(* 14, 14 *)\r
 413 (mk_real_int64 260714444341338L),(mk_real_int64 330391583671466L);(* 14, 14 *)\r
 414 (mk_real_int64 254337398475018L),(mk_real_int64 323388274481415L);(* 14, 14 *)\r
 415 (mk_real_int64 589092026220511L),(mk_real_int64 298771882739824L);(* 14, 14 *)\r
 416 (mk_real_int64 525020249786496L),(mk_real_int64 511606376139690L);(* 14, 14 *)\r
 417 (mk_real_int64 276282507311430L),(mk_real_int64 329572421020511L);(* 14, 14 *)\r
 418 (mk_real_int64 254182915914627L),(mk_real_int64 273595818133120L);(* 14, 14 *)\r
 419 (mk_real_int64 790949821261270L),(mk_real_int64 639850591427480L);(* 14, 14 *)\r
 420 (mk_real_int64 459385696269312L),(mk_real_int64 745337577516740L);(* 14, 14 *)\r
 421 (mk_real_int64 656959770026119L),(mk_real_int64 816167732165424L);(* 14, 14 *)\r
 422 (mk_real_int64 400346668530574L),(mk_real_int64 713375397363531L);(* 14, 14 *)\r
 423 (mk_real_int64 450921748647448L),(mk_real_int64 472250149612743L);(* 14, 14 *)\r
 424 (mk_real_int64 184845914397485L),(mk_real_int64 815771840516352L);(* 14, 14 *)\r
 425 (mk_real_int64 485550135694080L),(mk_real_int64 730836187559936L);(* 14, 14 *)\r
 426 (mk_real_int64 293019550619664L),(mk_real_int64 424006691696381L);(* 14, 14 *)\r
 427 (mk_real_int64 766911986571125L),(mk_real_int64 483480264465576L);(* 14, 14 *)\r
 428 (mk_real_int64 147930270810300L),(mk_real_int64 301359319749000L);(* 14, 14 *)\r
 429 (mk_real_int64 720513732547440L),(mk_real_int64 247958326593056L);(* 14, 14 *)\r
 430 (mk_real_int64 542530941365182L),(mk_real_int64 614438284446035L);(* 14, 14 *)\r
 431 (mk_real_int64 262544872512104L),(mk_real_int64 421783531057716L);(* 14, 14 *)\r
 432 (mk_real_int64 540825793168271L),(mk_real_int64 605524398040803L);(* 14, 14 *)\r
 433 (mk_real_int64 136712470567756L),(mk_real_int64 295610167857256L);(* 14, 14 *)\r
 434 (mk_real_int64 314286253763742L),(mk_real_int64 222791346299070L);(* 14, 14 *)\r
 435 (mk_real_int64 697155453298776L),(mk_real_int64 643645283640580L);(* 14, 14 *)\r
 436 (mk_real_int64 304198223340057L),(mk_real_int64 879272717581080L);(* 14, 14 *)\r
 437 (mk_real_int64 559954627241376L),(mk_real_int64 620713088907891L);(* 14, 14 *)\r
 438 (mk_real_int64 320192172138240L),(mk_real_int64 555120315626340L);(* 14, 14 *)\r
 439 (mk_real_int64 218618766984912L),(mk_real_int64 175507292601792L);(* 14, 14 *)\r
 440 (mk_real_int64 320913636291670L),(mk_real_int64 600649949676370L);(* 14, 14 *)\r
 441 (mk_real_int64 419584001038528L),(mk_real_int64 359339007207556L);(* 14, 14 *)\r
 442 (mk_real_int64 540571535652752L),(mk_real_int64 729063390272055L);(* 14, 14 *)\r
 443 (mk_real_int64 867328636501925L),(mk_real_int64 182230486261803L);(* 14, 14 *)\r
 444 (mk_real_int64 572411731757177L),(mk_real_int64 622483795886366L);(* 14, 14 *)\r
 445 (mk_real_int64 454716828819153L),(mk_real_int64 515263498916028L);(* 14, 14 *)\r
 446 (mk_real_int64 523929525121492L),(mk_real_int64 213494571300504L);(* 14, 14 *)\r
 447 (mk_real_int64 305126356206113L),(mk_real_int64 751079759759766L);(* 14, 14 *)\r
 448 (mk_real_int64 668250721031994L),(mk_real_int64 438217344609396L);(* 14, 14 *)\r
 449 (mk_real_int64 812312747546120L),(mk_real_int64 251742819157548L);(* 14, 14 *)\r
 450 (mk_real_int64 427545159075797L),(mk_real_int64 402515269217061L);(* 14, 14 *)\r
 451 (mk_real_int64 736520259942585L),(mk_real_int64 300614268785250L);(* 14, 14 *)\r
 452 (mk_real_int64 113670417077580L),(mk_real_int64 382888671428821L);(* 14, 14 *)\r
 453 (mk_real_int64 220907550360000L),(mk_real_int64 183017188568475L);(* 14, 14 *)\r
 454 (mk_real_int64 239798504389008L),(mk_real_int64 223672146085405L);(* 14, 14 *)\r
 455 (mk_real_int64 411615369630920L),(mk_real_int64 550341127415794L);(* 14, 14 *)\r
 456 (mk_real_int64 251102994852057L),(mk_real_int64 724662364742316L);(* 14, 14 *)\r
 457 (mk_real_int64 216207169348332L),(mk_real_int64 153651115563288L);(* 14, 14 *)\r
 458 (mk_real_int64 265186374526730L),(mk_real_int64 612532286336236L);(* 14, 14 *)\r
 459 (mk_real_int64 314927322086021L),(mk_real_int64 437863173099040L);(* 14, 14 *)\r
 460 (mk_real_int64 202042103055594L),(mk_real_int64 223538075733874L);(* 14, 14 *)\r
 461 (mk_real_int64 221167494199515L),(mk_real_int64 256050065441872L);(* 14, 14 *)\r
 462 (mk_real_int64 210859405081424L),(mk_real_int64 438287461768646L);(* 14, 14 *)\r
 463 (mk_real_int64 609033610480680L),(mk_real_int64 716505877240184L);(* 14, 14 *)\r
 464 (mk_real_int64 291541977608347L),(mk_real_int64 715998933910876L);(* 14, 14 *)\r
 465 (mk_real_int64 542236273592524L),(mk_real_int64 526438793041592L);(* 14, 14 *)\r
 466 (mk_real_int64 358239425660022L),(mk_real_int64 439666269321235L);(* 14, 14 *)\r
 467 (mk_real_int64 307975921543636L),(mk_real_int64 486427463641750L);(* 14, 14 *)\r
 468 (mk_real_int64 673536837278445L),(mk_real_int64 184223866927530L);(* 14, 14 *)\r
 469 (mk_real_int64 209831970073632L),(mk_real_int64 460050665433120L);(* 14, 14 *)\r
 470 (mk_real_int64 552104405477319L),(mk_real_int64 231973624166500L);(* 14, 14 *)\r
 471 (mk_real_int64 444365329006836L),(mk_real_int64 399706037011344L);(* 14, 14 *)\r
 472 (mk_real_int64 229997384570260L),(mk_real_int64 628084862849640L);(* 14, 14 *)\r
 473 (mk_real_int64 479999514424800L),(mk_real_int64 708581811939948L);(* 14, 14 *)\r
 474 (mk_real_int64 738464957427544L),(mk_real_int64 459798310444032L);(* 14, 14 *)\r
 475 (mk_real_int64 653284714320900L),(mk_real_int64 818386148868672L);(* 14, 14 *)\r
 476 (mk_real_int64 144096684612800L),(mk_real_int64 413418706745308L);(* 14, 14 *)\r
 477 (mk_real_int64 591479435374128L),(mk_real_int64 390781216393377L);(* 14, 14 *)\r
 478 (mk_real_int64 826682134372800L),(mk_real_int64 648839109408147L);(* 14, 14 *)\r
 479 (mk_real_int64 709403592830409L),(mk_real_int64 488339287510525L);(* 14, 14 *)\r
 480 (mk_real_int64 457113528866865L),(mk_real_int64 358648682654052L);(* 14, 14 *)\r
 481 (mk_real_int64 178461064852065L),(mk_real_int64 714540549678425L);(* 14, 14 *)\r
 482 (mk_real_int64 271555833747962L),(mk_real_int64 464695093013315L);(* 14, 14 *)\r
 483 (mk_real_int64 269854499766085L),(mk_real_int64 758705266978393L);(* 14, 14 *)\r
 484 (mk_real_int64 579193328897001L),(mk_real_int64 506057507584616L);(* 14, 14 *)\r
 485 (mk_real_int64 592807918976325L),(mk_real_int64 451912327542593L);(* 14, 14 *)\r
 486 (mk_real_int64 231442292051284L),(mk_real_int64 894902957784346L);(* 14, 14 *)\r
 487 (mk_real_int64 306614027776722L),(mk_real_int64 543489708815091L);(* 14, 14 *)\r
 488 (mk_real_int64 450257949207216L),(mk_real_int64 261968956458183L);(* 14, 14 *)\r
 489 (mk_real_int64 394369174361444L),(mk_real_int64 470186192332323L);(* 14, 14 *)\r
 490 (mk_real_int64 228356760582402L),(mk_real_int64 411424578059350L);(* 14, 14 *)\r
 491 (mk_real_int64 631166265992864L),(mk_real_int64 255589992393788L);(* 14, 14 *)\r
 492 (mk_real_int64 471133993562050L),(mk_real_int64 106796436325404L);(* 14, 14 *)\r
 493 (mk_real_int64 202378939457590L),(mk_real_int64 501124608873720L);(* 14, 14 *)\r
 494 (mk_real_int64 502686670709072L),(mk_real_int64 264808985782424L);(* 14, 14 *)\r
 495 (mk_real_int64 329658040849072L),(mk_real_int64 358739755376586L);(* 14, 14 *)\r
 496 (mk_real_int64 387436840701842L),(mk_real_int64 533923141421250L);(* 14, 14 *)\r
 497 (mk_real_int64 523490258455008L),(mk_real_int64 823405027863620L);(* 14, 14 *)\r
 498 (mk_real_int64 300095581763340L),(mk_real_int64 348366828293718L);(* 14, 14 *)\r
 499 (mk_real_int64 547963661603984L),(mk_real_int64 168937935721504L);(* 14, 14 *)\r
 500 (mk_real_int64 362248413268311L),(mk_real_int64 616389894532159L);(* 14, 14 *)\r
 501 (mk_real_int64 257960019608320L),(mk_real_int64 247032144833805L);(* 14, 14 *)\r
 502 (mk_real_int64 200519518487958L),(mk_real_int64 741974257482416L);(* 14, 14 *)\r
 503 (mk_real_int64 199379260872792L),(mk_real_int64 248326471900944L);(* 14, 14 *)\r
 504 (mk_real_int64 790684055753228L),(mk_real_int64 786433430318016L);(* 14, 14 *)\r
 505 (mk_real_int64 748998134147536L),(mk_real_int64 409900298978100L);(* 14, 14 *)\r
 506 (mk_real_int64 141379444193157L),(mk_real_int64 783011082748772L);(* 14, 14 *)\r
 507 (mk_real_int64 337709969129520L),(mk_real_int64 380282174153952L);(* 14, 14 *)\r
 508 (mk_real_int64 185769130480587L),(mk_real_int64 554843700594650L);(* 14, 14 *)\r
 509 (mk_real_int64 374930583476740L),(mk_real_int64 591498580052919L);(* 14, 14 *)\r
 510 (mk_real_int64 507810635816960L),(mk_real_int64 250435211923956L);(* 14, 14 *)\r
 511 (mk_real_int64 371575216781505L),(mk_real_int64 342769675430343L);(* 14, 14 *)\r
 512 (mk_real_int64 370409954642508L),(mk_real_int64 644888375155062L);(* 14, 14 *)\r
 513 (mk_real_int64 452313867539220L),(mk_real_int64 215128634727204L);(* 14, 14 *)\r
 514 (mk_real_int64 535512510993668L),(mk_real_int64 573980027463960L);(* 14, 14 *)\r
 515 (mk_real_int64 157246280372028L),(mk_real_int64 218052129413850L);(* 14, 14 *)\r
 516 (mk_real_int64 355540841043384L),(mk_real_int64 233671650737216L);(* 14, 14 *)\r
 517 (mk_real_int64 398861798671928L),(mk_real_int64 254408142012136L);(* 14, 14 *)\r
 518 (mk_real_int64 383082552257850L),(mk_real_int64 347287802872608L);(* 14, 14 *)\r
 519 (mk_real_int64 672738232373136L),(mk_real_int64 809306835283758L);(* 14, 14 *)\r
 520 (mk_real_int64 511579025091096L),(mk_real_int64 287484820856811L);(* 14, 14 *)\r
 521 (mk_real_int64 130517672620716L),(mk_real_int64 523234863852910L);(* 14, 14 *)\r
 522 (mk_real_int64 720769195231650L),(mk_real_int64 449145286747992L);(* 14, 14 *)\r
 523 (mk_real_int64 360242608161559L),(mk_real_int64 251547505894375L);(* 14, 14 *)\r
 524 (mk_real_int64 251839370695924L),(mk_real_int64 191265750289488L);(* 14, 14 *)\r
 525 (mk_real_int64 293734242063900L),(mk_real_int64 522204471166952L);(* 14, 14 *)\r
 526 (mk_real_int64 273366396121531L),(mk_real_int64 188388340868232L);(* 14, 14 *)\r
 527 (mk_real_int64 420297360384800L),(mk_real_int64 266322831169032L);(* 14, 14 *)\r
 528 (mk_real_int64 145767674013212L),(mk_real_int64 494918821666000L);(* 14, 14 *)\r
 529 (mk_real_int64 779636012457726L),(mk_real_int64 477967229752240L);(* 14, 14 *)\r
 530 (mk_real_int64 301136312364230L),(mk_real_int64 208237001472831L);(* 14, 14 *)\r
 531 (mk_real_int64 793869206035568L),(mk_real_int64 550520764618232L);(* 14, 14 *)\r
 532 (mk_real_int64 555522787535760L),(mk_real_int64 189681514192960L);(* 14, 14 *)\r
 533 (mk_real_int64 356170680559952L),(mk_real_int64 343072142499609L);(* 14, 14 *)\r
 534 (mk_real_int64 551125907708530L),(mk_real_int64 885557237296596L);(* 14, 14 *)\r
 535 (mk_real_int64 820210348169355L),(mk_real_int64 766498824333280L);(* 14, 14 *)\r
 536 (mk_real_int64 640835123352825L),(mk_real_int64 600456551580288L);(* 14, 14 *)\r
 537 (mk_real_int64 425344170765672L),(mk_real_int64 228361621541256L);(* 14, 14 *)\r
 538 (mk_real_int64 388342264778335L),(mk_real_int64 620697533883525L);(* 14, 14 *)\r
 539 (mk_real_int64 322992668287088L),(mk_real_int64 774903540525240L);(* 14, 14 *)\r
 540 (mk_real_int64 354498559753968L),(mk_real_int64 239340142680912L);(* 14, 14 *)\r
 541 (mk_real_int64 655811172600467L),(mk_real_int64 303007609123488L);(* 14, 14 *)\r
 542 (mk_real_int64 223187030821204L),(mk_real_int64 876371195873506L);(* 14, 14 *)\r
 543 (mk_real_int64 426656874014472L),(mk_real_int64 813923526014444L);(* 14, 14 *)\r
 544 (mk_real_int64 380840343693257L),(mk_real_int64 336637615674714L);(* 14, 14 *)\r
 545 (mk_real_int64 865895247465430L),(mk_real_int64 481178164821021L);(* 14, 14 *)\r
 546 (mk_real_int64 607067898284970L),(mk_real_int64 664341127051264L);(* 14, 14 *)\r
 547 (mk_real_int64 278522376483920L),(mk_real_int64 456589090915753L);(* 14, 14 *)\r
 548 (mk_real_int64 569154220760840L),(mk_real_int64 108447215549824L);(* 14, 14 *)\r
 549 (mk_real_int64 259868561936646L),(mk_real_int64 356032748971860L);(* 14, 14 *)\r
 550 (mk_real_int64 623651980661018L),(mk_real_int64 632572477277524L);(* 14, 14 *)\r
 551 (mk_real_int64 760796839815792L),(mk_real_int64 541910889773032L);(* 14, 14 *)\r
 552 (mk_real_int64 703798952573440L),(mk_real_int64 500422636762430L);(* 14, 14 *)\r
 553 (mk_real_int64 534112173388470L),(mk_real_int64 400690919781360L);(* 14, 14 *)\r
 554 (mk_real_int64 273824213252876L),(mk_real_int64 200795259470400L);(* 14, 14 *)\r
 555 (mk_real_int64 864519053242421L),(mk_real_int64 543977996587472L);(* 14, 14 *)\r
 556 (mk_real_int64 348627025497916L),(mk_real_int64 258383447040523L);(* 14, 14 *)\r
 557 (mk_real_int64 297309463250844L),(mk_real_int64 282746574452784L);(* 14, 14 *)\r
 558 (mk_real_int64 504330820474572L),(mk_real_int64 426123055903368L);(* 14, 14 *)\r
 559 (mk_real_int64 288591190562884L),(mk_real_int64 321436866725406L);(* 14, 14 *)\r
 560 (mk_real_int64 700377216102960L),(mk_real_int64 802095725756175L);(* 14, 14 *)\r
 561 (mk_real_int64 180527804443260L),(mk_real_int64 724206358890024L);(* 14, 14 *)\r
 562 (mk_real_int64 227074174078514L),(mk_real_int64 644464986753104L);(* 14, 14 *)\r
 563 (mk_real_int64 434722374899604L),(mk_real_int64 395013617517870L);(* 14, 14 *)\r
 564 (mk_real_int64 298577649252731L),(mk_real_int64 526008118997406L);(* 14, 14 *)\r
 565 (mk_real_int64 304241989187630L),(mk_real_int64 396440278691328L);(* 14, 14 *)\r
 566 (mk_real_int64 276593684577756L),(mk_real_int64 617272184339520L);(* 14, 14 *)\r
 567 (mk_real_int64 515596193963432L),(mk_real_int64 540982474434753L);(* 14, 14 *)\r
 568 (mk_real_int64 382901741333964L),(mk_real_int64 172346658576268L);(* 14, 14 *)\r
 569 (mk_real_int64 288585158527603L),(mk_real_int64 499110579283246L);(* 14, 14 *)\r
 570 (mk_real_int64 760232866068891L),(mk_real_int64 712275669956133L);(* 14, 14 *)\r
 571 (mk_real_int64 402521667332724L),(mk_real_int64 209229593862240L);(* 14, 14 *)\r
 572 (mk_real_int64 514618489656414L),(mk_real_int64 128788845770230L);(* 14, 14 *)\r
 573 (mk_real_int64 450834280924373L),(mk_real_int64 581444365300272L);(* 14, 14 *)\r
 574 (mk_real_int64 504245502371133L),(mk_real_int64 506935572643581L);(* 14, 14 *)\r
 575 (mk_real_int64 559278912149322L),(mk_real_int64 611987254866106L);(* 14, 14 *)\r
 576 (mk_real_int64 535516795129272L),(mk_real_int64 222366239451720L);(* 14, 14 *)\r
 577 (mk_real_int64 531463242485548L),(mk_real_int64 385376562766276L);(* 14, 14 *)\r
 578 (mk_real_int64 298134796795056L),(mk_real_int64 492727754026875L);(* 14, 14 *)\r
 579 (mk_real_int64 827342964690516L),(mk_real_int64 637577807408175L);(* 14, 14 *)\r
 580 (mk_real_int64 404989249823163L),(mk_real_int64 558499044572157L);(* 14, 14 *)\r
 581 (mk_real_int64 675340988213522L),(mk_real_int64 737884748959671L);(* 14, 14 *)\r
 582 (mk_real_int64 414423503320960L),(mk_real_int64 515592586264770L);(* 14, 14 *)\r
 583 (mk_real_int64 456543130822576L),(mk_real_int64 358867101667842L);(* 14, 14 *)\r
 584 (mk_real_int64 592102828349425L),(mk_real_int64 535359626320024L);(* 14, 14 *)\r
 585 (mk_real_int64 523050845127651L),(mk_real_int64 502450973382456L);(* 14, 14 *)\r
 586 (mk_real_int64 268040826889398L),(mk_real_int64 428182305986730L);(* 14, 14 *)\r
 587 (mk_real_int64 567009903899680L),(mk_real_int64 829260714777034L);(* 14, 14 *)\r
 588 (mk_real_int64 539062424789234L),(mk_real_int64 307825688646400L);(* 14, 14 *)\r
 589 (mk_real_int64 476371965213105L),(mk_real_int64 477524335067321L);(* 14, 14 *)\r
 590 (mk_real_int64 692666251791176L),(mk_real_int64 417509836631386L);(* 14, 14 *)\r
 591 (mk_real_int64 192453277976610L),(mk_real_int64 549697337694179L);(* 14, 14 *)\r
 592 (mk_real_int64 875287952743904L),(mk_real_int64 842982907138403L);(* 14, 14 *)\r
 593 (mk_real_int64 358407962990432L),(mk_real_int64 713297418318344L);(* 14, 14 *)\r
 594 (mk_real_int64 420904445122688L),(mk_real_int64 464160369737172L);(* 14, 14 *)\r
 595 (mk_real_int64 406937622299312L),(mk_real_int64 464734907915040L);(* 14, 14 *)\r
 596 (mk_real_int64 391899631028650L),(mk_real_int64 584356946072998L);(* 14, 14 *)\r
 597 (mk_real_int64 446891706480625L),(mk_real_int64 602600697244080L);(* 14, 14 *)\r
 598 (mk_real_int64 481799506534556L),(mk_real_int64 396077081873101L);(* 14, 14 *)\r
 599 (mk_real_int64 671982629724637L),(mk_real_int64 464193099830440L);(* 14, 14 *)\r
 600 (mk_real_int64 551530892722140L),(mk_real_int64 340542807735586L);(* 14, 14 *)\r
 601 (mk_real_int64 268144502189031L),(mk_real_int64 917683285194236L);(* 14, 14 *)\r
 602 (mk_real_int64 498968260351569L),(mk_real_int64 639069069190320L);(* 14, 14 *)\r
 603 (mk_real_int64 517476698419168L),(mk_real_int64 782771857142340L);(* 14, 14 *)\r
 604 (mk_real_int64 653900895142564L),(mk_real_int64 211660637941760L);(* 14, 14 *)\r
 605 (mk_real_int64 479287405123173L),(mk_real_int64 365830302399396L);(* 14, 14 *)\r
 606 (mk_real_int64 263372690124663L),(mk_real_int64 385530175619941L);(* 14, 14 *)\r
 607 (mk_real_int64 304766134973524L),(mk_real_int64 710056319580342L);(* 14, 14 *)\r
 608 (mk_real_int64 284615936587619L),(mk_real_int64 311143260716220L);(* 14, 14 *)\r
 609 (mk_real_int64 765589557255200L),(mk_real_int64 265233531196860L);(* 14, 14 *)\r
 610 (mk_real_int64 207138328584440L),(mk_real_int64 589508541177616L);(* 14, 14 *)\r
 611 (mk_real_int64 473993142083254L),(mk_real_int64 215588489608710L);(* 14, 14 *)\r
 612 (mk_real_int64 688655294007098L),(mk_real_int64 159938787375458L);(* 14, 14 *)\r
 613 (mk_real_int64 530971787060792L),(mk_real_int64 251548431566005L);(* 14, 14 *)\r
 614 (mk_real_int64 212739843776910L),(mk_real_int64 429217524506192L);(* 14, 14 *)\r
 615 (mk_real_int64 577487209982088L),(mk_real_int64 686170986207840L);(* 14, 14 *)\r
 616 (mk_real_int64 481358874475500L),(mk_real_int64 482350032174346L);(* 14, 14 *)\r
 617 (mk_real_int64 195056743964432L),(mk_real_int64 485023687637976L);(* 14, 14 *)\r
 618 (mk_real_int64 566022024312756L),(mk_real_int64 603473062410004L);(* 14, 14 *)\r
 619 (mk_real_int64 437254606965260L),(mk_real_int64 557756203255950L);(* 14, 14 *)\r
 620 (mk_real_int64 189138314204238L),(mk_real_int64 517501858009500L);(* 14, 14 *)\r
 621 (mk_real_int64 690926347781511L),(mk_real_int64 264873086127156L);(* 14, 14 *)\r
 622 (mk_real_int64 477565753516656L),(mk_real_int64 420575867512084L);(* 14, 14 *)\r
 623 (mk_real_int64 464964223903704L),(mk_real_int64 582209272943210L);(* 14, 14 *)\r
 624 (mk_real_int64 170790388705476L),(mk_real_int64 152689732450866L);(* 14, 14 *)\r
 625 (mk_real_int64 601032244916427L),(mk_real_int64 557305791795302L);(* 14, 14 *)\r
 626 (mk_real_int64 364393255520412L),(mk_real_int64 310152168497056L);(* 14, 14 *)\r
 627 (mk_real_int64 501436945574416L),(mk_real_int64 457716049565258L);(* 14, 14 *)\r
 628 (mk_real_int64 748469838326330L),(mk_real_int64 493571870419740L);(* 14, 14 *)\r
 629 (mk_real_int64 166897883082770L),(mk_real_int64 294430819655976L);(* 14, 14 *)\r
 630 (mk_real_int64 261855338937064L),(mk_real_int64 577479274050056L);(* 14, 14 *)\r
 631 (mk_real_int64 131751427939900L),(mk_real_int64 406892686908848L);(* 14, 14 *)\r
 632 (mk_real_int64 377013383132388L),(mk_real_int64 202029895018658L);(* 14, 14 *)\r
 633 (mk_real_int64 262978989783302L),(mk_real_int64 621321975020277L);(* 14, 14 *)\r
 634 (mk_real_int64 393861417389186L),(mk_real_int64 678615423359463L);(* 14, 14 *)\r
 635 (mk_real_int64 249918913114344L),(mk_real_int64 504455537302927L);(* 14, 14 *)\r
 636 (mk_real_int64 678557177170116L),(mk_real_int64 214541494088112L);(* 14, 14 *)\r
 637 (mk_real_int64 371792247030234L),(mk_real_int64 487643151055368L);(* 14, 14 *)\r
 638 (mk_real_int64 601069304565856L),(mk_real_int64 226191321071772L);(* 14, 14 *)\r
 639 (mk_real_int64 287539198480510L),(mk_real_int64 393537153874004L);(* 14, 14 *)\r
 640 (mk_real_int64 446125053399017L),(mk_real_int64 309924227555982L);(* 14, 14 *)\r
 641 (mk_real_int64 719875429928876L),(mk_real_int64 263571991592412L);(* 14, 14 *)\r
 642 (mk_real_int64 258118727970996L),(mk_real_int64 533012949653570L);(* 14, 14 *)\r
 643 (mk_real_int64 276807827291292L),(mk_real_int64 545153702756559L);(* 14, 14 *)\r
 644 (mk_real_int64 296018702541224L),(mk_real_int64 194513885560080L);(* 14, 14 *)\r
 645 (mk_real_int64 203811661994492L),(mk_real_int64 422787217602127L);(* 14, 14 *)\r
 646 (mk_real_int64 544168048729210L),(mk_real_int64 528959985408712L);(* 14, 14 *)\r
 647 (mk_real_int64 251696866400100L),(mk_real_int64 244530453059200L);(* 14, 14 *)\r
 648 (mk_real_int64 593807989783066L),(mk_real_int64 758441469513882L);(* 14, 14 *)\r
 649 (mk_real_int64 270849660518392L),(mk_real_int64 625985821144602L);(* 14, 14 *)\r
 650 (mk_real_int64 519409919896572L),(mk_real_int64 329615871362199L);(* 14, 14 *)\r
 651 (mk_real_int64 252535659077376L),(mk_real_int64 156233982224416L);(* 14, 14 *)\r
 652 (mk_real_int64 705127022430870L),(mk_real_int64 137538961435410L);(* 14, 14 *)\r
 653 (mk_real_int64 819897509404245L),(mk_real_int64 197148544762356L);(* 14, 14 *)\r
 654 (mk_real_int64 200180410835089L),(mk_real_int64 660291885802980L);(* 14, 14 *)\r
 655 (mk_real_int64 636076654560976L),(mk_real_int64 530742516962940L);(* 14, 14 *)\r
 656 (mk_real_int64 648323409557120L),(mk_real_int64 565998972842760L);(* 14, 14 *)\r
 657 (mk_real_int64 153035398552440L),(mk_real_int64 516930832843138L);(* 14, 14 *)\r
 658 (mk_real_int64 525484213260160L),(mk_real_int64 796647091970828L);(* 14, 14 *)\r
 659 (mk_real_int64 398472944272872L),(mk_real_int64 721070597577148L);(* 14, 14 *)\r
 660 (mk_real_int64 206779231443933L),(mk_real_int64 505652481968485L);(* 14, 14 *)\r
 661 (mk_real_int64 458488151021846L),(mk_real_int64 211709172051528L);(* 14, 14 *)\r
 662 (mk_real_int64 759253493894700L),(mk_real_int64 749999408208875L);(* 14, 14 *)\r
 663 (mk_real_int64 571479080079730L),(mk_real_int64 467800621697000L);(* 14, 14 *)\r
 664 (mk_real_int64 240577076832600L),(mk_real_int64 540498001890695L);(* 14, 14 *)\r
 665 (mk_real_int64 695977998860592L),(mk_real_int64 284149341686860L);(* 14, 14 *)\r
 666 (mk_real_int64 381205205453933L),(mk_real_int64 134953323166512L);(* 14, 14 *)\r
 667 (mk_real_int64 178003622623684L),(mk_real_int64 174366093663170L);(* 14, 14 *)\r
 668 (mk_real_int64 444773633368834L),(mk_real_int64 202105631390538L);(* 14, 14 *)\r
 669 (mk_real_int64 295977271656420L),(mk_real_int64 507133242212112L);(* 14, 14 *)\r
 670 (mk_real_int64 466889204754742L),(mk_real_int64 513352586255436L);(* 14, 14 *)\r
 671 (mk_real_int64 351294383870184L),(mk_real_int64 525613792063512L);(* 14, 14 *)\r
 672 (mk_real_int64 758622366175950L),(mk_real_int64 534617780403148L);(* 14, 14 *)\r
 673 (mk_real_int64 665279616202920L),(mk_real_int64 464245636765410L);(* 14, 14 *)\r
 674 (mk_real_int64 290350828414449L),(mk_real_int64 135703445872696L);(* 14, 14 *)\r
 675 (mk_real_int64 596653892373000L),(mk_real_int64 664905172163988L);(* 14, 14 *)\r
 676 (mk_real_int64 505544677867032L),(mk_real_int64 712956289774292L);(* 14, 14 *)\r
 677 (mk_real_int64 897069320244944L),(mk_real_int64 201561747590365L);(* 14, 14 *)\r
 678 (mk_real_int64 375078841474854L),(mk_real_int64 464173939662664L);(* 14, 14 *)\r
 679 (mk_real_int64 593595067945840L),(mk_real_int64 918210442569056L);(* 14, 14 *)\r
 680 (mk_real_int64 358997099861444L),(mk_real_int64 385492989975100L);(* 14, 14 *)\r
 681 (mk_real_int64 420148344733880L),(mk_real_int64 374882064402150L);(* 14, 14 *)\r
 682 (mk_real_int64 781786463923715L),(mk_real_int64 373782559793412L);(* 14, 14 *)\r
 683 (mk_real_int64 463800276922752L),(mk_real_int64 364428427128885L);(* 14, 14 *)\r
 684 (mk_real_int64 224781321071541L),(mk_real_int64 206199534951480L);(* 14, 14 *)\r
 685 (mk_real_int64 767412609496302L),(mk_real_int64 195282862037120L);(* 14, 14 *)\r
 686 (mk_real_int64 572239691685402L),(mk_real_int64 294415678048296L);(* 14, 14 *)\r
 687 (mk_real_int64 347625702733056L),(mk_real_int64 238340384638200L);(* 14, 14 *)\r
 688 (mk_real_int64 255413073181020L),(mk_real_int64 556373297873952L);(* 14, 14 *)\r
 689 (mk_real_int64 454334620485856L),(mk_real_int64 409595352669704L);(* 14, 14 *)\r
 690 (mk_real_int64 160089314476520L),(mk_real_int64 810922675617972L);(* 14, 14 *)\r
 691 (mk_real_int64 376552371061416L),(mk_real_int64 610174165993050L);(* 14, 14 *)\r
 692 (mk_real_int64 205980102482037L),(mk_real_int64 515482045053378L);(* 14, 14 *)\r
 693 (mk_real_int64 421460988299820L),(mk_real_int64 432225455395176L);(* 14, 14 *)\r
 694 (mk_real_int64 212517721199589L),(mk_real_int64 321540547948872L);(* 14, 14 *)\r
 695 (mk_real_int64 357537733648288L),(mk_real_int64 414280590690000L);(* 14, 14 *)\r
 696 (mk_real_int64 176884469305789L),(mk_real_int64 393560997608142L);(* 14, 14 *)\r
 697 (mk_real_int64 306642957585420L),(mk_real_int64 238828124932075L);(* 14, 14 *)\r
 698 (mk_real_int64 702614555880867L),(mk_real_int64 583938984302085L);(* 14, 14 *)\r
 699 (mk_real_int64 268188668429472L),(mk_real_int64 539343781389429L);(* 14, 14 *)\r
 700 (mk_real_int64 253691250299667L),(mk_real_int64 498993327323960L);(* 14, 14 *)\r
 701 (mk_real_int64 314123961366417L),(mk_real_int64 814041366625270L);(* 14, 14 *)\r
 702 (mk_real_int64 522333001293300L),(mk_real_int64 360047616981570L);(* 14, 14 *)\r
 703 (mk_real_int64 247549111962004L),(mk_real_int64 361254789250200L);(* 14, 14 *)\r
 704 (mk_real_int64 234378076762320L),(mk_real_int64 271713880568039L);(* 14, 14 *)\r
 705 (mk_real_int64 616004852870135L),(mk_real_int64 430817935527854L);(* 14, 14 *)\r
 706 (mk_real_int64 581794474849809L),(mk_real_int64 328873311563262L);(* 14, 14 *)\r
 707 (mk_real_int64 248898313673703L),(mk_real_int64 593939939111418L);(* 14, 14 *)\r
 708 (mk_real_int64 912890206860304L),(mk_real_int64 229054457755305L);(* 14, 14 *)\r
 709 (mk_real_int64 250624249476182L),(mk_real_int64 148730599352340L);(* 14, 14 *)\r
 710 (mk_real_int64 242985825652404L),(mk_real_int64 209024269906536L);(* 14, 14 *)\r
 711 (mk_real_int64 656783471248422L),(mk_real_int64 422841916228331L);(* 14, 14 *)\r
 712 (mk_real_int64 213190142831626L),(mk_real_int64 496313783414829L);(* 14, 14 *)\r
 713 (mk_real_int64 338338886336556L),(mk_real_int64 360183806467182L);(* 14, 14 *)\r
 714 (mk_real_int64 553272892495422L),(mk_real_int64 424888323760142L);(* 14, 14 *)\r
 715 (mk_real_int64 324045561260322L),(mk_real_int64 324915553512176L);(* 14, 14 *)\r
 716 (mk_real_int64 409323423885624L),(mk_real_int64 274667564368714L);(* 14, 14 *)\r
 717 (mk_real_int64 249064543767840L),(mk_real_int64 227300532143380L);(* 14, 14 *)\r
 718 (mk_real_int64 647693628891900L),(mk_real_int64 252892228152104L);(* 14, 14 *)\r
 719 (mk_real_int64 542292226151036L),(mk_real_int64 244226841868413L);(* 14, 14 *)\r
 720 (mk_real_int64 467720547080262L),(mk_real_int64 173653172812770L);(* 14, 14 *)\r
 721 (mk_real_int64 533978757539700L),(mk_real_int64 617242632265350L);(* 14, 14 *)\r
 722 (mk_real_int64 248058495967884L),(mk_real_int64 368252954213400L);(* 14, 14 *)\r
 723 (mk_real_int64 647468715267528L),(mk_real_int64 242477425452579L);(* 14, 14 *)\r
 724 (mk_real_int64 597997904795292L),(mk_real_int64 517298684546880L);(* 14, 14 *)\r
 725 (mk_real_int64 257132267239120L),(mk_real_int64 443581342779028L);(* 14, 14 *)\r
 726 (mk_real_int64 196977117902082L),(mk_real_int64 490742568627693L);(* 14, 14 *)\r
 727 (mk_real_int64 546761610058962L),(mk_real_int64 359240890305165L);(* 14, 14 *)\r
 728 (mk_real_int64 183239085047993L),(mk_real_int64 930930484736538L);(* 14, 14 *)\r
 729 (mk_real_int64 655385321984498L),(mk_real_int64 149251950775814L);(* 14, 14 *)\r
 730 (mk_real_int64 650898747514372L),(mk_real_int64 636631788479907L);(* 14, 14 *)\r
 731 (mk_real_int64 586227026518271L),(mk_real_int64 576710596233240L);(* 14, 14 *)\r
 732 (mk_real_int64 505364009274594L),(mk_real_int64 831126480906432L);(* 14, 14 *)\r
 733 (mk_real_int64 711329307929817L),(mk_real_int64 462615860781116L);(* 14, 14 *)\r
 734 (mk_real_int64 202703928463140L),(mk_real_int64 356189499776728L);(* 14, 14 *)\r
 735 (mk_real_int64 416729650981000L),(mk_real_int64 381257111837910L);(* 14, 14 *)\r
 736 (mk_real_int64 206410988621025L),(mk_real_int64 569734279908871L);(* 14, 14 *)\r
 737 (mk_real_int64 593237011088267L),(mk_real_int64 368953285756416L);(* 14, 14 *)\r
 738 (mk_real_int64 798228038468088L),(mk_real_int64 707639372105244L);(* 14, 14 *)\r
 739 (mk_real_int64 679039412288545L),(mk_real_int64 274846284755730L);(* 14, 14 *)\r
 740 (mk_real_int64 517285551119268L),(mk_real_int64 447956762378268L);(* 14, 14 *)\r
 741 (mk_real_int64 468474797060388L),(mk_real_int64 384425998935618L);(* 14, 14 *)\r
 742 (mk_real_int64 128552468662040L),(mk_real_int64 300071575813502L);(* 14, 14 *)\r
 743 (mk_real_int64 498782793936634L),(mk_real_int64 135807439880950L);(* 14, 14 *)\r
 744 (mk_real_int64 186767846927035L),(mk_real_int64 199472014413416L);(* 14, 14 *)\r
 745 (mk_real_int64 676962971424070L),(mk_real_int64 534860927345570L);(* 14, 14 *)\r
 746 (mk_real_int64 591276142148432L),(mk_real_int64 313766927505303L);(* 14, 14 *)\r
 747 (mk_real_int64 197128472968640L),(mk_real_int64 555871180309286L);(* 14, 14 *)\r
 748 (mk_real_int64 149990546118086L),(mk_real_int64 648497883393591L);(* 14, 14 *)\r
 749 (mk_real_int64 447257625367784L),(mk_real_int64 370813684717796L);(* 14, 14 *)\r
 750 (mk_real_int64 294976478624784L),(mk_real_int64 590248388188602L);(* 14, 14 *)\r
 751 (mk_real_int64 865718869133328L),(mk_real_int64 435438127904570L);(* 14, 14 *)\r
 752 (mk_real_int64 744556776312567L),(mk_real_int64 387746354056060L);(* 14, 14 *)\r
 753 (mk_real_int64 339457363823030L),(mk_real_int64 510552492281780L);(* 14, 14 *)\r
 754 (mk_real_int64 165150916394870L),(mk_real_int64 138943596167142L);(* 14, 14 *)\r
 755 (mk_real_int64 486357087572905L),(mk_real_int64 302618257844200L);(* 14, 14 *)\r
 756 (mk_real_int64 540675771843265L),(mk_real_int64 473665633848380L);(* 14, 14 *)\r
 757 (mk_real_int64 615663783924387L),(mk_real_int64 105838455752998L);(* 14, 14 *)\r
 758 (mk_real_int64 767873881450680L),(mk_real_int64 774852368113860L);(* 14, 14 *)\r
 759 (mk_real_int64 530569243945836L),(mk_real_int64 126199377469808L);(* 14, 14 *)\r
 760 (mk_real_int64 345284677563632L),(mk_real_int64 416175314965430L);(* 14, 14 *)\r
 761 (mk_real_int64 205606900468890L),(mk_real_int64 744713973284964L);(* 14, 14 *)\r
 762 (mk_real_int64 503429301207245L),(mk_real_int64 683044703458848L);(* 14, 14 *)\r
 763 (mk_real_int64 621417217412034L),(mk_real_int64 819945645396960L);(* 14, 14 *)\r
 764 (mk_real_int64 497543937667617L),(mk_real_int64 236475588512064L);(* 14, 14 *)\r
 765 (mk_real_int64 300961316566911L),(mk_real_int64 661409837432880L);(* 14, 14 *)\r
 766 (mk_real_int64 690123663286996L),(mk_real_int64 656253686899476L);(* 14, 14 *)\r
 767 (mk_real_int64 808055146247076L),(mk_real_int64 638883345620868L);(* 14, 14 *)\r
 768 (mk_real_int64 468149167107344L),(mk_real_int64 451633281438738L);(* 14, 14 *)\r
 769 (mk_real_int64 348479530337583L),(mk_real_int64 316585869201600L);(* 14, 14 *)\r
 770 (mk_real_int64 206390523135080L),(mk_real_int64 494138367818820L);(* 14, 14 *)\r
 771 (mk_real_int64 168414963144844L),(mk_real_int64 460316600911686L);(* 14, 14 *)\r
 772 (mk_real_int64 125110142250148L),(mk_real_int64 331790551174299L);(* 14, 14 *)\r
 773 (mk_real_int64 677850354201132L),(mk_real_int64 210780707831988L);(* 14, 14 *)\r
 774 (mk_real_int64 762063695110494L),(mk_real_int64 395074866460424L);(* 14, 14 *)\r
 775 (mk_real_int64 144582213963492L),(mk_real_int64 714352476346359L);(* 14, 14 *)\r
 776 (mk_real_int64 339308251059824L),(mk_real_int64 761834899034506L);(* 14, 14 *)\r
 777 (mk_real_int64 625721117000837L),(mk_real_int64 579163181788950L);(* 14, 14 *)\r
 778 (mk_real_int64 187061707393280L),(mk_real_int64 170858452909130L);(* 14, 14 *)\r
 779 (mk_real_int64 402943416536334L),(mk_real_int64 637521739802874L);(* 14, 14 *)\r
 780 (mk_real_int64 610062146882025L),(mk_real_int64 682863801173250L);(* 14, 14 *)\r
 781 (mk_real_int64 212022093676440L),(mk_real_int64 325667074230544L);(* 14, 14 *)\r
 782 (mk_real_int64 581452341231424L),(mk_real_int64 430412068140828L);(* 14, 14 *)\r
 783 (mk_real_int64 293266443037962L),(mk_real_int64 760787429234434L);(* 14, 14 *)\r
 784 (mk_real_int64 225627153802798L),(mk_real_int64 398761864662168L);(* 14, 14 *)\r
 785 (mk_real_int64 596437629497712L),(mk_real_int64 241463628412266L);(* 14, 14 *)\r
 786 (mk_real_int64 407240101585665L),(mk_real_int64 548271163542779L);(* 14, 14 *)\r
 787 (mk_real_int64 583327173792327L),(mk_real_int64 446012480810385L);(* 14, 14 *)\r
 788 (mk_real_int64 789796852357275L),(mk_real_int64 431677992361124L);(* 14, 14 *)\r
 789 (mk_real_int64 599415411416323L),(mk_real_int64 239145282634944L);(* 14, 14 *)\r
 790 (mk_real_int64 435874083915272L),(mk_real_int64 934782454965570L);(* 14, 14 *)\r
 791 (mk_real_int64 471076077598320L),(mk_real_int64 196074993060216L);(* 14, 14 *)\r
 792 (mk_real_int64 237390993001983L),(mk_real_int64 150705632570799L);(* 14, 14 *)\r
 793 (mk_real_int64 162251955534600L),(mk_real_int64 505139599827150L);(* 14, 14 *)\r
 794 (mk_real_int64 443006156913188L),(mk_real_int64 652884441114044L);(* 14, 14 *)\r
 795 (mk_real_int64 224477524191220L),(mk_real_int64 634294672038472L);(* 14, 14 *)\r
 796 (mk_real_int64 563149753605171L),(mk_real_int64 522141089425904L);(* 14, 14 *)\r
 797 (mk_real_int64 237750005353420L),(mk_real_int64 716646145586478L);(* 14, 14 *)\r
 798 (mk_real_int64 760458640533030L),(mk_real_int64 447433261203014L);(* 14, 14 *)\r
 799 (mk_real_int64 344103109020471L),(mk_real_int64 565227360818280L);(* 14, 14 *)\r
 800 (mk_real_int64 662619040902676L),(mk_real_int64 227123046408860L);(* 14, 14 *)\r
 801 (mk_real_int64 285321488935896L),(mk_real_int64 812920706100906L);(* 14, 14 *)\r
 802 (mk_real_int64 261843178592919L),(mk_real_int64 341213011880202L);(* 14, 14 *)\r
 803 (mk_real_int64 556139126753150L),(mk_real_int64 294250682526064L);(* 14, 14 *)\r
 804 (mk_real_int64 596446891266330L),(mk_real_int64 594800053552698L);(* 14, 14 *)\r
 805 (mk_real_int64 305036266603248L),(mk_real_int64 583347591055516L);(* 14, 14 *)\r
 806 (mk_real_int64 322306600454650L),(mk_real_int64 216592435745772L);(* 14, 14 *)\r
 807 (mk_real_int64 330192526079950L),(mk_real_int64 412361130814805L);(* 14, 14 *)\r
 808 (mk_real_int64 264481781883800L),(mk_real_int64 520987658600490L);(* 14, 14 *)\r
 809 (mk_real_int64 381257027568818L),(mk_real_int64 321665374212560L);(* 14, 14 *)\r
 810 (mk_real_int64 508183440589374L),(mk_real_int64 526619570329224L);(* 14, 14 *)\r
 811 (mk_real_int64 879422863453920L),(mk_real_int64 777391274672652L);(* 14, 14 *)\r
 812 (mk_real_int64 715871770524600L),(mk_real_int64 350406665865765L);(* 14, 14 *)\r
 813 (mk_real_int64 527431854752088L),(mk_real_int64 407046411162160L);(* 14, 14 *)\r
 814 (mk_real_int64 146452003162244L),(mk_real_int64 285383694690316L);(* 14, 14 *)\r
 815 (mk_real_int64 592225159107267L),(mk_real_int64 336983454226644L);(* 14, 14 *)\r
 816 (mk_real_int64 273912769814278L),(mk_real_int64 559844247536960L);(* 14, 14 *)\r
 817 (mk_real_int64 427845295069918L),(mk_real_int64 702722831950764L);(* 14, 14 *)\r
 818 (mk_real_int64 422271722392742L),(mk_real_int64 402749206005939L);(* 14, 14 *)\r
 819 (mk_real_int64 238490343284250L),(mk_real_int64 435016285075943L);(* 14, 14 *)\r
 820 (mk_real_int64 478886166821526L),(mk_real_int64 316627949988324L);(* 14, 14 *)\r
 821 (mk_real_int64 375751419876014L),(mk_real_int64 499887753715266L);(* 14, 14 *)\r
 822 (mk_real_int64 351022256512052L),(mk_real_int64 844962725337490L);(* 14, 14 *)\r
 823 (mk_real_int64 359637441060216L),(mk_real_int64 130901854920957L);(* 14, 14 *)\r
 824 (mk_real_int64 345514854286110L),(mk_real_int64 251432581019970L);(* 14, 14 *)\r
 825 (mk_real_int64 454720663677940L),(mk_real_int64 636634334090106L);(* 14, 14 *)\r
 826 (mk_real_int64 623514390876090L),(mk_real_int64 153830335700048L);(* 14, 14 *)\r
 827 (mk_real_int64 304100061444290L),(mk_real_int64 437231837892304L);(* 14, 14 *)\r
 828 (mk_real_int64 646388341505280L),(mk_real_int64 648766599450193L);(* 14, 14 *)\r
 829 (mk_real_int64 236154064165658L),(mk_real_int64 515948944128579L);(* 14, 14 *)\r
 830 (mk_real_int64 345710732904915L),(mk_real_int64 452088781837056L);(* 14, 14 *)\r
 831 (mk_real_int64 471285526580000L),(mk_real_int64 221956683205747L);(* 14, 14 *)\r
 832 (mk_real_int64 680082310467772L),(mk_real_int64 720446399819125L);(* 14, 14 *)\r
 833 (mk_real_int64 484250184957924L),(mk_real_int64 113148927184950L);(* 14, 14 *)\r
 834 (mk_real_int64 567118418748440L),(mk_real_int64 376640280642437L);(* 14, 14 *)\r
 835 (mk_real_int64 536117353041750L),(mk_real_int64 634757602277761L);(* 14, 14 *)\r
 836 (mk_real_int64 377509396423876L),(mk_real_int64 451642933957778L);(* 14, 14 *)\r
 837 (mk_real_int64 462029996541125L),(mk_real_int64 413387513323280L);(* 14, 14 *)\r
 838 (mk_real_int64 158714557959549L),(mk_real_int64 177672604581700L);(* 14, 14 *)\r
 839 (mk_real_int64 818120432360519L),(mk_real_int64 679116664278280L);(* 14, 14 *)\r
 840 (mk_real_int64 271226737296894L),(mk_real_int64 482948977291534L);(* 14, 14 *)\r
 841 (mk_real_int64 428748798858980L),(mk_real_int64 406793644471585L);(* 14, 14 *)\r
 842 (mk_real_int64 627869057149078L),(mk_real_int64 708628715816000L);(* 14, 14 *)\r
 843 (mk_real_int64 301948988737536L),(mk_real_int64 783370270333080L);(* 14, 14 *)\r
 844 (mk_real_int64 709537404084751L),(mk_real_int64 291715967255532L);(* 14, 14 *)\r
 845 (mk_real_int64 500976060195891L),(mk_real_int64 353548211060594L);(* 14, 14 *)\r
 846 (mk_real_int64 750173617535949L),(mk_real_int64 220190007255510L);(* 14, 14 *)\r
 847 (mk_real_int64 347060019010320L),(mk_real_int64 310710259258905L);(* 14, 14 *)\r
 848 (mk_real_int64 249839595953866L),(mk_real_int64 374108179461924L);(* 14, 14 *)\r
 849 (mk_real_int64 289053011951008L),(mk_real_int64 408495635272920L);(* 14, 14 *)\r
 850 (mk_real_int64 400965556733124L),(mk_real_int64 626239579541723L);(* 14, 14 *)\r
 851 (mk_real_int64 810629702279895L),(mk_real_int64 443195000824350L);(* 14, 14 *)\r
 852 (mk_real_int64 552938480715000L),(mk_real_int64 262629122411145L);(* 14, 14 *)\r
 853 (mk_real_int64 244663833190404L),(mk_real_int64 640907490981144L);(* 14, 14 *)\r
 854 (mk_real_int64 315322384246530L),(mk_real_int64 394650476739463L);(* 14, 14 *)\r
 855 (mk_real_int64 549724173390024L),(mk_real_int64 290171249116620L);(* 14, 14 *)\r
 856 (mk_real_int64 738446579109360L),(mk_real_int64 289267777188375L);(* 14, 14 *)\r
 857 (mk_real_int64 733891008478590L),(mk_real_int64 394392371191905L);(* 14, 14 *)\r
 858 (mk_real_int64 478479780024145L),(mk_real_int64 452244680725615L);(* 14, 14 *)\r
 859 (mk_real_int64 290985968594160L),(mk_real_int64 175180915904930L);(* 14, 14 *)\r
 860 (mk_real_int64 365431918522111L),(mk_real_int64 486663914224488L);(* 14, 14 *)\r
 861 (mk_real_int64 166485834418400L),(mk_real_int64 324090554347136L);(* 14, 14 *)\r
 862 (mk_real_int64 205540017838400L),(mk_real_int64 163398904655930L);(* 14, 14 *)\r
 863 (mk_real_int64 948261714384600L),(mk_real_int64 171758545307560L);(* 14, 14 *)\r
 864 (mk_real_int64 158877153497874L),(mk_real_int64 365721124314825L);(* 14, 14 *)\r
 865 (mk_real_int64 638550143217562L),(mk_real_int64 173260957679452L);(* 14, 14 *)\r
 866 (mk_real_int64 245650002828590L),(mk_real_int64 501930849007744L);(* 14, 14 *)\r
 867 (mk_real_int64 691482896804244L),(mk_real_int64 285113472254677L);(* 14, 14 *)\r
 868 (mk_real_int64 658149161166275L),(mk_real_int64 223814560963000L);(* 14, 14 *)\r
 869 (mk_real_int64 393023762289924L),(mk_real_int64 681202592099682L);(* 14, 14 *)\r
 870 (mk_real_int64 242892434084165L),(mk_real_int64 449634817964773L);(* 14, 14 *)\r
 871 (mk_real_int64 366170306802785L),(mk_real_int64 797055625815870L);(* 14, 14 *)\r
 872 (mk_real_int64 424035908411692L),(mk_real_int64 769103299805886L);(* 14, 14 *)\r
 873 (mk_real_int64 432867236803737L),(mk_real_int64 860182996999392L);(* 14, 14 *)\r
 874 (mk_real_int64 303966823679470L),(mk_real_int64 593310301049004L);(* 14, 14 *)\r
 875 (mk_real_int64 427538649482157L),(mk_real_int64 318651247504304L);(* 14, 14 *)\r
 876 (mk_real_int64 531454600852560L),(mk_real_int64 419850055835028L);(* 14, 14 *)\r
 877 (mk_real_int64 261703066572285L),(mk_real_int64 242551980493856L);(* 14, 14 *)\r
 878 (mk_real_int64 453018601332325L),(mk_real_int64 199518609350596L);(* 14, 14 *)\r
 879 (mk_real_int64 391661770799981L),(mk_real_int64 477868892797704L);(* 14, 14 *)\r
 880 (mk_real_int64 510352996648280L),(mk_real_int64 169390070500092L);(* 14, 14 *)\r
 881 (mk_real_int64 236258908593152L),(mk_real_int64 609459212576130L);(* 14, 14 *)\r
 882 (mk_real_int64 559330344952992L),(mk_real_int64 599173373580624L);(* 14, 14 *)\r
 883 (mk_real_int64 784408616010720L),(mk_real_int64 620029722255552L);(* 14, 14 *)\r
 884 (mk_real_int64 547902252576928L),(mk_real_int64 529223356003296L);(* 14, 14 *)\r
 885 (mk_real_int64 372544411072674L),(mk_real_int64 548420000436779L);(* 14, 14 *)\r
 886 (mk_real_int64 737232436825836L),(mk_real_int64 375502989223800L);(* 14, 14 *)\r
 887 (mk_real_int64 528207953584944L),(mk_real_int64 369524479533150L);(* 14, 14 *)\r
 888 (mk_real_int64 909186331014962L),(mk_real_int64 432432248190724L);(* 14, 14 *)\r
 889 (mk_real_int64 327595953859864L),(mk_real_int64 548508533764448L);(* 14, 14 *)\r
 890 (mk_real_int64 769896257589474L),(mk_real_int64 501431285139732L);(* 14, 14 *)\r
 891 (mk_real_int64 283445988614102L),(mk_real_int64 477927704102134L);(* 14, 14 *)\r
 892 (mk_real_int64 604344341699948L),(mk_real_int64 367160697825545L);(* 14, 14 *)\r
 893 (mk_real_int64 467323967396528L),(mk_real_int64 205500666179232L);(* 14, 14 *)\r
 894 (mk_real_int64 580920026089311L),(mk_real_int64 715284788000695L);(* 14, 14 *)\r
 895 (mk_real_int64 188837901505800L),(mk_real_int64 690650541439233L);(* 14, 14 *)\r
 896 (mk_real_int64 502957025802505L),(mk_real_int64 454915620363408L);(* 14, 14 *)\r
 897 (mk_real_int64 673766278337372L),(mk_real_int64 216418964685120L);(* 14, 14 *)\r
 898 (mk_real_int64 607789389993480L),(mk_real_int64 364403207121317L);(* 14, 14 *)\r
 899 (mk_real_int64 410082613758912L),(mk_real_int64 469243431399413L);(* 14, 14 *)\r
 900 (mk_real_int64 448803885085128L),(mk_real_int64 183330660493813L);(* 14, 14 *)\r
 901 (mk_real_int64 778682867340924L),(mk_real_int64 506179735514530L);(* 14, 14 *)\r
 902 (mk_real_int64 765938264601341L),(mk_real_int64 230123251183548L);(* 14, 14 *)\r
 903 (mk_real_int64 820262332173746L),(mk_real_int64 705760614036800L);(* 14, 14 *)\r
 904 (mk_real_int64 980893970525850L),(mk_real_int64 246368717537134L);(* 14, 14 *)\r
 905 (mk_real_int64 525553618847838L),(mk_real_int64 440557722027159L);(* 14, 14 *)\r
 906 (mk_real_int64 552813839356030L),(mk_real_int64 529618372314975L);(* 14, 14 *)\r
 907 (mk_real_int64 381919273092000L),(mk_real_int64 445633878297716L);(* 14, 14 *)\r
 908 (mk_real_int64 510444345536325L),(mk_real_int64 420100810987220L);(* 14, 14 *)\r
 909 (mk_real_int64 157482018586035L),(mk_real_int64 314508697459313L);(* 14, 14 *)\r
 910 (mk_real_int64 502546964747144L),(mk_real_int64 723832942056544L);(* 14, 14 *)\r
 911 (mk_real_int64 456444668354904L),(mk_real_int64 396384152048076L);(* 14, 14 *)\r
 912 (mk_real_int64 398160282751042L),(mk_real_int64 625529855643420L);(* 14, 14 *)\r
 913 (mk_real_int64 439752774789504L),(mk_real_int64 165062658456144L);(* 14, 14 *)\r
 914 (mk_real_int64 419477462674281L),(mk_real_int64 182366284906884L);(* 14, 14 *)\r
 915 (mk_real_int64 367513017575328L),(mk_real_int64 491720053462500L);(* 14, 14 *)\r
 916 (mk_real_int64 428376828922028L),(mk_real_int64 514155880605024L);(* 14, 14 *)\r
 917 (mk_real_int64 817718106349095L),(mk_real_int64 170677426396770L);(* 14, 14 *)\r
 918 (mk_real_int64 224677866316310L),(mk_real_int64 321162142131936L);(* 14, 14 *)\r
 919 (mk_real_int64 597473177182200L),(mk_real_int64 533253983995740L);(* 14, 14 *)\r
 920 (mk_real_int64 401486026409550L),(mk_real_int64 551514627776458L);(* 14, 14 *)\r
 921 (mk_real_int64 295794415226656L),(mk_real_int64 524545142457908L);(* 14, 14 *)\r
 922 (mk_real_int64 447973554990004L),(mk_real_int64 535983055241688L);(* 14, 14 *)\r
 923 (mk_real_int64 468656747540320L),(mk_real_int64 368689299457674L);(* 14, 14 *)\r
 924 (mk_real_int64 385528170030553L),(mk_real_int64 519262662801094L);(* 14, 14 *)\r
 925 (mk_real_int64 341867338110896L),(mk_real_int64 343406576887014L);(* 14, 14 *)\r
 926 (mk_real_int64 665809582618792L),(mk_real_int64 274082823830593L);(* 14, 14 *)\r
 927 (mk_real_int64 552934955727770L),(mk_real_int64 325152897697068L);(* 14, 14 *)\r
 928 (mk_real_int64 183174984013302L),(mk_real_int64 375706869791255L);(* 14, 14 *)\r
 929 (mk_real_int64 585680330160021L),(mk_real_int64 535512799687824L);(* 14, 14 *)\r
 930 (mk_real_int64 700253566002228L),(mk_real_int64 287279768189124L);(* 14, 14 *)\r
 931 (mk_real_int64 541451781064936L),(mk_real_int64 572961739763844L);(* 14, 14 *)\r
 932 (mk_real_int64 459438929948918L),(mk_real_int64 747649317106512L);(* 14, 14 *)\r
 933 (mk_real_int64 588225337930032L),(mk_real_int64 354302699520640L);(* 14, 14 *)\r
 934 (mk_real_int64 935214705361940L),(mk_real_int64 569441729046090L);(* 14, 14 *)\r
 935 (mk_real_int64 436907735484692L),(mk_real_int64 379585482881756L);(* 14, 14 *)\r
 936 (mk_real_int64 891838053657701L),(mk_real_int64 691563223844024L);(* 14, 14 *)\r
 937 (mk_real_int64 504677044860352L),(mk_real_int64 148737812748273L);(* 14, 14 *)\r
 938 (mk_real_int64 481940641764912L),(mk_real_int64 345721562301896L);(* 14, 14 *)\r
 939 (mk_real_int64 494335949343852L),(mk_real_int64 721698028328375L);(* 14, 14 *)\r
 940 (mk_real_int64 862443376792130L),(mk_real_int64 211339866876655L);(* 14, 14 *)\r
 941 (mk_real_int64 479183249103405L),(mk_real_int64 549212020961274L);(* 14, 14 *)\r
 942 (mk_real_int64 304032309300777L),(mk_real_int64 307394733821660L);(* 14, 14 *)\r
 943 (mk_real_int64 513547271618900L),(mk_real_int64 537179494651425L);(* 14, 14 *)\r
 944 (mk_real_int64 406834534601872L),(mk_real_int64 297556417194976L);(* 14, 14 *)\r
 945 (mk_real_int64 592394529824112L),(mk_real_int64 246066846676576L);(* 14, 14 *)\r
 946 (mk_real_int64 695035158557881L),(mk_real_int64 267009108414696L);(* 14, 14 *)\r
 947 (mk_real_int64 533652559710237L),(mk_real_int64 594607676091000L);(* 14, 14 *)\r
 948 (mk_real_int64 968528910905600L),(mk_real_int64 328795965893751L);(* 14, 14 *)\r
 949 (mk_real_int64 431677448200725L),(mk_real_int64 310799438183650L);(* 14, 14 *)\r
 950 (mk_real_int64 471338212190916L),(mk_real_int64 416909917636765L);(* 14, 14 *)\r
 951 (mk_real_int64 555097531242280L),(mk_real_int64 326780907657425L);(* 14, 14 *)\r
 952 (mk_real_int64 122172643078430L),(mk_real_int64 407985350233249L);(* 14, 14 *)\r
 953 (mk_real_int64 393468631846262L),(mk_real_int64 195231416406611L);(* 14, 14 *)\r
 954 (mk_real_int64 439897285615782L),(mk_real_int64 447117698836476L);(* 14, 14 *)\r
 955 (mk_real_int64 375576295353000L),(mk_real_int64 518361599504493L);(* 14, 14 *)\r
 956 (mk_real_int64 399500369210108L),(mk_real_int64 272510883241128L);(* 14, 14 *)\r
 957 (mk_real_int64 381990115372096L),(mk_real_int64 366831399334512L);(* 14, 14 *)\r
 958 (mk_real_int64 301663928500584L),(mk_real_int64 600410915782500L);(* 14, 14 *)\r
 959 (mk_real_int64 455419734175812L),(mk_real_int64 697234416653760L);(* 14, 14 *)\r
 960 (mk_real_int64 120712376726460L),(mk_real_int64 743144519548858L);(* 14, 14 *)\r
 961 (mk_real_int64 388484932571196L),(mk_real_int64 545807863934400L);(* 14, 14 *)\r
 962 (mk_real_int64 689894810856905L),(mk_real_int64 455506958750337L);(* 14, 14 *)\r
 963 (mk_real_int64 302243963986503L),(mk_real_int64 604443182153832L);(* 14, 14 *)\r
 964 (mk_real_int64 453007156298249L),(mk_real_int64 378871724582296L);(* 14, 14 *)\r
 965 (mk_real_int64 341414813208702L),(mk_real_int64 622848653932230L);(* 14, 14 *)\r
 966 (mk_real_int64 504984092898272L),(mk_real_int64 161628394556424L);(* 14, 14 *)\r
 967 (mk_real_int64 495600079041957L),(mk_real_int64 313009200381800L);(* 14, 14 *)\r
 968 (mk_real_int64 346755075562487L),(mk_real_int64 328327998666650L);(* 14, 14 *)\r
 969 (mk_real_int64 382086292889295L),(mk_real_int64 381969384268210L);(* 14, 14 *)\r
 970 (mk_real_int64 464728417911567L),(mk_real_int64 182239968412850L);(* 14, 14 *)\r
 971 (mk_real_int64 258399325869762L),(mk_real_int64 437795854174850L);(* 14, 14 *)\r
 972 (mk_real_int64 410778810055350L),(mk_real_int64 551821819755310L);(* 14, 14 *)\r
 973 (mk_real_int64 534617685441262L),(mk_real_int64 423311294018750L);(* 14, 14 *)\r
 974 (mk_real_int64 513339328787396L),(mk_real_int64 447417168979101L);(* 14, 14 *)\r
 975 (mk_real_int64 656751864450825L),(mk_real_int64 301604936270945L);(* 14, 14 *)\r
 976 (mk_real_int64 669269881768965L),(mk_real_int64 648844187191200L);(* 14, 14 *)\r
 977 (mk_real_int64 796510103913784L),(mk_real_int64 424223688511802L);(* 14, 14 *)\r
 978 (mk_real_int64 270861112056444L),(mk_real_int64 593953925553612L);(* 14, 14 *)\r
 979 (mk_real_int64 246866458987008L),(mk_real_int64 256396452986065L);(* 14, 14 *)\r
 980 (mk_real_int64 652154112539776L),(mk_real_int64 530649425308880L);(* 14, 14 *)\r
 981 (mk_real_int64 592747840471040L),(mk_real_int64 339235585740210L);(* 14, 14 *)\r
 982 (mk_real_int64 270457420009050L),(mk_real_int64 173209307507320L);(* 14, 14 *)\r
 983 (mk_real_int64 195174373864536L),(mk_real_int64 541810762591848L);(* 14, 14 *)\r
 984 (mk_real_int64 564262617296576L),(mk_real_int64 155043792801180L);(* 14, 14 *)\r
 985 (mk_real_int64 506193175942630L),(mk_real_int64 158571121761540L);(* 14, 14 *)\r
 986 (mk_real_int64 415202688442075L),(mk_real_int64 512187370962210L);(* 14, 14 *)\r
 987 (mk_real_int64 693356840546194L),(mk_real_int64 754402541412688L);(* 14, 14 *)\r
 988 (mk_real_int64 447287625790410L),(mk_real_int64 696843201181644L);(* 14, 14 *)\r
 989 (mk_real_int64 374037323413000L),(mk_real_int64 565014347241587L);(* 14, 14 *)\r
 990 (mk_real_int64 919758675756222L),(mk_real_int64 327139473818892L);(* 14, 14 *)\r
 991 (mk_real_int64 419585554051202L),(mk_real_int64 553635094854119L);(* 14, 14 *)\r
 992 (mk_real_int64 279662711969096L),(mk_real_int64 827744501220452L);(* 14, 14 *)\r
 993 (mk_real_int64 361721479611888L),(mk_real_int64 156073508919474L);(* 14, 14 *)\r
 994 (mk_real_int64 161136401266308L),(mk_real_int64 938864335216503L);(* 14, 14 *)\r
 995 (mk_real_int64 283752745291763L),(mk_real_int64 241868834757151L);(* 14, 14 *)\r
 996 (mk_real_int64 196716331920780L),(mk_real_int64 567016927424948L);(* 14, 14 *)\r
 997 (mk_real_int64 693253390612640L),(mk_real_int64 251728765683525L);(* 14, 14 *)\r
 998 (mk_real_int64 310462130525274L),(mk_real_int64 396955005175652L);(* 14, 14 *)\r
 999 (mk_real_int64 216804737077761L),(mk_real_int64 454210574958910L);(* 14, 14 *)\r
1000 (mk_real_int64 296578297721370L),(mk_real_int64 310834417328160L);(* 14, 14 *)\r
1001 (mk_real_int64 259480268524440L),(mk_real_int64 536928131719088L)(* 14, 14 *)\r
1002 ];;\r