# Manifold: Census Knot K8_162

# Number of Tetrahedra: 8

# Number Field
x^23 + 7*x^22 - 36*x^21 + 84*x^20 + 54*x^19 - 540*x^18 + 400*x^17 + 1429*x^16 - 335*x^15 - 3555*x^14 - 1899*x^13 + 5406*x^12 + 7441*x^11 - 583*x^10 - 8465*x^9 - 6242*x^8 + 1595*x^7 + 4760*x^6 + 1930*x^5 - 798*x^4 - 702*x^3 - 19*x^2 + 61*x + 7 

# Approximate Field Generator
-0.524009521935197 + 0.905840325233239*I

# Shape Parameters
629639617940850124393536041924629927379519/91667941719829066059187428769449988506212*y^22 + 3908281568636125891074340835570356160388245/91667941719829066059187428769449988506212*y^21 - 12883378592612490139500765269930022566850029/45833970859914533029593714384724994253106*y^20 + 73310176943476847372554238547308750382181161/91667941719829066059187428769449988506212*y^19 - 24082980536926067309902100839314440090831849/91667941719829066059187428769449988506212*y^18 - 321005575537424669350474580114299407749569179/91667941719829066059187428769449988506212*y^17 + 253153620881920719947647634301046276566530295/45833970859914533029593714384724994253106*y^16 + 124718883054806952650096902083275721215700645/22916985429957266514796857192362497126553*y^15 - 606823948915028460771760436589116908883097091/91667941719829066059187428769449988506212*y^14 - 439647759203460588376344045907162655067695922/22916985429957266514796857192362497126553*y^13 + 49579136363136564949265237684886258880485245/22916985429957266514796857192362497126553*y^12 + 3249895970794419496008606483973148773580038291/91667941719829066059187428769449988506212*y^11 + 2111602837231140907746801131056263382110158867/91667941719829066059187428769449988506212*y^10 - 1022562631996180681046860649452125232598863095/45833970859914533029593714384724994253106*y^9 - 929227984416662258753615304300538773254871005/22916985429957266514796857192362497126553*y^8 - 986432766434726162056836927608047688772993341/91667941719829066059187428769449988506212*y^7 + 448098997627481122741694293463200162406066290/22916985429957266514796857192362497126553*y^6 + 1583408350663647051732758238629806074622739949/91667941719829066059187428769449988506212*y^5 - 38904930855300998928007330134745111001433399/91667941719829066059187428769449988506212*y^4 - 237286157174543149276302242432582107231575905/45833970859914533029593714384724994253106*y^3 - 16909575890397242240407779184479364613281359/22916985429957266514796857192362497126553*y^2 + 20853637606076550677288580676517473957533511/45833970859914533029593714384724994253106*y + 2822635008675437674428921538632176818337455/45833970859914533029593714384724994253106

304078473867971681558759920086411680359758/664592577468760728929108858578512416670037*y^22 + 1794070469183979376688943140646833972579932/664592577468760728929108858578512416670037*y^21 - 13074852745307544296813746198848955099649132/664592577468760728929108858578512416670037*y^20 + 38876300263704860932790216404273049519950249/664592577468760728929108858578512416670037*y^19 - 20600349616539476863161314639266661191078041/664592577468760728929108858578512416670037*y^18 - 156132149416039306499466442770998275019682604/664592577468760728929108858578512416670037*y^17 + 290236010690202163894012739760202548494164991/664592577468760728929108858578512416670037*y^16 + 194088857453743354479840268345541795998216579/664592577468760728929108858578512416670037*y^15 - 394396443645354813223587861747842354347747328/664592577468760728929108858578512416670037*y^14 - 824325429288367578778645699374545559098796759/664592577468760728929108858578512416670037*y^13 + 388285728510118181983251447507044361402035115/664592577468760728929108858578512416670037*y^12 + 1700251693997438762255307659073369563671842312/664592577468760728929108858578512416670037*y^11 + 607570538414151437889028237866488303843935897/664592577468760728929108858578512416670037*y^10 - 1569742222805522898094654886294872724094628930/664592577468760728929108858578512416670037*y^9 - 1791980151670418403914792440459529668117431243/664592577468760728929108858578512416670037*y^8 + 121569254993356003343206787163923203158543555/664592577468760728929108858578512416670037*y^7 + 1368258312638906671231418671568942847284904832/664592577468760728929108858578512416670037*y^6 + 738088996656336355939625450731789962716345289/664592577468760728929108858578512416670037*y^5 - 310996250915184009444691278775091371380059027/664592577468760728929108858578512416670037*y^4 - 388032439178030064239642113237317168617176993/664592577468760728929108858578512416670037*y^3 - 28726402512101139094303163810428540007645457/664592577468760728929108858578512416670037*y^2 + 44733379998519846146262828825509817969206933/664592577468760728929108858578512416670037*y + 5665251921175771602369399393761854360722532/664592577468760728929108858578512416670037

