# Manifold: Census Knot K8_180

# Number of Tetrahedra: 8

# Number Field
x^22 - 18*x^21 + 86*x^20 - 142*x^19 - 210*x^18 + 943*x^17 + 673*x^16 - 5421*x^15 - 1087*x^14 + 30822*x^13 + 36625*x^12 - 55338*x^11 - 168278*x^10 - 142166*x^9 + 1203*x^8 + 101755*x^7 + 100315*x^6 + 53721*x^5 + 18271*x^4 + 4001*x^3 + 531*x^2 + 37*x + 1 

# Approximate Field Generator
-0.282358556532930 + 0.349085488795961*I

# Shape Parameters
-547918537478343962880082238/5573133090059843218573034425*y^21 + 23622831126826274612191729237/11146266180119686437146068850*y^20 - 82958064961426868152489467447/5573133090059843218573034425*y^19 + 259276704476898027973993951264/5573133090059843218573034425*y^18 - 462341724214350030500549850317/11146266180119686437146068850*y^17 - 318615327850422926906972937839/2229253236023937287429213770*y^16 + 1587387634613198868836832786136/5573133090059843218573034425*y^15 + 7060475849050751579851977290533/11146266180119686437146068850*y^14 - 2048456021826976850767693861527/1114626618011968643714606885*y^13 - 29626484395982569129525031605837/11146266180119686437146068850*y^12 + 79003778967876843551267243849063/11146266180119686437146068850*y^11 + 78505634573800938022211337195713/5573133090059843218573034425*y^10 - 36059004792072150151524138040028/5573133090059843218573034425*y^9 - 80659877351255463377951212569719/2229253236023937287429213770*y^8 - 331068437787330924952867038226353/11146266180119686437146068850*y^7 + 37320000375131677654314510966417/11146266180119686437146068850*y^6 + 119369665158044491687898590499876/5573133090059843218573034425*y^5 + 96533978926407272471748520982928/5573133090059843218573034425*y^4 + 16416493661771931390448532800301/2229253236023937287429213770*y^3 + 10151660704729754305858726909782/5573133090059843218573034425*y^2 + 2672264664636546641952590853323/11146266180119686437146068850*y + 69002125260105656861857007393/5573133090059843218573034425

-10346961490489556648651564376/1114626618011968643714606885*y^21 + 371491893487111523376602530907/2229253236023937287429213770*y^20 - 1760617981843522773707709768833/2229253236023937287429213770*y^19 + 1416382464226237033429019793209/1114626618011968643714606885*y^18 + 4587928009787423902605291496481/2229253236023937287429213770*y^17 - 9747448630196291130674177232767/1114626618011968643714606885*y^16 - 15028080218183815918334029840859/2229253236023937287429213770*y^15 + 112592722920590943465353768945819/2229253236023937287429213770*y^14 + 28241536473883984126734543891667/2229253236023937287429213770*y^13 - 128550977469811735394932674738377/445850647204787457485842754*y^12 - 78766798842518964610607875041968/222925323602393728742921377*y^11 + 1141687098296267804434672649124281/2229253236023937287429213770*y^10 + 1782519440699732384433641940880909/1114626618011968643714606885*y^9 + 3039366684667961723472462068089543/2229253236023937287429213770*y^8 - 3960463754014173079897136438603/222925323602393728742921377*y^7 - 220168920087446575006566128324939/222925323602393728742921377*y^6 - 427636105811993448283557214929107/445850647204787457485842754*y^5 - 557168927334636852084956855521226/1114626618011968643714606885*y^4 - 359905976715985130475087382863121/2229253236023937287429213770*y^3 - 71317445294397744312598059714059/2229253236023937287429213770*y^2 - 1515727930259143404926143648283/445850647204787457485842754*y - 266932261827639617005065613239/2229253236023937287429213770

