Update from HH

[Flyspeck/.git] / formal_lp / old / arith / tests / arith_test_data10.hl

let data = [\r
(mk_real_int64 1726243269L),(mk_real_int64 1817325359L);(* 9, 9 *)\r
(mk_real_int64 1768022689L),(mk_real_int64 1558161191L);(* 9, 9 *)\r
(mk_real_int64 1206033154L),(mk_real_int64 1558884794L);(* 9, 9 *)\r
(mk_real_int64 1906027066L),(mk_real_int64 1442177873L);(* 9, 9 *)\r
(mk_real_int64 1977549753L),(mk_real_int64 1273704457L);(* 9, 9 *)\r
(mk_real_int64 1291906284L),(mk_real_int64 1467314700L);(* 9, 9 *)\r
(mk_real_int64 1632659072L),(mk_real_int64 1469511878L);(* 9, 9 *)\r
(mk_real_int64 1982151253L),(mk_real_int64 1030366990L);(* 9, 9 *)\r
(mk_real_int64 1862370153L),(mk_real_int64 1995347081L);(* 9, 9 *)\r
(mk_real_int64 1677181149L),(mk_real_int64 1314591793L);(* 9, 9 *)\r
(mk_real_int64 1816907908L),(mk_real_int64 1848051783L);(* 9, 9 *)\r
(mk_real_int64 1991902175L),(mk_real_int64 1032625198L);(* 9, 9 *)\r
(mk_real_int64 1699941983L),(mk_real_int64 1526284142L);(* 9, 9 *)\r
(mk_real_int64 1934018658L),(mk_real_int64 1687620282L);(* 9, 9 *)\r
(mk_real_int64 1546815434L),(mk_real_int64 1081109949L);(* 9, 9 *)\r
(mk_real_int64 1187124574L),(mk_real_int64 1453327185L);(* 9, 9 *)\r
(mk_real_int64 1297171865L),(mk_real_int64 1988543779L);(* 9, 9 *)\r
(mk_real_int64 1642697472L),(mk_real_int64 1762963588L);(* 9, 9 *)\r
(mk_real_int64 1030394292L),(mk_real_int64 1381004506L);(* 9, 9 *)\r
(mk_real_int64 1343141844L),(mk_real_int64 1957455165L);(* 9, 9 *)\r
(mk_real_int64 1505129212L),(mk_real_int64 1715972512L);(* 9, 9 *)\r
(mk_real_int64 1118957729L),(mk_real_int64 1273451483L);(* 9, 9 *)\r
(mk_real_int64 1907097950L),(mk_real_int64 1794765593L);(* 9, 9 *)\r
(mk_real_int64 1337160339L),(mk_real_int64 1457208787L);(* 9, 9 *)\r
(mk_real_int64 1146825040L),(mk_real_int64 1221314739L);(* 9, 9 *)\r
(mk_real_int64 1410073279L),(mk_real_int64 1718726832L);(* 9, 9 *)\r
(mk_real_int64 1619830283L),(mk_real_int64 1487968052L);(* 9, 9 *)\r
(mk_real_int64 1194913436L),(mk_real_int64 1878191486L);(* 9, 9 *)\r
(mk_real_int64 1825423184L),(mk_real_int64 1735397491L);(* 9, 9 *)\r
(mk_real_int64 1858219207L),(mk_real_int64 1679749011L);(* 9, 9 *)\r
(mk_real_int64 1624866135L),(mk_real_int64 1218406783L);(* 9, 9 *)\r
(mk_real_int64 1895362439L),(mk_real_int64 1896439803L);(* 9, 9 *)\r
(mk_real_int64 1086579883L),(mk_real_int64 1838579099L);(* 9, 9 *)\r
(mk_real_int64 1170142834L),(mk_real_int64 1644115293L);(* 9, 9 *)\r
(mk_real_int64 1826814405L),(mk_real_int64 1219187664L);(* 9, 9 *)\r
(mk_real_int64 1999972697L),(mk_real_int64 1481365646L);(* 9, 9 *)\r
(mk_real_int64 1652205236L),(mk_real_int64 1719725983L);(* 9, 9 *)\r
(mk_real_int64 1809462580L),(mk_real_int64 1100935396L);(* 9, 9 *)\r
(mk_real_int64 1729094053L),(mk_real_int64 1718450691L);(* 9, 9 *)\r
(mk_real_int64 1125527248L),(mk_real_int64 1905176389L);(* 9, 9 *)\r
(mk_real_int64 1189123803L),(mk_real_int64 1476809871L);(* 9, 9 *)\r
(mk_real_int64 1540795242L),(mk_real_int64 1325500694L);(* 9, 9 *)\r
(mk_real_int64 1671036670L),(mk_real_int64 1468397741L);(* 9, 9 *)\r
(mk_real_int64 1833496901L),(mk_real_int64 1809203813L);(* 9, 9 *)\r
(mk_real_int64 1793630342L),(mk_real_int64 1764505986L);(* 9, 9 *)\r
(mk_real_int64 1937540404L),(mk_real_int64 1294996801L);(* 9, 9 *)\r
(mk_real_int64 1522785299L),(mk_real_int64 1663392833L);(* 9, 9 *)\r
(mk_real_int64 1332589029L),(mk_real_int64 1286722429L);(* 9, 9 *)\r
(mk_real_int64 1820610073L),(mk_real_int64 1222517925L);(* 9, 9 *)\r
(mk_real_int64 1186871599L),(mk_real_int64 1068518850L);(* 9, 9 *)\r
(mk_real_int64 1624622759L),(mk_real_int64 1693045045L);(* 9, 9 *)\r
(mk_real_int64 1630394382L),(mk_real_int64 1927637375L);(* 9, 9 *)\r
(mk_real_int64 1221342041L),(mk_real_int64 1928707632L);(* 9, 9 *)\r
(mk_real_int64 1066521596L),(mk_real_int64 1900104300L);(* 9, 9 *)\r
(mk_real_int64 1678505472L),(mk_real_int64 1093978040L);(* 9, 9 *)\r
(mk_real_int64 1149097432L),(mk_real_int64 1106972492L);(* 9, 9 *)\r
(mk_real_int64 1609870242L),(mk_real_int64 1953042817L);(* 9, 9 *)\r
(mk_real_int64 1490625208L),(mk_real_int64 1148056264L);(* 9, 9 *)\r
(mk_real_int64 1677611541L),(mk_real_int64 1569861744L);(* 9, 9 *)\r
(mk_real_int64 1225403132L),(mk_real_int64 1618182142L);(* 9, 9 *)\r
(mk_real_int64 1005082197L),(mk_real_int64 1360939021L);(* 9, 9 *)\r
(mk_real_int64 1850484951L),(mk_real_int64 1062308419L);(* 9, 9 *)\r
(mk_real_int64 1281647260L),(mk_real_int64 1704975895L);(* 9, 9 *)\r
(mk_real_int64 1958580347L),(mk_real_int64 1988812403L);(* 9, 9 *)\r
(mk_real_int64 1387136953L),(mk_real_int64 1522740151L);(* 9, 9 *)\r
(mk_real_int64 1280325323L),(mk_real_int64 1506576128L);(* 9, 9 *)\r
(mk_real_int64 1531579091L),(mk_real_int64 1057008397L);(* 9, 9 *)\r
(mk_real_int64 1280553630L),(mk_real_int64 1496078757L);(* 9, 9 *)\r
(mk_real_int64 1846415488L),(mk_real_int64 1613157866L);(* 9, 9 *)\r
(mk_real_int64 1104158652L),(mk_real_int64 1742329037L);(* 9, 9 *)\r
(mk_real_int64 1401876145L),(mk_real_int64 1933392601L);(* 9, 9 *)\r
(mk_real_int64 1130698341L),(mk_real_int64 1699652301L);(* 9, 9 *)\r
(mk_real_int64 1615408553L),(mk_real_int64 1830567911L);(* 9, 9 *)\r
(mk_real_int64 1685126559L),(mk_real_int64 1569742481L);(* 9, 9 *)\r
(mk_real_int64 1172767625L),(mk_real_int64 1184532765L);(* 9, 9 *)\r
(mk_real_int64 1609110887L),(mk_real_int64 1250748328L);(* 9, 9 *)\r
(mk_real_int64 1997114792L),(mk_real_int64 1568689457L);(* 9, 9 *)\r
(mk_real_int64 1063436652L),(mk_real_int64 1263683737L);(* 9, 9 *)\r
(mk_real_int64 1842560094L),(mk_real_int64 1568085962L);(* 9, 9 *)\r
(mk_real_int64 1645990114L),(mk_real_int64 1516366145L);(* 9, 9 *)\r
(mk_real_int64 1970127284L),(mk_real_int64 1077709192L);(* 9, 9 *)\r
(mk_real_int64 1512967346L),(mk_real_int64 1155765321L);(* 9, 9 *)\r
(mk_real_int64 1813652717L),(mk_real_int64 1642521304L);(* 9, 9 *)\r
(mk_real_int64 1575393400L),(mk_real_int64 1552861844L);(* 9, 9 *)\r
(mk_real_int64 1672489187L),(mk_real_int64 1994546450L);(* 9, 9 *)\r
(mk_real_int64 1301640775L),(mk_real_int64 1064453674L);(* 9, 9 *)\r
(mk_real_int64 1465703091L),(mk_real_int64 1483074095L);(* 9, 9 *)\r
(mk_real_int64 1216305996L),(mk_real_int64 1071689596L);(* 9, 9 *)\r
(mk_real_int64 1230240680L),(mk_real_int64 1150832649L);(* 9, 9 *)\r
(mk_real_int64 1446899866L),(mk_real_int64 1451079349L);(* 9, 9 *)\r
(mk_real_int64 1019849336L),(mk_real_int64 1388837866L);(* 9, 9 *)\r
(mk_real_int64 1816044778L),(mk_real_int64 1202604188L);(* 9, 9 *)\r
(mk_real_int64 1913629263L),(mk_real_int64 1029576994L);(* 9, 9 *)\r
(mk_real_int64 1509461335L),(mk_real_int64 1962889634L);(* 9, 9 *)\r
(mk_real_int64 1993571745L),(mk_real_int64 1016869892L);(* 9, 9 *)\r
(mk_real_int64 1653518663L),(mk_real_int64 1278329526L);(* 9, 9 *)\r
(mk_real_int64 1967167752L),(mk_real_int64 1587792507L);(* 9, 9 *)\r
(mk_real_int64 1772201752L),(mk_real_int64 1324166952L);(* 9, 9 *)\r
(mk_real_int64 1420425255L),(mk_real_int64 1974933019L);(* 9, 9 *)\r
(mk_real_int64 1885999584L),(mk_real_int64 1972887248L);(* 9, 9 *)\r
(mk_real_int64 1255174511L),(mk_real_int64 1132264714L);(* 9, 9 *)\r
(mk_real_int64 1897253294L),(mk_real_int64 1178221175L);(* 9, 9 *)\r
(mk_real_int64 1882891989L),(mk_real_int64 1544657213L);(* 9, 9 *)\r
(mk_real_int64 1785045237L),(mk_real_int64 1514040697L);(* 9, 9 *)\r
(mk_real_int64 1352383461L),(mk_real_int64 1991747056L);(* 9, 9 *)\r
(mk_real_int64 1033443057L),(mk_real_int64 1691727444L);(* 9, 9 *)\r
(mk_real_int64 1121186096L),(mk_real_int64 1194910765L);(* 9, 9 *)\r
(mk_real_int64 1496516809L),(mk_real_int64 1581289418L);(* 9, 9 *)\r
(mk_real_int64 1261664414L),(mk_real_int64 1310363158L);(* 9, 9 *)\r
(mk_real_int64 1242136058L),(mk_real_int64 1784075723L);(* 9, 9 *)\r
(mk_real_int64 1133059969L),(mk_real_int64 1612503766L);(* 9, 9 *)\r
(mk_real_int64 1559290099L),(mk_real_int64 1655619294L);(* 9, 9 *)\r
(mk_real_int64 1341027786L),(mk_real_int64 1023311249L);(* 9, 9 *)\r
(mk_real_int64 1097285922L),(mk_real_int64 1877910584L);(* 9, 9 *)\r
(mk_real_int64 1710872342L),(mk_real_int64 1892139044L);(* 9, 9 *)\r
(mk_real_int64 1651264341L),(mk_real_int64 1255307660L);(* 9, 9 *)\r
(mk_real_int64 1264833064L),(mk_real_int64 1474012618L);(* 9, 9 *)\r
(mk_real_int64 1195904838L),(mk_real_int64 1887584622L);(* 9, 9 *)\r
(mk_real_int64 1491584571L),(mk_real_int64 1637823602L);(* 9, 9 *)\r
(mk_real_int64 1319712198L),(mk_real_int64 1368972049L);(* 9, 9 *)\r
(mk_real_int64 1244531756L),(mk_real_int64 1995420637L);(* 9, 9 *)\r
(mk_real_int64 1610506173L),(mk_real_int64 1001824689L);(* 9, 9 *)\r
(mk_real_int64 1983426835L),(mk_real_int64 1961791218L);(* 9, 9 *)\r
(mk_real_int64 1157143429L),(mk_real_int64 1772256987L);(* 9, 9 *)\r
(mk_real_int64 1091275698L),(mk_real_int64 1190912333L);(* 9, 9 *)\r
(mk_real_int64 1062502537L),(mk_real_int64 1110062096L);(* 9, 9 *)\r
(mk_real_int64 1732796961L),(mk_real_int64 1101923861L);(* 9, 9 *)\r
(mk_real_int64 1839827278L),(mk_real_int64 1642670744L);(* 9, 9 *)\r
(mk_real_int64 1572974614L),(mk_real_int64 1241634000L);(* 9, 9 *)\r
(mk_real_int64 1837193388L),(mk_real_int64 1859580740L);(* 9, 9 *)\r
(mk_real_int64 1447371291L),(mk_real_int64 1907134653L);(* 9, 9 *)\r
(mk_real_int64 1803168354L),(mk_real_int64 1460244416L);(* 9, 9 *)\r
(mk_real_int64 1340482714L),(mk_real_int64 1778135396L);(* 9, 9 *)\r
(mk_real_int64 1426894379L),(mk_real_int64 1647173478L);(* 9, 9 *)\r
(mk_real_int64 1999005927L),(mk_real_int64 1608932186L);(* 9, 9 *)\r
(mk_real_int64 1089704847L),(mk_real_int64 1623840811L);(* 9, 9 *)\r
(mk_real_int64 1990650959L),(mk_real_int64 1873164008L);(* 9, 9 *)\r
(mk_real_int64 1539543967L),(mk_real_int64 1137639332L);(* 9, 9 *)\r
(mk_real_int64 1001997593L),(mk_real_int64 1557465410L);(* 9, 9 *)\r
(mk_real_int64 1672192458L),(mk_real_int64 1379236567L);(* 9, 9 *)\r
(mk_real_int64 1866167819L),(mk_real_int64 1325028935L);(* 9, 9 *)\r
(mk_real_int64 1786634886L),(mk_real_int64 1519960008L);(* 9, 9 *)\r
(mk_real_int64 1829636507L),(mk_real_int64 1541202244L);(* 9, 9 *)\r
(mk_real_int64 1522510698L),(mk_real_int64 1162909203L);(* 9, 9 *)\r
(mk_real_int64 1634185339L),(mk_real_int64 1553234093L);(* 9, 9 *)\r
(mk_real_int64 1314610007L),(mk_real_int64 1249950571L);(* 9, 9 *)\r
(mk_real_int64 1800630214L),(mk_real_int64 1460131458L);(* 9, 9 *)\r
(mk_real_int64 1921600758L),(mk_real_int64 1337397102L);(* 9, 9 *)\r
(mk_real_int64 1192252282L),(mk_real_int64 1150261756L);(* 9, 9 *)\r
(mk_real_int64 1661341974L),(mk_real_int64 1205291438L);(* 9, 9 *)\r
(mk_real_int64 1534896838L),(mk_real_int64 1509969951L);(* 9, 9 *)\r
(mk_real_int64 1773251059L),(mk_real_int64 1482343511L);(* 9, 9 *)\r
(mk_real_int64 1101207486L),(mk_real_int64 1438661725L);(* 9, 9 *)\r
(mk_real_int64 1119411137L),(mk_real_int64 1859632953L);(* 9, 9 *)\r
(mk_real_int64 1562379894L),(mk_real_int64 1702187946L);(* 9, 9 *)\r
(mk_real_int64 1640673151L),(mk_real_int64 1015509204L);(* 9, 9 *)\r
(mk_real_int64 1569441541L),(mk_real_int64 1457956820L);(* 9, 9 *)\r
(mk_real_int64 1993412920L),(mk_real_int64 1122342356L);(* 9, 9 *)\r
(mk_real_int64 1120499767L),(mk_real_int64 1283208346L);(* 9, 9 *)\r
(mk_real_int64 1630607909L),(mk_real_int64 1799280470L);(* 9, 9 *)\r
(mk_real_int64 1255624698L),(mk_real_int64 1263985176L);(* 9, 9 *)\r
(mk_real_int64 1012988138L),(mk_real_int64 1445771834L);(* 9, 9 *)\r
(mk_real_int64 1294322178L),(mk_real_int64 1839754275L);(* 9, 9 *)\r
(mk_real_int64 1823210597L),(mk_real_int64 1530519501L);(* 9, 9 *)\r
(mk_real_int64 1951563249L),(mk_real_int64 1202146864L);(* 9, 9 *)\r
(mk_real_int64 1945387049L),(mk_real_int64 1851735836L);(* 9, 9 *)\r
(mk_real_int64 1896123436L),(mk_real_int64 1466901020L);(* 9, 9 *)\r
(mk_real_int64 1844339729L),(mk_real_int64 1356197867L);(* 9, 9 *)\r
(mk_real_int64 1551777875L),(mk_real_int64 1304291374L);(* 9, 9 *)\r
(mk_real_int64 1418752521L),(mk_real_int64 1390974781L);(* 9, 9 *)\r
(mk_real_int64 1421791107L),(mk_real_int64 1662877745L);(* 9, 9 *)\r
(mk_real_int64 1600529309L),(mk_real_int64 1931997393L);(* 9, 9 *)\r
(mk_real_int64 1912560941L),(mk_real_int64 1299100803L);(* 9, 9 *)\r
(mk_real_int64 1680509030L),(mk_real_int64 1342673394L);(* 9, 9 *)\r
(mk_real_int64 1466718537L),(mk_real_int64 1799258402L);(* 9, 9 *)\r
(mk_real_int64 1216897335L),(mk_real_int64 1909043936L);(* 9, 9 *)\r
(mk_real_int64 1519653847L),(mk_real_int64 1862061504L);(* 9, 9 *)\r
(mk_real_int64 1949666740L),(mk_real_int64 1270911662L);(* 9, 9 *)\r
(mk_real_int64 1496981813L),(mk_real_int64 1327479225L);(* 9, 9 *)\r
(mk_real_int64 1188021332L),(mk_real_int64 1261453211L);(* 9, 9 *)\r
(mk_real_int64 1615451128L),(mk_real_int64 1588891635L);(* 9, 9 *)\r
(mk_real_int64 1908069703L),(mk_real_int64 1360233029L);(* 9, 9 *)\r
(mk_real_int64 1756800896L),(mk_real_int64 1788937314L);(* 9, 9 *)\r
(mk_real_int64 1119385767L),(mk_real_int64 1102540520L);(* 9, 9 *)\r
(mk_real_int64 1613617091L),(mk_real_int64 1637215053L);(* 9, 9 *)\r
(mk_real_int64 1570564480L),(mk_real_int64 1816208392L);(* 9, 9 *)\r
(mk_real_int64 1864455824L),(mk_real_int64 1239633127L);(* 9, 9 *)\r
(mk_real_int64 1377489362L),(mk_real_int64 1592746952L);(* 9, 9 *)\r
(mk_real_int64 1663455866L),(mk_real_int64 1080990745L);(* 9, 9 *)\r
(mk_real_int64 1533210892L),(mk_real_int64 1995221375L);(* 9, 9 *)\r
(mk_real_int64 1159245245L),(mk_real_int64 1480537203L);(* 9, 9 *)\r
(mk_real_int64 1063800964L),(mk_real_int64 1152304847L);(* 9, 9 *)\r
(mk_real_int64 1985249528L),(mk_real_int64 1036343113L);(* 9, 9 *)\r
(mk_real_int64 1332081989L),(mk_real_int64 1034061932L);(* 9, 9 *)\r
(mk_real_int64 1517234280L),(mk_real_int64 1573428066L);(* 9, 9 *)\r
(mk_real_int64 1859216054L),(mk_real_int64 1224298649L);(* 9, 9 *)\r
(mk_real_int64 1116270042L),(mk_real_int64 1157299310L);(* 9, 9 *)\r
(mk_real_int64 1775523653L),(mk_real_int64 1832899472L);(* 9, 9 *)\r
(mk_real_int64 1754808041L),(mk_real_int64 1240296279L);(* 9, 9 *)\r
(mk_real_int64 1175196496L),(mk_real_int64 1123623626L);(* 9, 9 *)\r
(mk_real_int64 1179715036L),(mk_real_int64 1577968509L);(* 9, 9 *)\r
(mk_real_int64 1729056302L),(mk_real_int64 1829503484L);(* 9, 9 *)\r
(mk_real_int64 1228693921L),(mk_real_int64 1400688942L);(* 9, 9 *)\r
(mk_real_int64 1044588112L),(mk_real_int64 1280020719L);(* 9, 9 *)\r
(mk_real_int64 1484572141L),(mk_real_int64 1356919787L);(* 9, 9 *)\r
(mk_real_int64 1607455795L),(mk_real_int64 1415991068L);(* 9, 9 *)\r
(mk_real_int64 1794268333L),(mk_real_int64 1192799957L);(* 9, 9 *)\r
(mk_real_int64 1102207966L),(mk_real_int64 1134913924L);(* 9, 9 *)\r
(mk_real_int64 1525090671L),(mk_real_int64 1755764856L);(* 9, 9 *)\r
(mk_real_int64 1374983501L),(mk_real_int64 1720457783L);(* 9, 9 *)\r
(mk_real_int64 1456855325L),(mk_real_int64 1085323835L);(* 9, 9 *)\r
(mk_real_int64 1585306240L),(mk_real_int64 1040189024L);(* 9, 9 *)\r
(mk_real_int64 1777998998L),(mk_real_int64 1346265831L);(* 9, 9 *)\r
(mk_real_int64 1699938350L),(mk_real_int64 1707156513L);(* 9, 9 *)\r
(mk_real_int64 1464109474L),(mk_real_int64 1544589890L);(* 9, 9 *)\r
(mk_real_int64 1837938911L),(mk_real_int64 1423159586L);(* 9, 9 *)\r
(mk_real_int64 1905794248L),(mk_real_int64 1409587265L);(* 9, 9 *)\r
(mk_real_int64 1815506338L),(mk_real_int64 1581276736L);(* 9, 9 *)\r
(mk_real_int64 1751480900L),(mk_real_int64 1234297479L);(* 9, 9 *)\r
(mk_real_int64 1923610925L),(mk_real_int64 1584560585L);(* 9, 9 *)\r
(mk_real_int64 1991755000L),(mk_real_int64 1052061270L);(* 9, 9 *)\r
(mk_real_int64 1549489790L),(mk_real_int64 1160314492L);(* 9, 9 *)\r
(mk_real_int64 1965972270L),(mk_real_int64 1443224986L);(* 9, 9 *)\r
(mk_real_int64 1430030316L),(mk_real_int64 1923470084L);(* 9, 9 *)\r
(mk_real_int64 1055091344L),(mk_real_int64 1640609728L);(* 9, 9 *)\r
(mk_real_int64 1307808800L),(mk_real_int64 1999043185L);(* 9, 9 *)\r
(mk_real_int64 1865312778L),(mk_real_int64 1454738712L);(* 9, 9 *)\r
(mk_real_int64 1666768301L),(mk_real_int64 1094391200L);(* 9, 9 *)\r
(mk_real_int64 1992662268L),(mk_real_int64 1688867278L);(* 9, 9 *)\r
(mk_real_int64 1051504485L),(mk_real_int64 1882428090L);(* 9, 9 *)\r
(mk_real_int64 1700750592L),(mk_real_int64 1337431598L);(* 9, 9 *)\r
(mk_real_int64 1815911245L),(mk_real_int64 1939982251L);(* 9, 9 *)\r
(mk_real_int64 1518980876L),(mk_real_int64 1184296208L);(* 9, 9 *)\r
(mk_real_int64 1510196819L),(mk_real_int64 1384681067L);(* 9, 9 *)\r
(mk_real_int64 1377293618L),(mk_real_int64 1520931230L);(* 9, 9 *)\r
(mk_real_int64 1383433024L),(mk_real_int64 1290793191L);(* 9, 9 *)\r
(mk_real_int64 1832153930L),(mk_real_int64 1790422915L);(* 9, 9 *)\r
(mk_real_int64 1728702782L),(mk_real_int64 1404794055L);(* 9, 9 *)\r
(mk_real_int64 1535834045L),(mk_real_int64 1424991748L);(* 9, 9 *)\r
(mk_real_int64 1074216753L),(mk_real_int64 1334774012L);(* 9, 9 *)\r
(mk_real_int64 1916235514L),(mk_real_int64 1776468266L);(* 9, 9 *)\r
(mk_real_int64 1652065169L),(mk_real_int64 1823499745L);(* 9, 9 *)\r
(mk_real_int64 1236781089L),(mk_real_int64 1838895725L);(* 9, 9 *)\r
(mk_real_int64 1557846808L),(mk_real_int64 1451055536L);(* 9, 9 *)\r
(mk_real_int64 1742818964L),(mk_real_int64 1721115138L);(* 9, 9 *)\r
(mk_real_int64 1588614467L),(mk_real_int64 1062613622L);(* 9, 9 *)\r
(mk_real_int64 1182792993L),(mk_real_int64 1041182835L);(* 9, 9 *)\r
(mk_real_int64 1883809993L),(mk_real_int64 1654323402L);(* 9, 9 *)\r
(mk_real_int64 1236150024L),(mk_real_int64 1609507539L);(* 9, 9 *)\r
(mk_real_int64 1641333616L),(mk_real_int64 1781676061L);(* 9, 9 *)\r
(mk_real_int64 1933028167L),(mk_real_int64 1045349248L);(* 9, 9 *)\r
(mk_real_int64 1546176465L),(mk_real_int64 1534160114L);(* 9, 9 *)\r
(mk_real_int64 1257176704L),(mk_real_int64 1017015608L);(* 9, 9 *)\r
(mk_real_int64 1166889254L),(mk_real_int64 1074889862L);(* 9, 9 *)\r
(mk_real_int64 1726035929L),(mk_real_int64 1261974246L);(* 9, 9 *)\r
(mk_real_int64 1558557154L),(mk_real_int64 1567670519L);(* 9, 9 *)\r
(mk_real_int64 1614650524L),(mk_real_int64 1716730473L);(* 9, 9 *)\r
(mk_real_int64 1966192575L),(mk_real_int64 1924282325L);(* 9, 9 *)\r
(mk_real_int64 1685366429L),(mk_real_int64 1992411500L);(* 9, 9 *)\r
(mk_real_int64 1703201161L),(mk_real_int64 1680085150L);(* 9, 9 *)\r
(mk_real_int64 1626449400L),(mk_real_int64 1059141282L);(* 9, 9 *)\r
(mk_real_int64 1641862103L),(mk_real_int64 1656178479L);(* 9, 9 *)\r
(mk_real_int64 1932316762L),(mk_real_int64 1320819401L);(* 9, 9 *)\r
(mk_real_int64 1108000197L),(mk_real_int64 1790971095L);(* 9, 9 *)\r
(mk_real_int64 1906612921L),(mk_real_int64 1074379380L);(* 9, 9 *)\r
(mk_real_int64 1168644030L),(mk_real_int64 1926326506L);(* 9, 9 *)\r
(mk_real_int64 1783658132L),(mk_real_int64 1292540691L);(* 9, 9 *)\r
(mk_real_int64 1401745845L),(mk_real_int64 1870886266L);(* 9, 9 *)\r
(mk_real_int64 1230291800L),(mk_real_int64 1117905055L);(* 9, 9 *)\r
(mk_real_int64 1566323040L),(mk_real_int64 1219765480L);(* 9, 9 *)\r
(mk_real_int64 1672006471L),(mk_real_int64 1482956945L);(* 9, 9 *)\r
(mk_real_int64 1725019606L),(mk_real_int64 1480844717L);(* 9, 9 *)\r
(mk_real_int64 1162557983L),(mk_real_int64 1020943948L);(* 9, 9 *)\r
(mk_real_int64 1447963097L),(mk_real_int64 1466062520L);(* 9, 9 *)\r
(mk_real_int64 1074990259L),(mk_real_int64 1959527668L);(* 9, 9 *)\r
(mk_real_int64 1968956972L),(mk_real_int64 1243738524L);(* 9, 9 *)\r
(mk_real_int64 1906306377L),(mk_real_int64 1961248465L);(* 9, 9 *)\r
(mk_real_int64 1155226661L),(mk_real_int64 1873886884L);(* 9, 9 *)\r
(mk_real_int64 1403487145L),(mk_real_int64 1889997986L);(* 9, 9 *)\r
(mk_real_int64 1601843351L),(mk_real_int64 1936357303L);(* 9, 9 *)\r
(mk_real_int64 1909015411L),(mk_real_int64 1375918158L);(* 9, 9 *)\r
(mk_real_int64 1168276941L),(mk_real_int64 1651656548L);(* 9, 9 *)\r
(mk_real_int64 1093330215L),(mk_real_int64 1632230648L);(* 9, 9 *)\r
(mk_real_int64 1784012387L),(mk_real_int64 1322109832L);(* 9, 9 *)\r
(mk_real_int64 1314984628L),(mk_real_int64 1095306309L);(* 9, 9 *)\r
(mk_real_int64 1693990525L),(mk_real_int64 1567461374L);(* 9, 9 *)\r
(mk_real_int64 1426088459L),(mk_real_int64 1483435680L);(* 9, 9 *)\r
(mk_real_int64 1008078678L),(mk_real_int64 1143492454L);(* 9, 9 *)\r
(mk_real_int64 1334121676L),(mk_real_int64 1161017385L);(* 9, 9 *)\r
(mk_real_int64 1493620496L),(mk_real_int64 1911372814L);(* 9, 9 *)\r
(mk_real_int64 1872856303L),(mk_real_int64 1641937677L);(* 9, 9 *)\r
(mk_real_int64 1715980836L),(mk_real_int64 1947085253L);(* 9, 9 *)\r
(mk_real_int64 1105422407L),(mk_real_int64 1924905506L);(* 9, 9 *)\r
(mk_real_int64 1020020128L),(mk_real_int64 1822409666L);(* 9, 9 *)\r
(mk_real_int64 1137314030L),(mk_real_int64 1527858961L);(* 9, 9 *)\r
(mk_real_int64 1467399121L),(mk_real_int64 1340293814L);(* 9, 9 *)\r
(mk_real_int64 1516061703L),(mk_real_int64 1629965737L);(* 9, 9 *)\r
(mk_real_int64 1310750069L),(mk_real_int64 1296088312L);(* 9, 9 *)\r
(mk_real_int64 1314680004L),(mk_real_int64 1073363057L);(* 9, 9 *)\r
(mk_real_int64 1387514501L),(mk_real_int64 1530327335L);(* 9, 9 *)\r
(mk_real_int64 1236931560L),(mk_real_int64 1125853265L);(* 9, 9 *)\r
(mk_real_int64 1151077892L),(mk_real_int64 1979683950L);(* 9, 9 *)\r
(mk_real_int64 1265537142L),(mk_real_int64 1401495598L);(* 9, 9 *)\r
(mk_real_int64 1817650064L),(mk_real_int64 1422870696L);(* 9, 9 *)\r
(mk_real_int64 1953169786L),(mk_real_int64 1011734206L);(* 9, 9 *)\r
(mk_real_int64 1539765207L),(mk_real_int64 1242469759L);(* 9, 9 *)\r
(mk_real_int64 1396377490L),(mk_real_int64 1690470537L);(* 9, 9 *)\r
(mk_real_int64 1063500999L),(mk_real_int64 1267077733L);(* 9, 9 *)\r
(mk_real_int64 1659937322L),(mk_real_int64 1221191688L);(* 9, 9 *)\r
(mk_real_int64 1546234140L),(mk_real_int64 1168424709L);(* 9, 9 *)\r
(mk_real_int64 1612210519L),(mk_real_int64 1961602720L);(* 9, 9 *)\r
(mk_real_int64 1184795802L),(mk_real_int64 1787125666L);(* 9, 9 *)\r
(mk_real_int64 1627907188L),(mk_real_int64 1353696711L);(* 9, 9 *)\r
(mk_real_int64 1051399670L),(mk_real_int64 1796122722L);(* 9, 9 *)\r
(mk_real_int64 1172685611L),(mk_real_int64 1711990366L);(* 9, 9 *)\r
(mk_real_int64 1828812450L),(mk_real_int64 1260758618L);(* 9, 9 *)\r
(mk_real_int64 1773502883L),(mk_real_int64 1963293160L);(* 9, 9 *)\r
(mk_real_int64 1674441253L),(mk_real_int64 1747003038L);(* 9, 9 *)\r
(mk_real_int64 1490859785L),(mk_real_int64 1736296885L);(* 9, 9 *)\r
(mk_real_int64 1681548110L),(mk_real_int64 1703926808L);(* 9, 9 *)\r
(mk_real_int64 1107255442L),(mk_real_int64 1597149431L);(* 9, 9 *)\r
(mk_real_int64 1869239879L),(mk_real_int64 1125579823L);(* 9, 9 *)\r
(mk_real_int64 1988093753L),(mk_real_int64 1224929361L);(* 9, 9 *)\r
(mk_real_int64 1943916324L),(mk_real_int64 1825591165L);(* 9, 9 *)\r
(mk_real_int64 1566464738L),(mk_real_int64 1043672336L);(* 9, 9 *)\r
(mk_real_int64 1636150989L),(mk_real_int64 1093488316L);(* 9, 9 *)\r
(mk_real_int64 1527128916L),(mk_real_int64 1219089792L);(* 9, 9 *)\r
(mk_real_int64 1918116815L),(mk_real_int64 1275328839L);(* 9, 9 *)\r
(mk_real_int64 1941057463L),(mk_real_int64 1363952225L);(* 9, 9 *)\r
(mk_real_int64 1351776761L),(mk_real_int64 1911840430L);(* 9, 9 *)\r
(mk_real_int64 1350095928L),(mk_real_int64 1021527341L);(* 9, 9 *)\r
(mk_real_int64 1250185085L),(mk_real_int64 1241179420L);(* 9, 9 *)\r
(mk_real_int64 1182921756L),(mk_real_int64 1279006589L);(* 9, 9 *)\r
(mk_real_int64 1468966875L),(mk_real_int64 1433084329L);(* 9, 9 *)\r
(mk_real_int64 1016029283L),(mk_real_int64 1316497960L);(* 9, 9 *)\r
(mk_real_int64 1776217948L),(mk_real_int64 1923640436L);(* 9, 9 *)\r
(mk_real_int64 1539643577L),(mk_real_int64 1842307331L);(* 9, 9 *)\r
(mk_real_int64 1061169267L),(mk_real_int64 1015061087L);(* 9, 9 *)\r
(mk_real_int64 1092362841L),(mk_real_int64 1059215978L);(* 9, 9 *)\r
(mk_real_int64 1799031913L),(mk_real_int64 1402977826L);(* 9, 9 *)\r
(mk_real_int64 1409780387L),(mk_real_int64 1225808504L);(* 9, 9 *)\r
(mk_real_int64 1229657984L),(mk_real_int64 1129013274L);(* 9, 9 *)\r
(mk_real_int64 1075839377L),(mk_real_int64 1735324134L);(* 9, 9 *)\r
(mk_real_int64 1733629701L),(mk_real_int64 1554413091L);(* 9, 9 *)\r
(mk_real_int64 1045176345L),(mk_real_int64 1399112413L);(* 9, 9 *)\r
(mk_real_int64 1805945575L),(mk_real_int64 1126907560L);(* 9, 9 *)\r
(mk_real_int64 1384520124L),(mk_real_int64 1769707680L);(* 9, 9 *)\r
(mk_real_int64 1353830880L),(mk_real_int64 1085728100L);(* 9, 9 *)\r
(mk_real_int64 1346964346L),(mk_real_int64 1628060459L);(* 9, 9 *)\r
(mk_real_int64 1942658067L),(mk_real_int64 1709087164L);(* 9, 9 *)\r
(mk_real_int64 1755962486L),(mk_real_int64 1510831994L);(* 9, 9 *)\r
(mk_real_int64 1809561882L),(mk_real_int64 1249966777L);(* 9, 9 *)\r
(mk_real_int64 1267454388L),(mk_real_int64 1712510552L);(* 9, 9 *)\r
(mk_real_int64 1553844739L),(mk_real_int64 1684821585L);(* 9, 9 *)\r
(mk_real_int64 1157920525L),(mk_real_int64 1903055727L);(* 9, 9 *)\r
(mk_real_int64 1182965998L),(mk_real_int64 1881841484L);(* 9, 9 *)\r
(mk_real_int64 1564920311L),(mk_real_int64 1948798934L);(* 9, 9 *)\r
(mk_real_int64 1502060043L),(mk_real_int64 1124287423L);(* 9, 9 *)\r
(mk_real_int64 1791869357L),(mk_real_int64 1121171810L);(* 9, 9 *)\r
(mk_real_int64 1165340043L),(mk_real_int64 1447597621L);(* 9, 9 *)\r
(mk_real_int64 1545376887L),(mk_real_int64 1914553784L);(* 9, 9 *)\r
(mk_real_int64 1387907983L),(mk_real_int64 1616916870L);(* 9, 9 *)\r
(mk_real_int64 1510552384L),(mk_real_int64 1649310387L);(* 9, 9 *)\r
(mk_real_int64 1539120312L),(mk_real_int64 1769935896L);(* 9, 9 *)\r
(mk_real_int64 1488476451L),(mk_real_int64 1975441166L);(* 9, 9 *)\r
(mk_real_int64 1668096741L),(mk_real_int64 1464302381L);(* 9, 9 *)\r
(mk_real_int64 1116557910L),(mk_real_int64 1089944749L);(* 9, 9 *)\r
(mk_real_int64 1647015340L),(mk_real_int64 1898948392L);(* 9, 9 *)\r
(mk_real_int64 1416246622L),(mk_real_int64 1979691206L);(* 9, 9 *)\r
(mk_real_int64 1861558886L),(mk_real_int64 1363328824L);(* 9, 9 *)\r
(mk_real_int64 1181479395L),(mk_real_int64 1048808116L);(* 9, 9 *)\r
(mk_real_int64 1396492565L),(mk_real_int64 1142120617L);(* 9, 9 *)\r
(mk_real_int64 1216146415L),(mk_real_int64 1924104090L);(* 9, 9 *)\r
(mk_real_int64 1561987248L),(mk_real_int64 1435721189L);(* 9, 9 *)\r
(mk_real_int64 1267647636L),(mk_real_int64 1229543456L);(* 9, 9 *)\r
(mk_real_int64 1293858743L),(mk_real_int64 1225792535L);(* 9, 9 *)\r
(mk_real_int64 1462720416L),(mk_real_int64 1495060445L);(* 9, 9 *)\r
(mk_real_int64 1163710276L),(mk_real_int64 1841408702L);(* 9, 9 *)\r
(mk_real_int64 1122924010L),(mk_real_int64 1192645012L);(* 9, 9 *)\r
(mk_real_int64 1739414393L),(mk_real_int64 1618144000L);(* 9, 9 *)\r
(mk_real_int64 1173390240L),(mk_real_int64 1783908842L);(* 9, 9 *)\r
(mk_real_int64 1196345133L),(mk_real_int64 1182479358L);(* 9, 9 *)\r
(mk_real_int64 1234958985L),(mk_real_int64 1718663616L);(* 9, 9 *)\r
(mk_real_int64 1765283574L),(mk_real_int64 1474975561L);(* 9, 9 *)\r
(mk_real_int64 1301783594L),(mk_real_int64 1603111650L);(* 9, 9 *)\r
(mk_real_int64 1708040801L),(mk_real_int64 1812178150L);(* 9, 9 *)\r
(mk_real_int64 1259612924L),(mk_real_int64 1802011218L);(* 9, 9 *)\r
(mk_real_int64 1266118226L),(mk_real_int64 1496568771L);(* 9, 9 *)\r
(mk_real_int64 1518061218L),(mk_real_int64 1245787365L);(* 9, 9 *)\r
(mk_real_int64 1400770454L),(mk_real_int64 1586448293L);(* 9, 9 *)\r
(mk_real_int64 1087323139L),(mk_real_int64 1103399123L);(* 9, 9 *)\r
(mk_real_int64 1502288260L),(mk_real_int64 1258932994L);(* 9, 9 *)\r
(mk_real_int64 1681582423L),(mk_real_int64 1442304205L);(* 9, 9 *)\r
(mk_real_int64 1001581965L),(mk_real_int64 1621497464L);(* 9, 9 *)\r
(mk_real_int64 1926234473L),(mk_real_int64 1805606638L);(* 9, 9 *)\r
(mk_real_int64 1776024381L),(mk_real_int64 1223601610L);(* 9, 9 *)\r
(mk_real_int64 1240276813L),(mk_real_int64 1243414886L);(* 9, 9 *)\r
(mk_real_int64 1189938584L),(mk_real_int64 1397570553L);(* 9, 9 *)\r
(mk_real_int64 1852462982L),(mk_real_int64 1214013206L);(* 9, 9 *)\r
(mk_real_int64 1907161632L),(mk_real_int64 1497482798L);(* 9, 9 *)\r
(mk_real_int64 1158820516L),(mk_real_int64 1087011686L);(* 9, 9 *)\r
(mk_real_int64 1133937595L),(mk_real_int64 1664535986L);(* 9, 9 *)\r
(mk_real_int64 1521502655L),(mk_real_int64 1481680592L);(* 9, 9 *)\r
(mk_real_int64 1966179611L),(mk_real_int64 1660709197L);(* 9, 9 *)\r
(mk_real_int64 1228942219L),(mk_real_int64 1667141504L);(* 9, 9 *)\r
(mk_real_int64 1323347483L),(mk_real_int64 1877136644L);(* 9, 9 *)\r
(mk_real_int64 1791874557L),(mk_real_int64 1152966099L);(* 9, 9 *)\r
(mk_real_int64 1530820860L),(mk_real_int64 1069991116L);(* 9, 9 *)\r
(mk_real_int64 1281620581L),(mk_real_int64 1937412139L);(* 9, 9 *)\r
(mk_real_int64 1500896935L),(mk_real_int64 1792654780L);(* 9, 9 *)\r
(mk_real_int64 1717081651L),(mk_real_int64 1143786109L);(* 9, 9 *)\r
(mk_real_int64 1548741088L),(mk_real_int64 1496176955L);(* 9, 9 *)\r
(mk_real_int64 1827087268L),(mk_real_int64 1484439190L);(* 9, 9 *)\r
(mk_real_int64 1571901337L),(mk_real_int64 1016198037L);(* 9, 9 *)\r
(mk_real_int64 1612072634L),(mk_real_int64 1868547672L);(* 9, 9 *)\r
(mk_real_int64 1644105788L),(mk_real_int64 1304048011L);(* 9, 9 *)\r
(mk_real_int64 1338625733L),(mk_real_int64 1903287656L);(* 9, 9 *)\r
(mk_real_int64 1427627777L),(mk_real_int64 1000311452L);(* 9, 9 *)\r
(mk_real_int64 1969461528L),(mk_real_int64 1837752274L);(* 9, 9 *)\r
(mk_real_int64 1737430338L),(mk_real_int64 1199901830L);(* 9, 9 *)\r
(mk_real_int64 1476124594L),(mk_real_int64 1340872768L);(* 9, 9 *)\r
(mk_real_int64 1392555244L),(mk_real_int64 1259092968L);(* 9, 9 *)\r
(mk_real_int64 1482259155L),(mk_real_int64 1898887737L);(* 9, 9 *)\r
(mk_real_int64 1431727053L),(mk_real_int64 1087310713L);(* 9, 9 *)\r
(mk_real_int64 1712594025L),(mk_real_int64 1119947467L);(* 9, 9 *)\r
(mk_real_int64 1115949971L),(mk_real_int64 1915050843L);(* 9, 9 *)\r
(mk_real_int64 1713116271L),(mk_real_int64 1114506851L);(* 9, 9 *)\r
(mk_real_int64 1780401146L),(mk_real_int64 1015034406L);(* 9, 9 *)\r
(mk_real_int64 1538270598L),(mk_real_int64 1637760639L);(* 9, 9 *)\r
(mk_real_int64 1837448717L),(mk_real_int64 1037063465L);(* 9, 9 *)\r
(mk_real_int64 1909779255L),(mk_real_int64 1949981573L);(* 9, 9 *)\r
(mk_real_int64 1048636563L),(mk_real_int64 1360394546L);(* 9, 9 *)\r
(mk_real_int64 1023035716L),(mk_real_int64 1019299471L);(* 9, 9 *)\r
(mk_real_int64 1538510910L),(mk_real_int64 1888586900L);(* 9, 9 *)\r
(mk_real_int64 1725338321L),(mk_real_int64 1530509407L);(* 9, 9 *)\r
(mk_real_int64 1100529588L),(mk_real_int64 1443868307L);(* 9, 9 *)\r
(mk_real_int64 1199981800L),(mk_real_int64 1300995105L);(* 9, 9 *)\r
(mk_real_int64 1316530185L),(mk_real_int64 1376208883L);(* 9, 9 *)\r
(mk_real_int64 1751230864L),(mk_real_int64 1289648119L);(* 9, 9 *)\r
(mk_real_int64 1013917800L),(mk_real_int64 1928199531L);(* 9, 9 *)\r
(mk_real_int64 1052712137L),(mk_real_int64 1484590623L);(* 9, 9 *)\r
(mk_real_int64 1303604012L),(mk_real_int64 1492125166L);(* 9, 9 *)\r
(mk_real_int64 1752597701L),(mk_real_int64 1729054945L);(* 9, 9 *)\r
(mk_real_int64 1590931740L),(mk_real_int64 1224118881L);(* 9, 9 *)\r
(mk_real_int64 1122886509L),(mk_real_int64 1412593370L);(* 9, 9 *)\r
(mk_real_int64 1462040854L),(mk_real_int64 1331700889L);(* 9, 9 *)\r
(mk_real_int64 1000303556L),(mk_real_int64 1700366873L);(* 9, 9 *)\r
(mk_real_int64 1290122575L),(mk_real_int64 1526143020L);(* 9, 9 *)\r
(mk_real_int64 1292236204L),(mk_real_int64 1032160697L);(* 9, 9 *)\r
(mk_real_int64 1236057252L),(mk_real_int64 1462959683L);(* 9, 9 *)\r
(mk_real_int64 1360376826L),(mk_real_int64 1543140152L);(* 9, 9 *)\r
(mk_real_int64 1361972391L),(mk_real_int64 1182084617L);(* 9, 9 *)\r
(mk_real_int64 1019417878L),(mk_real_int64 1672081664L);(* 9, 9 *)\r
(mk_real_int64 1715069042L),(mk_real_int64 1412121166L);(* 9, 9 *)\r
(mk_real_int64 1797976666L),(mk_real_int64 1404192263L);(* 9, 9 *)\r
(mk_real_int64 1263803542L),(mk_real_int64 1248622478L);(* 9, 9 *)\r
(mk_real_int64 1623842838L),(mk_real_int64 1909249186L);(* 9, 9 *)\r
(mk_real_int64 1984351327L),(mk_real_int64 1425188631L);(* 9, 9 *)\r
(mk_real_int64 1646377561L),(mk_real_int64 1556511396L);(* 9, 9 *)\r
(mk_real_int64 1607796845L),(mk_real_int64 1293980770L);(* 9, 9 *)\r
(mk_real_int64 1428367731L),(mk_real_int64 1314392028L);(* 9, 9 *)\r
(mk_real_int64 1765700390L),(mk_real_int64 1312744951L);(* 9, 9 *)\r
(mk_real_int64 1068468553L),(mk_real_int64 1768828699L);(* 9, 9 *)\r
(mk_real_int64 1443564750L),(mk_real_int64 1499614927L);(* 9, 9 *)\r
(mk_real_int64 1010872529L),(mk_real_int64 1790387165L);(* 9, 9 *)\r
(mk_real_int64 1083972678L),(mk_real_int64 1719070166L);(* 9, 9 *)\r
(mk_real_int64 1053590867L),(mk_real_int64 1550958117L);(* 9, 9 *)\r
(mk_real_int64 1567822705L),(mk_real_int64 1509571984L);(* 9, 9 *)\r
(mk_real_int64 1122618231L),(mk_real_int64 1121519394L);(* 9, 9 *)\r
(mk_real_int64 1472707288L),(mk_real_int64 1080516037L);(* 9, 9 *)\r
(mk_real_int64 1013985903L),(mk_real_int64 1178810574L);(* 9, 9 *)\r
(mk_real_int64 1426142215L),(mk_real_int64 1718694246L);(* 9, 9 *)\r
(mk_real_int64 1148789828L),(mk_real_int64 1213418376L);(* 9, 9 *)\r
(mk_real_int64 1707858051L),(mk_real_int64 1091054370L);(* 9, 9 *)\r
(mk_real_int64 1716015545L),(mk_real_int64 1864933943L);(* 9, 9 *)\r
(mk_real_int64 1879765458L),(mk_real_int64 1735724808L);(* 9, 9 *)\r
(mk_real_int64 1424363852L),(mk_real_int64 1942076481L);(* 9, 9 *)\r
(mk_real_int64 1034591951L),(mk_real_int64 1045984797L);(* 9, 9 *)\r
(mk_real_int64 1777439761L),(mk_real_int64 1049227440L);(* 9, 9 *)\r
(mk_real_int64 1113616064L),(mk_real_int64 1250589178L);(* 9, 9 *)\r
(mk_real_int64 1228516913L),(mk_real_int64 1215454115L);(* 9, 9 *)\r
(mk_real_int64 1401248636L),(mk_real_int64 1007589500L);(* 9, 9 *)\r
(mk_real_int64 1320219584L),(mk_real_int64 1544733375L);(* 9, 9 *)\r
(mk_real_int64 1195031610L),(mk_real_int64 1072884720L);(* 9, 9 *)\r
(mk_real_int64 1341426480L),(mk_real_int64 1474779342L);(* 9, 9 *)\r
(mk_real_int64 1302570399L),(mk_real_int64 1524858167L);(* 9, 9 *)\r
(mk_real_int64 1083804108L),(mk_real_int64 1527280808L);(* 9, 9 *)\r
(mk_real_int64 1279994867L),(mk_real_int64 1249557157L);(* 9, 9 *)\r
(mk_real_int64 1888249813L),(mk_real_int64 1047006144L);(* 9, 9 *)\r
(mk_real_int64 1163955123L),(mk_real_int64 1855050176L);(* 9, 9 *)\r
(mk_real_int64 1060970648L),(mk_real_int64 1352510380L);(* 9, 9 *)\r
(mk_real_int64 1783599381L),(mk_real_int64 1145938586L);(* 9, 9 *)\r
(mk_real_int64 1910621707L),(mk_real_int64 1348247870L);(* 9, 9 *)\r
(mk_real_int64 1294706314L),(mk_real_int64 1111514386L);(* 9, 9 *)\r
(mk_real_int64 1516366165L),(mk_real_int64 1521837908L);(* 9, 9 *)\r
(mk_real_int64 1732132222L),(mk_real_int64 1073390791L);(* 9, 9 *)\r
(mk_real_int64 1007903329L),(mk_real_int64 1222118109L);(* 9, 9 *)\r
(mk_real_int64 1851999123L),(mk_real_int64 1798531787L);(* 9, 9 *)\r
(mk_real_int64 1777561937L),(mk_real_int64 1418552715L);(* 9, 9 *)\r
(mk_real_int64 1398474661L),(mk_real_int64 1604056452L);(* 9, 9 *)\r
(mk_real_int64 1018386766L),(mk_real_int64 1634973330L);(* 9, 9 *)\r
(mk_real_int64 1749627889L),(mk_real_int64 1241236202L);(* 9, 9 *)\r
(mk_real_int64 1562363544L),(mk_real_int64 1354907290L);(* 9, 9 *)\r
(mk_real_int64 1651920700L),(mk_real_int64 1897083043L);(* 9, 9 *)\r
(mk_real_int64 1662081613L),(mk_real_int64 1785034794L);(* 9, 9 *)\r
(mk_real_int64 1157734984L),(mk_real_int64 1730433617L);(* 9, 9 *)\r
(mk_real_int64 1885272317L),(mk_real_int64 1258565888L);(* 9, 9 *)\r
(mk_real_int64 1189618530L),(mk_real_int64 1876006532L);(* 9, 9 *)\r
(mk_real_int64 1431854733L),(mk_real_int64 1255310050L);(* 9, 9 *)\r
(mk_real_int64 1096967793L),(mk_real_int64 1971971714L);(* 9, 9 *)\r
(mk_real_int64 1250027061L),(mk_real_int64 1083517224L);(* 9, 9 *)\r
(mk_real_int64 1556518554L),(mk_real_int64 1819588572L);(* 9, 9 *)\r
(mk_real_int64 1742647120L),(mk_real_int64 1229179607L);(* 9, 9 *)\r
(mk_real_int64 1516954838L),(mk_real_int64 1861685999L);(* 9, 9 *)\r
(mk_real_int64 1675281684L),(mk_real_int64 1481463080L);(* 9, 9 *)\r
(mk_real_int64 1471995219L),(mk_real_int64 1469697097L);(* 9, 9 *)\r
(mk_real_int64 1648531483L),(mk_real_int64 1559898670L);(* 9, 9 *)\r
(mk_real_int64 1836663409L),(mk_real_int64 1425997317L);(* 9, 9 *)\r
(mk_real_int64 1602882490L),(mk_real_int64 1542363178L);(* 9, 9 *)\r
(mk_real_int64 1583575041L),(mk_real_int64 1555714416L);(* 9, 9 *)\r
(mk_real_int64 1696327169L),(mk_real_int64 1397623270L);(* 9, 9 *)\r
(mk_real_int64 1449432772L),(mk_real_int64 1731331371L);(* 9, 9 *)\r
(mk_real_int64 1364102923L),(mk_real_int64 1001698605L);(* 9, 9 *)\r
(mk_real_int64 1188118474L),(mk_real_int64 1749337441L);(* 9, 9 *)\r
(mk_real_int64 1032499578L),(mk_real_int64 1975992591L);(* 9, 9 *)\r
(mk_real_int64 1366677053L),(mk_real_int64 1522251887L);(* 9, 9 *)\r
(mk_real_int64 1321584922L),(mk_real_int64 1426502946L);(* 9, 9 *)\r
(mk_real_int64 1354029391L),(mk_real_int64 1934869542L);(* 9, 9 *)\r
(mk_real_int64 1078454776L),(mk_real_int64 1930039317L);(* 9, 9 *)\r
(mk_real_int64 1498589082L),(mk_real_int64 1333183936L);(* 9, 9 *)\r
(mk_real_int64 1837952452L),(mk_real_int64 1790234701L);(* 9, 9 *)\r
(mk_real_int64 1221801358L),(mk_real_int64 1180618533L);(* 9, 9 *)\r
(mk_real_int64 1313039575L),(mk_real_int64 1688037886L);(* 9, 9 *)\r
(mk_real_int64 1081902133L),(mk_real_int64 1325373646L);(* 9, 9 *)\r
(mk_real_int64 1421902478L),(mk_real_int64 1763621212L);(* 9, 9 *)\r
(mk_real_int64 1273124042L),(mk_real_int64 1889491555L);(* 9, 9 *)\r
(mk_real_int64 1671735008L),(mk_real_int64 1541253376L);(* 9, 9 *)\r
(mk_real_int64 1275644545L),(mk_real_int64 1852403790L);(* 9, 9 *)\r
(mk_real_int64 1634084451L),(mk_real_int64 1825187183L);(* 9, 9 *)\r
(mk_real_int64 1455485648L),(mk_real_int64 1740948514L);(* 9, 9 *)\r
(mk_real_int64 1041061133L),(mk_real_int64 1767617396L);(* 9, 9 *)\r
(mk_real_int64 1829186420L),(mk_real_int64 1699289093L);(* 9, 9 *)\r
(mk_real_int64 1114786026L),(mk_real_int64 1949743331L);(* 9, 9 *)\r
(mk_real_int64 1148112175L),(mk_real_int64 1222028536L);(* 9, 9 *)\r
(mk_real_int64 1205869278L),(mk_real_int64 1901793867L);(* 9, 9 *)\r
(mk_real_int64 1347542541L),(mk_real_int64 1672843172L);(* 9, 9 *)\r
(mk_real_int64 1043774095L),(mk_real_int64 1250391105L);(* 9, 9 *)\r
(mk_real_int64 1717761963L),(mk_real_int64 1906092468L);(* 9, 9 *)\r
(mk_real_int64 1175821912L),(mk_real_int64 1268814239L);(* 9, 9 *)\r
(mk_real_int64 1418291795L),(mk_real_int64 1676065037L);(* 9, 9 *)\r
(mk_real_int64 1919796471L),(mk_real_int64 1862744828L);(* 9, 9 *)\r
(mk_real_int64 1327434962L),(mk_real_int64 1268878366L);(* 9, 9 *)\r
(mk_real_int64 1702868548L),(mk_real_int64 1477185498L);(* 9, 9 *)\r
(mk_real_int64 1850516878L),(mk_real_int64 1780331545L);(* 9, 9 *)\r
(mk_real_int64 1150858401L),(mk_real_int64 1501625601L);(* 9, 9 *)\r
(mk_real_int64 1300785090L),(mk_real_int64 1253267592L);(* 9, 9 *)\r
(mk_real_int64 1474553668L),(mk_real_int64 1757640568L);(* 9, 9 *)\r
(mk_real_int64 1292122803L),(mk_real_int64 1070335055L);(* 9, 9 *)\r
(mk_real_int64 1961048280L),(mk_real_int64 1522512265L);(* 9, 9 *)\r
(mk_real_int64 1065832507L),(mk_real_int64 1363296243L);(* 9, 9 *)\r
(mk_real_int64 1539925711L),(mk_real_int64 1859873596L);(* 9, 9 *)\r
(mk_real_int64 1119504367L),(mk_real_int64 1520108610L);(* 9, 9 *)\r
(mk_real_int64 1416078670L),(mk_real_int64 1600280869L);(* 9, 9 *)\r
(mk_real_int64 1845717460L),(mk_real_int64 1421343903L);(* 9, 9 *)\r
(mk_real_int64 1823491412L),(mk_real_int64 1369552076L);(* 9, 9 *)\r
(mk_real_int64 1676581878L),(mk_real_int64 1365270211L);(* 9, 9 *)\r
(mk_real_int64 1406895387L),(mk_real_int64 1779420611L);(* 9, 9 *)\r
(mk_real_int64 1821152042L),(mk_real_int64 1178316305L);(* 9, 9 *)\r
(mk_real_int64 1440182434L),(mk_real_int64 1560308053L);(* 9, 9 *)\r
(mk_real_int64 1996420545L),(mk_real_int64 1637600527L);(* 9, 9 *)\r
(mk_real_int64 1099226452L),(mk_real_int64 1367780629L);(* 9, 9 *)\r
(mk_real_int64 1071170135L),(mk_real_int64 1704243677L);(* 9, 9 *)\r
(mk_real_int64 1601008776L),(mk_real_int64 1094274948L);(* 9, 9 *)\r
(mk_real_int64 1198289504L),(mk_real_int64 1286133526L);(* 9, 9 *)\r
(mk_real_int64 1958268302L),(mk_real_int64 1647426908L);(* 9, 9 *)\r
(mk_real_int64 1945044187L),(mk_real_int64 1653309646L);(* 9, 9 *)\r
(mk_real_int64 1202981731L),(mk_real_int64 1054995552L);(* 9, 9 *)\r
(mk_real_int64 1136139325L),(mk_real_int64 1059922874L);(* 9, 9 *)\r
(mk_real_int64 1743240460L),(mk_real_int64 1807326352L);(* 9, 9 *)\r
(mk_real_int64 1852799695L),(mk_real_int64 1102587678L);(* 9, 9 *)\r
(mk_real_int64 1631468037L),(mk_real_int64 1429172975L);(* 9, 9 *)\r
(mk_real_int64 1956840133L),(mk_real_int64 1781306324L);(* 9, 9 *)\r
(mk_real_int64 1825043723L),(mk_real_int64 1935514878L);(* 9, 9 *)\r
(mk_real_int64 1846372205L),(mk_real_int64 1695133057L);(* 9, 9 *)\r
(mk_real_int64 1936488525L),(mk_real_int64 1113806498L);(* 9, 9 *)\r
(mk_real_int64 1630152621L),(mk_real_int64 1400740226L);(* 9, 9 *)\r
(mk_real_int64 1526091720L),(mk_real_int64 1428231979L);(* 9, 9 *)\r
(mk_real_int64 1264069790L),(mk_real_int64 1172145082L);(* 9, 9 *)\r
(mk_real_int64 1788703461L),(mk_real_int64 1415260689L);(* 9, 9 *)\r
(mk_real_int64 1919099833L),(mk_real_int64 1321803721L);(* 9, 9 *)\r
(mk_real_int64 1401991365L),(mk_real_int64 1559583933L);(* 9, 9 *)\r
(mk_real_int64 1463075601L),(mk_real_int64 1176064504L);(* 9, 9 *)\r
(mk_real_int64 1424507888L),(mk_real_int64 1023272231L);(* 9, 9 *)\r
(mk_real_int64 1162288480L),(mk_real_int64 1351899835L);(* 9, 9 *)\r
(mk_real_int64 1643281285L),(mk_real_int64 1761229167L);(* 9, 9 *)\r
(mk_real_int64 1435075844L),(mk_real_int64 1632856082L);(* 9, 9 *)\r
(mk_real_int64 1707508358L),(mk_real_int64 1893832866L);(* 9, 9 *)\r
(mk_real_int64 1006132490L),(mk_real_int64 1670053477L);(* 9, 9 *)\r
(mk_real_int64 1410940495L),(mk_real_int64 1289863810L);(* 9, 9 *)\r
(mk_real_int64 1879199954L),(mk_real_int64 1665493897L);(* 9, 9 *)\r
(mk_real_int64 1247902743L),(mk_real_int64 1503156447L);(* 9, 9 *)\r
(mk_real_int64 1349645001L),(mk_real_int64 1844461803L);(* 9, 9 *)\r
(mk_real_int64 1017274286L),(mk_real_int64 1544303960L);(* 9, 9 *)\r
(mk_real_int64 1127217926L),(mk_real_int64 1774749752L);(* 9, 9 *)\r
(mk_real_int64 1790925761L),(mk_real_int64 1963994243L);(* 9, 9 *)\r
(mk_real_int64 1271219413L),(mk_real_int64 1327979770L);(* 9, 9 *)\r
(mk_real_int64 1888226518L),(mk_real_int64 1530995974L);(* 9, 9 *)\r
(mk_real_int64 1700596313L),(mk_real_int64 1071884104L);(* 9, 9 *)\r
(mk_real_int64 1966097374L),(mk_real_int64 1780775628L);(* 9, 9 *)\r
(mk_real_int64 1356798436L),(mk_real_int64 1801771492L);(* 9, 9 *)\r
(mk_real_int64 1773226398L),(mk_real_int64 1494472369L);(* 9, 9 *)\r
(mk_real_int64 1051851771L),(mk_real_int64 1175259358L);(* 9, 9 *)\r
(mk_real_int64 1678730653L),(mk_real_int64 1997296539L);(* 9, 9 *)\r
(mk_real_int64 1693231868L),(mk_real_int64 1632258854L);(* 9, 9 *)\r
(mk_real_int64 1422099489L),(mk_real_int64 1594016313L);(* 9, 9 *)\r
(mk_real_int64 1761204586L),(mk_real_int64 1498839651L);(* 9, 9 *)\r
(mk_real_int64 1536060735L),(mk_real_int64 1253605935L);(* 9, 9 *)\r
(mk_real_int64 1073900978L),(mk_real_int64 1898834918L);(* 9, 9 *)\r
(mk_real_int64 1209938932L),(mk_real_int64 1618613797L);(* 9, 9 *)\r
(mk_real_int64 1158790217L),(mk_real_int64 1880203927L);(* 9, 9 *)\r
(mk_real_int64 1896054304L),(mk_real_int64 1387538727L);(* 9, 9 *)\r
(mk_real_int64 1560974073L),(mk_real_int64 1679287041L);(* 9, 9 *)\r
(mk_real_int64 1490009754L),(mk_real_int64 1107096073L);(* 9, 9 *)\r
(mk_real_int64 1744629563L),(mk_real_int64 1176512383L);(* 9, 9 *)\r
(mk_real_int64 1193236552L),(mk_real_int64 1934248385L);(* 9, 9 *)\r
(mk_real_int64 1703956102L),(mk_real_int64 1630164867L);(* 9, 9 *)\r
(mk_real_int64 1933065374L),(mk_real_int64 1077428462L);(* 9, 9 *)\r
(mk_real_int64 1892267499L),(mk_real_int64 1753430373L);(* 9, 9 *)\r
(mk_real_int64 1451304675L),(mk_real_int64 1174385642L);(* 9, 9 *)\r
(mk_real_int64 1165731149L),(mk_real_int64 1019977747L);(* 9, 9 *)\r
(mk_real_int64 1851072092L),(mk_real_int64 1494959072L);(* 9, 9 *)\r
(mk_real_int64 1352650263L),(mk_real_int64 1196909448L);(* 9, 9 *)\r
(mk_real_int64 1202789657L),(mk_real_int64 1772379762L);(* 9, 9 *)\r
(mk_real_int64 1791919034L),(mk_real_int64 1634620582L);(* 9, 9 *)\r
(mk_real_int64 1457094995L),(mk_real_int64 1801761395L);(* 9, 9 *)\r
(mk_real_int64 1861945172L),(mk_real_int64 1347483576L);(* 9, 9 *)\r
(mk_real_int64 1621985411L),(mk_real_int64 1476594508L);(* 9, 9 *)\r
(mk_real_int64 1905717187L),(mk_real_int64 1385687671L);(* 9, 9 *)\r
(mk_real_int64 1933498295L),(mk_real_int64 1372564729L);(* 9, 9 *)\r
(mk_real_int64 1685249604L),(mk_real_int64 1571634580L);(* 9, 9 *)\r
(mk_real_int64 1252666975L),(mk_real_int64 1516719484L);(* 9, 9 *)\r
(mk_real_int64 1439022301L),(mk_real_int64 1487851103L);(* 9, 9 *)\r
(mk_real_int64 1890060210L),(mk_real_int64 1131039719L);(* 9, 9 *)\r
(mk_real_int64 1565774276L),(mk_real_int64 1458632273L);(* 9, 9 *)\r
(mk_real_int64 1361338436L),(mk_real_int64 1320470604L);(* 9, 9 *)\r
(mk_real_int64 1447530242L),(mk_real_int64 1035553289L);(* 9, 9 *)\r
(mk_real_int64 1452882647L),(mk_real_int64 1138812470L);(* 9, 9 *)\r
(mk_real_int64 1029131835L),(mk_real_int64 1401095232L);(* 9, 9 *)\r
(mk_real_int64 1034888464L),(mk_real_int64 1364064625L);(* 9, 9 *)\r
(mk_real_int64 1476497384L),(mk_real_int64 1717629991L);(* 9, 9 *)\r
(mk_real_int64 1315177038L),(mk_real_int64 1110008981L);(* 9, 9 *)\r
(mk_real_int64 1719417387L),(mk_real_int64 1391475156L);(* 9, 9 *)\r
(mk_real_int64 1072303213L),(mk_real_int64 1356472525L);(* 9, 9 *)\r
(mk_real_int64 1008179455L),(mk_real_int64 1456470865L);(* 9, 9 *)\r
(mk_real_int64 1171711274L),(mk_real_int64 1506579827L);(* 9, 9 *)\r
(mk_real_int64 1819932077L),(mk_real_int64 1078739945L);(* 9, 9 *)\r
(mk_real_int64 1489136038L),(mk_real_int64 1594096569L);(* 9, 9 *)\r
(mk_real_int64 1767310771L),(mk_real_int64 1334352607L);(* 9, 9 *)\r
(mk_real_int64 1055936770L),(mk_real_int64 1864799159L);(* 9, 9 *)\r
(mk_real_int64 1306849237L),(mk_real_int64 1071749938L);(* 9, 9 *)\r
(mk_real_int64 1206605485L),(mk_real_int64 1333286760L);(* 9, 9 *)\r
(mk_real_int64 1273282145L),(mk_real_int64 1136624391L);(* 9, 9 *)\r
(mk_real_int64 1354231152L),(mk_real_int64 1826391882L);(* 9, 9 *)\r
(mk_real_int64 1894600929L),(mk_real_int64 1483172940L);(* 9, 9 *)\r
(mk_real_int64 1447462672L),(mk_real_int64 1504621955L);(* 9, 9 *)\r
(mk_real_int64 1350799206L),(mk_real_int64 1569433670L);(* 9, 9 *)\r
(mk_real_int64 1896067345L),(mk_real_int64 1967619612L);(* 9, 9 *)\r
(mk_real_int64 1256457541L),(mk_real_int64 1142657994L);(* 9, 9 *)\r
(mk_real_int64 1797302096L),(mk_real_int64 1047547145L);(* 9, 9 *)\r
(mk_real_int64 1415547890L),(mk_real_int64 1533587684L);(* 9, 9 *)\r
(mk_real_int64 1122860263L),(mk_real_int64 1109303410L);(* 9, 9 *)\r
(mk_real_int64 1286920999L),(mk_real_int64 1854758609L);(* 9, 9 *)\r
(mk_real_int64 1500538526L),(mk_real_int64 1368790297L);(* 9, 9 *)\r
(mk_real_int64 1546417251L),(mk_real_int64 1858786078L);(* 9, 9 *)\r
(mk_real_int64 1371501699L),(mk_real_int64 1694779228L);(* 9, 9 *)\r
(mk_real_int64 1345158461L),(mk_real_int64 1170089305L);(* 9, 9 *)\r
(mk_real_int64 1057215387L),(mk_real_int64 1404747446L);(* 9, 9 *)\r
(mk_real_int64 1511024506L),(mk_real_int64 1981890277L);(* 9, 9 *)\r
(mk_real_int64 1836726835L),(mk_real_int64 1582792996L);(* 9, 9 *)\r
(mk_real_int64 1037244003L),(mk_real_int64 1245911330L);(* 9, 9 *)\r
(mk_real_int64 1461871596L),(mk_real_int64 1525006515L);(* 9, 9 *)\r
(mk_real_int64 1009008193L),(mk_real_int64 1667089319L);(* 9, 9 *)\r
(mk_real_int64 1155780620L),(mk_real_int64 1250498407L);(* 9, 9 *)\r
(mk_real_int64 1182672599L),(mk_real_int64 1521516426L);(* 9, 9 *)\r
(mk_real_int64 1337639028L),(mk_real_int64 1624652776L);(* 9, 9 *)\r
(mk_real_int64 1537050510L),(mk_real_int64 1008389625L);(* 9, 9 *)\r
(mk_real_int64 1449251268L),(mk_real_int64 1773261553L);(* 9, 9 *)\r
(mk_real_int64 1948889675L),(mk_real_int64 1097302075L);(* 9, 9 *)\r
(mk_real_int64 1046365761L),(mk_real_int64 1418523536L);(* 9, 9 *)\r
(mk_real_int64 1636085865L),(mk_real_int64 1985440855L);(* 9, 9 *)\r
(mk_real_int64 1279974631L),(mk_real_int64 1035814851L);(* 9, 9 *)\r
(mk_real_int64 1111671240L),(mk_real_int64 1752683443L);(* 9, 9 *)\r
(mk_real_int64 1159463493L),(mk_real_int64 1180709901L);(* 9, 9 *)\r
(mk_real_int64 1512218282L),(mk_real_int64 1491319899L);(* 9, 9 *)\r
(mk_real_int64 1456595106L),(mk_real_int64 1274567263L);(* 9, 9 *)\r
(mk_real_int64 1305931159L),(mk_real_int64 1214509100L);(* 9, 9 *)\r
(mk_real_int64 1010303141L),(mk_real_int64 1169636560L);(* 9, 9 *)\r
(mk_real_int64 1071716087L),(mk_real_int64 1597853747L);(* 9, 9 *)\r
(mk_real_int64 1100295217L),(mk_real_int64 1619831680L);(* 9, 9 *)\r
(mk_real_int64 1698977988L),(mk_real_int64 1250040118L);(* 9, 9 *)\r
(mk_real_int64 1186117697L),(mk_real_int64 1024900824L);(* 9, 9 *)\r
(mk_real_int64 1521147049L),(mk_real_int64 1746848923L);(* 9, 9 *)\r
(mk_real_int64 1157728718L),(mk_real_int64 1336768836L);(* 9, 9 *)\r
(mk_real_int64 1720838037L),(mk_real_int64 1283953834L);(* 9, 9 *)\r
(mk_real_int64 1455857771L),(mk_real_int64 1413722431L);(* 9, 9 *)\r
(mk_real_int64 1935524516L),(mk_real_int64 1418203298L);(* 9, 9 *)\r
(mk_real_int64 1946707130L),(mk_real_int64 1051803148L);(* 9, 9 *)\r
(mk_real_int64 1965936698L),(mk_real_int64 1426056745L);(* 9, 9 *)\r
(mk_real_int64 1413335275L),(mk_real_int64 1256324749L);(* 9, 9 *)\r
(mk_real_int64 1507625825L),(mk_real_int64 1975070719L);(* 9, 9 *)\r
(mk_real_int64 1738280125L),(mk_real_int64 1691352700L);(* 9, 9 *)\r
(mk_real_int64 1064921319L),(mk_real_int64 1063071765L);(* 9, 9 *)\r
(mk_real_int64 1318721616L),(mk_real_int64 1322541409L);(* 9, 9 *)\r
(mk_real_int64 1998086483L),(mk_real_int64 1279614708L);(* 9, 9 *)\r
(mk_real_int64 1701545465L),(mk_real_int64 1351035927L);(* 9, 9 *)\r
(mk_real_int64 1997006857L),(mk_real_int64 1426534081L);(* 9, 9 *)\r
(mk_real_int64 1719545548L),(mk_real_int64 1386045746L);(* 9, 9 *)\r
(mk_real_int64 1799323157L),(mk_real_int64 1255073806L);(* 9, 9 *)\r
(mk_real_int64 1514667801L),(mk_real_int64 1364822317L);(* 9, 9 *)\r
(mk_real_int64 1594954725L),(mk_real_int64 1822694657L);(* 9, 9 *)\r
(mk_real_int64 1459871864L),(mk_real_int64 1228264447L);(* 9, 9 *)\r
(mk_real_int64 1035462128L),(mk_real_int64 1042872675L);(* 9, 9 *)\r
(mk_real_int64 1339042747L),(mk_real_int64 1887727860L);(* 9, 9 *)\r
(mk_real_int64 1267801969L),(mk_real_int64 1958499993L);(* 9, 9 *)\r
(mk_real_int64 1203699861L),(mk_real_int64 1645659342L);(* 9, 9 *)\r
(mk_real_int64 1184518472L),(mk_real_int64 1843970467L);(* 9, 9 *)\r
(mk_real_int64 1112205854L),(mk_real_int64 1723907268L);(* 9, 9 *)\r
(mk_real_int64 1511759993L),(mk_real_int64 1494764996L);(* 9, 9 *)\r
(mk_real_int64 1959979504L),(mk_real_int64 1458075284L);(* 9, 9 *)\r
(mk_real_int64 1428127306L),(mk_real_int64 1835187309L);(* 9, 9 *)\r
(mk_real_int64 1338682352L),(mk_real_int64 1441223329L);(* 9, 9 *)\r
(mk_real_int64 1582408369L),(mk_real_int64 1104821843L);(* 9, 9 *)\r
(mk_real_int64 1416715573L),(mk_real_int64 1508990434L);(* 9, 9 *)\r
(mk_real_int64 1698657750L),(mk_real_int64 1560661384L);(* 9, 9 *)\r
(mk_real_int64 1252479990L),(mk_real_int64 1710862892L);(* 9, 9 *)\r
(mk_real_int64 1911388944L),(mk_real_int64 1048512958L);(* 9, 9 *)\r
(mk_real_int64 1661370024L),(mk_real_int64 1684931168L);(* 9, 9 *)\r
(mk_real_int64 1515198855L),(mk_real_int64 1510015677L);(* 9, 9 *)\r
(mk_real_int64 1655890572L),(mk_real_int64 1022048644L);(* 9, 9 *)\r
(mk_real_int64 1724029017L),(mk_real_int64 1430993756L);(* 9, 9 *)\r
(mk_real_int64 1054739439L),(mk_real_int64 1039586490L);(* 9, 9 *)\r
(mk_real_int64 1075914846L),(mk_real_int64 1055886122L);(* 9, 9 *)\r
(mk_real_int64 1166517455L),(mk_real_int64 1153036390L);(* 9, 9 *)\r
(mk_real_int64 1314328226L),(mk_real_int64 1995638280L);(* 9, 9 *)\r
(mk_real_int64 1874285753L),(mk_real_int64 1304558160L);(* 9, 9 *)\r
(mk_real_int64 1295094302L),(mk_real_int64 1056592516L);(* 9, 9 *)\r
(mk_real_int64 1936695010L),(mk_real_int64 1759767415L);(* 9, 9 *)\r
(mk_real_int64 1484012304L),(mk_real_int64 1018648535L);(* 9, 9 *)\r
(mk_real_int64 1645856077L),(mk_real_int64 1930640284L);(* 9, 9 *)\r
(mk_real_int64 1626157102L),(mk_real_int64 1830052312L);(* 9, 9 *)\r
(mk_real_int64 1189070110L),(mk_real_int64 1707140585L);(* 9, 9 *)\r
(mk_real_int64 1706020002L),(mk_real_int64 1492836969L);(* 9, 9 *)\r
(mk_real_int64 1734270397L),(mk_real_int64 1136005514L);(* 9, 9 *)\r
(mk_real_int64 1182600443L),(mk_real_int64 1427274686L);(* 9, 9 *)\r
(mk_real_int64 1208708413L),(mk_real_int64 1001744315L);(* 9, 9 *)\r
(mk_real_int64 1838874424L),(mk_real_int64 1937930860L);(* 9, 9 *)\r
(mk_real_int64 1734046266L),(mk_real_int64 1997133550L);(* 9, 9 *)\r
(mk_real_int64 1780447869L),(mk_real_int64 1299095862L);(* 9, 9 *)\r
(mk_real_int64 1365308482L),(mk_real_int64 1526522246L);(* 9, 9 *)\r
(mk_real_int64 1938304388L),(mk_real_int64 1263679183L);(* 9, 9 *)\r
(mk_real_int64 1194662207L),(mk_real_int64 1703019469L);(* 9, 9 *)\r
(mk_real_int64 1686375630L),(mk_real_int64 1947921829L);(* 9, 9 *)\r
(mk_real_int64 1415768590L),(mk_real_int64 1854796427L);(* 9, 9 *)\r
(mk_real_int64 1111817947L),(mk_real_int64 1901602608L);(* 9, 9 *)\r
(mk_real_int64 1200918863L),(mk_real_int64 1496550320L);(* 9, 9 *)\r
(mk_real_int64 1864159600L),(mk_real_int64 1725250288L);(* 9, 9 *)\r
(mk_real_int64 1395891542L),(mk_real_int64 1893976705L);(* 9, 9 *)\r
(mk_real_int64 1241923645L),(mk_real_int64 1347598853L);(* 9, 9 *)\r
(mk_real_int64 1333566487L),(mk_real_int64 1583077877L);(* 9, 9 *)\r
(mk_real_int64 1321615724L),(mk_real_int64 1030511940L);(* 9, 9 *)\r
(mk_real_int64 1970435946L),(mk_real_int64 1887053540L);(* 9, 9 *)\r
(mk_real_int64 1786929867L),(mk_real_int64 1872541437L);(* 9, 9 *)\r
(mk_real_int64 1465683736L),(mk_real_int64 1357163441L);(* 9, 9 *)\r
(mk_real_int64 1322546249L),(mk_real_int64 1939561459L);(* 9, 9 *)\r
(mk_real_int64 1979319545L),(mk_real_int64 1184916442L);(* 9, 9 *)\r
(mk_real_int64 1653340052L),(mk_real_int64 1119333830L);(* 9, 9 *)\r
(mk_real_int64 1992335896L),(mk_real_int64 1362477918L);(* 9, 9 *)\r
(mk_real_int64 1635390104L),(mk_real_int64 1486050640L);(* 9, 9 *)\r
(mk_real_int64 1020764954L),(mk_real_int64 1758098172L);(* 9, 9 *)\r
(mk_real_int64 1077068379L),(mk_real_int64 1879473970L);(* 9, 9 *)\r
(mk_real_int64 1024187566L),(mk_real_int64 1280997834L);(* 9, 9 *)\r
(mk_real_int64 1226355822L),(mk_real_int64 1712158092L);(* 9, 9 *)\r
(mk_real_int64 1137584715L),(mk_real_int64 1113624136L);(* 9, 9 *)\r
(mk_real_int64 1542039317L),(mk_real_int64 1840069561L);(* 9, 9 *)\r
(mk_real_int64 1755209905L),(mk_real_int64 1432849016L);(* 9, 9 *)\r
(mk_real_int64 1965529374L),(mk_real_int64 1782230604L);(* 9, 9 *)\r
(mk_real_int64 1204906521L),(mk_real_int64 1907792447L);(* 9, 9 *)\r
(mk_real_int64 1293243236L),(mk_real_int64 1307608667L);(* 9, 9 *)\r
(mk_real_int64 1916089602L),(mk_real_int64 1813834193L);(* 9, 9 *)\r
(mk_real_int64 1482238093L),(mk_real_int64 1058605148L);(* 9, 9 *)\r
(mk_real_int64 1532250177L),(mk_real_int64 1172256487L);(* 9, 9 *)\r
(mk_real_int64 1922283062L),(mk_real_int64 1016002421L);(* 9, 9 *)\r
(mk_real_int64 1843210267L),(mk_real_int64 1744825769L);(* 9, 9 *)\r
(mk_real_int64 1732914392L),(mk_real_int64 1033413623L);(* 9, 9 *)\r
(mk_real_int64 1258586601L),(mk_real_int64 1755873004L);(* 9, 9 *)\r
(mk_real_int64 1326833898L),(mk_real_int64 1575468315L);(* 9, 9 *)\r
(mk_real_int64 1506009498L),(mk_real_int64 1442141754L);(* 9, 9 *)\r
(mk_real_int64 1006324374L),(mk_real_int64 1689438111L);(* 9, 9 *)\r
(mk_real_int64 1660697717L),(mk_real_int64 1074771774L);(* 9, 9 *)\r
(mk_real_int64 1734956722L),(mk_real_int64 1352059600L);(* 9, 9 *)\r
(mk_real_int64 1815124124L),(mk_real_int64 1482476688L);(* 9, 9 *)\r
(mk_real_int64 1184351554L),(mk_real_int64 1546470529L);(* 9, 9 *)\r
(mk_real_int64 1219387068L),(mk_real_int64 1871109447L);(* 9, 9 *)\r
(mk_real_int64 1914427308L),(mk_real_int64 1084543448L);(* 9, 9 *)\r
(mk_real_int64 1069234682L),(mk_real_int64 1327781437L);(* 9, 9 *)\r
(mk_real_int64 1569961038L),(mk_real_int64 1206930761L);(* 9, 9 *)\r
(mk_real_int64 1275860079L),(mk_real_int64 1018463231L);(* 9, 9 *)\r
(mk_real_int64 1347223792L),(mk_real_int64 1851931078L);(* 9, 9 *)\r
(mk_real_int64 1358714772L),(mk_real_int64 1210353401L);(* 9, 9 *)\r
(mk_real_int64 1868947824L),(mk_real_int64 1392758945L);(* 9, 9 *)\r
(mk_real_int64 1380709743L),(mk_real_int64 1508625693L);(* 9, 9 *)\r
(mk_real_int64 1581482960L),(mk_real_int64 1999336901L);(* 9, 9 *)\r
(mk_real_int64 1106015117L),(mk_real_int64 1390061059L);(* 9, 9 *)\r
(mk_real_int64 1276221106L),(mk_real_int64 1762764767L);(* 9, 9 *)\r
(mk_real_int64 1901468073L),(mk_real_int64 1603805124L);(* 9, 9 *)\r
(mk_real_int64 1646910949L),(mk_real_int64 1841317828L);(* 9, 9 *)\r
(mk_real_int64 1078877470L),(mk_real_int64 1130178492L);(* 9, 9 *)\r
(mk_real_int64 1243481023L),(mk_real_int64 1049773489L);(* 9, 9 *)\r
(mk_real_int64 1987904933L),(mk_real_int64 1375812533L);(* 9, 9 *)\r
(mk_real_int64 1796615353L),(mk_real_int64 1972100819L);(* 9, 9 *)\r
(mk_real_int64 1830398460L),(mk_real_int64 1648370943L);(* 9, 9 *)\r
(mk_real_int64 1964178941L),(mk_real_int64 1930805163L);(* 9, 9 *)\r
(mk_real_int64 1185911966L),(mk_real_int64 1119903137L);(* 9, 9 *)\r
(mk_real_int64 1299608235L),(mk_real_int64 1487546267L);(* 9, 9 *)\r
(mk_real_int64 1094917962L),(mk_real_int64 1154393295L);(* 9, 9 *)\r
(mk_real_int64 1330723339L),(mk_real_int64 1450344315L);(* 9, 9 *)\r
(mk_real_int64 1205823949L),(mk_real_int64 1342197776L);(* 9, 9 *)\r
(mk_real_int64 1971349856L),(mk_real_int64 1306498431L);(* 9, 9 *)\r
(mk_real_int64 1900993728L),(mk_real_int64 1185014653L);(* 9, 9 *)\r
(mk_real_int64 1440455412L),(mk_real_int64 1829326008L);(* 9, 9 *)\r
(mk_real_int64 1594888341L),(mk_real_int64 1151662541L);(* 9, 9 *)\r
(mk_real_int64 1183075375L),(mk_real_int64 1465429557L);(* 9, 9 *)\r
(mk_real_int64 1680870487L),(mk_real_int64 1728643210L);(* 9, 9 *)\r
(mk_real_int64 1128053291L),(mk_real_int64 1145681587L);(* 9, 9 *)\r
(mk_real_int64 1774982207L),(mk_real_int64 1297450303L);(* 9, 9 *)\r
(mk_real_int64 1864026145L),(mk_real_int64 1982902239L);(* 9, 9 *)\r
(mk_real_int64 1413738048L),(mk_real_int64 1896847004L);(* 9, 9 *)\r
(mk_real_int64 1562360484L),(mk_real_int64 1732338799L);(* 9, 9 *)\r
(mk_real_int64 1544446751L),(mk_real_int64 1650677796L);(* 9, 9 *)\r
(mk_real_int64 1813424935L),(mk_real_int64 1986111980L);(* 9, 9 *)\r
(mk_real_int64 1090452823L),(mk_real_int64 1788674839L);(* 9, 9 *)\r
(mk_real_int64 1667846804L),(mk_real_int64 1747074778L);(* 9, 9 *)\r
(mk_real_int64 1273081784L),(mk_real_int64 1196566633L);(* 9, 9 *)\r
(mk_real_int64 1635493878L),(mk_real_int64 1736679693L);(* 9, 9 *)\r
(mk_real_int64 1158828635L),(mk_real_int64 1936982592L);(* 9, 9 *)\r
(mk_real_int64 1148779760L),(mk_real_int64 1802890280L);(* 9, 9 *)\r
(mk_real_int64 1935357120L),(mk_real_int64 1967289344L);(* 9, 9 *)\r
(mk_real_int64 1377212478L),(mk_real_int64 1678735919L);(* 9, 9 *)\r
(mk_real_int64 1465295568L),(mk_real_int64 1498749383L);(* 9, 9 *)\r
(mk_real_int64 1249934676L),(mk_real_int64 1457268756L);(* 9, 9 *)\r
(mk_real_int64 1991849845L),(mk_real_int64 1153926648L);(* 9, 9 *)\r
(mk_real_int64 1712564059L),(mk_real_int64 1797467659L);(* 9, 9 *)\r
(mk_real_int64 1290367150L),(mk_real_int64 1347821100L);(* 9, 9 *)\r
(mk_real_int64 1036606267L),(mk_real_int64 1308976944L);(* 9, 9 *)\r
(mk_real_int64 1779837292L),(mk_real_int64 1239011056L);(* 9, 9 *)\r
(mk_real_int64 1762051679L),(mk_real_int64 1250315932L);(* 9, 9 *)\r
(mk_real_int64 1371589718L),(mk_real_int64 1454343431L);(* 9, 9 *)\r
(mk_real_int64 1738873185L),(mk_real_int64 1806213502L);(* 9, 9 *)\r
(mk_real_int64 1483815736L),(mk_real_int64 1436000596L);(* 9, 9 *)\r
(mk_real_int64 1192347772L),(mk_real_int64 1484303853L);(* 9, 9 *)\r
(mk_real_int64 1093149331L),(mk_real_int64 1391373597L);(* 9, 9 *)\r
(mk_real_int64 1986852951L),(mk_real_int64 1837999615L);(* 9, 9 *)\r
(mk_real_int64 1148670542L),(mk_real_int64 1061135864L);(* 9, 9 *)\r
(mk_real_int64 1047545118L),(mk_real_int64 1446448703L);(* 9, 9 *)\r
(mk_real_int64 1519634526L),(mk_real_int64 1883624565L);(* 9, 9 *)\r
(mk_real_int64 1267043231L),(mk_real_int64 1045697367L);(* 9, 9 *)\r
(mk_real_int64 1400743119L),(mk_real_int64 1356156178L);(* 9, 9 *)\r
(mk_real_int64 1994262134L),(mk_real_int64 1936526175L);(* 9, 9 *)\r
(mk_real_int64 1076110779L),(mk_real_int64 1870379145L);(* 9, 9 *)\r
(mk_real_int64 1456707627L),(mk_real_int64 1925260683L);(* 9, 9 *)\r
(mk_real_int64 1159960366L),(mk_real_int64 1326516933L);(* 9, 9 *)\r
(mk_real_int64 1956842401L),(mk_real_int64 1919817578L);(* 9, 9 *)\r
(mk_real_int64 1174930912L),(mk_real_int64 1898463828L);(* 9, 9 *)\r
(mk_real_int64 1431300562L),(mk_real_int64 1481013688L);(* 9, 9 *)\r
(mk_real_int64 1228416159L),(mk_real_int64 1570998976L);(* 9, 9 *)\r
(mk_real_int64 1194920182L),(mk_real_int64 1029294971L);(* 9, 9 *)\r
(mk_real_int64 1306401610L),(mk_real_int64 1765630823L);(* 9, 9 *)\r
(mk_real_int64 1364119424L),(mk_real_int64 1600476248L);(* 9, 9 *)\r
(mk_real_int64 1167073696L),(mk_real_int64 1874564443L);(* 9, 9 *)\r
(mk_real_int64 1648797116L),(mk_real_int64 1229231285L);(* 9, 9 *)\r
(mk_real_int64 1300275982L),(mk_real_int64 1590157563L);(* 9, 9 *)\r
(mk_real_int64 1789342418L),(mk_real_int64 1896212726L);(* 9, 9 *)\r
(mk_real_int64 1971967825L),(mk_real_int64 1716354311L);(* 9, 9 *)\r
(mk_real_int64 1849572812L),(mk_real_int64 1015433539L);(* 9, 9 *)\r
(mk_real_int64 1460081297L),(mk_real_int64 1802347009L);(* 9, 9 *)\r
(mk_real_int64 1730102722L),(mk_real_int64 1613436591L);(* 9, 9 *)\r
(mk_real_int64 1979292969L),(mk_real_int64 1267087089L);(* 9, 9 *)\r
(mk_real_int64 1324343486L),(mk_real_int64 1766632397L);(* 9, 9 *)\r
(mk_real_int64 1434531196L),(mk_real_int64 1067035372L);(* 9, 9 *)\r
(mk_real_int64 1663068703L),(mk_real_int64 1250206714L);(* 9, 9 *)\r
(mk_real_int64 1629835301L),(mk_real_int64 1566531429L);(* 9, 9 *)\r
(mk_real_int64 1218032544L),(mk_real_int64 1948635550L);(* 9, 9 *)\r
(mk_real_int64 1688704383L),(mk_real_int64 1237748259L);(* 9, 9 *)\r
(mk_real_int64 1739295756L),(mk_real_int64 1635112296L);(* 9, 9 *)\r
(mk_real_int64 1992036754L),(mk_real_int64 1393785886L);(* 9, 9 *)\r
(mk_real_int64 1769452478L),(mk_real_int64 1201546336L);(* 9, 9 *)\r
(mk_real_int64 1221582029L),(mk_real_int64 1227476341L);(* 9, 9 *)\r
(mk_real_int64 1624984701L),(mk_real_int64 1569802802L);(* 9, 9 *)\r
(mk_real_int64 1537174515L),(mk_real_int64 1060629675L);(* 9, 9 *)\r
(mk_real_int64 1947849753L),(mk_real_int64 1458576600L);(* 9, 9 *)\r
(mk_real_int64 1048891015L),(mk_real_int64 1415867023L);(* 9, 9 *)\r
(mk_real_int64 1020932391L),(mk_real_int64 1426069149L);(* 9, 9 *)\r
(mk_real_int64 1840896253L),(mk_real_int64 1581483591L);(* 9, 9 *)\r
(mk_real_int64 1050002002L),(mk_real_int64 1039314521L);(* 9, 9 *)\r
(mk_real_int64 1441287336L),(mk_real_int64 1597487027L);(* 9, 9 *)\r
(mk_real_int64 1165945051L),(mk_real_int64 1100038324L);(* 9, 9 *)\r
(mk_real_int64 1211495740L),(mk_real_int64 1398590402L);(* 9, 9 *)\r
(mk_real_int64 1599395984L),(mk_real_int64 1733744553L);(* 9, 9 *)\r
(mk_real_int64 1372125019L),(mk_real_int64 1840706868L);(* 9, 9 *)\r
(mk_real_int64 1207508342L),(mk_real_int64 1734219566L);(* 9, 9 *)\r
(mk_real_int64 1977058554L),(mk_real_int64 1214460516L);(* 9, 9 *)\r
(mk_real_int64 1023396784L),(mk_real_int64 1066295410L);(* 9, 9 *)\r
(mk_real_int64 1032894530L),(mk_real_int64 1528556386L);(* 9, 9 *)\r
(mk_real_int64 1391854562L),(mk_real_int64 1751816627L);(* 9, 9 *)\r
(mk_real_int64 1642102387L),(mk_real_int64 1754540684L);(* 9, 9 *)\r
(mk_real_int64 1229457881L),(mk_real_int64 1373901521L);(* 9, 9 *)\r
(mk_real_int64 1119185619L),(mk_real_int64 1204492102L);(* 9, 9 *)\r
(mk_real_int64 1201315698L),(mk_real_int64 1213968278L);(* 9, 9 *)\r
(mk_real_int64 1545599037L),(mk_real_int64 1791963394L);(* 9, 9 *)\r
(mk_real_int64 1107739296L),(mk_real_int64 1107220792L);(* 9, 9 *)\r
(mk_real_int64 1187746256L),(mk_real_int64 1699981234L);(* 9, 9 *)\r
(mk_real_int64 1193824959L),(mk_real_int64 1394549727L);(* 9, 9 *)\r
(mk_real_int64 1227840834L),(mk_real_int64 1669414154L);(* 9, 9 *)\r
(mk_real_int64 1990050595L),(mk_real_int64 1822991626L);(* 9, 9 *)\r
(mk_real_int64 1628080357L),(mk_real_int64 1891240148L);(* 9, 9 *)\r
(mk_real_int64 1197677783L),(mk_real_int64 1696467647L);(* 9, 9 *)\r
(mk_real_int64 1853121332L),(mk_real_int64 1213630186L);(* 9, 9 *)\r
(mk_real_int64 1481518045L),(mk_real_int64 1834430499L);(* 9, 9 *)\r
(mk_real_int64 1392470238L),(mk_real_int64 1954636981L);(* 9, 9 *)\r
(mk_real_int64 1393174619L),(mk_real_int64 1312339867L);(* 9, 9 *)\r
(mk_real_int64 1189629029L),(mk_real_int64 1298185375L);(* 9, 9 *)\r
(mk_real_int64 1397212134L),(mk_real_int64 1686746652L);(* 9, 9 *)\r
(mk_real_int64 1368029145L),(mk_real_int64 1792043530L);(* 9, 9 *)\r
(mk_real_int64 1980852705L),(mk_real_int64 1007003637L);(* 9, 9 *)\r
(mk_real_int64 1197274704L),(mk_real_int64 1385427705L);(* 9, 9 *)\r
(mk_real_int64 1188145515L),(mk_real_int64 1580161624L);(* 9, 9 *)\r
(mk_real_int64 1732967571L),(mk_real_int64 1100287550L);(* 9, 9 *)\r
(mk_real_int64 1546473309L),(mk_real_int64 1277077320L);(* 9, 9 *)\r
(mk_real_int64 1020635556L),(mk_real_int64 1628847057L);(* 9, 9 *)\r
(mk_real_int64 1838454575L),(mk_real_int64 1363480376L);(* 9, 9 *)\r
(mk_real_int64 1538505790L),(mk_real_int64 1568862935L);(* 9, 9 *)\r
(mk_real_int64 1123736269L),(mk_real_int64 1750862239L);(* 9, 9 *)\r
(mk_real_int64 1556862900L),(mk_real_int64 1532990234L);(* 9, 9 *)\r
(mk_real_int64 1520780188L),(mk_real_int64 1905555432L);(* 9, 9 *)\r
(mk_real_int64 1722974056L),(mk_real_int64 1366885198L);(* 9, 9 *)\r
(mk_real_int64 1821498040L),(mk_real_int64 1590962056L);(* 9, 9 *)\r
(mk_real_int64 1398788775L),(mk_real_int64 1795399428L);(* 9, 9 *)\r
(mk_real_int64 1917591763L),(mk_real_int64 1889560881L);(* 9, 9 *)\r
(mk_real_int64 1302769100L),(mk_real_int64 1507078306L);(* 9, 9 *)\r
(mk_real_int64 1026520581L),(mk_real_int64 1435797304L);(* 9, 9 *)\r
(mk_real_int64 1688561448L),(mk_real_int64 1983046957L);(* 9, 9 *)\r
(mk_real_int64 1625716922L),(mk_real_int64 1242652651L);(* 9, 9 *)\r
(mk_real_int64 1703094632L),(mk_real_int64 1617516159L);(* 9, 9 *)\r
(mk_real_int64 1963500075L),(mk_real_int64 1752833781L);(* 9, 9 *)\r
(mk_real_int64 1667156877L),(mk_real_int64 1204440725L);(* 9, 9 *)\r
(mk_real_int64 1813794942L),(mk_real_int64 1763623180L);(* 9, 9 *)\r
(mk_real_int64 1116182405L),(mk_real_int64 1029694242L);(* 9, 9 *)\r
(mk_real_int64 1773834077L),(mk_real_int64 1620766093L);(* 9, 9 *)\r
(mk_real_int64 1174449105L),(mk_real_int64 1646349895L);(* 9, 9 *)\r
(mk_real_int64 1129883752L),(mk_real_int64 1835038911L);(* 9, 9 *)\r
(mk_real_int64 1271263342L),(mk_real_int64 1075297273L);(* 9, 9 *)\r
(mk_real_int64 1284029581L),(mk_real_int64 1830389505L);(* 9, 9 *)\r
(mk_real_int64 1563929665L),(mk_real_int64 1597183459L);(* 9, 9 *)\r
(mk_real_int64 1181372848L),(mk_real_int64 1937568142L);(* 9, 9 *)\r
(mk_real_int64 1182695787L),(mk_real_int64 1656912428L);(* 9, 9 *)\r
(mk_real_int64 1974308219L),(mk_real_int64 1513557249L);(* 9, 9 *)\r
(mk_real_int64 1602326475L),(mk_real_int64 1402657271L);(* 9, 9 *)\r
(mk_real_int64 1674918928L),(mk_real_int64 1555458832L);(* 9, 9 *)\r
(mk_real_int64 1943146012L),(mk_real_int64 1881083617L);(* 9, 9 *)\r
(mk_real_int64 1047767606L),(mk_real_int64 1939346740L);(* 9, 9 *)\r
(mk_real_int64 1569490158L),(mk_real_int64 1767946407L);(* 9, 9 *)\r
(mk_real_int64 1238398554L),(mk_real_int64 1518533331L);(* 9, 9 *)\r
(mk_real_int64 1553090256L),(mk_real_int64 1057874859L);(* 9, 9 *)\r
(mk_real_int64 1474779650L),(mk_real_int64 1369094533L);(* 9, 9 *)\r
(mk_real_int64 1021565351L),(mk_real_int64 1296825669L);(* 9, 9 *)\r
(mk_real_int64 1715111776L),(mk_real_int64 1656419205L);(* 9, 9 *)\r
(mk_real_int64 1377194554L),(mk_real_int64 1191481670L);(* 9, 9 *)\r
(mk_real_int64 1164533962L),(mk_real_int64 1613264175L);(* 9, 9 *)\r
(mk_real_int64 1699017376L),(mk_real_int64 1795327417L);(* 9, 9 *)\r
(mk_real_int64 1678722986L),(mk_real_int64 1105911173L);(* 9, 9 *)\r
(mk_real_int64 1436143310L),(mk_real_int64 1025931932L);(* 9, 9 *)\r
(mk_real_int64 1570137994L),(mk_real_int64 1010244449L);(* 9, 9 *)\r
(mk_real_int64 1230132505L),(mk_real_int64 1300237692L);(* 9, 9 *)\r
(mk_real_int64 1161296704L),(mk_real_int64 1713525134L);(* 9, 9 *)\r
(mk_real_int64 1354775314L),(mk_real_int64 1218375244L);(* 9, 9 *)\r
(mk_real_int64 1677620081L),(mk_real_int64 1293365487L);(* 9, 9 *)\r
(mk_real_int64 1598582288L),(mk_real_int64 1190537011L);(* 9, 9 *)\r
(mk_real_int64 1265548752L),(mk_real_int64 1503316934L);(* 9, 9 *)\r
(mk_real_int64 1836898718L),(mk_real_int64 1765496250L);(* 9, 9 *)\r
(mk_real_int64 1277299248L),(mk_real_int64 1506054806L);(* 9, 9 *)\r
(mk_real_int64 1122403808L),(mk_real_int64 1812278315L);(* 9, 9 *)\r
(mk_real_int64 1916002791L),(mk_real_int64 1885870118L);(* 9, 9 *)\r
(mk_real_int64 1941800652L),(mk_real_int64 1317889014L);(* 9, 9 *)\r
(mk_real_int64 1136362695L),(mk_real_int64 1410844804L);(* 9, 9 *)\r
(mk_real_int64 1238123309L),(mk_real_int64 1061654752L);(* 9, 9 *)\r
(mk_real_int64 1856441456L),(mk_real_int64 1147818595L);(* 9, 9 *)\r
(mk_real_int64 1202360631L),(mk_real_int64 1941856433L);(* 9, 9 *)\r
(mk_real_int64 1503203430L),(mk_real_int64 1543558225L);(* 9, 9 *)\r
(mk_real_int64 1197808412L),(mk_real_int64 1228154105L);(* 9, 9 *)\r
(mk_real_int64 1288400825L),(mk_real_int64 1252852563L)(* 9, 9 *)\r
];;\r