# Manifold: Census Knot K8_164

# Number of Tetrahedra: 8

# Number Field
x^20 + 22*x^19 + 205*x^18 + 1134*x^17 + 4203*x^16 + 9718*x^15 + 9309*x^14 - 15378*x^13 - 49661*x^12 + 12566*x^11 + 202490*x^10 - 20168*x^9 - 404013*x^8 - 30902*x^7 + 496748*x^6 + 156776*x^5 - 365198*x^4 - 232728*x^3 + 93095*x^2 + 123057*x + 31529 

# Approximate Field Generator
-0.606118851133446 + 0.509263668526197*I

# Shape Parameters
8150053540283417353320001588366951608234843623013623970226941/251669906045112730637837498137402048457897334569014243408521900215*y^19 + 170222394051831805220448797617153752896308450356728521772418153/251669906045112730637837498137402048457897334569014243408521900215*y^18 + 1480103716883801489988675671290910630740839075004145804279761378/251669906045112730637837498137402048457897334569014243408521900215*y^17 + 398527706802963131346791076613960165642403446255628727358786938/13245784528690143717780920954600107813573543924684960179395889485*y^16 + 5127795429892491969853737787431540713153219876286708289465726684/50333981209022546127567499627480409691579466913802848681704380043*y^15 + 49761680063053419968602678587991056277279966289832357177762244193/251669906045112730637837498137402048457897334569014243408521900215*y^14 + 17731392514224420825603370349590506237570917629977349553180510877/251669906045112730637837498137402048457897334569014243408521900215*y^13 - 148878768300791863580616533967389955716615954427828834097917365586/251669906045112730637837498137402048457897334569014243408521900215*y^12 - 233111688231878516935475540943504900327985046901412722666579228072/251669906045112730637837498137402048457897334569014243408521900215*y^11 + 397568553853409867058504369889885661678651294408902044499760532959/251669906045112730637837498137402048457897334569014243408521900215*y^10 + 1253788680672854057687593051573413535698845578114589589340184603534/251669906045112730637837498137402048457897334569014243408521900215*y^9 - 1619443226563134986470424421315440817481758324098762244136687896769/251669906045112730637837498137402048457897334569014243408521900215*y^8 - 1675805519359033472243541862002229636142671441269726963693144129712/251669906045112730637837498137402048457897334569014243408521900215*y^7 + 1879973896153125255720004481599116515086532028646740303125714257226/251669906045112730637837498137402048457897334569014243408521900215*y^6 + 123569859389498274179951129464012439494055752867308998557773080086/13245784528690143717780920954600107813573543924684960179395889485*y^5 - 318087743537372233416933630608807842814743509329107286414860541540/50333981209022546127567499627480409691579466913802848681704380043*y^4 - 1730512501110430546574281343537493917925366075924629215764857631038/251669906045112730637837498137402048457897334569014243408521900215*y^3 + 228368809691571018734004269066892714946510415753262892822575609759/251669906045112730637837498137402048457897334569014243408521900215*y^2 + 1179454656693462252186131189739615855308470994242882229892911374669/251669906045112730637837498137402048457897334569014243408521900215*y + 62658748713478322680244255870555098291388898778544296703367026121/251669906045112730637837498137402048457897334569014243408521900215

44563269851803204451409615219094136833857450328122247878018050916/3424535991321586638478900185576211753884114184491415297868618596495033*y^19 + 956605161984787235021423382723938505787667489832683663326404384056/3424535991321586638478900185576211753884114184491415297868618596495033*y^18 + 209653319446891823873432866338348131028399438294608800780973830257/83525268081014308255582931355517359850832053280278421899234599914513*y^17 + 45291875595971710697850108348553630118235531436738642922709378559598/3424535991321586638478900185576211753884114184491415297868618596495033*y^16 + 156826366655594715568971945005352354536258056096388818746960198863082/3424535991321586638478900185576211753884114184491415297868618596495033*y^15 + 313166352228508040351439294988785744234979134272548745534140604539650/3424535991321586638478900185576211753884114184491415297868618596495033*y^14 + 107178478492849087181086622878294520444586291852918565670073179851198/3424535991321586638478900185576211753884114184491415297868618596495033*y^13 - 1095047830491150721592461691454825502699055789325452734001241573119082/3424535991321586638478900185576211753884114184491415297868618596495033*y^12 - 2070128936603132661370131256332045072408595820529563716304726345038382/3424535991321586638478900185576211753884114184491415297868618596495033*y^11 + 1915977540409406111212761263689503349195784246480538191515543790069002/3424535991321586638478900185576211753884114184491415297868618596495033*y^10 + 9624477790141594466567362559191146391626806110573030600108647012290422/3424535991321586638478900185576211753884114184491415297868618596495033*y^9 - 5568517912340774904649795113128321849829198504722751568606595209538464/3424535991321586638478900185576211753884114184491415297868618596495033*y^8 - 20866276312169057692354977304921724831046483671126110390410348934658482/3424535991321586638478900185576211753884114184491415297868618596495033*y^7 + 7102473509103229625552413971316642607492340919224067863789577916514236/3424535991321586638478900185576211753884114184491415297868618596495033*y^6 + 29141439532313607657310118828270699661757449654685703637478239737862028/3424535991321586638478900185576211753884114184491415297868618596495033*y^5 - 1205593990458568939214424730985085949767236107741352009116445009225327/3424535991321586638478900185576211753884114184491415297868618596495033*y^4 - 27183740069994740216846611256969025444107505879510301086223935790688450/3424535991321586638478900185576211753884114184491415297868618596495033*y^3 - 8467216473083621846303902915560035832961978349910170051576577310953416/3424535991321586638478900185576211753884114184491415297868618596495033*y^2 + 12621706600930967379074845810264241718344982843905023598483633868164943/3424535991321586638478900185576211753884114184491415297868618596495033*y + 11017172367951605439900516389053119410778337431580734284713065306524928/3424535991321586638478900185576211753884114184491415297868618596495033

