# Manifold: Census Knot K8_108

# Number of Tetrahedra: 8

# Number Field
x^28 - 65*x^26 - 74*x^25 + 1704*x^24 + 3309*x^23 - 21017*x^22 - 56926*x^21 + 113531*x^20 + 460246*x^19 - 116143*x^18 - 1808122*x^17 - 1103203*x^16 + 3515788*x^15 + 4645619*x^14 - 2696307*x^13 - 8095790*x^12 - 1787168*x^11 + 6727742*x^10 + 5026740*x^9 - 1908381*x^8 - 3601689*x^7 - 714191*x^6 + 977346*x^5 + 552709*x^4 - 14796*x^3 - 86414*x^2 - 24242*x - 2059 

# Approximate Field Generator
-0.677693356111237 + 0.615221625134731*I

# Shape Parameters
-1157494373119560304621230526882025254103996206767218374/146576373346417513687065855470415985680455946533171610221*y^27 + 681088682050283969915759087449341614201080973652976708/146576373346417513687065855470415985680455946533171610221*y^26 + 74767140159243962571944333057115325096321915334322580752/146576373346417513687065855470415985680455946533171610221*y^25 + 41737030146748468678703735671147295903353609246294894677/146576373346417513687065855470415985680455946533171610221*y^24 - 1992496253014532891567360332214123555420992432354163008974/146576373346417513687065855470415985680455946533171610221*y^23 - 2657538207655758442612621561030465552756619771835275550594/146576373346417513687065855470415985680455946533171610221*y^22 + 25771477503620659912302414874851074146516148287191928234428/146576373346417513687065855470415985680455946533171610221*y^21 + 50630253266532518205831630173402880289272921808256091840800/146576373346417513687065855470415985680455946533171610221*y^20 - 159610187865888010607470681717610128728697930155067686715289/146576373346417513687065855470415985680455946533171610221*y^19 - 436615481491722642500313634137084640124520747224653708989483/146576373346417513687065855470415985680455946533171610221*y^18 + 380640944267878984795339393608546422563794865043809139185115/146576373346417513687065855470415985680455946533171610221*y^17 + 63737121937335235483151655764442779039874223445428317609910/5054357701600603920243650188635033988981239535626607249*y^16 + 222900323234067268402522513539709485382380620494077089170082/146576373346417513687065855470415985680455946533171610221*y^15 - 4107616342400625846364126075469208496688238015068795227105203/146576373346417513687065855470415985680455946533171610221*y^14 - 2995871050999879533989555797334173597856774668795434090786153/146576373346417513687065855470415985680455946533171610221*y^13 + 4656732244573549897255805556207704059440209644341809384147406/146576373346417513687065855470415985680455946533171610221*y^12 + 6571136441139191956512366194341456521424007797634345054645771/146576373346417513687065855470415985680455946533171610221*y^11 - 1488400596424847009962933335013758435665596466789629193073658/146576373346417513687065855470415985680455946533171610221*y^10 - 6682325580749845365336456627679201659342382019210311887011996/146576373346417513687065855470415985680455946533171610221*y^9 - 2095408287274024710067365367279708873201187450952780227383308/146576373346417513687065855470415985680455946533171610221*y^8 + 3154465654763160098708748983627478656865204787812064987201274/146576373346417513687065855470415985680455946533171610221*y^7 + 2338760892162240288235561952930177248214145998549643158976669/146576373346417513687065855470415985680455946533171610221*y^6 - 377101478856522261235888588792476088118684895464137626228826/146576373346417513687065855470415985680455946533171610221*y^5 - 861250277820981088420373627653284809700239953669537970980129/146576373346417513687065855470415985680455946533171610221*y^4 - 179279346722268424962390816838594103188924181428229828231817/146576373346417513687065855470415985680455946533171610221*y^3 + 96535712175150025677188022312170894294768072419183723191483/146576373346417513687065855470415985680455946533171610221*y^2 + 45647265103574979093012327502466017627381344924610629481358/146576373346417513687065855470415985680455946533171610221*y + 181772911104149649309933223599877206425053138130226845327/5054357701600603920243650188635033988981239535626607249

-20976980096298347345375744095490217412943361436674047850938/140859894785907230653270287107069762238918164618377917422381*y^27 + 15586395128092229736829505272304639657917628787650286107382/140859894785907230653270287107069762238918164618377917422381*y^26 + 1352195544006938567868399097221411443669232656890483289089730/140859894785907230653270287107069762238918164618377917422381*y^25 + 546865299400348882984195297548114064770664158131300810941068/140859894785907230653270287107069762238918164618377917422381*y^24 - 36167649190433656355735192390983073375018770538267740538874990/140859894785907230653270287107069762238918164618377917422381*y^23 - 42514615641128850540444972331002679149018919579093622227178109/140859894785907230653270287107069762238918164618377917422381*y^22 + 472905009459001482953063075950750352093317930953967046076590494/140859894785907230653270287107069762238918164618377917422381*y^21 + 842453386428138761690406014491037001060604189613643542479853273/140859894785907230653270287107069762238918164618377917422381*y^20 - 3013582910885166052659043287514654029336788409021870505591688366/140859894785907230653270287107069762238918164618377917422381*y^19 - 7414739102007854489380036602578261079081265642139010275312776803/140859894785907230653270287107069762238918164618377917422381*y^18 + 257756089451877859089565653665619779093723165586917124974446963/4543867573738942924299041519582895556094134342528319916851*y^17 + 1103642117008406353046310575877718007014833655160841715883627828/4857237751238180367354147831278267663410971193737169566289*y^16 - 818243759315782536198346895025034015371993763772935321787339680/140859894785907230653270287107069762238918164618377917422381*y^15 - 73254682040288678254408662676067965604752240055015194041258990724/140859894785907230653270287107069762238918164618377917422381*y^14 - 42612011090468378237746083008159878829375309521349452614835841964/140859894785907230653270287107069762238918164618377917422381*y^13 + 88598001941290173352538851604065026667801123513161906485938038749/140859894785907230653270287107069762238918164618377917422381*y^12 + 103457251078067185142238431967126409137726682290650221227160956111/140859894785907230653270287107069762238918164618377917422381*y^11 - 40081727272083435027900358481966864705784773046140515435420549961/140859894785907230653270287107069762238918164618377917422381*y^10 - 110983375919795671959531388054108102788510071124586533818197939262/140859894785907230653270287107069762238918164618377917422381*y^9 - 22221873712955651622534301424587378587151364559758906793831691521/140859894785907230653270287107069762238918164618377917422381*y^8 + 56494584703413136051349375560154497162278072161184086393236935966/140859894785907230653270287107069762238918164618377917422381*y^7 + 33090935593479835458710418246190082357699469346876298510789549097/140859894785907230653270287107069762238918164618377917422381*y^6 - 9695674954579975249543543491583895001334678297606755912822848322/140859894785907230653270287107069762238918164618377917422381*y^5 - 13122326395165268297336063312335389220359845699585609248188859738/140859894785907230653270287107069762238918164618377917422381*y^4 - 1786466713848750116603135278485312358952121072346149579189757954/140859894785907230653270287107069762238918164618377917422381*y^3 + 1604383184144437731675269065769700421491037201606560985295766079/140859894785907230653270287107069762238918164618377917422381*y^2 + 608252144095708147825268781496441295632848882061234705418539215/140859894785907230653270287107069762238918164618377917422381*y + 2037066411648428463980598319442906916973459803440218140435743/4857237751238180367354147831278267663410971193737169566289

