# Manifold: Census Knot K8_175

# Number of Tetrahedra: 8

# Number Field
x^22 + 10*x^21 + 13*x^20 + 61*x^19 + 258*x^18 + 48*x^17 + 840*x^16 + 1821*x^15 + 6791*x^14 + 13454*x^13 + 4660*x^12 - 10883*x^11 - 46192*x^10 - 58857*x^9 - 13004*x^8 + 38504*x^7 + 50242*x^6 + 31971*x^5 + 12541*x^4 + 3125*x^3 + 463*x^2 + 35*x + 1 

# Approximate Field Generator
-0.272311866779482 - 0.388460862165638*I

# Shape Parameters
-464946277916051151729230718995/957975191363925153960065086499*y^21 - 4778050437758048851380850667559/957975191363925153960065086499*y^20 - 7272490627036932429101454476608/957975191363925153960065086499*y^19 - 29481246737256234354878841099099/957975191363925153960065086499*y^18 - 18185431339308552594887862699944/136853598766275021994295012357*y^17 - 2274283958987191089155156184099/41651095276692397998263699413*y^16 - 383455691278484268602805061669256/957975191363925153960065086499*y^15 - 136933183038455647300840580932239/136853598766275021994295012357*y^14 - 3345204135546186603127434758690451/957975191363925153960065086499*y^13 - 7047470890940351746673857219162538/957975191363925153960065086499*y^12 - 3553902878576412988929152540865309/957975191363925153960065086499*y^11 + 5056293948987250269485534579652732/957975191363925153960065086499*y^10 + 990476328425493764772200879875778/41651095276692397998263699413*y^9 + 1411569056951528789361138087943220/41651095276692397998263699413*y^8 + 11003303315594979834078647254344172/957975191363925153960065086499*y^7 - 2678700829375649656988889614445604/136853598766275021994295012357*y^6 - 27817285053886306475225572624437679/957975191363925153960065086499*y^5 - 18656404057236867569337873175852598/957975191363925153960065086499*y^4 - 7445411450916404894701304375230663/957975191363925153960065086499*y^3 - 1812398738376773028703325938488127/957975191363925153960065086499*y^2 - 238686719993554530714788361801003/957975191363925153960065086499*y - 10489373908345419090858368438724/957975191363925153960065086499

-1437577814336484103958571001050/22033429401370278541081496989477*y^21 - 12855839809957966459507781026543/22033429401370278541081496989477*y^20 - 3296004071382108308675736057714/22033429401370278541081496989477*y^19 - 65239203705234014364045920592472/22033429401370278541081496989477*y^18 - 267271047329217479769666430688718/22033429401370278541081496989477*y^17 + 2195781000419471415492727135893/136853598766275021994295012357*y^16 - 1017325812908081822975091644593739/22033429401370278541081496989477*y^15 - 151751071654490078389098015868985/3147632771624325505868785284211*y^14 - 6506507307719979768819076021319107/22033429401370278541081496989477*y^13 - 7629754861073647223375586375958223/22033429401370278541081496989477*y^12 + 2511136666333353307887004676738112/3147632771624325505868785284211*y^11 + 33308593069939521198614877650500553/22033429401370278541081496989477*y^10 + 3031198892658417120858143801239457/957975191363925153960065086499*y^9 + 1609215288965340424909283398121062/957975191363925153960065086499*y^8 - 58308050560382496050019037189824790/22033429401370278541081496989477*y^7 - 94142417346346456775821517984731786/22033429401370278541081496989477*y^6 - 9121108034456372485122870983370777/3147632771624325505868785284211*y^5 - 3228800657963146877608414229186510/3147632771624325505868785284211*y^4 - 3496303845198105071107834177243156/22033429401370278541081496989477*y^3 + 39774677492855033379952871705270/3147632771624325505868785284211*y^2 + 21629408676559797886058017613722/3147632771624325505868785284211*y + 12131342206405660593730877537935/22033429401370278541081496989477

