# Manifold: Census Knot K8_202

# Number of Tetrahedra: 8

# Number Field
x^21 - 39*x^20 + 210*x^19 + 1583*x^18 - 3172*x^17 - 8654*x^16 + 1272*x^15 + 5218*x^14 + 10727*x^13 + 1967*x^12 + 5784*x^11 - 2365*x^10 - 7009*x^9 - 7421*x^8 - 124*x^7 + 3653*x^6 + 1605*x^5 - 182*x^4 - 527*x^3 + 5*x^2 + 16*x + 1 

# Approximate Field Generator
0.292909158439574 - 0.944253252076301*I

# Shape Parameters
-19479763123819941311758854349022929898536699123635/208167783273179363628324304088647843263974488645708*y^20 + 190743072728982922768472794798870310321805414631371/52041945818294840907081076022161960815993622161427*y^19 - 4218908590684672651254406547651072296772313015094575/208167783273179363628324304088647843263974488645708*y^18 - 7528487189819413949697699676785578704982268507007422/52041945818294840907081076022161960815993622161427*y^17 + 16685929878973719207332897099461775264790152250995214/52041945818294840907081076022161960815993622161427*y^16 + 39186811854049652947930530788446339260707566040009599/52041945818294840907081076022161960815993622161427*y^15 - 12392239648535006412431360753972052159202698245901899/52041945818294840907081076022161960815993622161427*y^14 - 44749060351701347240394568345335682313849643669034371/104083891636589681814162152044323921631987244322854*y^13 - 98133617540521700466702024772972127539469347575694019/104083891636589681814162152044323921631987244322854*y^12 - 9344350110917500360744314953825672112098246155209173/208167783273179363628324304088647843263974488645708*y^11 - 112496214191647255817567107138763606921969532359506965/208167783273179363628324304088647843263974488645708*y^10 + 65612348432139779649082474907779295457302102033059645/208167783273179363628324304088647843263974488645708*y^9 + 125172212143175023598796124211853989526760791452683705/208167783273179363628324304088647843263974488645708*y^8 + 62035854186969944641979001285237273543145585410720173/104083891636589681814162152044323921631987244322854*y^7 - 3669642808732974926616523323490301614541415153481569/52041945818294840907081076022161960815993622161427*y^6 - 68076004379700139732060296184859963941283117620136749/208167783273179363628324304088647843263974488645708*y^5 - 5734492908503467781462425678149355714792776226096862/52041945818294840907081076022161960815993622161427*y^4 + 2700372500168164082012187988631234917060032492909659/104083891636589681814162152044323921631987244322854*y^3 + 4628284136737367877023067922971323293754945751283557/104083891636589681814162152044323921631987244322854*y^2 - 414166146904326081882796018917188915649002029235245/104083891636589681814162152044323921631987244322854*y - 55954229815698716102766862173206593562117842197763/104083891636589681814162152044323921631987244322854

-133051517437469987170068670745394416386262279357466/52041945818294840907081076022161960815993622161427*y^20 + 5196130901358918073266310760544984055151728770109982/52041945818294840907081076022161960815993622161427*y^19 - 28220724866597971578542436247779069276345391094773105/52041945818294840907081076022161960815993622161427*y^18 - 209041960994820241894002769385869973565985941394500275/52041945818294840907081076022161960815993622161427*y^17 + 432905039559591653560459023363044102599360568141702380/52041945818294840907081076022161960815993622161427*y^16 + 1125190613530503178214509924312962087025681650668372409/52041945818294840907081076022161960815993622161427*y^15 - 225969174166269036764592695012637535961311933683667120/52041945818294840907081076022161960815993622161427*y^14 - 663540871358689893248613337117633434636423760539657115/52041945818294840907081076022161960815993622161427*y^13 - 1381643899031866757756192014395587335395349367073094159/52041945818294840907081076022161960815993622161427*y^12 - 193927856892212261334575902825456086805098609647801406/52041945818294840907081076022161960815993622161427*y^11 - 782743699089769335153702339643354159852872353199149169/52041945818294840907081076022161960815993622161427*y^10 + 338768665055569487225681454295487650843147713546535773/52041945818294840907081076022161960815993622161427*y^9 + 894935627023762563319784363748436436851364025693060555/52041945818294840907081076022161960815993622161427*y^8 + 931601669599936408292439711800935904063942208137298734/52041945818294840907081076022161960815993622161427*y^7 - 24019456103626434895261283544501339566180562281158625/52041945818294840907081076022161960815993622161427*y^6 - 464229165029402635604341211763402371743590424521884377/52041945818294840907081076022161960815993622161427*y^5 - 177008277090834284990860780063321972475915586367877117/52041945818294840907081076022161960815993622161427*y^4 + 32576936108641284547770395338936623213445501176976618/52041945818294840907081076022161960815993622161427*y^3 + 64358012090725970202386761899466938213562772541886186/52041945818294840907081076022161960815993622161427*y^2 - 5680684319389663326964053530019599273980622353315342/52041945818294840907081076022161960815993622161427*y - 1535184653260637893542695806209709485923682645357784/52041945818294840907081076022161960815993622161427

