# Manifold: Census Knot K8_4

# Number of Tetrahedra: 8

# Number Field
x^29 - 2*x^28 - 38*x^27 + 232*x^26 - 146*x^25 - 1598*x^24 + 3521*x^23 + 3446*x^22 - 929*x^21 - 26297*x^20 - 9771*x^19 + 62597*x^18 + 39895*x^17 - 71113*x^16 - 111216*x^15 + 80384*x^14 + 151598*x^13 - 91225*x^12 - 108533*x^11 + 61202*x^10 + 47391*x^9 - 20569*x^8 - 14280*x^7 + 3005*x^6 + 2748*x^5 - 50*x^4 - 230*x^3 - 26*x^2 + 5*x + 1 

# Approximate Field Generator
-0.172460838141702 - 0.128994494663964*I

# Shape Parameters
13062101125783967207407520357720898352686775422887641099350892218/20590092537991656100447826007235479935337788738551822386778675777*y^28 - 2718761916675897135293639371268213605230662038559404104569934298/20590092537991656100447826007235479935337788738551822386778675777*y^27 - 527235854937102815293901586768212306123783078099259492369561167936/20590092537991656100447826007235479935337788738551822386778675777*y^26 + 2122889112121106404839453135033452808628330226064656865043706593179/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 2901148580273722974504758853209865817643396611229187195686565259297/20590092537991656100447826007235479935337788738551822386778675777*y^24 - 21129490577224168246993535527676775554395740588628197331379504096979/20590092537991656100447826007235479935337788738551822386778675777*y^23 + 9018892507421385277405270987570008690054451795888762862433072738015/20590092537991656100447826007235479935337788738551822386778675777*y^22 + 102186636663406430994294214688957047748547922987409628781110724122355/20590092537991656100447826007235479935337788738551822386778675777*y^21 + 102856099603569691414895792894357462003030491029768195476388616458581/20590092537991656100447826007235479935337788738551822386778675777*y^20 - 279599949769496458413373705689466731894549079669781336368425312087323/20590092537991656100447826007235479935337788738551822386778675777*y^19 - 685736547438519038109369398599304381817831774521861842603748297261863/20590092537991656100447826007235479935337788738551822386778675777*y^18 + 216220899302374915677639872100015433821704543263798176815414038689701/20590092537991656100447826007235479935337788738551822386778675777*y^17 + 1507076971176297125962417013594210756477121220605222023188970680663740/20590092537991656100447826007235479935337788738551822386778675777*y^16 + 605115513380524095933680557829568303673449288134367769483106686193682/20590092537991656100447826007235479935337788738551822386778675777*y^15 - 1946649160131287837311556698559900125406129999707016320377032476548510/20590092537991656100447826007235479935337788738551822386778675777*y^14 - 1705783279532097888455476684566020106559796545647194732344375469651828/20590092537991656100447826007235479935337788738551822386778675777*y^13 + 1914639919229466762003748435984925883979830879330953732957259165040348/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 1973579868922679443000499677072397816940185382401325403440018403953370/20590092537991656100447826007235479935337788738551822386778675777*y^11 - 1387989881636039815878153568329655109885587762302534049441872184963868/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 1328304107002087660870590099534673952697282008458982881473058833118400/20590092537991656100447826007235479935337788738551822386778675777*y^9 + 585800209196885840090109493197595429955889691270753724115861784059222/20590092537991656100447826007235479935337788738551822386778675777*y^8 + 555002543812220019234160201260656120821969261132010188994546312887444/20590092537991656100447826007235479935337788738551822386778675777*y^7 - 98188448804197415417495907907958577224983769629658673631938317623330/20590092537991656100447826007235479935337788738551822386778675777*y^6 - 132665335116215019271438781298711303464159886247406154777041399046491/20590092537991656100447826007235479935337788738551822386778675777*y^5 - 4699908309183566163685393721769592146427207831675211277655057251259/20590092537991656100447826007235479935337788738551822386778675777*y^4 + 91957427103943733796539942371667660527738894469507972996984141729/136358228728421563579124675544605827386342971778488889978666727*y^3 + 1712311899368379345590182765247718862039590621996671792009140093181/20590092537991656100447826007235479935337788738551822386778675777*y^2 - 381209338340924160865105920859296686664251774923932037682495621926/20590092537991656100447826007235479935337788738551822386778675777*y - 44626268615949867691725851213507187619049664034413681502989727249/20590092537991656100447826007235479935337788738551822386778675777

151202562194375565362422961440543548864595526100723918719803974566/185310832841924904904030434065119319418040098646966401481008081993*y^28 - 91495824510235825144931758832111009629054170397476666586390902860/185310832841924904904030434065119319418040098646966401481008081993*y^27 - 1998862085704874955128208036757072748177301906632249869999575692648/61770277613974968301343478021706439806013366215655467160336027331*y^26 + 26868927081466563968393180834852249783686811104272296147738445065267/185310832841924904904030434065119319418040098646966401481008081993*y^25 + 20194795889004295460392040948507888218545068924909158320275572543504/185310832841924904904030434065119319418040098646966401481008081993*y^24 - 79487391088944172332769007652596077071248471234067084322926316926290/61770277613974968301343478021706439806013366215655467160336027331*y^23 + 199376251632665115177771035133910539794647685242815497792930793067915/185310832841924904904030434065119319418040098646966401481008081993*y^22 + 994323509986962610000487634896288647143458567987306799679215887126186/185310832841924904904030434065119319418040098646966401481008081993*y^21 + 958067141504682943913835933201685638577967094698684036010519039769153/185310832841924904904030434065119319418040098646966401481008081993*y^20 - 363211217434037290826208714664094170051461461126496487448152591447848/20590092537991656100447826007235479935337788738551822386778675777*y^19 - 2135448077077258944607201703316172639367018310096545453569548962673535/61770277613974968301343478021706439806013366215655467160336027331*y^18 + 3456940804215769563215028518314374431645412114895408315486408212653842/185310832841924904904030434065119319418040098646966401481008081993*y^17 + 4729661301954682317459427738002156908711582264035269915355920622204375/61770277613974968301343478021706439806013366215655467160336027331*y^16 + 3993758362921958316561524976518001964721100114846291983239442656079146/185310832841924904904030434065119319418040098646966401481008081993*y^15 - 19674932908701925216675573414963295387042295428664944026210257691120928/185310832841924904904030434065119319418040098646966401481008081993*y^14 - 12953846961275840341074934221182394034697897254383838497743634764294029/185310832841924904904030434065119319418040098646966401481008081993*y^13 + 2185212814887511907414181788476785909537222872209340656273650461243567/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 14548651602199829039607982672468761806047066383917229698538702615071662/185310832841924904904030434065119319418040098646966401481008081993*y^11 - 1463872355971488625880748901477800161969211176917766869783035881178796/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 10054737592611978892349012066711487360030731459856416567478895153285982/185310832841924904904030434065119319418040098646966401481008081993*y^9 + 5080923475642094363443680875415452827841126643789446069024405136080929/185310832841924904904030434065119319418040098646966401481008081993*y^8 + 4506629938256578729199967542059715070536776124230724231268959865417629/185310832841924904904030434065119319418040098646966401481008081993*y^7 - 841193065510628109745481745932204714798879347522076667126014008160776/185310832841924904904030434065119319418040098646966401481008081993*y^6 - 373083988999071777374072383628309919877444030427391635262932451739415/61770277613974968301343478021706439806013366215655467160336027331*y^5 - 2507095510839515688354036667682711552069289166269646972475301389852/20590092537991656100447826007235479935337788738551822386778675777*y^4 + 745026498353496500162354164785956396990345644506252803782421877575/1227224058555794072212122079901452446477086746006400009808000543*y^3 + 14169438006182238774631442781156971785691165433140299005402156590869/185310832841924904904030434065119319418040098646966401481008081993*y^2 - 314630774736086139408009603607810167318438153673130174275615163443/20590092537991656100447826007235479935337788738551822386778675777*y - 588410264702238507412935177629097079209588571558948831573212746108/185310832841924904904030434065119319418040098646966401481008081993

