# Manifold: Census Knot K8_165

# Number of Tetrahedra: 8

# Number Field
x^21 + 22*x^20 + 203*x^19 + 1142*x^18 + 4664*x^17 + 13308*x^16 + 25062*x^15 + 31860*x^14 + 14207*x^13 + 26518*x^12 + 90432*x^11 + 105296*x^10 - 18804*x^9 - 48128*x^8 + 51694*x^7 + 87403*x^6 + 9668*x^5 - 33643*x^4 - 13655*x^3 + 5228*x^2 + 4384*x + 781 

# Approximate Field Generator
-0.558637645980997 + 0.514651399353272*I

# Shape Parameters
2158787656507520584972016337201818529313003807898137559215/18781826489368102333434407341044929853399867237231424036389347*y^20 + 48279437275787308030602064048495867687449143852681859358142/18781826489368102333434407341044929853399867237231424036389347*y^19 + 35043361634226059704171056241941677785356543072075193637955/1444755883797546333341108257003456142569220556710109541260719*y^18 + 2625712994851000436639867362397743367461679558698502416576707/18781826489368102333434407341044929853399867237231424036389347*y^17 + 844135188600959053166658414684009342288357584521182304020523/1444755883797546333341108257003456142569220556710109541260719*y^16 + 32436287005402924981986357038650021859641495794307660195475927/18781826489368102333434407341044929853399867237231424036389347*y^15 + 64719831947062857440265067244211547344496300259210102724139121/18781826489368102333434407341044929853399867237231424036389347*y^14 + 88865010107604055459770496886402578827671349777085717522011173/18781826489368102333434407341044929853399867237231424036389347*y^13 + 56166113770306744368716474841660341347738292308706925805221691/18781826489368102333434407341044929853399867237231424036389347*y^12 + 68156892546326598534785835522254927436222146113028811993278089/18781826489368102333434407341044929853399867237231424036389347*y^11 + 214075124352540690268641714295913260370692156370307932781755471/18781826489368102333434407341044929853399867237231424036389347*y^10 + 296554223068797724909161738487936703223561341453108148654149875/18781826489368102333434407341044929853399867237231424036389347*y^9 + 46265168306966337460552978745142107653817875508636888689098657/18781826489368102333434407341044929853399867237231424036389347*y^8 - 115192210853432065524494051435594128447318601464459403587831759/18781826489368102333434407341044929853399867237231424036389347*y^7 + 58936753753918852593881363569540186927292521652515778087659538/18781826489368102333434407341044929853399867237231424036389347*y^6 + 219826378468491700284055002384683529220607329653219386178273553/18781826489368102333434407341044929853399867237231424036389347*y^5 + 103498511086808826593877203559940837519818368235312439127124045/18781826489368102333434407341044929853399867237231424036389347*y^4 - 3838473389081010406584510699994490881122247329539563054839547/1444755883797546333341108257003456142569220556710109541260719*y^3 - 71741253833367974328577481124284334398665151382590928413302064/18781826489368102333434407341044929853399867237231424036389347*y^2 - 12880900269416732176454228510755337922087504632339463518523670/18781826489368102333434407341044929853399867237231424036389347*y + 34039259087569496991906602528952274782037890154111008014218062/18781826489368102333434407341044929853399867237231424036389347

75929009978315191791881487499369766098670202571342898714969358/161354671370161367146534993466916992370558259435055163896620880077*y^20 + 148333626065463675908800762845601947272578560822333957371378084/14668606488196487922412272133356090215505296312277742172420080007*y^19 + 1118626119936814197466584002227682011019412060057216172707376205/12411897797704720549733461035916691720812173802696551068970836929*y^18 + 78426189190624402024847136654083417748385297374289541627983317658/161354671370161367146534993466916992370558259435055163896620880077*y^17 + 2139480550493920305444188898986555768246416514968985251328046841/1128354345245883686339405548719699247346561254790595551724621539*y^16 + 807090260260236857058924402826683176991258105719321659473607062299/161354671370161367146534993466916992370558259435055163896620880077*y^15 + 1292728324867902423630953615308546080624045110363251361842064182771/161354671370161367146534993466916992370558259435055163896620880077*y^14 + 1168826159541085176720166827609602722879257797630851673295477905999/161354671370161367146534993466916992370558259435055163896620880077*y^13 - 712443714593577450249313770980073149004796108106311297382668610125/161354671370161367146534993466916992370558259435055163896620880077*y^12 + 699264480640676240162155318101320543409005121000303080060279561137/161354671370161367146534993466916992370558259435055163896620880077*y^11 + 5355830497692747887880656081532375447933343625149588775597430202139/161354671370161367146534993466916992370558259435055163896620880077*y^10 + 3903587298785319833821597531004027930444299031336457737323855654105/161354671370161367146534993466916992370558259435055163896620880077*y^9 - 7349038867752102101323472458098866466178965559642288176832548436985/161354671370161367146534993466916992370558259435055163896620880077*y^8 - 5473008992595908322934396915115941704012976067178387129368931472541/161354671370161367146534993466916992370558259435055163896620880077*y^7 + 5393452502028662096152305785961167401699026561177127237166046496021/161354671370161367146534993466916992370558259435055163896620880077*y^6 + 5621949346666827931062283502303367357705959237265305892747963022155/161354671370161367146534993466916992370558259435055163896620880077*y^5 - 3160712574995646848452069090309540534218980805505850547796883443470/161354671370161367146534993466916992370558259435055163896620880077*y^4 - 370601564743159017108574365191537624766951677995328798051774484381/12411897797704720549733461035916691720812173802696551068970836929*y^3 - 621683319514931563789850029439260425348711204455689940502320487949/161354671370161367146534993466916992370558259435055163896620880077*y^2 + 1355030672102061634244233401616220805864076593686395831131604660785/161354671370161367146534993466916992370558259435055163896620880077*y + 746521047534183043300690685033327537542298340425812315877398872240/161354671370161367146534993466916992370558259435055163896620880077

