# Manifold: Census Knot K8_298

# Number of Tetrahedra: 8

# Number Field
x^31 + 5*x^30 - 41/2*x^29 - 275/2*x^28 + 97*x^27 + 2751/2*x^26 + 183*x^25 - 14833/2*x^24 - 7015/2*x^23 + 24961*x^22 + 34201/2*x^21 - 55502*x^20 - 49516*x^19 + 165741/2*x^18 + 94684*x^17 - 163795/2*x^16 - 119104*x^15 + 100525/2*x^14 + 94725*x^13 - 14387*x^12 - 45145*x^11 - 3350*x^10 + 12251*x^9 + 4460*x^8 - 1843*x^7 - 1623*x^6 + 229*x^5 + 577/2*x^4 - 50*x^3 - 41/2*x^2 + 13/2*x - 1/2 

# Approximate Field Generator
0.897333544553780 + 0.0675424675454584*I

# Shape Parameters
1602215567039523678426613963407557729349168420160802095616/140758740910530849744158601026843915628541452809819354955*y^30 + 8221957418734661405666194898041412594908301318675647001084/140758740910530849744158601026843915628541452809819354955*y^29 - 31771150954690752406960659252530244952738785862480249559842/140758740910530849744158601026843915628541452809819354955*y^28 - 224572202670670463462428500597901747127963963895720421476628/140758740910530849744158601026843915628541452809819354955*y^27 + 8384605311034615848749795394778377346727308837701873664327/9383916060702056649610573401789594375236096853987956997*y^26 + 82308514487149821440752252535907909958894630964096084979589/5213286700390031472005874112105330208464498252215531665*y^25 + 39437988371296688655044257138803739532684530348504637218156/9383916060702056649610573401789594375236096853987956997*y^24 - 11817552807571265538545390604706629955858582821187215922699294/140758740910530849744158601026843915628541452809819354955*y^23 - 2413045918817426777493049605391789716279591124836223768544267/46919580303510283248052867008947971876180484269939784985*y^22 + 39065551907170262629682146120070526120575718738138280797928652/140758740910530849744158601026843915628541452809819354955*y^21 + 32880441574848939705733344803816370601621250592973395212163791/140758740910530849744158601026843915628541452809819354955*y^20 - 28173505661149147281656081957260266538156392186349650151540741/46919580303510283248052867008947971876180484269939784985*y^19 - 91548413085220715627887456239868169635039045980854482434147788/140758740910530849744158601026843915628541452809819354955*y^18 + 120073057872702895696966114908263588768298361488694790883021611/140758740910530849744158601026843915628541452809819354955*y^17 + 6286615030439283391006678354487076201569326379348066399802379/5213286700390031472005874112105330208464498252215531665*y^16 - 106803030567250586349196994315023285407832921422190461392265673/140758740910530849744158601026843915628541452809819354955*y^15 - 207778194123275853139653368965679552487620259156859658193273691/140758740910530849744158601026843915628541452809819354955*y^14 + 49328008518206705703823374381334320926593541275553262558343556/140758740910530849744158601026843915628541452809819354955*y^13 + 160395358888053311189893629152724099657555999923791478692149889/140758740910530849744158601026843915628541452809819354955*y^12 + 2416133546404191949351743716379245555648945273213445501635974/140758740910530849744158601026843915628541452809819354955*y^11 - 24178760990964566443052379411415581663900883202804226737067338/46919580303510283248052867008947971876180484269939784985*y^10 - 17739239304414133610659495127581410552597722137512302886359491/140758740910530849744158601026843915628541452809819354955*y^9 + 16862639009395638135222496158388106834670019043462871191536727/140758740910530849744158601026843915628541452809819354955*y^8 + 10273080734605396952249121473650654540044154038512513388116003/140758740910530849744158601026843915628541452809819354955*y^7 - 1193207880953263849628331172929932276970459657545066985447871/140758740910530849744158601026843915628541452809819354955*y^6 - 2844941884224969221661940831134919332926528964393522951138017/140758740910530849744158601026843915628541452809819354955*y^5 - 143312681086940344141573399291217893153797595212863615960414/140758740910530849744158601026843915628541452809819354955*y^4 + 9559759825669516041625975723513800422152262859784889279338/3127972020234018883203524467263198125078698951329318999*y^3 + 53208581469583860624066544813360234555218329877634015939/28151748182106169948831720205368783125708290561963870991*y^2 - 31302721046319344682058587344664160357829687043569305213528/140758740910530849744158601026843915628541452809819354955*y + 3969047773004980181694737778357953004220414350327745653557/140758740910530849744158601026843915628541452809819354955

228571429005960818695133461659711611088007638912258262600/28151748182106169948831720205368783125708290561963870991*y^30 + 1066238636948274230794606872957793361964330168196925500582/28151748182106169948831720205368783125708290561963870991*y^29 - 5014771971194510200759907863277342729810482513141387189298/28151748182106169948831720205368783125708290561963870991*y^28 - 29624638163900612037144266950224537675073320219105398179547/28151748182106169948831720205368783125708290561963870991*y^27 + 10477995955979727357408147750532311387659649311624963550133/9383916060702056649610573401789594375236096853987956997*y^26 + 33375521563311622278825565762867416085478194842265699764088/3127972020234018883203524467263198125078698951329318999*y^25 - 17904577914673406431091375556870111695611363381748478447140/9383916060702056649610573401789594375236096853987956997*y^24 - 1640873196571361224759602865410438382577909962537162558457369/28151748182106169948831720205368783125708290561963870991*y^23 - 90210280671221682274601290481590237079857732889633246188019/9383916060702056649610573401789594375236096853987956997*y^22 + 5591536354833858231562130962771973756459084552864421314366008/28151748182106169948831720205368783125708290561963870991*y^21 + 2065610368402269262708513768773936654432136436084831465552374/28151748182106169948831720205368783125708290561963870991*y^20 - 4219368100325561782095049464357399160564669445655675062258599/9383916060702056649610573401789594375236096853987956997*y^19 - 7030687169144792701274961136556343624997690890012525915199837/28151748182106169948831720205368783125708290561963870991*y^18 + 19596383986797298642197783957241294863417624226178161817457748/28151748182106169948831720205368783125708290561963870991*y^17 + 1628401177846588370531485367288298151140002555454595884188761/3127972020234018883203524467263198125078698951329318999*y^16 - 20824340578977020151412508140608783379350551951733321746427335/28151748182106169948831720205368783125708290561963870991*y^15 - 19072806931708653505009382537380608930058830503436352065776978/28151748182106169948831720205368783125708290561963870991*y^14 + 14601526338269713007037767562933401471938404264677808390618808/28151748182106169948831720205368783125708290561963870991*y^13 + 14992329708075229050971807035847673693788182912100483000659487/28151748182106169948831720205368783125708290561963870991*y^12 - 5681948842643345044948183869388805748067773820673334314804305/28151748182106169948831720205368783125708290561963870991*y^11 - 2296414242477935555541289899258228518973994274514635072013767/9383916060702056649610573401789594375236096853987956997*y^10 + 260789679500843328039677578845147856374773140476299008692061/28151748182106169948831720205368783125708290561963870991*y^9 + 1928335555337369478175124348248403640329222319812363162267185/28151748182106169948831720205368783125708290561963870991*y^8 + 628733464530490379118175418841512445718920151335987079021243/28151748182106169948831720205368783125708290561963870991*y^7 - 355407572891068004585616835585291874117277104887480518779213/28151748182106169948831720205368783125708290561963870991*y^6 - 218306034362975712448175531811619036238603062334502539451817/28151748182106169948831720205368783125708290561963870991*y^5 + 54725615960753023376715162489938412874880295268438577877095/28151748182106169948831720205368783125708290561963870991*y^4 + 8425874380570814103159356492569544192424735237360565528486/9383916060702056649610573401789594375236096853987956997*y^3 - 6875055567749952396039689853158775042082026920158474699961/28151748182106169948831720205368783125708290561963870991*y^2 - 119241203635730878446496483937599059844791214773730175126/28151748182106169948831720205368783125708290561963870991*y + 116574395128579606579590533745080402790066938466070438375/28151748182106169948831720205368783125708290561963870991

