# Manifold: Census Knot K8_171

# Number of Tetrahedra: 8

# Number Field
x^23 + 19*x^22 - 247*x^21 + 1163*x^20 - 3563*x^19 + 6933*x^18 - 11867*x^17 + 10705*x^16 - 9101*x^15 - 16962*x^14 + 2034*x^13 - 50225*x^12 + 17372*x^11 + 3766*x^10 + 43504*x^9 + 47197*x^8 - 50543*x^7 - 7526*x^6 - 8261*x^5 - 4348*x^4 + 17856*x^3 - 2240*x^2 - 3840*x + 1024 

# Approximate Field Generator
-0.553168112264200 + 1.03799388147575*I

# Shape Parameters
-65838089223872855349336893614902633522645409/1395230536494195812042590925748490862082561532*y^22 - 639344737149081965889125198356501665780432085/697615268247097906021295462874245431041280766*y^21 + 15722051266140141653275217622530161995138065183/1395230536494195812042590925748490862082561532*y^20 - 69952505673618376116992627128802830757961841959/1395230536494195812042590925748490862082561532*y^19 + 205252255420950996159120103474558025709020042843/1395230536494195812042590925748490862082561532*y^18 - 370714670984819331638692128984084337699898594041/1395230536494195812042590925748490862082561532*y^17 + 627538243532227360285879692198153202720232392817/1395230536494195812042590925748490862082561532*y^16 - 445402889644448643888087000273084083783769978259/1395230536494195812042590925748490862082561532*y^15 + 420908297955649239981839119761742884102922136211/1395230536494195812042590925748490862082561532*y^14 + 642112753458449425491032138590314073852147783025/697615268247097906021295462874245431041280766*y^13 + 418624440275992110427855089801892126817272447479/1395230536494195812042590925748490862082561532*y^12 + 3490420601955876540185814263078006411639537126625/1395230536494195812042590925748490862082561532*y^11 + 331899470496255534497265254437690219776822038861/1395230536494195812042590925748490862082561532*y^10 - 69058483504518496212229704344613305913843432139/1395230536494195812042590925748490862082561532*y^9 - 1451687179019517620049810562762402515180265646077/697615268247097906021295462874245431041280766*y^8 - 4313792826644391142360955463691015156968294265711/1395230536494195812042590925748490862082561532*y^7 + 369064216888066407171889031056632797601739199065/348807634123548953010647731437122715520640383*y^6 + 274033670179390808608006298399758673073188656143/348807634123548953010647731437122715520640383*y^5 + 256729985372217159869462197214812365467685745866/348807634123548953010647731437122715520640383*y^4 + 710741578062560311649890697331187867431019219325/1395230536494195812042590925748490862082561532*y^3 - 864076164228329822394931945550240304484791172937/1395230536494195812042590925748490862082561532*y^2 - 54711584515374592654762811751790707247954942856/348807634123548953010647731437122715520640383*y + 39235930059993772707049127359352989543939841616/348807634123548953010647731437122715520640383

179614191907350875698183115720009166350829320663/714358034685028255765806553983227321386271504384*y^22 + 3489746275823159987867534862473131648891554214297/714358034685028255765806553983227321386271504384*y^21 - 42866540337346669753073311481245241664001102442053/714358034685028255765806553983227321386271504384*y^20 + 190508066691966871018349678828627218580001773326209/714358034685028255765806553983227321386271504384*y^19 - 558374935808552157051912615741918543842913506358865/714358034685028255765806553983227321386271504384*y^18 + 1006456844192569425155279436282463069109860998622487/714358034685028255765806553983227321386271504384*y^17 - 1702198497237700359152756610151748220378858365497337/714358034685028255765806553983227321386271504384*y^16 + 1197907472645103042420466061591522793912441514632507/714358034685028255765806553983227321386271504384*y^15 - 1130863021546004420705529057669647951294498444677767/714358034685028255765806553983227321386271504384*y^14 - 1760022024736950411325095030441341264544228156404449/357179017342514127882903276991613660693135752192*y^13 - 578771786604477462825332670599829313794540036893445/357179017342514127882903276991613660693135752192*y^12 - 9521872383515324470553482676799066460543730614578975/714358034685028255765806553983227321386271504384*y^11 - 30164115388680063489795951052870605538265530372941/22323688583907132992681454811975853793320984512*y^10 + 114153453823060539295565851258436361588163905478629/357179017342514127882903276991613660693135752192*y^9 + 991784232856843202164062510731932410132387230318565/89294754335628531970725819247903415173283938048*y^8 + 11865750652405847431475639718910537204663057267023579/714358034685028255765806553983227321386271504384*y^7 - 3953926743805113646314042037531508547532427579812261/714358034685028255765806553983227321386271504384*y^6 - 1519399285045649397276208173293219776492519362674403/357179017342514127882903276991613660693135752192*y^5 - 2819715069778756535135790380272777749099912035596363/714358034685028255765806553983227321386271504384*y^4 - 247364187491224068078434865608365928497575784548411/89294754335628531970725819247903415173283938048*y^3 + 146642425951645463061522569264298049442301378567085/44647377167814265985362909623951707586641969024*y^2 + 9531950312536881396337995569385315453270216976495/11161844291953566496340727405987926896660492256*y - 820240529504585149850434951444017454134291139473/1395230536494195812042590925748490862082561532