-13927551597216216680794158752228266723810391/9494910764988600250141120973767575740702907*y^21 + 2560706951128623672344054825090089147123932821/94949107649886002501411209737675757407029070*y^20 - 864506018010419836332107616674474384354920929/6329940509992400166760747315845050493801938*y^19 + 24812857216326439334036170640149623910285432349/94949107649886002501411209737675757407029070*y^18 + 229533042872446507276704902670211784561375737/1117048325292776500016602467502067734200342*y^17 - 3552482385411428869069667439860553017759005437/2434592503843230833369518198401942497616130*y^16 - 40040509705913789837725216984510919172568432451/94949107649886002501411209737675757407029070*y^15 + 768666172871997853930547261008900088395590086921/94949107649886002501411209737675757407029070*y^14 - 48487278371657161263461851447710984274306718567/31649702549962000833803736579225252469009690*y^13 - 704486134991584842779764246219030013683580391002/15824851274981000416901868289612626234504845*y^12 - 1736531804848315964109512171713816042610329793416/47474553824943001250705604868837878703514535*y^11 + 8994887416567563133377860492965947514681944523343/94949107649886002501411209737675757407029070*y^10 + 1993259086065087597704871161401682735080853230916/9494910764988600250141120973767575740702907*y^9 + 12230471375942550550646547377406445849584891152741/94949107649886002501411209737675757407029070*y^8 - 4661713348748979671768868449836651272960567746813/94949107649886002501411209737675757407029070*y^7 - 4092753390770977431477105541180280371073128451781/31649702549962000833803736579225252469009690*y^6 - 4664210859376213965733973212685394924256764956464/47474553824943001250705604868837878703514535*y^5 - 4015888572855953416274540038934846724540200847613/94949107649886002501411209737675757407029070*y^4 - 534491578307929896636435758284752490947388414826/47474553824943001250705604868837878703514535*y^3 - 27923075668602728224475209488314892837645074339/15824851274981000416901868289612626234504845*y^2 - 2209453600553581567012012795453015388196392472/15824851274981000416901868289612626234504845*y - 399504927282959511646011902429914900928752757/94949107649886002501411209737675757407029070

29517367079920173532725195448374812953734962/47474553824943001250705604868837878703514535*y^21 - 217516598168251170076231300483381642625009489/18989821529977200500282241947535151481405814*y^20 + 1846118367418551240674298469233300975765378647/31649702549962000833803736579225252469009690*y^19 - 1075288722870523766291866819558029996521180704/9494910764988600250141120973767575740702907*y^18 - 226865154028968612194376371410020979607312558/2792620813231941250041506168755169335500855*y^17 + 752588631374452490920172415209850122765619197/1217296251921615416684759099200971248808065*y^16 + 14558766412305015047884217125198365603112262389/94949107649886002501411209737675757407029070*y^15 - 324563533648723674278148470024042126542832503039/94949107649886002501411209737675757407029070*y^14 + 24660383839621999254478057988457318372801963409/31649702549962000833803736579225252469009690*y^13 + 593058203846767356345990807859759753548605187159/31649702549962000833803736579225252469009690*y^12 + 1409173268891581214699447321472507219006060712477/94949107649886002501411209737675757407029070*y^11 - 762268193852730712376579104912346110538850933515/18989821529977200500282241947535151481405814*y^10 - 8271570838663352573407576557591839345089839494971/94949107649886002501411209737675757407029070*y^9 - 5001940529310972813921482437266525089669196829537/94949107649886002501411209737675757407029070*y^8 + 1923818242998837749924388616680399646610652848773/94949107649886002501411209737675757407029070*y^7 + 1676267788220269003723753924217569926164673547151/31649702549962000833803736579225252469009690*y^6 + 3870344888290948764175735327533218621588989276903/94949107649886002501411209737675757407029070*y^5 + 853803414482947182303876325475763708125828371351/47474553824943001250705604868837878703514535*y^4 + 235199059853651254521325769410392314032203161617/47474553824943001250705604868837878703514535*y^3 + 12702332258781962653210836568276558855307836817/15824851274981000416901868289612626234504845*y^2 + 1976456839804776510774507713645029452042244849/31649702549962000833803736579225252469009690*y + 29648749356547652782208670085457939601722783/18989821529977200500282241947535151481405814

7816534759865363068974863304385993328705049/3164970254996200083380373657922525246900969*y^21 - 144313895467772126344289609901574688990192125/3164970254996200083380373657922525246900969*y^20 + 1476901631419280567804201470282195078606930161/6329940509992400166760747315845050493801938*y^19 - 1441570174566279337169271744493630148788112837/3164970254996200083380373657922525246900969*y^18 - 60420617091315552036851123249502769657104585/186174720882129416669433744583677955700057*y^17 + 1223815234934961687026067523625901331286359717/486918500768646166673903639680388499523226*y^16 + 1632465155406328267505964004004316231605598701/3164970254996200083380373657922525246900969*y^15 - 43689821865498532488368760073881484127699093273/3164970254996200083380373657922525246900969*y^14 + 23418488678675908705062610145651471084606541109/6329940509992400166760747315845050493801938*y^13 + 238529208495916724077327868758300913100508525784/3164970254996200083380373657922525246900969*y^12 + 349090077802203985110565602857714414243202487939/6329940509992400166760747315845050493801938*y^11 - 1059094180689937763584369892679945452625438359703/6329940509992400166760747315845050493801938*y^10 - 2158401108779220578276342349734142475126107687523/6329940509992400166760747315845050493801938*y^9 - 573297631892240047133662231451954957350571692615/3164970254996200083380373657922525246900969*y^8 + 341669832237342103825527731889850682267340093836/3164970254996200083380373657922525246900969*y^7 + 1324969209850441774062342560237298911161411238995/6329940509992400166760747315845050493801938*y^6 + 447189186250393979644261684868108217839602023588/3164970254996200083380373657922525246900969*y^5 + 345668018266206199769492274364103858866358292297/6329940509992400166760747315845050493801938*y^4 + 40987135021349449288418259082041019281272366414/3164970254996200083380373657922525246900969*y^3 + 11561475255134839276340544611690629753720211143/6329940509992400166760747315845050493801938*y^2 + 867181008413504543504581300575654817165560653/6329940509992400166760747315845050493801938*y + 19840590254594317693454149630465995915710408/3164970254996200083380373657922525246900969