820251205842995962868262221898361415161387671827667234206/140758740910530849744158601026843915628541452809819354955*y^30 + 4484774738339959225087241371750343610948935487885807893474/140758740910530849744158601026843915628541452809819354955*y^29 - 14793590647154788900118892638693702509313021563394990613697/140758740910530849744158601026843915628541452809819354955*y^28 - 120041950227978943347123048633871347840086459105457282204133/140758740910530849744158601026843915628541452809819354955*y^27 + 1676508538746590629623124601945869222310098419525195313933/9383916060702056649610573401789594375236096853987956997*y^26 + 42576574247831518862116600735428334284617397368402672913684/5213286700390031472005874112105330208464498252215531665*y^25 + 45046627651692022173026046448280928655068926867868570029494/9383916060702056649610573401789594375236096853987956997*y^24 - 5865756715680548805951036326458531618201424382637505542902334/140758740910530849744158601026843915628541452809819354955*y^23 - 206928826110935936275033164032649515219773035010932024123868/5213286700390031472005874112105330208464498252215531665*y^22 + 18407796768538062120358999177562847628156456569683853769337237/140758740910530849744158601026843915628541452809819354955*y^21 + 22646142070103882205916856703686292510055242470490405969847856/140758740910530849744158601026843915628541452809819354955*y^20 - 4092332916367218501353258438814851386523370688591723623280502/15639860101170094416017622336315990625393494756646594995*y^19 - 58273468836656471136463299419872732915228767773632534156581698/140758740910530849744158601026843915628541452809819354955*y^18 + 45115629374263200650096643440035172753875438265345662930648391/140758740910530849744158601026843915628541452809819354955*y^17 + 11174914772070128749041503548115092974375559815469242271604887/15639860101170094416017622336315990625393494756646594995*y^16 - 27173837700645929193328834226315453925668425092792887686462288/140758740910530849744158601026843915628541452809819354955*y^15 - 114564094373886340150658190218342252663688228558218180763347791/140758740910530849744158601026843915628541452809819354955*y^14 - 4502246715228724953872573189538855146057655080267579109936604/140758740910530849744158601026843915628541452809819354955*y^13 + 81338900556443471957154735887761163433167420823038296641921904/140758740910530849744158601026843915628541452809819354955*y^12 + 20338649682174368978903320169821642037963063227744376433505534/140758740910530849744158601026843915628541452809819354955*y^11 - 1194025273172085403674498108036422097510717734263914839900817/5213286700390031472005874112105330208464498252215531665*y^10 - 15236155745892922135732558069273088740511370820382189133119236/140758740910530849744158601026843915628541452809819354955*y^9 + 5198083332334566273671166291301733865463394868633455054150927/140758740910530849744158601026843915628541452809819354955*y^8 + 5757743142079833057788051583226044571175765300317277705397413/140758740910530849744158601026843915628541452809819354955*y^7 + 490794119123557408111445919671791031663791812673515916899809/140758740910530849744158601026843915628541452809819354955*y^6 - 1272565049684805792605429174404304622981153208765568141930447/140758740910530849744158601026843915628541452809819354955*y^5 - 261522057422348476138088025651770438930789123174802394574504/140758740910530849744158601026843915628541452809819354955*y^4 + 12118718893286220425582460991843500623022724135317443991035/9383916060702056649610573401789594375236096853987956997*y^3 + 3844000372448900931117036791928582969640658960503315909840/28151748182106169948831720205368783125708290561963870991*y^2 - 14801942168800148492622038120955630296686649047937972598538/140758740910530849744158601026843915628541452809819354955*y + 1449036676489857053523809029881777907888936899261124333922/140758740910530849744158601026843915628541452809819354955

10783789665375075608744059110860280994535503273179973838/140758740910530849744158601026843915628541452809819354955*y^30 + 202475460376915917814576309224369099896610957793027108622/140758740910530849744158601026843915628541452809819354955*y^29 + 507610994570975449183534138807524113520324849491530472129/140758740910530849744158601026843915628541452809819354955*y^28 - 4553205864900581300066442204010533020376158618966626804309/140758740910530849744158601026843915628541452809819354955*y^27 - 1258297029067853034779424425853115376831189503200811277450/9383916060702056649610573401789594375236096853987956997*y^26 + 1118900575403491962262552362371985196930319707796904706757/5213286700390031472005874112105330208464498252215531665*y^25 + 13264417003342739524113714419738359859977475704438228945618/9383916060702056649610573401789594375236096853987956997*y^24 - 66629732195091523801363392886390904373489023733824349302047/140758740910530849744158601026843915628541452809819354955*y^23 - 360770746650671591680288994046174228196154747017455535363076/46919580303510283248052867008947971876180484269939784985*y^22 - 151395836663527777852847158833045307034272829392454955425734/140758740910530849744158601026843915628541452809819354955*y^21 + 3619996518783449922083015366775191858634580257636155942460008/140758740910530849744158601026843915628541452809819354955*y^20 + 501007008645888732907696950441091649289839255040703602447137/46919580303510283248052867008947971876180484269939784985*y^19 - 7943503893958962096980498618961817782963894220196606487641759/140758740910530849744158601026843915628541452809819354955*y^18 - 5168656649155288293636590653549853965751688485912588686621687/140758740910530849744158601026843915628541452809819354955*y^17 + 431649146070971275113388053733012656403663351990957431780947/5213286700390031472005874112105330208464498252215531665*y^16 + 10429324665531323805322401430330516981243955676894831437842601/140758740910530849744158601026843915628541452809819354955*y^15 - 11248390950682397226802170102413293260317537098804156687452463/140758740910530849744158601026843915628541452809819354955*y^14 - 12893451738631230739555348022533297479735589961433726124026037/140758740910530849744158601026843915628541452809819354955*y^13 + 6630590148923954893773982172252532641851735003002767344367902/140758740910530849744158601026843915628541452809819354955*y^12 + 9391573140882380612326394372560263330091444583825563404133717/140758740910530849744158601026843915628541452809819354955*y^11 - 569056117159783242511551914910772909441850524031192468101124/46919580303510283248052867008947971876180484269939784985*y^10 - 3748628049425709945681283197616241726894464884760114934749978/140758740910530849744158601026843915628541452809819354955*y^9 - 451721985455020448216045016270927196703739027019104656419219/140758740910530849744158601026843915628541452809819354955*y^8 + 785487738715784721422842233763560839285576331308861238725174/140758740910530849744158601026843915628541452809819354955*y^7 + 412432926092595414849705126804803803193531537679040046794127/140758740910530849744158601026843915628541452809819354955*y^6 - 101309165769003528434262119253948225809674955928412321439801/140758740910530849744158601026843915628541452809819354955*y^5 - 100757914954934075826897654487807616311485670288025811490097/140758740910530849744158601026843915628541452809819354955*y^4 + 441919477015197305978339106961780849801219238895281195921/3127972020234018883203524467263198125078698951329318999*y^3 + 1952399682593494389861609179000927876367994152832518275236/28151748182106169948831720205368783125708290561963870991*y^2 - 3152983846299207020865588148592714346696282534988926404074/140758740910530849744158601026843915628541452809819354955*y + 384926017927475670761202756016551136898038440465013905071/140758740910530849744158601026843915628541452809819354955