-17667768542298251692223241569777467117886488433430991710295/322614597735464947625231947890385584482683538319510714096421*y^27 + 173889837684068309953104478167276701775023633839476185276/4543867573738942924299041519582895556094134342528319916851*y^26 + 1138606421889053662218311612475326054420877965821506299655753/322614597735464947625231947890385584482683538319510714096421*y^25 + 513212728389235397549357213230283895380753277033208751292204/322614597735464947625231947890385584482683538319510714096421*y^24 - 428026128662225021380108470103058280552094480723509536855610/4543867573738942924299041519582895556094134342528319916851*y^23 - 37232643648506832183322843347599695453500080362936292590713018/322614597735464947625231947890385584482683538319510714096421*y^22 + 395332477824066584715624178152564190160837899396356502071926816/322614597735464947625231947890385584482683538319510714096421*y^21 + 728116014242305850673330145523871518764603297107661486288309631/322614597735464947625231947890385584482683538319510714096421*y^20 - 2487741630464799815658324561935350199461444689238299720028066030/322614597735464947625231947890385584482683538319510714096421*y^19 - 6359380799359295108014186513991069813280165905216906542541030509/322614597735464947625231947890385584482683538319510714096421*y^18 + 203659029768010330886521566784687763670690650453717370409030059/10406922507595643471781675738399534983312372203855184325691*y^17 + 27211107179312513624872255325725717106550287202676013530574485201/322614597735464947625231947890385584482683538319510714096421*y^16 + 1064321436157842125694101987707396070120672154398848000827238847/322614597735464947625231947890385584482683538319510714096421*y^15 - 61377932693699622464139423379675350025273086912371628088710017800/322614597735464947625231947890385584482683538319510714096421*y^14 - 39899974642968051015035362599737446254847462537943640153878156099/322614597735464947625231947890385584482683538319510714096421*y^13 + 71856486283361024299349952986867113679216957703735484797923255786/322614597735464947625231947890385584482683538319510714096421*y^12 + 92120610334995426492912933387358046682970707420084598436395328610/322614597735464947625231947890385584482683538319510714096421*y^11 - 27712331788772505064604041293038276957233914398888430245396867446/322614597735464947625231947890385584482683538319510714096421*y^10 - 96104352510096929516454983702714154042513692541770308889178507983/322614597735464947625231947890385584482683538319510714096421*y^9 - 25233241618202494280747382041582539940490561250211479090318160717/322614597735464947625231947890385584482683538319510714096421*y^8 + 46907624367921231163673804446177700847959095272511586564681655048/322614597735464947625231947890385584482683538319510714096421*y^7 + 31493798258845667380373284525985123386090903836145435671677107434/322614597735464947625231947890385584482683538319510714096421*y^6 - 6651903476138300055873568168251295753603481742560151307086839552/322614597735464947625231947890385584482683538319510714096421*y^5 - 11962600429904279797713863291483165288259091653304048782273561478/322614597735464947625231947890385584482683538319510714096421*y^4 - 2173568663735352919631271502990317001365624312660795207684426505/322614597735464947625231947890385584482683538319510714096421*y^3 + 1389302104379236351062433349589861235589556970135879282979376663/322614597735464947625231947890385584482683538319510714096421*y^2 + 610772535197965801351007613562686980888665919808694075706407088/322614597735464947625231947890385584482683538319510714096421*y + 64914291333277726911739071752879809755127463969503217958283605/322614597735464947625231947890385584482683538319510714096421

405658320906371929935947957147470758325614401087256613916588460751643319395592023/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^27 - 216205879133657170496811874187841742869508848225418162201637932298354928599397055/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^26 - 26231513334449085505201466723208253759186969189237719616032282113268415901577332035/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^25 - 16021007670816570299322209887445833474723518952527396896883487575367117183420141147/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^24 + 698406942987816101187178722332322072672898922274991054083877936702384782276116975311/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 + 967448784703856742722178447099685647491033529924119590700807937886655658226110993867/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^22 - 692798374819867334385446693824545773288951896951254459344621234265280813900716386774/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^21 - 18194578409417164362955609489467142082384626769272251991437789172932622105116085815891/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^20 + 55355307487123256573054124449954078877828921219601947105639937864517504539223750575981/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^19 + 155658269743203225961014936154580561358129764360863352482133293310766859550650340191244/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^18 - 9883514328743740879718463598520785601711186434705759542530612950545424787692114144641/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^17 - 22533477299566044724026243847148621544857019345107588666532303816428047618310913745860/607704059037599138772181516119832551777010416148618830007437859242704082409837547*y^16 - 95385148228187321263695782002396440633111875260597739183592639446285927395885805790883/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^15 + 1436823393912972127581946011125810927096740557985204661332134750037066408580745381227371/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^14 + 1072673773107083950610296139928134581522681682442103182618433648229591395029409446944802/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^13 - 1604942398465769708407860753531873501330472618331456683668756083409509735883200960126948/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^12 - 2293803979585447175909066766631404048948686034290650868102105112723871000284467581414248/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^11 + 37910409467743247715708557791643120671554917205196554887232116046837093138101435365167/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^10 + 2282781387690492428517421687613786921319813580623109540362656938787600021516456704772152/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^9 + 712386456364814615808113888113989361587878978370609272021756711512129129508647830252709/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^8 - 1053449843537877163000208457228512376309560020957255652474776954019129879426562724829872/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^7 - 763104057751590613338196345703193473051580097716781072240662388028112127954295337610682/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^6 + 128677994705824259984184485896755662829221242272341861343162426229469916907160039621298/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^5 + 270031162958889380661037245215380992098527543980683344699725672448887231236073442225581/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^4 + 50600849567468495928727303209331530320666588723512653769761238175790533994622904631465/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^3 - 29514122378156190134708575443107321599279960201565967078703306474689121342175653398035/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^2 - 12434091257601141819864926053441422822932494328292183953773635386015347966525627277300/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y - 42211479767533228758805621640506670965319467672422785745998789472511599737773394235/607704059037599138772181516119832551777010416148618830007437859242704082409837547