7306913159890693844489357708793291627953502583/428190582207958343700804427079223275278713727*y^21 + 71654706885522490993372528930643201999526245402/428190582207958343700804427079223275278713727*y^20 + 81137713827166857441997998775250596946457447723/428190582207958343700804427079223275278713727*y^19 + 430201630349943153062071765250866099310885407561/428190582207958343700804427079223275278713727*y^18 + 1802172307218080349835693656027304009447806237971/428190582207958343700804427079223275278713727*y^17 + 2992579004691148604868720886873930822324886483/428190582207958343700804427079223275278713727*y^16 + 6142093650436413217059028752120033429583469263542/428190582207958343700804427079223275278713727*y^15 + 12118377642988850597398140153560403866256136755467/428190582207958343700804427079223275278713727*y^14 + 1630687108276126829668763664868819303553727324143/14765192489929598058648428519973216388921163*y^13 + 89189249081195279004663664012994627839270887413928/428190582207958343700804427079223275278713727*y^12 + 16912059307138337130803348293730894782440409858299/428190582207958343700804427079223275278713727*y^11 - 82534563792583848294507758298882572481702467908264/428190582207958343700804427079223275278713727*y^10 - 321443856820123148757812233517826423134273711007285/428190582207958343700804427079223275278713727*y^9 - 368072733118969863775756631277415450139027174423562/428190582207958343700804427079223275278713727*y^8 - 24643340371545936715762372366556009119003128494201/428190582207958343700804427079223275278713727*y^7 + 284965274634124020642791960172380167134429625912252/428190582207958343700804427079223275278713727*y^6 + 311730175547874937208113834468984966007191974206827/428190582207958343700804427079223275278713727*y^5 + 174132640171897122808921802190978131254812075163424/428190582207958343700804427079223275278713727*y^4 + 58919149248635889575242297140919444094309655125184/428190582207958343700804427079223275278713727*y^3 + 11946630657945178495579583293083378001493567544744/428190582207958343700804427079223275278713727*y^2 + 41898108087219554894782659491429829739384774938/14765192489929598058648428519973216388921163*y + 38221137504360102133140437547457919011188355529/428190582207958343700804427079223275278713727

-11359746014600900686115434086496714717882829674/68938683735481293335829512759754947319872910047*y^21 - 107713858581127873572726628318036465865935499160/68938683735481293335829512759754947319872910047*y^20 - 90126027472527866259970365014056997056828429391/68938683735481293335829512759754947319872910047*y^19 - 625814011599713127288722086289235910545129274057/68938683735481293335829512759754947319872910047*y^18 - 364581221871885587247821673525414868801382118885/9848383390783041905118501822822135331410415721*y^17 + 41675254755686557105154115990707569614081216701/2997334075455708405905630989554562926950996089*y^16 - 9324916995490194976452711611680015720195890502946/68938683735481293335829512759754947319872910047*y^15 - 2104551894592050786466093618743426103597261188869/9848383390783041905118501822822135331410415721*y^14 - 2298857220667069021396662384669542070234890084869/2377195990878665287442396991715687838616307243*y^13 - 111144073771340748589323987902637421897538032598095/68938683735481293335829512759754947319872910047*y^12 + 26550173658891380289659983895346228421694698555269/68938683735481293335829512759754947319872910047*y^11 + 164490947445407862963805499787202012021742118797910/68938683735481293335829512759754947319872910047*y^10 + 22720982908922777914807762342461889553076600792289/2997334075455708405905630989554562926950996089*y^9 + 20871849907791953113323998805875540011404925960977/2997334075455708405905630989554562926950996089*y^8 - 93984170714515950177173877163593626517701642587417/68938683735481293335829512759754947319872910047*y^7 - 73549565438074286989262947021499798980699410392432/9848383390783041905118501822822135331410415721*y^6 - 515380871659057465043942158745078584096234875226743/68938683735481293335829512759754947319872910047*y^5 - 277902519684052821025140427789093132618075956963205/68938683735481293335829512759754947319872910047*y^4 - 91992601832464604054438807357834278014079806893120/68938683735481293335829512759754947319872910047*y^3 - 17151434190760278189290965631174296260498002858072/68938683735481293335829512759754947319872910047*y^2 - 46843568060121981222068994505479174616084930160/2377195990878665287442396991715687838616307243*y + 46291852593213302815153611726031326886509078886/68938683735481293335829512759754947319872910047

-245808362368992290163009513124847309924922858/428190582207958343700804427079223275278713727*y^21 - 2268068485177190936143177291389887873213863819/428190582207958343700804427079223275278713727*y^20 - 1375994533055445930233442013928020839412010746/428190582207958343700804427079223275278713727*y^19 - 13313348646917214269598611384782438102188229765/428190582207958343700804427079223275278713727*y^18 - 52701907834143288916632350440366580653300846529/428190582207958343700804427079223275278713727*y^17 + 32552289631330648455348977518482071890010619442/428190582207958343700804427079223275278713727*y^16 - 217113534727992895980042047585294203336307394354/428190582207958343700804427079223275278713727*y^15 - 287323195102241209408767951804123078887169256249/428190582207958343700804427079223275278713727*y^14 - 47919707655223908099235257491071516764358235859/14765192489929598058648428519973216388921163*y^13 - 2149778836550548326147678262507636323296503183918/428190582207958343700804427079223275278713727*y^12 + 896951325632769085505056056297555805409296798625/428190582207958343700804427079223275278713727*y^11 + 2594458484186295875716579830648315505674637368990/428190582207958343700804427079223275278713727*y^10 + 9154271996817833162185451382467393507626866727903/428190582207958343700804427079223275278713727*y^9 + 6664383446144546412045588636988436321753374270290/428190582207958343700804427079223275278713727*y^8 - 4471389687770571006874971629885124627755730646426/428190582207958343700804427079223275278713727*y^7 - 8007118906362351174656007525216942337058659772454/428190582207958343700804427079223275278713727*y^6 - 5068308045971064573927748128794590685511103945422/428190582207958343700804427079223275278713727*y^5 - 1655002416629028897236860712953739400979758491013/428190582207958343700804427079223275278713727*y^4 - 289624374574882446346526978074932750295569106609/428190582207958343700804427079223275278713727*y^3 - 31287358987143605719734523231449998572013807203/428190582207958343700804427079223275278713727*y^2 - 124885676810797865373123713045730497456287117/14765192489929598058648428519973216388921163*y - 718953152928374989989055949566238609226815736/428190582207958343700804427079223275278713727