-65838089223872855349336893614902633522645409/1395230536494195812042590925748490862082561532*y^22 - 639344737149081965889125198356501665780432085/697615268247097906021295462874245431041280766*y^21 + 15722051266140141653275217622530161995138065183/1395230536494195812042590925748490862082561532*y^20 - 69952505673618376116992627128802830757961841959/1395230536494195812042590925748490862082561532*y^19 + 205252255420950996159120103474558025709020042843/1395230536494195812042590925748490862082561532*y^18 - 370714670984819331638692128984084337699898594041/1395230536494195812042590925748490862082561532*y^17 + 627538243532227360285879692198153202720232392817/1395230536494195812042590925748490862082561532*y^16 - 445402889644448643888087000273084083783769978259/1395230536494195812042590925748490862082561532*y^15 + 420908297955649239981839119761742884102922136211/1395230536494195812042590925748490862082561532*y^14 + 642112753458449425491032138590314073852147783025/697615268247097906021295462874245431041280766*y^13 + 418624440275992110427855089801892126817272447479/1395230536494195812042590925748490862082561532*y^12 + 3490420601955876540185814263078006411639537126625/1395230536494195812042590925748490862082561532*y^11 + 331899470496255534497265254437690219776822038861/1395230536494195812042590925748490862082561532*y^10 - 69058483504518496212229704344613305913843432139/1395230536494195812042590925748490862082561532*y^9 - 1451687179019517620049810562762402515180265646077/697615268247097906021295462874245431041280766*y^8 - 4313792826644391142360955463691015156968294265711/1395230536494195812042590925748490862082561532*y^7 + 369064216888066407171889031056632797601739199065/348807634123548953010647731437122715520640383*y^6 + 274033670179390808608006298399758673073188656143/348807634123548953010647731437122715520640383*y^5 + 256729985372217159869462197214812365467685745866/348807634123548953010647731437122715520640383*y^4 + 710741578062560311649890697331187867431019219325/1395230536494195812042590925748490862082561532*y^3 - 864076164228329822394931945550240304484791172937/1395230536494195812042590925748490862082561532*y^2 - 54711584515374592654762811751790707247954942856/348807634123548953010647731437122715520640383*y + 39235930059993772707049127359352989543939841616/348807634123548953010647731437122715520640383

441380246040255546852470495044445048457256315396684819263187/4518399059868999971909520240524047825286355756196517380543424*y^22 + 8615986544966394409808823155018097797980259536489508627682805/4518399059868999971909520240524047825286355756196517380543424*y^21 - 104534446449414978325096174031408884603562970476882360348796689/4518399059868999971909520240524047825286355756196517380543424*y^20 + 458935592092614909227031692426690186734730803948054284916616605/4518399059868999971909520240524047825286355756196517380543424*y^19 - 1334089806644141862906648161936963587558613840136512725668702541/4518399059868999971909520240524047825286355756196517380543424*y^18 + 2367354216697167157354382707550789166436217490379734988267249451/4518399059868999971909520240524047825286355756196517380543424*y^17 - 4011049512727092206609049388123016983778555223504050072657060005/4518399059868999971909520240524047825286355756196517380543424*y^16 + 2648562345736770117573633213981296166333446140216786574856107615/4518399059868999971909520240524047825286355756196517380543424*y^15 - 156418487283358947286954376851730345201154682875017049453192795/265788179992294115994677661207296930899197397423324551796672*y^14 - 4423851010816030953523905667056036912720388095889781949246486577/2259199529934499985954760120262023912643177878098258690271712*y^13 - 1865636835186366955128714772008589765111260025700337563445229089/2259199529934499985954760120262023912643177878098258690271712*y^12 - 24121516095900007369769424273023063528117835130347235231183595595/4518399059868999971909520240524047825286355756196517380543424*y^11 - 610970081387940700263155801601481262764331627862917059215576503/564799882483624996488690030065505978160794469524564672567928*y^10 - 474099463891228229569388223214940784672136479514595399637278119/2259199529934499985954760120262023912643177878098258690271712*y^9 + 2344830529992408802088020372134101926174915331693957252425203715/564799882483624996488690030065505978160794469524564672567928*y^8 + 30591775062098780507613433041248565449260748909040169231912365863/4518399059868999971909520240524047825286355756196517380543424*y^7 - 6286544254048158653600470181797755283931001129512807184817096929/4518399059868999971909520240524047825286355756196517380543424*y^6 - 3269302063470764641785869501640613055661037339063266461884002451/2259199529934499985954760120262023912643177878098258690271712*y^5 - 7104551210118513459537662084733717072043331694641325731456506119/4518399059868999971909520240524047825286355756196517380543424*y^4 - 351069761094103739991578784032080363270444091539926992363270259/282399941241812498244345015032752989080397234762282336283964*y^3 + 307331714150414328467673192315649681754600952044432595892840481/282399941241812498244345015032752989080397234762282336283964*y^2 + 24491070717239622070843221216741017009949555237220036164649860/70599985310453124561086253758188247270099308690570584070991*y - 13461580465904829217299869973689423511721420707512330180754140/70599985310453124561086253758188247270099308690570584070991