2068991667814046721371107310526545841807479092595387401976916041/83525268081014308255582931355517359850832053280278421899234599914513*y^19 + 45118422114112433974620842443117921238835779922611386180225489411/83525268081014308255582931355517359850832053280278421899234599914513*y^18 + 10126883626861991933100138497789208913300600893541601362642117219/2037201660512544103794705642817496581727611055616546875591087802793*y^17 + 2260898649849994040551184390539882438058850307662232161751629951372/83525268081014308255582931355517359850832053280278421899234599914513*y^16 + 8210028323809239674840804454183897517932663266598878518399238011773/83525268081014308255582931355517359850832053280278421899234599914513*y^15 + 18240579967094189108974473938183872001539766478076921779639781141440/83525268081014308255582931355517359850832053280278421899234599914513*y^14 + 14667004886487967048430747203625801057360104123378731883143657625299/83525268081014308255582931355517359850832053280278421899234599914513*y^13 - 37252695688945106630813789632763485325631693640728984611517605468332/83525268081014308255582931355517359850832053280278421899234599914513*y^12 - 98486720328742902895296149962684887759108530391747326745494171536611/83525268081014308255582931355517359850832053280278421899234599914513*y^11 + 47944458795795864245220414774241835448268420680092793807949746583204/83525268081014308255582931355517359850832053280278421899234599914513*y^10 + 422531052916805443276014517468428549205712078288594393603644801664394/83525268081014308255582931355517359850832053280278421899234599914513*y^9 - 123236390853765774732422206455398051618031066084620393391041555678710/83525268081014308255582931355517359850832053280278421899234599914513*y^8 - 863475105200288151904270158140387997862613644005244047105895964922113/83525268081014308255582931355517359850832053280278421899234599914513*y^7 + 88982688907909519973487656800875478493683457398404712316250156369366/83525268081014308255582931355517359850832053280278421899234599914513*y^6 + 1116157414495825811565300590164461106698038556075904199291578082475733/83525268081014308255582931355517359850832053280278421899234599914513*y^5 + 149243173135548278260722318125767913670882337282386438888518393193070/83525268081014308255582931355517359850832053280278421899234599914513*y^4 - 921030116027891393790115402566602609194237478596222923553667237857254/83525268081014308255582931355517359850832053280278421899234599914513*y^3 - 409872281185981708048127349471198850203638904500609381738783376585213/83525268081014308255582931355517359850832053280278421899234599914513*y^2 + 381583019939639310508763049425334827244690233030123781570118359368891/83525268081014308255582931355517359850832053280278421899234599914513*y + 291728146833367938872659363878561702217747539645665420340988113316725/83525268081014308255582931355517359850832053280278421899234599914513