-2116784330837828408064384103374556760225426021/94949107649886002501411209737675757407029070*y^21 + 19242550267985240156717417489462023295454216208/47474553824943001250705604868837878703514535*y^20 - 31501468217596846166922537548536871271174256569/15824851274981000416901868289612626234504845*y^19 + 167412491076426024287593454474916656800008946792/47474553824943001250705604868837878703514535*y^18 + 11285367277162839031839988804836855990233163757/2792620813231941250041506168755169335500855*y^17 - 26474401987388099486741348731822737045936402829/1217296251921615416684759099200971248808065*y^16 - 525467163162879919187718544971702869086245669091/47474553824943001250705604868837878703514535*y^15 + 5831435758561619314677430131034538764989550912411/47474553824943001250705604868837878703514535*y^14 + 63783497950759870770551317141808517096150059617/31649702549962000833803736579225252469009690*y^13 - 2175518000126044678127296802917464422090961269930/3164970254996200083380373657922525246900969*y^12 - 13145549204704396228873642434000682607093717338813/18989821529977200500282241947535151481405814*y^11 + 128964087824129293753349259320848527537489200310053/94949107649886002501411209737675757407029070*y^10 + 332848420032379244457746317859827613177984279167619/94949107649886002501411209737675757407029070*y^9 + 120435845163836451284655394593363282482397997863817/47474553824943001250705604868837878703514535*y^8 - 4587186512796916463914898090182595377100651121008/9494910764988600250141120973767575740702907*y^7 - 13799368682271874309541991083791125032616020481879/6329940509992400166760747315845050493801938*y^6 - 34996011557778726256284212247013431469693740956575/18989821529977200500282241947535151481405814*y^5 - 82199695448402373936039138545276676327074350949011/94949107649886002501411209737675757407029070*y^4 - 11955417018925757627461455076987319143241224281599/47474553824943001250705604868837878703514535*y^3 - 698405983767414921299676325284505208291257460607/15824851274981000416901868289612626234504845*y^2 - 25188815176794690729455148904800387591862428355/6329940509992400166760747315845050493801938*y - 11109799521316487193642713546906927775992644127/94949107649886002501411209737675757407029070

632378835287599276508758241177240606487610558/47474553824943001250705604868837878703514535*y^21 - 11520504001681784529045606854481543052717841858/47474553824943001250705604868837878703514535*y^20 + 56897672163249863216307187890570922482791434172/47474553824943001250705604868837878703514535*y^19 - 34091429029214828578236775466238580680159343929/15824851274981000416901868289612626234504845*y^18 - 12950401819982089117798787827596804665928040559/5585241626463882500083012337510338671001710*y^17 + 47646932501645995781136509598371903888963334977/3651888755764846250054277297602913746424195*y^16 + 580237040759428215721767639455681797833922277317/94949107649886002501411209737675757407029070*y^15 - 1162141521203065457639716978171354285471792039622/15824851274981000416901868289612626234504845*y^14 + 24205779384596788647527186220624574131684585539/15824851274981000416901868289612626234504845*y^13 + 1296577420703768125542471386979096939772047544266/3164970254996200083380373657922525246900969*y^12 + 7573568235057122243250791092733068224314743131745/18989821529977200500282241947535151481405814*y^11 - 38971294631286469956059477668802582505249946489289/47474553824943001250705604868837878703514535*y^10 - 97825345805083136026087759557640100155647673885412/47474553824943001250705604868837878703514535*y^9 - 68928218575777645417879859793323662709395256225522/47474553824943001250705604868837878703514535*y^8 + 1007446098574989250509617614843585368464059674565/3164970254996200083380373657922525246900969*y^7 + 8094988908105261916210356989066537268697958013055/6329940509992400166760747315845050493801938*y^6 + 20172135565034858886280773904170661581140424885409/18989821529977200500282241947535151481405814*y^5 + 46794897806733931023244775015466247773825083864261/94949107649886002501411209737675757407029070*y^4 + 13462925159134747129171212800382647214636024073553/94949107649886002501411209737675757407029070*y^3 + 2333451991582773589555464185317515308284434189157/94949107649886002501411209737675757407029070*y^2 + 41739183311163653450824391135154719061632821735/18989821529977200500282241947535151481405814*y + 2171511154677210650467485549285265629811208799/31649702549962000833803736579225252469009690