3611232063458633129708153246961734565339721115189286322964/9383916060702056649610573401789594375236096853987956997*y^30 + 18704813811392395422886189166688106462724593055841295726598/9383916060702056649610573401789594375236096853987956997*y^29 - 70665379459395417271449800880117202937903158029737573066746/9383916060702056649610573401789594375236096853987956997*y^28 - 509212501850728868831305763097197321078606302653902354206549/9383916060702056649610573401789594375236096853987956997*y^27 + 28746429050695603148068059781938973299281368052599325959088/1042657340078006294401174822421066041692899650443106333*y^26 + 1671012409461212476960595957210431699902038518438988054223557/3127972020234018883203524467263198125078698951329318999*y^25 + 173539247176703931731085553360770873737680949366439343314276/1042657340078006294401174822421066041692899650443106333*y^24 - 26495351351892489009698930499928024702394218615525958279642086/9383916060702056649610573401789594375236096853987956997*y^23 - 5808411138087112763956543443724581392981378346225946787958077/3127972020234018883203524467263198125078698951329318999*y^22 + 86973589773025636870529402307167947104605178553684616323704269/9383916060702056649610573401789594375236096853987956997*y^21 + 77362287348879244472812548950183551963825733113249828133018006/9383916060702056649610573401789594375236096853987956997*y^20 - 62137838982766111678490796126722193688102286900098978334764607/3127972020234018883203524467263198125078698951329318999*y^19 - 212225850724871100421772105375768836288889407801355946187142888/9383916060702056649610573401789594375236096853987956997*y^18 + 260879148313685658832332305688860471483505341200104927114071552/9383916060702056649610573401789594375236096853987956997*y^17 + 43174853877227725001458433485837228888596453439036898996045252/1042657340078006294401174822421066041692899650443106333*y^16 - 225566439083444275494133883525849573218373943630430888378430803/9383916060702056649610573401789594375236096853987956997*y^15 - 470224533306794016342168365163366093679426348231400430144240280/9383916060702056649610573401789594375236096853987956997*y^14 + 96672814349750837244129449373706511705979065500094227557525524/9383916060702056649610573401789594375236096853987956997*y^13 + 358943413890851693411328691376774650692555972817684970297373292/9383916060702056649610573401789594375236096853987956997*y^12 + 12738402606128905785882380024051931328823911670265766218512821/9383916060702056649610573401789594375236096853987956997*y^11 - 53457120015880082179360751885654215948494945684264208386563249/3127972020234018883203524467263198125078698951329318999*y^10 - 40954950956588858797499840723201992030964362772838232599389830/9383916060702056649610573401789594375236096853987956997*y^9 + 36727704291575770031731959677832615097409602589831517768590486/9383916060702056649610573401789594375236096853987956997*y^8 + 22679489860736992878190139771027822737194130747159703671888247/9383916060702056649610573401789594375236096853987956997*y^7 - 2545873193107216739869573846943272054680081829162768880456554/9383916060702056649610573401789594375236096853987956997*y^6 - 6298526950301575337511964421951992953123929350542407610210602/9383916060702056649610573401789594375236096853987956997*y^5 - 308362023675898741693266847385379251968540046694647271695063/9383916060702056649610573401789594375236096853987956997*y^4 + 327037563888536168855661234475410403953112555531705666228483/3127972020234018883203524467263198125078698951329318999*y^3 - 4005682289878694677628014872858407663817113243370773772208/9383916060702056649610573401789594375236096853987956997*y^2 - 74157502533476664689120927056246320681619886845850579245678/9383916060702056649610573401789594375236096853987956997*y + 10104628378626997061601041352839238005315008149060061349567/9383916060702056649610573401789594375236096853987956997

-13831116659960990409083497669357424017570755078748450129472/28151748182106169948831720205368783125708290561963870991*y^30 - 71671355429239675707034273613689852281924129306438630331832/28151748182106169948831720205368783125708290561963870991*y^29 + 270498339129333493669216808332662041753796466529532855403330/28151748182106169948831720205368783125708290561963870991*y^28 + 1950967598253399960633527983983340105622921489293771375818754/28151748182106169948831720205368783125708290561963870991*y^27 - 328891303251086461540087520609694217040626054994724857553407/9383916060702056649610573401789594375236096853987956997*y^26 - 2133755817584544822600926829399571819611332743870361140123267/3127972020234018883203524467263198125078698951329318999*y^25 - 2008275449778381662918085673946174398779567142164163613589632/9383916060702056649610573401789594375236096853987956997*y^24 + 101478575509404740296174995971359638129527654308947494634535132/28151748182106169948831720205368783125708290561963870991*y^23 + 22324732078625405524450293528085859506391493578851358054298784/9383916060702056649610573401789594375236096853987956997*y^22 - 333032414134981493319033491576384546299096201889176716864518507/28151748182106169948831720205368783125708290561963870991*y^21 - 297104527649836183278155883069592555826036341749481186693914899/28151748182106169948831720205368783125708290561963870991*y^20 + 237841388556916336575210269743312976331834511640473135617232400/9383916060702056649610573401789594375236096853987956997*y^19 + 814657680324769115508582281671065552337603510966428750040175288/28151748182106169948831720205368783125708290561963870991*y^18 - 997786862948313571226427774481191795592868371463624512109454698/28151748182106169948831720205368783125708290561963870991*y^17 - 165672638146334066331415419471954677636183079088119983192798018/3127972020234018883203524467263198125078698951329318999*y^16 + 861126113068645183022253475215253401810492380120454935024245147/28151748182106169948831720205368783125708290561963870991*y^15 + 1803853205773582624763660940337758425809852282157821342993600891/28151748182106169948831720205368783125708290561963870991*y^14 - 366583863182400979222917695164745987847406606786911978495158171/28151748182106169948831720205368783125708290561963870991*y^13 - 1376598439950881663220900644493640982604006557848733669041542955/28151748182106169948831720205368783125708290561963870991*y^12 - 51824550292813908699131638825423443393375227817731561829157597/28151748182106169948831720205368783125708290561963870991*y^11 + 204911683021467448191843079159045656899913072528672864067256083/9383916060702056649610573401789594375236096853987956997*y^10 + 158360694522094785040215317759796614433059595364168798537876114/28151748182106169948831720205368783125708290561963870991*y^9 - 140490034437055302488364922632054390657103228791488914609903601/28151748182106169948831720205368783125708290561963870991*y^8 - 87279826391512869828340018175106471693612485666833835901405590/28151748182106169948831720205368783125708290561963870991*y^7 + 9558220283604621001530394987143137398666822736101879317677905/28151748182106169948831720205368783125708290561963870991*y^6 + 24175790299107457887916579469451334915875495261539315550809234/28151748182106169948831720205368783125708290561963870991*y^5 + 1242807824982349567645495011376242630897510763354324067286455/28151748182106169948831720205368783125708290561963870991*y^4 - 1252797692158438611248730270722537863075908945990133100035406/9383916060702056649610573401789594375236096853987956997*y^3 + 6295322535874073468840116518168374727665692828614340450948/28151748182106169948831720205368783125708290561963870991*y^2 + 283883224851922943954527350490984241305751524598525271951793/28151748182106169948831720205368783125708290561963870991*y - 38133980490890336462022342113502680328335950427723470820213/28151748182106169948831720205368783125708290561963870991