948153216212678146540552581539412799377522145223780405497745/2649156905738028743556184190920021562714708784936992035879177897*y^19 + 20294753949603402078468873006516709528063741043507371005204504/2649156905738028743556184190920021562714708784936992035879177897*y^18 + 182230027931703630166430408897202390697124946290964242923788523/2649156905738028743556184190920021562714708784936992035879177897*y^17 + 965440066915428788971088596293602418936839849505209998826063108/2649156905738028743556184190920021562714708784936992035879177897*y^16 + 3398296789427131457397135561138147807188899117815601010985737210/2649156905738028743556184190920021562714708784936992035879177897*y^15 + 7122906516774033319664400050802530836608641240672585651268105542/2649156905738028743556184190920021562714708784936992035879177897*y^14 + 4324127478060363252260807276190332215147022016496929606465354158/2649156905738028743556184190920021562714708784936992035879177897*y^13 - 17806360226730034357773377333495764438041408174286066620906305115/2649156905738028743556184190920021562714708784936992035879177897*y^12 - 37309002861791947663192125663917539142719452200393221299006753550/2649156905738028743556184190920021562714708784936992035879177897*y^11 + 34468193757350194164504492075897594626458087832488700238887887196/2649156905738028743556184190920021562714708784936992035879177897*y^10 + 173989197870588373886598060595062554737878750772565259647196648110/2649156905738028743556184190920021562714708784936992035879177897*y^9 - 122557173721410727026659520019564009072593805284029133588107787906/2649156905738028743556184190920021562714708784936992035879177897*y^8 - 320326790771842191142670407981069158373079700288276494874114230130/2649156905738028743556184190920021562714708784936992035879177897*y^7 + 159571589913503282960360253713736330770925947655306154357080155539/2649156905738028743556184190920021562714708784936992035879177897*y^6 + 393616888929519581896952741622266037625676617370996642813780756570/2649156905738028743556184190920021562714708784936992035879177897*y^5 - 79496283901975468059118427077981982819699163313231715579164902893/2649156905738028743556184190920021562714708784936992035879177897*y^4 - 317430570003191864376433857993221722491387905376496713649798451061/2649156905738028743556184190920021562714708784936992035879177897*y^3 - 44036816399135010462470248576716539680627575969162528192079422707/2649156905738028743556184190920021562714708784936992035879177897*y^2 + 123121023136636915924624028362719756109080952498215648953978814957/2649156905738028743556184190920021562714708784936992035879177897*y + 56202185772678220126803110905968790479330477548704952230906200757/2649156905738028743556184190920021562714708784936992035879177897

9078783834403376552591237326919182484858109349571205572574549/251669906045112730637837498137402048457897334569014243408521900215*y^19 + 190657258874299067441924654324314448947303867713647109616761527/251669906045112730637837498137402048457897334569014243408521900215*y^18 + 1670134285425095783075851345542879976532647189640503762420399272/251669906045112730637837498137402048457897334569014243408521900215*y^17 + 453457783176249646670277775723610212823418335057511584186063137/13245784528690143717780920954600107813573543924684960179395889485*y^16 + 5888108048284165974192219369551795890309248807722808112980633689/50333981209022546127567499627480409691579466913802848681704380043*y^15 + 58137455892273911316452524436517446283487241656656475985662082892/251669906045112730637837498137402048457897334569014243408521900215*y^14 + 23547244958313471521261549541482973885180529193125324683767466888/251669906045112730637837498137402048457897334569014243408521900215*y^13 - 171628120632136272247749057936386283488565522261066857318860888929/251669906045112730637837498137402048457897334569014243408521900215*y^12 - 295154981066208444596685229930466547769572249442112845689888792353/251669906045112730637837498137402048457897334569014243408521900215*y^11 + 396515660699135122186174070055010495452627907109439128391068679556/251669906045112730637837498137402048457897334569014243408521900215*y^10 + 1455072946762699025288666629281256137446877997909823475905150950681/251669906045112730637837498137402048457897334569014243408521900215*y^9 - 1616922061611490822923331939718667583955112435394876297390152984521/251669906045112730637837498137402048457897334569014243408521900215*y^8 - 2131826850654963418772299170682832053684205166285107311053667188008/251669906045112730637837498137402048457897334569014243408521900215*y^7 + 1700695467628239794007932689201870127100382795565900707364603966234/251669906045112730637837498137402048457897334569014243408521900215*y^6 + 150956395343070221372040248529571390495070704762480018085821137364/13245784528690143717780920954600107813573543924684960179395889485*y^5 - 249174150338798580804695319306188015099756469102540046182816153656/50333981209022546127567499627480409691579466913802848681704380043*y^4 - 2125114470014650172537461598724356628827789102449977572165551134807/251669906045112730637837498137402048457897334569014243408521900215*y^3 - 420725422360777513678805641870594495339848227158428906384634302274/251669906045112730637837498137402048457897334569014243408521900215*y^2 + 940262389793178166567255179589116865763166252938643228200849652516/251669906045112730637837498137402048457897334569014243408521900215*y + 508632944116708596370663828217023665713933719159010793565807123004/251669906045112730637837498137402048457897334569014243408521900215