-431178063993961420819241344686195630787781950570438606518039/4518399059868999971909520240524047825286355756196517380543424*y^22 - 8424348127468461386958405983100812513754015526083457264655217/4518399059868999971909520240524047825286355756196517380543424*y^21 + 101969478088771137230568758310454573565284709713299889861478125/4518399059868999971909520240524047825286355756196517380543424*y^20 - 446590166456281459063789266694575186299975515960989114701261321/4518399059868999971909520240524047825286355756196517380543424*y^19 + 1295890358302429222784096009706674516762934549731542639084654585/4518399059868999971909520240524047825286355756196517380543424*y^18 - 2291608826544008203275946009175963124366142163733977655398859391/4518399059868999971909520240524047825286355756196517380543424*y^17 + 3882250273383453552012083747505105987633505897296866409410836785/4518399059868999971909520240524047825286355756196517380543424*y^16 - 2524175780938948196558958105612000247274663186376249058099091075/4518399059868999971909520240524047825286355756196517380543424*y^15 + 150612151309470045989613658704098995031352146026092400697548719/265788179992294115994677661207296930899197397423324551796672*y^14 + 4347651692495593723083131415408147872527031505029131071824404309/2259199529934499985954760120262023912643177878098258690271712*y^13 + 1896502589754639254332586239702254937051435903299281058060741893/2259199529934499985954760120262023912643177878098258690271712*y^12 + 23686831345395627577790666108631372450898167035109766505109991247/4518399059868999971909520240524047825286355756196517380543424*y^11 + 654310526652960363864679444490265058674682337810614669263090091/564799882483624996488690030065505978160794469524564672567928*y^10 + 573166511247199962172901217128024068309116608448757683612362803/2259199529934499985954760120262023912643177878098258690271712*y^9 - 2272051615157913742032925857242287801480261309155359721850563367/564799882483624996488690030065505978160794469524564672567928*y^8 - 30172839556819272119426397330034856797278908369207387117726073787/4518399059868999971909520240524047825286355756196517380543424*y^7 + 5567149033912672544859801530188102616023030342379172209830946605/4518399059868999971909520240524047825286355756196517380543424*y^6 + 3133671075240478302834594443379264517825550785201319991674024335/2259199529934499985954760120262023912643177878098258690271712*y^5 + 6963724342698848986610721302843375117700893176009130008623532875/4518399059868999971909520240524047825286355756196517380543424*y^4 + 352380388296102745057607814865565120892079531281654523962627167/282399941241812498244345015032752989080397234762282336283964*y^3 - 145904886913176657720719313690696108241953743697753562333307379/141199970620906249122172507516376494540198617381141168141982*y^2 - 24248798633955093944943876241995457576273707010576137839127476/70599985310453124561086253758188247270099308690570584070991*y + 12760840764394893294062417516275405387344027234389745148000363/70599985310453124561086253758188247270099308690570584070991

-41487060796212496700515162290342085380867730586627274177928217/1102489370608035993145922938687867669369870804511950240852595456*y^22 - 813759454429729821726285190092809719019896875491368602257263879/1102489370608035993145922938687867669369870804511950240852595456*y^21 + 9748101175913747522104203675542977743728265460453766036400735915/1102489370608035993145922938687867669369870804511950240852595456*y^20 - 42235126991106345665095147930922910224132999366998151538342055535/1102489370608035993145922938687867669369870804511950240852595456*y^19 + 121605539277229906835205480904979247710453853087404338714237290783/1102489370608035993145922938687867669369870804511950240852595456*y^18 - 211829920544883310056280215907020542710337255644365723482516359033/1102489370608035993145922938687867669369870804511950240852595456*y^17 + 359148801911869825612905150470139412686142342444295308448843291159/1102489370608035993145922938687867669369870804511950240852595456*y^16 - 218344560194307697612991141584726944843300588296041385589816143221/1102489370608035993145922938687867669369870804511950240852595456*y^15 + 13803400686040178612459658248384305791730320251478785399225532569/64852315918119764302701349334580451139404164971291190638387968*y^14 + 426215402355208472816893307591236212791639013337684422827973326303/551244685304017996572961469343933834684935402255975120426297728*y^13 + 216538132259532426158477190740558482980727964270025972223980994483/551244685304017996572961469343933834684935402255975120426297728*y^12 + 2326648743328204926790718962835063554636493541106370344751747576401/1102489370608035993145922938687867669369870804511950240852595456*y^11 + 43240048172350761096911533698333548461733629881288679788587715249/68905585663002249571620183667991729335616925281996890053287216*y^10 + 99217326040937352285023228892692252467786142805660251118267867789/551244685304017996572961469343933834684935402255975120426297728*y^9 - 215206404640996355180001346034014824581997783738251777101694831239/137811171326004499143240367335983458671233850563993780106574432*y^8 - 3046375667141441018542912011640882841486979014277254225551888879221/1102489370608035993145922938687867669369870804511950240852595456*y^7 + 252675719925260123855507481741994409475890816100080133912647653723/1102489370608035993145922938687867669369870804511950240852595456*y^6 + 273942531301598228041679160181959972258249719975181197456058029901/551244685304017996572961469343933834684935402255975120426297728*y^5 + 696016499695534383954715681872279883616398959890678853794547163989/1102489370608035993145922938687867669369870804511950240852595456*y^4 + 76755507313024071823969362659761152487299308613916448187059090235/137811171326004499143240367335983458671233850563993780106574432*y^3 - 1481389339541698326181676620580375082220309689369368120037379460/4306599103937640598226261479249483083476057830124805628330451*y^2 - 2471142780214723786430122620952633047622522315956487464403482177/17226396415750562392905045916997932333904231320499222513321804*y + 259949808057670926268536602120058911868424096496392120140348198/4306599103937640598226261479249483083476057830124805628330451