68962562666281162972333963965529879448343942168447998170217454997922810216881243657/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^27 - 456876084605596187893578533071599306264318676675761047856481392548555408166955179/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^26 - 2231455135443521637846806362009490130351950982210351650669831545059783768947487881970/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^25 - 1505061435247758510271736049631565272400069532313094996492207245030339864503352117982/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^24 + 835542388019778304476508663761748733273828855441029861422654840108404398931720240963/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 + 172457064879210056371623047192307083145951370733549537733487959879336313502710726685277/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^22 - 58571791084663114157274190009381082198797169881996196102924645024193156018641685684218/96250973658339740517840133976210401854528034373077397768101119398517515821681193021*y^21 - 1602699748023415894917634302570233223757724791693697804493413508105901729356125887648218/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^20 + 318369481178363060561847397411122558904149792457522965358190610524086207095292734253215/86293976383339077705649775289016222352335479093103873861056176012463979702196931674*y^19 + 27283427419314736696939798947882011750580644965709604309452032973420690601700740534222229/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^18 - 773263335023025056242276860447479434988587497068536639020441171160367808372232925234653/96250973658339740517840133976210401854528034373077397768101119398517515821681193021*y^17 - 57039397736092028669282798585146456967621084135725990920703308900263043337116641009208828/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^16 - 25025183010944214427019960509454122318360389070475375814595433592844092791570798249143409/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^15 + 248550745085117528829495153039014651139750913328120571107298999822143037641358444268322663/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^14 + 103773663212457153185710864915642231861820456207177414850173798819879825583684969660099735/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^13 - 268327810581437588782044945033550676604954468238475396156118779336434016139899203522604235/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^12 - 431715182969108623817108840960832232329099596213490621731874246836748368910376375959939463/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^11 + 4326596820987161353351889794602693613567826346841627585330040279975388395291216367609479/192501947316679481035680267952420803709056068746154795536202238797035031643362386042*y^10 + 425400190004800335150663513925612393941187140444311295003467391729625252375773369935894335/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^9 + 166332483295168020951572407420877086648395538004072710317769285667121680219955414030740161/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^8 - 95017915441745269510980980320143485477467845658660839193733689262705687767577438010516640/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^7 - 165243415444595774318785716697438518754790937792972213130087785023805624660849893278428233/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^6 + 6936678082666705849535937780639162634820968905172752412140868003655031978205447388791822/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^5 + 29249972385641455770521254531618459568454833019507647843112788579348339126828482807005847/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^4 + 15499674408189681760441439599700526803597555813791481320412955602138304656407423813827965/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^3 - 6039892425415129131008212975127953949416724969010891638165402924863748719926098847779997/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y^2 - 3548159477328743660385565184057248740909722679217009086755121384549199989471650192012311/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546*y - 457226696258984166872028805403787045260053113673253693205397345386168303404275020068901/2502525315116833253463843483381470448217728893700012341970629104361455411363711018546

-1199672582760183584845582165887145050087406573681749682102290138820730550391306533/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^27 + 716758807080394809221610085020964849388049070969610076682271707198125550242214751/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^26 + 77530819466482294770473373724282422092716650581597422616381665271517807136498538732/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^25 + 42465600211614283145482856569268424284191488719519304373695192648488978895180980233/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^24 - 2068351078277994910334742610071879971115889376002932947852342101317283103578046507364/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 - 2733241633858943343971692523514817831037098372068628327906860019504117427157581055842/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^22 + 2062550801801808097689331827719432415082858570936812292355987324559393526471315598372/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^21 + 52227878144432531641058614407713075324854098271721931768426251213993161812112058309864/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^20 - 166979015977367372768908321452338233255368448853663511634174981537591298717863593978058/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^19 - 451539321018072366876481774555529616535545792406710946187241296555455777536416769994944/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^18 + 31273625744660042906399097631810580487583789950775390992981149384565231081135603886098/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^17 + 66178511024363566643991389781133557012097436402329440962798341849375644683985279630726/607704059037599138772181516119832551777010416148618830007437859242704082409837547*y^16 + 182419807036505635811154898623062686446027231512590960719380766090646813979872304681631/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^15 - 4298212325431009895224772372737630418837616254476695978702770365545073139255799265197261/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^14 - 2999941258698089397798721461792572102562794487151781386403905306536845296493479447856161/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^13 + 4968375264629911649172032581502792741006496339053534370146361262073191094812260670409782/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^12 + 6697620864160947956587354338212357270093337416596252163237207393109041123864601559813006/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^11 - 138460664592652745808384568301669515193771418913335416378754074522185933606585502801451/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^10 - 6907302661413623049252600123246641667105184856144461572471583161222025031443011141689489/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^9 - 1911266905826901057783848259000525551248868483975780251796401897228886805857637166684192/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^8 + 3357795928555833823147959903753613135127293998575583714244903679300598338130977338975642/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^7 + 2284351333309709226468496629764315916101262737128454422108009375818994809634121168977357/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^6 - 484943618408344288355691799322127660909652433918344686383081878281171358810860055599574/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^5 - 862014923289370988314721478841444689125701180156789623777825609112109500217940497238186/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^4 - 147035145916031779685845042163865645243626680098312085592473784013003680719682582902203/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^3 + 101912584373338323591939193181155347138897834406963498942800264932657315146768465396368/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^2 + 41586947739081348329614284598077015058409431695623985629244507157584348549312325780744/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y + 142697781662570803153457877709833145453922654558998810403930185447587567566622178656/607704059037599138772181516119832551777010416148618830007437859242704082409837547

-15376891650777763455119072625005022848094743397856851624880173652273223542205199528/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^27 + 156791168414898730764361130576546667300673931738104397369776158057754540616266291/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^26 + 992419855632110901423921048325938121653169873727385912645875621690148269955626989410/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^25 + 420299523197268055046015927440155935322010784407008927700300069452789739309434006790/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^24 - 374231687192939806879199875784227553083945034212918818127068812241108400723461811005/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 - 31775116943987750478017758600285243063161248719638223786828406083490783749197376692872/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^22 + 26753690921501856050879627335823130927351021640829028659048136181153376548462919049463/96250973658339740517840133976210401854528034373077397768101119398517515821681193021*y^21 + 628257279474030619517493300032810084050309213281270792091212087697156393118048702951790/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^20 - 2218640961121902783386212549276230523100096453239810974907682982293008352615976257129573/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^19 - 5544478565037353278431431933626784485885989746212286719158369077342255539463338058019968/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^18 + 451313036063283606329882797464978190360682232251747038431730061768858163080019227188247/96250973658339740517840133976210401854528034373077397768101119398517515821681193021*y^17 + 24100121751866278255713827347494961683908930825603939370885730631854428565287346406133095/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^16 - 250355320690138237345695786571623972217848196103823721130254158602146622577585670393331/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^15 - 55740189978650126212648829098073469940288300256600649314355918808240687656793084181135906/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^14 - 33430167273206672150628045050104058771101846426015188141948425080789556387397498101568891/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^13 + 68283312575656656098177302965249236537410434784749171320376678838038830785790707746576528/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^12 + 81709849502112855917125222243339485214775130908181411081821995985938183358674096238715726/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^11 - 2404439651558958256412812005748610637851076258377595472590815268754379259827718323933392/96250973658339740517840133976210401854528034373077397768101119398517515821681193021*y^10 - 3090539612401987823373934360546109331911500873137411233400645645005448913532880149812862/43146988191669538852824887644508111176167739546551936930528088006231989851098465837*y^9 - 18526239604321709386689963228984774232472787752544617700992128731445533872185787935088352/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^8 + 47202607908655859894298443034461307915477975798469038406609013183722245686530223825526458/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^7 + 977079385079255249323026077390979579716040725289153077832242391197903026199269134416722/43146988191669538852824887644508111176167739546551936930528088006231989851098465837*y^6 - 8497578467516909988732452924712405894573509743734494060861251813539246374791129612184703/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^5 - 11815258997093514955748369898351404350796490355030726808798437013164617480716649565756388/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^4 - 1620762756294447549863344614372692320540415073088655712305478428665857746106366745336930/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^3 + 1559195386139392424915212540387811013217334985404846012941767542743179021761649524425674/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y^2 + 586431716297501364438900174634113659746363541980252473918350521965837889047461180096470/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273*y + 51375112450759957161009296080182747889600161884503834279629089464322727248847896895165/1251262657558416626731921741690735224108864446850006170985314552180727705681855509273