-1546188128769165981035571016535294675823428777490925918464903640912/19962539071362419673084320593968649004348860733986542833917069379568607*y^19 - 32583212265610389455997191849785943250303529488965768246858478187747/19962539071362419673084320593968649004348860733986542833917069379568607*y^18 - 6990600747849813061406643298632989627582511797764827137311305942768/486891196862498040806934648633381683032899042292354703266269984867527*y^17 - 1484378548377456628119595038372765809127358802344836612923466606077878/19962539071362419673084320593968649004348860733986542833917069379568607*y^16 - 5092321045429849216281166633564252250596265330330037164253313374288285/19962539071362419673084320593968649004348860733986542833917069379568607*y^15 - 10139883092790922167001133149769572647250069846330522446151066810446815/19962539071362419673084320593968649004348860733986542833917069379568607*y^14 - 4380355824684765308177521058995661688263738665601845889117568521285489/19962539071362419673084320593968649004348860733986542833917069379568607*y^13 + 29283787609310743621532734999764795262597877819973066399203895617052613/19962539071362419673084320593968649004348860733986542833917069379568607*y^12 + 51287741924318913888510299063300878533681283513643644221863024064104812/19962539071362419673084320593968649004348860733986542833917069379568607*y^11 - 67891241586244280096652203248261000617728967838256704647756611224809989/19962539071362419673084320593968649004348860733986542833917069379568607*y^10 - 254442344441199934736805920004338939142269194641128436907219228280346475/19962539071362419673084320593968649004348860733986542833917069379568607*y^9 + 270421083564572480507926114969662380127042657002949268648076533401398783/19962539071362419673084320593968649004348860733986542833917069379568607*y^8 + 396336590981152275607267681238837489133291553090004824667206667824475594/19962539071362419673084320593968649004348860733986542833917069379568607*y^7 - 333416984351144311339230937266353021354654911121769813332634025881905476/19962539071362419673084320593968649004348860733986542833917069379568607*y^6 - 480364575597865957809254997964871291740177319705235467878871992444337398/19962539071362419673084320593968649004348860733986542833917069379568607*y^5 + 203611080321016698543057502394508494258570696550800377971917130324438614/19962539071362419673084320593968649004348860733986542833917069379568607*y^4 + 397910455737906498133750558996588526335731129249392013813925684302215289/19962539071362419673084320593968649004348860733986542833917069379568607*y^3 - 5078278009759457386275351588581773399684881448274583206806727722859743/19962539071362419673084320593968649004348860733986542833917069379568607*y^2 - 154853751473798463179001123840507260684511036965098508308779464397351928/19962539071362419673084320593968649004348860733986542833917069379568607*y - 49437830336738070130883630166334414016818242711985299353282134879904985/19962539071362419673084320593968649004348860733986542833917069379568607

-85556027200593645978665884215590557455463974727758342625310893/633148500471388869709928021629885153488815399599941096575123517383*y^19 - 1823894473040196332480507479475803001583924996507433149120168526/633148500471388869709928021629885153488815399599941096575123517383*y^18 - 16285271265920357075323743009593412664980291686756660840081521789/633148500471388869709928021629885153488815399599941096575123517383*y^17 - 85707240735727222495834122080254671449923333954771434469389856247/633148500471388869709928021629885153488815399599941096575123517383*y^16 - 299344695516768076698280996843128656043632262372139843140726928168/633148500471388869709928021629885153488815399599941096575123517383*y^15 - 618099708598362899912374709592713812527091178854213597029353087215/633148500471388869709928021629885153488815399599941096575123517383*y^14 - 343649582485756013332218403061352848574025698683291795480656200588/633148500471388869709928021629885153488815399599941096575123517383*y^13 + 1611734706412770771804633776159942615862992565149898498773407495998/633148500471388869709928021629885153488815399599941096575123517383*y^12 + 3178109529449842749975280525340253389630443738434916549945056558335/633148500471388869709928021629885153488815399599941096575123517383*y^11 - 3402425858094349487354734260978472529369839703171370370300124335974/633148500471388869709928021629885153488815399599941096575123517383*y^10 - 15265256365760955034058001816132798276240004456060134296386893563379/633148500471388869709928021629885153488815399599941096575123517383*y^9 + 12558065778269053619895450264820128560777338199883448739367608786670/633148500471388869709928021629885153488815399599941096575123517383*y^8 + 27304803596884342028800808318990524561561523160690670833110006615977/633148500471388869709928021629885153488815399599941096575123517383*y^7 - 18051600169163269463341052927378794285256988510131983559529050220526/633148500471388869709928021629885153488815399599941096575123517383*y^6 - 31442281152436003135932374326578819646868074672209080202078854324117/633148500471388869709928021629885153488815399599941096575123517383*y^5 + 9753742226795002810129475394018443390956176633851249467317404185828/633148500471388869709928021629885153488815399599941096575123517383*y^4 + 25917458513601226905653486381667132491150044107591734920758220119888/633148500471388869709928021629885153488815399599941096575123517383*y^3 + 638569474128235446148584527449992001048011597046844593751948626468/633148500471388869709928021629885153488815399599941096575123517383*y^2 - 9764028437166301816624546297617594034864566967861362182269521976670/633148500471388869709928021629885153488815399599941096575123517383*y - 3192349454234515841587342505509902105254921521783293188609486181132/633148500471388869709928021629885153488815399599941096575123517383