84624594059655899910747229154199937428610624894301/52041945818294840907081076022161960815993622161427*y^20 - 6617188439703454011841286281066964563868940712933337/104083891636589681814162152044323921631987244322854*y^19 + 36188248002565977685360821516257859792624040518474589/104083891636589681814162152044323921631987244322854*y^18 + 264322667299678822911502554583280774840715708254449661/104083891636589681814162152044323921631987244322854*y^17 - 562166881690730996183642818792679035922576399479084491/104083891636589681814162152044323921631987244322854*y^16 - 703412102147751568516224777860503215543729312146721314/52041945818294840907081076022161960815993622161427*y^15 + 172996433664673105928977182205043651659244565661001838/52041945818294840907081076022161960815993622161427*y^14 + 416071717890941017726215643546995254435187213941290022/52041945818294840907081076022161960815993622161427*y^13 + 868492106372606039005559306373508269252567706505462996/52041945818294840907081076022161960815993622161427*y^12 + 86699132800602778759224477575496290881327373164519891/52041945818294840907081076022161960815993622161427*y^11 + 981462968680530360524254959351395760766319729897290819/104083891636589681814162152044323921631987244322854*y^10 - 244910493230967884347880454127745154480392718383882715/52041945818294840907081076022161960815993622161427*y^9 - 563015154610594812558043313743104221877838315949929772/52041945818294840907081076022161960815993622161427*y^8 - 574474895258786839255918304919239821256810131165174833/52041945818294840907081076022161960815993622161427*y^7 + 76773515116285931303728124799159793794214984572723047/104083891636589681814162152044323921631987244322854*y^6 + 298564303301201702745808302439739946857464144686614880/52041945818294840907081076022161960815993622161427*y^5 + 212195744686939703208558999979032308522019263329077679/104083891636589681814162152044323921631987244322854*y^4 - 46135623981476556847994114933930960823400622327277789/104083891636589681814162152044323921631987244322854*y^3 - 41071152271158656016573291972265357378359764225121310/52041945818294840907081076022161960815993622161427*y^2 + 4493157704958299749018571305427273957626573443910713/52041945818294840907081076022161960815993622161427*y + 682500835102837073590918090858846624530929313452133/52041945818294840907081076022161960815993622161427

3553098809102756569273041222154756100630652484872/52041945818294840907081076022161960815993622161427*y^20 - 139941388515098087201197215181474086044252977047193/52041945818294840907081076022161960815993622161427*y^19 + 799459454169547195552714948540265426210408726034867/52041945818294840907081076022161960815993622161427*y^18 + 5341742112301338675801611450728150945409415729437960/52041945818294840907081076022161960815993622161427*y^17 - 13448616595071411516714178374650718814798865802412636/52041945818294840907081076022161960815993622161427*y^16 - 26739207110029197590895372531102607857969640481303370/52041945818294840907081076022161960815993622161427*y^15 + 15960034936188265308366024270460338449889717814835034/52041945818294840907081076022161960815993622161427*y^14 + 19700044383682875225813990812780034194763197593942368/52041945818294840907081076022161960815993622161427*y^13 + 35581925512853747020415335412612466340181672877878992/52041945818294840907081076022161960815993622161427*y^12 - 9021486579574992541200140969756262620385978103275838/52041945818294840907081076022161960815993622161427*y^11 + 14011948285375598247015151317222282675086936061781671/52041945818294840907081076022161960815993622161427*y^10 - 21542719518186846546677598616089189753399972888368844/52041945818294840907081076022161960815993622161427*y^9 - 24641739218765094567354366252722512051189420793262834/52041945818294840907081076022161960815993622161427*y^8 - 20257399121017136945116132145442920692929278626052362/52041945818294840907081076022161960815993622161427*y^7 + 10763033305006851011880787158923449582547395916783899/52041945818294840907081076022161960815993622161427*y^6 + 17928644387209219621994989171839527284121627987960219/52041945818294840907081076022161960815993622161427*y^5 + 4231373635113424669198553693422884799334423175082706/52041945818294840907081076022161960815993622161427*y^4 - 2622636826403426794746975546246284260817865554319712/52041945818294840907081076022161960815993622161427*y^3 - 2811019266508372260948355977958252079057037093916487/52041945818294840907081076022161960815993622161427*y^2 + 282384067593610976847827233842688932858904064896204/52041945818294840907081076022161960815993622161427*y + 64949655936827371951008760428189138071124899572545/52041945818294840907081076022161960815993622161427