98254940258464628155791181608985079243141626194037381280698367316/20590092537991656100447826007235479935337788738551822386778675777*y^28 - 120355810122434364688045666866076463811655122359742505014494717573/20590092537991656100447826007235479935337788738551822386778675777*y^27 - 3826106317784034729912843701095001885082642421899343098639208798694/20590092537991656100447826007235479935337788738551822386778675777*y^26 + 19828261554233776252268178968589748229245923491147328036566930520179/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 989808715390160765744721184274731419010633821623121318255469445287/20590092537991656100447826007235479935337788738551822386778675777*y^24 - 156056659572281992390158474101141312346413824034625142852873185554135/20590092537991656100447826007235479935337788738551822386778675777*y^23 + 224938333733975889519782827128396056511512727592188004360079276909227/20590092537991656100447826007235479935337788738551822386778675777*y^22 + 511574214164187742398772619751910159670920485054210742666512469803154/20590092537991656100447826007235479935337788738551822386778675777*y^21 + 307716626433570037434996772666698594014048138973798005186313202910952/20590092537991656100447826007235479935337788738551822386778675777*y^20 - 2341710213103671061103843471563256047935964354219482846644688373867184/20590092537991656100447826007235479935337788738551822386778675777*y^19 - 2773691535284885087069676750693385159317355246013971498216817265997672/20590092537991656100447826007235479935337788738551822386778675777*y^18 + 3979060971319386758947556473336674283563664368213327509443218514288062/20590092537991656100447826007235479935337788738551822386778675777*y^17 + 6987449784087287043540035110834505028636699192605644467091592922056824/20590092537991656100447826007235479935337788738551822386778675777*y^16 - 1529376397218153673409336220840108961330328515183808683560590044267867/20590092537991656100447826007235479935337788738551822386778675777*y^15 - 12064581138082393200299971351186268969387459446510107409165578265618152/20590092537991656100447826007235479935337788738551822386778675777*y^14 - 1484670273901102171742658596825816316163493256581013762140476716081117/20590092537991656100447826007235479935337788738551822386778675777*y^13 + 13645152149161093897328386067943806501580969695761469574708269148731518/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 1634314667583032088937860843297088068440750851163841327092969132353597/20590092537991656100447826007235479935337788738551822386778675777*y^11 - 9280086099609962058218884159875928952037620575019549204828950331378045/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 1202263338719514517293692209964610853154974984772779403841586747339670/20590092537991656100447826007235479935337788738551822386778675777*y^9 + 3646297384330277267694908324716242125462193042554354022233273470660548/20590092537991656100447826007235479935337788738551822386778675777*y^8 + 817103626021275688682773027174317483077822715551940082960547216267052/20590092537991656100447826007235479935337788738551822386778675777*y^7 - 737997006935423417595812117940626057538712064757092253835254765388220/20590092537991656100447826007235479935337788738551822386778675777*y^6 - 277993292230247110756970531967650057258713861954169442708621422778876/20590092537991656100447826007235479935337788738551822386778675777*y^5 + 46938091189459629742769899338212227914270105270242551335732906293453/20590092537991656100447826007235479935337788738551822386778675777*y^4 + 204854373655801647946588967675553908841143484813016817022284019262/136358228728421563579124675544605827386342971778488889978666727*y^3 + 2186120958279604477297937600733213730219648497230220158569792440457/20590092537991656100447826007235479935337788738551822386778675777*y^2 - 764765694237178303373858551655980218868737405215321984208277049912/20590092537991656100447826007235479935337788738551822386778675777*y - 108923696858749146539020747222561637339230185583023842317706705345/20590092537991656100447826007235479935337788738551822386778675777

-2010259276279141023668183113078630355410485251400430399026812480434/1008914534361591148921943474354538516831551648189039296952155113073*y^28 + 2081970215765868871719535637504748709922795069781671109455026227747/1008914534361591148921943474354538516831551648189039296952155113073*y^27 + 78696063864830835571874541532530819260123598802777705275303585769221/1008914534361591148921943474354538516831551648189039296952155113073*y^26 - 55864657998736479709403228795594373726394471139184255343464704969708/144130647765941592703134782050648359547364521169862756707450730439*y^25 - 94852240475725775234559578028715681680651721037585896358990762078618/1008914534361591148921943474354538516831551648189039296952155113073*y^24 + 3188535681503771052304682888850109386645849829549640376881448954699503/1008914534361591148921943474354538516831551648189039296952155113073*y^23 - 4044980759686622312573072900739164212599644496962874125834218386455097/1008914534361591148921943474354538516831551648189039296952155113073*y^22 - 11273474796009187508870020943577103559641658912786736128176286413994772/1008914534361591148921943474354538516831551648189039296952155113073*y^21 - 8026515120884117083236048318042293378218259634506047651755490617020746/1008914534361591148921943474354538516831551648189039296952155113073*y^20 + 46024665699405250866126944626370432569939912421440392354303441631994538/1008914534361591148921943474354538516831551648189039296952155113073*y^19 + 64373923422160599499646506987656782618246129331414738263339385802459402/1008914534361591148921943474354538516831551648189039296952155113073*y^18 - 71041148707037346050524203673129975026933573211526073815287366385390617/1008914534361591148921943474354538516831551648189039296952155113073*y^17 - 152265028543956195631036594485956010619171366344277908968032935567220916/1008914534361591148921943474354538516831551648189039296952155113073*y^16 + 10420069355529737832570827242053360395085773570819485292730396866938508/1008914534361591148921943474354538516831551648189039296952155113073*y^15 + 245038638864849215187796266256301231037941549579222148831570827612406585/1008914534361591148921943474354538516831551648189039296952155113073*y^14 + 62476935474139607301780537166465012485093352946442597963514824141191107/1008914534361591148921943474354538516831551648189039296952155113073*y^13 - 272451423464425924216737385603153713017959575729167816263645992954578869/1008914534361591148921943474354538516831551648189039296952155113073*y^12 - 9270754591139632548998770115622259292625644906750155389815514580479367/144130647765941592703134782050648359547364521169862756707450730439*y^11 + 186991260814839238074446358313148573260981127380031978569773619622514598/1008914534361591148921943474354538516831551648189039296952155113073*y^10 + 40688959953141857448564281479919651255802782658779043716320249242044327/1008914534361591148921943474354538516831551648189039296952155113073*y^9 - 72952239607211971379968236472258056168542026210317414532357406377588357/1008914534361591148921943474354538516831551648189039296952155113073*y^8 - 20720586855815940924871974914038305758022003430266606726202839634256145/1008914534361591148921943474354538516831551648189039296952155113073*y^7 + 14210091761995280004412558732942323774640320334864868094201157397348802/1008914534361591148921943474354538516831551648189039296952155113073*y^6 + 6135395235441987041973661051508639084318467643766156717718069839839534/1008914534361591148921943474354538516831551648189039296952155113073*y^5 - 855783644794176743305471623230216277431965152528312931897835964182768/1008914534361591148921943474354538516831551648189039296952155113073*y^4 - 4310946658900483190135573863405534164498521628760718366496894500941/6681553207692656615377109101685685541930805617145955608954669623*y^3 - 48803612775007739575226677700253020832348478995706527429533530807384/1008914534361591148921943474354538516831551648189039296952155113073*y^2 + 2250306309947224265889949549323774920591349513416922106569242543045/144130647765941592703134782050648359547364521169862756707450730439*y + 3396300217615023762363485554915772009219283509973931889792571814074/1008914534361591148921943474354538516831551648189039296952155113073