76492394065258843911954801757035290388450607004295558387894253/5223269313208563967527405398045799286031027254163174091908198144*y^22 + 1511129072138790731999228503129585189442766339166008652162175251/5223269313208563967527405398045799286031027254163174091908198144*y^21 - 17770374744025107021457925041926596422821612623730171603725714519/5223269313208563967527405398045799286031027254163174091908198144*y^20 + 75198913872376226240038606047708475712344440635096900975920905387/5223269313208563967527405398045799286031027254163174091908198144*y^19 - 211216451197032000336081882566690424012971868023244820662801189979/5223269313208563967527405398045799286031027254163174091908198144*y^18 + 348735170432793811239823557302619597217842350764429229527068797245/5223269313208563967527405398045799286031027254163174091908198144*y^17 - 573932516074226303265922741824460903326136023104197082541675211699/5223269313208563967527405398045799286031027254163174091908198144*y^16 + 238338082059594871706547722824852690489648894835680782381416547657/5223269313208563967527405398045799286031027254163174091908198144*y^15 - 14588162888567069420420811624984416449985124626738091348134239133/307251136071091998089847376355635252119472191421363181876952832*y^14 - 891177547085783508178129015787019922390871672137260121579293510403/2611634656604281983763702699022899643015513627081587045954099072*y^13 - 437244578200479631604907962011384398311830477435946918200156389671/2611634656604281983763702699022899643015513627081587045954099072*y^12 - 4361025820611803425389055400427682518957148851849708994497612068261/5223269313208563967527405398045799286031027254163174091908198144*y^11 - 120006914756530445019508784858647011519915920983911840224853217717/326454332075535247970462837377862455376939203385198380744262384*y^10 - 108204513703550093799588676798188956324227853562924569249177339465/2611634656604281983763702699022899643015513627081587045954099072*y^9 + 335273464692091968390438697093449550479950885652652142943377289971/652908664151070495940925674755724910753878406770396761488524768*y^8 + 5987154252741345090925120589007778368915921093605912291743791560985/5223269313208563967527405398045799286031027254163174091908198144*y^7 - 355165633894920092279379835960375181075837172165790251939668262711/5223269313208563967527405398045799286031027254163174091908198144*y^6 - 685800982271762074739443742322285643667231397870946296422567144521/2611634656604281983763702699022899643015513627081587045954099072*y^5 - 989773314994482311780220676274193163895100945131979625788805492201/5223269313208563967527405398045799286031027254163174091908198144*y^4 - 157831793362588434363221355343175587421883507520120192191217588935/652908664151070495940925674755724910753878406770396761488524768*y^3 + 51157712902510753387176799659974648620486357957018154440215011753/326454332075535247970462837377862455376939203385198380744262384*y^2 + 2984853374460275755688751485987199510249863870739044174211083447/40806791509441905996307854672232806922117400423149797593032798*y - 685737215410492083782373065897343026828184559939424579811010833/20403395754720952998153927336116403461058700211574898796516399

688025702586837119752382903820703998511628734133554990770069007/67251851607090195581901299259959927831562119075228964692008322816*y^22 + 13425334068016218259337752120635433218891458760316710023374548897/67251851607090195581901299259959927831562119075228964692008322816*y^21 - 163040918342561552952209050317189687256407088612497313143775821229/67251851607090195581901299259959927831562119075228964692008322816*y^20 + 716880835176968211375753123087677365407775702166649600649821741001/67251851607090195581901299259959927831562119075228964692008322816*y^19 - 2087668325001269375248342576508198404872652395266444471848470600217/67251851607090195581901299259959927831562119075228964692008322816*y^18 + 3716566812755687337581630181900048047146727664813029470561123912207/67251851607090195581901299259959927831562119075228964692008322816*y^17 - 6309531360047096902711954427518155559256127673161487145834673091969/67251851607090195581901299259959927831562119075228964692008322816*y^16 + 4223084679395610817692838275540717274449458968679330746405707230291/67251851607090195581901299259959927831562119075228964692008322816*y^15 - 250754590350354887141047635216730189083368175558657505105263155343/3955991271005305622464782309409407519503654063248762628941666048*y^14 - 6861484523582916222670348007588642644797196783661484210205564716361/33625925803545097790950649629979963915781059537614482346004161408*y^13 - 2901631755763424102631501458968710443458368471423348749935316187373/33625925803545097790950649629979963915781059537614482346004161408*y^12 - 37798058578768426907566248697187535182886058398948492180856280145175/67251851607090195581901299259959927831562119075228964692008322816*y^11 - 239146910371182781816930232069118015516250061321673294193585069947/2101620362721568611934415601873747744736316221100905146625260088*y^10 - 1149748087603238457169101472394980579357378706508716704370110637555/33625925803545097790950649629979963915781059537614482346004161408*y^9 + 3561270567000756976543696548033175150463545349205709556700563415293/8406481450886274447737662407494990978945264884403620586501040352*y^8 + 46719671341867940238418086366471168419792322661441097060185538316851/67251851607090195581901299259959927831562119075228964692008322816*y^7 - 10144660343620340278307672768282990540149619340976896725913992764301/67251851607090195581901299259959927831562119075228964692008322816*y^6 - 4695578504392501257611993846761394795397043016743896163755137110683/33625925803545097790950649629979963915781059537614482346004161408*y^5 - 10420258617781551143846332331511950542125280091976735641667607116451/67251851607090195581901299259959927831562119075228964692008322816*y^4 - 1033897396530437456333620234672179999757151943665387139904553078379/8406481450886274447737662407494990978945264884403620586501040352*y^3 + 487732172277676418541339494678400061517160527631947663122493671893/4203240725443137223868831203747495489472632442201810293250520176*y^2 + 36126327738752776274563440037646097979913189781463565028349370351/1050810181360784305967207800936873872368158110550452573312630044*y - 5380653479365621611231564295063251469070671401944803913230562668/262702545340196076491801950234218468092039527637613143328157511


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

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

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

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

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