-826596052769189927284267123307362163923641063944299/52041945818294840907081076022161960815993622161427*y^20 + 32318783959729401545521842278716045095411769129343695/52041945818294840907081076022161960815993622161427*y^19 - 176778223389511978334086263675915038615802090980997215/52041945818294840907081076022161960815993622161427*y^18 - 1290868058956363751977700054272356804782008300267695236/52041945818294840907081076022161960815993622161427*y^17 + 2748266095872987826974307995218050646882789002910634288/52041945818294840907081076022161960815993622161427*y^16 + 6874181618107531510626901942541501293310519082161882549/52041945818294840907081076022161960815993622161427*y^15 - 1714685585651231798098048340957369371073789973186957795/52041945818294840907081076022161960815993622161427*y^14 - 4099054715485102306202767132092634695836994804756927108/52041945818294840907081076022161960815993622161427*y^13 - 8461631914263637340076626878474711352761062085385221140/52041945818294840907081076022161960815993622161427*y^12 - 815612779173623381255232987940952017547978887181862541/52041945818294840907081076022161960815993622161427*y^11 - 4760416115082109122349389246818708001599474977281751521/52041945818294840907081076022161960815993622161427*y^10 + 2406970197782280661061580094433566497451573003071853380/52041945818294840907081076022161960815993622161427*y^9 + 5522677475281318392803124084765756146139980222581748283/52041945818294840907081076022161960815993622161427*y^8 + 5597884438669242106077272998299791899642206182901366218/52041945818294840907081076022161960815993622161427*y^7 - 415480641141631226264350113175299860628882094660426584/52041945818294840907081076022161960815993622161427*y^6 - 2934714800327225669343686337252777945154703522595779979/52041945818294840907081076022161960815993622161427*y^5 - 1029399836870713947248366728721257510282401137595593330/52041945818294840907081076022161960815993622161427*y^4 + 234752388135844571667156785187767689129351516965084208/52041945818294840907081076022161960815993622161427*y^3 + 401597248338920916298771982937118316096986386538777273/52041945818294840907081076022161960815993622161427*y^2 - 44589703000339136803573779517400734822920576219715120/52041945818294840907081076022161960815993622161427*y - 6132638340039529024726583307169848549845094078610756/52041945818294840907081076022161960815993622161427

8445610172233915687336762682365112664253070895636/52041945818294840907081076022161960815993622161427*y^20 - 330524303579921738556877675526382195509541313897384/52041945818294840907081076022161960815993622161427*y^19 + 1817664529418060697814517329938460400347511580211330/52041945818294840907081076022161960815993622161427*y^18 + 13151502749789261752916270232963273208288363110838943/52041945818294840907081076022161960815993622161427*y^17 - 28715128916013947234735827138617301384868510244932571/52041945818294840907081076022161960815993622161427*y^16 - 70446870983239856547291457159286030759155238446628148/52041945818294840907081076022161960815993622161427*y^15 + 22074611727387634117551588602719875093133157577029201/52041945818294840907081076022161960815993622161427*y^14 + 48567747076645377396572633615475032605786790481430814/52041945818294840907081076022161960815993622161427*y^13 + 86002194043146468805315654790863845391617216356190969/52041945818294840907081076022161960815993622161427*y^12 + 1610436826762182433341122000260989198600580649296783/52041945818294840907081076022161960815993622161427*y^11 + 40778423327563934117139448167409964739791032673434141/52041945818294840907081076022161960815993622161427*y^10 - 31058865443989163505023751142982275992579265271395959/52041945818294840907081076022161960815993622161427*y^9 - 61297830092343217298062330631881230247830244034802425/52041945818294840907081076022161960815993622161427*y^8 - 56942960804384840543300357798727590776762151708000902/52041945818294840907081076022161960815993622161427*y^7 + 11426586589623429844711838221292242392027694327540201/52041945818294840907081076022161960815993622161427*y^6 + 35589198947153531596618465326522509679002583931023236/52041945818294840907081076022161960815993622161427*y^5 + 11536482744256572428697268619082664233690359074514517/52041945818294840907081076022161960815993622161427*y^4 - 4180544869527048981881775943197736850155704971687404/52041945818294840907081076022161960815993622161427*y^3 - 4907096379309018428219495593485650041839004112261253/52041945818294840907081076022161960815993622161427*y^2 + 481951547176117739416157575484956262978366213011204/52041945818294840907081076022161960815993622161427*y + 168249775169383848253404364971807730139027991364114/52041945818294840907081076022161960815993622161427