-344095714640415147048971610254840301553472528439270572687359059108/144130647765941592703134782050648359547364521169862756707450730439*y^28 + 400960366119000617045666556965040049014207531238354100290405912189/144130647765941592703134782050648359547364521169862756707450730439*y^27 + 13427097038080467349746354824158452323850433482572038587526462672471/144130647765941592703134782050648359547364521169862756707450730439*y^26 - 9809158359162958139945972293528584772689285457791114127768521747784/20590092537991656100447826007235479935337788738551822386778675777*y^25 - 7689135051641481135069722982022053117209605024273052461565152748244/144130647765941592703134782050648359547364521169862756707450730439*y^24 + 547636117333001482141032385110025716718607561657553154624391979789521/144130647765941592703134782050648359547364521169862756707450730439*y^23 - 759204989696334649578987163544696448268134975451234843137680895197138/144130647765941592703134782050648359547364521169862756707450730439*y^22 - 1842658311175919378566331444497914303987523368517131497638138978221917/144130647765941592703134782050648359547364521169862756707450730439*y^21 - 1148361713870525541585352107643568608010731647693756477262853866564589/144130647765941592703134782050648359547364521169862756707450730439*y^20 + 8104083942360592994102725678618291313444038438552423428526762041852812/144130647765941592703134782050648359547364521169862756707450730439*y^19 + 10121489584114321031733469211176097963438226017734257641719551749038749/144130647765941592703134782050648359547364521169862756707450730439*y^18 - 13510910831682031738168203892835868018622782314968146731062464489121938/144130647765941592703134782050648359547364521169862756707450730439*y^17 - 24953020920660758833674166764999719275856063812952207946135149791043192/144130647765941592703134782050648359547364521169862756707450730439*y^16 + 4527151617374208634256075948592522205496480415452848650332365860305835/144130647765941592703134782050648359547364521169862756707450730439*y^15 + 42196986923215500680686651636462072244222975847767639454046717238535516/144130647765941592703134782050648359547364521169862756707450730439*y^14 + 6579388327115028612276553033647722812381408701395081811408470674238045/144130647765941592703134782050648359547364521169862756707450730439*y^13 - 47791244542270520330998345237109085588333215583822253610950828063176903/144130647765941592703134782050648359547364521169862756707450730439*y^12 - 976588429721198798259604094143863722737291851334856312751041624075724/20590092537991656100447826007235479935337788738551822386778675777*y^11 + 32750758830260533234237540287836524015067105143470010902272341167730744/144130647765941592703134782050648359547364521169862756707450730439*y^10 + 4423685795560569443112334525056034784917495218890513963216543893452566/144130647765941592703134782050648359547364521169862756707450730439*y^9 - 12812010314517695692802770258205952835559957998267984460527386012393762/144130647765941592703134782050648359547364521169862756707450730439*y^8 - 2738924004842545913432055287514391545889222206585898436015000453419136/144130647765941592703134782050648359547364521169862756707450730439*y^7 + 2560715255330428394564400592424993482424914631106907269543333091069505/144130647765941592703134782050648359547364521169862756707450730439*y^6 + 906783113376140762390647671784329861313109003532089584108033928444064/144130647765941592703134782050648359547364521169862756707450730439*y^5 - 172617782041065584651731143579366234115940835256451274520585280153409/144130647765941592703134782050648359547364521169862756707450730439*y^4 - 629760338087568198758199254178997896048261702636882249262635433278/954507601098950945053872728812240791704400802449422229850667089*y^3 - 4534729595636404660623275218319631432257848014158814147604969800609/144130647765941592703134782050648359547364521169862756707450730439*y^2 + 310994331942499895857539093950483662470266247883357101590116972791/20590092537991656100447826007235479935337788738551822386778675777*y + 215861036598586338659361429401917902833251390759504303562267917637/144130647765941592703134782050648359547364521169862756707450730439

-126857057021796515990506110982056213865446874699804792250972351572/20590092537991656100447826007235479935337788738551822386778675777*y^28 + 169194876929579835900084856652863804487087854664891945419135391081/20590092537991656100447826007235479935337788738551822386778675777*y^27 + 4919914028026171741052622532754606868287448952411385824199919310703/20590092537991656100447826007235479935337788738551822386778675777*y^26 - 26134712300085262951377311773025137946191340918867195785589480311785/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 1627632106548042587196462795237365275538076970702424744959482459878/20590092537991656100447826007235479935337788738551822386778675777*y^24 + 201030613302865153491588318343742662008877940396779193064015404782963/20590092537991656100447826007235479935337788738551822386778675777*y^23 - 312496386973406558289378227058648005882627289681280683738620820411594/20590092537991656100447826007235479935337788738551822386778675777*y^22 - 624057168068142624074827286771730395093439392523581659257928051352396/20590092537991656100447826007235479935337788738551822386778675777*y^21 - 331514062895237242753707700260747417050795293605939880104842475186923/20590092537991656100447826007235479935337788738551822386778675777*y^20 + 3049496885286998804572675480227176676106575220421405944255382535917796/20590092537991656100447826007235479935337788738551822386778675777*y^19 + 3239420333046343953485109947995370440602056695860884906013812471105393/20590092537991656100447826007235479935337788738551822386778675777*y^18 - 5458578890246769622921834018425824651384527814234393932976279328033966/20590092537991656100447826007235479935337788738551822386778675777*y^17 - 8364472950946956635307986707026479339140778443244802977178061586904432/20590092537991656100447826007235479935337788738551822386778675777*y^16 + 2852888835524974604402718535379269041536382483674196583582786269016495/20590092537991656100447826007235479935337788738551822386778675777*y^15 + 15136951972516632145513170915272353952745103844837043156525343724634488/20590092537991656100447826007235479935337788738551822386778675777*y^14 + 234612130086092813226210750625135918954781727685025333891656799760710/20590092537991656100447826007235479935337788738551822386778675777*y^13 - 17468264259308596611381619280868020956519793987742310792921988486586145/20590092537991656100447826007235479935337788738551822386778675777*y^12 - 103881405791435827176360330022717168693848359263733191257483037915442/20590092537991656100447826007235479935337788738551822386778675777*y^11 + 11811842054023560412124977622866179353620024307211441680129397030013756/20590092537991656100447826007235479935337788738551822386778675777*y^10 + 164748552607298753369624547395975235341319437373909034114671940346856/20590092537991656100447826007235479935337788738551822386778675777*y^9 - 4603385505972626631043631658219692483276399761664318824996518214417613/20590092537991656100447826007235479935337788738551822386778675777*y^8 - 497306095402722038230828834568591280306442847375628555428278492893495/20590092537991656100447826007235479935337788738551822386778675777*y^7 + 962785497588718746959262297888252796813513947234738974334151636710336/20590092537991656100447826007235479935337788738551822386778675777*y^6 + 233430805096654940586810135469518405686714838212217041103752592996893/20590092537991656100447826007235479935337788738551822386778675777*y^5 - 79333967558923294434375564334630039601543333113463783469839104756510/20590092537991656100447826007235479935337788738551822386778675777*y^4 - 176307327458759335692460477366175614599476085383140051021453999376/136358228728421563579124675544605827386342971778488889978666727*y^3 + 5801587151883406750969721078499181825056693671032247346376318234/20590092537991656100447826007235479935337788738551822386778675777*y^2 + 544212751994809851500735409424709442254703201936867225141952380524/20590092537991656100447826007235479935337788738551822386778675777*y + 37079151106060816835795035722740002122067835904678712887486855248/20590092537991656100447826007235479935337788738551822386778675777