-237524793204252014051755333980284359142415/320837796019401731207156000693074959771742*y^22 - 107468025765344947723823507370320288915576/22916985429957266514796857192362497126553*y^21 + 9556457210480703961989548691315861393774449/320837796019401731207156000693074959771742*y^20 - 3753745803993078928095986031402666911760357/45833970859914533029593714384724994253106*y^19 + 4588191033944781348328513337088259241969141/320837796019401731207156000693074959771742*y^18 + 125175479160492018992205303303142269767806439/320837796019401731207156000693074959771742*y^17 - 177162594453646434968313210008373001955710773/320837796019401731207156000693074959771742*y^16 - 223545616798368793868025407599582296567418365/320837796019401731207156000693074959771742*y^15 + 112520636636626680002221176218342678901542845/160418898009700865603578000346537479885871*y^14 + 352914726492882206642647133410892996698239529/160418898009700865603578000346537479885871*y^13 - 4983684316300175232073114283325468987233721/160418898009700865603578000346537479885871*y^12 - 1296077452418956411529356291948843411595987915/320837796019401731207156000693074959771742*y^11 - 134358664789877449463539559295238581480569797/45833970859914533029593714384724994253106*y^10 + 775227581896009195482311216286314149081630363/320837796019401731207156000693074959771742*y^9 + 783847311839175104272625050464024153906462298/160418898009700865603578000346537479885871*y^8 + 244391977665465255694686453062766090099151362/160418898009700865603578000346537479885871*y^7 - 371037169181905128645039419424826831853088590/160418898009700865603578000346537479885871*y^6 - 102387476067207488305490804880175447207288223/45833970859914533029593714384724994253106*y^5 - 7660673750125948694522951029162766705402035/160418898009700865603578000346537479885871*y^4 + 16048441073146470617203635510315698511534696/22916985429957266514796857192362497126553*y^3 + 24572087151519163493481215046626333696126980/160418898009700865603578000346537479885871*y^2 - 21218756890315168273207492456106454703253429/320837796019401731207156000693074959771742*y - 5045696061917019538879584787695744134544503/320837796019401731207156000693074959771742

-7329827460816242188914406798137990729669/22916985429957266514796857192362497126553*y^22 - 45625183060904296336668183872963367541173/22916985429957266514796857192362497126553*y^21 + 299646539099689358852679870071470790833964/22916985429957266514796857192362497126553*y^20 - 845400360497492581473820387876636892405024/22916985429957266514796857192362497126553*y^19 + 244874751888518984721706272629313231374546/22916985429957266514796857192362497126553*y^18 + 3805965435243147213760300606438198478627618/22916985429957266514796857192362497126553*y^17 - 5876453256730098538286530132868090958526801/22916985429957266514796857192362497126553*y^16 - 6120115237262944573821891133961238071302242/22916985429957266514796857192362497126553*y^15 + 7406751303081386062370983577964485204830088/22916985429957266514796857192362497126553*y^14 + 20769973170307984270821290412430127310317255/22916985429957266514796857192362497126553*y^13 - 2345170336807658194560522299983855365092917/22916985429957266514796857192362497126553*y^12 - 39100735214674083085706035938850455820009460/22916985429957266514796857192362497126553*y^11 - 24766901585693282703322688420695029275962649/22916985429957266514796857192362497126553*y^10 + 25441226312616801566206720668229773724950492/22916985429957266514796857192362497126553*y^9 + 44828467225718228255930298319959610242505920/22916985429957266514796857192362497126553*y^8 + 10757396606906369233545799146771184666922897/22916985429957266514796857192362497126553*y^7 - 22957658363706771343397821127888048083190902/22916985429957266514796857192362497126553*y^6 - 19368566782247438317046912366620998595634365/22916985429957266514796857192362497126553*y^5 + 1069730231953942510519757987362353957159784/22916985429957266514796857192362497126553*y^4 + 6381644210283700811734888611341444451962662/22916985429957266514796857192362497126553*y^3 + 866556145842161060329460946434512959372007/22916985429957266514796857192362497126553*y^2 - 624704664158496260951380145980950528929179/22916985429957266514796857192362497126553*y - 107734271019699436645430744518330284752981/22916985429957266514796857192362497126553