339945219202138728578545358111951633048271726280894/52041945818294840907081076022161960815993622161427*y^20 - 13277969311047905310573840309934407795288757943476249/52041945818294840907081076022161960815993622161427*y^19 + 72177524366040151883336725154163208582393401387694047/52041945818294840907081076022161960815993622161427*y^18 + 533721279505237285289625649205371979695039375025247750/52041945818294840907081076022161960815993622161427*y^17 - 1109159503309824369230431120387485282561585114919553247/52041945818294840907081076022161960815993622161427*y^16 - 2870077879446032116430675054136963164943109397104548123/52041945818294840907081076022161960815993622161427*y^15 + 593316112551452463846021818200745230164583571142641833/52041945818294840907081076022161960815993622161427*y^14 + 1702683616875723274751599842966267774420003759605066206/52041945818294840907081076022161960815993622161427*y^13 + 3533163639783616209935545283141247478501892562020089429/52041945818294840907081076022161960815993622161427*y^12 + 472157672193366214184523899049427850494303455409627581/52041945818294840907081076022161960815993622161427*y^11 + 1984553192722269209615529123340099557723672695023281331/52041945818294840907081076022161960815993622161427*y^10 - 892487821377476491392394992272031144415153105784657813/52041945818294840907081076022161960815993622161427*y^9 - 2293569220704195540037852786083455444128652782744394064/52041945818294840907081076022161960815993622161427*y^8 - 2378619149535740242204438741489107746011446879920210976/52041945818294840907081076022161960815993622161427*y^7 + 77813251238274066080694893916820159409561029534996456/52041945818294840907081076022161960815993622161427*y^6 + 1199497780771713253223665629909665510630511179156450537/52041945818294840907081076022161960815993622161427*y^5 + 456032816723859027009833278566177078247181031122729079/52041945818294840907081076022161960815993622161427*y^4 - 84590625074646828061345650197963197754220486549900168/52041945818294840907081076022161960815993622161427*y^3 - 166468091072266323254878312872062266402106994930625636/52041945818294840907081076022161960815993622161427*y^2 + 14474859937306676463878864049157978121932200167951985/52041945818294840907081076022161960815993622161427*y + 4073506819768939549177761343053072622232626325378027/52041945818294840907081076022161960815993622161427

-283535101010552246604629200316652129167749556559630/52041945818294840907081076022161960815993622161427*y^20 + 11078356955354196733656296049081171002442002829969683/52041945818294840907081076022161960815993622161427*y^19 - 60344273972653622869718106360202349170887378496371342/52041945818294840907081076022161960815993622161427*y^18 - 444422135641894684810682830780298798150119887413039165/52041945818294840907081076022161960815993622161427*y^17 + 931221856015042786483963746466588055545670924967113218/52041945818294840907081076022161960815993622161427*y^16 + 2384093093477135050417284082918062716230030368999021609/52041945818294840907081076022161960815993622161427*y^15 - 529706392785344146360314966190050474186776818887863264/52041945818294840907081076022161960815993622161427*y^14 - 1427639739610074681862240419556945541374691548515490162/52041945818294840907081076022161960815993622161427*y^13 - 2932960364504102691096516952575317030851312188648532569/52041945818294840907081076022161960815993622161427*y^12 - 350271248200358422384996716157090497482135392919670656/52041945818294840907081076022161960815993622161427*y^11 - 1632369793320632274101356123847210275338594543787237762/52041945818294840907081076022161960815993622161427*y^10 + 777464470837412040140057871956830809337896884393700378/52041945818294840907081076022161960815993622161427*y^9 + 1917013400815126494004709641980299824238432951398480193/52041945818294840907081076022161960815993622161427*y^8 + 1962307148341463464932282157031949736398627437152326865/52041945818294840907081076022161960815993622161427*y^7 - 99491915839815982643231942585058904383462447752665956/52041945818294840907081076022161960815993622161427*y^6 - 1013929618945913942411600287335089913942016628554311803/52041945818294840907081076022161960815993622161427*y^5 - 374661066249954667127592586565970440128251436027194369/52041945818294840907081076022161960815993622161427*y^4 + 77208199510588207488501640738193332989627980935798918/52041945818294840907081076022161960815993622161427*y^3 + 140771356032495611532724036859733996555434591148411733/52041945818294840907081076022161960815993622161427*y^2 - 12742365557634079893917226298110280796685358224190880/52041945818294840907081076022161960815993622161427*y - 3350087468539742578726391653390752762808087627647000/52041945818294840907081076022161960815993622161427