52130652818613366268380682621422107909640704777767109751607037766/20590092537991656100447826007235479935337788738551822386778675777*y^28 - 56895229351819442421934872062878078032563224927036102341807548759/20590092537991656100447826007235479935337788738551822386778675777*y^27 - 2039414712761398310288299690018866934733734067867987500032685169839/20590092537991656100447826007235479935337788738551822386778675777*y^26 + 10250319819124841268552274122626722381614430283545666701928456569538/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 1964562141074062802242087524352241630383911272458102523271453702757/20590092537991656100447826007235479935337788738551822386778675777*y^24 - 82912326674691510713018722449060048324765402854408632812511359119055/20590092537991656100447826007235479935337788738551822386778675777*y^23 + 108299503667966242765465498280429416811249038894737676860383928400167/20590092537991656100447826007235479935337788738551822386778675777*y^22 + 288791605628100125884217680642812132140696659401359876289494045497713/20590092537991656100447826007235479935337788738551822386778675777*y^21 + 197300443389498177734498556802725205352034587349931969679474357898910/20590092537991656100447826007235479935337788738551822386778675777*y^20 - 1225135728054908452761256002934803710275505432218983945402097090474088/20590092537991656100447826007235479935337788738551822386778675777*y^19 - 1639594020806212980495694824312789534332338917706610237488418972903997/20590092537991656100447826007235479935337788738551822386778675777*y^18 + 1936980887969176967493760299258347534416250929919039409613518564967045/20590092537991656100447826007235479935337788738551822386778675777*y^17 + 4012542590475315605285818824785500846075987685278269793063388516037646/20590092537991656100447826007235479935337788738551822386778675777*y^16 - 357462009367344864667300624492673870532686641227164453085194734092152/20590092537991656100447826007235479935337788738551822386778675777*y^15 - 6573131080564808409624417182070296925288413699080751797792210993960814/20590092537991656100447826007235479935337788738551822386778675777*y^14 - 1620948109659087794373091220483734525776197215760897678430926387092707/20590092537991656100447826007235479935337788738551822386778675777*y^13 + 7249963371782199915556234420851826485180086433264585372099453067633784/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 1839840462496162728859699896452921716040571816517897782253880518452074/20590092537991656100447826007235479935337788738551822386778675777*y^11 - 4940310555280296688283368029036475697751778344410460741613002988674060/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 1304354953020586007506258319514263768423752884101508125246213206209902/20590092537991656100447826007235479935337788738551822386778675777*y^9 + 1940339388616388304486890461253591792572901965098634115103249832074573/20590092537991656100447826007235479935337788738551822386778675777*y^8 + 700143620393763819031485005602773547977561851306580421740201807895205/20590092537991656100447826007235479935337788738551822386778675777*y^7 - 369966103765467520201577587526315173777660769698925466312499935983078/20590092537991656100447826007235479935337788738551822386778675777*y^6 - 206652620746716061954707708327096091837822871443500346622903087744816/20590092537991656100447826007235479935337788738551822386778675777*y^5 + 12531693471759962636111063124375499771340837498530829182867502197487/20590092537991656100447826007235479935337788738551822386778675777*y^4 + 145807662264717090367048147564262004633807415821099374328351541022/136358228728421563579124675544605827386342971778488889978666727*y^3 + 2918851813855130876014639580006509616623079463840916506201885345198/20590092537991656100447826007235479935337788738551822386778675777*y^2 - 458623773612418375182703544637477261857235094651435505981631789039/20590092537991656100447826007235479935337788738551822386778675777*y - 90190184486939277814430668757544778144869692627429652574680593542/20590092537991656100447826007235479935337788738551822386778675777

52130652818613366268380682621422107909640704777767109751607037766/20590092537991656100447826007235479935337788738551822386778675777*y^28 - 56895229351819442421934872062878078032563224927036102341807548759/20590092537991656100447826007235479935337788738551822386778675777*y^27 - 2039414712761398310288299690018866934733734067867987500032685169839/20590092537991656100447826007235479935337788738551822386778675777*y^26 + 10250319819124841268552274122626722381614430283545666701928456569538/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 1964562141074062802242087524352241630383911272458102523271453702757/20590092537991656100447826007235479935337788738551822386778675777*y^24 - 82912326674691510713018722449060048324765402854408632812511359119055/20590092537991656100447826007235479935337788738551822386778675777*y^23 + 108299503667966242765465498280429416811249038894737676860383928400167/20590092537991656100447826007235479935337788738551822386778675777*y^22 + 288791605628100125884217680642812132140696659401359876289494045497713/20590092537991656100447826007235479935337788738551822386778675777*y^21 + 197300443389498177734498556802725205352034587349931969679474357898910/20590092537991656100447826007235479935337788738551822386778675777*y^20 - 1225135728054908452761256002934803710275505432218983945402097090474088/20590092537991656100447826007235479935337788738551822386778675777*y^19 - 1639594020806212980495694824312789534332338917706610237488418972903997/20590092537991656100447826007235479935337788738551822386778675777*y^18 + 1936980887969176967493760299258347534416250929919039409613518564967045/20590092537991656100447826007235479935337788738551822386778675777*y^17 + 4012542590475315605285818824785500846075987685278269793063388516037646/20590092537991656100447826007235479935337788738551822386778675777*y^16 - 357462009367344864667300624492673870532686641227164453085194734092152/20590092537991656100447826007235479935337788738551822386778675777*y^15 - 6573131080564808409624417182070296925288413699080751797792210993960814/20590092537991656100447826007235479935337788738551822386778675777*y^14 - 1620948109659087794373091220483734525776197215760897678430926387092707/20590092537991656100447826007235479935337788738551822386778675777*y^13 + 7249963371782199915556234420851826485180086433264585372099453067633784/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 1839840462496162728859699896452921716040571816517897782253880518452074/20590092537991656100447826007235479935337788738551822386778675777*y^11 - 4940310555280296688283368029036475697751778344410460741613002988674060/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 1304354953020586007506258319514263768423752884101508125246213206209902/20590092537991656100447826007235479935337788738551822386778675777*y^9 + 1940339388616388304486890461253591792572901965098634115103249832074573/20590092537991656100447826007235479935337788738551822386778675777*y^8 + 700143620393763819031485005602773547977561851306580421740201807895205/20590092537991656100447826007235479935337788738551822386778675777*y^7 - 369966103765467520201577587526315173777660769698925466312499935983078/20590092537991656100447826007235479935337788738551822386778675777*y^6 - 206652620746716061954707708327096091837822871443500346622903087744816/20590092537991656100447826007235479935337788738551822386778675777*y^5 + 12531693471759962636111063124375499771340837498530829182867502197487/20590092537991656100447826007235479935337788738551822386778675777*y^4 + 145807662264717090367048147564262004633807415821099374328351541022/136358228728421563579124675544605827386342971778488889978666727*y^3 + 2918851813855130876014639580006509616623079463840916506201885345198/20590092537991656100447826007235479935337788738551822386778675777*y^2 - 458623773612418375182703544637477261857235094651435505981631789039/20590092537991656100447826007235479935337788738551822386778675777*y - 90190184486939277814430668757544778144869692627429652574680593542/20590092537991656100447826007235479935337788738551822386778675777


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

# B Gluing Matrix
{{2,0,2,0,0,0,0,0},{0,1,2,0,0,0,0,0},{0,0,4,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,1},{0,0,0,0,0,0,0,2}}

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

# f Combinatorial flattening
{12, 15, -10, 3, 2, 1, 8, 0}

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