1369311829366792430651906622932848294517752977140729661742944836/151322491612661939860672797169542551683826880504385922081454520654537*y^19 + 21772447983517194509835343521781271761250065080980346872379558965/151322491612661939860672797169542551683826880504385922081454520654537*y^18 + 107521842787743674295171468877078037310303182470167168278904545714/151322491612661939860672797169542551683826880504385922081454520654537*y^17 + 63755736718113639745543446657380989704132145047353883625363354290/151322491612661939860672797169542551683826880504385922081454520654537*y^16 - 1748048800236293856467970413314816595579497167212278162386675812300/151322491612661939860672797169542551683826880504385922081454520654537*y^15 - 11586624621799423194051808371296941861384654795045066091136731258052/151322491612661939860672797169542551683826880504385922081454520654537*y^14 - 33363499184068650405352585253153425467683238606545328697301870417038/151322491612661939860672797169542551683826880504385922081454520654537*y^13 - 28944682914082259587762349015384126718767335636233747351950940930150/151322491612661939860672797169542551683826880504385922081454520654537*y^12 + 90302918118187008473255595918754518483783183602654807983911059946267/151322491612661939860672797169542551683826880504385922081454520654537*y^11 + 228321900042662435424960670512294869712502712103371807425154778157342/151322491612661939860672797169542551683826880504385922081454520654537*y^10 - 183532639314103012435159289798745373757816108916683766201144816814948/151322491612661939860672797169542551683826880504385922081454520654537*y^9 - 1243584539782928966770143160239252410627686436160584993173737479170242/151322491612661939860672797169542551683826880504385922081454520654537*y^8 + 1392901819289732404355857904069809067257121199839613784022648306827008/151322491612661939860672797169542551683826880504385922081454520654537*y^7 + 1466001434968598702504188365656088710929117940809328424496542164762714/151322491612661939860672797169542551683826880504385922081454520654537*y^6 - 1991255615356521110858078395719525164175642353316575683109428356608855/151322491612661939860672797169542551683826880504385922081454520654537*y^5 - 1228224838448817272520400465530052724974097253735403038285120752645723/151322491612661939860672797169542551683826880504385922081454520654537*y^4 + 1437072359029673894669019296029253734641760514483475855324896810309814/151322491612661939860672797169542551683826880504385922081454520654537*y^3 + 954418746701491275517108537209672470186862222691318160961061496698232/151322491612661939860672797169542551683826880504385922081454520654537*y^2 - 509109754138627131521552794071452170440119249240468311302570996273022/151322491612661939860672797169542551683826880504385922081454520654537*y - 263653422326028068180508083521658369083635209697331512530743035577498/151322491612661939860672797169542551683826880504385922081454520654537


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

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

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

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

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

# 1 Loop Invariant
-22812424027966500483409395707013634575564129260395366863837728/2649156905738028743556184190920021562714708784936992035879177897*y^19 - 487401827346938287634382843528397355319209162372288049682507253/2649156905738028743556184190920021562714708784936992035879177897*y^18 - 4367335699456139564562999659475135875684951396892348760423845560/2649156905738028743556184190920021562714708784936992035879177897*y^17 - 46195811137051721164929346710097625116491483686655933851706648595/5298313811476057487112368381840043125429417569873984071758355794*y^16 - 162427204702895143248366972343448150856280567011880311854861140321/5298313811476057487112368381840043125429417569873984071758355794*y^15 - 340098266399045046723008174532531068307750312177142348858437110631/5298313811476057487112368381840043125429417569873984071758355794*y^14 - 207661000096243952967730597426216667321850106496837223192090679093/5298313811476057487112368381840043125429417569873984071758355794*y^13 + 838153868612207879133998778923767510349644022290402361540237824611/5298313811476057487112368381840043125429417569873984071758355794*y^12 + 1745385516090210827987684944936831706466517005088683738080423100185/5298313811476057487112368381840043125429417569873984071758355794*y^11 - 833931227078743015405527341441604328429948693567501291174300036047/2649156905738028743556184190920021562714708784936992035879177897*y^10 - 4095287991841981137162329328746497579718692648407003239319194336165/2649156905738028743556184190920021562714708784936992035879177897*y^9 + 3035762485281298664853130162289973193491918425589480788568803108727/2649156905738028743556184190920021562714708784936992035879177897*y^8 + 14594365799718517849064559223169156061198198354760052186840486379849/5298313811476057487112368381840043125429417569873984071758355794*y^7 - 3826596928179316500162204873399968380695967675928786788381622441599/2649156905738028743556184190920021562714708784936992035879177897*y^6 - 8902570180016475415507633165463444410554710788157080962398110590648/2649156905738028743556184190920021562714708784936992035879177897*y^5 + 1859809556383053854190979683943245353791111223857750447938569647635/2649156905738028743556184190920021562714708784936992035879177897*y^4 + 7161415139817162843218127737732294881058853977052494079248872360678/2649156905738028743556184190920021562714708784936992035879177897*y^3 + 1008509461912043539206799337348218885185440211995478179191125992401/2649156905738028743556184190920021562714708784936992035879177897*y^2 - 2748526845265619698744089614944120122536398908688826775808460003939/2649156905738028743556184190920021562714708784936992035879177897*y - 2388194774103939142831256937617407188180324441890326023594212237673/5298313811476057487112368381840043125429417569873984071758355794

