Exact global Y/Z certificate: logs 4
Definitionmme_released_global_yz_logs_4matrix-multiplicationmore-asymmetrynumerical-certificate
One component of the exact six-orientation Y/Z certificate: word enumeration and cached integer counts, finite entropy expressions, or outward-rounded logarithm intervals. All numerical data are connected to the published profile by the accompanying full proofs. Tables are split by orientation to fit publication and compilation limits.
Definition code
import Definitions.Def_mme_released_global_yz_expression_primitives
open BigOperators MME MME.ReleasedGlobalYZ
set_option autoImplicit false
set_option maxRecDepth 100000
set_option maxHeartbeats 16000000
namespace MME.ReleasedGlobalYZ
private def mkLog (q : ℚ) (k : ℕ) (lo hi : ℤ) : Entry :=
((q,q),(k,(lo : ℚ)/1000000000000,(hi : ℚ)/1000000000000))
private def logTable : Fin 471 → Entry :=
![mkLog (23073656383/1000000000000) 6 (-3769063728605) (-3769063728484),
mkLog (113875631401/1000000000000) 4 (-2172648378773) (-2172648378692),
mkLog (289599598993/1000000000000) 2 (-1239256003185) (-1239256003144),
mkLog (352758014859/1000000000000) 2 (-1041972967454) (-1041972967413),
mkLog (1520635981/8000000000) 3 (-1660312885808) (-1660312885747),
mkLog (28920610917/1000000000000) 6 (-3543200757598) (-3543200757477),
mkLog (1659731621/1000000000000) 10 (-6401099363882) (-6401099363681),
mkLog (3313847/100000000000) 15 (-10314815714956) (-10314815714655),
mkLog (119731/1000000000000) 23 (-15938018277359) (-15938018276898),
mkLog (28468789396760345107446406007238903/1000000000000000000000000000000000000) 6 (-3558946900724) (-3558946900603),
mkLog (28469026303739654892553593992761097/1000000000000000000000000000000000000) 6 (-3558938579120) (-3558938578999),
mkLog (432579397863248126784592143683126190492670077/250000000000000000000000000000000000000000000000) 10 (-6359450308547) (-6359450308346),
mkLog (6229457016811971870336474576050799434507329923/125000000000000000000000000000000000000000000000) 5 (-2999024564562) (-2999024564461),
mkLog (432579397854614534881592143683126190492670077/250000000000000000000000000000000000000000000000) 10 (-6359450308567) (-6359450308366),
mkLog (45751775529640721506280727825301639/1000000000000000000000000000000000000) 5 (-3084524678673) (-3084524678572),
mkLog (45751775529120791894444727825301639/1000000000000000000000000000000000000) 5 (-3084524678685) (-3084524678584),
mkLog (2162896638138171634694380177205326824702753/1250000000000000000000000000000000000000000000) 10 (-6359450470912) (-6359450470711),
mkLog (45751775529169100362474727825301639/1000000000000000000000000000000000000) 5 (-3084524678684) (-3084524678583),
mkLog (45751775529379934810489727825301639/1000000000000000000000000000000000000) 5 (-3084524678679) (-3084524678578),
mkLog (31147231836027549252062841660870947550297247/625000000000000000000000000000000000000000000) 5 (-2999026274120) (-2999026274019),
mkLog (2162896637709512132371880177205326824702753/1250000000000000000000000000000000000000000000) 10 (-6359450471110) (-6359450470909),
mkLog (4628208381463250300849708444556079/2000000000000000000000000000000000000) 9 (-6068732625070) (-6068732624889),
mkLog (4628208381482405094173708444556079/2000000000000000000000000000000000000) 9 (-6068732625066) (-6068732624885),
mkLog (137089467110483071580282614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5899144527212) (-5899144527031),
mkLog (2009795500213392487853313337365868237237399203/25000000000000000000000000000000000000000000000) 4 (-2520842849201) (-2520842849120),
mkLog (137089467110727424682082614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5899144527210) (-5899144527029),
mkLog (2741789427041281378466165138916463390216789107/1000000000000000000000000000000000000000000000000) 9 (-5899144496272) (-5899144496091),
mkLog (2741789427027092338142165138916463390216789107/1000000000000000000000000000000000000000000000000) 9 (-5899144496277) (-5899144496096),
mkLog (137089467111436876698282614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5899144527205) (-5899144527024),
mkLog (2009795500253689609041513337365868237237399203/25000000000000000000000000000000000000000000000) 4 (-2520842849181) (-2520842849100),
mkLog (137089467108599068633482614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5899144527226) (-5899144527045),
mkLog (40195908708126024496037728570856918859783210893/500000000000000000000000000000000000000000000000) 4 (-2520842881447) (-2520842881366),
mkLog (40195908707308392352985728570856918859783210893/500000000000000000000000000000000000000000000000) 4 (-2520842881467) (-2520842881386),
mkLog (2314108275516364992141520294114479/1000000000000000000000000000000000000) 9 (-6068730859903) (-6068730859722),
mkLog (2741789427012667224926165138916463390216789107/1000000000000000000000000000000000000000000000000) 9 (-5899144496282) (-5899144496101),
mkLog (2314108275511438584623520294114479/1000000000000000000000000000000000000) 9 (-6068730859905) (-6068730859724),
mkLog (24097647176011399056217887718467/250000000000000000000000000000000000) 14 (-9247101988806) (-9247101988525),
mkLog (15759622966909140125392480948326599/4000000000000000000000000000000000000) 8 (-5536598479459) (-5536598479298),
mkLog (15759622966902258339488480948326599/4000000000000000000000000000000000000) 8 (-5536598479459) (-5536598479298),
mkLog (97021675684893272706044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240576143897) (-9240576143616),
mkLog (2047660266195635991782986851340355520325741350923585910123/500000000000000000000000000000000000000000000000000000000000) 8 (-5497910290733) (-5497910290572),
mkLog (97021675697428031955044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240576143768) (-9240576143487),
mkLog (15759622967000570188936480948326599/4000000000000000000000000000000000000) 8 (-5536598479453) (-5536598479292),
mkLog (15759622963887034333824480948326599/4000000000000000000000000000000000000) 8 (-5536598479651) (-5536598479490),
mkLog (2047660241644638620534374096901226043504143629923585910123/500000000000000000000000000000000000000000000000000000000000) 8 (-5497910302723) (-5497910302562),
mkLog (35399525453160613217793548476353226417985165617576414089877/250000000000000000000000000000000000000000000000000000000000) 3 (-1954762503121) (-1954762503060),
mkLog (2047660240921555072070874096901226043504143629923585910123/500000000000000000000000000000000000000000000000000000000000) 8 (-5497910303076) (-5497910302915),
mkLog (15759621703080868412210395910485009/4000000000000000000000000000000000000) 8 (-5536598559653) (-5536598559492),
mkLog (15759621703131007449206395910485009/4000000000000000000000000000000000000) 8 (-5536598559650) (-5536598559489),
mkLog (2047660268601449505462486851340355520325741350923585910123/500000000000000000000000000000000000000000000000000000000000) 8 (-5497910289558) (-5497910289397),
mkLog (97021675722251772385044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240576143512) (-9240576143231),
mkLog (15759621703081851524482395910485009/4000000000000000000000000000000000000) 8 (-5536598559653) (-5536598559492),
mkLog (15759621703535069081990395910485009/4000000000000000000000000000000000000) 8 (-5536598559624) (-5536598559463),
mkLog (96391816755526939264436618306769/1000000000000000000000000000000000000) 14 (-9247089248520) (-9247089248239),
mkLog (170630387716308834163263997260673/1000000000000000000000000000000000000) 13 (-8676010816295) (-8676010816034),
mkLog (188878971888402374263585824698797620581433767/1000000000000000000000000000000000000000000000000) 13 (-8574404108533) (-8574404108272),
mkLog (188878971878999174438585824698797620581433767/1000000000000000000000000000000000000000000000000) 13 (-8574404108583) (-8574404108322),
mkLog (170630387735251246225263997260673/1000000000000000000000000000000000000) 13 (-8676010816184) (-8676010815923),
mkLog (3340882259973279521296771953666548379418566233/500000000000000000000000000000000000000000000000) 8 (-5008373176703) (-5008373176542),
mkLog (3340882260745543760331271953666548379418566233/500000000000000000000000000000000000000000000000) 8 (-5008373176472) (-5008373176311),
mkLog (18887897062985124098799831629381041261473733/100000000000000000000000000000000000000000000000) 13 (-8574404115196) (-8574404114935),
mkLog (334088240717325059382220954329468258738526267/50000000000000000000000000000000000000000000000) 8 (-5008373132643) (-5008373132482),
mkLog (18887897062513263952399831629381041261473733/100000000000000000000000000000000000000000000000) 13 (-8574404115221) (-8574404114960),
mkLog (188878971874246569871585824698797620581433767/1000000000000000000000000000000000000000000000000) 13 (-8574404108608) (-8574404108347),
mkLog (334088240730005777904770954329468258738526267/50000000000000000000000000000000000000000000000) 8 (-5008373132605) (-5008373132444),
mkLog (18887897063450183624599831629381041261473733/100000000000000000000000000000000000000000000000) 13 (-8574404115172) (-8574404114911),
mkLog (170629850547770360021604726831649/1000000000000000000000000000000000000) 13 (-8676013964442) (-8676013964181),
mkLog (170629850581140601299604726831649/1000000000000000000000000000000000000) 13 (-8676013964246) (-8676013963985),
mkLog (128976991313567494485268502949790205351977/15625000000000000000000000000000000000000000000) 17 (-11704748727215) (-11704748726874),
mkLog (1834465471204064962763341909013834794648023/7812500000000000000000000000000000000000000000) 13 (-8356727151451) (-8356727151189),
mkLog (72318146794137437166725025817169/250000000000000000000000000000000000) 12 (-8148141106291) (-8148141106050),
mkLog (72318146438224360782475025817169/250000000000000000000000000000000000) 12 (-8148141111213) (-8148141110972),
mkLog (128976991313615723907143502949790205351977/15625000000000000000000000000000000000000000000) 17 (-11704748727215) (-11704748726874),
mkLog (72318146773516525222725025817169/250000000000000000000000000000000000) 12 (-8148141106576) (-8148141106335),
mkLog (72318146781867408103225025817169/250000000000000000000000000000000000) 12 (-8148141106461) (-8148141106220),
mkLog (257953986484129172241629664094907662799073/31250000000000000000000000000000000000000000000) 17 (-11704748712263) (-11704748711922),
mkLog (3668930992826403698861143057685592337200927/15625000000000000000000000000000000000000000000) 13 (-8356727137709) (-8356727137447),
mkLog (257953985574220732804129664094907662799073/31250000000000000000000000000000000000000000000) 17 (-11704748715790) (-11704748715449),
mkLog (3313847/400000000000) 17 (-11701110076096) (-11701110075755),
mkLog (16460001/4000000000000) 18 (-12400871663263) (-12400871662902),
mkLog (16460001/1000000000000) 16 (-11014577302123) (-11014577301802),
mkLog (778906987296021089/200000000000000000000000) 18 (-12455936286085) (-12455936285724),
mkLog (17719526188920738303/200000000000000000000000) 14 (-9331405439626) (-9331405439345),
mkLog (15222537299858840941/200000000000000000000000) 14 (-9483295598863) (-9483295598582),
mkLog (3805634242500085787/50000000000000000000000) 14 (-9483295620532) (-9483295620251),
mkLog (38945349359828813/10000000000000000000000) 18 (-12455936286213) (-12455936285852),
mkLog (3044507456312198481/40000000000000000000000) 14 (-9483295600065) (-9483295599784),
mkLog (15222537285339895907/200000000000000000000000) 14 (-9483295599817) (-9483295599536),
mkLog (155781395748753159/40000000000000000000000) 18 (-12455936297065) (-12455936296704),
mkLog (17719526055266888127/200000000000000000000000) 14 (-9331405447169) (-9331405446888),
mkLog (31156278632637521/8000000000000000000000) 18 (-12455936313663) (-12455936313302),
mkLog (99444829/200000000000) 11 (-7606469637671) (-7606469637450),
mkLog (1765545958452774649/31250000000000000000000) 15 (-9781314687859) (-9781314687558),
mkLog (3278862500762266979/62500000000000000000000) 15 (-9855425272176) (-9855425271875),
mkLog (6557724999755058409/125000000000000000000000) 15 (-9855425272446) (-9855425272145),
mkLog (3531091917495374481/62500000000000000000000) 15 (-9781314687692) (-9781314687391),
mkLog (127278655621474606427/125000000000000000000000) 10 (-6889690194782) (-6889690194581),
mkLog (127278655622654256793/125000000000000000000000) 10 (-6889690194773) (-6889690194572),
mkLog (6557725025707366461/125000000000000000000000) 15 (-9855425268489) (-9855425268188),
mkLog (127278651905575953527/125000000000000000000000) 10 (-6889690223977) (-6889690223776),
mkLog (3278862512558770639/62500000000000000000000) 15 (-9855425268579) (-9855425268278),
mkLog (63639325979035197407/62500000000000000000000) 10 (-6889690223565) (-6889690223364),
mkLog (655772502747684201/12500000000000000000000) 15 (-9855425268219) (-9855425267918),
mkLog (7062200060491708109/125000000000000000000000) 15 (-9781312390176) (-9781312389875),
mkLog (88277500734027907/1562500000000000000000) 15 (-9781312390427) (-9781312390125),
mkLog (589825183/125000000000) 8 (-5356242823371) (-5356242823210),
mkLog (22393770251697340123/1000000000000000000000000) 16 (-10706727751709) (-10706727751388),
mkLog (78231354924687299107/200000000000000000000000) 12 (-7846402120346) (-7846402120105),
mkLog (195578387354729681901/500000000000000000000000) 12 (-7846402120126) (-7846402119885),
mkLog (22287440628523533207/1000000000000000000000000) 16 (-10711487238831) (-10711487238510),
mkLog (95069024086134514327/250000000000000000000000) 12 (-7874612999861) (-7874612999620),
mkLog (97789193683509331541/250000000000000000000000) 12 (-7846402120063) (-7846402119822),
mkLog (391156774795482232069/1000000000000000000000000) 12 (-7846402119906) (-7846402119665),
mkLog (380276099674851957359/1000000000000000000000000) 12 (-7874612991103) (-7874612990862),
mkLog (7504685405222290146753/1000000000000000000000000) 8 (-4892227732881) (-4892227732720),
mkLog (190138049954171299899/500000000000000000000000) 12 (-7874612990489) (-7874612990248),
mkLog (195578398783482180231/500000000000000000000000) 12 (-7846402061691) (-7846402061450),
mkLog (11883627993869465167/31250000000000000000000) 12 (-7874613001283) (-7874613001042),
mkLog (5571860160203128597/250000000000000000000000) 16 (-10711487238280) (-10711487237959),
mkLog (391156797554675379281/1000000000000000000000000) 12 (-7846402061722) (-7846402061481),
mkLog (391156797530097416919/1000000000000000000000000) 12 (-7846402061785) (-7846402061544),
mkLog (5598390546739241153/250000000000000000000000) 16 (-10706737042941) (-10706737042620),
mkLog (12288981181/1000000000000) 7 (-4399052257121) (-4399052256980),
mkLog (13176637304979077667/250000000000000000000000) 15 (-9850770836667) (-9850770836366),
mkLog (329415932594916441/6250000000000000000000) 15 (-9850770836757) (-9850770836456),
mkLog (11643695508540319461/250000000000000000000000) 15 (-9974451321528) (-9974451321227),
mkLog (129570492033450696087/125000000000000000000000) 10 (-6871843943319) (-6871843943118),
mkLog (582184775249652969/12500000000000000000000) 15 (-9974451321833) (-9974451321532),
mkLog (11643695246043073467/250000000000000000000000) 15 (-9974451344072) (-9974451343771),
mkLog (5821847621247906693/125000000000000000000000) 15 (-9974451344377) (-9974451344076),
mkLog (16196311540097345331/15625000000000000000000) 10 (-6871843941101) (-6871843940900),
mkLog (11643695494351279137/250000000000000000000000) 15 (-9974451322747) (-9974451322446),
mkLog (64785247504800952023/62500000000000000000000) 10 (-6871843920349) (-6871843920148),
mkLog (259140990003832347741/250000000000000000000000) 10 (-6871843920408) (-6871843920207),
mkLog (3294155082243687507/62500000000000000000000) 15 (-9850772125009) (-9850772124708),
mkLog (1647077541713053767/31250000000000000000000) 15 (-9850772124650) (-9850772124349),
mkLog (1182420027/250000000000) 8 (-5353897709290) (-5353897709129),
mkLog (27730962997944209/8000000000000000000000) 19 (-12572402513153) (-12572402512772),
mkLog (3125786575857834023/40000000000000000000000) 14 (-9456948777447) (-9456948777166),
mkLog (3466370376754520513/1000000000000000000000000) 19 (-12572402512573) (-12572402512192),
mkLog (83179672007815437357/1000000000000000000000000) 14 (-9394507566960) (-9394507566679),
mkLog (83179672013849920521/1000000000000000000000000) 14 (-9394507566888) (-9394507566607),
mkLog (216648174539436577/62500000000000000000000) 19 (-12572402392598) (-12572402392217),
mkLog (83179672008821184551/1000000000000000000000000) 14 (-9394507566948) (-9394507566667),
mkLog (41589836003153408283/500000000000000000000000) 14 (-9394507566978) (-9394507566697),
mkLog (39072381244239151093/500000000000000000000000) 14 (-9456947522185) (-9456947521904),
mkLog (1733185267076978187/500000000000000000000000) 19 (-12572402467166) (-12572402466784),
mkLog (502873597/1000000000000) 11 (-7595171717767) (-7595171717546),
mkLog (16581709/4000000000000) 18 (-12393504698875) (-12393504698514),
mkLog (16581709/1000000000000) 16 (-11007210337735) (-11007210337414),
mkLog (119929/1000000000000) 23 (-15936365936167) (-15936365935706),
mkLog (11536768227/500000000000) 6 (-3769068926278) (-3769068926157),
mkLog (28464643969510345107446406007238903/1000000000000000000000000000000000000) 6 (-3559092524376) (-3559092524255),
mkLog (28464880876489654892553593992761097/1000000000000000000000000000000000000) 6 (-3559084201560) (-3559084201439),
mkLog (28464762423/250000000000) 4 (-2172794001820) (-2172794001739),
mkLog (431712805269562370253342143683126190492670077/250000000000000000000000000000000000000000000000) 10 (-6361455632397) (-6361455632196),
mkLog (6219688933762416139014599576050799434507329923/125000000000000000000000000000000000000000000000) 5 (-3000593842502) (-3000593842401),
mkLog (431712805260425904753342143683126190492670077/250000000000000000000000000000000000000000000000) 10 (-6361455632418) (-6361455632217),
mkLog (45668595857632906068923727825301639/1000000000000000000000000000000000000) 5 (-3086344397708) (-3086344397607),
mkLog (45668595857106941973923727825301639/1000000000000000000000000000000000000) 5 (-3086344397719) (-3086344397618),
mkLog (2158563674647382903154380177205326824702753/1250000000000000000000000000000000000000000000) 10 (-6361455795330) (-6361455795129),
mkLog (45668595857160279177923727825301639/1000000000000000000000000000000000000) 5 (-3086344397718) (-3086344397617),
mkLog (45668595857373627993923727825301639/1000000000000000000000000000000000000) 5 (-3086344397713) (-3086344397612),
mkLog (31098391359472250313196591660870947550297247/625000000000000000000000000000000000000000000) 5 (-3000595556716) (-3000595556615),
mkLog (2158563674541819686904380177205326824702753/1250000000000000000000000000000000000000000000) 10 (-6361455795379) (-6361455795178),
mkLog (72274181349/250000000000) 2 (-1240993956935) (-1240993956894),
mkLog (4522795283023417679513708444556079/2000000000000000000000000000000000000) 9 (-6091772231487) (-6091772231306),
mkLog (4522795283052031833053708444556079/2000000000000000000000000000000000000) 9 (-6091772231481) (-6091772231300),
mkLog (134760728008775007688082614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5916277463716) (-5916277463535),
mkLog (1983881401806702348635913337365868237237399203/25000000000000000000000000000000000000000000000) 4 (-2533820595148) (-2533820595067),
mkLog (134760728009728812806082614235649687762600797/50000000000000000000000000000000000000000000000) 9 (-5916277463709) (-5916277463528),
mkLog (2695214646057109084598165138916463390216789107/1000000000000000000000000000000000000000000000000) 9 (-5916277431851) (-5916277431670),
mkLog (1983881401789533856511913337365868237237399203/25000000000000000000000000000000000000000000000) 4 (-2533820595157) (-2533820595076),
mkLog (39677626728087616879853728570856918859783210893/500000000000000000000000000000000000000000000000) 4 (-2533820628115) (-2533820628034),
mkLog (39677626727300727657503728570856918859783210893/500000000000000000000000000000000000000000000000) 4 (-2533820628135) (-2533820628054),
mkLog (2261401794200465992029520294114479/1000000000000000000000000000000000000) 9 (-6091770395152) (-6091770394971),
mkLog (2695214646028494931058165138916463390216789107/1000000000000000000000000000000000000000000000000) 9 (-5916277431862) (-5916277431681),
mkLog (2261401794176620864079520294114479/1000000000000000000000000000000000000) 9 (-6091770395162) (-6091770394981),
mkLog (348028334751/1000000000000) 2 (-1055471380845) (-1055471380804),
mkLog (18499204613087064025467887718467/250000000000000000000000000000000000) 14 (-9511488459713) (-9511488459432),
mkLog (14194995868415394143252480948326599/4000000000000000000000000000000000000) 9 (-5641160141327) (-5641160141146),
mkLog (14194995868064420884280480948326599/4000000000000000000000000000000000000) 9 (-5641160141352) (-5641160141171),
mkLog (74734235056369739499044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9501572270334) (-9501572270053),
mkLog (1857522218023366963128986851340355520325741350923585910123/500000000000000000000000000000000000000000000000000000000000) 9 (-5595364639724) (-5595364639543),
mkLog (74734235068904498748044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9501572270166) (-9501572269885),
mkLog (14194995864705105405548480948326599/4000000000000000000000000000000000000) 9 (-5641160141589) (-5641160141408),
mkLog (1857522191807212641854874096901226043504143629923585910123/500000000000000000000000000000000000000000000000000000000000) 9 (-5595364653838) (-5595364653656),
mkLog (33523354101855040681105298476353226417985165617576414089877/250000000000000000000000000000000000000000000000000000000000) 3 (-2009218584580) (-2009218584519),
mkLog (1857522190967383772171874096901226043504143629923585910123/500000000000000000000000000000000000000000000000000000000000) 9 (-5595364654290) (-5595364654108),
mkLog (14194994512813010970362395910485009/4000000000000000000000000000000000000) 9 (-5641160236826) (-5641160236645),
mkLog (14194994512863150007358395910485009/4000000000000000000000000000000000000) 9 (-5641160236822) (-5641160236641),
mkLog (1857522220699538062790486851340355520325741350923585910123/500000000000000000000000000000000000000000000000000000000000) 9 (-5595364638283) (-5595364638102),
mkLog (74734235081439257997044318407130768184949401576414089877/1000000000000000000000000000000000000000000000000000000000000) 14 (-9501572269998) (-9501572269717),
mkLog (14194994513414679414314395910485009/4000000000000000000000000000000000000) 9 (-5641160236784) (-5641160236602),
mkLog (73998254568569974652436618306769/1000000000000000000000000000000000000) 14 (-9511469052091) (-9511469051810),
mkLog (44447629111/250000000000) 3 (-1727149295691) (-1727149295630),
mkLog (114132917045820045395263997260673/1000000000000000000000000000000000000) 14 (-9078146849892) (-9078146849610),
mkLog (136417171876206102599585824698797620581433767/1000000000000000000000000000000000000000000000000) 13 (-8899792927089) (-8899792926828),
mkLog (136417171880958707166585824698797620581433767/1000000000000000000000000000000000000000000000000) 13 (-8899792927055) (-8899792926794),
mkLog (114132917055325254529263997260673/1000000000000000000000000000000000000) 14 (-9078146849808) (-9078146849527),
mkLog (2831767637487381095588771953666548379418566233/500000000000000000000000000000000000000000000000) 8 (-5173706974948) (-5173706974787),
mkLog (2831767638254926733159271953666548379418566233/500000000000000000000000000000000000000000000000) 8 (-5173706974677) (-5173706974516),
mkLog (13641717042419230929999831629381041261473733/100000000000000000000000000000000000000000000000) 13 (-8899792937733) (-8899792937472),
mkLog (283176779955094677971420954329468258738526267/50000000000000000000000000000000000000000000000) 8 (-5173706917717) (-5173706917556),
mkLog (283176779946777619979170954329468258738526267/50000000000000000000000000000000000000000000000) 8 (-5173706917747) (-5173706917586),
mkLog (13641717041468710016599831629381041261473733/100000000000000000000000000000000000000000000000) 13 (-8899792937803) (-8899792937542),
mkLog (114132250063836695149604726831649/1000000000000000000000000000000000000) 14 (-9078152693814) (-9078152693533),
mkLog (114132250111362740819604726831649/1000000000000000000000000000000000000) 14 (-9078152693398) (-9078152693117),
mkLog (24202009453/1000000000000) 6 (-3721319614080) (-3721319613959),
mkLog (68124882931065846907143502949790205351977/15625000000000000000000000000000000000000000000) 18 (-12343040219229) (-12343040218868),
mkLog (1142296479449348622802404409013834794648023/7812500000000000000000000000000000000000000000) 13 (-8830439602407) (-8830439602146),
mkLog (53289975169313885990475025817169/250000000000000000000000000000000000) 13 (-8453467966621) (-8453467966360),
mkLog (53289975225723931847475025817169/250000000000000000000000000000000000) 13 (-8453467965562) (-8453467965301),
mkLog (68124882938883203594643502949790205351977/15625000000000000000000000000000000000000000000) 18 (-12343040219115) (-12343040218754),
mkLog (53289975171565284716475025817169/250000000000000000000000000000000000) 13 (-8453467966579) (-8453467966318),
mkLog (53289975175192538219475025817169/250000000000000000000000000000000000) 13 (-8453467966511) (-8453467966250),
mkLog (136249771055415766772879664094907662799073/31250000000000000000000000000000000000000000000) 18 (-12343040181113) (-12343040180752),
mkLog (2284593019758678063939268057685592337200927/15625000000000000000000000000000000000000000000) 13 (-8830439575768) (-8830439575507),
mkLog (136249772165480416397879664094907662799073/31250000000000000000000000000000000000000000000) 18 (-12343040172966) (-12343040172605),
mkLog (290626869/250000000000) 10 (-6757175989657) (-6757175989456),
mkLog (16678469/4000000000000) 18 (-12387686313118) (-12387686312757),
mkLog (16678469/1000000000000) 16 (-11001391951978) (-11001391951657),
mkLog (4554128373/200000000000) 6 (-3782283210300) (-3782283210179),
mkLog (7101681819/62500000000) 4 (-2174834924871) (-2174834924790),
mkLog (28986149829/100000000000) 2 (-1238352062209) (-1238352062168),
mkLog (44159664109/125000000000) 2 (-1040501941610) (-1040501941569),
mkLog (37995144889/200000000000) 3 (-1660858981094) (-1660858981033),
mkLog (7203509757/250000000000) 6 (-3546892544424) (-3546892544303),
mkLog (102542147/62500000000) 10 (-6412647931519) (-6412647931318),
mkLog (6615829/200000000000) 15 (-10316607534727) (-10316607534426),
mkLog (120899/1000000000000) 23 (-15928310350890) (-15928310350429),
mkLog (14203360211010353286735946766717523/500000000000000000000000000000000000) 6 (-3561129527291) (-3561129527170),
mkLog (14203367064989646713264053233282477/500000000000000000000000000000000000) 6 (-3561129044731) (-3561129044610),
mkLog (808361453556143887981891572117338921852738683/500000000000000000000000000000000000000000000000) 10 (-6427354075502) (-6427354075301),
mkLog (12530139239865946430390922058687346328147261317/250000000000000000000000000000000000000000000000) 5 (-2993324036548) (-2993324036447),
mkLog (808361453538637352862391572117338921852738683/500000000000000000000000000000000000000000000000) 10 (-6427354075524) (-6427354075323),
mkLog (183153493808548104898466563702384737/4000000000000000000000000000000000000) 5 (-3083725074896) (-3083725074795),
mkLog (183153493808247785533094563702384737/4000000000000000000000000000000000000) 5 (-3083725074898) (-3083725074797),
mkLog (808361466797179373878522573943854860787370997/500000000000000000000000000000000000000000000000) 10 (-6427354059122) (-6427354058921),
mkLog (183153493809098035933622563702384737/4000000000000000000000000000000000000) 5 (-3083725074893) (-3083725074792),
mkLog (183153493808209727159282563702384737/4000000000000000000000000000000000000) 5 (-3083725074898) (-3083725074797),
mkLog (12530138960156857811363772869655275639212629003/250000000000000000000000000000000000000000000000) 5 (-2993324058870) (-2993324058769),
mkLog (808361466799474211209522573943854860787370997/500000000000000000000000000000000000000000000000) 10 (-6427354059120) (-6427354058919),
mkLog (1153917599191897680012631811434569/500000000000000000000000000000000000) 9 (-6071445337490) (-6071445337309),
mkLog (1153917599168134657177631811434569/500000000000000000000000000000000000) 9 (-6071445337510) (-6071445337329),
mkLog (2700590419551963979845918445776262728555662083/1000000000000000000000000000000000000000000000000) 9 (-5914284856060) (-5914284855879),
mkLog (40305158083885268390311866365855504271444337917/500000000000000000000000000000000000000000000000) 4 (-2518128645545) (-2518128645464),
mkLog (2700590419561469188979918445776262728555662083/1000000000000000000000000000000000000000000000000) 9 (-5914284856057) (-5914284855876),
mkLog (1080236066814767663880838263887510617299220803/400000000000000000000000000000000000000000000000) 9 (-5914284949564) (-5914284949383),
mkLog (1080236066816668705707638263887510617299220803/400000000000000000000000000000000000000000000000) 9 (-5914284949562) (-5914284949381),
mkLog (2700590419566257051684918445776262728555662083/1000000000000000000000000000000000000000000000000) 9 (-5914284856055) (-5914284855874),
mkLog (40305158082584746648489366365855504271444337917/500000000000000000000000000000000000000000000000) 4 (-2518128645577) (-2518128645496),
mkLog (16122068224761011512523413860530712782700779197/200000000000000000000000000000000000000000000000) 4 (-2518128335956) (-2518128335875),
mkLog (16122068224687640957499213860530712782700779197/200000000000000000000000000000000000000000000000) 4 (-2518128335961) (-2518128335880),
mkLog (2307802774404175983204906131776211/1000000000000000000000000000000000000) 9 (-6071459387110) (-6071459386929),
mkLog (2307802774294125657265906131776211/1000000000000000000000000000000000000) 9 (-6071459387157) (-6071459386976),
mkLog (95818444298235543104786305737107/1000000000000000000000000000000000000) 14 (-9253055362451) (-9253055362170),
mkLog (1886194696210954444397936463316761/500000000000000000000000000000000000) 9 (-5580046687281) (-5580046687099),
mkLog (1886194696148280050837936463316761/500000000000000000000000000000000000) 9 (-5580046687314) (-5580046687132),
mkLog (100478490927360298435085944911222032517846695582326515901/1000000000000000000000000000000000000000000000000000000000000) 14 (-9205566874135) (-9205566873854),
mkLog (1860614136969849787174557623726833911185596223917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5593701484119) (-5593701483938),
mkLog (100478490902290779937085944911222032517846695582326515901/1000000000000000000000000000000000000000000000000000000000000) 14 (-9205566874385) (-9205566874104),
mkLog (1886194696129479106594436463316761/500000000000000000000000000000000000) 9 (-5580046687324) (-5580046687142),
mkLog (1860614204270189949735312890041048598688427011917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5593701447948) (-5593701447767),
mkLog (36079536081867543330240573185116557457608130068582326515901/250000000000000000000000000000000000000000000000000000000000) 3 (-1935735080823) (-1935735080762),
mkLog (1860614202509304160975812890041048598688427011917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5593701448895) (-5593701448713),
mkLog (943097529140227120993408772142009/250000000000000000000000000000000000) 9 (-5580046495323) (-5580046495141),
mkLog (943097528635771155131158772142009/250000000000000000000000000000000000) 9 (-5580046495858) (-5580046495676),
mkLog (100478490914825539186085944911222032517846695582326515901/1000000000000000000000000000000000000000000000000000000000000) 14 (-9205566874260) (-9205566873979),
mkLog (1860614135164761428533557623726833911185596223917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5593701485089) (-5593701484908),
mkLog (943097528642037937440658772142009/250000000000000000000000000000000000) 9 (-5580046495851) (-5580046495669),
mkLog (943097528519837773007908772142009/250000000000000000000000000000000000) 9 (-5580046495981) (-5580046495799),
mkLog (95816322731129833970063058274013/1000000000000000000000000000000000000) 14 (-9253077504228) (-9253077503947),
mkLog (43678326480116366256383133955993/250000000000000000000000000000000000) 13 (-8652364179457) (-8652364179196),
mkLog (92777240832628292413553513559796543917587879/500000000000000000000000000000000000000000000000) 13 (-8592162017470) (-8592162017209),
mkLog (92777240818321215643553513559796543917587879/500000000000000000000000000000000000000000000000) 13 (-8592162017625) (-8592162017364),
mkLog (43678326458932896719883133955993/250000000000000000000000000000000000) 13 (-8652364179942) (-8652364179681),
mkLog (1664421908121159957785982371175528456082412121/250000000000000000000000000000000000000000000000) 8 (-5011983057129) (-5011983056968),
mkLog (1664421908195948790200982371175528456082412121/250000000000000000000000000000000000000000000000) 8 (-5011983057084) (-5011983056923),
mkLog (18555447420114341258241866496257995444041843/100000000000000000000000000000000000000000000000) 13 (-8592162057696) (-8592162057435),
mkLog (332884354230178655127898995622006504555958157/50000000000000000000000000000000000000000000000) 8 (-5011983139422) (-5011983139261),
mkLog (18555447421058506528641866496257995444041843/100000000000000000000000000000000000000000000000) 13 (-8592162057646) (-8592162057385),
mkLog (92777240830267879237553513559796543917587879/500000000000000000000000000000000000000000000000) 13 (-8592162017496) (-8592162017235),
mkLog (332884354236662763899098995622006504555958157/50000000000000000000000000000000000000000000000) 8 (-5011983139403) (-5011983139242),
mkLog (18555447418678813657441866496257995444041843/100000000000000000000000000000000000000000000000) 13 (-8592162057774) (-8592162057513),
mkLog (87356789550472783543753341434719/500000000000000000000000000000000000) 13 (-8652362615865) (-8652362615604),
mkLog (87356789557481724214753341434719/500000000000000000000000000000000000) 13 (-8652362615785) (-8652362615524),
mkLog (3948303596983389457151681205416011778119419/500000000000000000000000000000000000000000000000) 17 (-11749077360029) (-11749077359688),
mkLog (61176793820651310892829478866230488221880581/250000000000000000000000000000000000000000000000) 12 (-8315448265293) (-8315448265052),
mkLog (70001832151998353254683201229881/250000000000000000000000000000000000) 12 (-8180694781659) (-8180694781418),
mkLog (70001832163080271307433201229881/250000000000000000000000000000000000) 12 (-8180694781500) (-8180694781259),
mkLog (3948303629429682097151681205416011778119419/500000000000000000000000000000000000000000000000) 17 (-11749077351811) (-11749077351470),
mkLog (70001832083737761752433201229881/250000000000000000000000000000000000) 12 (-8180694782634) (-8180694782393),
mkLog (70001832329031826548183201229881/250000000000000000000000000000000000) 12 (-8180694779130) (-8180694778889),
mkLog (3948303559783286558754177552748684111654041/500000000000000000000000000000000000000000000000) 17 (-11749077369451) (-11749077369110),
mkLog (61087858289421125821531857456080815888345959/250000000000000000000000000000000000000000000000) 12 (-8316903069203) (-8316903068962),
mkLog (3948303537962342732754177552748684111654041/500000000000000000000000000000000000000000000000) 17 (-11749077374978) (-11749077374637),
mkLog (6615829/800000000000) 17 (-11702901895867) (-11702901895526),
mkLog (4148489/1000000000000) 18 (-12392766386588) (-12392766386227),
mkLog (4148489/250000000000) 16 (-11006472025448) (-11006472025127),
mkLog (3967619974061433/1000000000000000000000) 18 (-12437344145976) (-12437344145615),
mkLog (84905210916902973/1000000000000000000000) 14 (-9373975089559) (-9373975089278),
mkLog (3080916924035397/40000000000000000000) 14 (-9471407477948) (-9471407477667),
mkLog (77022922887536109/1000000000000000000000) 14 (-9471407480718) (-9471407480437),
mkLog (1983810029256003/500000000000000000000) 18 (-12437344124691) (-12437344124330),
mkLog (15404584566839781/200000000000000000000) 14 (-9471407481410) (-9471407481129),
mkLog (77022923360163/1000000000000000000) 14 (-9471407474581) (-9471407474300),
mkLog (3967620259514247/1000000000000000000000) 18 (-12437344074030) (-12437344073669),
mkLog (84995616312166293/1000000000000000000000) 14 (-9372910875743) (-9372910875462),
mkLog (3967620296060109/1000000000000000000000) 18 (-12437344064819) (-12437344064458),
mkLog (493863/1000000000) 11 (-7613252407285) (-7613252407064),
mkLog (2775608785543492899/50000000000000000000000) 15 (-9798908179246) (-9798908178945),
mkLog (667140248330953201/12500000000000000000000) 15 (-9838238911249) (-9838238910948),
mkLog (2668560991893105127/50000000000000000000000) 15 (-9838238911785) (-9838238911484),
mkLog (5551217573471498593/100000000000000000000000) 15 (-9798908178817) (-9798908178515),
mkLog (103000178197510419483/100000000000000000000000) 10 (-6878194746770) (-6878194746569),
mkLog (103000178354888263953/100000000000000000000000) 10 (-6878194745242) (-6878194745041),
mkLog (5337122138779541929/100000000000000000000000) 15 (-9838238882744) (-9838238882443),
mkLog (51500092189322243341/50000000000000000000000) 10 (-6878194686759) (-6878194686558),
mkLog (51500092223659227589/50000000000000000000000) 10 (-6878194686093) (-6878194685892),
mkLog (5337122136871931693/100000000000000000000000) 15 (-9838238883101) (-9838238882800),
mkLog (1387802747696369179/25000000000000000000000) 15 (-9798909364627) (-9798909364326),
mkLog (5551210989354769039/100000000000000000000000) 15 (-9798909364884) (-9798909364583),
mkLog (476902559/100000000000) 8 (-5345613273857) (-5345613273696),
mkLog (79021666861823547/4000000000000000000000) 16 (-10832082840308) (-10832082839987),
mkLog (399181090968324530727/1000000000000000000000000) 12 (-7826095382084) (-7826095381843),
mkLog (99795272707610544747/250000000000000000000000) 12 (-7826095382429) (-7826095382188),
mkLog (4783526569672796313/250000000000000000000000) 16 (-10864038146443) (-10864038146122),
mkLog (405235834170892380969/1000000000000000000000000) 12 (-7811041353859) (-7811041353618),
mkLog (9567053126810833377/500000000000000000000000) 16 (-10864038147753) (-10864038147432),
mkLog (399181090817907419739/1000000000000000000000000) 12 (-7826095382461) (-7826095382220),
mkLog (405235815744796284939/1000000000000000000000000) 12 (-7811041399329) (-7811041399088),
mkLog (7604319951206489047041/1000000000000000000000000) 8 (-4879038778625) (-4879038778463),
mkLog (81047163484890804861/200000000000000000000000) 12 (-7811041395184) (-7811041394943),
mkLog (3193448311793145327/8000000000000000000000) 12 (-7826095512336) (-7826095512095),
mkLog (199590519906986017779/500000000000000000000000) 12 (-7826095510232) (-7826095509991),
mkLog (19134106266156426003/1000000000000000000000000) 16 (-10864038147098) (-10864038146777),
mkLog (202617914409275090823/500000000000000000000000) 12 (-7811041367067) (-7811041366826),
mkLog (399181039901715350301/1000000000000000000000000) 12 (-7826095510012) (-7826095509771),
mkLog (19755637916352353853/1000000000000000000000000) 16 (-10832071643397) (-10832071643076),
mkLog (12534759249/1000000000000) 7 (-4379249753930) (-4379249753789),
mkLog (45358453840213436021/1000000000000000000000000) 15 (-10000913985692) (-10000913985391),
mkLog (45358453792687390351/1000000000000000000000000) 15 (-10000913986740) (-10000913986439),
mkLog (2675003057554143537/62500000000000000000000) 15 (-10058971312518) (-10058971312217),
mkLog (1057192435551374288491/1000000000000000000000000) 10 (-6852138530534) (-6852138530333),
mkLog (21400024465185752863/500000000000000000000000) 15 (-10058971312296) (-10058971311995),
mkLog (4280005193401759207/100000000000000000000000) 15 (-10058971242117) (-10058971241816),
mkLog (42800051938770196637/1000000000000000000000000) 15 (-10058971242006) (-10058971241705),
mkLog (66074527232357215521/62500000000000000000000) 10 (-6852138530376) (-6852138530175),
mkLog (211438437609046729653/200000000000000000000000) 10 (-6852138764650) (-6852138764449),
mkLog (264298046627535593281/250000000000000000000000) 10 (-6852138766102) (-6852138765901),
mkLog (45359005047291116681/1000000000000000000000000) 15 (-10000901833520) (-10000901833219),
mkLog (45359005037785907547/1000000000000000000000000) 15 (-10000901833730) (-10000901833429),
mkLog (4752604567/1000000000000) 8 (-5349062481400) (-5349062481239),
mkLog (741809263806028107/250000000000000000000000) 19 (-12727879322761) (-12727879322380),
mkLog (2235980138522489631/31250000000000000000000) 14 (-9545094982645) (-9545094982364),
mkLog (74180925492551091/25000000000000000000000) 19 (-12727879334732) (-12727879334351),
mkLog (674490528459866421/7812500000000000000000) 14 (-9357277939932) (-9357277939651),
mkLog (21583696907088471969/250000000000000000000000) 14 (-9357277940100) (-9357277939819),
mkLog (741809233787378427/250000000000000000000000) 19 (-12727879363227) (-12727879362846),
mkLog (215836969612471191/2500000000000000000000) 14 (-9357277937591) (-9357277937310),
mkLog (21583696904837073243/250000000000000000000000) 14 (-9357277940204) (-9357277939923),
mkLog (4471960305437618751/62500000000000000000000) 14 (-9545094976296) (-9545094976015),
mkLog (9272615420778759/3125000000000000000000) 19 (-12727879363396) (-12727879363015),
mkLog (125077707/250000000000) 11 (-7600280996801) (-7600280996580),
mkLog (16485189/4000000000000) 18 (-12399342577840) (-12399342577479),
mkLog (16485189/1000000000000) 16 (-11013048216700) (-11013048216379),
mkLog (3928909296341408307/1000000000000000000000000) 18 (-12447148703521) (-12447148703160),
mkLog (21012468871766880309/250000000000000000000000) 14 (-9384100179667) (-9384100179386),
mkLog (19065300034467147501/250000000000000000000000) 14 (-9481346266351) (-9481346266070),
mkLog (15252240079109015643/200000000000000000000000) 14 (-9481346262972) (-9481346262691),
mkLog (3928909276783420587/1000000000000000000000000) 18 (-12447148708499) (-12447148708138),
mkLog (15252240026302448799/200000000000000000000000) 14 (-9481346266434) (-9481346266153),
mkLog (38130600293362204089/500000000000000000000000) 14 (-9481346260465) (-9481346260184),
mkLog (392890948752073827/100000000000000000000000) 18 (-12447148654862) (-12447148654501),
mkLog (8413937879330360259/100000000000000000000000) 14 (-9383035862983) (-9383035862702),
mkLog (1964454703666494309/500000000000000000000000) 18 (-12447148675272) (-12447148674911),
mkLog (488949693/1000000000000) 11 (-7623250951193) (-7623250950972),
mkLog (3457549857872122683/62500000000000000000000) 15 (-9802361631214) (-9802361630913),
mkLog (661990547382387003/12500000000000000000000) 15 (-9845987925467) (-9845987925166),
mkLog (1728774925542967401/31250000000000000000000) 15 (-9802361633177) (-9802361632876),
mkLog (254741825825462679/250000000000000000000) 10 (-6888965612402) (-6888965612201),
mkLog (3184272818835086253/3125000000000000000000) 10 (-6888965613653) (-6888965613452),
mkLog (3309952833098771937/62500000000000000000000) 15 (-9845987896407) (-9845987896106),
mkLog (63685460165459924187/62500000000000000000000) 10 (-6888965554161) (-6888965553960),
mkLog (3309952833688875231/62500000000000000000000) 15 (-9845987896229) (-9845987895928),
mkLog (413744092077110421/7812500000000000000000) 15 (-9845987925556) (-9845987925255),
mkLog (63685460130643829841/62500000000000000000000) 10 (-6888965554708) (-6888965554507),
mkLog (103436026043556987/1953125000000000000000) 15 (-9845987896318) (-9845987896017),
mkLog (345754593988130217/6250000000000000000000) 15 (-9802362764385) (-9802362764083),
mkLog (864386485412903013/15625000000000000000000) 15 (-9802362763873) (-9802362763571),
mkLog (295051647/62500000000) 8 (-5355771420213) (-5355771420052),
mkLog (22670450445759846183/1000000000000000000000000) 16 (-10694448224119) (-10694448223798),
mkLog (101952619705791877599/250000000000000000000000) 12 (-7804708004289) (-7804708004048),
mkLog (81562095767140215003/200000000000000000000000) 12 (-7804708004258) (-7804708004017),
mkLog (21903487610628860217/1000000000000000000000000) 16 (-10728864682355) (-10728864682034),
mkLog (1647446664565953153/4000000000000000000000) 12 (-7794823026909) (-7794823026668),
mkLog (407810478810633945777/1000000000000000000000000) 12 (-7804708004320) (-7804708004079),
mkLog (411861662644623759549/1000000000000000000000000) 12 (-7794823035399) (-7794823035158),
mkLog (468167446458984666699/62500000000000000000000) 8 (-4894095812301) (-4894095812139),
mkLog (51482707180399305333/125000000000000000000000) 12 (-7794823048028) (-7794823047787),
mkLog (203905212527087647443/500000000000000000000000) 12 (-7804708136137) (-7804708135896),
mkLog (203905211098261280877/500000000000000000000000) 12 (-7804708143144) (-7804708142903),
mkLog (411861667883653770291/1000000000000000000000000) 12 (-7794823022679) (-7794823022438),
mkLog (25488151388849355687/62500000000000000000000) 12 (-7804708143083) (-7804708142842),
mkLog (203905210822522859259/500000000000000000000000) 12 (-7804708144497) (-7804708144256),
mkLog (11335407116236456329/500000000000000000000000) 16 (-10694432177512) (-10694432177191),
mkLog (12533564619/1000000000000) 7 (-4379345063852) (-4379345063711),
mkLog (10685419333452467811/200000000000000000000000) 15 (-9837192512622) (-9837192512321),
mkLog (4767535026652270437/100000000000000000000000) 15 (-9951096059692) (-9951096059391),
mkLog (209637544637121950727/200000000000000000000000) 10 (-6860692584048) (-6860692583847),
mkLog (9535070701581151131/200000000000000000000000) 15 (-9951095991703) (-9951095991402),
mkLog (1907014010852422683/40000000000000000000000) 15 (-9951096059591) (-9951096059290),
mkLog (209637544083645022029/200000000000000000000000) 10 (-6860692586688) (-6860692586487),
mkLog (209637496969160859747/200000000000000000000000) 10 (-6860692811431) (-6860692811230),
mkLog (209637497202808559751/200000000000000000000000) 10 (-6860692810316) (-6860692810115),
mkLog (5342764109991838731/100000000000000000000000) 15 (-9837182322476) (-9837182322175),
mkLog (10685528199874654101/200000000000000000000000) 15 (-9837182324358) (-9837182324057),
mkLog (957572541/200000000000) 8 (-5341671166591) (-5341671166430),
mkLog (1842370482699296457/500000000000000000000000) 19 (-12511310329314) (-12511310328932),
mkLog (78818483755354397631/1000000000000000000000000) 14 (-9448363023325) (-9448363023044),
mkLog (3684740965907591463/1000000000000000000000000) 19 (-12511310329176) (-12511310328794),
mkLog (21038913409265975727/250000000000000000000000) 14 (-9382842454496) (-9382842454215),
mkLog (84155653576493075577/1000000000000000000000000) 14 (-9382842455216) (-9382842454935),
mkLog (3684740920097722053/1000000000000000000000000) 19 (-12511310341608) (-12511310341226),
mkLog (16831130714484217437/200000000000000000000000) 14 (-9382842455264) (-9382842454983),
mkLog (21038913393996019257/250000000000000000000000) 14 (-9382842455222) (-9382842454941),
mkLog (39409243553045922849/500000000000000000000000) 14 (-9448362980813) (-9448362980532),
mkLog (3684740925187707543/1000000000000000000000000) 19 (-12511310340227) (-12511310339845),
mkLog (508998549/1000000000000) 11 (-7583065392217) (-7583065391996),
mkLog (130691/31250000000) 18 (-12384694176054) (-12384694175693),
mkLog (130691/7812500000) 16 (-10998399814914) (-10998399814593),
mkLog (4554080441/200000000000) 6 (-3782293735311) (-3782293735190),
mkLog (14199184346385353286735946766717523/500000000000000000000000000000000000) 6 (-3561423575921) (-3561423575800),
mkLog (14199191200364646713264053233282477/500000000000000000000000000000000000) 6 (-3561423093219) (-3561423093098),
mkLog (113593502187/1000000000000) 4 (-2175128973430) (-2175128973349),
mkLog (805035464545832535310891572117338921852738683/500000000000000000000000000000000000000000000000) 10 (-6431477045721) (-6431477045520),
mkLog (12492546777818927913935172058687346328147261317/250000000000000000000000000000000000000000000000) 5 (-2996328709212) (-2996328709111),
mkLog (182471532043428397679282563702384737/4000000000000000000000000000000000000) 5 (-3087455468101) (-3087455468000),
mkLog (805035477869555755998022573943854860787370997/500000000000000000000000000000000000000000000000) 10 (-6431477029170) (-6431477028969),
mkLog (12492546497158584374935272869655275639212629003/250000000000000000000000000000000000000000000000) 5 (-2996328731678) (-2996328731577),
mkLog (288852188913/1000000000000) 2 (-1241840178778) (-1241840178737),
mkLog (1104524823938159792474631811434569/500000000000000000000000000000000000) 9 (-6115192879616) (-6115192879435),
mkLog (2610115020364574978883918445776262728555662083/1000000000000000000000000000000000000000000000000) 9 (-5948360989604) (-5948360989423),
mkLog (39252468004516776369248866365855504271444337917/500000000000000000000000000000000000000000000000) 4 (-2544593777115) (-2544593777034),
mkLog (1044045904637998324790838263887510617299220803/400000000000000000000000000000000000000000000000) 9 (-5948361088745) (-5948361088564),
mkLog (15700992290182803923123413860530712782700779197/200000000000000000000000000000000000000000000000) 4 (-2544593453035) (-2544593452954),
mkLog (2209016128256966479213906131776211/1000000000000000000000000000000000000) 9 (-6115208053504) (-6115208053323),
mkLog (429671057/1250000000) 2 (-1067878898100) (-1067878898059),
mkLog (53392577137019810171786305737107/1000000000000000000000000000000000000) 15 (-9837838826736) (-9837838826435),
mkLog (1482698911315208423836436463316761/500000000000000000000000000000000000) 9 (-5820744082730) (-5820744082549),
mkLog (59440897038040252966085944911222032517846695582326515901/1000000000000000000000000000000000000000000000000000000000000) 15 (-9730528066332) (-9730528066030),
mkLog (1452065386813659452565057623726833911185596223917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5841621150884) (-5841621150703),
mkLog (1452065465075479927491312890041048598688427011917673484099/500000000000000000000000000000000000000000000000000000000000) 9 (-5841621096987) (-5841621096806),
mkLog (32305786308229982401684323185116557457608130068582326515901/250000000000000000000000000000000000000000000000000000000000) 3 (-2046214561039) (-2046214560978),
mkLog (741349663133147505803158772142009/250000000000000000000000000000000000) 9 (-5820743802868) (-5820743802687),
mkLog (53389870582304567459063058274013/1000000000000000000000000000000000000) 15 (-9837889519613) (-9837889519312),
mkLog (164907400577/1000000000000) 3 (-1802371171273) (-1802371171212),
mkLog (15970083120910411029383133955993/250000000000000000000000000000000000) 14 (-9658499029956) (-9658499029675),
mkLog (39612009004094684253553513559796543917587879/500000000000000000000000000000000000000000000000) 14 (-9443231047579) (-9443231047298),
mkLog (1152179636801921230078482371175528456082412121/250000000000000000000000000000000000000000000000) 8 (-5379805433102) (-5379805432941),
mkLog (7922400748376764230041866496257995444041843/100000000000000000000000000000000000000000000000) 14 (-9443231180423) (-9443231180142),
mkLog (230435893908488472437298995622006504555958157/50000000000000000000000000000000000000000000000) 8 (-5379805578270) (-5379805578109),
mkLog (31940367077494982603753341434719/500000000000000000000000000000000000) 14 (-9658492742104) (-9658492741823),
mkLog (9662093543/500000000000) 6 (-3946397750862) (-3946397750741),
mkLog (38961781968803651681205416011778119419/500000000000000000000000000000000000000000000000) 34 (-23275292719564) (-23275292718883),
mkLog (18938022219658687333829478866230488221880581/250000000000000000000000000000000000000000000000) 14 (-9488044538141) (-9488044537860),
mkLog (31680801342309974503683201229881/250000000000000000000000000000000000) 13 (-8973505335453) (-8973505335192),
mkLog (38686265793923754177552748684111654041/500000000000000000000000000000000000000000000000) 34 (-23282389287709) (-23282389287028),
mkLog (18804109513053651924031857456080815888345959/250000000000000000000000000000000000000000000000) 14 (-9495140759917) (-9495140759636),
mkLog (657861659/1000000000000) 11 (-7326515893535) (-7326515893314)]
private def refs0 : List (Bool × Fin 471) :=
[(false,0),
(false,1),
(false,2),
(false,3),
(false,4),
(false,5),
(false,6),
(false,7),
(false,8),
(false,0),
(true,0),
(false,9),
(false,9),
(false,10),
(false,10),
(true,1),
(false,11),
(false,12),
(false,13),
(false,14),
(false,15),
(false,16),
(false,17),
(false,18),
(false,19),
(false,20),
(true,2),
(false,21),
(false,22),
(false,23),
(false,24),
(false,25),
(false,26),
(false,27),
(false,28),
(false,29),
(false,30),
(false,31),
(false,32),
(false,33),
(false,34),
(false,26),
(false,35),
(true,3),
(false,36),
(false,37),
(false,38),
(false,39),
(false,40),
(false,41),
(false,42),
(false,43),
(false,44),
(false,45),
(false,46),
(false,47),
(false,48),
(false,39),
(false,49),
(false,50),
(false,51),
(false,52),
(false,53),
(true,4),
(false,54),
(false,55),
(false,56),
(false,57),
(false,58),
(false,59),
(false,60),
(false,61),
(false,62),
(false,56),
(false,63),
(false,62),
(false,64),
(false,65),
(false,66),
(false,67),
(true,5),
(false,68),
(false,69),
(false,70),
(false,71),
(false,72),
(false,73),
(false,74),
(false,75),
(false,76),
(false,77),
(true,6),
(false,78),
(false,78),
(false,78),
(false,78),
(true,7),
(false,8),
(true,8),
(true,8),
(false,8),
(true,79),
(true,79),
(true,79),
(true,79),
(false,80),
(true,81),
(true,82),
(true,83),
(true,84),
(true,85),
(true,86),
(true,87),
(true,88),
(true,89),
(true,90),
(false,91),
(true,92),
(true,93),
(true,94),
(true,95),
(true,96),
(true,97),
(true,98),
(true,99),
(true,100),
(true,94),
(true,94),
(true,100),
(true,101),
(true,102),
(true,103),
(true,104),
(false,105),
(true,106),
(true,107),
(true,108),
(true,109),
(true,110),
(true,109),
(true,111),
(true,112),
(true,113),
(true,114),
(true,115),
(true,116),
(true,116),
(true,109),
(true,117),
(true,118),
(true,119),
(true,120),
(true,121),
(false,122),
(true,123),
(true,124),
(true,125),
(true,126),
(true,127),
(true,128),
(true,129),
(true,125),
(true,130),
(true,131),
(true,132),
(true,133),
(true,134),
(true,128),
(true,128),
(true,135),
(false,136),
(true,137),
(true,138),
(true,139),
(true,140),
(true,141),
(true,142),
(true,143),
(true,144),
(true,145),
(true,146),
(false,147),
(true,148),
(true,148),
(true,148),
(true,148),
(false,149),
(true,150),
(false,150),
(true,151),
(false,151),
(true,152),
(true,152),
(true,153),
(true,153),
(false,154),
(true,155),
(true,156),
(true,157),
(true,158),
(true,159),
(true,160),
(true,161),
(true,162),
(true,163),
(true,164),
(false,165),
(true,166),
(true,167),
(true,168),
(true,169),
(true,170),
(true,171),
(true,171),
(true,170),
(true,172),
(true,170),
(true,173),
(true,174),
(true,175),
(true,176),
(true,171),
(true,177),
(false,178),
(true,179),
(true,180),
(true,181),
(true,182),
(true,183),
(true,184),
(true,181),
(true,185),
(true,186),
(true,187),
(true,188),
(true,189),
(true,190),
(true,182),
(true,191),
(true,192),
(true,190),
(true,193),
(true,194),
(false,195),
(true,196),
(true,197),
(true,198),
(true,199),
(true,200),
(true,201),
(true,202),
(true,203),
(true,202),
(true,198),
(true,197),
(true,202),
(true,204),
(true,205),
(true,206),
(true,207),
(false,208),
(true,209),
(true,210),
(true,211),
(true,212),
(true,213),
(true,214),
(true,215),
(true,216),
(true,217),
(true,218),
(false,219),
(true,220),
(true,220),
(true,220),
(true,220),
(false,221)]
private def refs1 : List (Bool × Fin 471) :=
[(false,222),
(false,223),
(false,224),
(false,225),
(false,226),
(false,227),
(false,228),
(false,229),
(false,230),
(false,222),
(true,222),
(false,231),
(false,231),
(false,232),
(false,232),
(true,223),
(false,233),
(false,234),
(false,235),
(false,236),
(false,237),
(false,238),
(false,239),
(false,240),
(false,241),
(false,242),
(true,224),
(false,243),
(false,244),
(false,245),
(false,246),
(false,247),
(false,248),
(false,249),
(false,250),
(false,251),
(false,247),
(false,252),
(false,253),
(false,254),
(false,249),
(false,248),
(false,255),
(true,225),
(false,256),
(false,257),
(false,258),
(false,259),
(false,260),
(false,261),
(false,258),
(false,262),
(false,263),
(false,264),
(false,265),
(false,266),
(false,267),
(false,268),
(false,269),
(false,261),
(false,270),
(false,271),
(false,272),
(true,226),
(false,273),
(false,274),
(false,275),
(false,276),
(false,277),
(false,278),
(false,279),
(false,280),
(false,281),
(false,282),
(false,282),
(false,279),
(false,283),
(false,284),
(false,285),
(false,286),
(true,227),
(false,287),
(false,288),
(false,289),
(false,290),
(false,291),
(false,292),
(false,293),
(false,294),
(false,295),
(false,296),
(true,228),
(false,297),
(false,297),
(false,297),
(false,297),
(true,229),
(false,230),
(true,230),
(true,230),
(false,230),
(true,298),
(true,298),
(true,298),
(true,298),
(false,299),
(true,300),
(true,301),
(true,302),
(true,303),
(true,304),
(true,305),
(true,306),
(true,307),
(true,308),
(true,309),
(false,310),
(true,311),
(true,312),
(true,313),
(true,314),
(true,315),
(true,316),
(true,317),
(true,318),
(true,317),
(true,312),
(true,312),
(true,317),
(true,319),
(true,320),
(true,321),
(true,322),
(false,323),
(true,324),
(true,325),
(true,326),
(true,327),
(true,328),
(true,329),
(true,326),
(true,330),
(true,331),
(true,332),
(true,333),
(true,334),
(true,335),
(true,336),
(true,337),
(true,329),
(true,335),
(true,338),
(true,339),
(false,340),
(true,341),
(true,342),
(true,343),
(true,344),
(true,345),
(true,346),
(true,347),
(true,345),
(true,348),
(true,345),
(true,349),
(true,350),
(true,351),
(true,347),
(true,346),
(true,352),
(false,353),
(true,354),
(true,355),
(true,356),
(true,357),
(true,358),
(true,359),
(true,360),
(true,361),
(true,362),
(true,363),
(false,364),
(true,220),
(true,220),
(true,220),
(true,220),
(false,221),
(true,8),
(false,8),
(true,365),
(true,365),
(true,365),
(true,365),
(false,366),
(true,367),
(true,368),
(true,369),
(true,370),
(true,371),
(true,372),
(true,373),
(true,374),
(true,375),
(true,376),
(false,377),
(true,378),
(true,379),
(true,379),
(true,380),
(true,381),
(true,382),
(true,383),
(true,384),
(true,385),
(true,386),
(true,386),
(true,383),
(true,387),
(true,388),
(true,389),
(true,390),
(false,391),
(true,392),
(true,393),
(true,394),
(true,395),
(true,396),
(true,395),
(true,394),
(true,397),
(true,398),
(true,399),
(true,400),
(true,401),
(true,402),
(true,395),
(true,403),
(true,395),
(true,404),
(true,405),
(true,406),
(false,407),
(true,408),
(true,408),
(true,409),
(true,410),
(true,409),
(true,411),
(true,411),
(true,412),
(true,413),
(true,409),
(true,414),
(true,415),
(true,416),
(true,411),
(true,411),
(true,417),
(false,418),
(true,419),
(true,420),
(true,421),
(true,422),
(true,423),
(true,424),
(true,425),
(true,426),
(true,427),
(true,428),
(false,429),
(true,430),
(true,430),
(true,430),
(true,430),
(false,431),
(true,150),
(false,150),
(true,432),
(false,432),
(true,433),
(true,433),
(true,434),
(true,434),
(false,435),
(true,436),
(true,437),
(true,436),
(true,438),
(true,438),
(true,439),
(true,438),
(true,438),
(true,440),
(true,439),
(false,441),
(true,442),
(true,442),
(true,443),
(true,444),
(true,443),
(true,445),
(true,445),
(true,443),
(true,444),
(true,443),
(true,446),
(true,446),
(true,447),
(true,445),
(true,445),
(true,447),
(false,448),
(true,449),
(true,450),
(true,450),
(true,451),
(true,452),
(true,451),
(true,450),
(true,450),
(true,453),
(true,454),
(true,453),
(true,455),
(true,455),
(true,451),
(true,452),
(true,451),
(true,455),
(true,455),
(true,456),
(false,457),
(true,458),
(true,459),
(true,459),
(true,458),
(true,460),
(true,460),
(true,461),
(true,462),
(true,461),
(true,459),
(true,459),
(true,461),
(true,462),
(true,461),
(true,463),
(true,463),
(false,464),
(true,465),
(true,466),
(true,467),
(true,467),
(true,465),
(true,467),
(true,467),
(true,468),
(true,469),
(true,468),
(false,470)]
def entriesOwner4 (i : Fin 2) : List Entry :=
((![(refs0),(refs1)] i).map (fun p ↦
let e := logTable p.2
((if p.1 then e.1.1 else -e.1.1,e.1.2),e.2)))
end MME.ReleasedGlobalYZ
Source
Exact released global candidate from primitive seed f8187420c24231b83d9d1fb7b327fee76cd50ada0af0525e77b3d3b0d8f4d4e6.