7061104797521701554326348195668444318028579725/428190582207958343700804427079223275278713727*y^21 + 69386638400345300057229351639253314126312381583/428190582207958343700804427079223275278713727*y^20 + 79761719294111411511764556761322576107045436977/428190582207958343700804427079223275278713727*y^19 + 416888281703025938792473153866083661208697177796/428190582207958343700804427079223275278713727*y^18 + 1749470399383937060919061305586937428794505391442/428190582207958343700804427079223275278713727*y^17 + 35544868636021797060217698405356002712335505925/428190582207958343700804427079223275278713727*y^16 + 5924980115708420321078986704534739226247161869188/428190582207958343700804427079223275278713727*y^15 + 11831054447886609387989372201756280787368967499218/428190582207958343700804427079223275278713727*y^14 + 1582767400620902921569528407377747786789369088284/14765192489929598058648428519973216388921163*y^13 + 87039470244644730678515985750486991515974384230010/428190582207958343700804427079223275278713727*y^12 + 17809010632771106216308404350028450587849706656924/428190582207958343700804427079223275278713727*y^11 - 79940105308397552418791178468234256976027830539274/428190582207958343700804427079223275278713727*y^10 - 312289584823305315595626782135359029626646844279382/428190582207958343700804427079223275278713727*y^9 - 361408349672825317363711042640427013817273800153272/428190582207958343700804427079223275278713727*y^8 - 29114730059316507722637343996441133746758859140627/428190582207958343700804427079223275278713727*y^7 + 276958155727761669468135952647163224797370966139798/428190582207958343700804427079223275278713727*y^6 + 306661867501903872634186086340190375321680870261405/428190582207958343700804427079223275278713727*y^5 + 172477637755268093911684941478024391853832316672411/428190582207958343700804427079223275278713727*y^4 + 58629524874061007128895770162844511344014086018575/428190582207958343700804427079223275278713727*y^3 + 11915343298958034889859848769851928002921553737541/428190582207958343700804427079223275278713727*y^2 + 41773222410408757029409535778384099241928487821/14765192489929598058648428519973216388921163*y + 37502184351431727143151381597891680401961539793/428190582207958343700804427079223275278713727

1330092920441872205689248569083808561176637757/2140952911039791718504022135396116376393568635*y^21 + 12856581795522851574968189897559243724006411948/2140952911039791718504022135396116376393568635*y^20 + 12957449374978090530325720254724612067034271828/2140952911039791718504022135396116376393568635*y^19 + 76429648045845195442099387202563176697128913579/2140952911039791718504022135396116376393568635*y^18 + 317233619409354908885137014915925133714110239437/2140952911039791718504022135396116376393568635*y^17 - 44310525120509622318930248235707244899124546856/2140952911039791718504022135396116376393568635*y^16 + 1122726673483214160991013821808548483628193750481/2140952911039791718504022135396116376393568635*y^15 + 2048087461639246409222487026123344708222547780266/2140952911039791718504022135396116376393568635*y^14 + 286817456587245225795759105855410209187146162904/73825962449647990293242142599866081944605815*y^13 + 15053295530717693883010555760727919770309373430377/2140952911039791718504022135396116376393568635*y^12 + 930404943070447970963366775030667481806084629688/2140952911039791718504022135396116376393568635*y^11 - 15232545618094045727400652400587329273404119876044/2140952911039791718504022135396116376393568635*y^10 - 11272317597851467152581136309491715320876430604926/428190582207958343700804427079223275278713727*y^9 - 58936206393748477919955205120549460279806459771029/2140952911039791718504022135396116376393568635*y^8 + 4051084068125067853979731003872724217387676730981/2140952911039791718504022135396116376393568635*y^7 + 51634442033017175416276315860417335417610730267657/2140952911039791718504022135396116376393568635*y^6 + 49294351559902209261194690569366359864972156944277/2140952911039791718504022135396116376393568635*y^5 + 4863726403009085453375104653329767015556493397522/428190582207958343700804427079223275278713727*y^4 + 7119814908012592403315572108527211685900176901622/2140952911039791718504022135396116376393568635*y^3 + 1181821264640914018998617373348154031035114134763/2140952911039791718504022135396116376393568635*y^2 + 3120414159122114878181599888930246037413279397/73825962449647990293242142599866081944605815*y + 4140102350873362134982666647081867868341746562/2140952911039791718504022135396116376393568635