# A Gluing Matrix
{{-5,-4,6,-2,2,-4,-7,6},{-6,-4,7,-2,2,-4,-8,7},{-4,-3,5,-2,0,-2,-5,5},{-6,-4,8,-3,2,-5,-9,8},{-4,-3,5,-2,2,-3,-6,6},{-6,-4,8,-3,2,-4,-8,7},{0,0,0,0,1,0,1,-1},{-8,-6,10,-4,2,-6,-11,10}}

# B Gluing Matrix
{{1,0,0,0,0,0,0,8},{0,1,0,0,0,0,0,9},{0,0,1,0,0,0,0,5},{0,0,0,1,0,0,0,10},{0,0,0,0,1,0,0,7},{0,0,0,0,0,1,0,9},{0,0,0,0,0,0,2,1},{0,0,0,0,0,0,0,12}}

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

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

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

# 1 Loop Invariant
1858888064388784866340617481051079762017505983453049/104083891636589681814162152044323921631987244322854*y^20 - 36381226943270359153775741889053632091932874108433123/52041945818294840907081076022161960815993622161427*y^19 + 200371965352764626261923622814319070602068364621206225/52041945818294840907081076022161960815993622161427*y^18 + 1443188190982717294785172800516256922270587925361666142/52041945818294840907081076022161960815993622161427*y^17 - 3157248821999238011655486047317689484600673722056750990/52041945818294840907081076022161960815993622161427*y^16 - 15229525571857778897177864604311207193973979028200162167/104083891636589681814162152044323921631987244322854*y^15 + 4610945810629462052813670135107455000963583987270609499/104083891636589681814162152044323921631987244322854*y^14 + 9303778412399571782743800856722859482672918757726007371/104083891636589681814162152044323921631987244322854*y^13 + 9342765430069938846816383831277015783673181112048186872/52041945818294840907081076022161960815993622161427*y^12 + 884057993501285166346509716661462205178463259646309957/104083891636589681814162152044323921631987244322854*y^11 + 10289928124776321136351124783300538864178143953523930517/104083891636589681814162152044323921631987244322854*y^10 - 3032044506008878079117878392234517822825609026992228912/52041945818294840907081076022161960815993622161427*y^9 - 6210301301723394581790201309614897734761641569972942886/52041945818294840907081076022161960815993622161427*y^8 - 6031154104906299743064437569286619759890232149631406970/52041945818294840907081076022161960815993622161427*y^7 + 1654538788464089486345766781302298310461763405609130329/104083891636589681814162152044323921631987244322854*y^6 + 6831974396046240428078872723333920490903464578341290167/104083891636589681814162152044323921631987244322854*y^5 + 1063752862750757344098093081900350581190493022460668935/52041945818294840907081076022161960815993622161427*y^4 - 339262830992548991568802511743155372879811722198514561/52041945818294840907081076022161960815993622161427*y^3 - 470685695957132922987782788603155425877408659937948664/52041945818294840907081076022161960815993622161427*y^2 + 123344270974712754243688856395130037259705840036362599/104083891636589681814162152044323921631987244322854*y + 14795114372458496959919596096888082290040117301627837/104083891636589681814162152044323921631987244322854