# 1 Loop Invariant
-2326124262806011306689229110207324499810243062166347717386919861777/20590092537991656100447826007235479935337788738551822386778675777*y^28 + 3421284541251360367467747826304524153227564358811311100235994290293/20590092537991656100447826007235479935337788738551822386778675777*y^27 + 89711198710320765356403458145324068916970356262838206290663464143596/20590092537991656100447826007235479935337788738551822386778675777*y^26 - 491479590130258057066248487619664303282995815296851112207229195858688/20590092537991656100447826007235479935337788738551822386778675777*y^25 + 98530021019678232702501574099248154593825640132601831240810466378556/20590092537991656100447826007235479935337788738551822386778675777*y^24 + 3665970638280619320387448787644149324845258417767091377688429878462490/20590092537991656100447826007235479935337788738551822386778675777*y^23 - 6233050649107288945904876005306714817343927054229359707354219579531213/20590092537991656100447826007235479935337788738551822386778675777*y^22 - 10537731038630953727340029113331226401758961563775847189226759592399193/20590092537991656100447826007235479935337788738551822386778675777*y^21 - 4707925424298273927594518567772525970616582520581302855329656629537342/20590092537991656100447826007235479935337788738551822386778675777*y^20 + 56401828315477971462854325296801620183584159302999757162516571510819965/20590092537991656100447826007235479935337788738551822386778675777*y^19 + 51511658978409897631863519892515180195002938166222187085266480567395451/20590092537991656100447826007235479935337788738551822386778675777*y^18 - 106447930360258155664892243202050609500022639388145941754745595016427562/20590092537991656100447826007235479935337788738551822386778675777*y^17 - 137843030859666038816308555201762796023193431120347219579191232982884732/20590092537991656100447826007235479935337788738551822386778675777*y^16 + 70273293572672341268103715597953078620949328231878428395253542274013962/20590092537991656100447826007235479935337788738551822386778675777*y^15 + 265970719221677730833697202897811723831738227415383084574969385701642478/20590092537991656100447826007235479935337788738551822386778675777*y^14 - 32179209128879162383765331523157180303390293142592926444055600682926085/20590092537991656100447826007235479935337788738551822386778675777*y^13 - 312832357585567230913983994176291507454387437936641319296029026389777239/20590092537991656100447826007235479935337788738551822386778675777*y^12 + 41526650386993151074425381975897279961019193554143896309875032542006735/20590092537991656100447826007235479935337788738551822386778675777*y^11 + 207750454718232552631121696699783609885700672711554016077294475095693556/20590092537991656100447826007235479935337788738551822386778675777*y^10 - 25653893005211200939454896647318109837558373223799863750896556250174158/20590092537991656100447826007235479935337788738551822386778675777*y^9 - 79150986545081595861660065888174658415244320370825242597937487673752552/20590092537991656100447826007235479935337788738551822386778675777*y^8 + 1784844519509971033218558064491904955006293836242857161301305520086901/20590092537991656100447826007235479935337788738551822386778675777*y^7 + 16934194442976466010246931820930205533966774931442705688108089898537349/20590092537991656100447826007235479935337788738551822386778675777*y^6 + 1913615647862595655478592495926601152866161578413104376150396799945090/20590092537991656100447826007235479935337788738551822386778675777*y^5 - 1654923477409392523321597479211863193371921760001332508942983083336185/20590092537991656100447826007235479935337788738551822386778675777*y^4 - 1696447005963101984155010842425977470779979433826774954633465404972/136358228728421563579124675544605827386342971778488889978666727*y^3 + 28519555937934118442873454200167739735238661396158677587005178108833/20590092537991656100447826007235479935337788738551822386778675777*y^2 + 7093549559703144227778858682953941211699782884624890482598665456507/20590092537991656100447826007235479935337788738551822386778675777*y + 104754061406100413510743636209843834013321353045989476915996292625/20590092537991656100447826007235479935337788738551822386778675777

# 2 Loop Invariant
-2666491522190174863069095756409862985927927892087519963536922922041115942901348686207090363365192792257377334706175898350698841933679256133626895333718432444033/10109549751054940028522329056889893145921326675060206029589044572867260007422642148877176022177636620918252305299178778999503332302354992952582629752287218618788*y^28 + 13719687401606637266162319250670442570059624921813467254590923769121170059394999101228239076246094658844131113563786695456523812532390202828542981337060958269555/40438199004219760114089316227559572583685306700240824118356178291469040029690568595508704088710546483673009221196715115998013329209419971810330519009148874475152*y^27 + 1243608515448290769613095045187225203939442846773398757903477321948821793172359206487661580974610044785881509652759601869902837299011045131567488413388816187541975/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^26 - 408369710099803529317801302025032401815813249098517044681317902138775419994089460344508117291053362026727149245637107498485291408421745918163059159332635124487473/7582162313291205021391746792667419859440995006295154522191783429650445005566981611657882016633227465688689228974384084249627499226766244714436972314215413964091*y^25 + 74269908199426521813915151018877613044915289422136470064054161530288076250354538212645572420585406056090558035921051133660537483849896292393337286465614781676611/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^24 + 16948702918983230010267391608649120292620202544123676174874742022971373673707129258951792600448831595432649327722086323487882344882914767324619267272118822895499569/40438199004219760114089316227559572583685306700240824118356178291469040029690568595508704088710546483673009221196715115998013329209419971810330519009148874475152*y^23 - 76401551859097827046139605758321301881297286783814686776133235631699712007745375865711397266661539521797808864247346641843924647336833731714793892546636308105819365/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^22 - 162093020819797856651902015148841172160505807208340198020639856594741488023752168244729875751417382293234192714688959284747082213653273090623707889818973760100882961/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^21 - 14965520820751581896734155079250797965737459928208087715261206474291650578198878325126714993034195742866051618119516036710790560757381330509588852327429577032377247/20219099502109880057044658113779786291842653350120412059178089145734520014845284297754352044355273241836504610598357557999006664604709985905165259504574437237576*y^20 + 192096620680065621625024293382403515676817646814431756430131172629093524151007590568261333215898347324436689611805111932596994937962097915259873052928898465194367641/30328649253164820085566987170669679437763980025180618088767133718601780022267926446631528066532909862754756915897536336998509996907064978857747889256861655856364*y^19 + 855937030226826563343716125733411199582149626058115794345461387847598023659234795381810059076994605300929741248455501294673809155307043260316407842708714454425203549/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^18 - 450569410935894392610289175826147594827553260495003542259775272031585667747011422043926369461326102996068448522183394900014543421164491017955215844849845744198338731/40438199004219760114089316227559572583685306700240824118356178291469040029690568595508704088710546483673009221196715115998013329209419971810330519009148874475152*y^17 - 274130476767562914175686132097408198453050980337577518421796135940649575743089080494953130034466686021138369410181223264993391707542152847099040784897500261644361067/15164324626582410042783493585334839718881990012590309044383566859300890011133963223315764033266454931377378457948768168499254998453532489428873944628430827928182*y^16 + 40025730372246670962651541694694920595227785908764640969669772890078529194263916901766042441621923564350368721882966167409256329971118774584050272484770804449424242/7582162313291205021391746792667419859440995006295154522191783429650445005566981611657882016633227465688689228974384084249627499226766244714436972314215413964091*y^15 + 1946928383926815952662863878928358502473362191940906305752526894433581752523522107099410199997485341218794541108281981817138175203859206954253462227859508714761808871/60657298506329640171133974341339358875527960050361236177534267437203560044535852893263056133065819725509513831795072673997019993814129957715495778513723311712728*y^14 + 236369128562313223001243182989160275267006020595259925091681187026928344541142342615401620260007952815425468189779093815181832991533539592497942367399018215221726851/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^13 - 2235501949288480463331811350824505585695624992423982406912558016211041914117520723084421113284434542845572411997754183837184793159279744765783241212099086462931257171/60657298506329640171133974341339358875527960050361236177534267437203560044535852893263056133065819725509513831795072673997019993814129957715495778513723311712728*y^12 - 124092895485836543189315486821408338743835045421194630711356438757740085932069772790997165853870796828669460507192511247789078947973996157648174043293297554689142861/60657298506329640171133974341339358875527960050361236177534267437203560044535852893263056133065819725509513831795072673997019993814129957715495778513723311712728*y^11 + 190776624043584660329740695999799174464658747831779549713943409212370362092258126039922697930726067043821576322148935197130609217988291868147773997032213119827538370/7582162313291205021391746792667419859440995006295154522191783429650445005566981611657882016633227465688689228974384084249627499226766244714436972314215413964091*y^10 + 48471460760009264579591062194814240018388237150842448814162423185243645387704680076116307054469016043213442020454584466591278279999333912213536116061129616617937171/30328649253164820085566987170669679437763980025180618088767133718601780022267926446631528066532909862754756915897536336998509996907064978857747889256861655856364*y^9 - 402633215557308250214660361635413172714502984762362984496722801307212328781086786764079234093866753402429841057450443546887673142713490157297965451691668382469911819/40438199004219760114089316227559572583685306700240824118356178291469040029690568595508704088710546483673009221196715115998013329209419971810330519009148874475152*y^8 - 186671789567652059632496170009327482384121326045319006394836898613182678720781320925811237649754767985625866925636724043630626492308776713781529880932239815596588931/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^7 + 42436505753177148772042566899536449923799159612689342585316576165046039472563062074802401471077400274166440362401757331008099188820072513398837235872982775021011123/20219099502109880057044658113779786291842653350120412059178089145734520014845284297754352044355273241836504610598357557999006664604709985905165259504574437237576*y^6 + 18436884653772319613959595752218443471661320428256961387741129797283516687809550612432260004804439761921457557454307705748135383551768949662201413211054221776230193/30328649253164820085566987170669679437763980025180618088767133718601780022267926446631528066532909862754756915897536336998509996907064978857747889256861655856364*y^5 - 20434866897823904975481883906765742559073594866784686146381228117333137849296050999268951824931123589207882753617381461877567175650636344818197709297264164328593425/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y^4 - 4788658149269245168956470563906466093470088792688323262865148927258656665674399727537569276638341443981020039369327098576244725506871810313617094615478641671897/66950660603012847871008801701257570502790242881193417414496983926273245082269153303822357762765805436544717253636945556288101538426192006308494236770114030588*y^3 - 10040566448877125999012606370238494209336834495172031341084642122098282540317137325936853395253122778503650883658115098235265384770258267089109203553647931737529/20219099502109880057044658113779786291842653350120412059178089145734520014845284297754352044355273241836504610598357557999006664604709985905165259504574437237576*y^2 + 246481405797136777982523951320668944050955285379600680766841713654352504969753837010962306928755221842383426185650309379142117579228926315399163728506358909729969/121314597012659280342267948682678717751055920100722472355068534874407120089071705786526112266131639451019027663590145347994039987628259915430991557027446623425456*y + 160825750174072393949394420467464786258916903719486644877532509545243165550154542273808578837653315171783910834190808528558725037911094959764564206999409535694455/5054774875527470014261164528444946572960663337530103014794522286433630003711321074438588011088818310459126152649589389499751666151177496476291314876143609309394