338425077619594112551574589120717253832462403095835079730/9383916060702056649610573401789594375236096853987956997*y^30 + 1747053570382815423626145199071214461434446143284903731172/9383916060702056649610573401789594375236096853987956997*y^29 - 6657754070186255759056736893149736108942367233396260403921/9383916060702056649610573401789594375236096853987956997*y^28 - 47631248268680860582639031803703159834387650301875559410768/9383916060702056649610573401789594375236096853987956997*y^27 + 8390919791954739419412042115589284843868992429602065724598/3127972020234018883203524467263198125078698951329318999*y^26 + 156687398892482834444322758205106341590701798617396093594523/3127972020234018883203524467263198125078698951329318999*y^25 + 45932358269265197118940034029926382203336458522865687231208/3127972020234018883203524467263198125078698951329318999*y^24 - 2492275295151574211569674505024574039895210922853762778132853/9383916060702056649610573401789594375236096853987956997*y^23 - 530428557992732838011745866345000805465307056631077484097708/3127972020234018883203524467263198125078698951329318999*y^22 + 8214366067218642420163716012287763942878420699362465839545537/9383916060702056649610573401789594375236096853987956997*y^21 + 7127511041827282949713432278824799594850798271822685763340129/9383916060702056649610573401789594375236096853987956997*y^20 - 1967817928295678021467487305415234330780018518669032530369897/1042657340078006294401174822421066041692899650443106333*y^19 - 19672128299238816428321749706537359873533484805798760448976603/9383916060702056649610573401789594375236096853987956997*y^18 + 25036991708628003702961042892733147861464726797681716481752482/9383916060702056649610573401789594375236096853987956997*y^17 + 4025550944670611632674200046122957073046484771202593349042494/1042657340078006294401174822421066041692899650443106333*y^16 - 22109915390645872619288538718349770181754120098486492997975415/9383916060702056649610573401789594375236096853987956997*y^15 - 44134576471305515545901717159022404025207288641517306586293832/9383916060702056649610573401789594375236096853987956997*y^14 + 10122038723262648879964957690834186967254339158647366277169550/9383916060702056649610573401789594375236096853987956997*y^13 + 33990931169904497167036144286962156544924881426917291286116688/9383916060702056649610573401789594375236096853987956997*y^12 + 468748408354946667210664461953358408839713202326174180328221/9383916060702056649610573401789594375236096853987956997*y^11 - 5138093659344221188641327805744422871426190133451858929013037/3127972020234018883203524467263198125078698951329318999*y^10 - 3573088882916746613134284028626856432315073487583067768523028/9383916060702056649610573401789594375236096853987956997*y^9 + 3653836493736975242533593933196325519121815598364729221221717/9383916060702056649610573401789594375236096853987956997*y^8 + 2103115642096580521757950131175129999994709161327579765059925/9383916060702056649610573401789594375236096853987956997*y^7 - 304064598456064319059876899795646454493997289609725556710321/9383916060702056649610573401789594375236096853987956997*y^6 - 606596573316784916538364518469187520709063396223493912036704/9383916060702056649610573401789594375236096853987956997*y^5 - 16943532321496297092154589939941528761538313975540454479492/9383916060702056649610573401789594375236096853987956997*y^4 + 32449263776795514359890010033836060468614218349379524947228/3127972020234018883203524467263198125078698951329318999*y^3 - 1895504902727790145894753893621552934926879319648158002692/9383916060702056649610573401789594375236096853987956997*y^2 - 7505532297159741568471494010434102449058013754943020656636/9383916060702056649610573401789594375236096853987956997*y + 1084743843624907805319791672277829734250312525274839694504/9383916060702056649610573401789594375236096853987956997

-266823119935135016419978265389383266176993105890700931048/28151748182106169948831720205368783125708290561963870991*y^30 - 1408685569113239941054342268851948562513894281628657280218/28151748182106169948831720205368783125708290561963870991*y^29 + 5063008830969209340247878562804057051281044755417345737388/28151748182106169948831720205368783125708290561963870991*y^28 + 38035782046147238133779784990601099008559816616107889346103/28151748182106169948831720205368783125708290561963870991*y^27 - 4998275869260285779577969235966355580141652638470878870634/9383916060702056649610573401789594375236096853987956997*y^26 - 41043589199865428765709451136644722915077636007394792898693/3127972020234018883203524467263198125078698951329318999*y^25 - 51009522063933781322230733804719179922042089115045870240985/9383916060702056649610573401789594375236096853987956997*y^24 + 1918629752024611123258996361676249118502487902549030916286585/28151748182106169948831720205368783125708290561963870991*y^23 + 54342350742074456337523076790803303748553301068265033125678/1042657340078006294401174822421066041692899650443106333*y^22 - 6160083157561908917627412674667456574569051170150631422927405/28151748182106169948831720205368783125708290561963870991*y^21 - 6229447483997049778707268915883172991535395277637900511897547/28151748182106169948831720205368783125708290561963870991*y^20 + 473426986765564182656766551049718878725724156523848607399335/1042657340078006294401174822421066041692899650443106333*y^19 + 16546618890019176298845216200980474839056427886982010138004571/28151748182106169948831720205368783125708290561963870991*y^18 - 16901130458804090652059889577420106908843939773177237615951482/28151748182106169948831720205368783125708290561963870991*y^17 - 3261956638540542259344178031589902244805709319676071461823058/3127972020234018883203524467263198125078698951329318999*y^16 + 12871895699946963696883573231498629069402359518285418241190348/28151748182106169948831720205368783125708290561963870991*y^15 + 34282340846162877747021728985698084057809662994620365903827153/28151748182106169948831720205368783125708290561963870991*y^14 - 3206370559374709957222694524057536662447003452341689298056060/28151748182106169948831720205368783125708290561963870991*y^13 - 24955390242466641017222138071169506762532662238588490916237279/28151748182106169948831720205368783125708290561963870991*y^12 - 3380070326271234528279951054448531525987948993408558966199092/28151748182106169948831720205368783125708290561963870991*y^11 + 381539533493685339986747372028086967205016237069001533620932/1042657340078006294401174822421066041692899650443106333*y^10 + 3743935672648400360503528025225651251206151046118973840228258/28151748182106169948831720205368783125708290561963870991*y^9 - 1947021978318350854620929504817305450464480863816953862912050/28151748182106169948831720205368783125708290561963870991*y^8 - 1652547643237570568023519823701759170194787907964330766778562/28151748182106169948831720205368783125708290561963870991*y^7 - 11386637030798622365959718692780255491512504710485085087157/28151748182106169948831720205368783125708290561963870991*y^6 + 393896885985533141645323829567758309741810941190550455680578/28151748182106169948831720205368783125708290561963870991*y^5 + 50921287662734464643434146852873601106451696355686244205756/28151748182106169948831720205368783125708290561963870991*y^4 - 18340748696905557215642567190115681433880521174108556473509/9383916060702056649610573401789594375236096853987956997*y^3 - 2629997978416073470923259131152115021829916273748112907852/28151748182106169948831720205368783125708290561963870991*y^2 + 3931836554221171743056042347327664956468926358717036977709/28151748182106169948831720205368783125708290561963870991*y - 418826439058457249194119850458686807134078423798894503170/28151748182106169948831720205368783125708290561963870991


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

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

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

# f Combinatorial flattening
{-5, 5, -4, -3, 10, 11, 22, 1}

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

# 1 Loop Invariant
-3133452020795708597640995313892539567698269827035509512412/28151748182106169948831720205368783125708290561963870991*y^30 - 14724900422725002302820747658132949663415357698596281089926/28151748182106169948831720205368783125708290561963870991*y^29 + 68618489804246832750800138749311360299148003891956658146774/28151748182106169948831720205368783125708290561963870991*y^28 + 410320019285244188766183318484360492680481145384867276180453/28151748182106169948831720205368783125708290561963870991*y^27 - 141566989597747303750264825911941261010127773489350045417116/9383916060702056649610573401789594375236096853987956997*y^26 - 464739878668753832101849167590537581925736411932592418047323/3127972020234018883203524467263198125078698951329318999*y^25 + 211279765317631057926068999348960817871238623881636084071498/9383916060702056649610573401789594375236096853987956997*y^24 + 23011643406915207915960436755269086103738607782106472303071248/28151748182106169948831720205368783125708290561963870991*y^23 + 1503723470162398999181967358574170958739245548094331891188918/9383916060702056649610573401789594375236096853987956997*y^22 - 79115508930947447251754686742351143066358050513639255140448909/28151748182106169948831720205368783125708290561963870991*y^21 - 31965555738429177948709181885528913813172008355055791632144832/28151748182106169948831720205368783125708290561963870991*y^20 + 60328709584848106555491859936880614384169165424203325910841344/9383916060702056649610573401789594375236096853987956997*y^19 + 107435807214105714404081816261950028110122028522485519604600819/28151748182106169948831720205368783125708290561963870991*y^18 - 283250609788221862540610599382140623380973776029498235918255971/28151748182106169948831720205368783125708290561963870991*y^17 - 24977975350706659121940551382450331681142975460458026320443101/3127972020234018883203524467263198125078698951329318999*y^16 + 303731854961376126001543071738595526258332572251659257077030339/28151748182106169948831720205368783125708290561963870991*y^15 + 298401206736251802856984302092502900398459902571743697203084469/28151748182106169948831720205368783125708290561963870991*y^14 - 213882114186882873733630432440492873612560637453541513849731733/28151748182106169948831720205368783125708290561963870991*y^13 - 243976274181884135397976663424785865324237178734545131911274854/28151748182106169948831720205368783125708290561963870991*y^12 + 82488530721033075827164860746126326859705022128425970688523366/28151748182106169948831720205368783125708290561963870991*y^11 + 39556740420245926011287751135965856414186680762434091076251222/9383916060702056649610573401789594375236096853987956997*y^10 - 1690423926652738035609018863567864313671276391418952760429754/28151748182106169948831720205368783125708290561963870991*y^9 - 34354904322357109658497384814768275398390537160805522454274795/28151748182106169948831720205368783125708290561963870991*y^8 - 11591760716947456336070465195137661809654129671834248270763253/28151748182106169948831720205368783125708290561963870991*y^7 + 5956677743841782325440341706353241244546042693072955145135588/28151748182106169948831720205368783125708290561963870991*y^6 + 4185377286459855268842714241578060359742152046057665065119130/28151748182106169948831720205368783125708290561963870991*y^5 - 741957178543089063987272711980786247873511522190633185888173/28151748182106169948831720205368783125708290561963870991*y^4 - 190520444133678310660754136747785377320775021649631947062687/9383916060702056649610573401789594375236096853987956997*y^3 + 99363317632331787410044475524330989088610565573967737529190/28151748182106169948831720205368783125708290561963870991*y^2 + 25275393462522090941870121981473457347210398134535778700950/28151748182106169948831720205368783125708290561963870991*y - 4246214899619345817490011110655854973254353876093665279781/28151748182106169948831720205368783125708290561963870991