157640715706921993538978768276515456159143563/12659881019984800333521494631690100987603876*y^21 - 2870962747142564252172045003782674346485572549/12659881019984800333521494631690100987603876*y^20 + 3541705468377098106478970564043149661934075121/3164970254996200083380373657922525246900969*y^19 - 25405624235487914662066591122238396765523573361/12659881019984800333521494631690100987603876*y^18 - 1625576165572562248296756532516846330827853067/744698883528517666677734978334711822800228*y^17 + 11874044045107128319095906165206616123070054061/973837001537292333347807279360776999046452*y^16 + 73216197511057408695177747390482016012780110405/12659881019984800333521494631690100987603876*y^15 - 869201795820862576582455169443571115886520516955/12659881019984800333521494631690100987603876*y^14 + 13287638442268846754550317801023603893187573141/12659881019984800333521494631690100987603876*y^13 + 2425498296559176407750387649798515377716354728427/6329940509992400166760747315845050493801938*y^12 + 2372753748700682395240779853725101408234508439079/6329940509992400166760747315845050493801938*y^11 - 2425577640838087494875696212486784786067734885282/3164970254996200083380373657922525246900969*y^10 - 12223113356898182850477340351780908205555916024021/6329940509992400166760747315845050493801938*y^9 - 8642732111987004115040078849441362743326075632329/6329940509992400166760747315845050493801938*y^8 + 3722752605223758098614835854492468622598323511381/12659881019984800333521494631690100987603876*y^7 + 7585070396244332646384481355697032693242382946661/6329940509992400166760747315845050493801938*y^6 + 3157673154917890112775659558689013340172582800986/3164970254996200083380373657922525246900969*y^5 + 5874093078215245943999545833281099517756281175367/12659881019984800333521494631690100987603876*y^4 + 423800049686837693094904145995052229806407446568/3164970254996200083380373657922525246900969*y^3 + 147629390414364559132558545631897556675198482769/6329940509992400166760747315845050493801938*y^2 + 26595949107171009475109122143926127647623005807/12659881019984800333521494631690100987603876*y + 414680542357916841474126201657981698331786235/6329940509992400166760747315845050493801938


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

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

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

# f Combinatorial flattening
{-2, 2, 0, -2, -1, -1, 2, 1}

# f' Combinatorial flattening
{0, -2, 0, 0, 2, 0, 0, 0}

# 1 Loop Invariant
1230883417588805147317319043735527281267388027/63299405099924001667607473158450504938019380*y^21 - 22232147418723747834069974471867463649572630867/63299405099924001667607473158450504938019380*y^20 + 107203895333202052196684740739056577746151721163/63299405099924001667607473158450504938019380*y^19 - 180880371543741243365104270758179930190845393853/63299405099924001667607473158450504938019380*y^18 - 3678751615607762518303773527272046742504026047/930873604410647083347168722918389778500285*y^17 + 22734410259063132263174068971625511007884014627/1217296251921615416684759099200971248808065*y^16 + 378930788222282823412144587576331766506093917937/31649702549962000833803736579225252469009690*y^15 - 6750148828933773248418510514489277440061487207909/63299405099924001667607473158450504938019380*y^14 - 459758137708365555459731240105980592832907760211/31649702549962000833803736579225252469009690*y^13 + 3815974272086514345956681468254128330833520809617/6329940509992400166760747315845050493801938*y^12 + 2131910618786145964419720968635939622270927763642/3164970254996200083380373657922525246900969*y^11 - 71636711651774882138471611431485074152024485586191/63299405099924001667607473158450504938019380*y^10 - 203154460277298475789353371110339540937499243207503/63299405099924001667607473158450504938019380*y^9 - 40075433286087815809430033757918875544911627557527/15824851274981000416901868289612626234504845*y^8 + 2999024423644925697879902347965522003913965553853/12659881019984800333521494631690100987603876*y^7 + 6281611507037856025778226961465344060616220795359/3164970254996200083380373657922525246900969*y^6 + 22818116884329598155372505569687947589355750154273/12659881019984800333521494631690100987603876*y^5 + 56976728389972938078587563990045559137222574889957/63299405099924001667607473158450504938019380*y^4 + 17799096206995066083499032416949520870894451428311/63299405099924001667607473158450504938019380*y^3 + 1712016379248795327158791986745506629310973208997/31649702549962000833803736579225252469009690*y^2 + 70301050774584256657895342456027166647159554047/12659881019984800333521494631690100987603876*y + 10831563029179014750415350994112871539323643149/63299405099924001667607473158450504938019380