885774899736966544619297827608336050467662/22916985429957266514796857192362497126553*y^22 + 5498062025070021447925372057626994249488450/22916985429957266514796857192362497126553*y^21 - 36247514807317203763842330103103608797002779/22916985429957266514796857192362497126553*y^20 + 103146972809710003874151213159075186802996140/22916985429957266514796857192362497126553*y^19 - 33956451517917130432570763266334093472169948/22916985429957266514796857192362497126553*y^18 - 451394255606959616537731567195454536327860082/22916985429957266514796857192362497126553*y^17 + 712231469949980711258958825284797535832072754/22916985429957266514796857192362497126553*y^16 + 701044196370317286608034098210252041779779846/22916985429957266514796857192362497126553*y^15 - 852647885155283920914216995469450273754094399/22916985429957266514796857192362497126553*y^14 - 2472923786444504539972396758295197539152612187/22916985429957266514796857192362497126553*y^13 + 279021925607864306053572367206071743935969345/22916985429957266514796857192362497126553*y^12 + 4567336650184756370040997110440918656640167649/22916985429957266514796857192362497126553*y^11 + 2968846558058291604285208945586343972154614065/22916985429957266514796857192362497126553*y^10 - 2870820442549877985540988769235554219892745909/22916985429957266514796857192362497126553*y^9 - 5220685582619578599694965647316777703934358768/22916985429957266514796857192362497126553*y^8 - 1388272036943515471313990408823679681060946010/22916985429957266514796857192362497126553*y^7 + 2512646976818591651193212136639789617258719418/22916985429957266514796857192362497126553*y^6 + 2221949987332753032475246183505324894508888338/22916985429957266514796857192362497126553*y^5 - 52675681356792272970585711086427324664384708/22916985429957266514796857192362497126553*y^4 - 663937130006735095361055675487360733564016338/22916985429957266514796857192362497126553*y^3 - 94588043494174556660356031674616457474113378/22916985429957266514796857192362497126553*y^2 + 58156842138799174602289059591578240865155087/22916985429957266514796857192362497126553*y + 7802100214026161496213491163181599211151931/22916985429957266514796857192362497126553

-120296764872288674650193153419291934880639/22916985429957266514796857192362497126553*y^22 - 746645958660975645838145464456537264968574/22916985429957266514796857192362497126553*y^21 + 4923178688800949725497083526739292482213176/22916985429957266514796857192362497126553*y^20 - 14009060301278439757954955093422182284068900/22916985429957266514796857192362497126553*y^19 + 4611865360173729137889772166800263205727259/22916985429957266514796857192362497126553*y^18 + 61310823341816666926380574767766799156398333/22916985429957266514796857192362497126553*y^17 - 96730395519424724665798414532037649179587125/22916985429957266514796857192362497126553*y^16 - 95267433799631549383791151580361854405499203/22916985429957266514796857192362497126553*y^15 + 115871453219729049020630359831745050543388787/22916985429957266514796857192362497126553*y^14 + 336087522624272620265931434315522953525110247/22916985429957266514796857192362497126553*y^13 - 38085531866339619134600470732371756926025805/22916985429957266514796857192362497126553*y^12 - 620825069670392919344992126653144675338602718/22916985429957266514796857192362497126553*y^11 - 403461981684448895999673877305432932415904235/22916985429957266514796857192362497126553*y^10 + 391078605212383440896605269076452197782048409/22916985429957266514796857192362497126553*y^9 + 710176264560070370400794719470160003432689069/22916985429957266514796857192362497126553*y^8 + 188147034908753164977079064947237265436386749/22916985429957266514796857192362497126553*y^7 - 342901626540368406459353662987235053072835406/22916985429957266514796857192362497126553*y^6 - 302607738880520739666592780229894136836676309/22916985429957266514796857192362497126553*y^5 + 7714402216540523558835045530900973742952694/22916985429957266514796857192362497126553*y^4 + 90889020283667310403389191029359403312939346/22916985429957266514796857192362497126553*y^3 + 12955796252003029342230775976761260887082351/22916985429957266514796857192362497126553*y^2 - 8020383439393908101751203270504545378126662/22916985429957266514796857192362497126553*y - 1031969457723020994304155401043911869528632/22916985429957266514796857192362497126553