58960235565111091098404378824927497393147321/428190582207958343700804427079223275278713727*y^21 + 515802657223428297844571667096383974265524242/428190582207958343700804427079223275278713727*y^20 + 69482819034175119166248761822645364263105385/428190582207958343700804427079223275278713727*y^19 + 3032841018412541344666956233872935721825497884/428190582207958343700804427079223275278713727*y^18 + 11101433882350788877288635605754364647331927582/428190582207958343700804427079223275278713727*y^17 - 13879117804147930709905687993960546270358216327/428190582207958343700804427079223275278713727*y^16 + 55714318352440944295750863046396550901147330163/428190582207958343700804427079223275278713727*y^15 + 43743913410812566524302112128248252753926004631/428190582207958343700804427079223275278713727*y^14 + 10351131212732959071502141079300125046693041143/14765192489929598058648428519973216388921163*y^13 + 354873533528410848455678869440375880125053909433/428190582207958343700804427079223275278713727*y^12 - 464779157911705422580652220270684544154690442374/428190582207958343700804427079223275278713727*y^11 - 527985376975262241695610934388022070235529312942/428190582207958343700804427079223275278713727*y^10 - 1911163536079603675529804532572812065995493499784/428190582207958343700804427079223275278713727*y^9 - 551525964250741696036137498364944418575128349530/428190582207958343700804427079223275278713727*y^8 + 1845338239773355812816908092396670349165307712912/428190582207958343700804427079223275278713727*y^7 + 1443126620438507973157881880456033730612426018054/428190582207958343700804427079223275278713727*y^6 + 332525761862949790480913851362349538787736785007/428190582207958343700804427079223275278713727*y^5 - 186015871236409168115490400460629699219198427125/428190582207958343700804427079223275278713727*y^4 - 135962537118688265263520646548947721450520343083/428190582207958343700804427079223275278713727*y^3 - 33028563269474538832767199412889052376860193074/428190582207958343700804427079223275278713727*y^2 - 153759022564958439105788441816021524213598230/14765192489929598058648428519973216388921163*y + 132750113037952303078160719541677459821562291/428190582207958343700804427079223275278713727


# A Gluing Matrix
{{2,0,0,-2,-2,0,-2,-2},{0,1,0,-2,-2,0,-2,-2},{0,0,1,0,-1,-1,0,-1},{-2,-2,0,6,5,-1,6,5},{-2,-2,-1,5,5,-1,5,5},{0,0,-1,-1,-1,1,-1,0},{-2,-2,0,6,5,-1,7,6},{-2,-2,-1,5,5,0,6,7}}

# B Gluing Matrix
{{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,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}}

# nu Gluing Vector
{-2, -3, -1, 8, 7, -1, 9, 9}

# f Combinatorial flattening
{5, 7, -3, 7, -3, -3, -3, 4}

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

# 1 Loop Invariant
-6387360541752583922892764144808591280114083865/428190582207958343700804427079223275278713727*y^21 - 63815449813949145485365469261960705568673341021/428190582207958343700804427079223275278713727*y^20 - 82265490628979270046617002020666454013982335336/428190582207958343700804427079223275278713727*y^19 - 774160335329150026775991052633100024745525551341/856381164415916687401608854158446550557427454*y^18 - 1642819027504315878400697243569301398922841991307/428190582207958343700804427079223275278713727*y^17 - 280738748593439014428978723890267243459926266819/428190582207958343700804427079223275278713727*y^16 - 10637814347580868376861542781890568808900964038003/856381164415916687401608854158446550557427454*y^15 - 23188176248353606359554474436478171835221365734515/856381164415916687401608854158446550557427454*y^14 - 2972547597637446000155347077699503181508554190591/29530384979859196117296857039946432777842326*y^13 - 85272315207984273368780846618203107324103623506484/428190582207958343700804427079223275278713727*y^12 - 27820287998033914875812235050889028746956694645634/428190582207958343700804427079223275278713727*y^11 + 71795299720366855189005936205954762307527213206693/428190582207958343700804427079223275278713727*y^10 + 294427522256151004625823511071640822667182235733638/428190582207958343700804427079223275278713727*y^9 + 743114160571530212675333636861881505800280960701887/856381164415916687401608854158446550557427454*y^8 + 72322637254567831086562557168157954198478457086962/428190582207958343700804427079223275278713727*y^7 - 253737730097837034946474009594167045759787277922183/428190582207958343700804427079223275278713727*y^6 - 635333950943742501449901213072962525486820416628915/856381164415916687401608854158446550557427454*y^5 - 195563030837566280859639606160281689133764443839220/428190582207958343700804427079223275278713727*y^4 - 73024012259905556594554681451488611238546004841174/428190582207958343700804427079223275278713727*y^3 - 33242712194812868049842050356447536568112454362047/856381164415916687401608854158446550557427454*y^2 - 137213990949355048233879537207426431845779791521/29530384979859196117296857039946432777842326*y - 132841570493664850854356936579879978709865547781/856381164415916687401608854158446550557427454