# 1 Loop Invariant
552698754973022137656633758513650929850105718278128694906433979/36147192478951999775276161924192382602290846049572139044347392*y^22 + 10743756861501541853898062511147769634873359368808064550205528029/36147192478951999775276161924192382602290846049572139044347392*y^21 - 131802874308168092829517941986017582459057432377564133548607861145/36147192478951999775276161924192382602290846049572139044347392*y^20 + 584968019482378084201909315025892714668594430721833084078096622469/36147192478951999775276161924192382602290846049572139044347392*y^19 - 1712676596699174066763615756422620006631902137504966981064867360885/36147192478951999775276161924192382602290846049572139044347392*y^18 + 3080692384659037146944478745569650039318530152111126355060432919331/36147192478951999775276161924192382602290846049572139044347392*y^17 - 5207995311174866940964344291684012244396845410115184574080743917293/36147192478951999775276161924192382602290846049572139044347392*y^16 + 3633164797432442539385759780437781422524098837974857507695541154935/36147192478951999775276161924192382602290846049572139044347392*y^15 - 202287295181077121088352951348041180936077294694359937044844389043/2126305439938352927957421289658375447193579179386596414373376*y^14 - 5440379819411623019709418716828127839301166708275931049332010244625/18073596239475999887638080962096191301145423024786069522173696*y^13 - 1826767889088329036044637201330651322074052148653069896009718419337/18073596239475999887638080962096191301145423024786069522173696*y^12 - 29363915146236518875662478245576985039530175538362996631114475581587/36147192478951999775276161924192382602290846049572139044347392*y^11 - 410708187377485193585920169647192349930060954425624259516163698873/4518399059868999971909520240524047825286355756196517380543424*y^10 + 312079427516269167084831353572382639419582410997129372786645791985/18073596239475999887638080962096191301145423024786069522173696*y^9 + 3039209381886834123150080668990718312308635910361704562971558589767/4518399059868999971909520240524047825286355756196517380543424*y^8 + 36736070325241935498514538620237897458686482673843731952725930384111/36147192478951999775276161924192382602290846049572139044347392*y^7 - 11810268562005949838846526471917947780611519517609536907593691828489/36147192478951999775276161924192382602290846049572139044347392*y^6 - 4666512109525771758113458099441089602742425295289357211046056772883/18073596239475999887638080962096191301145423024786069522173696*y^5 - 8653081247996279942442019590670293719207310009491509769245639161583/36147192478951999775276161924192382602290846049572139044347392*y^4 - 12088904678117654597491855731414657560289325818748857727542443994/70599985310453124561086253758188247270099308690570584070991*y^3 + 446499591669611126329541396526120046358150572842308635297818847601/2259199529934499985954760120262023912643177878098258690271712*y^2 + 14809107723895913318643127448792459648107824654069632315735344859/282399941241812498244345015032752989080397234762282336283964*y - 5044957458139841946648340973104197545741698275446093169955240685/141199970620906249122172507516376494540198617381141168141982

# 2 Loop Invariant
-36474896684529897326720891161458384687048940469754345823856753019307617351036765973667642955026249780298073989838817193678378474259823/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^22 - 236173090706628449322486259948438573214818365037121687234842497008250326736613012088072194335224727184719419518135684814323125991627891/746243843402787076240107067085136892126231336768744855891071604313029243434998918583862121374275781852725544962623966264172105266256896*y^21 + 8708432759553373879020089726081171689523784361410844940001456184385170436250183334923095856512106412576589933110720274237920063249119317/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^20 - 12905815114645864058669848988804882799611188893056823672782788334846411873424279027681494152855066463093550164781749494265574537200829467/746243843402787076240107067085136892126231336768744855891071604313029243434998918583862121374275781852725544962623966264172105266256896*y^19 + 113482157833540002328017019202381182370525693932584275042465738079750160659375942329607372414404859317936102667770468106499997112962671361/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^18 - 204580298538481334191753093655268060366022680076255750875253569097852512354454144712133727589366692297815805471359691496639130067596344119/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^17 + 345760313665015363929677126422313484167835480694973499337102898358352306489674560427355174651817517124619351460393493574235254579161508473/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^16 - 243553430971378216035345882973527308609558055199832613540678007586564858955595992613629594429380678579959370304568014270861883388913081563/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^15 + 13439834030424952563523342741380414206857128940215317684543395606578588119319821093265031482739859530406597736031323242178684133114415783/131690090012256542865901247132671216257570235900366739274894988996416925312058632691269786124872196797539802052227758752500959752868864*y^14 + 215537689963308444744786436381586530139752525216363053613700130823202156786323712673102272618488245044164136192155810879488741304677397/675537577009161505347109596033618188406365120792466677028731084169911807575436558766320568534347418695889147521989106455195025889792*y^13 + 114881372162331858913886361673375328627065544435030767968102513130889783443372868308471514388049161893891822085497509057213868133627645085/1119365765104180614360160600627705338189347005153117283836607406469543865152498377875793182061413672779088317443935949396258157899385344*y^12 + 1924574759174552692788091072691026377393581228779150831839852478784814024483894006356834166509879483771148196865642708628285143723079295271/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^11 + 7382719284879231045417525156071765499655758445210215688776233202444301136130274988112421972269088162590329856857148840382782415137985353/93280480425348384530013383385642111515778917096093106986383950539128655429374864822982765171784472731590693120327995783021513158282112*y^10 - 37513018247792662791036137049483980170842269687259034549145880634703449282866932112567499628631598501837193174997838619587148310208417733/1119365765104180614360160600627705338189347005153117283836607406469543865152498377875793182061413672779088317443935949396258157899385344*y^9 - 68281582433332195994683473736991942547963787832647214964152668540661167008365498893928392680343934361170641058309865238431943147185330469/93280480425348384530013383385642111515778917096093106986383950539128655429374864822982765171784472731590693120327995783021513158282112*y^8 - 2428412771834042433787302015893064074875694771896278398394936438915446936048235435931530008895413203877616574705097766210362528899499284915/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^7 + 808343263386889685503356346413261217130547948550142466346729916932812324495968247566687347908171505524703513189220030136586814794011989365/2238731530208361228720321201255410676378694010306234567673214812939087730304996755751586364122827345558176634887871898792516315798770688*y^6 + 105712521925497396443399306855780253871527246924842846343573728752148196231358494863533823613375151296941439718858795892065057170334115837/373121921701393538120053533542568446063115668384372427945535802156514621717499459291931060687137890926362772481311983132086052633128448*y^5 + 195733839554599822449632850304985622451179703915894604722887293407363569902247930978310441802688034541387428184447045103807624690409049633/746243843402787076240107067085136892126231336768744855891071604313029243434998918583862121374275781852725544962623966264172105266256896*y^4 + 25634821561072100692940717886067579038091693559678897818137117989819143960536145713361153694635679663325423468424242274981175269329060791/139920720638022576795020075078463167273668375644139660479575925808692983144062297234474147757676709097386039680491993674532269737423168*y^3 - 2483036116259417390539961331211239155398387312669529764193438768618829954690461199305460271442640287435270453378947104668752969327012873/11660060053168548066251672923205263939472364637011638373297993817391081928671858102872845646473059091448836640040999472877689144785264*y^2 - 492258659025598112839353682519992208033526929755568843448743825666546130777615529046217429361327728830087022503958435836679290532999507/8745045039876411049688754692403947954604273477758728779973495363043311446503893577154634234854794318586627480030749604658266858588948*y + 738020058552876474244031698247147289412035512391192580969664156236862470522048862040553870849562024133941311285902173468013746321379887/17490090079752822099377509384807895909208546955517457559946990726086622893007787154309268469709588637173254960061499209316533717177896