133619164237678148901188508414559225687984/664592577468760728929108858578512416670037*y^22 + 876845763862925761683585967460569725337735/664592577468760728929108858578512416670037*y^21 - 5162847437358635799836574227965975036494351/664592577468760728929108858578512416670037*y^20 + 13697602473653223289023216639970906950712995/664592577468760728929108858578512416670037*y^19 + 56096729521909902397112271122304104629921/664592577468760728929108858578512416670037*y^18 - 69383903206042298814758102149995069293719065/664592577468760728929108858578512416670037*y^17 + 85154720017196136627118957855770137364245688/664592577468760728929108858578512416670037*y^16 + 136206866463172484368392963829361650897049341/664592577468760728929108858578512416670037*y^15 - 88727960635234840932256356596809614371890746/664592577468760728929108858578512416670037*y^14 - 393469662999152046180655132305158223288300582/664592577468760728929108858578512416670037*y^13 - 100449882120003393455674277554850651508065780/664592577468760728929108858578512416670037*y^12 + 658976774130612217932362088371380640113070755/664592577468760728929108858578512416670037*y^11 + 659898541397900361805367697430105900842610244/664592577468760728929108858578512416670037*y^10 - 188379124991630566468047312714122568603713603/664592577468760728929108858578512416670037*y^9 - 840371551554767679405225561389586147826051069/664592577468760728929108858578512416670037*y^8 - 508126942652200687644773930435048186080337011/664592577468760728929108858578512416670037*y^7 + 172061794540416211559453752620107772448948062/664592577468760728929108858578512416670037*y^6 + 380077341766808843959439796286835000310411996/664592577468760728929108858578512416670037*y^5 + 141870723982830205465534273736898482010795516/664592577468760728929108858578512416670037*y^4 - 29182876400978098683643061425547476594331716/664592577468760728929108858578512416670037*y^3 - 16790211796683495950383085533521740445627401/664592577468760728929108858578512416670037*y^2 - 3817623248004141516943151403053318194615906/664592577468760728929108858578512416670037*y - 349312235847092825388118383438047474633317/664592577468760728929108858578512416670037

y


# A Gluing Matrix
{{1,0,-2,0,-2,2,0,2},{0,0,-1,0,0,2,0,2},{-2,-1,3,0,4,-2,0,-2},{0,0,0,0,0,1,0,2},{-2,-1,3,-1,4,-3,1,-2},{2,1,-3,0,-3,4,1,2},{0,-1,-1,-1,1,1,1,0},{2,2,-2,2,-2,2,0,1}}

# B Gluing Matrix
{{1,0,0,0,0,0,0,0},{0,1,0,0,0,0,1,0},{0,0,1,0,0,0,1,0},{0,0,0,1,0,0,1,0},{0,0,0,0,1,0,1,0},{0,0,0,0,0,1,1,0},{0,0,0,0,0,0,2,0},{0,0,0,0,0,0,0,1}}

# nu Gluing Vector
{1, 2, 1, 2, 1, 1, 0, 1}

# f Combinatorial flattening
{273, 215, 48, -309, 167, 48, -261, -23}

# f' Combinatorial flattening
{108, 0, 0, 0, 0, 0, 0, 0}

# 1 Loop Invariant
2300666513050442185716719669649896371078685/45833970859914533029593714384724994253106*y^22 + 14340972685011887606706360681486293895711125/45833970859914533029593714384724994253106*y^21 - 46910102177333480955104978071912237811512429/22916985429957266514796857192362497126553*y^20 + 132578564584566862563369095042185753997898834/22916985429957266514796857192362497126553*y^19 - 78985806212278241203954677576645920339992543/45833970859914533029593714384724994253106*y^18 - 590942248804058129525192512652572795150026492/22916985429957266514796857192362497126553*y^17 + 1826021482442228872337612376125187532313596123/45833970859914533029593714384724994253106*y^16 + 944084573062149637811168183086963352918672811/22916985429957266514796857192362497126553*y^15 - 2216414746055795844718548580235090756341808799/45833970859914533029593714384724994253106*y^14 - 6482201182850596199768742611074041938641442021/45833970859914533029593714384724994253106*y^13 + 294928839235026378362596935175551686289146836/22916985429957266514796857192362497126553*y^12 + 5995851674119812972513142359116096026198785225/22916985429957266514796857192362497126553*y^11 + 3975413276576392992014038470995699692557751216/22916985429957266514796857192362497126553*y^10 - 3714291768163112763822970854194608734690295311/22916985429957266514796857192362497126553*y^9 - 13820795574070390860711961309260712826310371143/45833970859914533029593714384724994253106*y^8 - 3815866151694927865983966739421505948076458271/45833970859914533029593714384724994253106*y^7 + 6598678057475506266495239690656900962127763069/45833970859914533029593714384724994253106*y^6 + 5941560771703947827832509805561359509891275753/45833970859914533029593714384724994253106*y^5 - 38331661545013634270954461111785781293695345/22916985429957266514796857192362497126553*y^4 - 1783934900154875365222113044271621182986786691/45833970859914533029593714384724994253106*y^3 - 268228404815322316739340662261492749373788613/45833970859914533029593714384724994253106*y^2 + 77562153318808030055608513403742950812410567/22916985429957266514796857192362497126553*y + 25573709332392140610531252258619733310392303/45833970859914533029593714384724994253106