7391776716756527572894230011495035422925259002290675337235/131472785425576716334040851387314508973799070660619968254725429*y^20 + 22952354936987869752757900203606323247654701176186776959164/18781826489368102333434407341044929853399867237231424036389347*y^19 + 208596131818594488453940079355768559667467282178338891209748/18781826489368102333434407341044929853399867237231424036389347*y^18 + 8098477572394333241523814157499905795583954180261229811853678/131472785425576716334040851387314508973799070660619968254725429*y^17 + 32694713880176517208473070764746086477592227848400647254527451/131472785425576716334040851387314508973799070660619968254725429*y^16 + 13079232808536639041320549572622965777672282547599599239884785/18781826489368102333434407341044929853399867237231424036389347*y^15 + 167829990784763929731205045402593254708743951112514029647656831/131472785425576716334040851387314508973799070660619968254725429*y^14 + 207433202144234716488665753650256762472220531245551233981512669/131472785425576716334040851387314508973799070660619968254725429*y^13 + 72453355584932083168676378789009063849494249946504243227054365/131472785425576716334040851387314508973799070660619968254725429*y^12 + 194023459730503006756300847012238297107279042203532909189564141/131472785425576716334040851387314508973799070660619968254725429*y^11 + 84673404451416936938633169003738032817939236101804977310351759/18781826489368102333434407341044929853399867237231424036389347*y^10 + 679615101483104562664829660257406353859523162880810350259391632/131472785425576716334040851387314508973799070660619968254725429*y^9 - 16852184494711044202716055603804481658397037490073660290923295/10113291186582824333387757799024192997984543896970766788825033*y^8 - 265211564009616572526675894581302966615774739651520163406596940/131472785425576716334040851387314508973799070660619968254725429*y^7 + 254947049336106162378980592992104040415627676326383144107150154/131472785425576716334040851387314508973799070660619968254725429*y^6 + 630784490572331993321349508435868575404771676338145271262726629/131472785425576716334040851387314508973799070660619968254725429*y^5 + 7317656125472771005401753017255681491598748987820208972337031/131472785425576716334040851387314508973799070660619968254725429*y^4 - 177937371716524805572988998803881006175331271151572927129881467/131472785425576716334040851387314508973799070660619968254725429*y^3 - 295929340641999487880475462832689899609732499180150418142986463/131472785425576716334040851387314508973799070660619968254725429*y^2 + 69610723181896572753048677400351896014156927269057625245986904/131472785425576716334040851387314508973799070660619968254725429*y + 124359243095341411702061238648283482049077288274045440743471217/131472785425576716334040851387314508973799070660619968254725429

15257432598201394658472195187907344928638022916879583977828715/14668606488196487922412272133356090215505296312277742172420080007*y^20 + 30361591272790755355411377215873360741694822563398400188953165/1333509680745135265673842921214190019591390573843431106583643637*y^19 + 235350198224807171392150416240255057526893913136739308872347711/1128354345245883686339405548719699247346561254790595551724621539*y^18 + 17068192776473695515798798170565754053949897189265705461674235415/14668606488196487922412272133356090215505296312277742172420080007*y^17 + 483286599923305408014675398226344190050210959083796148847879151/102577667749625789667218686247245386122414659526417777429511049*y^16 + 194475408446998622848146890676384199458061114422189939644224169201/14668606488196487922412272133356090215505296312277742172420080007*y^15 + 357049035624903668519698810952148211529146122127481851039676556343/14668606488196487922412272133356090215505296312277742172420080007*y^14 + 435555613828040342158077121168998790950355799629340455306070206399/14668606488196487922412272133356090215505296312277742172420080007*y^13 + 147358772028608446598833718966319235336749067404204304188321827892/14668606488196487922412272133356090215505296312277742172420080007*y^12 + 360730862784495016201398105141590246225039485416712698870183723699/14668606488196487922412272133356090215505296312277742172420080007*y^11 + 1326529611641867448299289817689955918258904192304979036116256167371/14668606488196487922412272133356090215505296312277742172420080007*y^10 + 1439353950740879772858679085640783535256358686930542179026901351789/14668606488196487922412272133356090215505296312277742172420080007*y^9 - 518509610793310048311966476072488279255710790603881161217982209235/14668606488196487922412272133356090215505296312277742172420080007*y^8 - 770442812533977431679641686403560682803122527715826027751126446637/14668606488196487922412272133356090215505296312277742172420080007*y^7 + 878682837407953338649691512214881303058369784408916008351974196989/14668606488196487922412272133356090215505296312277742172420080007*y^6 + 1287515776698785873458623931060854782807533657593411455727701077967/14668606488196487922412272133356090215505296312277742172420080007*y^5 - 24175543224480934363737773785749625551221918898772522707583628273/14668606488196487922412272133356090215505296312277742172420080007*y^4 - 45702934004622093389599858360544661502857473121873758363413487530/1128354345245883686339405548719699247346561254790595551724621539*y^3 - 169368221809100545403385288153830729084518025793175535521465182634/14668606488196487922412272133356090215505296312277742172420080007*y^2 + 135795776867257279225111649200445664452277067039249980126877434004/14668606488196487922412272133356090215505296312277742172420080007*y + 76948567620929382012552856170685719084299433585457217166768072830/14668606488196487922412272133356090215505296312277742172420080007