# 2 Loop Invariant
102797803134209313865420486793392684541595435107152681329223137635655962535968859667373630299707077195999675463033319/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^20 - 4013799766779933795319696501325394011871060393151358917628316749278058940458968959295330769326495043158502266101661589/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^19 + 7255546615666928637182520994883767191961848595509537092574584912802562097271772179481473763587941388617969241664264245/553539056813458493832067427029332996405555290089972588432848157037597724624993062088407353175039949937040708094234928*y^18 + 53961792792237705737330384279187343085890598654901582505273597027486579285389472051993209685471693450711190919814944427/553539056813458493832067427029332996405555290089972588432848157037597724624993062088407353175039949937040708094234928*y^17 - 83551438951407739142362817972207847125521550654741110194777791608391346480263245484531990922181907043011722752725548765/415154292610093870374050570271999747304166467567479441324636117778198293468744796566305514881279962452780531070676196*y^16 - 880796648939423579405205681930400544485165064126468307026794206500092858333329613481084103728829025423609459818840974279/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^15 + 181182756289452720217470135634316876041652651572673443292247021312804221848283824883296163686601176407888273813692904791/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^14 + 567114414185761409233661313561253158330064794891225435888865585013796427196320934325891417567478642472505634883382584405/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^13 + 67403058273972167875630142324212424313912631931601871801485186699195992443738929716493050259834238097615933490263531362/103788573152523467593512642567999936826041616891869860331159029444549573367186199141576378720319990613195132767669049*y^12 + 126860864633838802336990708305698971508386895208542251054820832318673766987042544300029111753091826401124180012434862025/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^11 + 554436032613993011699650719731959349421820557197325434276881241969529624724085527021532340716159176598869445417943242783/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^10 - 24044513853026226552258797307072734701778178161066804650105466246928647543880906263893717619684878600805829797884853143/138384764203364623458016856757333249101388822522493147108212039259399431156248265522101838293759987484260177023558732*y^9 - 730589513312665972989589384255535434789060796299544675898566096168361023603257076490406952286386362261397916817601482811/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y^8 - 245954603224152422472626142662185932497020816137865692850858513088382342841091726342281200089416242611627007039599641711/553539056813458493832067427029332996405555290089972588432848157037597724624993062088407353175039949937040708094234928*y^7 + 2254812589616339783721395885613737590025863675359928614782895547728786435659879884955715457434495781853181843762339367/69192382101682311729008428378666624550694411261246573554106019629699715578124132761050919146879993742130088511779366*y^6 + 133900281874172877338197991010423950542267757418263670590607469605415237794913022660612465681741469417655266138862140897/553539056813458493832067427029332996405555290089972588432848157037597724624993062088407353175039949937040708094234928*y^5 + 50368836432177937565121740814576273042756822898743184129311929783663194650448549896113831927536136167991923165886149343/553539056813458493832067427029332996405555290089972588432848157037597724624993062088407353175039949937040708094234928*y^4 - 17344541278714203353072811514386655501812437518394831241949298062069167996484966776173945546765231922450660470680480669/830308585220187740748101140543999494608332935134958882649272235556396586937489593132611029762559924905561062141352392*y^3 - 27988712307233405458746240241732397420121537397991237505752765300921415048697367236440811773248318084483788689802973035/830308585220187740748101140543999494608332935134958882649272235556396586937489593132611029762559924905561062141352392*y^2 + 4127510092046235146799322191114909432029316207530160215149355763679193166223596930648314909750234565904049467378770241/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784*y + 1098883535547737752940930983168365662929321546755046039476098647796271843077653298818777556825778079744390796119086673/1660617170440375481496202281087998989216665870269917765298544471112793173874979186265222059525119849811122124282704784

# 3 Loop Invariant
43975156545983174122097613245324610661803523573269738037017698829763918200019694357542290469351107943778089160210502683128621220342501866162537146995/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^20 - 1724469956071333802552685052971065132143226040356921415699002865228226907044638505532326290376190836527453513780924775538612100929094835748808717608079/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^19 + 4804504584939549872318957207485225686898255676902699838503419909849952734256000703847669356886057669480389788317557053567320907800773362178163769628821/902642224323211171671780606386832605168036035507682407832511057174040618446221308112876957290849510568158897303213756781973082314907711278513482773088*y^18 + 67389744847864198940992964624567993386540094253237724825094446257493569683613513915086972366144617905642182494446788022303509420111278983372824518278365/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^17 - 19131698352803109791216582164895515384371695878550784097062023358834208264099604347531499828855520759110050146018942964031512722992575241549235384000557/225660556080802792917945151596708151292009008876920601958127764293510154611555327028219239322712377642039724325803439195493270578726927819628370693272*y^16 - 341416594271994986086416761027223564004172104998927921671801038462434539298406184589268895102881381718126986156547461857191876459070514789154978206399869/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^15 + 28519576794704806685077086057468472097720115682767626296466623910506690450119272614075228860139939401960566809291744066024789477661785024532304022385067/451321112161605585835890303193416302584018017753841203916255528587020309223110654056438478645424755284079448651606878390986541157453855639256741386544*y^14 + 171199302732060477344674706836866086000679487581697435040891263224073507783847908205017588638686295997342272087257139867021088480885994001422422532266757/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^13 + 457739365696067769864161733208616792296826945358320191725474548859111328194792224828785264788244733982557968097503805405957768210411007279841497864312071/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^12 + 13596616940923252608145882214920125472851381884344212516770202036403544112330022548497313159255823899030781287750729928587560670805418339779305919760283/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^11 + 34140887563524716666612892008204380760507884039371282547238986579733627689140763162117703281828533386000132436109024298666457456093193935065586885983593/225660556080802792917945151596708151292009008876920601958127764293510154611555327028219239322712377642039724325803439195493270578726927819628370693272*y^10 - 20223442373323618086793630651548483900803444940564263583703296865428652419963345197994248938004621638055791981695005602677752247469608727336497415633943/225660556080802792917945151596708151292009008876920601958127764293510154611555327028219239322712377642039724325803439195493270578726927819628370693272*y^9 - 65213982579837119956099814163445538683125155742046611338524923486732165964107764975626321447046291488920103309285940702119468028494456125700851834660083/451321112161605585835890303193416302584018017753841203916255528587020309223110654056438478645424755284079448651606878390986541157453855639256741386544*y^8 - 279053761947596364030965860745883364365742904220341785884743173040889858178941365779116861461387363414699242404809492560172585489052649011666088552148461/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^7 + 9150728861230806279778795173642572144213268192580394502194607133242966642960444161595614105497003750287688662981941654205142854194909318830323341196879/902642224323211171671780606386832605168036035507682407832511057174040618446221308112876957290849510568158897303213756781973082314907711278513482773088*y^6 + 9146193224455063454988156462641890054689584182890151961069282276371558559060507631130313674513178857347211825562828072455591420750723162712971921627637/112830278040401396458972575798354075646004504438460300979063882146755077305777663514109619661356188821019862162901719597746635289363463909814185346636*y^5 + 25437069805754057278185412333212259914939887553754163196601448255296221024604289363299209582019220240250277189935333638235095883995472588295235778851813/902642224323211171671780606386832605168036035507682407832511057174040618446221308112876957290849510568158897303213756781973082314907711278513482773088*y^4 - 6186527298411595760478603177426386968185512879648482299231443087450078455522530300825033190719935548401869988988289307675306820378032115280999640959897/1805284448646422343343561212773665210336072071015364815665022114348081236892442616225753914581699021136317794606427513563946164629815422557026965546176*y^3 - 11309014509140069842210400748985224811041388454843051152700099229429170603093115200545256075464338656259597830010804452119074372829778626730833380668415/902642224323211171671780606386832605168036035507682407832511057174040618446221308112876957290849510568158897303213756781973082314907711278513482773088*y^2 + 472684986662785341487766864660716392787057865728881236289652510168161975899886798524124410221420719702238628270459218337820375369962586615030614115631/451321112161605585835890303193416302584018017753841203916255528587020309223110654056438478645424755284079448651606878390986541157453855639256741386544*y + 278272584847156071973605514908146843122301352138981339820016412255188091368889293277704153323890941316020630008271711450789237234810151935863143200147/902642224323211171671780606386832605168036035507682407832511057174040618446221308112876957290849510568158897303213756781973082314907711278513482773088