# 2 Loop Invariant
29523928837830700478001658165627567231909411249055381373687305352312196352865991162167738529510954163621943870581/7182866377364820800167228437429285130909211225440201187438274782254213020668871936990487354653657824440558285697000*y^22 + 1239307277644564927451835513519511346770694155434548502910780413633330167625945943469928074973937188379617150253229/43097198264188924801003370624575710785455267352641207124629648693525278124013231621942924127921946946643349714182000*y^21 - 553023872353428940196478512273516794248118737067467097354179238416422883662804941912387399162405161084766368845239/3591433188682410400083614218714642565454605612720100593719137391127106510334435968495243677326828912220279142848500*y^20 + 6694991255894262362801693576190594783596457593378594509032684473222575339736189939167505630294993808956512769593399/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^19 + 674870996809287354701716995443113534943602382733852654919398570572600709352615036356929571586727080430886977103451/1436573275472964160033445687485857026181842245088040237487654956450842604133774387398097470930731564888111657139400*y^18 - 12818249547100074024038911811020996546828129297158775150701270058340912968534984429018106122014602088707488078112653/4309719826418892480100337062457571078545526735264120712462964869352527812401323162194292412792194694664334971418200*y^17 + 18144539406843907607040711743025905763055168037870562831416371686060107182837843809742231571585326819177562099001943/8619439652837784960200674124915142157091053470528241424925929738705055624802646324388584825584389389328669942836400*y^16 + 372381442572721216588051222754797327034400128222894205140624133874190365181876614852084362055867738549731682065601049/43097198264188924801003370624575710785455267352641207124629648693525278124013231621942924127921946946643349714182000*y^15 - 145403235814024327365897715430352690528477714032971178556508470123133518245484408442579166032515957405990405711911771/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^14 - 377467401393343373909930885889561459577841331588341953656086593799767773663141637087794897983547404155245145056557687/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^13 - 48124452929081096640541395655252807467240743311405068009949780624668152582224988652486222989367345031926339875106191/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^12 + 530538061746050820980930376637447580299912626498603930444264238206523375165107414344758054891536737942725396341063189/14365732754729641600334456874858570261818422450880402374876549564508426041337743873980974709307315648881116571394000*y^11 + 224064478293263482386264461243651680821110857285619866321282119479169914197825792302857050899186367440960930002012009/8619439652837784960200674124915142157091053470528241424925929738705055624802646324388584825584389389328669942836400*y^10 - 52770575325117415423821227638066847073349501363351984849954150483251119898405083434066233908653045379149117939047727/1795716594341205200041807109357321282727302806360050296859568695563553255167217984247621838663414456110139571424250*y^9 - 701568263554633201237665693811018312026707720728334193454801831609296113560890292077223195821822446078672220783040417/14365732754729641600334456874858570261818422450880402374876549564508426041337743873980974709307315648881116571394000*y^8 - 165127228246715745959262081479660200967705288106611727542248715760530145671714983059149302993647617484152602487721047/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^7 + 249119472474008819462954787059484847227331165403590879766517182026457955359256433430127696267810794434852297562395377/7182866377364820800167228437429285130909211225440201187438274782254213020668871936990487354653657824440558285697000*y^6 + 368643137777768371824130289605396961408796122369981659057683837126476901927026725089408391313882876362882153906470673/14365732754729641600334456874858570261818422450880402374876549564508426041337743873980974709307315648881116571394000*y^5 - 100378865006962527049594669735741123645337183739641553718463615064556595879757596749469606979746320361536585378674481/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^4 - 294829780830137385467726349908228595697527278441917497938261054178594865160948250167406926545028671879476125249612081/21548599132094462400501685312287855392727633676320603562314824346762639062006615810971462063960973473321674857091000*y^3 - 7640736542193792529278026425567460207018523585655995162998097948691105849403222378433107232607516002283691568172441/2693574891511807800062710664035981924090954209540075445289353043345329882750826976371432757995121684165209357136375*y^2 + 26405019758326942949442159959271735981078562046118157633527569113675100776227558764935385207205503491856161928240583/14365732754729641600334456874858570261818422450880402374876549564508426041337743873980974709307315648881116571394000*y - 9818666589556098576066809551731491262891858942447703635786737768739924392212367186891698783070653133703844673984495446/2693574891511807800062710664035981924090954209540075445289353043345329882750826976371432757995121684165209357136375