# 2 Loop Invariant
440066856538800674584344251981449909582234643559030848787197618979699031004487695245560792265765057130440023354684545521/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^19 + 9420012482759733041534279174508355165811505781219003866086659804763392345085497443781282529930994731822216812180922863313/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^18 + 84590803174071825991122359331267687904986964037755073433562190636562321518346730933388171833162246374363573855404452599161/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^17 + 74698687226938119641831087982891825570385759485468238352254751251005257845958793413417944574344405677835915449352167288121/1133866663851652039809114103231935993116245537553277275246812587386306682017262747519992710701404195061234359519981861217266*y^16 + 1577720871922770095059632817682147109078213793951850708109444439897685954175219261440045927715399372121728454388864030907415/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^15 + 3307206255425073622772434214237912723227674283513751269190571225363982982129575814082881595703756661371311033389324705598749/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^14 + 669229123863794263775247153728166847429424807651803479864893023963402745182362699082333733784202610947027202478480167589931/2267733327703304079618228206463871986232491075106554550493625174772613364034525495039985421402808390122468719039963722434532*y^13 - 8272260107270488788110365651814060077852188200875053069088594641862104420192538772387125902553578669309092928328820779781647/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^12 - 2890580571012563645373102218213023511989452309592554247964172918045749636052700658374308281245989356150482922669948539639755/1133866663851652039809114103231935993116245537553277275246812587386306682017262747519992710701404195061234359519981861217266*y^11 + 15975031733202517995057043874558476112702802370725884821932278488783527814861607696992371656361870339311243094594613417972547/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^10 + 80822320167404441100229918504425009139042430480482700338424735011872671500516243836804051754034566486131835362768998358592111/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^9 - 18915632174704162537086595297423361787346910744949421782252485000132623093476486330647342177587462569188897004315361655783747/2267733327703304079618228206463871986232491075106554550493625174772613364034525495039985421402808390122468719039963722434532*y^8 - 12411990080250979426385471061517125872871639372835004088576569485472390315322941926051877154972423628497071856090888257101666/566933331925826019904557051615967996558122768776638637623406293693153341008631373759996355350702097530617179759990930608633*y^7 + 73634753718795998215759400819498757143464057886241722801830398286704887876750319321391950899570249469651810185557874214824839/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^6 + 45837518617231501919230533489351349818559220470164441869392909592434027993759859726542164304676004565621881447084523670083825/1700799995777478059713671154847903989674368306329915912870218881079460023025894121279989066052106292591851539279972791825899*y^5 - 36503454002158791512666093607446950704947743899651025437966140975999945756282112869595683833758389001714034739201982084274283/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y^4 - 73972559080321475472022036026068029104800250224340560771923292871565170232299890103369216062766251781161207482105362158210813/3401599991554956119427342309695807979348736612659831825740437762158920046051788242559978132104212585183703078559945583651798*y^3 - 5270109577269037215345672677316536832728180059718533153262649176930468270551264451122440721214351597562904606229838567924277/1700799995777478059713671154847903989674368306329915912870218881079460023025894121279989066052106292591851539279972791825899*y^2 + 57572333955350669361062392555707817719004404766081760041837471309587497386559528792427478088825330958395094301185787763549713/6803199983109912238854684619391615958697473225319663651480875524317840092103576485119956264208425170367406157119891167303596*y + 18954146348787925366858623186663959938148252813243517674629879646992085446791708260233263113888331979859287909464241634299443/4535466655406608159236456412927743972464982150213109100987250349545226728069050990079970842805616780244937438079927444869064