# 2 Loop Invariant
-892686936802719106328546451934396646766054978589675603647961669555172706019471120638605469638124877741947565181123/13915871070656819461296797962826989886330362499604488120366172852589697865436961795663933216694435021309910840404180*y^21 + 8384736411869849443254188578170452289481412567739831889875821900386302318093041141527111808053748717876056267981909/6957935535328409730648398981413494943165181249802244060183086426294848932718480897831966608347217510654955420202090*y^20 - 119497328579825167761821751285049279294641204588209772986724406637383448707823147939026911570054749668404985230680761/18554494760875759281729063950435986515107149999472650827154897136786263820582615727551910955592580028413214453872240*y^19 + 382572082561166413459040096155429716073365821946280435273889061853161772117906591448919074247704280931985840441065099/27831742141313638922593595925653979772660724999208976240732345705179395730873923591327866433388870042619821680808360*y^18 + 15759341780484975686622399676628018037977207611833468749015370464443487353378987445717907975018351124827340638345053/3274322604860428108540423050076938796783614705789291322439099494726987733043991010744454874516337652072920197742160*y^17 - 24390192777207453377584600836093491568543834799343881997093749409906567608599253339522883082830718322632947102914669/356817206939918447725558922123768971444368269220627900522209560322812765780434917837536749146011154392561816420620*y^16 + 200180098541381790304019298456930086893653419444692447450134253418478419942593008894832741705473573547796555859360203/27831742141313638922593595925653979772660724999208976240732345705179395730873923591327866433388870042619821680808360*y^15 + 20335407113539236736700203038916329414635742618605628096329813988066788132519853690727516935709710341184681691482023159/55663484282627277845187191851307959545321449998417952481464691410358791461747847182655732866777740085239643361616720*y^14 - 1956206150606479150205304391448165147188460958106849294883157029236324065458512952707184212428152105633942540108165453/9277247380437879640864531975217993257553574999736325413577448568393131910291307863775955477796290014206607226936120*y^13 - 1199888443136456394155995552803446885473940839199047723195119626770211105052573029391321219191158428362504510268449563/618483158695858642724302131681199550503571666649088360905163237892875460686087190918397031853086000947107148462408*y^12 - 8900056881936914927756880625431252577499164965425050472301440097553184148421045009790311517629585225162316457213435973/11132696856525455569037438370261591909064289999683590496292938282071758292349569436531146573355548017047928672323344*y^11 + 271792062874896796150725927012677576926924544597125465612801869824557273290786096517131494468879700310909118158677924341/55663484282627277845187191851307959545321449998417952481464691410358791461747847182655732866777740085239643361616720*y^10 + 209100610273854626180821807606037153738906237819410313768699924617585584386625002234485841347058960553015155629629632089/27831742141313638922593595925653979772660724999208976240732345705179395730873923591327866433388870042619821680808360*y^9 + 93209051964353351752893676492494475094640652923148698995998653126246966802036155956509276044332783614795968425354809763/55663484282627277845187191851307959545321449998417952481464691410358791461747847182655732866777740085239643361616720*y^8 - 51971709887459423306072273338868017103257687667780418502318865762625199937575424097180203084284367149123002407971953883/11132696856525455569037438370261591909064289999683590496292938282071758292349569436531146573355548017047928672323344*y^7 - 2169642439220739759978177247979696110576978466075442103404458089471262520212623490722341020749693352329581888069515263/463862369021893982043226598760899662877678749986816270678872428419656595514565393188797773889814500710330361346806*y^6 - 4849588118085836322950249088585444284390885166139587536892857985020431697329397431685097101475294388833476680761758095/2783174214131363892259359592565397977266072499920897624073234570517939573087392359132786643338887004261982168080836*y^5 - 158276589491188650703346114516831338876108110505693836514891525588179966220286728285230364758206829848637087497292133/13915871070656819461296797962826989886330362499604488120366172852589697865436961795663933216694435021309910840404180*y^4 + 6111254213997340569729781143261863498465068033172069620257042518331293002724225261173037636244912113356010808845260417/27831742141313638922593595925653979772660724999208976240732345705179395730873923591327866433388870042619821680808360*y^3 + 1445672538134324510448872608975397312542383205068654520678123955100294252750782147063117838208298028832022550207865567/18554494760875759281729063950435986515107149999472650827154897136786263820582615727551910955592580028413214453872240*y^2 + 37875642323175497518053262703481014447942310531171698945466261010029142913897012784060072613644207761683754329551713/3710898952175151856345812790087197303021429999894530165430979427357252764116523145510382191118516005682642890774448*y + 28889608530127579748198024564009671747247794676705218077961280018804995422750907178674680542446677534870256225074293/27831742141313638922593595925653979772660724999208976240732345705179395730873923591327866433388870042619821680808360