# 3 Loop Invariant
57220295227267493355169310427650468155806717715979165916748299444768880185029638103843869480221845544692818298030908336934342531400006668668991445136438900127803953015610564792220774595378437712741216487688435/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^28 - 140196252744422065674952497834297125651310735991289489962035575974092409318228396060031917631361851047844851916676430220207332195709100497921059075193312457844456054509956129360546188554256337658724803376111707/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^27 - 4457225644280701782670667082658775860828289000575567246312050094842079584075168583121621560677341007651903726830102810684951166024393880213476711703693082428538197608623334629308884155343180403992653539336025271/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^26 + 721746978531046823412980273254955787884908189620402150434199655875758936542158092979361407581317752205882913707209558329556328489289131660300330901803914358625432573357325550938444860941834324497623483886641123/1770959299262277243817017416451254216224681292880548298571334331216142064408205799437636696996508302598041871141760441400627718417249356705892317523175315018742344353886974263843021875661712118070499329123286*y^25 + 1183452803590254922691908706358765833899511474922658005811902910606131643798899189294916384013700681361208049399388011349852247802295032330491017565290948048332061510507865029001438577088010389867391818828208483/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^24 - 181925688943450576701592814990545128565180109338880181666865600145193258503338631387978020737064896820851871546785195632829116213918342182815715957228705045161803967835812298642158886171201866735047641389135526097/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^23 + 966642984198844400721612902785769512929194481837380864007557875035146792250258202710586027765989697749104380090959452060571668782337271636678112319549786490981876670826355798001171331240468771226146813729512933/209116965226541962369537111905683154683357200635341496510268260512607181037131312110717248353831238683163615780576878689373014720856012599957764430780849005903155052857502496099545018528320250104265603438912*y^22 + 597113281564969140772382711220474423058338440234989639442801578924327189590224648980799192327320862441360057131993287197684738313846969472131073066189191960103661505450526944733614105315390776585636811666099678675/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^21 + 178406820273062787182283363871957146715922682566411154152419851400218805399500516976392974526384031463369093215950567641992944445119953309428716837855113796312835129451346644593206129873014628578009558631036523889/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^20 - 1260221946358259494752787680345283852247713220645069771127171877423887827102854454652691236672476159466500785452230164128567182267130902675945242002621057569881861338442103292113072917133704797550761895696580879/26139620653317745296192138988210394335419650079417687063783532564075897629641414013839656044228904835395451972572109836171626840107001574994720553847606125737894381607187812012443127316040031263033200429864*y^19 - 1617518768595062354517849710245852296459418114292864340685998068597985032559964527710118805439699836491689239826977341487018018057729043708784738128836025943978309918166599774897321989176593853410761929728821616933/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^18 + 2326401500548339193314633231856666164161829090827218747117169857831589784129946005959778557621296333768213157902916239430844806044873553081711272271724680717230474216543948859729729566970749518246997470881235290791/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^17 + 4083617561228622261978586137021217729722016269134156610723222186054543528396560596969433909956431412877589766365332655340940755109626787814513657670399661676906371212081492456262106617837964657574182766814934272541/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^16 - 901120846336810431771044530861790980062789193207183545602859892481305272175071147405736553753370760153601352405672308388669321444954125057739708069613479681706233471528863102116101366329208187622129073481138635071/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^15 - 14113810664013733097384593780698521157714323479781009930435697651272880131900877659953028393384525495450222250961671748258055443042531415343889893740283350547704712062738882725581380425065755169365603182161074732545/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^14 - 870826564166015902915438750822100293577925091867353219617583332164731548066780794155685672909203283226289171104774276771457876717122671333651335134434480060799584118028769556005092094021113552298308984075739009117/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^13 + 7990166208988973497748666129057362654029819270608615751537019516561690687725208304922187072600045535915042652631494219066516291292325647908084576731945326658823879202750493868176257344332241759750018608052020126141/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^12 + 30370196318391320711175434406990983938561772222071949621976665135875176802623721523212045910671371022523215585825970976071809845571133802865090469836469684263388396165748334081015043377539522802198502175240772061/885479649631138621908508708225627108112340646440274149285667165608071032204102899718818348498254151299020935570880220700313859208624678352946158761587657509371172176943487131921510937830856059035249664561643*y^11 - 10892802684570840121962077597344026119336773284965818082667009958461407786114505306569769458429880772031907080796346378608881099296139249963323353847543003321610813369248793769137727521745197891706925679666098337139/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^10 - 718535341428562057218380101363280237280468071683398559773728179198372947071126980714333340711897165312634440123235191155447991317136865265754398157232968331158802012577227214926007205543157055789055436913584659727/28335348788196435901072278663220067459594900686088772777141349299458273030531292791002187151944132841568669938268167062410043494675989707294277080370805040299877509662191588221488350010587393889127989265972576*y^9 + 268470558224508961364739945727918950042335868689474830439950474581712090471598891442816939348379597918932394920023800814039793660757338242433146796229158903130564379409551161128543507119006345365704263608425434765/3541918598524554487634034832902508432449362585761096597142668662432284128816411598875273393993016605196083742283520882801255436834498713411784635046350630037484688707773948527686043751323424236140998658246572*y^8 + 30449018194203583163007363032113447052121993669198478451447091446727100953547512665706006601464802463224155916781518215879981082178828153673813927246952655857489945832998815038998051075558546105531826474312632243/1770959299262277243817017416451254216224681292880548298571334331216142064408205799437636696996508302598041871141760441400627718417249356705892317523175315018742344353886974263843021875661712118070499329123286*y^7 - 873623373329123434007159265091130953889699069116148407217291994296980122146324451731807252703981916408534295831815632194213526181948627049399708087807755269957024820345878807097089907300823468666355268966372160691/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^6 - 83084139543762214271133538672693504968146012885392814314253963176811453288288813510426145968638397658617775595293368715058273703982721697872998905188414919360251395470225240326644782726616041890056531810716903523/14167674394098217950536139331610033729797450343044386388570674649729136515265646395501093575972066420784334969134083531205021747337994853647138540185402520149938754831095794110744175005293696944563994632986288*y^5 + 6976675140134230557934446409264949950498703510195605009721648305709630768921421087111489133703365085965497118592353522425091444843366733426699674648634510003249881145100924882323723746785383027202370599219175103/7083837197049108975268069665805016864898725171522193194285337324864568257632823197750546787986033210392167484567041765602510873668997426823569270092701260074969377415547897055372087502646848472281997316493144*y^4 + 246450624391791212872652853387582312656329080262056342839994072485837178827332361578157547141721103026487531496149322773654802311942777113825627230172523111240784668934215698349776488346828428324099983738464507/375302632956244184120162631300928045822449015709785069895911911251102954046772089947048836449591163464485694546598239237219119134781320626414265965176225699336125955790617062536269536564071442240105818092352*y^3 + 2599813007421944601565387105161083576973847121276114946440286218098533093981951911255612663082232534877599973269616254515616930188475702976347221474181063546725971634193437847795733918038799191242309454875688311/56670697576392871802144557326440134919189801372177545554282698598916546061062585582004374303888265683137339876536334124820086989351979414588554160741610080599755019324383176442976700021174787778255978531945152*y^2 - 115920895616141821028318595782864485338140193351327591696330227115349284009761177973259159041244659709673860708644783787554338612190814495040960360493309820488334629485540374340529026847446173268089445255091705/7083837197049108975268069665805016864898725171522193194285337324864568257632823197750546787986033210392167484567041765602510873668997426823569270092701260074969377415547897055372087502646848472281997316493144*y - 36574242457177824935802681429796254550334546817910892319230846190152786274889870436585025964447427495241479652108548786947787610978270497609222967272116675874981297733358533456063026353731749308525862824187977/14167674394098217950536139331610033729797450343044386388570674649729136515265646395501093575972066420784334969134083531205021747337994853647138540185402520149938754831095794110744175005293696944563994632986288