# 2 Loop Invariant
96366557727742518205797837365941703721114780118458667043214289491278454653378710467033922694112919538106711464713/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^21 + 33192579790525133804482821742728244415255403005271375974459741416951067626688735992710766814815262292397962947881/21696613910335817131297388612784955428427888181584278824234153651205003086688514909800605673839835746012602454916*y^20 + 921138623201262536470985582869775110516160976447722068588207572073253189857887068375598317850597513344910763258813/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^19 + 1385245825762867887275730779729775676414515783947693567272724952608958515074912404550552131604418591556081087933455/151876297372350719919081720289494687998995217271089951769639075558435021606819604368604239716878850222088217184412*y^18 + 22887908340898865714060805739450437836913869229896684265587153687528917262985622492614293124391471669877212757844563/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^17 - 892979999208060987750940156699538815283026855103161438908848074171776328143537037850792903433469046147220468921767/151876297372350719919081720289494687998995217271089951769639075558435021606819604368604239716878850222088217184412*y^16 + 40998137402469600320152968553664305483502709847136097473794537058028476958648948190039561565505170148730547809397911/303752594744701439838163440578989375997990434542179903539278151116870043213639208737208479433757700444176434368824*y^15 + 146510436148508902832925663739446587435586119113975742111960455896034017324423719651507471965817427659712360689129563/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^14 + 12527598101006557804769701032267151506920321490494390570799169072714988091511812193181059759720914114298668966328808/12656358114362559993256810024124557333249601439257495980803256296536251800568300364050353309739904185174018098701*y^13 + 180252900979335047452000762245680588265321436293516813413532797480604183474646406461513313948709790656669750397385367/101250864914900479946054480192996458665996811514059967846426050372290014404546402912402826477919233481392144789608*y^12 + 2788057311404555185049243335239956310110386217419208380166706412629998680584096073059820331925331939679655679345963/28928818547114422841729851483713273904570517575445705098978871534940004115584686546400807565119780994683469939888*y^11 - 359327129607435416609814594228804276114481854442011133125608002077128553451104458388589510653995668736461580963952951/202501729829800959892108960385992917331993623028119935692852100744580028809092805824805652955838466962784289579216*y^10 - 1354127232368103039934144672480238565456497425764568411397398487638233640670890373830879681619878842642704149737834749/202501729829800959892108960385992917331993623028119935692852100744580028809092805824805652955838466962784289579216*y^9 - 4217810703181351597180216786820177990801077626081069699538780927933142269339510073991525371817079034024209758414518309/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^8 + 93721092576089609042537296293002939548555062392888675778854063574685219632848040874305294411106487447431730578586949/202501729829800959892108960385992917331993623028119935692852100744580028809092805824805652955838466962784289579216*y^7 + 226743913034538995709765361044242485222198370543801245411750737398874780009014846934406030283424227879129378060435392/37969074343087679979770430072373671999748804317772487942409768889608755401704901092151059929219712555522054296103*y^6 + 3522502405643648732808340453894827008412822432911466580190046370272315294450595806505573340150226444733878849109448713/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^5 + 300126031995898581716190667773004658335378624620943337780076293913099608850788487659729278327519408695366344991019847/101250864914900479946054480192996458665996811514059967846426050372290014404546402912402826477919233481392144789608*y^4 + 563665910315310890184222390708471155624078539247221356044070263512480562804448207331316571858186766093422179434584229/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^3 + 106318133161987473102392096657400223652711650375933007365997786308813462214822700085302535114260007960541263387936841/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y^2 + 10294769304887101447160090375415445449153574235587012427761222567088396414812222699425674818025212320202113093897935/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648*y + 1584733496995839549277678573890793242744578618457175284214541516328285562387126006349466918578310554769155216869259/607505189489402879676326881157978751995980869084359807078556302233740086427278417474416958867515400888352868737648