# 3 Loop Invariant
-782847862204421992221601554798503288573554471466252685748898872646611998608106639548244345167443966172494401180510058529282607433673899741952626134401/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^21 + 14517612595245218329456290456204343662987729664965642928073701376038737274170994811025933696962393640451395715094130038215995140247404396779041037817441/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^20 - 25058090688879569120031140606783583563465780471182154631098257884187700555731351863916697183670797796209162528543859134276665929873297139296969773933683/3866535472581161500498284090075548031807474938737474261440748994660446910160552415712520439410682990916693915974769710315661113391304264077427494151360*y^19 + 75519752145381298004985396625377604540260481082423398297274066967455081954468744025334871829374890324448313391965948591301717009056590761898677556152837/5799803208871742250747426135113322047711212408106211392161123491990670365240828623568780659116024486375040873962154565473491670086956396116141241227040*y^18 + 1290255762162677410092657010472983510150030418829454841703877831133737454066721501268735699118313780305348462337764468760408647940558857750760315157451/170582447319757125021983121620980060226800364944300335063562455646784422507083194810846489974000720187501202175357487219808578531969305768121801212560*y^17 - 10225417561217378861743413560284112797328401959523640331369231783288020157404690692320815090861906839208827678370203435937778628506954254721439286737679/148712902791583134634549388079828770454133651489902856209259576717709496544636631373558478438872422727565150614414219627525427438127087079901057467360*y^16 - 97874645092580123329187219291721255929508469994330787521768757467154571108252426137039412838602103142907182490377953781152341919052018069468346658271767/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^15 + 1089076643672673952997053660114001281355373913329799202281118468887408484830101087194357381256507136267608040947820683960788953984781738584733124392270723/2899901604435871125373713067556661023855606204053105696080561745995335182620414311784390329558012243187520436981077282736745835043478198058070620613520*y^14 - 63346657691195080468066636826471069428129019586798160138864187848897534295715702240100477983529592896577822794042320829092511301654151194082453388633211/483316934072645187562285511259443503975934367342184282680093624332555863770069051964065054926335373864586739496846213789457639173913033009678436768920*y^13 - 2733955335921650862208998191249661392411207528870328850777323664936305668590836210772164815422683552734934430121983786216776040231342935343221436087510/1342547039090681076561904197942898622155373242617178563000260067590432954916858477677958485906487149623852054157906149415160108816425091693551213247*y^12 - 3132542804547378226436736353551227277873622023309193870019926992287643369926153842674513133910844282187263065411935982857523513021137436014036254469076763/2319921283548696900298970454045328819084484963242484556864449396796268146096331449427512263646409794550016349584861826189396668034782558446456496490816*y^11 + 6696549228828877908472679200553162226693277554645855200736028499937109542760158123243343560648858346237063642567645408514684171253284565129237632509257751/1449950802217935562686856533778330511927803102026552848040280872997667591310207155892195164779006121593760218490538641368372917521739099029035310306760*y^10 + 103518670217513831857288205973117200904427931841300372860636111139080977342290349979090139231611054381223344110055234743599958657681389475279645273057987139/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^9 + 50844384922302755719936498638694955086963795191456997186425625382124731012023068672172995438245578145021951205707845537428963291440493101656989459916655609/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^8 - 7158617987015251745799174406590180971244993022726725833801313140311777548574799145407607184807172024741435656309862739714405328298191862747385578266263925/2319921283548696900298970454045328819084484963242484556864449396796268146096331449427512263646409794550016349584861826189396668034782558446456496490816*y^7 - 1399618359153039132867917917971219079999453160349073035668716040380631474515312766116475454499426342475162756813692235777744926306733903015631351140040665/257769031505410766699885606005036535453831662582498284096049932977363127344036827714168029294045532727779594398317980687710740892753617605161832943424*y^6 - 1027344778146608311353953176618269007358572566980974135585181821045030071114367958957133046574460166722956270848836582198247972137857586984618526842978455/289990160443587112537371306755666102385560620405310569608056174599533518262041431178439032955801224318752043698107728273674583504347819805807062061352*y^5 - 15351610293025718022805995141357864924246718812798556988005589917286209001533816864661303287491301226006896962572951249691796139568471012284880517611703171/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080*y^4 - 1761602654391032388599493496635668036427535335316852882564479779320991281115940398565232997315481156612883932893734464097874420046564142556243404004379449/5799803208871742250747426135113322047711212408106211392161123491990670365240828623568780659116024486375040873962154565473491670086956396116141241227040*y^3 - 156815903749687838765445411178906017261434484061584795974295323308609714930347734888639833954721046445392015941682603652311485429083533752198516365164769/3866535472581161500498284090075548031807474938737474261440748994660446910160552415712520439410682990916693915974769710315661113391304264077427494151360*y^2 - 2288457215129402238232683134875785160530053562802858753285803618538204168267535366150582416646102480528726698304769690339166815466229781978244927653029/773307094516232300099656818015109606361494987747494852288149798932089382032110483142504087882136598183338783194953942063132222678260852815485498830272*y - 592619702092931027249309092846658254519124664185493834409584031466983362294600114395122391302240986404447245408013101531018325059764593949606927951167/11599606417743484501494852270226644095422424816212422784322246983981340730481657247137561318232048972750081747924309130946983340173912792232282482454080