# 4 Loop Invariant
-270662573694764667569282741071044197739864551305048733060477982742032832867200034960873137553074846824032080435779132371834737611848671513979032636523456801883488399598801097720396069807654158621237104163505618262651/72006491730209224862256344357555016349472299088785970276919843276740910981090312292985998192715463933744445347023717747447167614632332627360226032730799092331648600217094684234161076265574837204511026810391693814570240*y^20 + 137405303734470245355254996841153667834037911117160874463096026439124615007573735648016173799280744332049369033160845218864688049590191062087113604454128126826419827179777051767391765360696037695583605753397106102921749/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^19 - 1113471625550406860315466770165306251734060359060736147109217298804234260897092535020751546269207114920875014260967322452939895352237298086819171890566291675836279219166315042084030976619135559355825384558110086614895277/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^18 - 1192411810698408131113836369565093864205816231316242743005469897780361854848060081010986103021411241386089069534952846145376831234664316547790523519461304241390091571114425095770890630600425849094265485990154923271312651/432038950381255349173538066145330098096833794532715821661519059660445465886541873757915989156292783602466672082142306484683005687793995764161356196384794553989891601302568105404966457593449023227066160862350162887421440*y^17 + 1355242240582339568590919924115041354050300306202922353049982561266130973730202984802651589239969642764606647519901733493675364870244000658931370987108188372489790523740756607835114436334454721297070675772396872523515277/48004327820139483241504229571703344232981532725857313517946562184493940654060208195323998795143642622496296898015811831631445076421555084906817355153866061554432400144729789489440717510383224803007351206927795876380160*y^16 - 2487193304097268988301928549303204065201853749767266965293509346383716220031063356601896392924002736216617283330025489135171577513288564986145475685977207667390555577456630187495946699721036845520774482716995011341886579/86407790076251069834707613229066019619366758906543164332303811932089093177308374751583197831258556720493334416428461296936601137558799152832271239276958910797978320260513621080993291518689804645413232172470032577484288*y^15 - 47183987482778024514467259102809326793377276951565164118589793014686228104022046485921377911596283089550570371417102582030119681958884754668745804552616182092686315069204470757511899751425699287497534726590000213876107411/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^14 + 87943393838481904905898120850839966516227118861086105651362143970257126837816285027902838875971307079141721443651473814111678654830112116348460365153931104656903301659298169419263219638497442369941738143544220480385957581/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^13 - 4221025909293648140881636699112298282637985414667067678290429949506559038379162325799041514936245431524856212759332867005347092602967884505499090626897412930322943714629618215833828658551519493922133975813500370989328011/72006491730209224862256344357555016349472299088785970276919843276740910981090312292985998192715463933744445347023717747447167614632332627360226032730799092331648600217094684234161076265574837204511026810391693814570240*y^12 + 15010352750267220181101590658198695187663721292020972755502935081365030695784358009809311365987944695067532040122891969060374802651483982352326155137475577805590091313660037021335999046758805838612063760026848099767305713/216019475190627674586769033072665049048416897266357910830759529830222732943270936878957994578146391801233336041071153242341502843896997882080678098192397276994945800651284052702483228796724511613533080431175081443710720*y^11 - 88288855321608850743664449128226140413418582993389294574839333969005297171437704045077175348418408156207271288738278605478796767765809980609509793208737865215055665584926379146010302637530007673024581586319941368846430551/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^10 + 5932237809674429074210985667053202245821267853687108100663020866958776598409377030188018077307910490522044328291970950631640944673924890603652912316014998496570962235758941539830743933067172859681817636679593033841067469/57605193384167379889805075486044013079577839271028776221535874621392728784872249834388798554172371146995556277618974197957734091705866101888180826184639273865318880173675747387328861012459869763608821448313355051656192*y^9 - 63768694613285968092205784292690677717700038001681343368102938867519707797226734243464104550377068854411690237874516878877646556847909868094827270142527923418392204700598794215204615128652216994087841927261509229388824081/864077900762510698347076132290660196193667589065431643323038119320890931773083747515831978312585567204933344164284612969366011375587991528322712392769589107979783202605136210809932915186898046454132321724700325774842880*y^8 - 1974303750476049575767667252443862396204483504533978072675913777267757629324458985820613270157118583489472186095908527494983813802043991119440717194887797202906908447257664475403290101752774066391090584193382857871728247/172815580152502139669415226458132039238733517813086328664607623864178186354616749503166395662517113440986668832856922593873202275117598305664542478553917821595956640521027242161986583037379609290826464344940065154968576*y^7 + 3262109769278437457098357886560361226409499741607479539103018968739234345712870994760717098907030852678190809110015518281905518136087773978911576118736838660493201540620495483657080891684000354305062305174361185571647387/216019475190627674586769033072665049048416897266357910830759529830222732943270936878957994578146391801233336041071153242341502843896997882080678098192397276994945800651284052702483228796724511613533080431175081443710720*y^6 + 2390987167346625036799598971367908165621818798016493970039233761493868951303809676654352868509358224976703904802469663663388848526520398877492012434553730458718647840841288059612170785602519820869943888110893736841584431/108009737595313837293384516536332524524208448633178955415379764915111366471635468439478997289073195900616668020535576621170751421948498941040339049096198638497472900325642026351241614398362255806766540215587540721855360*y^5 + 1628280567109290050275545668478332997865786141585789099853407106105848999359754743392375807687496649176234120358183826589739235274081147984439543086785607089534947216824570835152650343649153134041080849437458670911124109/216019475190627674586769033072665049048416897266357910830759529830222732943270936878957994578146391801233336041071153242341502843896997882080678098192397276994945800651284052702483228796724511613533080431175081443710720*y^4 - 8545295864943861024966084967881625167591616467542183652752685393753981193110346028723631776102804398939137318833982687088738182597177412649552548937995518477651445122048866329844506440042576916220356767151164488899637083/432038950381255349173538066145330098096833794532715821661519059660445465886541873757915989156292783602466672082142306484683005687793995764161356196384794553989891601302568105404966457593449023227066160862350162887421440*y^3 + 59000626797075485894442015369855787749384843904669786056423087912545055009451346494618030948831401937213251321650776002860246320362244701817361035536136041206366078149582522302736524440495730865716935664246809919642521/13501217199414229661673064567041565565526056079147369426922470614388920808954433554934874661134149487577083502566947077646343927743562367630042381137024829812184112540705253293905201799795281975845817526948442590231920*y^2 + 145674929632853017550657032829500096321824684929824906985399368267481244943350616584532836642704212650308680931638178267931108644897017930973761132182992693098752223622399908771937549063113022477860287667537675806866707/288025966920836899449025377430220065397889196355143881107679373106963643924361249171943992770861855734977781388094870989788670458529330509440904130923196369326594400868378736936644305062299348818044107241566775258280960*y - 115546180676913271567442709803340954648773882328224751957220332867636578282921134861784395248057257514956233515362520467696728803886362936707625530054829693804696083618691373363680997314354436443191985611997889560817/3600324586510461243112817217877750817473614954439298513845992163837045549054515614649299909635773196687222267351185887372358380731616631368011301636539954616582430010854734211708053813278741860225551340519584690728512