-54826266772659134383593459891474862501866848758318412738905679969057212617321504/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^27 - 41630724826691178204924533297394963439231002781354563111484392378217605995989045/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^26 + 3596582010769223907190638832501261428877312468434338094551015501334112090764957883/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^25 + 6713538404153116738295305054887794808773552584564085339709266046139029271420924017/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^24 - 92458398640678760455606557936035471547950743006971787683939625731971922740463573761/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 - 251578492918291749677069199262220942557861549356353275864885809672484646270860978140/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^22 + 82522220372671029736535036180923105700642060429499299564840897199747994206005770743/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^21 + 4019388144287115915026072546215506399091764165882066988145690621808407457988920692227/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^20 - 4670895292520765636744457750700267016096033773409233828534432060938851976038299212892/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^19 - 30736318850405661157392702898279941573888806920316938301937612051936550204209574003334/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^18 - 519585951133336157832172292017031142311412014318223180312744277446016610392582064869/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^17 + 3877826887320325316220476032264782931439899925150378103767776116527602328560897055568/607704059037599138772181516119832551777010416148618830007437859242704082409837547*y^16 + 112535009197285158391830934547820163433668596870103034111184992209990085216372028706036/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^15 - 191523182118158920535301646877848202565424140787703100230506310336839290022155647714235/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^14 - 357515998512361259518253869955045231280599496796411070562720110536891709045975126295527/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^13 + 84142637906294071783073313842697001067721006264882091353963775820441777981863882969335/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^12 + 538253351670204981848414861363181213159043248731405287338149883830820935543763687888729/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^11 + 16653070009871755688376089816939202361995515593849065574965377070779551069633210006850/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^10 - 378062037161901695081796451734472357481425380248828545498244777490911614091826578812514/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^9 - 351445352983059665934669422536153294561583446625742544163901745294487236601215611101618/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^8 + 67768626169299687207428379588366081444846201174023575001385699084082508593564407504237/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^7 + 197576785552911049713255910005722910200455116254956098924237929945447057050735632008476/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^6 + 47540673281497071152251390522067449250609227185377216463737363598340034949133217246101/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^5 - 41017749339930260777864490280136461000114601703672302111293383224984740272871305713418/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^4 - 21290419681242576178933810259638756948747769121989827804910462015937488134480056590353/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^3 + 714615114207136224263469898321646133828670996929797394336505937167201229037046490765/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^2 + 1871591187821242229749344045285000986659627496866176661594313445511080486875567366682/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y + 8101964833618904078081168633345574028561916677809027356170144129263476242023301105/607704059037599138772181516119832551777010416148618830007437859242704082409837547


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

# B Gluing Matrix
{{2,0,0,0,0,0,5,0},{0,1,0,0,0,0,3,0},{0,0,1,0,0,0,2,0},{0,0,0,1,0,0,1,0},{0,0,0,0,1,0,7,0},{0,0,0,0,0,2,7,0},{0,0,0,0,0,0,8,0},{0,0,0,0,0,0,0,1}}

# nu Gluing Vector
{4, 3, 2, 1, 6, 6, 6, 1}

# f Combinatorial flattening
{34, -67, -28, 34, 1, 12, -10, 11}

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

# 1 Loop Invariant
288973301796216759715744562746352982804816121920265934844943221451028516422591927/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^27 - 2020385537442384242796404301939323242484312745328068762769391427688688701634369581/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^26 - 7913556804055265424133440909800517440107112333046614742543080395955492349976716456/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^25 + 53485373629726441428520073105726693138841515063109113303167842312929262435834054240/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^24 + 226133309184856402243716831381162256255460402838323183446856059236803064458253848659/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^23 - 2513790734886430231028100857077564747758415435867249170447399721248919540974194025523/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^22 - 294744522715430871700316173965312642201148976005993601842909996357215605611766832872/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^21 + 15325452124448677077814409790925999938593806681070417111272253969358186554514985825558/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^20 + 80188273186834399239345422165820740087497636283173685150992398014194473881626893409717/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^19 - 196720615238716298559757050650989645713677660707686061499468942892719320383372452249083/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^18 - 19816617808141432214691085909220122536541892241191639756628037591814833212759541285652/1355647516314644232645635689805780307810254005254611236170438301387570645375791451*y^17 + 10845767514965911705726437531224335448836575895423988598731081632792402144823611535803/607704059037599138772181516119832551777010416148618830007437859242704082409837547*y^16 + 1982084459286027688329569259275288305303683481910652801864351901354300320644759514409025/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^15 - 828235020402022621973417641706932177749056603532175996843684384843077443522346616573849/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^14 - 2291224401843646850825739583678467140609898573693192681639062704706501544592362288078629/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^13 - 475754882692873538446223574588470155264791399583418463295741510013585527981183502839193/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^12 + 6378763338660415191792140803217244819658169842762748767704791420974706663070564522384847/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^11 + 243348617169364761186505563294833176455907351905931790988697255703608323882578039010661/2711295032629288465291271379611560615620508010509222472340876602775141290751582902*y^10 - 4978930994683937348361550648530295277251946595086809927248819189537438045061087603651405/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^9 - 4411223370666270230963578921689359899731297962227842566538117821516159519068502074360055/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^8 + 841723580382784513721512784144136119079641550582216094126458475949156467628217116207861/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^7 + 2865787371763413237967451367130789375161092108704699568539083640695927598699508486720233/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^6 + 83618512295619325786980130887839595348845152823066823396392214878348193005832914751540/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^5 - 430687340424361881740157086978025483647527305334517012112704310960848658641840408483816/17623417712090375024393263967475144001533302068309946070215697918038418389885288863*y^4 - 250800071343132595039628308358593818407242445790101777047774219169367461392489051671165/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^3 + 82839600071787897975323154918062103903872638222377627393691225107181791818809194908753/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y^2 + 43328557486325601514156308056372102357405921546107648463081719417285773943708481944743/35246835424180750048786527934950288003066604136619892140431395836076836779770577726*y + 186631104547686052737954813667106540252823163224161338205944093108947298068591479447/1215408118075198277544363032239665103554020832297237660014875718485408164819675094