# 2 Loop Invariant
-48739312467302791502540030560520111894153628458286685562055832534589362133606558773419617782172282657179621421115304138490274147553985628707089813750063461556591/19628753116745878876757194136817710754322179261199884163157993447393036646279018283782227136322887513028522161751162378147963265998969500120018788471244137778714*y^30 - 127378998644106294192236002438130394679460826356615203910940896365881929988003354116948274111898373558134882901555607378716859740995016187777720178717676626411322/9814376558372939438378597068408855377161089630599942081578996723696518323139509141891113568161443756514261080875581189073981632999484750060009394235622068889357*y^29 + 3757890691401314727236800678203296040316979998707499066432180667828507758908803063464356892685687341170959790612344115649304366629779912328868420615776329753070313/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^28 + 27623672487049721035291322659539509727367125582128020581100460655321421526661535345995121306983320793841153605260552138757557640130503960139412431540965088276350089/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^27 - 8322216567009358379983111745152649468903845272155066977656400394874032315193181667287392028045301805150463033177737258950929905628058809384869572186375739789969857/52343341644655677004685851031513895344859144696533024435087982526381431056744048756752605696861033368076059098003099675061235375997252000320050102589984367409904*y^26 - 6666960675131550640145799345739984246381687404626838848145218056581184307711633405984441254953727765644755631287304195409585469687683590026707705556518814533182017/1938642283135395444617994482648662790550338692464186090188443797273386335434964768768615025809667902521335522148262950928193902814713037048890744540369791385552*y^25 - 4076652190445175826939441863833379459056948204698530294027469045395481906255353378161167135753710175698584171781996524885811283169546863489335639470761270611809555/3271458852790979812792865689469618459053696543533314027192998907898839441046503047297037856053814585504753693625193729691327210999828250020003131411874022963119*y^24 + 1413862187430814652848020731937899789962878946405723962317197448212724813277086291264978979890731118771013586412482470676376825916014948024327354999134345550514376769/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^23 + 670067686367041269046169648534568481793873701569268516667561741795897637090247724286491065718449652236888009084946727590027975668821273410556875607158259109888049221/52343341644655677004685851031513895344859144696533024435087982526381431056744048756752605696861033368076059098003099675061235375997252000320050102589984367409904*y^22 - 4585460773055516940938227824181021517131461227109040885812570474635249020002529751472339520305171763361149039245972701433459193854529944265859535568861012278005638729/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^21 - 8718121495819473428378460468715362070966412629108299393414947413382436790300804323809533775253558608548212299484596428082584232360343889172353330147397318390282430293/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^20 + 6436756545935579065617492703848907234774601345197791123486517543238192954242124544979808531698831258032184480911013619273676687595807213619345272666849252632853824941/52343341644655677004685851031513895344859144696533024435087982526381431056744048756752605696861033368076059098003099675061235375997252000320050102589984367409904*y^19 + 23514563115444718448398368947642850212031038974779346064785145592470233254073500327714509576864238860515164159391013079914941169287137032507486018015759006763860693051/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^18 - 13100000830260621474342668522389921515879976382746241102539686725184565271007009922164948425322449323872472925220200372763601124649732168412426824011533640420482060861/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^17 - 4703363393398449364411486435690888555545617857643010465683604016446158080361139949241168786163842149812729923478448708330378040566511588263370669195741891150807479367/17447780548218559001561950343837965114953048232177674811695994175460477018914682918917535232287011122692019699334366558353745125332417333440016700863328122469968*y^16 + 10586355108202102128809506740525376631045581664175530295161233733963536421036339116968138074017117704801903462866818598559620188912217120443285671125077201830781321583/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^15 + 50205973507000638419047273951391922573610725935429678499126205049696653994004677101845921787887376146307559363000798643353335631931924302538579322794971863306186696957/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^14 - 7051646614990444685079887690582805306084420069274424536892399004943918160082542442852347271707513198039672117957934417600149271086202479802563381848759563208855114373/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^13 - 18628010985003622993784434317222207862000217967290226688340956897257143075536728741117017787121860306264941308251339149870042230658531987170009454390408632988224192505/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^12 - 447438796001600854249965336405953323218466680749588160427004742667326786651581176707633850346363256127865351426543124152615254891313270388127938262517559160994104967/19628753116745878876757194136817710754322179261199884163157993447393036646279018283782227136322887513028522161751162378147963265998969500120018788471244137778714*y^11 + 5281338520401537274243206426675381590953167543535430741434620856355491537568444569120554607351903377144697282878808811725356443168668273777361265831403218417037668925/52343341644655677004685851031513895344859144696533024435087982526381431056744048756752605696861033368076059098003099675061235375997252000320050102589984367409904*y^10 + 5135958172716378998999685023713481481654485180482344772568786511241839989162303589189001864113011954579355918539651600950182599129692430389533544127011284444964453429/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^9 - 1607483654309657492112983246037197830849930091046549716004962416869448311523769386853745758825622390431701305026029831286884836063813359427240092792378526045785759263/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^8 - 1222017868717008047430765812218144778209342384330252616326169060820955452361680685503159997364450914856746542168549169431960480698417886833605758203441040852356224483/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^7 + 69743609532179343659495819712485429675807291402732562973619482748406016699447400503169794030018612459183651324672401941209284412838764873627932766523354930275187767/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^6 + 303226385096989255592144722014050494568251361354061105545851886497201280236989850104241207021133825649757179435956316185032130044731556037386137558391127161501301227/78515012466983515507028776547270843017288717044799536652631973789572146585116073135128908545291550052114088647004649512591853063995878000480075153884976551114856*y^5 + 62662310379818348393789483661569311168319573544313054467850476900581707765046423280972385570068107447277688792939296340336958256214072459999710797743666251873847625/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^4 - 3611443563053914866722011131380803240985306262435293335943366535179404159506996652230075609987573601965158447883754339967999542908531085760356169301039858953476003/6542917705581959625585731378939236918107393087066628054385997815797678882093006094594075712107629171009507387250387459382654421999656500040006262823748045926238*y^3 - 2515925346885184401539969492548548430430326221160908834814582377692458475343366149507411069722503732868380263802541203828925243910486994813178684374656808980959703/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y^2 + 6327698860916306407427590999762338828521965765557533064009311212470183834322630624615778231842972963787538250426099961301386459698534388542043557673235855520522891/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712*y - 292086981058413116542693617021944371607923645604097069779738447018397913709389565174744641197136104549443336907630184849739020228997467971856310647446997823494487/157030024933967031014057553094541686034577434089599073305263947579144293170232146270257817090583100104228177294009299025183706127991756000960150307769953102229712