7391776716756527572894230011495035422925259002290675337235/131472785425576716334040851387314508973799070660619968254725429*y^20 + 22952354936987869752757900203606323247654701176186776959164/18781826489368102333434407341044929853399867237231424036389347*y^19 + 208596131818594488453940079355768559667467282178338891209748/18781826489368102333434407341044929853399867237231424036389347*y^18 + 8098477572394333241523814157499905795583954180261229811853678/131472785425576716334040851387314508973799070660619968254725429*y^17 + 32694713880176517208473070764746086477592227848400647254527451/131472785425576716334040851387314508973799070660619968254725429*y^16 + 13079232808536639041320549572622965777672282547599599239884785/18781826489368102333434407341044929853399867237231424036389347*y^15 + 167829990784763929731205045402593254708743951112514029647656831/131472785425576716334040851387314508973799070660619968254725429*y^14 + 207433202144234716488665753650256762472220531245551233981512669/131472785425576716334040851387314508973799070660619968254725429*y^13 + 72453355584932083168676378789009063849494249946504243227054365/131472785425576716334040851387314508973799070660619968254725429*y^12 + 194023459730503006756300847012238297107279042203532909189564141/131472785425576716334040851387314508973799070660619968254725429*y^11 + 84673404451416936938633169003738032817939236101804977310351759/18781826489368102333434407341044929853399867237231424036389347*y^10 + 679615101483104562664829660257406353859523162880810350259391632/131472785425576716334040851387314508973799070660619968254725429*y^9 - 16852184494711044202716055603804481658397037490073660290923295/10113291186582824333387757799024192997984543896970766788825033*y^8 - 265211564009616572526675894581302966615774739651520163406596940/131472785425576716334040851387314508973799070660619968254725429*y^7 + 254947049336106162378980592992104040415627676326383144107150154/131472785425576716334040851387314508973799070660619968254725429*y^6 + 630784490572331993321349508435868575404771676338145271262726629/131472785425576716334040851387314508973799070660619968254725429*y^5 + 7317656125472771005401753017255681491598748987820208972337031/131472785425576716334040851387314508973799070660619968254725429*y^4 - 177937371716524805572988998803881006175331271151572927129881467/131472785425576716334040851387314508973799070660619968254725429*y^3 - 295929340641999487880475462832689899609732499180150418142986463/131472785425576716334040851387314508973799070660619968254725429*y^2 + 69610723181896572753048677400351896014156927269057625245986904/131472785425576716334040851387314508973799070660619968254725429*y + 124359243095341411702061238648283482049077288274045440743471217/131472785425576716334040851387314508973799070660619968254725429

-2252384310630849727647649210312728331855377714228624558609/18781826489368102333434407341044929853399867237231424036389347*y^20 - 49504504953958934452059061543586608202032696010264631477106/18781826489368102333434407341044929853399867237231424036389347*y^19 - 35093054995535439358244057069763304942185299141257454882975/1444755883797546333341108257003456142569220556710109541260719*y^18 - 2562800332769404443081958081898105900293674325902007909340772/18781826489368102333434407341044929853399867237231424036389347*y^17 - 803731734780801700670930949436843299167929575552588611538885/1444755883797546333341108257003456142569220556710109541260719*y^16 - 29711274309070552690354461976052443278340183146353348307366076/18781826489368102333434407341044929853399867237231424036389347*y^15 - 55538504568126432520220283421300830864208700937582074147257577/18781826489368102333434407341044929853399867237231424036389347*y^14 - 69315854413072488869887460179686030544673156757525496487849226/18781826489368102333434407341044929853399867237231424036389347*y^13 - 26719553473972662514910076523329735384264061399794496496668934/18781826489368102333434407341044929853399867237231424036389347*y^12 - 52443197444375663443406709142537718076551310489488254227188023/18781826489368102333434407341044929853399867237231424036389347*y^11 - 195573251241068168139536801955061534057763804612082600655986829/18781826489368102333434407341044929853399867237231424036389347*y^10 - 234609626607294207590475856581235452051102691410666725001247086/18781826489368102333434407341044929853399867237231424036389347*y^9 + 47597591530455511930637351331041946043812587273887254486965803/18781826489368102333434407341044929853399867237231424036389347*y^8 + 147292884649153794115399287114855427884418254692350641539827134/18781826489368102333434407341044929853399867237231424036389347*y^7 - 99599631879600612284575303413341298133053320326907856180342139/18781826489368102333434407341044929853399867237231424036389347*y^6 - 231087875582258214989666474855266970067622264184214444427890806/18781826489368102333434407341044929853399867237231424036389347*y^5 - 40810530681110249097120739719895826657399045836136059996876841/18781826489368102333434407341044929853399867237231424036389347*y^4 + 10444688303754003559521449656576519645002126498880893309055228/1444755883797546333341108257003456142569220556710109541260719*y^3 + 2197546112746203957460117892401255231580289148516075801671539/18781826489368102333434407341044929853399867237231424036389347*y^2 - 24780284554823162964484287018997349316425985876999815433348847/18781826489368102333434407341044929853399867237231424036389347*y + 5039998052098586407272608879469676157063639022336487929559089/18781826489368102333434407341044929853399867237231424036389347

