Exact global Y/Z certificate: logs 2
Definitionmme_released_global_yz_logs_2matrix-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 463 → Entry :=
![mkLog (5768826387/250000000000) 6 (-3768992257225) (-3768992257104),
mkLog (14234476301/125000000000) 4 (-2172646806823) (-2172646806742),
mkLog (57919719391/200000000000) 2 (-1239259463272) (-1239259463231),
mkLog (176377980429/500000000000) 2 (-1041978790162) (-1041978790121),
mkLog (190081284693/1000000000000) 3 (-1660303484165) (-1660303484104),
mkLog (7230004871/250000000000) 6 (-3543221208032) (-3543221207911),
mkLog (1659786671/1000000000000) 10 (-6401066196419) (-6401066196218),
mkLog (33115773/1000000000000) 15 (-10315500863555) (-10315500863254),
mkLog (11961/100000000000) 23 (-15939029387117) (-15939029386656),
mkLog (444827403453199502842083377034737/15625000000000000000000000000000000) 6 (-3558941125144) (-3558941125023),
mkLog (444827365359300497157916622965263/15625000000000000000000000000000000) 6 (-3558941210781) (-3558941210660),
mkLog (346755837385061450130032451055492736127721473/200000000000000000000000000000000000000000000000) 10 (-6357451752014) (-6357451751813),
mkLog (4982969428587995144984474167653412763872278527/100000000000000000000000000000000000000000000000) 5 (-2999144201900) (-2999144201799),
mkLog (346755837383854663306832451055492736127721473/200000000000000000000000000000000000000000000000) 10 (-6357451752017) (-6357451751816),
mkLog (183004090892054797794886018444522307/4000000000000000000000000000000000000) 5 (-3084541132960) (-3084541132859),
mkLog (183004090893960907055866018444522307/4000000000000000000000000000000000000) 5 (-3084541132949) (-3084541132848),
mkLog (866889412119663961416196196108746072408306913/500000000000000000000000000000000000000000000000) 10 (-6357451961202) (-6357451961001),
mkLog (183004090893585025248790018444522307/4000000000000000000000000000000000000) 5 (-3084541132951) (-3084541132850),
mkLog (183004090893659066698150018444522307/4000000000000000000000000000000000000) 5 (-3084541132951) (-3084541132850),
mkLog (12457423938457420775791282645988413427591693087/250000000000000000000000000000000000000000000000) 5 (-2999144172441) (-2999144172340),
mkLog (866889411945753878775196196108746072408306913/500000000000000000000000000000000000000000000000) 10 (-6357451961403) (-6357451961202),
mkLog (578572996611063358878859552004817/250000000000000000000000000000000000) 9 (-6068651475702) (-6068651475521),
mkLog (578572996618187177456359552004817/250000000000000000000000000000000000) 9 (-6068651475690) (-6068651475509),
mkLog (342701792190648938211020058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5899208357889) (-5899208357708),
mkLog (5024466842987446856836299231266044319899494303/62500000000000000000000000000000000000000000000) 4 (-2520847209365) (-2520847209284),
mkLog (342701792204361623791145058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5899208357849) (-5899208357668),
mkLog (171350894206487449633371503980085657909258163/62500000000000000000000000000000000000000000000) 9 (-5899208368912) (-5899208368731),
mkLog (342701792190052734490145058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5899208357891) (-5899208357710),
mkLog (5024466842956926624000549231266044319899494303/62500000000000000000000000000000000000000000000) 4 (-2520847209371) (-2520847209290),
mkLog (2512233329352483314609464696862351435840741837/31250000000000000000000000000000000000000000000) 4 (-2520847246042) (-2520847245961),
mkLog (2512233329339968391992245946862351435840741837/31250000000000000000000000000000000000000000000) 4 (-2520847246047) (-2520847245966),
mkLog (2314295126118770495612694725559627/1000000000000000000000000000000000000) 9 (-6068650119057) (-6068650118876),
mkLog (171350894206785551493809003980085657909258163/62500000000000000000000000000000000000000000000) 9 (-5899208368910) (-5899208368729),
mkLog (2314295126274902400239694725559627/1000000000000000000000000000000000000) 9 (-6068650118989) (-6068650118808),
mkLog (9637957327417968935673901232103/100000000000000000000000000000000000) 14 (-9247216274438) (-9247216274157),
mkLog (393957564835590615761086532376409/100000000000000000000000000000000000) 8 (-5536682265017) (-5536682264856),
mkLog (393957564840555455413686532376409/100000000000000000000000000000000000) 8 (-5536682265004) (-5536682264843),
mkLog (48479186011051777175157190277372571900160943554906410697/500000000000000000000000000000000000000000000000000000000000) 14 (-9241228826127) (-9241228825846),
mkLog (1024863277054132908678539221382299066602521473945093589303/250000000000000000000000000000000000000000000000000000000000) 8 (-5496901702490) (-5496901702329),
mkLog (393957564831805058678886532376409/100000000000000000000000000000000000) 8 (-5536682265026) (-5536682264865),
mkLog (393957564840530684476586532376409/100000000000000000000000000000000000) 8 (-5536682265004) (-5536682264843),
mkLog (1024863304677959019341758234016584624197378114445093589303/250000000000000000000000000000000000000000000000000000000000) 8 (-5496901675536) (-5496901675375),
mkLog (17698284383678478894655815428732540737299939468054906410697/125000000000000000000000000000000000000000000000000000000000) 3 (-1954846029927) (-1954846029866),
mkLog (1024863304696019821954258234016584624197378114445093589303/250000000000000000000000000000000000000000000000000000000000) 8 (-5496901675518) (-5496901675357),
mkLog (7879150119059272228739459896751379/2000000000000000000000000000000000000) 8 (-5536682414481) (-5536682414320),
mkLog (7879150118887236806495459896751379/2000000000000000000000000000000000000) 8 (-5536682414503) (-5536682414342),
mkLog (48479185986103724226657190277372571900160943554906410697/500000000000000000000000000000000000000000000000000000000000) 14 (-9241228826641) (-9241228826360),
mkLog (1024863277403553810669039221382299066602521473945093589303/250000000000000000000000000000000000000000000000000000000000) 8 (-5496901702149) (-5496901701988),
mkLog (7879150119595000796943459896751379/2000000000000000000000000000000000000) 8 (-5536682414413) (-5536682414252),
mkLog (7879150119540592661205459896751379/2000000000000000000000000000000000000) 8 (-5536682414420) (-5536682414259),
mkLog (24095268726734852330929825962369/250000000000000000000000000000000000) 14 (-9247200694155) (-9247200693874),
mkLog (170654983596724460094158093337759/1000000000000000000000000000000000000) 13 (-8675866679555) (-8675866679294),
mkLog (378305129378163743704832512561192229854594089/2000000000000000000000000000000000000000000000000) 13 (-8572956648086) (-8572956647825),
mkLog (170654983903349744335158093337759/1000000000000000000000000000000000000) 13 (-8675866677758) (-8675866677497),
mkLog (6681044606534034733458027600339182270145405911/1000000000000000000000000000000000000000000000000) 8 (-5008480925517) (-5008480925356),
mkLog (6681044607836923121877027600339182270145405911/1000000000000000000000000000000000000000000000000) 8 (-5008480925322) (-5008480925161),
mkLog (47288142306985530181311604756687500495214039/250000000000000000000000000000000000000000000000) 13 (-8572956624090) (-8572956623829),
mkLog (835130568124011999372588744860242999504785961/125000000000000000000000000000000000000000000000) 8 (-5008480934728) (-5008480934567),
mkLog (378305129378033635300832512561192229854594089/2000000000000000000000000000000000000000000000000) 13 (-8572956648086) (-8572956647825),
mkLog (835130567249177247626338744860242999504785961/125000000000000000000000000000000000000000000000) 8 (-5008480935776) (-5008480935615),
mkLog (47288142303478571982561604756687500495214039/250000000000000000000000000000000000000000000000) 13 (-8572956624164) (-8572956623903),
mkLog (68262136758746265962311598730569/400000000000000000000000000000000000) 13 (-8675864579999) (-8675864579738),
mkLog (68262136637034086409911598730569/400000000000000000000000000000000000) 13 (-8675864581782) (-8675864581521),
mkLog (2063432135560673398510981515357741426832751/250000000000000000000000000000000000000000000000) 17 (-11704845515371) (-11704845515030),
mkLog (29356555468690208600974052898270758573167249/125000000000000000000000000000000000000000000000) 13 (-8356553140101) (-8356553139839),
mkLog (289266710788481410338817409209807/1000000000000000000000000000000000000) 12 (-8148161420859) (-8148161420618),
mkLog (289266710767349290455817409209807/1000000000000000000000000000000000000) 12 (-8148161420932) (-8148161420691),
mkLog (2063432134936021765510981515357741426832751/250000000000000000000000000000000000000000000000) 17 (-11704845515674) (-11704845515333),
mkLog (289266710776364300238817409209807/1000000000000000000000000000000000000) 12 (-8148161420901) (-8148161420660),
mkLog (289266711128850206762817409209807/1000000000000000000000000000000000000) 12 (-8148161419683) (-8148161419442),
mkLog (8253729227970498269887342102772828442113/1000000000000000000000000000000000000000000000) 17 (-11704845432290) (-11704845431949),
mkLog (117426234141119906320037701823099171557887/500000000000000000000000000000000000000000000) 13 (-8356553035641) (-8356553035379),
mkLog (8253729197236031829887342102772828442113/1000000000000000000000000000000000000000000000) 17 (-11704845436014) (-11704845435673),
mkLog (33115773/4000000000000) 17 (-11701795224695) (-11701795224354),
mkLog (16441713/4000000000000) 18 (-12401983337985) (-12401983337624),
mkLog (16441713/1000000000000) 16 (-11015688976845) (-11015688976524),
mkLog (97390340998167739/25000000000000000000000) 18 (-12455659345680) (-12455659345319),
mkLog (2215054984122959721/25000000000000000000000) 14 (-9331353877271) (-9331353876990),
mkLog (190316896130518267/2500000000000000000000) 14 (-9483110732806) (-9483110732525),
mkLog (1903168961790044203/25000000000000000000000) 14 (-9483110732551) (-9483110732270),
mkLog (3043448155804231/781250000000000000000) 18 (-12455659345807) (-12455659345446),
mkLog (951584480876373581/12500000000000000000000) 14 (-9483110732571) (-9483110732290),
mkLog (951584480354215007/12500000000000000000000) 14 (-9483110733119) (-9483110732838),
mkLog (48695167521536763/12500000000000000000000) 18 (-12455659406826) (-12455659406465),
mkLog (88602192940876047/1000000000000000000000) 14 (-9331353949775) (-9331353949494),
mkLog (48695164885879199/12500000000000000000000) 18 (-12455659460952) (-12455659460591),
mkLog (12432347/25000000000) 11 (-7606329398885) (-7606329398664),
mkLog (56502436585600769743/1000000000000000000000000) 15 (-9781226795484) (-9781226795183),
mkLog (52416449432183478919/1000000000000000000000000) 15 (-9856290095590) (-9856290095289),
mkLog (1412560922780835433/25000000000000000000000) 15 (-9781226789721) (-9781226789420),
mkLog (1018493137536653904279/1000000000000000000000000) 10 (-6889431060235) (-6889431060034),
mkLog (254623284696818010881/250000000000000000000000) 10 (-6889431059007) (-6889431058806),
mkLog (6552056063989662623/125000000000000000000000) 15 (-9856290113147) (-9856290112846),
mkLog (203698628991083018511/200000000000000000000000) 10 (-6889431052951) (-6889431052750),
mkLog (10483289888324421277/200000000000000000000000) 15 (-9856290095410) (-9856290095109),
mkLog (1018493145531171367981/1000000000000000000000000) 10 (-6889431052386) (-6889431052185),
mkLog (52416448478882104853/1000000000000000000000000) 15 (-9856290113777) (-9856290113476),
mkLog (56502350458125142493/1000000000000000000000000) 15 (-9781228319800) (-9781228319499),
mkLog (28251175240860855579/500000000000000000000000) 15 (-9781228319382) (-9781228319081),
mkLog (4719313733/1000000000000) 8 (-5356091885587) (-5356091885426),
mkLog (11197610409640282263/500000000000000000000000) 16 (-10706662978310) (-10706662977989),
mkLog (24448241836247554233/62500000000000000000000) 12 (-7846363531048) (-7846363530807),
mkLog (19558593470226867831/50000000000000000000000) 12 (-7846363530985) (-7846363530744),
mkLog (11148817096482972237/500000000000000000000000) 16 (-10711029975289) (-10711029974968),
mkLog (23749235569674090009/62500000000000000000000) 12 (-7875371492423) (-7875371492182),
mkLog (195585934696124556087/500000000000000000000000) 12 (-7846363531017) (-7846363530776),
mkLog (195585934708412800533/500000000000000000000000) 12 (-7846363530954) (-7846363530713),
mkLog (47498470174720991007/125000000000000000000000) 12 (-7875371512732) (-7875371512491),
mkLog (938117192171307139323/125000000000000000000000) 8 (-4892194136814) (-4892194136653),
mkLog (11874617548288339419/31250000000000000000000) 12 (-7875371512344) (-7875371512103),
mkLog (195585955758175536531/500000000000000000000000) 12 (-7846363423330) (-7846363423089),
mkLog (19558595571516668097/50000000000000000000000) 12 (-7846363423550) (-7846363423309),
mkLog (5574408545169425007/250000000000000000000000) 16 (-10711029975840) (-10711029975519),
mkLog (189993884403789664497/500000000000000000000000) 12 (-7875371493231) (-7875371492990),
mkLog (195585955954787447667/500000000000000000000000) 12 (-7846363422325) (-7846363422084),
mkLog (195585955696734314301/500000000000000000000000) 12 (-7846363423644) (-7846363423403),
mkLog (2799370792753291539/125000000000000000000000) 16 (-10706674341391) (-10706674341070),
mkLog (6144122223/500000000000) 7 (-4399112209779) (-4399112209638),
mkLog (13173394464749542563/250000000000000000000000) 15 (-9851016972252) (-9851016971951),
mkLog (52693577873184555261/1000000000000000000000000) 15 (-9851016971983) (-9851016971682),
mkLog (46568147830737114501/1000000000000000000000000) 15 (-9974593773638) (-9974593773337),
mkLog (64773055560399799887/62500000000000000000000) 10 (-6872032128193) (-6872032127992),
mkLog (46568148209040714741/1000000000000000000000000) 15 (-9974593765514) (-9974593765213),
mkLog (8290951104581236341/8000000000000000000000) 10 (-6872032129055) (-6872032128854),
mkLog (1036368917570877771339/1000000000000000000000000) 10 (-6872032100592) (-6872032100391),
mkLog (129546114624836696997/125000000000000000000000) 10 (-6872032101144) (-6872032100943),
mkLog (52693525676745312147/1000000000000000000000000) 15 (-9851017962549) (-9851017962248),
mkLog (1317338145583448931/25000000000000000000000) 15 (-9851017959767) (-9851017959466),
mkLog (4728795003/1000000000000) 8 (-5354084865252) (-5354084865091),
mkLog (173051805935600781/50000000000000000000000) 19 (-12573942557639) (-12573942557258),
mkLog (78145279028435264079/1000000000000000000000000) 14 (-9456940912168) (-9456940911887),
mkLog (108157378521190047/31250000000000000000000) 19 (-12573942559383) (-12573942559001),
mkLog (41586642568717439991/500000000000000000000000) 14 (-9394584353938) (-9394584353657),
mkLog (5198330320775412597/62500000000000000000000) 14 (-9394584353998) (-9394584353717),
mkLog (3461036641150144497/1000000000000000000000000) 19 (-12573942406691) (-12573942406310),
mkLog (83173285486900230867/1000000000000000000000000) 14 (-9394584349736) (-9394584349455),
mkLog (20793321284610133917/250000000000000000000000) 14 (-9394584353926) (-9394584353645),
mkLog (9768159730911582609/125000000000000000000000) 14 (-9456940927283) (-9456940927002),
mkLog (3461036356549585359/1000000000000000000000000) 19 (-12573942488921) (-12573942488539),
mkLog (502827843/1000000000000) 11 (-7595262706997) (-7595262706776),
mkLog (16609381/4000000000000) 18 (-12391837263042) (-12391837262681),
mkLog (16609381/1000000000000) 16 (-11005542901902) (-11005542901581),
mkLog (120093/1000000000000) 23 (-15934999394554) (-15934999394093),
mkLog (4615037091/200000000000) 6 (-3768997461633) (-3768997461512),
mkLog (444762523058668252842083377034737/15625000000000000000000000000000000) 6 (-3559086990992) (-3559086990871),
mkLog (444762484964769247157916622965263/15625000000000000000000000000000000) 6 (-3559087076642) (-3559087076521),
mkLog (113859201027/1000000000000) 4 (-2172792672677) (-2172792672596),
mkLog (346063630161319047006032451055492736127721473/200000000000000000000000000000000000000000000000) 10 (-6359449985281) (-6359449985080),
mkLog (4975154900685151618576574167653412763872278527/100000000000000000000000000000000000000000000000) 5 (-3000713680097) (-3000713679996),
mkLog (182671397751505058274958018444522307/4000000000000000000000000000000000000) 5 (-3086360742109) (-3086360742008),
mkLog (182671397753431280649658018444522307/4000000000000000000000000000000000000) 5 (-3086360742098) (-3086360741997),
mkLog (865158893799088889167696196108746072408306913/500000000000000000000000000000000000000000000000) 10 (-6359450195190) (-6359450194989),
mkLog (182671397751637424325322018444522307/4000000000000000000000000000000000000) 5 (-3086360742108) (-3086360742007),
mkLog (182671397753105304555478018444522307/4000000000000000000000000000000000000) 5 (-3086360742100) (-3086360741999),
mkLog (12437887618995597610573282645988413427591693087/250000000000000000000000000000000000000000000000) 5 (-3000713650568) (-3000713650467),
mkLog (865158893767479086095696196108746072408306913/500000000000000000000000000000000000000000000000) 10 (-6359450195226) (-6359450195025),
mkLog (36136971139/125000000000) 2 (-1240997264774) (-1240997264733),
mkLog (565399602146313816315859552004817/250000000000000000000000000000000000) 9 (-6091683455344) (-6091683455163),
mkLog (565399602149891038641109552004817/250000000000000000000000000000000000) 9 (-6091683455337) (-6091683455156),
mkLog (336880773711806798898395058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5916339935826) (-5916339935645),
mkLog (4959693787427047056949299231266044319899494303/62500000000000000000000000000000000000000000000) 4 (-2533822554358) (-2533822554277),
mkLog (336880773725519484478520058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5916339935785) (-5916339935604),
mkLog (168440384943422404962059003980085657909258163/62500000000000000000000000000000000000000000000) 9 (-5916339947180) (-5916339946999),
mkLog (336880773711210595177520058700400555100505697/125000000000000000000000000000000000000000000000) 9 (-5916339935828) (-5916339935647),
mkLog (4959693787452385715086486731266044319899494303/62500000000000000000000000000000000000000000000) 4 (-2533822554353) (-2533822554272),
mkLog (2479846800678393384255120946862351435840741837/31250000000000000000000000000000000000000000000) 4 (-2533822591874) (-2533822591793),
mkLog (2479846800683759217742995946862351435840741837/31250000000000000000000000000000000000000000000) 4 (-2533822591872) (-2533822591791),
mkLog (2261601600442025183465694725559627/1000000000000000000000000000000000000) 9 (-6091682044017) (-6091682043836),
mkLog (168440384943720506822496503980085657909258163/62500000000000000000000000000000000000000000000) 9 (-5916339947178) (-5916339946997),
mkLog (2261601600451564442999694725559627/1000000000000000000000000000000000000) 9 (-6091682044013) (-6091682043832),
mkLog (69605433171/200000000000) 2 (-1055474739473) (-1055474739432),
mkLog (7398435245489912483073901232103/100000000000000000000000000000000000) 14 (-9511656940573) (-9511656940292),
mkLog (354840377897594528988286532376409/100000000000000000000000000000000000) 9 (-5641257416429) (-5641257416248),
mkLog (354840377900101719751686532376409/100000000000000000000000000000000000) 9 (-5641257416422) (-5641257416241),
mkLog (37330368914568804938157190277372571900160943554906410697/500000000000000000000000000000000000000000000000000000000000) 14 (-9502556202145) (-9502556201864),
mkLog (929866334775436548642539221382299066602521473945093589303/250000000000000000000000000000000000000000000000000000000000) 9 (-5594175347166) (-5594175346984),
mkLog (354840377892580147461486532376409/100000000000000000000000000000000000) 9 (-5641257416443) (-5641257416262),
mkLog (354840377898848124369986532376409/100000000000000000000000000000000000) 9 (-5641257416426) (-5641257416245),
mkLog (929866364328517037327758234016584624197378114445093589303/250000000000000000000000000000000000000000000000000000000000) 9 (-5594175315384) (-5594175315202),
mkLog (16760167191507171755332815428732540737299939468054906410697/125000000000000000000000000000000000000000000000000000000000) 3 (-2009308666702) (-2009308666641),
mkLog (929866364309713106602258234016584624197378114445093589303/250000000000000000000000000000000000000000000000000000000000) 9 (-5594175315404) (-5594175315222),
mkLog (7096806296026570082615459896751379/2000000000000000000000000000000000000) 9 (-5641257594245) (-5641257594064),
mkLog (37330368895764874212657190277372571900160943554906410697/500000000000000000000000000000000000000000000000000000000000) 14 (-9502556202649) (-9502556202368),
mkLog (929866335201658978420539221382299066602521473945093589303/250000000000000000000000000000000000000000000000000000000000) 9 (-5594175346707) (-5594175346526),
mkLog (7096806295775851006275459896751379/2000000000000000000000000000000000000) 9 (-5641257594280) (-5641257594099),
mkLog (7096806296753655404001459896751379/2000000000000000000000000000000000000) 9 (-5641257594143) (-5641257593962),
mkLog (18496527141228269252929825962369/250000000000000000000000000000000000) 14 (-9511633204619) (-9511633204338),
mkLog (177793040247/1000000000000) 3 (-1727135100417) (-1727135100356),
mkLog (114152547011123690351158093337759/1000000000000000000000000000000000000) 14 (-9077974872535) (-9077974872254),
mkLog (273472230513796785866832512561192229854594089/2000000000000000000000000000000000000000000000000) 13 (-8897457655719) (-8897457655458),
mkLog (114152546992116327015158093337759/1000000000000000000000000000000000000) 14 (-9077974872701) (-9077974872420),
mkLog (5662551468997380829179027600339182270145405911/1000000000000000000000000000000000000000000000000) 8 (-5173880698848) (-5173880698687),
mkLog (5662551469049651078353027600339182270145405911/1000000000000000000000000000000000000000000000000) 8 (-5173880698838) (-5173880698677),
mkLog (34184030179006204935311604756687500495214039/250000000000000000000000000000000000000000000000) 13 (-8897457615794) (-8897457615533),
mkLog (707818925004585112803213744860242999504785961/125000000000000000000000000000000000000000000000) 8 (-5173880711026) (-5173880710865),
mkLog (273472230494789422530832512561192229854594089/2000000000000000000000000000000000000000000000000) 13 (-8897457655788) (-8897457655527),
mkLog (707818924057780826628713744860242999504785961/125000000000000000000000000000000000000000000000) 8 (-5173880712364) (-5173880712203),
mkLog (34184030183758045769311604756687500495214039/250000000000000000000000000000000000000000000000) 13 (-8897457615655) (-8897457615394),
mkLog (45661196575496208965111598730569/400000000000000000000000000000000000) 14 (-9077970979264) (-9077970978983),
mkLog (45661196444345401946711598730569/400000000000000000000000000000000000) 14 (-9077970982137) (-9077970981855),
mkLog (24200705751/1000000000000) 6 (-3721373483041) (-3721373482920),
mkLog (1089528725578996008510981515357741426832751/250000000000000000000000000000000000000000000000) 18 (-12343470956134) (-12343470955773),
mkLog (18281280548075409995974052898270758573167249/125000000000000000000000000000000000000000000000) 13 (-8830191400979) (-8830191400718),
mkLog (213139952336274103538817409209807/1000000000000000000000000000000000000) 13 (-8453561554929) (-8453561554668),
mkLog (213139952295747522335817409209807/1000000000000000000000000000000000000) 13 (-8453561555119) (-8453561554858),
mkLog (1089528725078667845510981515357741426832751/250000000000000000000000000000000000000000000000) 18 (-12343470956593) (-12343470956232),
mkLog (213139952306254413758817409209807/1000000000000000000000000000000000000) 13 (-8453561555070) (-8453561554809),
mkLog (213139952700513006202817409209807/1000000000000000000000000000000000000) 13 (-8453561553220) (-8453561552959),
mkLog (4358115826247557229887342102772828442113/1000000000000000000000000000000000000000000000) 18 (-12343470744132) (-12343470743771),
mkLog (73125137670681882820037701823099171557887/500000000000000000000000000000000000000000000) 13 (-8830191189309) (-8830191189048),
mkLog (4358116006365695909887342102772828442113/1000000000000000000000000000000000000000000000) 18 (-12343470702802) (-12343470702441),
mkLog (1162492791/1000000000000) 10 (-6757188621913) (-6757188621712),
mkLog (833703/200000000000) 18 (-12387950700867) (-12387950700506),
mkLog (833703/50000000000) 16 (-11001656339727) (-11001656339406),
mkLog (11384882851/500000000000) 6 (-3782321688787) (-3782321688666),
mkLog (113627062839/1000000000000) 4 (-2174833571891) (-2174833571810),
mkLog (144930580793/500000000000) 2 (-1238353223813) (-1238353223772),
mkLog (70655597787/200000000000) 2 (-1040500027923) (-1040500027882),
mkLog (47494215089/250000000000) 3 (-1660853001869) (-1660853001808),
mkLog (14406619101/500000000000) 6 (-3546920337721) (-3546920337599),
mkLog (820377379/500000000000) 10 (-6412598924822) (-6412598924621),
mkLog (33046859/1000000000000) 15 (-10317584034156) (-10317584033855),
mkLog (120763/1000000000000) 23 (-15929435889985) (-15929435889524),
mkLog (56813533631505465627585151212614061/2000000000000000000000000000000000000) 6 (-3561127894097) (-3561127893976),
mkLog (56813529207494534372414848787385939/2000000000000000000000000000000000000) 6 (-3561127971966) (-3561127971845),
mkLog (1617209104026460488308479423509234538430725189/1000000000000000000000000000000000000000000000000) 10 (-6427053390815) (-6427053390614),
mkLog (25058008427959567417465595920229445461569274811/500000000000000000000000000000000000000000000000) 5 (-2993414624312) (-2993414624211),
mkLog (1617209103846342349628479423509234538430725189/1000000000000000000000000000000000000000000000000) 10 (-6427053390927) (-6427053390726),
mkLog (18316029367022966832765938384378169/400000000000000000000000000000000000) 5 (-3083687949012) (-3083687948911),
mkLog (18316029366879719829583938384378169/400000000000000000000000000000000000) 5 (-3083687949019) (-3083687948918),
mkLog (50537787468802303363542422218458386717422259/31250000000000000000000000000000000000000000000) 10 (-6427053332087) (-6427053331886),
mkLog (18316029366867779826757938384378169/400000000000000000000000000000000000) 5 (-3083687949020) (-3083687948919),
mkLog (18316029366874217095546338384378169/400000000000000000000000000000000000) 5 (-3083687949020) (-3083687948919),
mkLog (783062725860645829371199225730618957032577741/15625000000000000000000000000000000000000000000) 5 (-2993414672217) (-2993414672116),
mkLog (50537787469167080565823672218458386717422259/31250000000000000000000000000000000000000000000) 10 (-6427053332080) (-6427053331879),
mkLog (230823038929620925841971964801789/100000000000000000000000000000000000) 9 (-6071274113357) (-6071274113176),
mkLog (230823038987311129366171964801789/100000000000000000000000000000000000) 9 (-6071274113107) (-6071274112926),
mkLog (539535895241556542654915360093993423766362863/200000000000000000000000000000000000000000000000) 9 (-5915363328861) (-5915363328680),
mkLog (8061590566484422931354828091791801426233637137/100000000000000000000000000000000000000000000000) 4 (-2518059308225) (-2518059308144),
mkLog (539535895238712858517315360093993423766362863/200000000000000000000000000000000000000000000000) 9 (-5915363328866) (-5915363328685),
mkLog (2697679787341431335428158037947871168938532401/1000000000000000000000000000000000000000000000000) 9 (-5915363213527) (-5915363213346),
mkLog (2697679787331927653760158037947871168938532401/1000000000000000000000000000000000000000000000000) 9 (-5915363213531) (-5915363213350),
mkLog (8061590567211217127347228091791801426233637137/100000000000000000000000000000000000000000000000) 4 (-2518059308134) (-2518059308053),
mkLog (40307942250687280227265550828688849581061467599/500000000000000000000000000000000000000000000000) 4 (-2518059570747) (-2518059570666),
mkLog (40307942244042826363142550828688849581061467599/500000000000000000000000000000000000000000000000) 4 (-2518059570912) (-2518059570831),
mkLog (14426596172702274667533925624067/6250000000000000000000000000000000) 9 (-6071263283329) (-6071263283148),
mkLog (14426596172731278013733925624067/6250000000000000000000000000000000) 9 (-6071263283327) (-6071263283146),
mkLog (47930188195151378529418626574571/500000000000000000000000000000000000) 14 (-9252617837923) (-9252617837642),
mkLog (3017587639288840117264096970779517/800000000000000000000000000000000000) 9 (-5580154010516) (-5580154010335),
mkLog (3017587636129952683069696970779517/800000000000000000000000000000000000) 9 (-5580154011563) (-5580154011381),
mkLog (50334715745899545145471625015246727659325156319533048633/500000000000000000000000000000000000000000000000000000000000) 14 (-9203668364626) (-9203668364345),
mkLog (929039301916952379268358246464541961569768285680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5595065153401) (-5595065153219),
mkLog (50334715714560443789971625015246727659325156319533048633/500000000000000000000000000000000000000000000000000000000000) 14 (-9203668365248) (-9203668364967),
mkLog (3017587636230240313605696970779517/800000000000000000000000000000000000) 9 (-5580154011530) (-5580154011348),
mkLog (3017587636220212177101696970779517/800000000000000000000000000000000000) 9 (-5580154011533) (-5580154011351),
mkLog (929039299651363943752915199334102486535106455680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5595065155839) (-5595065155658),
mkLog (18042744597828774498163670779492669449235800102319533048633/125000000000000000000000000000000000000000000000000000000000) 3 (-1935570094701) (-1935570094640),
mkLog (929039299688970630423415199334102486535106455680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5595065155799) (-5595065155617),
mkLog (3771984502090465694175024855915983/1000000000000000000000000000000000000) 9 (-5580154022982) (-5580154022800),
mkLog (3771984502040321095720024855915983/1000000000000000000000000000000000000) 9 (-5580154022995) (-5580154022814),
mkLog (929039301779038873980358246464541961569768285680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5595065153549) (-5595065153368),
mkLog (3771984502103001647992024855915983/1000000000000000000000000000000000000) 9 (-5580154022979) (-5580154022797),
mkLog (3771984502077929740358024855915983/1000000000000000000000000000000000000) 9 (-5580154022985) (-5580154022804),
mkLog (11982558222675624679031458354607/125000000000000000000000000000000000) 14 (-9252616905410) (-9252616905129),
mkLog (21835392531811649395154642687417/125000000000000000000000000000000000) 13 (-8652536852456) (-8652536852195),
mkLog (185550961657234216884167947146234960509710179/1000000000000000000000000000000000000000000000000) 13 (-8592180987863) (-8592180987602),
mkLog (185550961657184527785167947146234960509710179/1000000000000000000000000000000000000000000000000) 13 (-8592180987864) (-8592180987603),
mkLog (21835392529439256786404642687417/125000000000000000000000000000000000) 13 (-8652536852564) (-8652536852303),
mkLog (3328761977511088828714181076556360539490289821/500000000000000000000000000000000000000000000000) 8 (-5012007642163) (-5012007642002),
mkLog (3328761976934361663436181076556360539490289821/500000000000000000000000000000000000000000000000) 8 (-5012007642336) (-5012007642175),
mkLog (46387745255705827969741130354855522200529103/250000000000000000000000000000000000000000000000) 13 (-8592180883495) (-8592180883234),
mkLog (832190700843304701546457144871073477799470897/125000000000000000000000000000000000000000000000) 8 (-5012007394064) (-5012007393903),
mkLog (46387745253345857635741130354855522200529103/250000000000000000000000000000000000000000000000) 13 (-8592180883546) (-8592180883285),
mkLog (185550961661904468453167947146234960509710179/1000000000000000000000000000000000000000000000000) 13 (-8592180987838) (-8592180987577),
mkLog (46387745281963636237741130354855522200529103/250000000000000000000000000000000000000000000000) 13 (-8592180882929) (-8592180882668),
mkLog (832190700730678164004582144871073477799470897/125000000000000000000000000000000000000000000000) 8 (-5012007394199) (-5012007394038),
mkLog (46387745255718250244491130354855522200529103/250000000000000000000000000000000000000000000000) 13 (-8592180883495) (-8592180883234),
mkLog (174682514605827910272478609288041/1000000000000000000000000000000000000) 13 (-8652540434082) (-8652540433821),
mkLog (174682514600958902307478609288041/1000000000000000000000000000000000000) 13 (-8652540434110) (-8652540433849),
mkLog (197384207893701443933420025020538315171413/25000000000000000000000000000000000000000000000) 17 (-11749234259743) (-11749234259402),
mkLog (3054573257649226994585525666750461684828587/12500000000000000000000000000000000000000000000) 12 (-8316844027076) (-8316844026835),
mkLog (28011034159144406102370323666881/100000000000000000000000000000000000) 12 (-8180326955432) (-8180326955191),
mkLog (28011034157735233017470323666881/100000000000000000000000000000000000) 12 (-8180326955482) (-8180326955241),
mkLog (197384210769382131783420025020538315171413/25000000000000000000000000000000000000000000000) 17 (-11749234245174) (-11749234244833),
mkLog (28011034168173560517870323666881/100000000000000000000000000000000000) 12 (-8180326955110) (-8180326954869),
mkLog (28011034151395824659370323666881/100000000000000000000000000000000000) 12 (-8180326955708) (-8180326955467),
mkLog (197384210909153970402945638331416632375267/25000000000000000000000000000000000000000000000) 17 (-11749234244466) (-11749234244125),
mkLog (3054575717596714935205446836457083367624733/12500000000000000000000000000000000000000000000) 12 (-8316843221743) (-8316843221502),
mkLog (197384210823622520027945638331416632375267/25000000000000000000000000000000000000000000000) 17 (-11749234244899) (-11749234244558),
mkLog (33046859/4000000000000) 17 (-11703878395296) (-11703878394955),
mkLog (16550261/4000000000000) 18 (-12395403047174) (-12395403046813),
mkLog (16550261/1000000000000) 16 (-11009108686034) (-11009108685713),
mkLog (3967984447691758413/1000000000000000000000000) 18 (-12437252288163) (-12437252287802),
mkLog (16999242606797395023/200000000000000000000000) 14 (-9372903855149) (-9372903854868),
mkLog (15401942957546544753/200000000000000000000000) 14 (-9471578978136) (-9471578977855),
mkLog (38504857210381333113/500000000000000000000000) 14 (-9471578982901) (-9471578982620),
mkLog (3967984510911364557/1000000000000000000000000) 18 (-12437252272231) (-12437252271870),
mkLog (7700971486922674731/100000000000000000000000) 14 (-9471578977077) (-9471578976796),
mkLog (15401942877534230727/200000000000000000000000) 14 (-9471578983331) (-9471578983050),
mkLog (3967984514862589941/1000000000000000000000000) 18 (-12437252271235) (-12437252270874),
mkLog (84996163512291431097/1000000000000000000000000) 14 (-9372904437783) (-9372904437502),
mkLog (493903173/1000000000000) 11 (-7613171066172) (-7613171065951),
mkLog (5552478845011323981/100000000000000000000000) 15 (-9798680998336) (-9798680998035),
mkLog (53377254772862744493/1000000000000000000000000) 15 (-9838125843471) (-9838125843170),
mkLog (26688627384046557363/500000000000000000000000) 15 (-9838125843560) (-9838125843259),
mkLog (13881197110143495069/250000000000000000000000) 15 (-9798680998508) (-9798680998207),
mkLog (257532042358461984183/250000000000000000000000) 10 (-6878072048240) (-6878072048039),
mkLog (6438301057888382907/6250000000000000000000) 10 (-6878072048406) (-6878072048205),
mkLog (10675450149459044229/200000000000000000000000) 15 (-9838125918888) (-9838125918587),
mkLog (16095749756710133349/15625000000000000000000) 10 (-6878072227833) (-6878072227632),
mkLog (53377250861766335553/1000000000000000000000000) 15 (-9838125916744) (-9838125916443),
mkLog (1030127984024030004141/1000000000000000000000000) 10 (-6878072228227) (-6878072228026),
mkLog (1668039086002026591/31250000000000000000000) 15 (-9838125918799) (-9838125918498),
mkLog (5552493039429510573/100000000000000000000000) 15 (-9798678441928) (-9798678441627),
mkLog (55524930379986216429/1000000000000000000000000) 15 (-9798678442186) (-9798678441885),
mkLog (4769629767/1000000000000) 8 (-5345486594156) (-5345486593995),
mkLog (19748595364042316591/1000000000000000000000000) 16 (-10832428190116) (-10832428189795),
mkLog (399215269744330151097/1000000000000000000000000) 12 (-7826009763517) (-7826009763276),
mkLog (199607634627713976117/500000000000000000000000) 12 (-7826009764742) (-7826009764501),
mkLog (19103418059431614407/1000000000000000000000000) 16 (-10865643283093) (-10865643282772),
mkLog (50712097771518499387/125000000000000000000000) 12 (-7809904519450) (-7809904519209),
mkLog (4775854505455938239/250000000000000000000000) 16 (-10865643285061) (-10865643284740),
mkLog (99803817345196872601/250000000000000000000000) 12 (-7826009764428) (-7826009764187),
mkLog (198094132556585543/488281250000000000000) 12 (-7809904516236) (-7809904515995),
mkLog (3801766877245381420273/500000000000000000000000) 8 (-4879142172139) (-4879142171977),
mkLog (202848391775551457483/500000000000000000000000) 12 (-7809904516051) (-7809904515810),
mkLog (399215280675681879521/1000000000000000000000000) 12 (-7826009736135) (-7826009735894),
mkLog (99803820153250527609/250000000000000000000000) 12 (-7826009736292) (-7826009736051),
mkLog (25356048779203642249/62500000000000000000000) 12 (-7809904523652) (-7809904523411),
mkLog (199607640344108916669/500000000000000000000000) 12 (-7826009736104) (-7826009735863),
mkLog (49901910082893240713/125000000000000000000000) 12 (-7826009736166) (-7826009735925),
mkLog (9874232438649517719/500000000000000000000000) 16 (-10832434797531) (-10832434797210),
mkLog (12535953817/1000000000000) 7 (-4379154458036) (-4379154457895),
mkLog (22673835713290533681/500000000000000000000000) 15 (-10001151729585) (-10001151729284),
mkLog (11336917938614521227/250000000000000000000000) 15 (-10001151722355) (-10001151722054),
mkLog (1339210168932181091/31250000000000000000000) 15 (-10057694641303) (-10057694641002),
mkLog (105690319386244318791/100000000000000000000000) 10 (-6852412162139) (-6852412161938),
mkLog (5356840673352803947/125000000000000000000000) 15 (-10057694641746) (-10057694641445),
mkLog (4285472130499115517/100000000000000000000000) 15 (-10057694736995) (-10057694736694),
mkLog (21427360647743736751/500000000000000000000000) 15 (-10057694737216) (-10057694736915),
mkLog (528451600718438738653/500000000000000000000000) 10 (-6852412154973) (-6852412154772),
mkLog (528451699186084500801/500000000000000000000000) 10 (-6852411968640) (-6852411968439),
mkLog (264225849579974688107/250000000000000000000000) 10 (-6852411968690) (-6852411968489),
mkLog (5668407001987939781/125000000000000000000000) 15 (-10001160890201) (-10001160889900),
mkLog (2834203502181930099/62500000000000000000000) 15 (-10001160889782) (-10001160889481),
mkLog (2375920417/500000000000) 8 (-5349223192092) (-5349223191931),
mkLog (741522480772166957/250000000000000000000000) 19 (-12728265996933) (-12728265996552),
mkLog (71565830492013027747/1000000000000000000000000) 14 (-9544892825814) (-9544892825533),
mkLog (741522435742632287/250000000000000000000000) 19 (-12728266057659) (-12728266057278),
mkLog (86333036950553164511/1000000000000000000000000) 14 (-9357298218085) (-9357298217804),
mkLog (86333036556294572067/1000000000000000000000000) 14 (-9357298222652) (-9357298222371),
mkLog (741522334676343361/250000000000000000000000) 19 (-12728266193955) (-12728266193574),
mkLog (21583259136446920161/250000000000000000000000) 14 (-9357298222774) (-9357298222493),
mkLog (86333036586314261847/1000000000000000000000000) 14 (-9357298222304) (-9357298222023),
mkLog (17891456880891509167/250000000000000000000000) 14 (-9544892867292) (-9544892867011),
mkLog (185380583794167881/62500000000000000000000) 19 (-12728266193280) (-12728266192899),
mkLog (500328163/1000000000000) 11 (-7600246348941) (-7600246348720),
mkLog (8248299/2000000000000) 18 (-12398650741436) (-12398650741075),
mkLog (8248299/500000000000) 16 (-11012356380296) (-11012356379975),
mkLog (392733463443598441/100000000000000000000000) 18 (-12447549572420) (-12447549572059),
mkLog (16819798286822359507/200000000000000000000000) 14 (-9383515983659) (-9383515983378),
mkLog (15242193584992633253/200000000000000000000000) 14 (-9482005169748) (-9482005169467),
mkLog (15242193655568298591/200000000000000000000000) 14 (-9482005165117) (-9482005164836),
mkLog (196366734312180289/50000000000000000000000) 18 (-12447549559229) (-12447549558868),
mkLog (121937548694017099/1600000000000000000000) 14 (-9482005169632) (-9482005169351),
mkLog (15242193649507784393/200000000000000000000000) 14 (-9482005165515) (-9482005165234),
mkLog (785466937541971843/200000000000000000000000) 18 (-12447549558855) (-12447549558494),
mkLog (420494712445529419/5000000000000000000000) 14 (-9383516565652) (-9383516565371),
mkLog (9818336710721503/2500000000000000000000) 18 (-12447549559727) (-12447549559366),
mkLog (97750229/200000000000) 11 (-7623657104068) (-7623657103847),
mkLog (13828954353150811887/250000000000000000000000) 15 (-9802451661325) (-9802451661024),
mkLog (13237159644384422139/250000000000000000000000) 15 (-9846188197871) (-9846188197570),
mkLog (6618579822782203653/125000000000000000000000) 15 (-9846188197782) (-9846188197481),
mkLog (13828954350790841553/250000000000000000000000) 15 (-9802451661496) (-9802451661194),
mkLog (63673256110265183781/62500000000000000000000) 10 (-6889157202689) (-6889157202488),
mkLog (63673256048905955097/62500000000000000000000) 10 (-6889157203652) (-6889157203451),
mkLog (1323715864493698569/25000000000000000000000) 15 (-9846188273374) (-9846188273073),
mkLog (254692978064103716523/250000000000000000000000) 10 (-6889157384778) (-6889157384577),
mkLog (3309289660644253839/62500000000000000000000) 15 (-9846188273553) (-9846188273252),
mkLog (13237159646744392473/250000000000000000000000) 15 (-9846188197693) (-9846188197392),
mkLog (63673244485051318497/62500000000000000000000) 10 (-6889157385265) (-6889157385064),
mkLog (13237158643757000523/250000000000000000000000) 15 (-9846188273463) (-9846188273162),
mkLog (13828990248299592027/250000000000000000000000) 15 (-9802449065677) (-9802449065375),
mkLog (13828990250659562361/250000000000000000000000) 15 (-9802449065506) (-9802449065205),
mkLog (1179985167/250000000000) 8 (-5355959049884) (-5355959049723),
mkLog (566611873404156777/25000000000000000000000) 16 (-10694711840285) (-10694711839964),
mkLog (40786611658459639689/100000000000000000000000) 12 (-7804571583159) (-7804571582918),
mkLog (40786611312488930301/100000000000000000000000) 12 (-7804571591641) (-7804571591400),
mkLog (2187457307679792747/100000000000000000000000) 16 (-10730185642562) (-10730185642241),
mkLog (8245856462358795303/20000000000000000000000) 12 (-7793776725466) (-7793776725225),
mkLog (2187457305172758621/100000000000000000000000) 16 (-10730185643708) (-10730185643387),
mkLog (20393305655617706619/50000000000000000000000) 12 (-7804571591672) (-7804571591431),
mkLog (515366030072596953/1250000000000000000000) 12 (-7793776723186) (-7793776722945),
mkLog (749024318391905973009/100000000000000000000000) 8 (-4894154014248) (-4894154014086),
mkLog (20614641206664429309/50000000000000000000000) 12 (-7793776723003) (-7793776722762),
mkLog (40786611691051083327/100000000000000000000000) 12 (-7804571582360) (-7804571582119),
mkLog (4078661169230460039/10000000000000000000000) 12 (-7804571582329) (-7804571582088),
mkLog (41229282427117546311/100000000000000000000000) 12 (-7793776722669) (-7793776722428),
mkLog (2266445968086361437/100000000000000000000000) 16 (-10694712513379) (-10694712513058),
mkLog (1253517063/100000000000) 7 (-4379216935250) (-4379216935109),
mkLog (3339483895043748501/62500000000000000000000) 15 (-9837105563269) (-9837105562968),
mkLog (3339483910607812107/62500000000000000000000) 15 (-9837105558608) (-9837105558307),
mkLog (5965342043761358517/125000000000000000000000) 15 (-9950102620743) (-9950102620442),
mkLog (5241792817494409281/5000000000000000000000) 10 (-6860529610958) (-6860529610757),
mkLog (1491335511089994087/31250000000000000000000) 15 (-9950102620642) (-9950102620341),
mkLog (2982670772556352647/62500000000000000000000) 15 (-9950102704333) (-9950102704032),
mkLog (131044820399048690841/125000000000000000000000) 10 (-6860529611250) (-6860529611049),
mkLog (131044845600859375941/125000000000000000000000) 10 (-6860529418936) (-6860529418735),
mkLog (131044843946279691057/125000000000000000000000) 10 (-6860529431562) (-6860529431361),
mkLog (3339457662413158419/62500000000000000000000) 15 (-9837113418595) (-9837113418294),
mkLog (1335783064606092669/25000000000000000000000) 15 (-9837113418864) (-9837113418563),
mkLog (598617831/125000000000) 8 (-5341445633552) (-5341445633391),
mkLog (460521323262309483/125000000000000000000000) 19 (-12511465136248) (-12511465135866),
mkLog (78828937739562174213/1000000000000000000000000) 14 (-9448230398457) (-9448230398176),
mkLog (42079349834388934749/500000000000000000000000) 14 (-9382806259939) (-9382806259658),
mkLog (84158699704918953987/1000000000000000000000000) 14 (-9382806259510) (-9382806259229),
mkLog (1842085214149687287/500000000000000000000000) 19 (-12511465179079) (-12511465178698),
mkLog (16831739937115167669/200000000000000000000000) 14 (-9382806259740) (-9382806259459),
mkLog (84158699661142429113/1000000000000000000000000) 14 (-9382806260030) (-9382806259749),
mkLog (78828940501555476147/1000000000000000000000000) 14 (-9448230363419) (-9448230363138),
mkLog (736834087594186479/200000000000000000000000) 19 (-12511465176454) (-12511465176073),
mkLog (509029359/1000000000000) 11 (-7583004863424) (-7583004863203),
mkLog (4183411/1000000000000) 18 (-12384383615671) (-12384383615310),
mkLog (4183411/250000000000) 16 (-10998089254531) (-10998089254210),
mkLog (22769525999/1000000000000) 6 (-3782332216092) (-3782332215971),
mkLog (56796829779505465627585151212614061/2000000000000000000000000000000000000) 6 (-3561421949175) (-3561421949053),
mkLog (56796825355494534372414848787385939/2000000000000000000000000000000000000) 6 (-3561422027066) (-3561422026945),
mkLog (22718731027/200000000000) 4 (-2175127626980) (-2175127626899),
mkLog (1610558843517273344616479423509234538430725189/1000000000000000000000000000000000000000000000000) 10 (-6431174052540) (-6431174052339),
mkLog (24982811043843779816485595920229445461569274811/500000000000000000000000000000000000000000000000) 5 (-2996420068328) (-2996420068227),
mkLog (18247832672375234419162338384378169/400000000000000000000000000000000000) 5 (-3087418231861) (-3087418231760),
mkLog (50329966851083404987979922218458386717422259/31250000000000000000000000000000000000000000000) 10 (-6431173993109) (-6431173992908),
mkLog (780712807610253305733464850730618957032577741/15625000000000000000000000000000000000000000000) 5 (-2996420116373) (-2996420116272),
mkLog (9026618877/31250000000) 2 (-1241841511117) (-1241841511076),
mkLog (220945097554892821504171964801789/100000000000000000000000000000000000) 9 (-6115011221760) (-6115011221579),
mkLog (521420402890372410045315360093993423766362863/200000000000000000000000000000000000000000000000) 9 (-5949516013912) (-5949516013731),
mkLog (7851064390748290426943828091791801426233637137/100000000000000000000000000000000000000000000000) 4 (-2544521072248) (-2544521072167),
mkLog (2607102333675538537906158037947871168938532401/1000000000000000000000000000000000000000000000000) 9 (-5949515891468) (-5949515891287),
mkLog (39255311169097758222700550828688849581061467599/500000000000000000000000000000000000000000000000) 4 (-2544521346979) (-2544521346898),
mkLog (13809230056361561836583925624067/6250000000000000000000000000000000) 9 (-6114999529571) (-6114999529390),
mkLog (343737205453/1000000000000) 2 (-1067877851215) (-1067877851174),
mkLog (26723653045047084693918626574571/500000000000000000000000000000000000) 15 (-9836814322474) (-9836814322173),
mkLog (2371922530225698878874496970779517/800000000000000000000000000000000000) 9 (-5820910907264) (-5820910907083),
mkLog (29845720177784774206971625015246727659325156319533048633/500000000000000000000000000000000000000000000000000000000000) 15 (-9726321925625) (-9726321925323),
mkLog (724541900594430439206858246464541961569768285680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5843676603038) (-5843676602857),
mkLog (724541897767872755136915199334102486535106455680466951367/250000000000000000000000000000000000000000000000000000000000) 9 (-5843676606939) (-5843676606758),
mkLog (16156022480527546676834170779492669449235800102319533048633/125000000000000000000000000000000000000000000000000000000000) 3 (-2046020848167) (-2046020848106),
mkLog (2964903104504272981384024855915983/1000000000000000000000000000000000000) 9 (-5820910926920) (-5820910926739),
mkLog (6680942652905293453031458354607/125000000000000000000000000000000000) 15 (-9836809923139) (-9836809922838),
mkLog (164905735909/1000000000000) 3 (-1802381265886) (-1802381265825),
mkLog (7980316798972088475404642687417/125000000000000000000000000000000000) 14 (-9659090906633) (-9659090906352),
mkLog (79225068306833783835167947146234960509710179/1000000000000000000000000000000000000000000000000) 14 (-9443217790341) (-9443217790060),
mkLog (2304311843912043390100181076556360539490289821/500000000000000000000000000000000000000000000000) 8 (-5379826015908) (-5379826015747),
mkLog (19806273923945036993491130354855522200529103/250000000000000000000000000000000000000000000000) 14 (-9443217444631) (-9443217444350),
mkLog (576078213757571776492957144871073477799470897/125000000000000000000000000000000000000000000000) 8 (-5379825577114) (-5379825576953),
mkLog (63841623218334436434478609288041/1000000000000000000000000000000000000) 14 (-9659105178935) (-9659105178654),
mkLog (19323667767/1000000000000) 6 (-3946424625264) (-3946424625143),
mkLog (1230840507873358420025020538315171413/25000000000000000000000000000000000000000000000) 35 (-23734444386419) (-23734444385718),
mkLog (940883201797992336460525666750461684828587/12500000000000000000000000000000000000000000000) 14 (-9494420191894) (-9494420191613),
mkLog (12688965887874817099370323666881/100000000000000000000000000000000000) 13 (-8972192677013) (-8972192676752),
mkLog (1230844842741502945638331416632375267/25000000000000000000000000000000000000000000000) 35 (-23734440864548) (-23734440863847),
mkLog (940886892579248498992946836457083367624733/12500000000000000000000000000000000000000000000) 14 (-9494416269225) (-9494416268944),
mkLog (16452511/25000000000) 11 (-7326152994022) (-7326152993801)]
private def refs0 : List (Bool × Fin 463) :=
[(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,26),
(false,27),
(false,28),
(false,27),
(false,29),
(false,30),
(false,31),
(false,26),
(false,32),
(false,33),
(true,3),
(false,34),
(false,35),
(false,36),
(false,37),
(false,38),
(false,37),
(false,39),
(false,40),
(false,41),
(false,42),
(false,43),
(false,44),
(false,45),
(false,46),
(false,47),
(false,37),
(false,48),
(false,49),
(false,50),
(true,4),
(false,51),
(false,52),
(false,52),
(false,53),
(false,54),
(false,55),
(false,56),
(false,57),
(false,56),
(false,58),
(false,52),
(false,56),
(false,59),
(false,60),
(false,61),
(false,62),
(true,5),
(false,63),
(false,64),
(false,65),
(false,66),
(false,67),
(false,68),
(false,69),
(false,70),
(false,71),
(false,72),
(true,6),
(false,73),
(false,73),
(false,73),
(false,73),
(true,7),
(false,8),
(true,8),
(true,8),
(false,8),
(true,74),
(true,74),
(true,74),
(true,74),
(false,75),
(true,76),
(true,77),
(true,78),
(true,79),
(true,80),
(true,81),
(true,82),
(true,83),
(true,84),
(true,85),
(false,86),
(true,87),
(true,88),
(true,88),
(true,89),
(true,90),
(true,91),
(true,92),
(true,93),
(true,92),
(true,94),
(true,88),
(true,92),
(true,95),
(true,96),
(true,97),
(true,98),
(false,99),
(true,100),
(true,101),
(true,102),
(true,103),
(true,104),
(true,103),
(true,105),
(true,106),
(true,107),
(true,108),
(true,109),
(true,110),
(true,111),
(true,112),
(true,113),
(true,103),
(true,114),
(true,115),
(true,116),
(false,117),
(true,118),
(true,119),
(true,120),
(true,121),
(true,120),
(true,122),
(true,122),
(true,120),
(true,123),
(true,120),
(true,124),
(true,125),
(true,126),
(true,122),
(true,122),
(true,127),
(false,128),
(true,129),
(true,130),
(true,131),
(true,132),
(true,133),
(true,134),
(true,135),
(true,136),
(true,137),
(true,138),
(false,139),
(true,140),
(true,140),
(true,140),
(true,140),
(false,141),
(true,142),
(false,142),
(true,143),
(false,143),
(true,144),
(true,144),
(true,145),
(true,145),
(false,146),
(true,147),
(true,148),
(true,147),
(true,149),
(true,150),
(true,151),
(true,152),
(true,153),
(true,154),
(true,155),
(false,156),
(true,157),
(true,158),
(true,159),
(true,160),
(true,161),
(true,162),
(true,162),
(true,163),
(true,164),
(true,163),
(true,165),
(true,166),
(true,167),
(true,162),
(true,168),
(true,169),
(false,170),
(true,171),
(true,172),
(true,173),
(true,174),
(true,175),
(true,174),
(true,176),
(true,177),
(true,178),
(true,179),
(true,180),
(true,181),
(true,181),
(true,182),
(true,183),
(true,174),
(true,184),
(true,185),
(true,186),
(false,187),
(true,188),
(true,189),
(true,189),
(true,190),
(true,191),
(true,192),
(true,193),
(true,194),
(true,193),
(true,195),
(true,189),
(true,193),
(true,196),
(true,197),
(true,198),
(true,199),
(false,200),
(true,201),
(true,202),
(true,203),
(true,204),
(true,205),
(true,206),
(true,207),
(true,208),
(true,209),
(true,210),
(false,211),
(true,212),
(true,212),
(true,212),
(true,212),
(false,213)]
private def refs1 : List (Bool × Fin 463) :=
[(false,214),
(false,215),
(false,216),
(false,217),
(false,218),
(false,219),
(false,220),
(false,221),
(false,222),
(false,214),
(true,214),
(false,223),
(false,223),
(false,224),
(false,224),
(true,215),
(false,225),
(false,226),
(false,227),
(false,228),
(false,229),
(false,230),
(false,231),
(false,232),
(false,233),
(false,234),
(true,216),
(false,235),
(false,236),
(false,237),
(false,238),
(false,239),
(false,240),
(false,241),
(false,239),
(false,242),
(false,239),
(false,243),
(false,244),
(false,245),
(false,240),
(false,240),
(false,246),
(true,217),
(false,247),
(false,248),
(false,249),
(false,250),
(false,251),
(false,252),
(false,253),
(false,254),
(false,255),
(false,256),
(false,257),
(false,258),
(false,259),
(false,250),
(false,260),
(false,250),
(false,261),
(false,262),
(false,263),
(true,218),
(false,264),
(false,265),
(false,266),
(false,267),
(false,268),
(false,269),
(false,270),
(false,271),
(false,272),
(false,266),
(false,273),
(false,274),
(false,275),
(false,276),
(false,277),
(false,278),
(true,219),
(false,279),
(false,280),
(false,281),
(false,282),
(false,283),
(false,284),
(false,285),
(false,286),
(false,287),
(false,288),
(true,220),
(false,289),
(false,289),
(false,289),
(false,289),
(true,221),
(false,222),
(true,222),
(true,222),
(false,222),
(true,290),
(true,290),
(true,290),
(true,290),
(false,291),
(true,292),
(true,293),
(true,294),
(true,295),
(true,296),
(true,297),
(true,298),
(true,299),
(true,300),
(true,299),
(false,301),
(true,302),
(true,303),
(true,304),
(true,305),
(true,306),
(true,307),
(true,308),
(true,309),
(true,308),
(true,304),
(true,304),
(true,310),
(true,311),
(true,312),
(true,313),
(true,314),
(false,315),
(true,316),
(true,317),
(true,318),
(true,319),
(true,320),
(true,321),
(true,322),
(true,322),
(true,323),
(true,324),
(true,325),
(true,326),
(true,327),
(true,319),
(true,328),
(true,319),
(true,329),
(true,330),
(true,331),
(false,332),
(true,333),
(true,334),
(true,335),
(true,336),
(true,337),
(true,338),
(true,339),
(true,337),
(true,340),
(true,337),
(true,341),
(true,342),
(true,343),
(true,338),
(true,338),
(true,344),
(false,345),
(true,346),
(true,347),
(true,348),
(true,349),
(true,350),
(true,351),
(true,352),
(true,353),
(true,354),
(true,355),
(false,356),
(true,212),
(true,212),
(true,212),
(true,212),
(false,213),
(true,8),
(false,8),
(true,357),
(true,357),
(true,357),
(true,357),
(false,358),
(true,359),
(true,360),
(true,361),
(true,362),
(true,363),
(true,364),
(true,365),
(true,366),
(true,367),
(true,368),
(false,369),
(true,370),
(true,371),
(true,372),
(true,373),
(true,374),
(true,375),
(true,376),
(true,377),
(true,378),
(true,372),
(true,379),
(true,378),
(true,380),
(true,381),
(true,382),
(true,383),
(false,384),
(true,385),
(true,386),
(true,387),
(true,388),
(true,389),
(true,390),
(true,387),
(true,391),
(true,392),
(true,393),
(true,394),
(true,395),
(true,396),
(true,388),
(true,397),
(true,388),
(true,395),
(true,395),
(true,398),
(false,399),
(true,400),
(true,401),
(true,402),
(true,403),
(true,404),
(true,405),
(true,405),
(true,404),
(true,406),
(true,404),
(true,407),
(true,408),
(true,409),
(true,405),
(true,405),
(true,410),
(false,411),
(true,412),
(true,413),
(true,412),
(true,414),
(true,415),
(true,416),
(true,417),
(true,418),
(true,419),
(true,420),
(false,421),
(true,422),
(true,422),
(true,422),
(true,422),
(false,423),
(true,142),
(false,142),
(true,424),
(false,424),
(true,425),
(true,425),
(true,426),
(true,426),
(false,427),
(true,428),
(true,429),
(true,428),
(true,430),
(true,430),
(true,431),
(true,430),
(true,430),
(true,432),
(true,431),
(false,433),
(true,434),
(true,434),
(true,435),
(true,436),
(true,435),
(true,437),
(true,437),
(true,435),
(true,436),
(true,435),
(true,438),
(true,438),
(true,439),
(true,437),
(true,437),
(true,439),
(false,440),
(true,441),
(true,442),
(true,442),
(true,443),
(true,444),
(true,443),
(true,442),
(true,442),
(true,445),
(true,446),
(true,445),
(true,447),
(true,447),
(true,443),
(true,444),
(true,443),
(true,447),
(true,447),
(true,448),
(false,449),
(true,450),
(true,451),
(true,451),
(true,450),
(true,452),
(true,452),
(true,453),
(true,454),
(true,453),
(true,451),
(true,451),
(true,453),
(true,454),
(true,453),
(true,455),
(true,455),
(false,456),
(true,457),
(true,458),
(true,459),
(true,459),
(true,457),
(true,459),
(true,459),
(true,460),
(true,461),
(true,460),
(false,462)]
def entriesOwner2 (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.