# 2 Loop Invariant
1483837607179770288967681982353078452270561825339778383085327331413681997382275153402776641334543273173913089796815578251729510004253402842472115973057037800775179369260511129/908667930300448354135773044496284853802714192439508236245275726087897735195782044918824147337381129151028428408389607327395718124514120150731220017923821263497786074682806798644*y^27 - 933049006716811142961311476422558829441841028786075887066141976722113933543488396205684649528528807819876942652642784176938024064861370625564707022287777079919661084050236087/908667930300448354135773044496284853802714192439508236245275726087897735195782044918824147337381129151028428408389607327395718124514120150731220017923821263497786074682806798644*y^26 - 383304995929172653970481267136067003721019516236024432848009671763941277914212566033593043646160461495602542672006908452243571924080846048051471167963771634319677016675286855813/3634671721201793416543092177985139415210856769758032944981102904351590940783128179675296589349524516604113713633558429309582872498056480602924880071695285053991144298731227194576*y^25 - 197849600638218270567600457840315449780147772132130993723836120998281522888513800768207240209953476070319627076876662219711797821986581041659645044241307574896572887610200623765/3634671721201793416543092177985139415210856769758032944981102904351590940783128179675296589349524516604113713633558429309582872498056480602924880071695285053991144298731227194576*y^24 + 10228562232901208401672851600063072959854499638471139347355463253851302210329184869201802180356919066472251465967433244722327882029969266872613358724083292296860165072343954698453/3634671721201793416543092177985139415210856769758032944981102904351590940783128179675296589349524516604113713633558429309582872498056480602924880071695285053991144298731227194576*y^23 + 1646956290156387812421592263161420921729292999080418898567501213567099197036424501073931055970320674827107153832991161849816285641586455268720806419971060566486722625850203083803/454333965150224177067886522248142426901357096219754118122637863043948867597891022459412073668690564575514214204194803663697859062257060075365610008961910631748893037341403399322*y^22 - 851231498542613618074002720026184839927531198033219071798294824843005041511239998901151229478308397368787988195833244749418025987577601185082351834403482175688141783869779642077/23299177700011496259891616525545765482120876729218159903725018617638403466558513972277542239420028952590472523292041213522967131397797952582851795331380032397379130120071969196*y^21 - 84439553919377837137975446515762655180242154793928225395221418132554472522493002139070922418030944061117242186824321504186972214750830750758296143134797552161632834841164852832059/1211557240400597805514364059328379805070285589919344314993700968117196980261042726558432196449841505534704571211186143103194290832685493534308293357231761684663714766243742398192*y^20 + 51927943611312261938644617118193532686117223110960096740656167105736177417769483178254976079751490772742133303532342082813951048894071619054076835995425162170941701026455666834915/227166982575112088533943261124071213450678548109877059061318931521974433798945511229706036834345282287757107102097401831848929531128530037682805004480955315874446518670701699661*y^19 + 731247616815535698488687186957429537054205450344615941704027743204833692978739961111313538033121922294398936276429653654751925185801647847736812116125140691210499896853917003597879/1211557240400597805514364059328379805070285589919344314993700968117196980261042726558432196449841505534704571211186143103194290832685493534308293357231761684663714766243742398192*y^18 - 158976779226881317056877563114764036316794874713173219053182101421430455375812353207153465696506863017023032989093207381393592146165978260295433735714891087783233444613574460545815/279590132400137955118699398306549185785450520750617918844700223411660841598702167667330506873040347431085670279504494562275605576773575430994221543976560388768549561440863630352*y^17 - 26789675203750760610798155345736727045781186452442776512378996248632540467155399789939392890153058289479115696876466261282973418657400332547378214499519569084886551779011971951089/10444458968970670737192793614899825905778324051028830301669835932044801553974506263434760314222771599437108372510225371579261127867978392537140459976135876591928575571066744812*y^16 - 72866988663208927602255757323963044530137677776503301606200751368346690082810178155859827277926292110018220382581793807216784712757638116128643493285067604157572407648916915540507/454333965150224177067886522248142426901357096219754118122637863043948867597891022459412073668690564575514214204194803663697859062257060075365610008961910631748893037341403399322*y^15 + 10443371438836555317028878715399100918379880465096709749334635839791168498513660617408092175770265233843409573157991488844260277527933431167197263012074078041491948238040730667884793/1817335860600896708271546088992569707605428384879016472490551452175795470391564089837648294674762258302056856816779214654791436249028240301462440035847642526995572149365613597288*y^14 + 6905800231173995540078252946489401987680682613582079035090134941628016096881043823014224670227832120891506386985746560514547000799541781812343008860543821662273452492239721939662653/1817335860600896708271546088992569707605428384879016472490551452175795470391564089837648294674762258302056856816779214654791436249028240301462440035847642526995572149365613597288*y^13 - 24306232218878146593708744433111956860110662206074023652374138626003817220828140115046519511658493990630444666611313551458413042668646918669234591510999184860693249503897579866133847/3634671721201793416543092177985139415210856769758032944981102904351590940783128179675296589349524516604113713633558429309582872498056480602924880071695285053991144298731227194576*y^12 - 10398865288245541826006759891799563306939894797735287369991502425572689211801966271474383730713777064783415624901233701699634081576007232073535197022365925394570819625480807782765933/1211557240400597805514364059328379805070285589919344314993700968117196980261042726558432196449841505534704571211186143103194290832685493534308293357231761684663714766243742398192*y^11 + 90875398802616507183052204984960355825275940636058008902024480850083044028287236114059261248193064665394462309888153650132651894399305516932507246443301841015674502483220149577867/34948766550017244389837424788318648223181315093827239855587527926457605199837770958416313359130043428885708784938061820284450697096696928874277692997070048596068695180107953794*y^10 + 10698228021917917340143581898050929435573736581878140247783559538435493359863167020130334037721654419260219366003636633241961128301013999059156872650891684907382393835194248266565317/1211557240400597805514364059328379805070285589919344314993700968117196980261042726558432196449841505534704571211186143103194290832685493534308293357231761684663714766243742398192*y^9 + 1988686451470773360033095125918897648805211022999719439585953404612705865081353866159205036074653475519774805201193308639828100453535430620749940341681779673292024621914365522364395/908667930300448354135773044496284853802714192439508236245275726087897735195782044918824147337381129151028428408389607327395718124514120150731220017923821263497786074682806798644*y^8 - 3892073966724816417391433079344053280940962820808622611041319548421747246687388209072697072473885314315446335445019274321617328703010183373128812108528419244093305342441941812953663/908667930300448354135773044496284853802714192439508236245275726087897735195782044918824147337381129151028428408389607327395718124514120150731220017923821263497786074682806798644*y^7 - 3287109541616560904597223741992639324343756805087513530010061797524137791611911783010697077367591570761870963081001125110715810349206239833700129318065716682737236202100686324430159/1211557240400597805514364059328379805070285589919344314993700968117196980261042726558432196449841505534704571211186143103194290832685493534308293357231761684663714766243742398192*y^6 + 400899823419599103393771893417602207962531642531935938426120878776975921280900226611078766723824964739721298961164645003208731214141861764940012950502272135225756878235748454201227/605778620200298902757182029664189902535142794959672157496850484058598490130521363279216098224920752767352285605593071551597145416342746767154146678615880842331857383121871199096*y^5 + 3661513001624599862543155472757694944658956091669343917354964836731196311345371739889063263081419659382676086074569460822538442839270863543820325992185625529236895995390480880097649/3634671721201793416543092177985139415210856769758032944981102904351590940783128179675296589349524516604113713633558429309582872498056480602924880071695285053991144298731227194576*y^4 + 261887754880186314196476586168800836165266529295510183998431588488770940609697300178406503445111420456599963463848835603990445853028663602688397114254797079093259923499588472420099/1817335860600896708271546088992569707605428384879016472490551452175795470391564089837648294674762258302056856816779214654791436249028240301462440035847642526995572149365613597288*y^3 - 17831314082259269324598216319344887811216544930830857129499283213567479811465905097507369342288378039134046061610012121488059812211942372519852133770755640899176077285115231482547/151444655050074725689295507416047475633785698739918039374212621014649622532630340819804024556230188191838071401398267887899286354085686691788536669653970210582964345780467799774*y^2 - 194276409158888944526747906466191191435730324490724218860568488300244105772251626836876066481818952342931985258739349095456285915957241531374485371070986944254948397689954397611/4606681522435733100815072468929200779734926197411955570318254631624323118863280329119514054942363138915226506506411190506442170466484766290145602118751945569063554244272784784*y - 2531885032064913052825490006981837062146506078037827886125720508855342784723829663339298457285229661591023157641195295439828363375252348234193703082398632134303172245067963218193/20888917937941341474385587229799651811556648102057660603339671864089603107949012526869520628445543198874216745020450743158522255735956785074280919952271753183857151142133489624