-10843731676136452308786742184051919082276371624975412919403994/14668606488196487922412272133356090215505296312277742172420080007*y^20 - 21463941600561427996715974183260208248850452846915912918652426/1333509680745135265673842921214190019591390573843431106583643637*y^19 - 165151171289300705627940393287010907606799884093141654165111955/1128354345245883686339405548719699247346561254790595551724621539*y^18 - 11879585193098475881630612832164928481142958063022377721207171919/14668606488196487922412272133356090215505296312277742172420080007*y^17 - 333728839925369972621301164157832947698835456717349937149479390/102577667749625789667218686247245386122414659526417777429511049*y^16 - 132599912406436448698178267536396431201249067553068683949857954267/14668606488196487922412272133356090215505296312277742172420080007*y^15 - 238100661078342666042339207653313272061189744268923689461256185930/14668606488196487922412272133356090215505296312277742172420080007*y^14 - 281337581486125778377763425414271437944583174054110752902865728570/14668606488196487922412272133356090215505296312277742172420080007*y^13 - 71663879115201121265678929139874299207634083893599834222367237598/14668606488196487922412272133356090215505296312277742172420080007*y^12 - 249007231811937983436055461453761827887594836271022595658017098158/14668606488196487922412272133356090215505296312277742172420080007*y^11 - 916678076322048845281492320036170321899485726908414295030256382633/14668606488196487922412272133356090215505296312277742172420080007*y^10 - 916546718182901812920067675511100237300470875224913074820390739865/14668606488196487922412272133356090215505296312277742172420080007*y^9 + 487275662947300955183191223020352248487871684502174230294313413924/14668606488196487922412272133356090215505296312277742172420080007*y^8 + 485650055678072412445608753794110127502456196177800890249870065536/14668606488196487922412272133356090215505296312277742172420080007*y^7 - 709509855474719411701168696055328666563388240097052085530403664817/14668606488196487922412272133356090215505296312277742172420080007*y^6 - 824466384083583517511564922705418882295001326024138198029345826160/14668606488196487922412272133356090215505296312277742172420080007*y^5 + 162014803385839639936637160180461306400057464882155266848600726291/14668606488196487922412272133356090215505296312277742172420080007*y^4 + 29281626404983731096118301105108778009322304564064636982772258433/1128354345245883686339405548719699247346561254790595551724621539*y^3 + 26915742150732355610947827617646382895299219786224835871809463258/14668606488196487922412272133356090215505296312277742172420080007*y^2 - 80335928237288479444982787780387822614490318669750607488907580590/14668606488196487922412272133356090215505296312277742172420080007*y - 21175877548659298491623835803675726824002657290678598377238483333/14668606488196487922412272133356090215505296312277742172420080007