# 3 Loop Invariant
-238006101940703548652403440509756443734405573851634890422329488552557252628824574864303654262750062253910435632878903452747261449299405377883487240037128445926091896029904925361106897947998579699115617347398264597/564260294932834564811729559312013763129328826872254937316412142440465865794556112646991311765678923215895895409241169261601286491874308194259176735892180874761439865590122760009287804196846759534433023718687209488*y^30 - 154138995722849591520055398249720217960551694918102867203839625755897147355279587993081138288327861929685953400318168098705660381203189337389424625925355938229524547977848551679737030420241896953972094645495444229/70532536866604320601466194914001720391166103359031867164551517805058233224319514080873913970709865401986986926155146157700160811484288524282397091986522609345179983198765345001160975524605844941804127964835901186*y^29 + 4657735198119372789067705071251724274449704237748694499978919924288120251097850711884896827084566722828559997775821824018961660281204581517986556483485110535780270837515382216185752861481415105772481639949476100033/564260294932834564811729559312013763129328826872254937316412142440465865794556112646991311765678923215895895409241169261601286491874308194259176735892180874761439865590122760009287804196846759534433023718687209488*y^28 + 67153802797285556940390489693583493176408237588864871833625185241466470880241844337041890585880679974447465325215185228033279923894132220296284202328677941115401319829811082730488939413060681883938860181068060437589/1128520589865669129623459118624027526258657653744509874632824284880931731589112225293982623531357846431791790818482338523202572983748616388518353471784361749522879731180245520018575608393693519068866047437374418976*y^27 - 22734702043567354987568820363929695122115757150524870843247275574079008818154867155701911027957964419943987044724390609340672511383500895584196617603753517827240292963497682783311158101532225499715597616312089436173/752347059910446086415639412416018350839105102496339916421882856587287821059408150195988415687571897621194527212321559015468381989165744259012235647856241166348586487453497013345717072262462346045910698291582945984*y^26 - 146972591255290863270244894744944539457037055597767927842852564301701673439541785600012725127035871114718508113823236687429955081315494187024037512126201407999671329841012037782037225348675592017298222902406926938897/250782353303482028805213137472006116946368367498779972140627618862429273686469383398662805229190632540398175737440519671822793996388581419670745215952080388782862162484499004448572357420820782015303566097194315328*y^25 - 137465357237933823606492443177406244824683898577019972503074482702284266638416564540914901873908300250658582325457402631695291351540513441414402105595790891516928329081427494186293405074158898660936964030945115629425/752347059910446086415639412416018350839105102496339916421882856587287821059408150195988415687571897621194527212321559015468381989165744259012235647856241166348586487453497013345717072262462346045910698291582945984*y^24 + 3497665307015915167778062619882152780346887640764413634214692982757356622841124589031391227744658804182787180143601750660611798778727274989036479106262446727784526776028627674161573385456288971618812477815531937619045/1128520589865669129623459118624027526258657653744509874632824284880931731589112225293982623531357846431791790818482338523202572983748616388518353471784361749522879731180245520018575608393693519068866047437374418976*y^23 + 42603799513226331232541724819291513683581088118596835430168854089837614829749003380712236380637312280120788897871598937794486827287790819417841624718244489973625566444556103583948566339448443556830994044590717616405/20898529441956835733767761456000509745530697291564997678385634905202439473872448616555233769099219378366514644786709972651899499699048451639228767996006699065238513540374917037381029785068398501275297174766192944*y^22 - 22982413987463782136244481713468198643246192171844417609862474329251970383219295875219505549317294179371214684056465906163186320851273110091767261687765762576436954301851902410690239721568815309722191653081295456000889/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^21 - 20435398977555373467301255825083215346331426353972584085302997482104275805988629811608667270372111476785817427441837166676095684616646228802219755432899793742915488577207434245325664985767354901913259014429633980760983/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^20 + 5480055229935011564056596680454116748308689700103145134113813364186051122742031602066256450579063897076294201276673934025395051218528381542300400034565795695299945312201875288229615915140646620311873425955856714926307/250782353303482028805213137472006116946368367498779972140627618862429273686469383398662805229190632540398175737440519671822793996388581419670745215952080388782862162484499004448572357420820782015303566097194315328*y^19 + 56090087018459913328470886087094638956286168827461632155857695193750216888344096101964193440088220152192638413200004313794833091917079889396054845435617491271829895192466794890215232197464837528836855947672611633084171/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^18 - 17290248775861663876319309083595895373854881827080849675332833106385292070384487743727632882960173233124772848224319365926609054403182161216575275202694942527741908505755074542294425213207567708329967451392647932086131/564260294932834564811729559312013763129328826872254937316412142440465865794556112646991311765678923215895895409241169261601286491874308194259176735892180874761439865590122760009287804196846759534433023718687209488*y^17 - 5710580668211897684024856959450668678158036050269941583927710547835306512780746895030354110804417811858971290643617988128417633556713068308762097077352043275878987049994623486116317629158220163490443720333877533409883/125391176651741014402606568736003058473184183749389986070313809431214636843234691699331402614595316270199087868720259835911396998194290709835372607976040194391431081242249502224286178710410391007651783048597157664*y^16 + 60038199773022508870373642382493561669485057972360811273258862180193875247454926441302718098496144715963060229303588428686408782448552750773848868801466322102916957610121515361882449329992092700296905885578969738416539/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^15 + 124587937273611412489813721918790861023777558517040580575453050123649665483925067728433534554463938850510155556495141829471208270685909472848054416231214491569453218404378109705789983693953057440598939494709933003467615/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^14 - 6515773620404427089055431434929501629787767121562489236665169789287634803726225767190071212879293155573643396901448321330380475133972989034311878388787770642151621409416438690528205596113134918462321121723642505258191/564260294932834564811729559312013763129328826872254937316412142440465865794556112646991311765678923215895895409241169261601286491874308194259176735892180874761439865590122760009287804196846759534433023718687209488*y^13 - 11921395877247261797273854680303333300811308558796178429521552598167507186336607360158092789796826781026605254394162053783772632470142252050241062958986091724287662602885404442074371439377701987738251968987654882395225/282130147466417282405864779656006881564664413436127468658206071220232932897278056323495655882839461607947947704620584630800643245937154097129588367946090437380719932795061380004643902098423379767216511859343604744*y^12 - 2984751076960513667392157835242654610236051831716901270244919916709021244607351518998614553779360026717082752159204434482798450613735591925566031235833689098203440519539700472299602093268676772970529807347899180939453/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^11 + 11411976056666384988381276571202245698168693164334209945812232412135684278516832430945877846475911997261494623379025244483690948294568372578834300638332081021449362141072320502952473250816092392049951816841574242819/601396530703793834065259322474834812821027260188920796500306040437480272629422981771373633643143003694000421432711078349694949631627293572351906992690840260870173051521580346399454094534342402914397041000465984*y^10 + 10684864912882742133059026190531349577977160125230267072001856355496892966829195715557127372974348688174105947689398472132753784281207902723110226338047240119697506635365180266548163572429575668055282894090687458491621/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^9 - 1239625816506061597414147243933850283018459613574447643939915661544211924451800511630638906392214654289432377019537035120134409710002532666073452916780690519930944564234824217278335244498559787984820130292412917830843/282130147466417282405864779656006881564664413436127468658206071220232932897278056323495655882839461607947947704620584630800643245937154097129588367946090437380719932795061380004643902098423379767216511859343604744*y^8 - 750800134452846903606072270320932275629747031530053414215774342789481200201492147618306073201693673034319931614213903417684221611047530425297680774953117500873991824497656147826099715634981297922816086152244168869885/282130147466417282405864779656006881564664413436127468658206071220232932897278056323495655882839461607947947704620584630800643245937154097129588367946090437380719932795061380004643902098423379767216511859343604744*y^7 + 181744893251682335506481978711951906731876275545547786760641498409656003591709137630492140177653625428099510693224507359136637359454844048851378375610027234427526695344843772602408577523538409464563840541656437118769/564260294932834564811729559312013763129328826872254937316412142440465865794556112646991311765678923215895895409241169261601286491874308194259176735892180874761439865590122760009287804196846759534433023718687209488*y^6 + 1690117932690500852759184679284341245632419146895096414544825315583771809920795035768431353409342847370763153031839472665203903284964514870590560909227556485575083164370224288259950825216964962214493831677568744628595/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y^5 + 4659722270000925603819829201026259880805592029299785437181067546292640282154111981892183231583017952725701117382673579011181706167438126176465591453741048024802777053617459618341351373408200787950803346622386423897/141065073733208641202932389828003440782332206718063734329103035610116466448639028161747827941419730803973973852310292315400321622968577048564794183973045218690359966397530690002321951049211689883608255929671802372*y^4 - 88809052705524606072987378368014697264108341701942174545899899883768514917741644769151994455624481454960979597479465737081251619078598579072473934186216209808118401382854805947178791801659856824501037050837540604127/752347059910446086415639412416018350839105102496339916421882856587287821059408150195988415687571897621194527212321559015468381989165744259012235647856241166348586487453497013345717072262462346045910698291582945984*y^3 + 857546602180101687398546442596472238783155665463227274462874167835983801931037792393027565044599611906248156101785908168341612149388414128494368483889723496740731060706088543974413225617793917557484529865753027371/1128520589865669129623459118624027526258657653744509874632824284880931731589112225293982623531357846431791790818482338523202572983748616388518353471784361749522879731180245520018575608393693519068866047437374418976*y^2 + 20271305745400034868694390306314125614784860738481320361674424315060427044857180735173096940613527714515018449196151720833737057170180514653232583529741920653535914023466142981141357437266507907909881351371813350657/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952*y - 2708183021449545828322160121727783263446606542953706660286709921868141700582098579696051254109036193983279031121426008800188183855894108203903719880280464760435009488125754663458135860815292969721733226425858857183/2257041179731338259246918237248055052517315307489019749265648569761863463178224450587965247062715692863583581636964677046405145967497232777036706943568723499045759462360491040037151216787387038137732094874748837952