# 3 Loop Invariant
1654949839711110958966255701577841072406104592815228693967252079386140849064687629644630642760867503664621488248940850652611558826621291409748401542/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^19 + 70184294988031293091200984976250169810156137465533036683468200999322556268307575927355933040067960816698738602814845312718065343681523804074921684713/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^18 + 622461864771621790651606184737321367156773954610730669834594998585928217039978220162981806548131584844045953453923168783973598163787773567180814847693/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^17 + 3253377312419481057264090969758619295714845253347446500115343210072953818584349842807323862842134893019023500523609842841814286658668341908203002171533/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^16 + 11280314547788501618843265053201375499735647674555338071201856795211895975865110439219960866628165066625366001340121334541995926745802568791484997873333/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^15 + 22964703949590844844527437370444162345579014402276877594260872948518444330542197538680501940148013962682266031897058478426420809914812447262715539925307/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^14 + 5867813145108293103028223033184603315810245929911408180249088934612461904445597644603247676735561890450491371367497598848842097938693824755523787869688/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^13 - 30999213180233983250355710321024223395550585794661227235512896556318433514203426743036559383426926429730035173603097233035737102019940600549479506371444/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^12 - 116587620795768989714855774400669937853303045905577400908588285929402388662110837876796086085410743811330787660763398414819203599277764995272381683630325/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^11 + 68367457206805044453491694331819373364365676000607609738173847415424375992253957636126968868145966809714646069669484840103914154406826492945986024322365/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^10 + 283483193501315250993171327406510211314058796951787845635867130249592441474316577779924603686786675828157735773701040646345623315274118650070154220069692/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^9 - 263340710928559156624356733645766171238478049406558176945767349220113513365199023585882571806764307723693382384872667765406621882842982157316314704849198/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^8 - 950874017358321678614004465512734512743648440371924296620683309535177688545171567431253617801510787238846539523291687282288072773251114151105182426180813/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^7 + 689987401052003456511917059008334589370501287340591714678335136679896915041647716132691929347391025497513489353973098221404577546546025872934582858290091/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^6 + 567115863527612868954308034284820631429220249430491572657508376042617765848891616394157104570857408138059663791832954353297075486964413270209998785376294/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^5 - 215177207447710213272232385567531412445508163186206683122909994371551274880784891118300056873632774672024050875378035578572933608746563490170991401402667/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^4 - 904586300344005006812584618499884912791399090718934317777427240905111729618362863883731617670088169335835102128736753472930769749114629878825308911458137/524534601141117286296874651491441744130953217366523637790084612241883358122157334803892241958383553722374522987882969355096746948747092076922420983687678*y^3 - 4891722285576453451941231057898769189595255285607308605970293438127407154353507877539771155937847030678322385748265570595566345651786366672429399992518/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y^2 + 172254022049635537356437777483532905430899890461554588261600958586615454483381728840195262879284767081339334702557301781593741737613809738669724770255230/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839*y + 60136251177744422473740333269840131187253054144038608443921294082005414756802764634668224471113406430164494209471617090182084146411726518900126838945278/262267300570558643148437325745720872065476608683261818895042306120941679061078667401946120979191776861187261493941484677548373474373546038461210491843839