# 3 Loop Invariant
-20215893552921844518163012686456409363080041406048105421358232585989017144386306561773688237544099635544571613881980230812642989683720060282095194535/454894385039088787892129309374376875118008163233531711700536994339070553564001238807502522156297057032218968509769174150237759712490814725427187535088*y^21 - 777172421930712065531864322347803264337584885334020761265666668323464124826210531622912258890730744531446257243542754438960105444906728503283253897585/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^20 - 26739842095152191743417860964952566571300050227758910358091620886351537197726283015492226880369805373550324799054670348904690272700460724100387081987/64984912148441255413161329910625267874001166176218815957219570619867221937714462686786074593756722433174138358538453450033965673212973532203883933584*y^19 - 2319802856127301271745013258272560211115899715890887633883226735645755915731905807548369127479296391787601863332630422424934978251326797145655997578533/909788770078177575784258618748753750236016326467063423401073988678141107128002477615005044312594114064437937019538348300475519424981629450854375070176*y^18 - 4762455156214987432730001664813569010199710943498008299686583160147353074540545527020957560763607013070811771569098167350401669177245407007945642936475/454894385039088787892129309374376875118008163233531711700536994339070553564001238807502522156297057032218968509769174150237759712490814725427187535088*y^17 + 1776220179800371458680571119985260094416300374580297896646277433974408962757666253944286766455155527361519666429513105762765585552885332529336037887779/909788770078177575784258618748753750236016326467063423401073988678141107128002477615005044312594114064437937019538348300475519424981629450854375070176*y^16 - 8653122047885580248687583783246052653261566672762942719398318872115102673101453418419883866715385471504027808937461681085456322431851126205599244506893/227447192519544393946064654687188437559004081616765855850268497169535276782000619403751261078148528516109484254884587075118879856245407362713593767544*y^15 - 120108283811487892467847327495275739855225071900984662584624331376880316385119935773172242811631590601593508724488134187651672240037341762978635298112795/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^14 - 17311786325159515774408925929484995517208615833328702826144886461816075318000321690537495249222969131465915041889022025615692084728218821266695149525347/62744053108839832812707490948189913809380436308073339544901654391595938422620860525172761676730628556168133587554368848308656512067698582817543108288*y^13 - 222893305518320055586136723552755966238510422963865170784743377410556610127825508017251506197312874926248050015330266659415128037717138455012940969594085/454894385039088787892129309374376875118008163233531711700536994339070553564001238807502522156297057032218968509769174150237759712490814725427187535088*y^12 - 13588016489543572934093046850786444614630908548011549746065962904558067209448718099772579472805474455108617563741347932639168893253854350377297144476297/909788770078177575784258618748753750236016326467063423401073988678141107128002477615005044312594114064437937019538348300475519424981629450854375070176*y^11 + 898367321389950216908212174526501670791570780640828533582479056584652980467350651268943420818846477600482413338328184190601133588792908946883635925768497/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^10 + 3400977750405792396474367686774327857483633833247760510987775666567791058772374991787757945388073274589000188373119717729347679706150562266691757169858421/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^9 + 3455182851845297676654687783006272589310955034298278911756865236345953473213020376737319615108028425959085720369113975131513118124013234766300944004894129/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^8 - 19962608322535739265825342462425609707926297155890981397250337722194438416695385410117094921550247778802462204063252109397491997080032671581475198054439/129969824296882510826322659821250535748002332352437631914439141239734443875428925373572149187513444866348276717076906900067931346425947064407767867168*y^7 - 188450980354282203409660575169266496447222924763861062203262115036821925725379516695347569555841436727878986443385510523393633017631275604217913467872899/113723596259772196973032327343594218779502040808382927925134248584767638391000309701875630539074264258054742127442293537559439928122703681356796883772*y^6 - 731709744381190152916203642145359134938898272469839542627811316072065297411025817680958820251548386725103701447623853253949875337779984331622816024900779/454894385039088787892129309374376875118008163233531711700536994339070553564001238807502522156297057032218968509769174150237759712490814725427187535088*y^5 - 1493048008263544182995508861106478574424995473818084771612728562292285377632584245736815303908201869288697481414937202170464611343626257056533924884484891/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352*y^4 - 233636548905449592038922382814452164675605910527065713393046001135738711259798414897713692318849249369854636434308532072998811148392174713142930276785967/909788770078177575784258618748753750236016326467063423401073988678141107128002477615005044312594114064437937019538348300475519424981629450854375070176*y^3 - 42958826889364052247196125316195074460024290541595143888637022419064471877935223513115491400335006509682274920891012489796049795327192319163228061983567/909788770078177575784258618748753750236016326467063423401073988678141107128002477615005044312594114064437937019538348300475519424981629450854375070176*y^2 - 275779165161615344085919638583149747551276489713472736107596686008145187818353163852475211126316855704200694201793242926064672648314255372369117828943/62744053108839832812707490948189913809380436308073339544901654391595938422620860525172761676730628556168133587554368848308656512067698582817543108288*y - 204019268072579668666395377781603858565082023257368155426634701750666914047215996228313468237278674853382551360736412000013950338476715197826691666545/1819577540156355151568517237497507500472032652934126846802147977356282214256004955230010088625188228128875874039076696600951038849963258901708750140352