# 3 Loop Invariant
-1264106995319918756934878104466249343400744104986009838193900288069949178627808355545969823333917726751539411051727527790565563999888742564109326839476979818910647460643608949730205829350698295450704356385265381777122444/4963532438542604087424686750434016598483862686517354809575788033545867254704086287908208239556875143050502131127664403486275558187900467263133997459059002179799264955974364511299147832025786272093325811738622326199495762441*y^27 + 30152008938761852502918900780712404002381669619503610258213513350253778867462545756080781991313833615902443869181162556308256964739600173178648060714701246200520179276371311323182496925900086547035260916154269290561635279/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^26 + 5236265863560060916995826356983789234205182042716724287271509815048114355402057888407729667720482031856113308110012178423281826260880507813880428413099836579899446003492702154412754572826704638968026261292610658877540271331/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^25 + 4036882507175500629444802119585125526638147192733291390868982333879750193375576435185102357315990236213763124348867650981337939607879305458063163114208883864302457979854041638796100326004776547979304450675158057120780165761/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^24 - 69323249709707120677771418792265297621471033257853331891407017939777750165627827555394730287993325393929533219513972384292043500108114991820683563156933237176975337134426373900389189055767106347542957672569168448361165759211/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^23 - 107651302833491241553130112897909383146452488925656613652346288171911371745410816899156939348196197016570146105504924897638978425285944366341112891159105487552255581168356559328470052276433551642465789891869462551534597337347/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^22 + 67771713720934702982915409460990230238977300170996723391229046155358250956348252640137624214307153245173451064000445579457588994871152852407848293233390119705396318177141866586940657214706127055828138705817201086969103885031/12217926002566410061353075077991425473191046612965796454340401313343673242348520093312512589678461890585851399698866223966216758616370380955406762976145236134890498353167666489351748509601935438998955844279685726029528030624*y^21 + 1957353355199613597450434500929342941843244556657922978337820273896080176041789765531188815474422936060424066061353378828195719610607415373174556527841970165177841656816427366408903802854783810799971823740718626131141518159199/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^20 - 10421109829352072986930746987351360337840291071729738723110004160985284839260947761182322056271161623410830832597906343534974318845336015041314119358522379329410192003565062747766459850844345518028469720428884264910863108411127/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^19 - 32767808862885700807624145151984884536358796952969271263003322593120075938933329440924811648361186538416250463190232167728700567954902770179227490862745742735107328535563070034078320299225981770293018252848774562617221902233993/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^18 + 1574767544668953301314445463143056919247107120083563504316810633483655965804225069708113296302577847972894030101128180809088956238913522189571633363782738072314366202800163715037242397994418024752393404730392739804750944579771/24435852005132820122706150155982850946382093225931592908680802626687346484697040186625025179356923781171702799397732447932433517232740761910813525952290472269780996706335332978703497019203870877997911688559371452059056061248*y^17 + 2311621108444966187585940505097490017267880832104190974892154708906800035104715521539673979006707917071392629293051462386764149719049452472611398502030214725873168357374604572735970388867203865985994292594007896154170539303151/5477001311495287268882412965996156246602882964432943238152593692188543177604509007346988402269655330262623041244319341777959236621131550083458204092754761025985395813488953943502507952580177955413325033642617739254616013728*y^16 + 39943928447250590974199134294571657533705172721777318911904677992465263800474807783926900940015925384314019279710992185768520718751214077344763055354317795905434694998079424067098396742508741179597037816273355360303631051449979/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^15 - 282617015225824701151850125407833918602789427768546221401877798471074685927728157839907015172044174856268656055783907988635928880704578567552507699515587695014545482808831530066452164682553603570811366750614518614159907321635671/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^14 - 32222278478213259348943911569118748635125471338590676208598313456056240706586834774931269156670039808774575813289196648203745149692395437016779801232920116018681952260515610351319818368504222693097005792767597402362262098002691/39708259508340832699397494003472132787870901492138838476606304268366938037632690303265665916455001144404017049021315227890204465503203738105071979672472017438394119647794916090393182656206290176746606493908978609595966099528*y^13 + 286711130751321292738004125493375600446823852904111238115745779309522813068152351841658565173381741067655719960788103640989334673567372159126359261801809544274691878732207791008896782767512458515590023057561232203902372638324931/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^12 + 251424918323845549114072559138193912209877498615529009121527838291673465831505132690213431749511871778411765731241560584755405073516693923544101291328362594108642445540349803801590516025515205969203581376032530780408337871930909/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^11 - 1277952900204172363020206207309742408692068514931314452862199760869484897026297501976155667072361943505859584579671002506003837577984573293764462875118637039383347673202849634024449984312199510177638959393633802317370281470547/12217926002566410061353075077991425473191046612965796454340401313343673242348520093312512589678461890585851399698866223966216758616370380955406762976145236134890498353167666489351748509601935438998955844279685726029528030624*y^10 - 232914579635364870767464266236031904380186142178682579599004467324979922256467504807067975933400791289789487171743337659097081222797886094602637058604722617966144392420134272358879846506225789894239044043185639825109171856749611/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^9 - 99427448965357196648101515394104087156508644935531435808793941061365762764256609168363068579043914025305138820420635503888284426140963746996573567822705602244272356690401534516085209174788336836927809270859165317521214032086257/158833038033363330797589976013888531151483605968555353906425217073467752150530761213062663665820004577616068196085260911560817862012814952420287918689888069753576478591179664361572730624825160706986425975635914438383864398112*y^8 + 11931442567096080775835512212728421038843790256782117556288057559918479720478819718062085047676265784422402474684272477491019553215128874309043344930861425787144383315159711857175174546539885104394851222098856288067889143675065/19854129754170416349698747001736066393935450746069419238303152134183469018816345151632832958227500572202008524510657613945102232751601869052535989836236008719197059823897458045196591328103145088373303246954489304797983049764*y^7 + 43105732157638374683670186233814849472947695355666482571750974883011459790611093146122330932149863921351626634099685568252072867110688501504757720384379700316618306424196217182017315599631403542471171644277945698793345929762253/79416519016681665398794988006944265575741802984277676953212608536733876075265380606531331832910002288808034098042630455780408931006407476210143959344944034876788239295589832180786365312412580353493212987817957219191932199056*y^6 - 2659607379255886846554172671362329199702926613639429884840829140908085772108594107249797683582528158121702506282230370599222956913160971936805531494587154947364513536629449522075900775573203479132823482056958834257165197464231/79416519016681665398794988006944265575741802984277676953212608536733876075265380606531331832910002288808034098042630455780408931006407476210143959344944034876788239295589832180786365312412580353493212987817957219191932199056*y^5 - 54377733897967838986587278431955990743432590419745521185377879867157480444486867583697527403404152921750078493409014678739864099259210123367493120312400945172330596986249560476631688882177882440302989826312364817248976682966273/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^4 - 13135429827849804486335637381065594504358612855220624110351236935817897861737950613312234971550069999186825956368099316680950531408020582229029740623183153130269072722768072610012134144948874923750760429156124745233997968341599/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^3 + 5089506188272297188732581120249691258454145508904844371972866500960995535339629447131987735283956762396493137669777275545400697052782538508932474814598572827334801490553793354301148767251311542182997964052245799306186251176907/317666076066726661595179952027777062302967211937110707812850434146935504301061522426125327331640009155232136392170521823121635724025629904840575837379776139507152957182359328723145461249650321413972851951271828876767728796224*y^2 + 151614470015012611388799978664754325769876691626127025252671105304532556506694909623747038712028011455017092377335503208612747565591313132328710249107901065199474075061028068291481609282327240978973349583140749752160097422871/19854129754170416349698747001736066393935450746069419238303152134183469018816345151632832958227500572202008524510657613945102232751601869052535989836236008719197059823897458045196591328103145088373303246954489304797983049764*y + 4388665929220505622082728381200220589385900746553156615182377040990108889065979604286547472515709641340277200768079929329379037675378236410906908167691445534046494179659854810213838805015820139341350646393961458470477971999/5477001311495287268882412965996156246602882964432943238152593692188543177604509007346988402269655330262623041244319341777959236621131550083458204092754761025985395813488953943502507952580177955413325033642617739254616013728