# 4 Loop Invariant
-624975969180255716674345416175657979418894268919118935631882091846005266834838750605765569477746554473197219472783486208989378058451024564918056821591951879839412347665932439269630770672947359885044165988802569639942790513/2400076489890878032249449956747946750697960513651015923797438773172932209667287830643719684813755678354299520540131486967142591896647643840653833528559486278547741809912268102412690414222760322904451050605067077964200330240*y^21 + 5757773233928904502947168223019835900826496613038744993105601019949513926959293037474744859215249894481577423324505354341492096178466746444595831824023099978040807883743447889117891785208841096708929111430032493287753100389/1200038244945439016124724978373973375348980256825507961898719386586466104833643915321859842406877839177149760270065743483571295948323821920326916764279743139273870904956134051206345207111380161452225525302533538982100165120*y^20 - 19547033480744038652843286541470236485728929814440940469589995769105972223378903053224381370517735042727282213387830673856113865477510390372569588820615693661425943846532148250409950687140676540036393954525003978834489274633/800025496630292677416483318915982250232653504550338641265812924390977403222429276881239894937918559451433173513377162322380863965549214613551277842853162092849247269970756034137563471407586774301483683535022359321400110080*y^19 + 56779638221623527603942236608369793317003127172174016371610762489867170294405601024776178965373405029508119364574107308771429350014680632324174435393155520823689689055251691504389099396970486983537841318210188809699430591321/1200038244945439016124724978373973375348980256825507961898719386586466104833643915321859842406877839177149760270065743483571295948323821920326916764279743139273870904956134051206345207111380161452225525302533538982100165120*y^18 + 4184470411300841832046258110417342804177050830304212881266915326846822251956975780664397358773906610081622327439747147875877284265741105935966261747709303249127061795251943851093069143823286329319867754648126334626511531135/120003824494543901612472497837397337534898025682550796189871938658646610483364391532185984240687783917714976027006574348357129594832382192032691676427974313927387090495613405120634520711138016145222552530253353898210016512*y^17 - 16067939639189845948725127719534021976156789598572492676413453146429527124395002386911692712436792020359364093081330570938186018016292337817680766514446404002188569895696772864542730332276057789099388985675668638629587352471/61540422817714821339729486070460173094819500350026049328139455722382877170956098221633838072147581496264090270259781717106220305042247277965482910988704776373019020766981233395197190108275905715498744887309412255492316160*y^16 - 3858661346893990690137650170117725995461488307965809808721596037919613328650954138878653392572066574602163611438453828320607274611820975758925198101818790826787671836827363687992732662856155033575615325321379782184304622609/60001912247271950806236248918698668767449012841275398094935969329323305241682195766092992120343891958857488013503287174178564797416191096016345838213987156963693545247806702560317260355569008072611276265126676949105008256*y^15 + 432707082944829312177606933841666933339850253829180562756773351251074431974055143888736086008873107460140453626670767336574955613202289664018597113998349710199835286567984377586733331139765797566110394149417936718025911078353/300009561236359754031181244593493343837245064206376990474679846646616526208410978830464960601719459794287440067516435870892823987080955480081729191069935784818467726239033512801586301777845040363056381325633384745525041280*y^14 - 265032652730687100702889145975813383015862743477785171266476877443757337360432045285698255016319564964676755286643493207464732372482426393145133984377190455482456659173982106482171989329563180488168460038840778670184867741087/800025496630292677416483318915982250232653504550338641265812924390977403222429276881239894937918559451433173513377162322380863965549214613551277842853162092849247269970756034137563471407586774301483683535022359321400110080*y^13 - 2107452708308342331885196417957581431658997894689692060622519966812713781576216297769385015595923287067971023311386897220908516680493135238640696798860477297984341501944640518606177494290880207375999425721663499085876776619727/266675165543430892472161106305327416744217834850112880421937641463659134407476425627079964979306186483811057837792387440793621321849738204517092614284387364283082423323585344712521157135862258100494561178340786440466703360*y^12 - 3697806351192847100727365874060484455555855649048159285197142985830165109657957322455483500759697291456940538027844049123981501157638472600066979021507964533062523182640939995282921002097130701943103765163350168710487174072149/600019122472719508062362489186986687674490128412753980949359693293233052416821957660929921203438919588574880135032871741785647974161910960163458382139871569636935452478067025603172603555690080726112762651266769491050082560*y^11 + 41104657528939237158888786205639572860573658230713514070414500479915847184117462627146802090884079261836484197669368267752845059172032581171485404264653422445983752661329846112716687679626737624603946392599754324050944116138149/2400076489890878032249449956747946750697960513651015923797438773172932209667287830643719684813755678354299520540131486967142591896647643840653833528559486278547741809912268102412690414222760322904451050605067077964200330240*y^10 + 87767224862149989136747901335797876118279791073120627306309763996277329378747617020680327876846467537909386853091695992088623381698299026191294787090550595232434934427292669734841379838631876354297142081504451945524989599233467/2400076489890878032249449956747946750697960513651015923797438773172932209667287830643719684813755678354299520540131486967142591896647643840653833528559486278547741809912268102412690414222760322904451050605067077964200330240*y^9 + 3184043222383278965671080234139119387057292697077431223036113465175885630362126364119128111912381652544347403217203044231834024925528307264140740466976041797327866103096658127449221856886405172594906551745477894321100761223733/150004780618179877015590622296746671918622532103188495237339923323308263104205489415232480300859729897143720033758217935446411993540477740040864595534967892409233863119516756400793150888922520181528190662816692372762520640*y^8 - 5823593120348251573376509006382208787806879852994999897336053022321269542971624728717316544626644624461877251662885219647462673079425502220501613012773539099717293096249209950221531382771272843975698365042532648916742072645981/600019122472719508062362489186986687674490128412753980949359693293233052416821957660929921203438919588574880135032871741785647974161910960163458382139871569636935452478067025603172603555690080726112762651266769491050082560*y^7 - 2247092840903011089136146162378801387429126490169030565765015120871211131100415039818674978669533307508650628730174903777544132369036260671980916037940413711513996575232617563539457519991854768422610811877148049984012688998819/100003187078786584677060414864497781279081688068792330158226615548872175402803659610154986867239819931429146689172145290297607995693651826693909730356645261606155908746344504267195433925948346787685460441877794915175013760*y^6 - 9828076187308828389676340018349563075922954496317076431259905346134654245375200548682640559699984485054652272250653073487587237787956645274217451684619117739293236278242759162966330034988074651506993893428168150265561842590457/600019122472719508062362489186986687674490128412753980949359693293233052416821957660929921203438919588574880135032871741785647974161910960163458382139871569636935452478067025603172603555690080726112762651266769491050082560*y^5 - 3269713366066047235731390864291554120524595752485247581173481200688430793616239558583511071255202259289399962546288245408429946623153952828404016556163975226352078895658676555421679439070599866877110784470956957072887368736275/480015297978175606449889991349589350139592102730203184759487754634586441933457566128743936962751135670859904108026297393428518379329528768130766705711897255709548361982453620482538082844552064580890210121013415592840066048*y^4 - 840904156235869212060179328118077679609475308455799403806682586326538646072280404876606285747763193884520455597609566873682779529677679492520554832207436512671128860642179245920524865490492429029959880254145715713321170175323/480015297978175606449889991349589350139592102730203184759487754634586441933457566128743936962751135670859904108026297393428518379329528768130766705711897255709548361982453620482538082844552064580890210121013415592840066048*y^3 - 10600068140965219274129630196665290743669292069022729264982456821002002093429989181199507720130278588278335432921533692548752460549110205647902165324877611917925196476964383172670038030358124926418164199328188586076656773841/40001274831514633870824165945799112511632675227516932063290646219548870161121463844061994746895927972571658675668858116119043198277460730677563892142658104642462363498537801706878173570379338715074184176751117966070005504*y^2 - 8046534832665269993912227460273717929000120313458223515384889535038372041684050690749538313960480301243140304490393818295307230383825835980914223597673202522452586486690163647208750647348910828144380022917611925690563288463/400012748315146338708241659457991125116326752275169320632906462195488701611214638440619947468959279725716586756688581161190431982774607306775638921426581046424623634985378017068781735703793387150741841767511179660700055040*y - 345797651045716936914350521253658563293737545609622019385392170652994470913632818685226397397451960683533856750532346581900130016074917497126885024170652200407075596007714560199865746875372648764858959224311998931297037781/600019122472719508062362489186986687674490128412753980949359693293233052416821957660929921203438919588574880135032871741785647974161910960163458382139871569636935452478067025603172603555690080726112762651266769491050082560