# 4 Loop Invariant
2546838339661215165288390759436699290640904558669157325947739771017100598225318196347838698928315386912631188269004028700915563166719063448058897491130701600912936397228993574655219647237785978795662690732351289516843953/26737661155191104719138484487442292116711862077415094740692497595338387523554674363188037318786557559996470985633670623340062004220617206867534482533698479011545731389196131558529749480079738978716043622641666936134320640*y^21 + 113365270398197424997785079590337548301074825171645003149420233149995806636999545514922020894258621324947229409330168535599518637998833037122923478384672175158216904391623569155696386566919668503795983031560281915061888953/124775752057558488689312927608064029877988689694603775456564988778245808443255147028210840821003935279983531266290462908920289353029546965381827585157259568720546746482915280606472164240372115234008203572327779035293496320*y^20 + 458077057621434380707025404104503107709129715451017744551851753691753084309150958712351739752520555674427893520013996351325801294859218056906864164635544153803286688646169786495193553925990917085070290389434834653364428687/561490884259013199101908174236288134450949103625716989554542449502106137994648161626948783694517708759925890698307083090141302088632961344218224133207668059242460359173118762729124739081674518553036916075475005658820733440*y^19 + 63229097849695670102336175220526248243006246332206794097543453793824530843918212194536353301735842060486323653064027296537980255889643005128220016427123413668159862914410865845330376172673078212497788697054138518388278817/11697726755396108314623086963256002801061439658869103949052967697960544541555170033894766326969118932498456056214730897711277126846520028004546336108493084567551257482773307556856765397534885803188269084905729284558765280*y^18 + 275182627374748873939917194722397829083805209733592687409317293866137855186929770633954342405132112474296665058670129168196866261788891981739076618799847695358995542975736120688516035225229546293620430776566171900603915615/12477575205755848868931292760806402987798868969460377545656498877824580844325514702821084082100393527998353126629046290892028935302954696538182758515725956872054674648291528060647216424037211523400820357232777903529349632*y^17 - 162549914107885079675917366584569732284978064425138040694330754731745590416504193564026532949478929685036720079329335008818813812380467019461347108589790238750220177176386601533373724371004882128864209429015855922975572583/28074544212950659955095408711814406722547455181285849477727122475105306899732408081347439184725885437996294534915354154507065104431648067210911206660383402962123017958655938136456236954083725927651845803773750282941036672*y^16 + 92056599071381961484530593680218212774235355654487998996069726211491420731533820042162417272811702710823979932237256008538751422588395514029477278650696909059405081400805088457479329845854896348236754769135644326189166285611/1122981768518026398203816348472576268901898207251433979109084899004212275989296323253897567389035417519851781396614166180282604177265922688436448266415336118484920718346237525458249478163349037106073832150950011317641466880*y^15 + 76215929674469261840261138725179881790729644823031268086733841714671085933192266303249383992532393657147573693502946408322231871956822942451467942377593477184269747332921069112959760216637023570053382478981812809662390404377/561490884259013199101908174236288134450949103625716989554542449502106137994648161626948783694517708759925890698307083090141302088632961344218224133207668059242460359173118762729124739081674518553036916075475005658820733440*y^14 + 22508904538175853961595382364492043161379186681285344599590660604851358199710289719846335020869389667011393645788314541945627896390446227585263965381511820087884703363132510836061705190658997623245496630778583141510260665247/38723509259242289593235046499054354100065455422463240658933962034628009516872287008755088530656393707581095910228074695871813937147100782359877526428115038568445542011939225015801706143563759900209442487963793493711774720*y^13 + 25171048783013192523106098066856946349635445017019836154604611382599624572229211359482469804633570750089890643053561843811482556161776548774876014642732664110061843692748602026861970738075404710478381119783424089787656724911/24955150411511697737862585521612805975597737938920755091312997755649161688651029405642168164200787055996706253258092581784057870605909393076365517031451913744109349296583056121294432848074423046801640714465555807058699264*y^12 - 46235013146773093869058625329413886725254415920804594443016602633684800241873055153513962299888872982235423065222865227990463919143837675618603936904392915538061312662560056164697523055263389439308068960656727454791961913787/1122981768518026398203816348472576268901898207251433979109084899004212275989296323253897567389035417519851781396614166180282604177265922688436448266415336118484920718346237525458249478163349037106073832150950011317641466880*y^11 - 1181006300025606007561356169321902509189793279820216558115877152706787644387820863478231310504119624828705333973837697789523940850103134296965044519670708278860784928982806870071860118528504307762417284975215430792672680139101/1122981768518026398203816348472576268901898207251433979109084899004212275989296323253897567389035417519851781396614166180282604177265922688436448266415336118484920718346237525458249478163349037106073832150950011317641466880*y^10 - 2201796441417564350701816643507891599362287898166324839063466030497059025274190776168128244293407596167452163628448173736210658331710356411282352682815533184274796752655879593374692317014483594147141839268113899831863784424371/561490884259013199101908174236288134450949103625716989554542449502106137994648161626948783694517708759925890698307083090141302088632961344218224133207668059242460359173118762729124739081674518553036916075475005658820733440*y^9 - 4250435107889809984919085169611964848628901708225846514397600965763337962960436418750580919011989183702154266049367007301111946695946750947650745955795969421523971117295647344926258562400590890352515409225791270258089138053239/1122981768518026398203816348472576268901898207251433979109084899004212275989296323253897567389035417519851781396614166180282604177265922688436448266415336118484920718346237525458249478163349037106073832150950011317641466880*y^8 + 679600336319486627562856957646316735189479964146600468180810015672930237375439587114002338018055684563428162660113622897594112768543617200416007585029992077985029296232888431478925217775617860379174953077870852751529023051003/1122981768518026398203816348472576268901898207251433979109084899004212275989296323253897567389035417519851781396614166180282604177265922688436448266415336118484920718346237525458249478163349037106073832150950011317641466880*y^7 + 97805395610947844738229765233928393892956029220543231051835600354596353964101235082741848927589945095450211251680694680721216295250776116987866113074966653592539721858036473953902270024140019553976333573642847560390866375093/28074544212950659955095408711814406722547455181285849477727122475105306899732408081347439184725885437996294534915354154507065104431648067210911206660383402962123017958655938136456236954083725927651845803773750282941036672*y^6 + 1780428040624758061070740597186178560285605013292759280670908777327580901184827479245318240270603498411654641061767176748181450770489550905785021539110110360077083347533519364764096478980588626502055426061906921581624224567253/561490884259013199101908174236288134450949103625716989554542449502106137994648161626948783694517708759925890698307083090141302088632961344218224133207668059242460359173118762729124739081674518553036916075475005658820733440*y^5 + 12297006481388719650953210717519970135316342925667017733210690410980422265506958235512255967225652582129022120296227590829411293286574972039358386345457671276022665399248895999262439611861209198917524919781258423873748271813/8021298346557331415741545346232687635013558623224528422207749278601516257066402308956411195635967267998941295690101187002018601266185162060260344760109543703463719416758839467558924844023921693614813086792500080840296192*y^4 + 169679775132769145687134736154878908712997598469566693604632833738417873057004355103434846191461230851574739584213125603248123335176531022605685287692568265572248703570497948243353015548166108915527467176563724019688616360341/374327256172675466067938782824192089633966069083811326369694966334737425329765441084632522463011805839950593798871388726760868059088640896145482755471778706161640239448745841819416492721116345702024610716983337105880488960*y^3 + 29303088152309196129195666164839394818849957387743451739791025053098016657757604792364343625778331573758505810784451874753711214757902411841423023994156251826413972066309319628577676122448185824814248394189945969663106959631/374327256172675466067938782824192089633966069083811326369694966334737425329765441084632522463011805839950593798871388726760868059088640896145482755471778706161640239448745841819416492721116345702024610716983337105880488960*y^2 + 815397053606470788734367170254999734005864270783521253941807725466837881840417538685179547253311021467509819171574141430181041607081190706599791485917182283683543382473734449088043183837960825271325395694686587672452421/122931775426165998708682687298585251111318906103057906853758609633739712751975514313508217557639345103432050508660554590069250594117780261459928655327349328788716006387108650843814940138297650476855372977662836487973888*y + 11853418134856617001216379019714012158560257814620237280459370911015766610486268322500798474625712936023642864907965330634121161073949898936193089509920879886871846656862161124582141699840691918117153823463179144996879837/56149088425901319910190817423628813445094910362571698955454244950210613799464816162694878369451770875992589069830708309014130208863296134421822413320766805924246035917311876272912473908167451855303691607547500565882073344