# 3 Loop Invariant
-681134679718776978849460731322360749742496867824495457454944327604953744811020783791766123375781526484111352758648491399647224134284756926896281856607/201065677244630864097893095619982025657658805480775908968990861833083077977786391332739665992141109925811705845914545638828178893296556982088196861450000*y^22 - 4645691592780561066321420435660407486312201193250415112641690911091876135060870429609922728592827604677969917663723509055160898872723215662769126746549/201065677244630864097893095619982025657658805480775908968990861833083077977786391332739665992141109925811705845914545638828178893296556982088196861450000*y^21 + 10278029066795638670202473906950636517064048484383585608582229194670861313776555559109189764398896897500835535486164592804036256866922787010811625955673/80426270897852345639157238247992810263063522192310363587596344733233231191114556533095866396856443970324682338365818255531271557318622792835278744580000*y^20 - 5972098778693157391637551746851888505026656243879165482772335237164559861230427136909145213002338312378744350767761715304954257701384425617869987702481/20106567724463086409789309561998202565765880548077590896899086183308307797778639133273966599214110992581170584591454563882817889329655698208819686145000*y^19 - 159679946459998785792050353411885287080470711556844195196965755910673237121099069655955718217190829481603105683461994806820875878798174561592569937954789/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^18 + 1662485987546324225523332243894346016880727541224505734704181619024289250963598134089103280163736544999395387180337558262769892058403217178694812269284927/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^17 - 730922855077217228248770357694769155543384282771060095127301777955526622195436669550896136182748449882671096653599831428040877585436527515405980124763333/402131354489261728195786191239964051315317610961551817937981723666166155955572782665479331984282219851623411691829091277656357786593113964176393722900000*y^16 - 4270752924625964620723348218326187136084651072114618507473806478222173975307715480533377655506023242995961697508913371946752774720806647337079200049813909/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^15 + 691838579037072990251447102520723513435561962278188560810648419440793736280225862094350607186041788280424803685869140414633209837920059138710733886459839/201065677244630864097893095619982025657658805480775908968990861833083077977786391332739665992141109925811705845914545638828178893296556982088196861450000*y^14 + 1003252651466863424530412469226014397130430334713322979405530344455355223894611601595166446235426468792085831006200617432330313547821062231620780805303417/80426270897852345639157238247992810263063522192310363587596344733233231191114556533095866396856443970324682338365818255531271557318622792835278744580000*y^13 + 2383232408742250635968976161053049184196160135686204882349482061447505199898732949678414479740380212824705222897426863466710896735541773854164868105881423/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^12 - 18633582062697301923354037892351634093195900964472922928803678556724537509985293516689773707471538918070515186339770377105837578426478901744624956852042159/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^11 - 4174961387349780746160154432199030209448195309836788887958074986738817544411238075810218220461085816618521427060436694755640220464055503021421780526683681/201065677244630864097893095619982025657658805480775908968990861833083077977786391332739665992141109925811705845914545638828178893296556982088196861450000*y^10 + 10463512722668754811459816252724818982127888434037073982359583369155909737284746962152202985567218539216025593666513120986117578285973325678323016015681951/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^9 + 799417349901915650510665478308670922428000151315013996088984896938972066335870634038381614892334056059059769770081800245688933800220874374489869884880407/25133209655578858012236636952497753207207350685096988621123857729135384747223298916592458249017638740726463230739318204853522361662069622761024607681250*y^8 + 9670446115053370663631461891211125830254382092098682392016193913883315977089545126985299384617353415230992453373687044765491007261066684642869106758274283/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^7 - 12462543970934700858234720984616306439251165525425156943418725793099875283411070762378136481963736944356507757624920466913017172376398424386816317227477263/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^6 - 13213525248914535528048808326513622599522621728837768590554381599784503635246808769634816471344722041777300536464770095241713241463420340333785038037143589/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^5 - 373631937213812485458699682921796180894749696110509145414256860706121741516598000961633971416842038866627367908833366074416264549407035616741361227353327/402131354489261728195786191239964051315317610961551817937981723666166155955572782665479331984282219851623411691829091277656357786593113964176393722900000*y^4 + 2363585954373540509972368272485324946593635693586362402735067033560884375379130191472667409262919495212039360463893004508045298175694948226164030702766617/402131354489261728195786191239964051315317610961551817937981723666166155955572782665479331984282219851623411691829091277656357786593113964176393722900000*y^3 + 1276841566947533808009251772733630613734343111705171220080477439061297903371445055551768583755178714161961979138724746257326916826617663295283353858911787/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000*y^2 - 22695983796605297661556165489188527302946904117712250342213486803043297576525143403694036809535708391643411590529227905022435795817987867716512671604367/32170508359140938255662895299197124105225408876924145435038537893293292476445822613238346558742577588129872935346327302212508622927449117134111497832000*y - 66074140679908216626297104774837594728234794402629953413592701228277749180420703523351712316755416590431612580097106405508016120566905240778092912179419/804262708978523456391572382479928102630635221923103635875963447332332311911145565330958663968564439703246823383658182555312715573186227928352787445800000