# 3 Loop Invariant
1072584195493865807390806717885964330119758131486322270927286665479023617923120010718771321054031808255433088951771277978156246406496951009427220728370225319046952188099/149847283905300817596807224911027214628725231283198695588167860088486509613692751589222440974152541180071649712407655282585154070575241065719820752788459181141404768020672*y^22 + 42051395474537779274953592848523618365045918371313318872461662800623743515211410432550436954286079994300226645393907186443814494818666685988644657592500299174885202802937/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^21 - 504468721970329092131775741886603644531159298490053957008293079117143007440383251174933819251264524739360262902794389372449043794123384407907183827721941246587051935046693/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^20 + 2191475577261720000191501719491613553747464670837082395462481284911206870846845512619021131677829218932684864410276743902827359311118976178924309120910763779464934905631591/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^19 - 6330490339478355469378184721273272921277207607106146795558515444966390240114433025578718615797255149531416200835360033200461310105742375634866915984594924638364857136974525/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^18 + 11089302224329441132339839715531237663111716212885886287004746744198056956397677866678654873981203066839557035982925394404281472211464486034011464173565131786335635310716285/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^17 - 18861104656147080482330997750583760543985807161880305469889927957578147036778051316085597743567454456197348768355233054745330017896083249313389890871681158065983136151266825/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^16 + 11728872102077865511262794675240413491122785533674442115467983234170412183449108237557751722654245072571219443465667153938634657858522159873205681290349808946202861188685217/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^15 - 746416555820286456987482221480864832078058360913975459497680604136410279250678121743457728441778769011711775396454971393355610850983543259571961058693196929080092209290713/17629092224153037364330261754238495838673556621552787716255042363351354072199147245790875408723828374126076436753841797951194596538263654790567147386877550722518208002432*y^14 - 43991805636111778629173749748476458638378214489859629074091019793497902668687022770853436036940935665696300048060154863919823721151234880613816646955232393426104559348948185/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^13 - 5582185251792206564690247729406525522715183702194357820495093644150489602835000747242822880735604431626628476038236041722687160077056377795825862053921365450765985314263585/74923641952650408798403612455513607314362615641599347794083930044243254806846375794611220487076270590035824856203827641292577035287620532859910376394229590570702384010336*y^12 - 61042569386952662421444701837293132810686500293122138667777758724448100403716362259769043356266942115194594444729528167541643989768821245417667722372271831701279088449491911/149847283905300817596807224911027214628725231283198695588167860088486509613692751589222440974152541180071649712407655282585154070575241065719820752788459181141404768020672*y^11 - 37259669103799646902218150018613095914645763209781654211221667389551031452913429985733518122621302972533730834920987201813912360037052144255800011758169764419677005637521975/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^10 - 2126595759529471470609499446032117303579957314629352268598438689071824924642888301124773199701059553763527464926146550342694622203030202058188677732542396315036490729189537/37461820976325204399201806227756803657181307820799673897041965022121627403423187897305610243538135295017912428101913820646288517643810266429955188197114795285351192005168*y^9 + 40419222471363419326259233776999621050216207142249236979652376896708829556398956142697911600309357538295616494130777976503486021779843548123919010179215543353662381900276459/149847283905300817596807224911027214628725231283198695588167860088486509613692751589222440974152541180071649712407655282585154070575241065719820752788459181141404768020672*y^8 + 74233814805309717687879296875736575643699880830793930479893875143616566390344199721885040118743351837123752628312455112464156011536084845638649126419035248456722663067801811/149847283905300817596807224911027214628725231283198695588167860088486509613692751589222440974152541180071649712407655282585154070575241065719820752788459181141404768020672*y^7 - 18433376536823414615507788322411652913687539103150271052674517221854510343208390056149279132301370145280338588907139082373793205115747416338614069116381706596289868678277417/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^6 - 24361530105619591151949772173780943059447313480284375448957376474559422192817553755049845805941331706213534950824632192362407492087321816806683558705064425599688378911367979/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^5 - 15499812823972927276308254504825587922984031968309684826428794140530228963866674727894864975916250480931245987911664461451618964639502489723692598828231694308012808309567529/149847283905300817596807224911027214628725231283198695588167860088486509613692751589222440974152541180071649712407655282585154070575241065719820752788459181141404768020672*y^4 - 27696714329208300305719149447667716321829647142878220779312994603756346367409531701047601408873616808145511907333136713656516666709426737513070341688388183961606117628273205/299694567810601635193614449822054429257450462566397391176335720176973019227385503178444881948305082360143299424815310565170308141150482131439641505576918362282809536041344*y^3 + 5321581588075831038331049937988688312360307366390809604114005500669896524063417917825370130443270901232556624653114579853627571404636550907374546924585197945479542826300575/74923641952650408798403612455513607314362615641599347794083930044243254806846375794611220487076270590035824856203827641292577035287620532859910376394229590570702384010336*y^2 + 458437002782295580385598141935607167920107639341944993467208204482258957141704755339206489197512808519003163094932355341818966773940809445876936088747713180003679147045105/18730910488162602199600903113878401828590653910399836948520982511060813701711593948652805121769067647508956214050956910323144258821905133214977594098557397642675596002584*y - 60045021347118839839826198781178716042836800577832818274394094802419814370945493887560490852330397743339940088270305834633683648350282813731679048885787216535306164436425/4682727622040650549900225778469600457147663477599959237130245627765203425427898487163201280442266911877239053512739227580786064705476283303744398524639349410668899000646