# 4 Loop Invariant
25471282995894826078782167664238573972321703329093286427382233766334239286009668435009317297925193276485458098487273046016075143746793624939164420105824552637606171522044955636549869477520639069250748958439398049103354856357551524399240532197583066862386808265022624807994019121616020659209351624915850115300240622591/54596480770051340822864572372446035423284357616370768121950766533639260483311724091532357477156494276673829563151475077957454219420937678639923077346588298774852321881099147038170785526673934073809782809484514306018655057158407178511336065538997465213963553321089917114126863929666436224443460185813792351006085270551040*y^27 - 10927379265459008858242215525102236145501743693703293099926632767115233611074932116005744274760779503602723643849309341997400298601016374722858477398377381813399533405538043979354486924578943781466154518417704619699529732841506922511540915489830918064181304914028058938940223862501433416051767403303127205800995808737/54596480770051340822864572372446035423284357616370768121950766533639260483311724091532357477156494276673829563151475077957454219420937678639923077346588298774852321881099147038170785526673934073809782809484514306018655057158407178511336065538997465213963553321089917114126863929666436224443460185813792351006085270551040*y^26 - 620795675862102682372725411690485276469783318401452554024483878710679280726351497205549496559315742418975520809318763492467577138293642920255761544072313847301543453103833919233528195108360615187889252752416966896136779895571486659499685193485445217200688165342798575080516022809237808312542689533119338750471958762693/20473680288769252808574214639667263283731634106139038045731537450114722681241896534324634053933685353752686086181803154234045332282851629489971154004970612040569620705412180139314044572502725277678668553556692864756995646434402691941751024577124049455236332495408718917797573973624913584166297569680172131627281976456640*y^25 - 21140686117734018106482984576398634118204365067162882827461547590258553030518872363636320766785223061504252246815072582228376974132186490357118051156038826401288829789599122248071201018322379306478871180739500710638450800183562501713352856880182278924015935234651180532856380432383796132005815514331052673869062374092759/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^24 + 159108661199755714344589893159697754656297768035049310558372175639677586349914127198302513626170434400405249297034534747040786865483961096979758176092737182903998968218069952054928594767390564845231592480777966267064577947492016356221028284363245619423058627095010129009886473095974276662774913594121249310044164098901069/196547330772184826962312460540805727523823687418934765239022759521101337739922206729516486917763379396025786427345310280646835189915375643103723078447717875589468358771956929337414827896026162665715218114144251501667158205770265842640809835940390874770268791955923701610856710146799170407996456668929652463621906973983744*y^23 + 73851991326412701802401716988395857667946667977561197451862871683748114230918088790532130484387484552227676699109991788219123833001248649083170035356362990445299651201128988135639514423003378103980785293626875293784668549172141450997054533263881557756643739448044021551489622833994831373633537539553742596651888619923287/61421040866307758425722643919001789851194902318417114137194612350344168043725689602973902161801056061258058258545409462702135996848554888469913462014911836121708862116236540417942133717508175833036005660670078594270986939303208075825253073731372148365708997486226156753392721920874740752498892709040516394881845929369920*y^22 - 197648619493410889839230952200534917636648050499662839643575558079513223721010176801650905190423599749285011677251015545775035820613010723433798068768249258529998272451485456080877682228869304037662871560326951984023662022433624943425127975014801603714658602696600697173801164813645568503308998599917818635912506914031757/18898781805017771823299275052000550723444585328743727426829111492413590167300212185530431434400324941925556387244741373139118768261093811836896449850742103422064265266534320128597579605387131025549540203283101105929534442862525561792385561148114507189448922303454202077966991360269151000768890064320158890732875670575360*y^21 - 2438911449472861649406053040836873333302207414340363242949933654362915101204611321996094517347214070709229713515959756073058468625843472542387983813442066339052334153140076440920720664629878376527880039593343055175444510658608500752168749638037508693280333009738577376561576712609193386209904908845645592688557562642678567/109192961540102681645729144744892070846568715232741536243901533067278520966623448183064714954312988553347659126302950155914908438841875357279846154693176597549704643762198294076341571053347868147619565618969028612037310114316814357022672131077994930427927106642179834228253727859332872448886920371627584702012170541102080*y^20 + 15772207095715535169113173557653554388085113225128878636046316705935333170463757907986389587152487616831641513818107597493800190409211845261065345471364512345197679957203959004944817838043035759733727352567163547258326743417757875896544804255951672310469952823423421455318228643408647885714663412878927358135832068147334707/245684163465231033702890575676007159404779609273668456548778449401376672174902758411895608647204224245032233034181637850808543987394219553879653848059647344486835448464946161671768534870032703332144022642680314377083947757212832303301012294925488593462835989944904627013570887683498963009995570836162065579527383717479680*y^19 + 188343848796415791173601831679943196847585860461719138589095222639461891666651601283779623957104785264315816405555781164411802418750845632888134354738587919029864819447471538557414912942955211084717041853776868933315595462565192984375075733004043506404657509072284659020363936260329891689581513988291359789195748098349495343/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^18 - 10942074261823579804037237523057515473424515080932545488157951573005370948546211703264876747793182256604413011648333168803789219816587220226821788282848849742098989180639086592567572944213207108712534827652760286936953288615473290741364468105985750481149926393433343548430429392489534199605781647811887049434886945110731313/75595127220071087293197100208002202893778341314974909707316445969654360669200848742121725737601299767702225548978965492556475073044375247347585799402968413688257061066137280514390318421548524102198160813132404423718137771450102247169542244592458028757795689213816808311867965441076604003075560257280635562931502682301440*y^17 - 1844090587211378082988960530503129678822991674782695409767844109763090753276179733774654554889433467248137062345922157558718858027031268550061196823947041183417049315507307706855180059024875511445598762435542450975854180372968251099425595853780706954512748703295749371637848975448215812878245729793522068986792142110767973/2259164721519365827153016787825353189929007901367066267115204132426452157930140307235821688709923901103744671578681727363756726320866386702341644579858826156200785733010999187786377332138231754778335840392462660938702967882416848765986319953337826146784698758114065535756973679848266326528694904240570717972665597402112*y^16 - 26253698910484062295935089388050095232120673765555738702797840893961486636523775112880029386041736487027161886601172833607179233741209595609266215732316147609182996709765939278082103162681592110268689209045255046024906961033578443601934557427110326287170846030024625722276654815353487359711743061787749194226623466318045449/163789442310154022468593717117338106269853072849112304365852299600917781449935172274597072431469482830021488689454425233872362658262813035919769232039764896324556965643297441114512356580021802221429348428453542918055965171475221535534008196616992395641890659963269751342380591788999308673330380557441377053018255811653120*y^15 + 1803436952490693730327312855120430117400284601719374131437116732437093200976327807061025855301235814363259828197752704110192580332709548451811872110750189273862679265812923997289849737959603401788653634728776714765706094342378309052720376218905926574913103621662987855562180992117804763460569518965971400871997173936826269081/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^14 + 362673880883798040026057054350890442868695719535403414199299607130641194532386063625052019339182013573128150096808606521317133711913640811623080608510553325298665231570873212957704907253018409331218859209059168664710958761516612370597164543538258705122778101393800758202215742674795183624434932927730195186591914857973752789/245684163465231033702890575676007159404779609273668456548778449401376672174902758411895608647204224245032233034181637850808543987394219553879653848059647344486835448464946161671768534870032703332144022642680314377083947757212832303301012294925488593462835989944904627013570887683498963009995570836162065579527383717479680*y^13 - 2060883308729868343938132689020445202355089635108184027141988145865786766267070498053857577942556089102569407097484388096652281125010674196217593077392286444479625687406563452755269506470565277316319477437991859871398273850609780864949242643291359914029425851520312815091753483009462178113822736820352206681871710316936082191/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^12 - 70136024608666501830334134100232068014871140617768487017612025856741906646871749324906480739968874826872212900362247810678445017838154104901061196483131350094883705161253408710447897023283497751860805991605122301174529945120945195744244292890930365952499879222622000736977533037347887792661917652150264319771277594567459853/21838592308020536329145828948978414169313743046548307248780306613455704193324689636612942990862597710669531825260590031182981687768375071455969230938635319509940928752439658815268314210669573629523913123793805722407462022863362871404534426215598986085585421328435966845650745571866574489777384074325516940402434108220416*y^11 + 15508393682278309734368040736397970544077912247247244090111762468011559407335416620524255703741673477901327395611630472685206137056385462979997506121317173928833274981155806556258984139726025230865326075971238959470238594616776857219996112436931157163687098802795299402988716096597043073292896198250969816187341128966580473/25198375740023695764399033402667400964592780438324969902438815323218120223066949580707241912533766589234075182992988497518825024348125082449195266467656137896085687022045760171463439473849508034066053604377468141239379257150034082389847414864152676252598563071272269437289321813692201334358520085760211854310500894100480*y^10 + 1647233658386601249021825491868652488408980350007577305030438576851325422944219434626416200649851476840696366477578399030687792021109527258598770185435883425119684953659697466753479116832123679341467849847997669729586631373671602262527830595719985444467866566835479682786171962951590685771566833274556242491012764392601417977/491368326930462067405781151352014318809559218547336913097556898802753344349805516823791217294408448490064466068363275701617087974788439107759307696119294688973670896929892323343537069740065406664288045285360628754167895514425664606602024589850977186925671979889809254027141775366997926019991141672324131159054767434959360*y^9 + 1135629430439500991132091440035724258464911897918645980993929621632901419383646747997632102723027459790674513895726790273660283899166237490248498431847761888608908326968619438854532789385539646804480262710472396245444341613882255133063555639963818804241172526533727289249606232011159494804892416997423253717167440127246152359/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^8 - 538390017785958312516305690501583872930326854259695039908789356911774756515208086022065647117617672560067283453939334835015892970902102031973029273051409390108146307198808937656510598571516795626962455440316959002320067344658282795119518160655867499765770656083709651226308391859029036591637652446373039084229046773770005587/327578884620308044937187434234676212539706145698224608731704599201835562899870344549194144862938965660042977378908850467744725316525626071839538464079529792649113931286594882229024713160043604442858696856907085836111930342950443071068016393233984791283781319926539502684761183577998617346660761114882754106036511623306240*y^7 - 1289943032207904869739070990288857264126048813057655809090700368641327432761528628554067927110836404771403730511796534886995107365989485418505518562500403548306662166079909488694688647715771271853816177096887016277546303044720185942941197152804575032625520682549081166907582669327473589176484970055419573672731868839311863289/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^6 + 182396934387416730883348891902943994237481316039910229949064478472051505165034259118103864836353969277383850374178395252656540969526767386229510954645171206250694381936677851627574312768236977302553186343112456454244107515735497306772854900657717207122779365367898637967201748404787060083423802358716436066182852540298713087/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^5 + 31439017954864839488410729409515609539906840313209459209419877721570472907453646171063450123975547570604460233601093892429063851597247070610085102426652389604041426231382407846264134152885135464292729896915814979415730974427549469248367401367766508016677993696907047461953846882499858266376504047861877833393451543556994917/61421040866307758425722643919001789851194902318417114137194612350344168043725689602973902161801056061258058258545409462702135996848554888469913462014911836121708862116236540417942133717508175833036005660670078594270986939303208075825253073731372148365708997486226156753392721920874740752498892709040516394881845929369920*y^4 + 121207891643580665370694373885958046150613598791098878339842589457651678584412295893896507554715101957606340472349944688704105159564239636772071113940978866612441732413431082771402826201455065242124693557327326824612665064720575154697447304343234188759132480177532703556809214073983073090407130309743922432404967334716124589/982736653860924134811562302704028637619118437094673826195113797605506688699611033647582434588816896980128932136726551403234175949576878215518615392238589377947341793859784646687074139480130813328576090570721257508335791028851329213204049179701954373851343959779618508054283550733995852039982283344648262318109534869918720*y^3 - 19426059291264972212287602807565585282652414564067339261891965043587239654970007156228268976266657828057338264898835781228306870426214183677625356688174779219005205189277755302458842517451609463767635112266887965364425178460098527405752035240016374752446749588249177670942379244105550333967118362512980724597259032048795561/327578884620308044937187434234676212539706145698224608731704599201835562899870344549194144862938965660042977378908850467744725316525626071839538464079529792649113931286594882229024713160043604442858696856907085836111930342950443071068016393233984791283781319926539502684761183577998617346660761114882754106036511623306240*y^2 - 123506129416196147207283098761943250706775205773952431980590269214543316464046441876059773549492249321149437954923425825345823309548575538904716947892808360398346090785874987320994278850131615038600911800034239924958771492453268806603492143708904037210315791071991677001816944269874993273421575677957115509622307601009677/3736641269433171615253088603437371245700070103021573483631611397739569158553654120333013059273068049354102403561697914080738311595349346827066978677713267596757953588820473941775947298403539214177095401409586530449945973493731289784045814371490320813122980835663948699826173196707208562889666476595620769270378459581440*y - 49749138029169655575067329119038632504659731041192423308805920752996060870512830117003603757439355825858700941063189491919649287201897031140660216404975010381370422365123796681995544504377306573805557870022037616450714209369077423824104351135659080614078792203411382169733862957294372011499611185964541216395962538910943/11295823607596829135765083939126765949645039506835331335576020662132260789650701536179108443549619505518723357893408636818783631604331933511708222899294130781003928665054995938931886660691158773891679201962313304693514839412084243829931599766689130733923493790570327678784868399241331632643474521202853589863327987010560