# 4 Loop Invariant
152502353189745450218439576596552199425201707592151938537161619712153673274473917337940759611092183113297525781820825848315484530534907210312159494049573151543135090481254765737779577584477362655534045904138478858551571427855079/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^22 + 1007888338141298293679633448359685814207476485375628062535123037050107033867266755776791400815975035565479480151993202840531847435579690211989100317747035168647237572265039981415607922661778918473541999380469494015814204269039881/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^21 - 1469130377365278065086643957948083909906553293772422934656495404182854477926879026281180567443706120381560057769228464902940263425142059295005479892854516094940714709701351505603840244536602665453695796446067285959447966369536413/5671797922213520113117379974284703187048801876125354314453611867924064644218434978063149346037911600754339143122435259074599662101881742044446029375130677930810121031922141311741090634435060888796574428629187768901884094500000000*y^20 + 15164678299773273162549018277833857505653876582027047950032230557778671826708368913422826980305822245504047860722853380576274230671337716988679401152150636676164839111830025515937875125075401322879368930675091955034830149116894797/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^19 + 410787215951279420131399700678681796216578113177599359213568543094761681534559982797450946964712115075642493846301312397364460367565058236622036027429862789617904678891279494670879254129173340649854810743411628317204331747231099/4537438337770816090493903979427762549639041500900283451562889494339251715374747982450519476830329280603471314497948207259679729681505393635556823500104542344648096825537713049392872507548048711037259542903350215121507275600000000*y^18 - 5508048083280743938193757841769217238128734822954981007427990351538830365749101648162046652532163398699458929606793164030736734829223493919898564497257984872020963776929285335620017439703048415589784057615473103573823974023156993/1512479445923605363497967993142587516546347166966761150520963164779750571791582660816839825610109760201157104832649402419893243227168464545185607833368180781549365608512571016464290835849349570345753180967783405040502425200000000*y^17 + 9399498109836342160058966320775327110530265033677334837426463707408380975713277009054370864700688669067073144338674369150112689245435997002865038907912959658244657782443311409884297721640218897551017599365431363427089227629061981/2268719168885408045246951989713881274819520750450141725781444747169625857687373991225259738415164640301735657248974103629839864840752696817778411750052271172324048412768856524696436253774024355518629771451675107560753637800000000*y^16 + 177132297129296731565490444850616042837507498844066979879056947291214001780941406122131420774795832258188963024775551272960468367808973911082020084159371094797543022181709528279011426487171305962571028762284282777355857053454890511/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^15 - 118623041256124034741921977113389374129102425778793053527282563652803042158086569868932540030385017871152046575780166061684197138427652398009939050751656570698440201618470210544363649129253918893851820950727535988833564567491095013/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^14 - 26882846641420265506675557801417377142474055845387698236909484447465016295308120656056072132787401971038233711336999997648817913023274136299749182990497025118040012266664772442513976391811335056036336403753631096330717181008048027/1260399538269671136248306660952156263788622639138967625434135970649792143159652217347366521341758133500964254027207835349911036022640387120988006527806817317957804673760475847053575696541124641954794317473152837533752021000000000*y^13 - 11091284145646989241792518029037191453012793398303456949575498228419928602609961607043739365164689882687679105037921003200492591928341879984349903097426045758854789595735758059650383362344597504074898613535017722222552860234177597/2520799076539342272496613321904312527577245278277935250868271941299584286319304434694733042683516267001928508054415670699822072045280774241976013055613634635915609347520951694107151393082249283909588634946305675067504042000000000*y^12 + 279374468780713763563803727704283841174541692721967030232223849659718232456443004122144061932546199702532991786118675754641525649091069133003915680964015528343917509536122375103996078016804935861751046958728602785054299645598595671/7562397229618026817489839965712937582731735834833805752604815823898752858957913304084199128050548801005785524163247012099466216135842322725928039166840903907746828042562855082321454179246747851728765904838917025202512126000000000*y^11 + 78414900210841462716526994997467487963692905778408254755528750821670129033189726304390150243087692020983340830126926759992905960785740044842263678199899186125526906283362874519570393926472631922499758467325181329829663026757115483/2268719168885408045246951989713881274819520750450141725781444747169625857687373991225259738415164640301735657248974103629839864840752696817778411750052271172324048412768856524696436253774024355518629771451675107560753637800000000*y^10 - 45355459696428379245003405219117399713770232416966447955760778419567386777686472105758911906320713928662788936629286931099822861103467221446386431219307772372336509175326740116896806641167157373308090316450658694025578102879410259/2835898961106760056558689987142351593524400938062677157226805933962032322109217489031574673018955800377169571561217629537299831050940871022223014687565338965405060515961070655870545317217530444398287214314593884450942047250000000*y^9 - 1085841600036342955526428585287057872333515304871096736143068300216659706758013142090360294332975013284451991677992102715081614679209126750671947889050350355340511210727807902577608331001140026737167758587079488074952826811986924339/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^8 - 14162052600142824956111535461370056761650828447322016780577176490737600644861759836775209063205918709959825470422911184083359938940249451287474917202672181324753963492798395700985622555511894507498348451853168340257545128215645131/630199769134835568124153330476078131894311319569483812717067985324896071579826108673683260670879066750482127013603917674955518011320193560494003263903408658978902336880237923526787848270562320977397158736576418766876010500000000*y^7 + 196494661907134133382120070067375318237181176620623521602758743775519603412617653487337072493072803252976106655975781578450872144416741041798693484863672713583358964941443283946872329034740021504166028284803202344646910397764307159/11343595844427040226234759948569406374097603752250708628907223735848129288436869956126298692075823201508678286244870518149199324203763484088892058750261355861620242063844282623482181268870121777593148857258375537803768189000000000*y^6 + 258508954363994938482326879028319623779252115898170598896850246184501532217443023210480762245816073009196417113925837387171097744313739527672875435374883740834601994508980182622260745619105735308176630164809172302176811215768386733/11343595844427040226234759948569406374097603752250708628907223735848129288436869956126298692075823201508678286244870518149199324203763484088892058750261355861620242063844282623482181268870121777593148857258375537803768189000000000*y^5 + 84607012915339098589206613758305824398199481876084955777038738452126454095397260183551951976833103866474283000424487066183664306183056410886754265957091371660167438816590364034931717397011000842003400826199902206280734420186039107/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^4 - 130531415766444102148270008685297727653212693605578137918353205062227621228285612272160369178338749226752696902062402073936583334657227717685131489069799562953712334858839138518569600057818529831987688639980726471228255634169319343/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000*y^3 - 13259996356552863022082863575388823747850354862482279580708339187782651778890093316821203085271931678174253274130281078865545559306516618812940257660544005154194561287450588862329737694513083340004403031946146186913839893641185753/7562397229618026817489839965712937582731735834833805752604815823898752858957913304084199128050548801005785524163247012099466216135842322725928039166840903907746828042562855082321454179246747851728765904838917025202512126000000000*y^2 + 6311352310481973412569688671023034546121097604709232343739517640993208764343846395956344124588741696084737322487070089169161367712115646494967128626937994497599345859048670363967431787898099774442538905327992913033668174570980243/11343595844427040226234759948569406374097603752250708628907223735848129288436869956126298692075823201508678286244870518149199324203763484088892058750261355861620242063844282623482181268870121777593148857258375537803768189000000000*y + 2030580264954542968381795923036601968809154254950334800644673753338361509596528256607772973833921130141048099577504215692146315654845037449531601267294897537084839232215210968600648619264574787243143412378499902118668043551917421/22687191688854080452469519897138812748195207504501417257814447471696258576873739912252597384151646403017356572489741036298398648407526968177784117500522711723240484127688565246964362537740243555186297714516751075607536378000000000