# 4 Loop Invariant
8398242765362410200911163646869046194768908220695419467938874883413879179480104836625523682888940730876941287001615205783370375292428536836149078375635169266242926843672862195291598357955991868874580324457376053477255079706864054352964073862743/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^22 + 33356114184680128409332369578205039682153849806053801444170816784887624003675134505183967808111388619918769335114792640232437453142290054303844357385082555503043400193709456515088723203686455812162175214731213061247717817725740845591389993948017/890938143576739099719842392001782385351598373881893097603531774610885448400724494012453425980049983982831942407357336398573410121484371347461372131320142761213631024658400127822163808609762624658743138488457734390825935766191792108819716605882368*y^21 - 128769393455568053509838971404353156829591972035192610455047289652961912465439785858711447497545409512787103006703139319167575882809580324221185172231846608243030890783222168244597491998866331833423067105944600370260411993338427065587029165682043/296979381192246366573280797333927461783866124627297699201177258203628482800241498004151141993349994660943980802452445466191136707161457115820457377106714253737877008219466709274054602869920874886247712829485911463608645255397264036273238868627456*y^20 + 8098956599223559700408365333935741760962426491290356375989761418033381265664945602300733711474051486419586805080853026256225354901319533257613389578031914303223021144986375806700839196687820646417765370361584522226463245788232961158337095715913189/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^19 - 7624173055193063431003691119627207178961229136729720499593900448432309989309153648411587325308051259020640415444482060122115863090211843667323789750705796863175208187380894219366230464101874348610775705370980806732983613952723568747163121481994659/1484896905961231832866403986669637308919330623136488496005886291018142414001207490020755709966749973304719904012262227330955683535807285579102286885533571268689385041097333546370273014349604374431238564147429557318043226276986320181366194343137280*y^18 + 38245065922013546766696501115571979366817850055963193167018888484998972737837282003486667324355724347500386077002055347100374187334860852954541868226267642210511908494642187489148888330152486889032110586827907096984774616059506893558820856268718983/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^17 - 66025746356463782362287139448154185406721594047095883066782432073806616667231262428621567265492921222289585544590823645854295260092259218727925963497210804781098886814952871922392578287525835867436104894870140004699157335891287369586652135434016081/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^16 + 6477015896209673553068586857982954223193585735925549216957821631560357417597446596501565710023409892922586893229121357353345653481009754789628696041990074506784022077471217191587433074523378536238932330351330229779355851413127897457269804454467503/890938143576739099719842392001782385351598373881893097603531774610885448400724494012453425980049983982831942407357336398573410121484371347461372131320142761213631024658400127822163808609762624658743138488457734390825935766191792108819716605882368*y^15 - 2780315699124876096381210594469643372222723557144148093531980218927013880774930178642318397088475442026457032344581044034558921550565554663904202612981359778092733853315996734665237987330672241755985403616089221214605171719144951026649663339505067/262040630463746794035247762353465407456352462906439146353979933709083955411977792356603948817661759994950571296281569528992179447495403337488638862152983165062832654311294155241812884885224301370218570143664039526713510519468174149652857825259520*y^14 - 18256156357130067266589289789282552805585968102526512769514187502917709281791067196059538391472473485832277796748731867278418547632156084136480139898247903222812954166676004251066607554104201540414518559000820917986772935720046471904055414262809/448067865407734409434642120298623207278011654537262672301112338870893908871818796023161047062990335939867200969300611747421751217805457326222778179098844679749361810832025813630136697148341694155473314468144102992771039914600579415016956651520*y^13 - 23073728970702910424394341680829666765046317849240469535167721995345335322514288746735339280763553032190021047663321470209854548377275329683220136308087894618852578533104341099770454871487674769533495114044525497752758129803263478357139076491546253/742448452980615916433201993334818654459665311568244248002943145509071207000603745010377854983374986652359952006131113665477841767903642789551143442766785634344692520548666773185136507174802187215619282073714778659021613138493160090683097171568640*y^12 - 176496548049316281631087467552920816952644557809155080824757212178511059916924163697546335621396474491612939687859032490514213577204735862093235018462508091712123184891915932514394140658723335981873934967747288882809857752066784972284302261124854589/1484896905961231832866403986669637308919330623136488496005886291018142414001207490020755709966749973304719904012262227330955683535807285579102286885533571268689385041097333546370273014349604374431238564147429557318043226276986320181366194343137280*y^11 - 3685192351255575589192923761383302038307863088997371815636040925865245225605015345044473533048820536999535894624583290045509024544447024776085711814022164738517547150915042004938724543211236111714866634762711829299774680454989491098939503451537275/55683633973546193732490149500111399084474898367618318600220735913180340525045280875778339123753123998926996400459833524910838132592773209216335758207508922575851939041150007988885238038110164041171446155528608399426620985386987006801232287867648*y^10 - 95922281405459858828122808046505826205862636183114916157709455074947427446544561065586782673865688385571136467450422597264702640424085337225677278228392565381413607245350292523277314505934818606231013685743244748613154786198949574249040907069485723/2227345358941847749299605980004455963378995934704732744008829436527213621001811235031133564950124959957079856018393340996433525303710928368653430328300356903034077561646000319555409521524406561646857846221144335977064839415479480272049291514705920*y^9 + 57781825639405829807461840692046402658942886174323782685598934107620949789899444178544494809830676315908596364383432447669122729605126239968918427700413546128499978895641407469265092690899155031411096650588758355785250336398777488671472363028534013/1113672679470923874649802990002227981689497967352366372004414718263606810500905617515566782475062479978539928009196670498216762651855464184326715164150178451517038780823000159777704760762203280823428923110572167988532419707739740136024645757352960*y^8 + 202589189003458047218696641230734962818441529743692669729246727609234171471235187384587115851968895814638050180444750466406179424680285813058181850218501541078620462024431275145826896913264286022166509534850408365867559853894821520949019818279440873/1484896905961231832866403986669637308919330623136488496005886291018142414001207490020755709966749973304719904012262227330955683535807285579102286885533571268689385041097333546370273014349604374431238564147429557318043226276986320181366194343137280*y^7 + 93776567403521363531687912238441639134168188747948403031884671486486973586393477283778858171167071156068690652121271155727020671243979536259408630813507194947421623785749542418019850357595613945337161588235574613860279068736785512385834058447464759/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^6 - 508264005776262863717994786975473376771449152010892181400931862199927547358307001856312187343509701542047445445356362803558437259179042069179241809197859860519088572877311459668665005687504473322300810148037879328116913701541018074646154160972419/148489690596123183286640398666963730891933062313648849600588629101814241400120749002075570996674997330471990401226222733095568353580728557910228688553357126868938504109733354637027301434960437443123856414742955731804322627698632018136619434313728*y^5 - 103361548041718337991799405369337794097514316360728371243639878269548861650458976431932590197161789241215491602241595424029938326735277311086667867504238096484240699973226026517086680079425302110055755423562038030985764574780999233184001905615753079/4454690717883695498599211960008911926757991869409465488017658873054427242003622470062267129900249919914159712036786681992867050607421856737306860656600713806068155123292000639110819043048813123293715692442288671954129678830958960544098583029411840*y^4 - 31718434683353757533763692583776758409550559973109145481922748662504588688955569284499381477487592553610097807401586958741342002197320706372269765915418827480048018516626024143330631183041187865400843702655656077195622017415525392196374555465368119/1113672679470923874649802990002227981689497967352366372004414718263606810500905617515566782475062479978539928009196670498216762651855464184326715164150178451517038780823000159777704760762203280823428923110572167988532419707739740136024645757352960*y^3 + 337662511803361657345873818759101365467895031670941187504389343005492682158692259940919251561672190762296858327866622286023682530419332036086916456228068317341166245081421001887177226135370662525683162313235621333461929934666561702085095750844931/34802271233466371082806343437569624427796811479761449125137959945737712828153300547361461952345702499329372750287395953069273832870483255760209848879693076609907461900718754993053273773818852525732153847205380249641638115866866879250770179917280*y^2 + 46223977525367170667185256686140175562109317346721702881688618212677440474432387844132333377615386781038184885497158765574639460194941199228819715708246240754498481171349087936874157529186680067002800193778633730916256746652673536906890321583621/7733838051881415796179187430571027650621513662169210916697324432386158406256289010524769322743489444295416166730532434015394185082329612391157744195487350357757213755715278887345171949737522783496034188267862277698141803525970417611282262203840*y - 5072480129186777512264245072910739767291925353855053721576096650687525646307182962064359752165673831766918484734172435258475803626135742322614609997920049968557921304334827404089956761289077844730125651669708800050098349726546669193639655383931/2900189269455530923567195286464135368983067623313454093761496662144809402346108378946788496028808541610781062523949662755772819405873604646684154073307756384158955158393229582754439481151571043811012820600448354136803176322238906604230848326440