15197048400269652022536541582242746860648304045912931200727/18781826489368102333434407341044929853399867237231424036389347*y^20 + 332777216978482729181503005696213717446368846617056842375042/18781826489368102333434407341044929853399867237231424036389347*y^19 + 234233139080149361246244397787658520666933133860895123217413/1444755883797546333341108257003456142569220556710109541260719*y^18 + 16920635802751840975075409030701474281192761125545983201671168/18781826489368102333434407341044929853399867237231424036389347*y^17 + 5238157744578019394323065186750616639744785634823114877225117/1444755883797546333341108257003456142569220556710109541260719*y^16 + 189810050055494390804249385314920736515674261351473868519107086/18781826489368102333434407341044929853399867237231424036389347*y^15 + 340702866937466890905180701279642122595972865474918734690771673/18781826489368102333434407341044929853399867237231424036389347*y^14 + 397015471163471587223717540068512013485458552575935730041277914/18781826489368102333434407341044929853399867237231424036389347*y^13 + 96106107944627653236134781675113933071783869323084023188306757/18781826489368102333434407341044929853399867237231424036389347*y^12 + 317126297826860207472617645835840909852163209375244974222450936/18781826489368102333434407341044929853399867237231424036389347*y^11 + 1374194243235067763388201779832342210060803982465390269616113892/18781826489368102333434407341044929853399867237231424036389347*y^10 + 1291835566774285139730665067192505595533073088482516608337829165/18781826489368102333434407341044929853399867237231424036389347*y^9 - 783557848558858460815899634249604230512034662477848067170325249/18781826489368102333434407341044929853399867237231424036389347*y^8 - 778336966690842681358488741139508569033833542134977240479318547/18781826489368102333434407341044929853399867237231424036389347*y^7 + 1284223953624715351865069316922252796104717491552674380623926784/18781826489368102333434407341044929853399867237231424036389347*y^6 + 1046309803157540324546189254160167736029839385475361486859402106/18781826489368102333434407341044929853399867237231424036389347*y^5 - 294835684049258110057798766626545776479814425650849408533302922/18781826489368102333434407341044929853399867237231424036389347*y^4 - 39618101496913941557863550785369675413420370552258445023483631/1444755883797546333341108257003456142569220556710109541260719*y^3 + 8313651901017221845963338690692135882700555050919544684554353/18781826489368102333434407341044929853399867237231424036389347*y^2 + 107719613794120388190238392628767098296375566889047758526066254/18781826489368102333434407341044929853399867237231424036389347*y + 46615333186939226619751777429050298904842428899418524312753214/18781826489368102333434407341044929853399867237231424036389347


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

# 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,0},{0,0,0,0,0,1,1,1},{0,0,0,0,0,0,2,1},{0,0,0,0,0,0,0,2}}

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

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

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

# 1 Loop Invariant
2512318283861639392242855299296946316318017869489482413570149/37563652978736204666868814682089859706799734474462848072778694*y^20 + 26992911135378724950643474479572031352024012713041199608012766/18781826489368102333434407341044929853399867237231424036389347*y^19 + 18550941385515384942883642874855209804046075056448760206425611/1444755883797546333341108257003456142569220556710109541260719*y^18 + 1310537101200250478742337371850516321610701106224246440522187514/18781826489368102333434407341044929853399867237231424036389347*y^17 + 398678625372018453358580616721688409583133399119425937876758427/1444755883797546333341108257003456142569220556710109541260719*y^16 + 28073053546019339434628062154401463204583172533651066793548108873/37563652978736204666868814682089859706799734474462848072778694*y^15 + 48376936636025983427351630531633171211103411299055250966941008415/37563652978736204666868814682089859706799734474462848072778694*y^14 + 27351680071832537245308198301094186595941469970340855491469872662/18781826489368102333434407341044929853399867237231424036389347*y^13 + 6740678329304032742189480411803262927359634410628741702561147839/37563652978736204666868814682089859706799734474462848072778694*y^12 + 31053922751331789328027532927974297158529078961842583463370298910/18781826489368102333434407341044929853399867237231424036389347*y^11 + 97684255322098961250514170483344894671877920089071792714176434768/18781826489368102333434407341044929853399867237231424036389347*y^10 + 162706383526298637249543214973494596117617730294737254730178795969/37563652978736204666868814682089859706799734474462848072778694*y^9 - 134871766708394488301715230528074406652066306893176220230393668439/37563652978736204666868814682089859706799734474462848072778694*y^8 - 54347953446202569390841312190841104452029392523080798574858642537/37563652978736204666868814682089859706799734474462848072778694*y^7 + 160770083583976907827643617942505655487061200497645798768173133527/37563652978736204666868814682089859706799734474462848072778694*y^6 + 135754178571578600228642367343347048848655907348655895885197806017/37563652978736204666868814682089859706799734474462848072778694*y^5 - 49201282194087825929522253185418777045682122482069346265857099779/37563652978736204666868814682089859706799734474462848072778694*y^4 - 4629735034353841314969563008109080524507840966762731866132167135/2889511767595092666682216514006912285138441113420219082521438*y^3 - 1612738531373451921694888647532350420654099279994979846303812483/18781826489368102333434407341044929853399867237231424036389347*y^2 + 7275597454872542452232629824496442843218472839762151966202419823/18781826489368102333434407341044929853399867237231424036389347*y + 1726476059201077503259156192693645205388559613638778572049646821/18781826489368102333434407341044929853399867237231424036389347