# 4 Loop Invariant
-52424152277963816203941861545942223820506727240006913072389537077167757754092196422270205030056883028458680717060322609725382291947935503887652582963312971424422836193538009420192210922002899931791413853737651/6735187677812653484958150605684339352208555060861479873720870837758369757101718507209245335312412598622415950316826938722810933950329209129452347069358148360938223412122994261375739826495079545190248799313293952520*y^19 - 557636181618795626028277253257094036769498585816851215244265027894918191683302679193007485036627936958467435238043720734520857364441982263868399919913157288828100230297277062095980828509596093310903578187636993/3367593838906326742479075302842169676104277530430739936860435418879184878550859253604622667656206299311207975158413469361405466975164604564726173534679074180469111706061497130687869913247539772595124399656646976260*y^18 - 59602744101706347990320793616854451510837594469704884490605818945535009262801891208154983560996983296695093945502707362491615889087781865635344494115542593541196082598572042622468246733967286924380899239135658307/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^17 - 312965397294169944246738375412102370189910966424067568498269761147984272027224708615534197638741472057569081187797371411208102459516776816867437017949471275040033031874371466359681569034797935929608160286524534939/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^16 - 1090574830888301422962168302566545907986763142719326523655738098631817057898004281832948082733087126857510012747390877756035846069698932502750962220033174492343720200833066412010374688433724610466804194134469789221/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^15 - 747135003105476233714061315395148214858920718067995598507487747159775493048723362341998895314910644344945209221387337944206186628750879757720720661563112326209250729464939593741316873755616400568810293681669916637/13470375355625306969916301211368678704417110121722959747441741675516739514203437014418490670624825197244831900633653877445621867900658418258904694138716296721876446824245988522751479652990159090380497598626587905040*y^14 - 605941690968098688354518288453317643069847143536192818044044088704453643933432031024762364329342912291028164435613178213349759640324328146777840629177902105874475978810553565726873180413376856261057851461754283007/20205563033437960454874451817053018056625665182584439621162612513275109271305155521627736005937237795867247850950480816168432801850987627388357041208074445082814670236368982784127219479485238635570746397939881857560*y^13 + 5932350895793194379157342723331807878839673877654190620412881005395464817855347233527917160668266954741349540557932446685863488820071266102678537510866367780342259130090780740422640381237914883244236131837848762783/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^12 + 11573471376388869517081501666458258235048747264074387439485346947749410904120570812824886200138107661370733302451360588776559722428273328088060905064282118422511351974874432937657895567814101430839758087426583280319/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^11 - 2494528939234107671380050202672916746876284415367645251530268300333420949288638282931687363810320375743806693606238758453830438643505259432068473672340473094310327272509556166146562476348317986692287110231460942729/8082225213375184181949780726821207222650266073033775848465045005310043708522062208651094402374895118346899140380192326467373120740395050955342816483229778033125868094547593113650887791794095454228298559175952743024*y^10 - 691744537716964177679838088144956299528755810287584464652033130505854198162305608551937447219890025475136331491709040158887031494063731969497610321259890177669957734490880923122106962304774877395625329723339156116/505139075835949011371861295426325451415641629564610990529065312831877731782628888040693400148430944896681196273762020404210820046274690684708926030201861127070366755909224569603180486987130965889268659948497046439*y^9 + 23409171181064245886815309767760039462471072255436342731392877187214243371583095225639281061576165270531583845317783616697954663220434609549474818071911786582868714100805861683244369532086768430680191094412413308831/20205563033437960454874451817053018056625665182584439621162612513275109271305155521627736005937237795867247850950480816168432801850987627388357041208074445082814670236368982784127219479485238635570746397939881857560*y^8 + 32153350331648046471766697506791461413937093114141275475879049732166927062156597452140250014601174863341485678646027674292100237099016341316149756856473835712274518376528551377255327367527930020361387436080136078443/13470375355625306969916301211368678704417110121722959747441741675516739514203437014418490670624825197244831900633653877445621867900658418258904694138716296721876446824245988522751479652990159090380497598626587905040*y^7 - 61270849769674784595577007535701063720957280448237553905818550534744426865912231936464061382262776475449917410447637253671784929950142470275903516527841347780580092355112467209194313144207558062021031347954911346631/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^6 - 116585565689659183508135091809542088607888142380389262866635932202602613608467256901643577423987296329777819736941866932573806894989885390750055462716363608534372486572453494060528237159097539673573742064796733595143/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y^5 + 2241934219431955067350764427217292806061573743614094263911027360851047402801319424652301245324814603173748935449848673412744874379307896258024449575901440864405618795162439935119794783826937938475832378995566176318/2525695379179745056859306477131627257078208147823054952645326564159388658913144440203467000742154724483405981368810102021054100231373453423544630151009305635351833779546122848015902434935654829446343299742485232195*y^4 + 23385001070398970153714026643909877087599291756795655867342529975251940228028451445051072255555898913655695107360412663369062482476068873871458125090275465123477979069917969191070460842582530866425804963302770739383/10102781516718980227437225908526509028312832591292219810581306256637554635652577760813868002968618897933623925475240408084216400925493813694178520604037222541407335118184491392063609739742619317785373198969940928780*y^3 + 2006924851360244073872696590187432658900521090438478206118107108212314360747310204606917737792495057336851152250179458466585942495522226130640801288344582726159551298644281362532592585215782026392477003518440929301/13470375355625306969916301211368678704417110121722959747441741675516739514203437014418490670624825197244831900633653877445621867900658418258904694138716296721876446824245988522751479652990159090380497598626587905040*y^2 - 36004146882026979710692867872296625867892644203212646150277576528384035121830722852029005985685089442242941718814641875884537476883892455789429237499741834170557888641066136835650693691727378223425300823597133272991/40411126066875920909748903634106036113251330365168879242325225026550218542610311043255472011874475591734495701900961632336865603701975254776714082416148890165629340472737965568254438958970477271141492795879763715120*y - 1709920685457319785036656990328739452734468066766134087773923932736910496545333941114183041327783782101544435269645626717230053301760008398880761770703140521111657719295117513571140670690311222959662014294721842421/5051390758359490113718612954263254514156416295646109905290653128318777317826288880406934001484309448966811962737620204042108200462746906847089260302018611270703667559092245696031804869871309658892686599484970464390