# 4 Loop Invariant
5304485395242377106155029547506420203050258948855291284909057831235095938371621467405056829541307533625913798776902579284773106554949937452739176064625025612928842583099100892615753528215835889439095146341709078072744821037000245823027879227330132979525236668558285477640011703685276122652203745612932587899774201569691/4721153067087514456560213731894662066822930384026409097509276530067404600862820967099833778572972149846405756658584039337444624029395348342693416525489275833698210461175825660851506704685508580140852606197566512097589070273693596905796997585166693234031165393755746962537095291391594945826209743309043452108478073271424*y^30 + 559573188122110458504086012291075501961591585966907554247914548171952213906367049118497966788124189902213605373222836933857403019814057599182229836831110111020848081547287295077674290448499413613264699241082931140056858878169720520417389396513343108024513323996667128285431021698140586353752357725402361021116636700472253/94423061341750289131204274637893241336458607680528181950185530601348092017256419341996675571459442996928115133171680786748892480587906966853868330509785516673964209223516513217030134093710171602817052123951330241951781405473871938115939951703333864680623307875114939250741905827831898916524194866180869042169561465428480*y^29 - 126327716138663535894414388421115375673714077807481317335120135927419536862064418858732633909657905506225978121410237698961443062788522896892646777356869194240147276295956017109465393815354025296364298848980494619102425908489430635751487272617068367739435376963510162922799046348582619935826657785213788726970206555294001/5901441333859393070700267164868327583528662980033011371886595662584255751078526208874792223216215187308007195823230049171805780036744185428366770656861594792122763076469782076064383380856885725176065757746958140121986337842116996132246246981458366542538956742194683703171369114239493682282762179136304315135597591589280*y^28 - 30283732212843393048961210146519909657116767090187268065214334442167367186832911875436995038069812314821864746839972203640450188941438058571467288665722530392548558102344026669848726554605647269221547570162957491502992328919381381504319779233603397104520931262606670150719327191825266343401490387421580208457675610542855233/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^27 + 127846165099357766694974047460993384502314154947749524175749512461190859242875782915637356266476577909369337366387435669051916767061817248350170785044344346089417299755812072665695338482693787301255672410978445664478771014532970373359417159213352318014628569380204643156762161254113246688022587519378928674109808867474551/1967147111286464356900089054956109194509554326677670457295531887528085250359508736291597407738738395769335731941076683057268593345581395142788923552287198264040921025489927358688127793618961908392021919248986046707328779280705665377415415660486122180846318914064894567723789704746497894094254059712101438378532530529760*y^26 + 2733414645101055125128000829252815722555502448183889022544279263595355597268455684750672913001681791654506722622339932325861699205461826616997535159959397387025336878280821218662104443996761928973829843292836681467724118988077464552938293338868383522210404490090832493194347820820667217041812953107251208999165787820843573/1748575210032412761688968048849874839564048290380151517596028344469409111430674432259197695767767462906076206169845940495349860751627906793590154268699731790258596467102157652167224705439077251904019483776876485962070026027293924779924813920432108605196727923613239615754479737552442572528225830855201278558695582693120*y^25 + 39913599553375993086562534436122466666393441744306529308417121783628890540822915405344296480897638649047483589384884731348659823302979676348115292080981976622255985624372355803118999281233245689935803009816596361235512652784004075542117546690183865957605168218234824846375204584260909291909781150054190481896926880503832581/62948707561166859420802849758595494224305738453685454633457020400898728011504279561331117047639628664618743422114453857832594987058604644569245553673190344449309472815677675478020089395806781068544701415967553494634520936982581292077293301135555909787082205250076626167161270551887932611016129910787246028113040976952320*y^24 - 192589767047194454937231617992750586343724502667144850803729376737889241295451734931323661887503999116059861546991986074579869161560658714892536244221178167029330803353978124831677565912674211519148370606507514734088771469973183170214069988637678776700291745748097163068050040175647151623675534585696893096504544356643034679/23605765335437572282801068659473310334114651920132045487546382650337023004314104835499168892864860749232028783292920196687223120146976741713467082627446379168491052305879128304257533523427542900704263030987832560487945351368467984528984987925833466170155826968778734812685476456957974729131048716545217260542390366357120*y^23 - 129548849511690022569849904101769797599221834197882027792497992474903367074656625864135788026279373096001493277344820046298652790857340230484359315769153722952197719182313496987141262444599461499562605514602480032909845223220244665106136920323574070552320131974871898314670995566178623709830888980739347664532803552822466499/20982902520388953140267616586198498074768579484561818211152340133632909337168093187110372349213209554872914474038151285944198329019534881523081851224396781483103157605225891826006696465268927022848233805322517831544840312327527097359097767045185303262360735083358875389053756850629310870338709970262415342704346992317440*y^22 + 4976520880527101844719322509646876328902757189937261743275674030136789120173785042209901576891596241669907410805607244398010972206444407272827681973087152107312977065397363180386749699015753734167186323241689441832956108186514655199986316672508778395510875848574598790344994762598167452366322338269078436568089583483243177387/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^21 + 498801878836138335650398693569318629151839949716430387836517543761754212823378327369377056261241233127230613546155047778884453076613804802193766523927918147231842828658842948359652545978822810945742722644986456648311058666585488233135496213507529997279912922827029297353593841799142626902591954100745465437727905347190408557/18884612268350057826240854927578648267291721536105636390037106120269618403451283868399335114291888599385623026634336157349778496117581393370773666101957103334792841844703302643406026818742034320563410424790266048390356281094774387623187990340666772936124661575022987850148381165566379783304838973236173808433912293085696*y^20 - 385581960760675335812260291326580636601012948654702869830592874859128701568678586324659411069816112883683400988932135590631070071709640175519713816036812512210876457225985796766029405193109720290472532521090575569646453805852698460800545065246516370511288451539126103456647728554792333113794467654765690476388061106231725667/6994300840129651046755872195399499358256193161520606070384113377877636445722697729036790783071069851624304824679383761981399443006511627174360617074798927161034385868408630608668898821756309007616077935107505943848280104109175699119699255681728434420786911694452958463017918950209770290112903323420805114234782330772480*y^19 - 13342862932019236284333295414320802914435326247283453669405220963753709921667147541609812620106846065404779225988009375057048018683027519275929933809303478588813705437662353198561469131723344252043599725064502567096725124689461845472263647179612436986896399275426970649132876118584335230302089628229354669475462609873667873229/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^18 + 13936010550311035145914369062188643412912144687025567065400166133408203914907382050850000603702047837401360214217720810166400070588710392390135069918521585299873446666152303212825589117999772337909279336240822755436873346205473666145871813130471320033857598527281345030962849107432494247638517410507619796316749993878397629581/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^17 + 1326093959217033527929661542388789933272795816441938597057712428377682289961484382093808173605539935018194657802376032618111302214315626499241106474314254346773721195380648011984110288576161051349348260385186845990914730777757551732320409851668473789669590764829974888271390603479507984352445274478621019307054324640846839419/10491451260194476570133808293099249037384289742280909105576170066816454668584046593555186174606604777436457237019075642972099164509767440761540925612198390741551578802612945913003348232634463511424116902661258915772420156163763548679548883522592651631180367541679437694526878425314655435169354985131207671352173496158720*y^16 - 2173228288041851128515166000899538820682190730712913826147884643843331395813516630643720380956307977646416522495232020918301919751229619039796516170834179382381442086418193274161669006705625808517470467281031935177374038331549361192305523921260904773781296827215098242886860342722239075993924900325387726977730288359020278293/37769224536700115652481709855157296534583443072211272780074212240539236806902567736798670228583777198771246053268672314699556992235162786741547332203914206669585683689406605286812053637484068641126820849580532096780712562189548775246375980681333545872249323150045975700296762331132759566609677946472347616867824586171392*y^15 - 5637676370362007937175954942916628582744447035382697591826421876400358624792448846606967306062624700329801846868385237161605079417534637505573074276316778594974447840246260489032862485576095550730788512773549031041092441725050392675343717449099881226868294224929450227207981889706509306334345705746775276520947175379215097253/37769224536700115652481709855157296534583443072211272780074212240539236806902567736798670228583777198771246053268672314699556992235162786741547332203914206669585683689406605286812053637484068641126820849580532096780712562189548775246375980681333545872249323150045975700296762331132759566609677946472347616867824586171392*y^14 + 1501257090288862309754610282421339683023484562361007969801325420868291753633786589455343855837397781092126168665510626284596872492040296750999906713484036179646412533321433014222426630973264761542814745435585861023053027202456580237085192951826876326271777294824179492984349892455988395120231699282592635322144062482634328423/94423061341750289131204274637893241336458607680528181950185530601348092017256419341996675571459442996928115133171680786748892480587906966853868330509785516673964209223516513217030134093710171602817052123951330241951781405473871938115939951703333864680623307875114939250741905827831898916524194866180869042169561465428480*y^13 + 10430499543076357748591977242810583836062621606791556546531126971345097834908937675028839857546573084012454980030802392986329337479743731144729059078331054762896985452727272203620600462908419287448254274055419792288607662149048589419118476245332763849998767576625381960395011356015399611138977569164956601033758114944381905913/94423061341750289131204274637893241336458607680528181950185530601348092017256419341996675571459442996928115133171680786748892480587906966853868330509785516673964209223516513217030134093710171602817052123951330241951781405473871938115939951703333864680623307875114939250741905827831898916524194866180869042169561465428480*y^12 + 2584114497517985515558945900149469529856278366941526148420495463577754403576763249082236274956435802540693017105816752712576919154055030028806425984086059508712032579188201471750475022114896523227867799354427076613522521312098919198914234174373820871089181029891422474372539551612153443649512304921925270620668875525387624189/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^11 - 245403751934769636164093595116533436549777199544339061967553343992188415713306589438609279450172365375778697870693388720103533522609438801532329846465326331799420528226637165364728821097052701015955445463149581839339876064443948953912602184541321850435731071169447921981697095722556882282311793683115194435227102113558854889/5245725630097238285066904146549624518692144871140454552788085033408227334292023296777593087303302388718228618509537821486049582254883720380770462806099195370775789401306472956501674116317231755712058451330629457886210078081881774339774441761296325815590183770839718847263439212657327717584677492565603835676086748079360*y^10 - 3071205746187987669805707077355562037982521973044864573965756933431483089989933165790447739803942981921537953226424014613479448895868054002422380535684371778734165251754842700554044620849114993118496488518183963936874619557449515200994327922776234905530487624564858761995753436566549863073448836644322487149236972300207186959/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^9 + 874592065418633960318304478670138546029184540335353293426297913623383642287222697955176268985316724604502661966725652512327340968611755677336874883626574055835923334037125244271044503547705776455935226747063058337085942380255187384174145684936629809562771147705657117744230118339170304327710514632605310696773172762349437677/94423061341750289131204274637893241336458607680528181950185530601348092017256419341996675571459442996928115133171680786748892480587906966853868330509785516673964209223516513217030134093710171602817052123951330241951781405473871938115939951703333864680623307875114939250741905827831898916524194866180869042169561465428480*y^8 + 280075945463020675961127368725148958152376537055350450288931160766108575932097028251351765154428857060007362978791376268823286908534420769401625676809949553725859358996663044448644662468732522241814751696181387829032964050762109950069470304559697625444585323492833613964816838484195339880416660364581186021167183132603704863/37769224536700115652481709855157296534583443072211272780074212240539236806902567736798670228583777198771246053268672314699556992235162786741547332203914206669585683689406605286812053637484068641126820849580532096780712562189548775246375980681333545872249323150045975700296762331132759566609677946472347616867824586171392*y^7 - 1118781193105304857251755400488124788125757204195574077782438062420355953652839765814671005981374880453743588642743996637594749537857535729318477639444969254768686745020940359470546586783104424172999762765589683169407038811055228578673508122737051833480808035058745280443014565486866844069651926163168919051135568339112401/18884612268350057826240854927578648267291721536105636390037106120269618403451283868399335114291888599385623026634336157349778496117581393370773666101957103334792841844703302643406026818742034320563410424790266048390356281094774387623187990340666772936124661575022987850148381165566379783304838973236173808433912293085696*y^6 - 341983377752647804373754219486420672184831681553729572640318377377312651877741738097984866464869628822750422355707945289756912343238998328065212162064400703476311505102391876013013063959616890749195168542363801552719012695353362674772779840487908890804548610886642376459440017417132203252899692214198869787289314505806993277/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^5 - 8392747523074457200402888758163164555685705202312568509720066573243087834388765781042773167300502023680548086622468596093414782161238943437664612767440667485396881092067616661368961096203653616395548454198454509065509385138568206075830649711640232664250535291198044479206020434277419421605166385420035050581114381180763835/37769224536700115652481709855157296534583443072211272780074212240539236806902567736798670228583777198771246053268672314699556992235162786741547332203914206669585683689406605286812053637484068641126820849580532096780712562189548775246375980681333545872249323150045975700296762331132759566609677946472347616867824586171392*y^4 + 8192975659646644777750878021454286054907048258234872816767696458728941625179833296943085915697213837094568745622647048355291229811558312525079246700066858636155459305698947227383795503998118140563795456220697133845903978816968496695553378946734075461488852313621391702352591759413671786648502275608007623232409822348602269/31474353780583429710401424879297747112152869226842727316728510200449364005752139780665558523819814332309371711057226928916297493529302322284622776836595172224654736407838837739010044697903390534272350707983776747317260468491290646038646650567777954893541102625038313083580635275943966305508064955393623014056520488476160*y^3 + 2072466109546859470447466727565940014156216630265098411327836923156980255274046790113796675953221687902036125709639057971845708075948256257365075073558820255596930834632323096144449065341758578130078742552417358987375121719768756882259804924379658812706909366263738880011213678520548236406572847156968493703873317475747171/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y^2 - 3719255696197351524218780400534792014456761356568244854412570669482863388727065865312892607323971566528171302838090277972677082589367092934970844490354220255228329021627574677540044544971913264536588534601554073216344404171919206611236539459811166574800774712400439644070314476110250150985719644383609787805727301089045779/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960*y + 437626304820062843676765411824017486449291635047781612193994725446051130428377162641469959608786297927698853183588426572784090298550836593166685889666835157372443888698159529798479098401445217124056384363916306860077133283320031613061540071922394690196034598436223479231192188673675067335028453574363578692519889568077311/188846122683500578262408549275786482672917215361056363900371061202696184034512838683993351142918885993856230266343361573497784961175813933707736661019571033347928418447033026434060268187420343205634104247902660483903562810947743876231879903406667729361246615750229878501483811655663797833048389732361738084339122930856960