# 2 Loop Invariant
617816881663478468813706960295026670180546022184395159745544823957478994700220953947911363470295352568434550929039125370593/1834692438619244582369510261413698122314196108009504679217036219270694796036279438320897960615280826829900373718321439303469452*y^20 + 39760579903230894619134118910854027268724205332607010647879428631844213091756141155841330682258044343521008691220925486806249/5504077315857733747108530784241094366942588324028514037651108657812084388108838314962693881845842480489701121154964317910408356*y^19 + 27266577231328342208396791549100626254411949062164130555916139780295443216596888069149468146185308912489730061380890749478157/423390562758287211316040829557007258995583717232962618280854512139391106777602947304822606295834036960746240088843409070031412*y^18 + 640783804447801889949263851560952699123580320164216412927452715292494676487634127955340840128584550206256735655753652922567143/1834692438619244582369510261413698122314196108009504679217036219270694796036279438320897960615280826829900373718321439303469452*y^17 + 48654266198860106922244802516507459986477132800046344252672311825290966600033055291409982162260388125426764292133765556739602/35282546896523934276336735796417271582965309769413551523404542678282592231466912275401883857986169746728853340736950755835951*y^16 + 20498180714398554093095199724142715208637985475457156081632248775210989726796735870383503571563008456486551879412394322956134973/5504077315857733747108530784241094366942588324028514037651108657812084388108838314962693881845842480489701121154964317910408356*y^15 + 8793633981214751576572971454741057499984880216177990496380221047710880433622762527989990064234705868491567791377706699396835312/1376019328964433436777132696060273591735647081007128509412777164453021097027209578740673470461460620122425280288741079477602089*y^14 + 13202941660026379910692644508302076819191055923536269476195015493377068820293372649977286567369344392850764273166603228723264675/1834692438619244582369510261413698122314196108009504679217036219270694796036279438320897960615280826829900373718321439303469452*y^13 + 697375733988079981258209870110320197631378999479061754445536483209236186433918621269917602411398077455139985334847826435246999/917346219309622291184755130706849061157098054004752339608518109635347398018139719160448980307640413414950186859160719651734726*y^12 + 15348170191809867690636692726328710119502482134124540403539947651266414290043684681302633845549722272103309623773600130848420587/1834692438619244582369510261413698122314196108009504679217036219270694796036279438320897960615280826829900373718321439303469452*y^11 + 141367945393263527143313910080409520077964162566002365797875842472948525666792388303391847323880760074457179511007794164289514141/5504077315857733747108530784241094366942588324028514037651108657812084388108838314962693881845842480489701121154964317910408356*y^10 + 58470902550322610713451657827860881516304990156515762140573497407904925055009440218576399744146514108852215010784855253535302749/2752038657928866873554265392120547183471294162014257018825554328906042194054419157481346940922921240244850560577482158955204178*y^9 - 25111428980706797803769540602740116744926762701816535496086831956910452878072199646800768870385918048171517975338551419532576773/1376019328964433436777132696060273591735647081007128509412777164453021097027209578740673470461460620122425280288741079477602089*y^8 - 18673215405096536369257110098750471299241873919911589978108070630277221009774922645232516789494994298676864676883590401489374715/2752038657928866873554265392120547183471294162014257018825554328906042194054419157481346940922921240244850560577482158955204178*y^7 + 113109485010503973883138982478493893887336942335025830049063061424829400133384425036577909367084658037710769858187905582071411557/5504077315857733747108530784241094366942588324028514037651108657812084388108838314962693881845842480489701121154964317910408356*y^6 + 24826479316072398407684199025333401113414410675169980526769233529191582119114276122173324407138388625514201065332774342120599993/1376019328964433436777132696060273591735647081007128509412777164453021097027209578740673470461460620122425280288741079477602089*y^5 - 37295023157286563582547936465023892932057815208284800151022855404978109531085422711309906629300522289867846238766502336441584181/5504077315857733747108530784241094366942588324028514037651108657812084388108838314962693881845842480489701121154964317910408356*y^4 - 852952254189192672660423302592540016584206764150922933028144039871180141950155180453458401382593165564257048072246732364539548/105847640689571802829010207389251814748895929308240654570213628034847776694400736826205651573958509240186560022210852267507853*y^3 - 2142359084967191804373771635952201884466605382136971132497057317657683278846860163278604287513071759896172315253337660196953005/2752038657928866873554265392120547183471294162014257018825554328906042194054419157481346940922921240244850560577482158955204178*y^2 + 870156058129549914481472216012123100788300372803754610525233406204477314999809428349984714081845584758013949858288262311772590/458673109654811145592377565353424530578549027002376169804259054817673699009069859580224490153820206707475093429580359825867363*y + 169879338174111267976223337141430211920949325947727168582882899425814625269923747833487822741367673434167920235865522610263490/458673109654811145592377565353424530578549027002376169804259054817673699009069859580224490153820206707475093429580359825867363