# 4 Loop Invariant
5299895726266175638955896127617750972702880505116236472107719360738487240366887137760713513181680991855391910008552237494664353422223153965972851216377583156893022573035135841924961378099460079409719297509995387440889887503902454327204325221059708644219104340629828463629297347692261944014249936265113723053/556496028872548350948142351079657971274989370498805214271323689106586410440351692739806203830778333838849752992152008635924428713016128407949368765636468637331446384321480023523507669377731422214826999527091036802864196683582516504447315136455159196970129680067710063200096220509289921736363191775671925760*y^28 - 972130322559474979914483678560028651392016265417086970137844847157424211661373150544202675733268298781502146747614359909410289592328801716842374827896223629600059651580533926631840984576507828041149239136831475073179088227282632396362731904334503188987182459354893588440905173325550572915680736123922329677/83474404330882252642221352661948695691248405574820782140698553365987961566052753910970930574616750075827462948822801295388664306952419261192405314845470295599716957648222003528526150406659713332224049929063655520429629502537377475667097270468273879545519452010156509480014433076393488260454478766350788864*y^27 - 1857901036072811871829732724794208519638623826761156781951414954727342252512480193979713441687232783623561932577227809933385203470255334695009858425572304911293386065685680060610072004126565061720108552542609809961214027003797561481640446239428826647679393130625771438219354940466555406577841669571555437763509/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^26 + 200464310397920902372344236283397257008048326543866291370070690899667220120720236355276619288900500967070521702983443210616619300422243973378637128114202382002191601712737745421576770997033226164863182996427167813691513198371457775755608550033086926935861467411696527047125725774259040405393403024700616230389/104343005413602815802776690827435869614060506968525977675873191707484951957565942388713663218270937594784328686028501619235830383690524076490506643556837869499646197060277504410657688008324641665280062411329569400537036878171721844583871588085342349431899315012695636850018041345491860325568098457938486080*y^25 + 85721235695867106218606700347660969772740627864627535934411787413554231197658262598759312334425286119831627081629500489087899909670717033980188854919661260560014002778327604883251040569955513651036342606869847466787944870645238521141825072664003372048471399490812041505130274871852479594965649115739936958849/834744043308822526422213526619486956912484055748207821406985533659879615660527539109709305746167500758274629488228012953886643069524192611924053148454702955997169576482220035285261504066597133322240499290636555204296295025373774756670972704682738795455194520101565094800144330763934882604544787663507888640*y^24 - 15164944241822035799977138961851503052961146754836172792295187560914547598270200076755774742525697109538581220791584794164838523310975889491251083820329065018158551613791152089048786497994302734612101020977896883868615793496319582253871187491053036109915148795248280140353094074663234490204009654449206050131497/1001692851970587031706656231943384348294980866897849385688382640391855538792633046931651166895401000909929555385873615544663971683429031134308863778145643547196603491778664042342313804879916559986688599148763866245155554030448529708005167245619286554546233424121878113760173196916721859125453745196209466368*y^23 + 27255041424152482157190690508530401411858272353853321127326534206859025092690632992536869648057635966725589052392818780043542051653792417321493979085774123844283743790968362876119630443970257751251082480818981117726323399805027696311299531290718598632772453653377625561323768165435206309534855322723562608565641/1252116064963233789633320289929230435368726083622311732110478300489819423490791308664563958619251251137411944232342019430829964604286288917886079722682054433995754364723330052927892256099895699983360748935954832806444442538060662135006459057024108193182791780152347642200216496145902323906817181495261832960*y^22 + 249108140642179324978888425809916157713759747248625887308308942392558574243100922655682482352467499443104757042339398536838074982415421508039529730030171788620743335202390123021029304851006693805039887698847541820609765481587642846524342865180350800214705979224122949850254886094027793993012297461295469027049599/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^21 + 29853675091578849620159561585190211120755971307828712672885603839104073899633810954900636806216993274442725608833860956784306150397569287542345473024317814197134055108532951678631100145028911703834742550753952865069950146822527641686694928401146710418968936544595391153548651392206724533948446058419837647119079/1001692851970587031706656231943384348294980866897849385688382640391855538792633046931651166895401000909929555385873615544663971683429031134308863778145643547196603491778664042342313804879916559986688599148763866245155554030448529708005167245619286554546233424121878113760173196916721859125453745196209466368*y^20 - 1138361848934397408814027553634000444775602885211781139104970632245100135469386230880906888834013085601732028338461634309229548362001836354330249625244881307613401025007760493857335565144408533460208889965114405345202462533234492306793577140439163160713637188825188759820499873125728065297116005499921000339189771/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^19 - 150085393514625503681547502136207079876461085639191160792167234761905200764798720185009179700905445472776652736862802665706119858319408986635869211611166731306098176038759097759693328958233404749279122427131831796409533119856748848879469301589013972543125697179029608520130488467295131499132183242221856556938139/556496028872548350948142351079657971274989370498805214271323689106586410440351692739806203830778333838849752992152008635924428713016128407949368765636468637331446384321480023523507669377731422214826999527091036802864196683582516504447315136455159196970129680067710063200096220509289921736363191775671925760*y^18 + 968101029064268169446480213006398897077403628796382468406202550596513599460302700735583869000429040371273660383899456079439502726548330548528534930837069657779569761530430409041493666246223269307229765219946611112182150691732809253713994606832121238763783351213159236223385352724150546054286361349293713179561997/2504232129926467579266640579858460870737452167244623464220956600979638846981582617329127917238502502274823888464684038861659929208572577835772159445364108867991508729446660105855784512199791399966721497871909665612888885076121324270012918114048216386365583560304695284400432992291804647813634362990523665920*y^17 + 3407818343966447042621608773059081466153506453258026171147326827478586784601492295626600780025426960007984977591312078728792810347932487628402044676363566586528206570410591408146544400427006890489944662764478362147917037794038236307027148819212286872543475514006179167686423773305104630630750069078499303534988867/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^16 - 92991303835473632240096258472490012126925783953815438390250498450902452897053559458266890768642623602161013789064444078131530674981064005949195217942159560786905691300767734229498042585734659008162865507520160449470800982162448943678252556223826624934109815020451007074151086766512995892440786674578117679632143/626058032481616894816660144964615217684363041811155866055239150244909711745395654332281979309625625568705972116171009715414982302143144458943039861341027216997877182361665026463946128049947849991680374467977416403222221269030331067503229528512054096591395890076173821100108248072951161953408590747630916480*y^15 - 1961137241153291306701093978165913817866745367412380390657907261986529478235090478044604933315133174728892032887854593668583353716446648517956739299850766932347003413385737697089322966462864566693912696579019940077713627420142026859259567375890979652880636744593152447787756518099272560899591177940857364197253819/1669488086617645052844427053238973913824968111496415642813971067319759231321055078219418611492335001516549258976456025907773286139048385223848106296909405911994339152964440070570523008133194266644480998581273110408592590050747549513341945409365477590910389040203130189600288661527869765209089575327015777280*y^14 - 24594186504917567550253269816635376840829070762145004045544802981725849210359077821427025389257340065999465260778254128917686482932870166487681417270571828776378366319151214823973259407542517416914096007462270194805959871537525002391247733078346541264665449092432135853250475426794829596423356098415099660970705/166948808661764505284442705323897391382496811149641564281397106731975923132105507821941861149233500151654925897645602590777328613904838522384810629690940591199433915296444007057052300813319426664448099858127311040859259005074754951334194540936547759091038904020313018960028866152786976520908957532701577728*y^13 + 3329227233553456535496955635040139372661720188090642421020068351384746867250711461805444159344605184056544624426428220906008800194338422619099315009819863627394522455400329717537475468884778607797825757429061748688451597879601632202433157439253472720909821602459231122647283946935460119037700739671556025140603471/2504232129926467579266640579858460870737452167244623464220956600979638846981582617329127917238502502274823888464684038861659929208572577835772159445364108867991508729446660105855784512199791399966721497871909665612888885076121324270012918114048216386365583560304695284400432992291804647813634362990523665920*y^12 + 823141370255006037064082660221571018694665244867295091945006273143967780886809136123250205101024041570066671859893568922364393219128316387419747439715100195617001530920417437801841712756779432945445487126741883933595409177199271182575584912174787747791557489566639008466622788965879896214069475418947317381814513/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^11 - 4538220601118310712984603563736154536497777040822714192997622396192047220335764305099214439094609574853202480984037058014791830936355683824612158614148930686647812030890928785210021376098381144006375279565170226007401160986173051114454525438793038859516548677820932028688102967244678679356836956299396710381413283/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^10 - 6749093141312535631648606573142395068196066613173189812287003311901394000257771631453900578464296901690754032965186894458673801623205174597453181426606049307544531024842972643101350858622796729686522964990631774738722121573203657430222822601274728396239945494625000113218066377860764208717506790455845131636297/55649602887254835094814235107965797127498937049880521427132368910658641044035169273980620383077833383884975299215200863592442871301612840794936876563646863733144638432148002352350766937773142221482699952709103680286419668358251650444731513645515919697012968006771006320009622050928992173636319177567192576*y^9 + 27956012961788161342951152968103715750438788876492152535725203957235782916236941112942497676464552596983327389043961388652889723827911110438342723193270699668223060131692497675677678824774890659048057525334494892117098610496030865618583444192494520671181518879824171259473956466635561280227698585964783468857203/78257254060202111852082518120576902210545380226394483256904893780613713968174456791535247413703203196088246514521376214426872787767893057367879982667628402124734647795208128307993266006243481248960046808497177050402777658628791383437903691064006762073924486259521727637513531009118895244176073843453864560*y^8 + 409200796564585013440577955356883535018129564876259656032051393845912161186661527712916740507137653983481861326928453055312063480269802614568805005275103230188047836545722078300277127203039154253529358850387691169742058018383685187729790077210107515045953783225527895210522162269442572594500674204421123945264589/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^7 - 363445909983809663200319459387908862623130100928238500915721497013480130685855974087881990259714044429530400013096318559207381698178728900233068372070184173848778307287837189068130569781596813019269346041157938762394381273591057343063997775129939023520351165574215558719060764334081950667576224732234764762500219/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y^6 - 46360918240213580478011945593832789768418364455807513091867990262928987059147899922190867011597069329388037531099218017375898535498777439125030971219781875638764527745571088334921230025564654267442471610652370041237402232897281479973659104235819273668950853211646315194239820978014193064258224249199196024248247/1669488086617645052844427053238973913824968111496415642813971067319759231321055078219418611492335001516549258976456025907773286139048385223848106296909405911994339152964440070570523008133194266644480998581273110408592590050747549513341945409365477590910389040203130189600288661527869765209089575327015777280*y^5 + 4613570765903001987738162319096669568530570759665852365822349362597104709455162020458695193113079504448508182124738707313781939684571457669099291292530009768273949165709540787055739955942368983010176733247758157207120822766981474096954641943461248895794580148998531605389159737031908064283352725299890661913257/1001692851970587031706656231943384348294980866897849385688382640391855538792633046931651166895401000909929555385873615544663971683429031134308863778145643547196603491778664042342313804879916559986688599148763866245155554030448529708005167245619286554546233424121878113760173196916721859125453745196209466368*y^4 + 1715890368648369031731717136297869553126908398734158326202655551301401150181741950399087086385561969897952700775247834154152082562142721149395980700053914493259249971661939773564319902784485929553451801780279399534592952140253334235139180737054273761395419690907780668452497527345414999510134764570601416377/552810624707829487696830150079130435041380169369674053911910949443628884543395721264708149500773179310115648667700670830388505344055756696638445793678611229137198395021337771712093711302382207498172516086514274969732645712168062752762233579260091917519996370928188804503406841565519789804334296465899264*y^3 + 550234389687248533735048100944754483815591468975446433247025583409838583498949762128226902922277483368329280895761584836061834044103276355376077625426174306082378963679746644219932871681781012840141112784588922641238199910762748189291279018181927854702201044799590888446135934155059668393212671841571052975847/2504232129926467579266640579858460870737452167244623464220956600979638846981582617329127917238502502274823888464684038861659929208572577835772159445364108867991508729446660105855784512199791399966721497871909665612888885076121324270012918114048216386365583560304695284400432992291804647813634362990523665920*y^2 - 386460082031506796827064232712976547595575183136351133314815110307821243337617159548800805668066437148202890973503384223723410224292441467106266410593633706686334253008830488175963911409865073290793486841248443863069451730112234750004297440752847190136130998979302453489172073499554188315339139271852106487363/5008464259852935158533281159716921741474904334489246928441913201959277693963165234658255834477005004549647776929368077723319858417145155671544318890728217735983017458893320211711569024399582799933442995743819331225777770152242648540025836228096432772731167120609390568800865984583609295627268725981047331840*y - 30732217249695033439280477550970717298501793771404345326561243058172928762653355417398142295373564037251946966123575574349920222346439788728120189279576208180798153529875480494203616087688776198177932437072260297807397948548496054728951381264640179503364603867406920750755824230884407834241779074888690954049/2504232129926467579266640579858460870737452167244623464220956600979638846981582617329127917238502502274823888464684038861659929208572577835772159445364108867991508729446660105855784512199791399966721497871909665612888885076121324270012918114048216386365583560304695284400432992291804647813634362990523665920