# 3 Loop Invariant
-6468618379516583465307792846432736458755354759193602797302400666182522060155995541115827482407203515062890890094505330044567384167217945419953685765670238/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^20 - 139376058377648852142849610781183605281617491151555953819799473257295998648499426236786050038730071031143264365961195960451954007634784242647764657888942012/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^19 - 192271369399214666144355275100484964019666571682465207393434883923335759935777996817736012348315561998812789647527311920545599127084874870635820483015848255/11027387883051662821820489755954935716507020327378442499280100760780478110765350271568109087973586080160058803535018063808296164866764218623217373231029472546*y^18 - 6816958866590540849166552007745544178273972335389389424597342180720372681483937796311850731279592340455314196489794935941773375672549822941593039201107960281/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^17 - 4161069372843809775061944006270631163885103306200781549169104930021144567336651910220870842594335877483733558424014745191333490911863513580495633394722022883/11027387883051662821820489755954935716507020327378442499280100760780478110765350271568109087973586080160058803535018063808296164866764218623217373231029472546*y^16 - 147290350049859882808634131556856296572106775393354117242022359934827443613198917214178793302586046551021409659977254961954392000421142784521260949392106905819/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y^15 - 128014098651927822684925622697384888327144693523859016257030526951501206967983343845401474573260271006618446065674773736977035659621853332191825729410213737086/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^14 - 292078726440152843330155016238271732814854367038932389710751925761102792643417480775925384596387354621619689757760781853220414890607917601718417795644318046491/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y^13 - 21890366644345985308797556437890888771042718083705326667421751401742508026185156108248718688424191378085367642669652469720747050737727508982976652384262301863/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^12 - 156524787367450635733093424210399119749598821171154286389871345532586514047155704488184071122928482668895055510937437655414511714466657163705761181018676060412/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^11 - 511003928248784220452150383617568072123764438227782684522092257254030223469826249103807282862356893485424443716919562071980099853267480893956276885320356336216/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^10 - 443016247446910572468857180060373043038843440825407278813754359325585469104128377114339040687941519292645620434551340942135515429570588451721399560772233918232/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^9 + 6542106219888271422862230829192256520508344211723624535848775664295781837752155203049174923035012632139271971495625802573006703206409023929282180693302151609/1391806237666714725084139483761302566161080235494366529035352523205303062523782073110538040229675913029910334426749852713668447992892571282541998563139642166*y^8 + 349082216348393369647694367966551834961515221417207472534441631280181451493057805462391964693641889310908430028653402760034571074084659681740551752810990957421/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y^7 - 413023520552131677987935555353457554189744037040383519976310890738478427777069094140710561775494054910079614325126964587754001835864947654147050111602670263665/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^6 - 376450699525116150319913717099606100117870998022880082982291719477927226844482257204443520428116996141811360284130635378416719207782786872427008793128771338918/71678021239835808341833183413707082157295632127959876245320654945073107719974776765192709071828309521040382222977617414753925071633967421050912926001691571549*y^5 + 234772664020741332293574251302384425803780125356104126033543658334095314524908009331646073299439051299437917555234894675023359737050747295957712864482691614303/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y^4 + 13484943438051744228047638400129220736828133214343917328739254141472484661077610432852458526363828790306221382490437327234246260417612046756159740388375346372/5513693941525831410910244877977467858253510163689221249640050380390239055382675135784054543986793040080029401767509031904148082433382109311608686615514736273*y^3 + 23359510746115742634758454751017084513866901707142826464378345026789819290241977272840243046979799428194187118417002006418850334213964832421554678045435134535/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y^2 - 78276979592434244277988288479395117096676076262139926032822415556968956674345499808997899076978169843693836678925754075486137274080430947880826593132465745969/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098*y - 20646680917148949205649988298662468720062372079980998746028362652670966825031497726636283136459329204477574505816735838234205448357891927028633094494555965217/143356042479671616683666366827414164314591264255919752490641309890146215439949553530385418143656619042080764445955234829507850143267934842101825852003383143098

# 4 Loop Invariant
-4626882293447527031730176639880096129128107473828162492098087013215283677625874940308106998117177071025776174268940448280305007467197239285902046448693900353572497418351386702755454810723316938520927940328516226915117448/78770567982647468327296858539179589673677222505401935408413698595010051785567004108300171320247554610394443914226321932295939267902375600734189801556003653721011262055451737054149484499762591371954333737195036096643005065945*y^20 - 33186243075679678101050554568800186158709525036543736402153299087446287126427613499692495281041648658601915830906269030984379163755125792623806253623443853574851230880031578846297628253014844687678860539611853269493405923/26256855994215822775765619513059863224559074168467311802804566198336683928522334702766723773415851536798147971408773977431979755967458533578063267185334551240337087351817245684716494833254197123984777912398345365547668355315*y^19 - 548370672116307775455610476565664682524813048374789247906227342752311732516335607354771621242403427822019963230103772249664228936506334699936634988277263501680685228971010543659044753022871030582711005279322016030195134449/48474195681629211278336528331802824414570598464862729482100737596929262637272002528184720812460033606396580870293121189105193395632231138913347570188309940751391545880277992033322759692161594690433436145966176059472618502120*y^18 - 77623393692087283600600315898103177860754546554057254406459693903199292906208324579298444431186657612546373493114171094992739470346908098160255340431018217245200600105681937137178781194415556807287781028462582456196252601929/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120*y^17 - 23651404731685428134621297426666488916078904935739691843244476020370741190916802731866247138564578680581472995167620274244905689166704161176382048188295743801584678512242440616600991244108529013970781586890558814550577843491/96948391363258422556673056663605648829141196929725458964201475193858525274544005056369441624920067212793161740586242378210386791264462277826695140376619881502783091760555984066645519384323189380866872291932352118945237004240*y^16 - 834891860103172756355939133618960314543878438093562440868205361672556179967704590301115372292771995208229052946924919293705271043620453615537544531650846526771225149933293372646045759735191682623683908518739518852935386605661/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120*y^15 - 144469125240874176878722974380160352736687007324283817347220388669569282921656668674922444958974923053979608799351002013709620326395744661916647562715522303496534226480820527463692952215311002350797949909446404974665846977709/126032908772235949323674973662687343477883556008643096653461917752016082856907206573280274112396087376631110262762115091673502828643800961174703682489605845953618019288722779286639175199620146195126933979512057754628808105512*y^14 - 546586365619634783771214372642584820828810298706100344095392633597433708506166374431884639049836263349173153651458795037878690013451024545952686446828077899354417321450180968009912086633838526109696940322768068074044862686373/420109695907453164412249912208957811592945186695476988844873059173386942856357355244267580374653624588770367542540383638911676095479336537249012274965352819845393397629075930955463917332067153983756446598373525848762693685040*y^13 - 44078206806087731433836296690116349705083276551672931396024436797417104689707503466659793131163618928858403729121334638116272395937189703319890396008780643367330779462106845637841501644060488001365965570386636714922863533905/252065817544471898647349947325374686955767112017286193306923835504032165713814413146560548224792174753262220525524230183347005657287601922349407364979211691907236038577445558573278350399240292390253867959024115509257616211024*y^12 - 1804284871220071790449620363157343932224279010061651278341413688598722479695457776504023797749809249212079136093759355133681535352109842143161289906336807363756260652884715250046773961486043185107210007838343753177085715076843/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120*y^11 - 1159312922999727379473741925877794422797297983647382875094340025739691428103155492008913027713890734336135725611207484431448991204927650832541731182903194913660672639786044495093360551449379837789158594105077947682803215462425/252065817544471898647349947325374686955767112017286193306923835504032165713814413146560548224792174753262220525524230183347005657287601922349407364979211691907236038577445558573278350399240292390253867959024115509257616211024*y^10 - 547419175546918394161952700347336521449968160937106444075810896421916399579331233335321437117723771375678712234174198110334647605233762173815939607673197589899018348475623339106384518290707154568942860220866341495082261333537/140036565302484388137416637402985937197648395565158996281624353057795647618785785081422526791551208196256789180846794546303892031826445512416337424988450939948464465876358643651821305777355717994585482199457841949587564561680*y^9 + 49096915473855670974326822441891949451928504982244555444457888534926330315372847899587111827800633166968159320049676289255734436853790993960386187816803967373003107734541931789577505915966503153017552745820021066014329832505/15754113596529493665459371707835917934735444501080387081682739719002010357113400821660034264049510922078888782845264386459187853580475120146837960311200730744202252411090347410829896899952518274390866747439007219328601013189*y^8 + 913542779841120509584125954625837032255520628562087578501265639632827390976407455548540669782601267711606898372506972953384626019862595379872271583066208161559129267005131548447493506441695090101546193213287135506621231625907/630164543861179746618374868313436717389417780043215483267309588760080414284536032866401370561980436883155551313810575458367514143219004805873518412448029229768090096443613896433195875998100730975634669897560288773144040527560*y^7 - 4727287856988486682066831746326981536811072901769241354433303514944210972149787483249742518047891867501194143718723725419275395386645919433267305179064307383866014336135073510725400023524765910029639093188153379045136434718537/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120*y^6 - 830896023890383418448577365200136045207880040331246561183765615262411507710974020124231326204242823711404193405171779208123481011453402197507860532982699569132257173841030253895082803744300860165951231986801011635433085866819/252065817544471898647349947325374686955767112017286193306923835504032165713814413146560548224792174753262220525524230183347005657287601922349407364979211691907236038577445558573278350399240292390253867959024115509257616211024*y^5 + 232695405137599815114137572059638926599737138512185511263398854345682974270792678462413983706192084531376444784901526558256939019103875250793956043022823935551010710936154053260667618295766660172666804522147976026895163144829/210054847953726582206124956104478905796472593347738494422436529586693471428178677622133790187326812294385183771270191819455838047739668268624506137482676409922696698814537965477731958666033576991878223299186762924381346842520*y^4 + 1845722985909544699182088827645055290425512487664410923018728038794110826867088673623473098710079933539544965396717124335695572493160266489409312088342382135391581275818655384768862193804080810721803135502448161174637138749/1211854892040730281958413208295070610364264961621568237052518439923231565931800063204618020311500840159914521757328029727629834890805778472833689254707748518784788647006949800833068992304039867260835903649154401486815462553*y^3 + 46563575066514517690052802716712732783549294440636111151565849615904789241824207235220940890122537830024252455864184688449501148294706802231854764813194675529843905825675106012302951566916595306785605503397432864015407097261/630164543861179746618374868313436717389417780043215483267309588760080414284536032866401370561980436883155551313810575458367514143219004805873518412448029229768090096443613896433195875998100730975634669897560288773144040527560*y^2 - 431585170224398330992029341134211823110859731045918349789322538418571782541938113642681982975643000998175455500583265717282115401978717641246274328294578196800819562891946657573329490905996700085962374804123276399619792349661/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120*y - 113920335192483172987231296230322047008813402099745539735460164099317012846133456036570138266955498889988334085842355778765547639736060192969334177994293854275751592602025493355719337378908367069807933517421776562937184676097/1260329087722359493236749736626873434778835560086430966534619177520160828569072065732802741123960873766311102627621150916735028286438009611747036824896058459536180192887227792866391751996201461951269339795120577546288081055120