# Manifold: Census Knot K8_189

# Number of Tetrahedra: 8

# Number Field
x^30 + 32*x^29 + 356*x^28 + 1701*x^27 + 3781*x^26 + 3455*x^25 + 2745*x^24 + 37730*x^23 - 2677*x^22 - 116083*x^21 - 573243*x^20 + 355483*x^19 + 552447*x^18 + 1438696*x^17 - 1531811*x^16 - 996462*x^15 - 496632*x^14 + 1548487*x^13 + 445675*x^12 - 390216*x^11 - 508093*x^10 + 94255*x^9 + 157162*x^8 - 1394*x^7 - 24448*x^6 - 2780*x^5 + 2033*x^4 + 274*x^3 - 73*x^2 - 6*x + 1 

# Approximate Field Generator
-0.690492189583426 + 1.21664709921111*I

# Shape Parameters
-572707367205223396224362618376205180492306589764868623340296740842788991699/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^29 - 987215017252552581976584021174126034726040035513479571528172917673161159593/263100973573907060085413579516233849512789172380921478764679833308423749054*y^28 - 186360367841608485833443046919745579714501679872761828645079257691033956152431/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^27 - 785431633034479720321585489310490594260164875291461846168618658878200344208897/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^26 - 36821025486485713911544366878133225856657142822638777096020990684776964030862/131550486786953530042706789758116924756394586190460739382339916654211874527*y^25 - 101473592348919240682544983804885830551300963936398609498815339059638705916620/1183954381082581770384361107823052322807551275714146654441059249887906870743*y^24 - 935998360267071442430904577036978012383954628773619927440011151705816682699873/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^23 - 5394618387941348297410165165523033798072394969838093648113803079951648350226629/1183954381082581770384361107823052322807551275714146654441059249887906870743*y^22 + 1169100018223324830854384608351504267801686688881443582687469486339015967103237/263100973573907060085413579516233849512789172380921478764679833308423749054*y^21 + 53208839371214486634359907382296593220246432507051352494970027165260243919257587/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^20 + 260664271262189486184783197718145698054704911203730445197818210146540937089838545/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^19 - 40986635386105281113394090283072246296827541367457226979531746788887771659835160/394651460360860590128120369274350774269183758571382218147019749962635623581*y^18 + 9701830558166963403894969458220944533595096762952452939716258216366546586379689/789302920721721180256240738548701548538367517142764436294039499925271247162*y^17 - 280832399678729496412907823340027265270565092218820791184654456098907802413980201/2367908762165163540768722215646104645615102551428293308882118499775813741486*y^16 + 1536550868236673785221562612323041608604584747153152787317059971351198325074750331/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^15 - 377433033577866619938404729256702356696565852116005233201753505044155432421835007/2367908762165163540768722215646104645615102551428293308882118499775813741486*y^14 + 7897312737299913618524187514936740400117471931868316819248330603149829383262023/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^13 - 292857805980290819009014472152552712674400731939816823717360208525872046831842789/1578605841443442360512481477097403097076735034285528872588078999850542494324*y^12 + 222774177772348782629506325501078590209857837028629475153107372333921824458815764/1183954381082581770384361107823052322807551275714146654441059249887906870743*y^11 + 163310168445194672688630532767275821866888279306850603597764097760630119403281963/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^10 - 10578800842026858146358033031719460624787057515364442422497837574440821974119045/526201947147814120170827159032467699025578344761842957529359666616847498108*y^9 - 83584282763308032043599276071387230092801696477957042178903312876700215318605683/1183954381082581770384361107823052322807551275714146654441059249887906870743*y^8 + 75243758288067165805958571719552365869309849544185762646488167933425278893793431/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^7 + 1457021719427692299343753823905230027733631995575024994808053244402556765395635/71754810974701925477840067140791049867124319740251312390367227265933749742*y^6 - 6777467104071189598726373098470962585918722979132415248979335754462334131671509/4735817524330327081537444431292209291230205102856586617764236999551627482972*y^5 - 2535777085221214142932934749414194360576130969528449921577765708432327616232575/789302920721721180256240738548701548538367517142764436294039499925271247162*y^4 - 296203345816605606381683778053229998029705927990090494165463760617953356115073/1183954381082581770384361107823052322807551275714146654441059249887906870743*y^3 + 208003107664466804477290053469415698077529658295719478979389802965824638964509/789302920721721180256240738548701548538367517142764436294039499925271247162*y^2 + 87522533200714143639069245555898053882749631778740815106751187363515778353311/4735817524330327081537444431292209291230205102856586617764236999551627482972*y - 13930658469261420165399816254666184574489552868568735209759098651531253733935/2367908762165163540768722215646104645615102551428293308882118499775813741486

851195784076988671100299818353662396671082224569576547886910387322905330272/131550486786953530042706789758116924756394586190460739382339916654211874527*y^29 + 27898853334121786913054359261407753199697865212356351755900565790016749915984/131550486786953530042706789758116924756394586190460739382339916654211874527*y^28 + 324149282115361672633925835104398924967788647491705626344230918979520347576109/131550486786953530042706789758116924756394586190460739382339916654211874527*y^27 + 1682588433934889972889053318863702162036915907018539596704845544792814981903963/131550486786953530042706789758116924756394586190460739382339916654211874527*y^26 + 4337327935777429164970422639829599918450073006351430085942552258491935484632541/131550486786953530042706789758116924756394586190460739382339916654211874527*y^25 + 5420577026363701239708178049830293578743198160965289363058370117916493502669258/131550486786953530042706789758116924756394586190460739382339916654211874527*y^24 + 4598236340043591314805454384958863997768950109307736784608698654309109981898251/131550486786953530042706789758116924756394586190460739382339916654211874527*y^23 + 33954291693720925440706542748992919537314288131989036300675599557433418702164204/131550486786953530042706789758116924756394586190460739382339916654211874527*y^22 + 22663914191797685284494751725235808710718287048053178418690379432319482753805841/131550486786953530042706789758116924756394586190460739382339916654211874527*y^21 - 101109499164070508135455557360279837227528650498515681754600670937111135052093228/131550486786953530042706789758116924756394586190460739382339916654211874527*y^20 - 563746811655781144305247831640245689813417253465146864840796218487491460032693661/131550486786953530042706789758116924756394586190460739382339916654211874527*y^19 - 74560312723477469717628283655778397920351991812099334101915346616780360043069898/131550486786953530042706789758116924756394586190460739382339916654211874527*y^18 + 711161618449127228343850329521448830160769846667329387046811079973959765915269752/131550486786953530042706789758116924756394586190460739382339916654211874527*y^17 + 1571599380949724926132295421491542997213019269421774788170171371196110708206466006/131550486786953530042706789758116924756394586190460739382339916654211874527*y^16 - 351241893833440772272059656172376233238323668254729404313844362921308981491285766/131550486786953530042706789758116924756394586190460739382339916654211874527*y^15 - 1870732117009765898819911977721877188190982893774918822797118810088814486472013466/131550486786953530042706789758116924756394586190460739382339916654211874527*y^14 - 1026901469948786546953303152362144717754996054221250024468978935293107614211309481/131550486786953530042706789758116924756394586190460739382339916654211874527*y^13 + 963704648885985818117159140788990269978542455708035651072068871551704729078724848/131550486786953530042706789758116924756394586190460739382339916654211874527*y^12 + 1392977339148625790113819166898432383184851434008607219164083280531860250127532218/131550486786953530042706789758116924756394586190460739382339916654211874527*y^11 - 69463323148165028756518199624172670572124009928507891267927089934324504949736548/131550486786953530042706789758116924756394586190460739382339916654211874527*y^10 - 658565248755758097125495862748487359877721732165746590994932018294192338530277681/131550486786953530042706789758116924756394586190460739382339916654211874527*y^9 - 244821529144514505013509940645882417620153662369874392793638136408296102508816893/131550486786953530042706789758116924756394586190460739382339916654211874527*y^8 + 193618747677160616447465839098879452183733677026041974685110529750784266487817329/131550486786953530042706789758116924756394586190460739382339916654211874527*y^7 + 8205138512862542596260917680533801407251767113652598569605863854991027673145193/11959135162450320912973344523465174977854053290041885398394537877655624957*y^6 - 20425422341165104333969893300478277976072620324772650966672965346334642793546245/131550486786953530042706789758116924756394586190460739382339916654211874527*y^5 - 15260946874324759711562537160824540303500038304470647769263550884005056832561042/131550486786953530042706789758116924756394586190460739382339916654211874527*y^4 - 63669870339741418014426167288216582636968141549792701623474604678495507941118/131550486786953530042706789758116924756394586190460739382339916654211874527*y^3 + 1120855836334147192839542883290877699444439940377582121506388823174261584279364/131550486786953530042706789758116924756394586190460739382339916654211874527*y^2 + 60701184966027828442142765768628013468729571496483433436513128160667129020655/131550486786953530042706789758116924756394586190460739382339916654211874527*y - 18505502981367457520818969891413531188989904757085341856330023992878760431008/131550486786953530042706789758116924756394586190460739382339916654211874527

69040518530936402398455635752231770956581769904645427542257629844911445060149961720656991912130/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^29 + 2207029850205864727215487958249553312903473085444593601820302652767963290426468536576249021793091/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^28 + 24507498927746587450439437755627819051845104069558477133203348603579514738377119223620459267855301/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^27 + 116682088582751475381843834806603105549982144869814599525744641343865285471796312982993244508225752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^26 + 257746947838543161626105042904462655633813714641288136229002620620288937948133563408839347164362509/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^25 + 232560808062782909839139482490561963691908416238844913080592581511458924400282523872062899015939729/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^24 + 187081838104356857763776531522123498631535320157598622271053049693640836911221329002923210666226365/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^23 + 2602646820188311512876827668356995573410161752750671047357886704745252094777000667288000664633288680/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^22 - 267578034599511908596174098852259583542219127237213319203580193914180665855419715943796673103659349/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^21 - 7949163407850792192289345932823480368358395408687631253571768212625593075999517654142879147602811609/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^20 - 39333622969660963607420291033313130697688516237537816087148754118653771508731880946950999281821719576/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^19 + 25654377293754635405224704185145025875263753264689730282807903383081269103888119725393527007943377392/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^18 + 36455723496159370131788908989586826499318724245469771984876690967209766047964179048455884686193205911/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^17 + 98879187134371204623662379180856070429331885482836567096999632990138307527930332105238096765184858938/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^16 - 108238899926433048891280742538611511320858343681290892107287337536303342927023713527523508212828995530/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^15 - 63197391601762863762624409998484064331072129832347244087770814636688347400553238585346866591300084752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^14 - 35093576567382875114799597207472735239483567770425226259699939861419614322283718336418618130871839730/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^13 + 106940453007948332921744960538389815586919436075278433534053083706371775599841880036476492978262538872/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^12 + 26798349722981604305973484907936771739976379285186845418019595562355013102925325577788683605327298752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^11 - 25166489367757823219141871573217612152430181961274618697191081770966149947009400699882544936697028517/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^10 - 33985977169657177182568236095386014098611880603532961243291365337703174232807036133847267243171003066/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^9 + 6868071407402909495764207379487913156786706374861257427727228774732786816545238896803514037905068349/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^8 + 9885417820848145604738777535415927599027198617694332402557894070486003597652373886375389199860105335/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^7 - 12698530915308835074386995269730348222926063456876645766529661230914585326498031423753687651573093/199058827229377982743366947117262377687346825768581460944305561058806184881590148532568545587*y^6 - 1451235361690515718754349594580103899094821660651420437163759973344614063988947554934605439340803023/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^5 - 174176682649293799250881964318408045563854487755600207450367414337123296613373692346168729824070427/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^4 + 108216465576300447926473351321890307619690098262086980524666429175158254460768396641067601069898706/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^3 + 13849617347519079378649644111603830222676075775106405690401943291265987834159133810761190954450454/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^2 - 2338875182573462413336485982456200717275579479187163652188921537134102224516787213824645920018391/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y - 151510675920486770397622077408410254455238954669278832593673229059882529131252237443571365217719/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457

69040518530936402398455635752231770956581769904645427542257629844911445060149961720656991912130/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^29 + 2207029850205864727215487958249553312903473085444593601820302652767963290426468536576249021793091/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^28 + 24507498927746587450439437755627819051845104069558477133203348603579514738377119223620459267855301/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^27 + 116682088582751475381843834806603105549982144869814599525744641343865285471796312982993244508225752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^26 + 257746947838543161626105042904462655633813714641288136229002620620288937948133563408839347164362509/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^25 + 232560808062782909839139482490561963691908416238844913080592581511458924400282523872062899015939729/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^24 + 187081838104356857763776531522123498631535320157598622271053049693640836911221329002923210666226365/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^23 + 2602646820188311512876827668356995573410161752750671047357886704745252094777000667288000664633288680/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^22 - 267578034599511908596174098852259583542219127237213319203580193914180665855419715943796673103659349/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^21 - 7949163407850792192289345932823480368358395408687631253571768212625593075999517654142879147602811609/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^20 - 39333622969660963607420291033313130697688516237537816087148754118653771508731880946950999281821719576/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^19 + 25654377293754635405224704185145025875263753264689730282807903383081269103888119725393527007943377392/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^18 + 36455723496159370131788908989586826499318724245469771984876690967209766047964179048455884686193205911/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^17 + 98879187134371204623662379180856070429331885482836567096999632990138307527930332105238096765184858938/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^16 - 108238899926433048891280742538611511320858343681290892107287337536303342927023713527523508212828995530/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^15 - 63197391601762863762624409998484064331072129832347244087770814636688347400553238585346866591300084752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^14 - 35093576567382875114799597207472735239483567770425226259699939861419614322283718336418618130871839730/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^13 + 106940453007948332921744960538389815586919436075278433534053083706371775599841880036476492978262538872/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^12 + 26798349722981604305973484907936771739976379285186845418019595562355013102925325577788683605327298752/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^11 - 25166489367757823219141871573217612152430181961274618697191081770966149947009400699882544936697028517/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^10 - 33985977169657177182568236095386014098611880603532961243291365337703174232807036133847267243171003066/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^9 + 6868071407402909495764207379487913156786706374861257427727228774732786816545238896803514037905068349/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^8 + 9885417820848145604738777535415927599027198617694332402557894070486003597652373886375389199860105335/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^7 - 12698530915308835074386995269730348222926063456876645766529661230914585326498031423753687651573093/199058827229377982743366947117262377687346825768581460944305561058806184881590148532568545587*y^6 - 1451235361690515718754349594580103899094821660651420437163759973344614063988947554934605439340803023/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^5 - 174176682649293799250881964318408045563854487755600207450367414337123296613373692346168729824070427/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^4 + 108216465576300447926473351321890307619690098262086980524666429175158254460768396641067601069898706/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^3 + 13849617347519079378649644111603830222676075775106405690401943291265987834159133810761190954450454/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^2 - 2338875182573462413336485982456200717275579479187163652188921537134102224516787213824645920018391/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y - 151510675920486770397622077408410254455238954669278832593673229059882529131252237443571365217719/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457

3368608061598775476703332928853147748071945645580455837333528248883105024026419370428496177157/39413647791416840583186655529217950782094671502179129266972501089643624606554849409448572026226*y^29 + 54253083238762745251409609492245809828484303130193527865806389422958812959145647326889326837003/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^28 + 814653217319364012208743414438385267001279760117217121818754516626836172177771528047329182107689/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^27 + 2991903927053314257736680816149357996420665186724284956628967194039750113418083989075886713486206/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^26 + 4654181501073820730301531620020644728472883747279440180099002574648310513261650684985474695768473/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^25 + 3219028532109518101432149567892658859529889481306636613312781016475056049142420089912231374851493/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^24 + 6208021941154286438744851329266298892430091103558732188708954135744572310062446798411207785812417/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^23 + 261224974457445163543050278901400936752963357340599800489881068708277118760993605939261586990304013/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y^22 + 38807678810794708771534836022819109886218463233615040167246374044059498259812712995883544331158793/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y^21 - 86862285339929056013792999035913111902006281534986612284338939807393648737601067284391449349965685/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^20 - 444073377956820703318405582367117331339488200442725097767574745562683193596531975475992645175631347/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^19 + 394276082219329092439511348002621754127870663825862881213577826679970624540945341080076772075087004/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^18 + 1032937235680397243924015113003395702024720911675400624592769343713132582182078203564946799165444917/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^17 + 836959965094526412701557528343206968083421970341505575583817106504622876476230757603976688114516081/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^16 - 2004395639765334886306788381733236903763938779271339848669420787272060449267218580542879644016571556/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^15 - 4275094668228245580594449060078208246691960239282208374414949518323972916723797759386165154936320387/39413647791416840583186655529217950782094671502179129266972501089643624606554849409448572026226*y^14 - 3646344955502969225213478142115798642184372619352471472940616581283678910394743166814257294900210529/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y^13 + 4314258188360751935574171794453422522160619773988381780549012141376371946437910259404863580361404243/39413647791416840583186655529217950782094671502179129266972501089643624606554849409448572026226*y^12 + 1184252489985152722371866557778066949145151788027109794897603226789861224014748606735000871575434541/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^11 - 852591296727897980291507023854123102225378887523059710971537262104448166948182896885541374806369075/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^10 - 490660171822403149131541261159133499399652729025800477796728998023509749524510983903603822801378999/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^9 + 16428871577173924252136304181017311150245141083654160674622233010531373236580001326449723821712361/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^8 + 1102739068860933284681734941191878946712130640008323712591388157981579445739878785315306797504915749/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y^7 - 690051764816717988199247022520712846209835729077419243996981550969765940156874634101496872413150/597176481688133948230100841351787133062040477305744382832916683176418554644770445597705636761*y^6 - 8005927850795001950072629889270735861305633666798908378034351941163505457356033792038043661375131/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^5 - 394426197821907434700611737272509683833585452851967976292399445535997714575205877103670572026481/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^4 + 12159916807662888406146965041306084730948919058254302037043310426986071587709714689913991957247401/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y^3 - 507197669383580196489623181727844557453866186400639691859687692394698778647638207087897838589824/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^2 - 536675321081089699552307466106403951124216196312687777896266845789025227913575139183807211349697/78827295582833681166373311058435901564189343004358258533945002179287249213109698818897144052452*y + 40475013580033099661960902517594447078318301848401521990118008533873152767483793468494283425133/39413647791416840583186655529217950782094671502179129266972501089643624606554849409448572026226

10947762294433434613823300789025310895176410801663088870667880932945049240569795779710212485360/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^29 + 113625156886467332146779151213688346725509864306113738981522183454786687151277038122488179153753/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^28 + 3599947824076758488264515385033853040577277689852745208339023571612160263770274071543431506482608/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^27 + 15419590541565924885015135555677675248801340821596204864624805837589945842310549558231814335313566/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^26 + 9051935078157452859259864322150447522088577916366105370052921078388018200754656896211158147950179/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^25 + 11212672807318631140816445891944547041365844033498936457148525434098135185612270252269186216544548/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^24 + 19354812937966307775903708998044611650090347608186428415134560519262577340963516385051630295723383/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^23 + 412146388451669249203325630595587288690080495390526367201990684389968739105545415262029185465970203/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^22 - 40218874404476165515272733678716629199928257683091478751266211360188856064004927088737356127924952/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^21 - 1045415017081918013938688138775312131093741929857364447790017430629400047308274776809418800292592819/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^20 - 5130804166912310758172081803147350997599767595837533900159558021478418982167254181805649540267053173/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^19 + 2921919673398567440461387140182502252698997342753334598361293824170403624385232159598677964353064375/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^18 - 118572381946367700929800687298351782261176163656850822876816173074779626554541080071191690742205582/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^17 + 11352608249997237689904374110041577667496868056664208500217698772532292173602584667054274952150561936/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^16 - 27754162213368582791431060227042563020927000226816805211036156340700472870556939404239212319516277924/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^15 + 11726562846695458883718753252230493212631007046316321313301155113581446175851613890201157877900119528/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^14 - 963058152055416085061541478358022279832296175207446435517413656442901371132947851955538681231230122/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^13 + 1808708638419208178722461842716743308375749680702352159931468939133317783235363317717130556511471584/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^12 - 14584028653296796916606218839852559821294315143241682945066534281992911698903863915009567427985088726/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^11 - 2887990162990930225308856893265515289096503786094933722076378458760666546123356478836873329592102419/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^10 + 462257186693511190960789968930131780172071211369364740263943720721078049781819858080459138011221439/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^9 + 5664568894567846941688228007611744286407891106708972554882255142803896827122603968864866878886567908/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^8 - 1301012260312337028599838209870357695144343355416023599571435314812313722149195364902861373795911297/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^7 - 51734716850824963767418061112911019823655293002443889163588441777549214496642828831031208090201708/597176481688133948230100841351787133062040477305744382832916683176418554644770445597705636761*y^6 + 155108569532824609984296020197971480319307489436451239395684118226263861351724664261765148523823309/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^5 + 94825806718228085503096523886549205096567520207218194129735526306083770115843147709830042346460422/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^4 + 17448043525428105732909736702164127724230444194921079044584390159008175334959558116388417634963890/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^3 - 8386544058504862363215826547404004088445727284773735903480812013840871394673973048753469203101988/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^2 - 1649074791344173160699601752700392897691052328175040172438222375727703394716074312129422714633353/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y + 630123728379702607263870748745669603105106854091235323643137038216079768604057284410927000736923/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113

2586166284421692669515767711675951686781849966554482839368561357544815857428890324421015623631/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^29 + 28349320226198657137331142414307464423798065560808125978934255230635643420777647625835588188664/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^28 + 995385723257634579331322734198344666403022546618028860416467075358464188457812065287732442890575/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^27 + 5260550266051514697068852155664161057182854944553191441650600050887182310213936014833997522672956/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^26 + 4735260137985721370679801996400938523959815173321857118979909475102045941846723466425296637431174/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^25 + 20331312389411826708772610837263589783744229512664222371069087982591068630284328726737642748557856/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^24 + 22083272588338705851831524243059050076576504520757611061909687891596445648987871326122107730494910/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^23 + 10295413603333277825160487960132266988140248022568884411430904873601714315826079467927248272294090/1791529445064401844690302524055361399186121431917233148498750049529255663934311336793116910283*y^22 + 9934128646161774610090642660198631122093463581937470360112399255318022667000235778180487066121420/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^21 - 246774837317928888449865961308636522120604464132782743006156404556119863686105871251564846650438835/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^20 - 1714413257567410016452274512069758578476400530586142907230363236786833800536003218066578601870192255/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^19 - 178333680300554253104123744761195772691454845703175413290877508404819424563388836407688532408459384/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^18 + 448469537821127074365519575281123845152663219981665212859364161101233676637312151185264795615359178/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^17 + 4917042485107358167978080299095859441350223092143923357467572688245197886327977963875138925252888710/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^16 + 55090624146310529305281024109311627911835265011350057550197132248757913422743030991012078483822252/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^15 - 326780878534923039570782591463265002321605262705197577226519496973580324600909905322063108635297623/1791529445064401844690302524055361399186121431917233148498750049529255663934311336793116910283*y^14 - 4139435718858126681003311217084565854359768976925132996083442003834146277497017047325272058197169224/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^13 + 126342486258205255963061247408253918211462260703726646052370978989392462727269496339939231096032165/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^12 + 2875029549113910895719681109013137665691988756598898477354098054686706852926134890147963576208336777/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^11 + 1020141580818436858346800217893460317974256716343556225681432291786401949818398252662192899458593518/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^10 - 320289302008026285624044325519095439515869883847500264593142216753739322980623097906247362729558044/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^9 - 652313196607196519193090384630111252928189716563078553133292773474388191578414122685311586050175332/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^8 + 85659175775933092132175836577837859760182158989847246882412912258917620278325465416408250495519526/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^7 + 48992985812233721633169642076438603025015326680971790032025822198148119810920426651000075208679202/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^6 + 1274541257530296871638021472590832224670343243823028329948304153831773390376998638130809565188275/1791529445064401844690302524055361399186121431917233148498750049529255663934311336793116910283*y^5 - 4460215562432688258758650221986035311049311735689738266214899556572359773209356152238127707059648/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^4 - 2285806841755659752628079998583011719958960798028135671290855032298238910766196029256397803633490/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y^3 + 148819789446417391281861512915395469998410376031288891591982201310925463752628450904836376611965/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^2 + 73826170464927129073406124504912267036903776989957026423454461004933518917701454382358487007746/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113*y + 13440541908861717521954226780071827864450609605849931160611786810116132116718119522592932597057/19706823895708420291593327764608975391047335751089564633486250544821812303277424704724286013113

-13619476701154740486451792933521481626306698235763860132759835497174549670274159490539147507/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^29 - 408224094901990315943827875348125247362691709827888653740415107297661006567215366466224805338/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^28 - 24924717752705291601728886152108622351171012426185951127152521823535673236694509509205487205101/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^27 - 184264668575561809443015771130038118509025523866513270220379696739518201160484802074768395170041/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^26 - 116051496720491811802739313708775386817939563238222216418613397353790937065658401669358928497189/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^25 - 329788018634097803182228282925881945854258873102607560403158778449815501611551789878207896704133/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^24 - 378534402416845047577798183900021792476953914397181794994708588628115795697955470034098816472201/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^23 - 1188746077802544972822729303806029845740214680208819846796869853099042759722905283657418251651563/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^22 - 6054985907455144568266435119605337172192860641160091849747938279574655445580731586960185881605249/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^21 + 6934225096715306820413080857535031137349245580180121388473148826063240617571263314801379059780941/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^20 + 60530601781716147059442756762960080234986664389140758052241569580819511964802632275978449561524065/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^19 + 84092167350432575180068073935694656452477812572761948151780775006789884229483250824740282695607943/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^18 - 77706840054821633866228500277305944398236557207567656618263502883703409476140128442796932201071931/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^17 - 107900347906686970357377193815125596880301440461640981561791882756608249525264552114604913161951429/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^16 - 393970604505677671257664481033376550377355941523752823703667874160760870001095135374847682252664183/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^15 + 142817089607377941928645674837166813301946106758810446066119217157410842429818810546220035666358450/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^14 + 265572821968747377232517420779155469556634163170351789471394753720501234602888285645113307243917461/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^13 + 94646619901288309159789316547979445521022021241493409204284893365002992947614360444817348673628165/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^12 - 83452800206636223600495046515728962341633941315122091632771005708560911392300369499952441324128545/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^11 - 71897717918604328401123885257734798004421899866223557085863265863029544220059616078076069118367663/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^10 + 42945889618155344983540270118457200552379281108979971113516971378375439855363339983392262410012733/8758588398092631240708145673159544618243260333817584281549444686587472134789966535433016005828*y^9 + 62477053139091770425023974834538718540367258364982915741005005593195701410481885526746217127571223/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^8 - 40822688100906642742208083988852245988085620378785171946580613763259875838318298564080507754358639/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^7 - 262662931282427535501993256069815128295054950752548735866203831759498507188038814052637819202105/199058827229377982743366947117262377687346825768581460944305561058806184881590148532568545587*y^6 + 8004553466150632305908150888618991777527642810155117992719808312166733847880541348179506800167313/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y^5 + 202281967912879720608903454213987280162152994133853976039228843446980037034082093962747596576993/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^4 - 49845239836340842490451381243988388603432383288958985004533020824693209770228934915001854434264/6568941298569473430531109254869658463682445250363188211162083514940604101092474901574762004371*y^3 - 150417808582977059892397661786213207219543474114494726661432050427859089380878204286504101450611/13137882597138946861062218509739316927364890500726376422324167029881208202184949803149524008742*y^2 + 156054153367752504664665774571697048419278703556846723751164053624116889446292180758328355647477/26275765194277893722124437019478633854729781001452752844648334059762416404369899606299048017484*y + 2264404605289302531007699901947698405374889451688929650447883742324533087994946274959214803177/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457


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

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

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

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

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

# 1 Loop Invariant
60013111131302637608093340269232774996713562201097301351981317419011012221660125760193378253910/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^29 + 1952045003087566822992374035031206187106002559476013661886445358520790650859406189483949761569929/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^28 + 22375577307111436244677852035666729399836622259670054449027271776179523783182168150321049649143991/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^27 + 113306679268720126572123921717478167642354749193899446499371971262599225066976358741319284194022640/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^26 + 560691096930138197451399840121054939618985236807280395713109386465221402733069832427349184516291071/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^25 + 650859762516862204828955810962025991425432691520635355299001676580081517666124219365001268937283977/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^24 + 543482381089074812577680260747807275652172656962250826161525461813631443306450475322485573291704287/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^23 + 2351894303590223818953148672592192254014924575509278837752872327181881045285681011027724314919950148/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^22 + 1034889439356365558212776797831928565318767493889713733787691922997874315450275632565753949668342482/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^21 - 7087251634863182783011867367222094215322879772716004713905193859032183699605557123449969625893627371/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^20 - 38027038973976131810267894463028495261522976933841655344446479931699894356890923404470999395020078264/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^19 + 3342657545334949576513334387309874367772847130421005530360633588099232308049032110675585381001005761/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^18 + 89840177976471353403750663880099191842361474299850055026800442553021167414473002082693729375410076775/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^17 + 205575652100213806318756951025235823831627524998473219703013073693212793281595932945867599673248769077/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^16 - 46846116616671453865582848659916256081392130574143854086298360758867389459183553050907721501626342607/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^15 - 218736331579477740389032867138887329615775691613047536344405150811832018882618287032305739571225492055/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^14 - 57977124177678100633194591521446399930138457502367700178093984722703600876990957685835946474061492658/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^13 + 154463539149799215765699142477233257357596445966238141221492200347936238116844101640034473482351458829/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^12 + 150792767069346560315203185954860281530073417327629594659564967769783545188314562425782011677546514521/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^11 - 11930641559426257449883432242625737957024301921060586118611770772825657800205490138094081619573000524/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^10 - 84367440689490579036701773790347703575399822346975677821336239615470558660978206034432206554728154269/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^9 - 19081282403287550241466425553524124901895332324785015123896646474110299441070244680119517182608533309/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^8 + 25756993806923960526661935053593721192836032009495958589049973119798021993564267316580890571114750959/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^7 + 400647086399142467198777603601128892769624282219517809515936990022284316418624189841063785999828998/199058827229377982743366947117262377687346825768581460944305561058806184881590148532568545587*y^6 - 1643946948200650599541826593810962204288808545786026864955292409755922943420686528984649057929327299/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^5 - 1707415794029252734032541668868387468705333412727608058805316577924622463066883713068022026564166045/4379294199046315620354072836579772309121630166908792140774722343293736067394983267716508002914*y^4 + 58134989331479953590254500245077164728975386152342530478547189291748535129081863315845009524309165/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^3 + 71452208072728654252568798563267793937134820301966193148941804842164646065928696967817804604735695/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y^2 + 1000054861090465360623170085337622122076595292666900897531895295432070040257596108523306208041469/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457*y - 1885827170050296794644701140651835267760566290660183220416869372272342261852082948677676493533526/2189647099523157810177036418289886154560815083454396070387361171646868033697491633858254001457

# 2 Loop Invariant
61234858154419257401979477222335011577918633188044685687344570417221977031630330031717003558274267422762238459797525784261450571341346846958260867549136372627067298781089863354225605618449868167795734915/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^29 + 2010051902764006151830104489809740115762087599743911993651090240126132347214799612244038007427331671145722986360866703471766600732751959803578308654658590968830031784032755440171428928047372943840655462823/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^28 + 23454802281704679328153921743238926274533412090443201911626094353344706022129245513942045082607454243575596937565537406204213893892875901670106655224343991490199657149268759670644481247140338932876199527765/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^27 + 30848660540974214520182489799926981073495431732851176116575724868875461124653439563790603789551916704330830337890412186764908431915347204956981378564979389975419429773346123078308675516810563827298783423447/3562169323148488693166768476547766064380437708817579580557052582478928612738796097676797093276262613850551593930603589984970087441979740722767053530839672694955833660237014228878448442997451398745287452464*y^26 + 331892569796033010389866294041408730033507555520277411527587043247177276220450120022379981718703695930283034797836171957947188913123788957802424740818535658214536768703735416665220235471949411793521753166349/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^25 + 39782779919044517743057650273566009290913864558377038378665841043355618258677641335018311066611177986060205415945156025305979964596842167683121163247443168307765857954524866482628104652466912171756719314661/1187389774382829564388922825515922021460145902939193193519017527492976204246265365892265697758754204616850531310201196661656695813993246907589017843613224231651944553412338076292816147665817132915095817488*y^24 + 19972872569383068147083258791844499249965105885118967816050089123238858995192165925663519059202622933280785439268275012913124642123580581924017772519987748068050521451049439969196928440216971621385062711937/527728788614590917506187922451520898426731512417419197119563345552433868553895718174340310115001868718600236137867198516291864806219220847817341263828099658511975357072150256130140510073696503517820363328*y^23 + 2721392597299942184321550661652637113577928223805699482799407252532925740270379078634399247972711140342095607393679655268112693208538250511946915996933188217866339311935312997546613799194366535837098188439433/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^22 + 14204761723956147115051467107227115016218287019733589698882721753645736987635950903009660716841359715810632497776024078841974688111921295016208901172935217622984917345681332042622834008763598549831219903975/98949147865235797032410235459660168455012158578266099459918127291081350353855447157688808146562850384737544275850099721804724651166103908965751486967768685970995379451028173024401345638818094409591318124*y^21 - 5592562201805781537297478906000554507524372659471793995615123917071921188926465678350734926410910350337981559054017326506886333558712285598848978695213134350313590364850331077836312372631529958309112955037213/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^20 - 19961414755142221156559063118298664227774262259606930193889115461480040795452809959728727785947616866810072222261627248162504668783636799341192671442180688563775461790633602236406798931576058812073596264579109/7124338646296977386333536953095532128760875417635159161114105164957857225477592195353594186552525227701103187861207179969940174883959481445534107061679345389911667320474028457756896885994902797490574904928*y^19 - 3593376046799741916090017709285409770045397923658062158041784271534108527325427220107703898977590362833514076793865350986496698849959893104692892834815350605136649368207545832843026055482508761639780030151237/4749559097531318257555691302063688085840583611756772774076070109971904816985061463569062791035016818467402125240804786646626783255972987630356071374452896926607778213649352305171264590663268531660383269952*y^18 + 2289117739356495552929906907466304100896216172791887218881616566381753049392941703769671888011513693429461592020704744459250828513876078075341541316947595706810787144748881385389756969811880849072828644709953/1187389774382829564388922825515922021460145902939193193519017527492976204246265365892265697758754204616850531310201196661656695813993246907589017843613224231651944553412338076292816147665817132915095817488*y^17 + 14043876291218403726004989511082064592719713717234958663999783913194412229820578437111453114858159332280165111754016337086547472778003654579577755656857634165411964411752405875783704473488660131952062048289973/1781084661574244346583384238273883032190218854408789790278526291239464306369398048838398546638131306925275796965301794992485043720989870361383526765419836347477916830118507114439224221498725699372643726232*y^16 - 473753718175583013815218695740648514148367679996127320304110843660587531952136472025942132714185112044560996944212659350231237066976739180640697993870929158628313700511389385776304739121224510051320911361641/1583186365843772752518563767354562695280194537252257591358690036657301605661687154523020930345005606155800708413601595548875594418657662543452023791484298975535926071216450768390421530221089510553461089984*y^15 - 7823135979773363334848534427228416603686384186462406687721034722593108716268515605383550993693874977657055293808135198868277898087416558327192978077960211808879529966053543721901477289411797575868213551606771/1583186365843772752518563767354562695280194537252257591358690036657301605661687154523020930345005606155800708413601595548875594418657662543452023791484298975535926071216450768390421530221089510553461089984*y^14 - 30234096900328313725898803803063547928738408233600029685139370319543049376718893235753299494294360044403682687972416401671352335522041367807309633694392236586670737184647374808962230982970416253826259436855415/4749559097531318257555691302063688085840583611756772774076070109971904816985061463569062791035016818467402125240804786646626783255972987630356071374452896926607778213649352305171264590663268531660383269952*y^13 + 3624896527497164566288089300135348831124510123895096354849816805370966946022444535491724933127566762938996382576859733097842641784980924084636368097473110583774690436887875519188026609067530675219401443567951/1781084661574244346583384238273883032190218854408789790278526291239464306369398048838398546638131306925275796965301794992485043720989870361383526765419836347477916830118507114439224221498725699372643726232*y^12 + 17448283358604624967199887835272048568749516466594119880449102174138560831908996884518114673272888390255060721242045892151044391751658088203150269479896276680729507131311179160351373067610945861665681802592789/4749559097531318257555691302063688085840583611756772774076070109971904816985061463569062791035016818467402125240804786646626783255972987630356071374452896926607778213649352305171264590663268531660383269952*y^11 + 6473303430983385197977871504012963249181249844912514048835699424497490412834475674680664065489715757425571264915584078296817939111636310321251123720088812721627433298105373166981051011176846463118401802175219/4749559097531318257555691302063688085840583611756772774076070109971904816985061463569062791035016818467402125240804786646626783255972987630356071374452896926607778213649352305171264590663268531660383269952*y^10 - 10343110976746383462798290550354950038413823913004826314483655674462275211023699856984572652327215284905340302968935849327088539227593804258696481590419910644952937408223128861720508253473808669280655484916941/7124338646296977386333536953095532128760875417635159161114105164957857225477592195353594186552525227701103187861207179969940174883959481445534107061679345389911667320474028457756896885994902797490574904928*y^9 - 8565769656582876506412123362177890520361267823520008425952975276342002769010127272205004388070116123243520412638291187731068869973900055149017203242982846762496663768107927105837284328344733139428123915395155/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^8 + 2767831775089053670548538654346839738388660145267192329625394712802725711758562126307358697269133734586752248574179478549280353009701849370537302619566311064575678924923881454616990260070474375011317796137749/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^7 + 208107830014612666379653242877462286039240541129926180734020838669942578464709644157723067521349833447089530559103450554191414538208391083505404194544266903561850079124746089455616653530738925052659368632169/1295334299326723161151552173290096750683795530479119847475291848174155859177744035518835306645913677763836943247492214539989122706174451171915292193032608252711212240086186992319435797453618690452831800896*y^6 - 84251590227778981171456527470400777641240880890874356276475872083535690738875291301033755235069769186345327697033976434296400341285925545796464126600162678715044567506085000478334566362048127567890425798567/1583186365843772752518563767354562695280194537252257591358690036657301605661687154523020930345005606155800708413601595548875594418657662543452023791484298975535926071216450768390421530221089510553461089984*y^5 - 283508464934872496741737979116016324280448312596468984973396704903189372950298760639313948776861908382957932086646594277087024891974373368618888416767491685722865935177542824867996691612864901556053506251367/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y^4 + 58341300106174978891020741182857167041134097342184000783793174240495849066823723140225831568703188750994270731749262905864258906662991242997626743386573684220280593931956891462949952752941185925555349888653/7124338646296977386333536953095532128760875417635159161114105164957857225477592195353594186552525227701103187861207179969940174883959481445534107061679345389911667320474028457756896885994902797490574904928*y^3 + 3286839314146380236308075103193779223254499112133433249552741853106492478153177933014130265365873561078313544710170229598572028745400574718288999108042474414690419384141971918429261705312492487678989280785/1187389774382829564388922825515922021460145902939193193519017527492976204246265365892265697758754204616850531310201196661656695813993246907589017843613224231651944553412338076292816147665817132915095817488*y^2 - 3345659387887017729627002265435239587542580363487098950924005053357474643932502814294626789542626902369747050963063712776408260707010987083492553204970920750051110883265687955459650977613196659707194112391/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856*y - 2299342861700635672098463872925444805558646499558954110146240009392706074524183367586994032009566449510778670583603846247019470365155532293772712667394867185174098334553685657935768663321129110576453707769/14248677292593954772667073906191064257521750835270318322228210329915714450955184390707188373105050455402206375722414359939880349767918962891068214123358690779823334640948056915513793771989805594981149809856

# 3 Loop Invariant
2230369786828582561742159791006223299897651974817151313861311539180661618042217694762071640289301501057193657272546305129623979357834296391028628106404966707132149733807694355048560462953252428634940422574731037360551809738429742541642883313783978490348659/1024092367841203580593222640149693772189025282396810488873748015152225499434634775640514097438353367796794614797560359719317063532170459257886143107556036172850874693521840381795994573873559312949830293964356347100347047950198038210804940918470165826862080832*y^29 + 3925273869708543233559872763660349590369242587228488935439751741626254886161903426942600113994350324132054744096859174346527410091700808416101195925313215150131738152018726420243052584660485841020049703333245466109624999604406659307559441406628158362587107475/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^28 + 3767659273594722133494174444643434197572127180836637449938863238550012116594925244689445705800052199428994464980147053884107822642935323216994288131504604318516009956191180207165157924609812159009285493952620257106378763027716643734672321515548475263268618163/4608415655285416112669501880673621974850613770785647199931866068185014747455856490382313438472590155085575766589021618736926785894767066660487643984002162777828936120848281718081975582431016908274236322839603561951561715775891171948622234133115746220879363744*y^27 + 232079001675465221015675607645575552555098498545105885824385619841789875940837394199992406500686439339407502188195393553381912671559670822782700844306001880828141410516211125173177674453429733991969512703320794697277669910947965831932575489254154897303748085621/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^26 + 598096332709639873675000797229811187537570458408412204780195928277748219424008904515491255612588190536025234434241902730765493076625331646586098829946090206320759630773225390763172182662970443802078055448875010260930722221322913848155881237191079190843502153453/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^25 + 49841606008546744823368400351427372863084650167267822290821025700389337876635705792369492307158028423425332822149259772825144947214823577743559671395630232860712690323263784746092622407125661811317316423626946007182382693798837477066027433447170364067066295411/3456311741464062084502126410505216481137960328089235399948899551138761060591892367786735078854442616314181824941766214052695089421075299995365732988001622083371702090636211288561481686823262681205677242129702671463671286831918378961466675599836809665659522808*y^24 + 217777098920531085527547758232902853802768899970092586117990345896013737449027548156343730837850992146639319969846385879812724254468190741646727651034361426371675123313638352725745026390726175619737793579683348720908679037521165282120793361057303617154402312921/13825246965856248338008505642020865924551841312356941599795598204555044242367569471146940315417770465256727299767064856210780357684301199981462931952006488333486808362544845154245926747293050724822708968518810685854685147327673515845866702399347238662638091232*y^23 + 5144955401095279356323473909956711622497693059666207728945975170237940277711181408872112940412183766595948111545065392184791588471985982332513200667938178462517020899018969929758774239679672724494944307694881620475390069611432442562765056484611865308262011464205/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^22 + 351057688575836167292614785500545557625104261962114521666293016621508892493875844976428138369590452310757111672241108211094914015169037494392757653369507275808042193499145874428457049587586926997625500173464286822703474216890361009466163954170463898829923475649/6912623482928124169004252821010432962275920656178470799897799102277522121183784735573470157708885232628363649883532428105390178842150599990731465976003244166743404181272422577122963373646525362411354484259405342927342573663836757922933351199673619331319045616*y^21 - 5853391254532988087127031255499580013432882177971808772522758986151076599166625970365954568094501895093755961193986581395807179364302955670605252590063608209288243829649364400532934517981451464404279653718989963850139312241884013006499612826312315641398542764111/27650493931712496676017011284041731849103682624713883199591196409110088484735138942293880630835540930513454599534129712421560715368602399962925863904012976666973616725089690308491853494586101449645417937037621371709370294655347031691733404798694477325276182464*y^20 - 25246720846398433773124733702540009228252112913212287341618387604617750906258139285206481839104432665858531022936464805634177280429538391163480699676076890213452139846940567671674206782034050838851152512427465576007614961140314440085126666878847066394821294709887/18433662621141664450678007522694487899402455083142588799727464272740058989823425961529253753890360620342303066356086474947707143579068266641950575936008651111315744483393126872327902329724067633096945291358414247806246863103564687794488936532462984883517454976*y^19 - 3459098358133125125024803620930212325765311934655722752471334340347685528202463879112553334311427409138429844721426931581529145244998984794218095803139875002688916354339960340946732825524444613723157313930698656739657365599718121675144379405263882659990586462281/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^18 + 13822376802229926288480849849870977748921430886528179156687207411652683155218508503852136829013670623263989558442680516379873462390236707779281445986922043569692738902262434404981291932627596416225370547872335370119982196802435641718780237325589308234908200064477/13825246965856248338008505642020865924551841312356941599795598204555044242367569471146940315417770465256727299767064856210780357684301199981462931952006488333486808362544845154245926747293050724822708968518810685854685147327673515845866702399347238662638091232*y^17 + 3237212062093858496230948901675554066235791200442446149474191117682922731739842290823598854503417700875970887348929280491496519170432697886888983776088844143678443847700106327864506844765899767828436431951447058578489705955002303915013147355244398990632869272653/864077935366015521125531602626304120284490082022308849987224887784690265147973091946683769713610654078545456235441553513173772355268824998841433247000405520842925522659052822140370421705815670301419310532425667865917821707979594740366668899959202416414880702*y^16 - 3075586160120956041476256120306626700236746349043537146292305951481334863283977939947672951640703861812241894680947524899539696362512497999683421559023465459295824395704767603026241435607207466548933421213448948110440879083793350386188532807467973827025827324445/3072277103523610741779667920449081316567075847190431466621244045456676498303904326921542292315060103390383844392681079157951190596511377773658429322668108518552624080565521145387983721620677938849490881893069041301041143850594114632414822755410497480586242496*y^15 - 4706563616927908028675734762398242838294745643424524975476026216844304339864987507707951060252162939434868951367807617774942870838263452154784138475890886640451597932230524807195695241642863357679407645364368832587445562890094549947316436426018896223497305362343/2048184735682407161186445280299387544378050564793620977747496030304450998869269551281028194876706735593589229595120719438634127064340918515772286215112072345701749387043680763591989147747118625899660587928712694200694095900396076421609881836940331653724161664*y^14 - 126986780628988962697661190104882411093960921934475852648581135671041244555877212861374018481055528365398637274325064119510857256163996256459329089106403527872383275804151873725510305070921043647277571425117163232453072440014854623317085887770384574102365944901/48004329742556417840307311257016895571360560112350491665956938210260570285998505108149098317422814115474747568635641861842987353070490277713412958166689195602384751258836267896687245650323092794523295029579203770328767872665533041131481605553289023134160039*y^13 + 28671614885017771466606434505015748198722103793800704538062595856556778362301925522303315558852631348982894259306953860480769319884688849370462565360727807791036536268507371514966360904106752927352038317147629633174391020940842695575561169723393232206401344675803/18433662621141664450678007522694487899402455083142588799727464272740058989823425961529253753890360620342303066356086474947707143579068266641950575936008651111315744483393126872327902329724067633096945291358414247806246863103564687794488936532462984883517454976*y^12 + 85574113766714106845646634352695380466481360858378849878539317570861637033197167624474881850622778584747819774704302201077709542603813849272244459716106439067830225322151118105141989248781219017121981449949683023070298749295024018329220554793120417005806056191685/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^11 + 2236435291228656744898334340897875044981246442987417514179541628636603253591994369778055489969548684374022614746933071558075456303192129379481746112476480500929114601719545036964673949214139253853100510158348075123489903796268337710846847170941209828899060092481/6912623482928124169004252821010432962275920656178470799897799102277522121183784735573470157708885232628363649883532428105390178842150599990731465976003244166743404181272422577122963373646525362411354484259405342927342573663836757922933351199673619331319045616*y^10 - 41118165871618171490819884384467945367279521614748610559579031432294423267364678071190054390100296188481033304088265238928680840791652880148954593015463223770443936720168727103416118328810456079506693951318448521013422110293573618674818580489582891341709713323351/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^9 - 9738657707770369930815494834783740541668273585391903987529048234897614549217588290403756348916398668027708494502769620834788661827476661249993756876121759474094150190018980722738499418822911284212881046865740113255296063196068863952486437527919723976075935208557/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^8 + 1705406649877497054103844059285406415016651016509372130862047382922653459560889781712457621190935429355737922611590913441492711332886844749032903017634398501987325487583724991751469150629746600842078092424112282960518103315460378329799508883149565027845740836923/13825246965856248338008505642020865924551841312356941599795598204555044242367569471146940315417770465256727299767064856210780357684301199981462931952006488333486808362544845154245926747293050724822708968518810685854685147327673515845866702399347238662638091232*y^7 + 230352776169126556513078617350428255130655738967113358516443766182530369379711936281770171727749522566496333385670603678559341802144227605144191802719026985207256403012980763815385796287868968303128010981115088921610214106554943506588468225359240569395573928329/5027362533038635759275820233462133063473396840857069672652944801656379724497297989507978296515552896456991745369841765894829220976109527265986520709820541212177021222743580056089427908106563899935530534006840249401703689937335823943951528145217177695504760448*y^6 - 507894837955359134106128662832173022486977908579032213561714838319139865371218060058582602620343125717936397326730028828554031193281470665932266215826476414503348319478450430455870796574306909249259446348099705922109612954746859016391019089477229989490906614199/27650493931712496676017011284041731849103682624713883199591196409110088484735138942293880630835540930513454599534129712421560715368602399962925863904012976666973616725089690308491853494586101449645417937037621371709370294655347031691733404798694477325276182464*y^5 - 269931015879143060555945633012068713102506279194432220022412931674223800349758978091963030868690406913086116629418219722275944946120930585762131702426300876186711417827372082893345159604364332242919836682235030986240868376052458725794300961652132336448224115395/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928*y^4 + 21292979327898343950174696309406973220172390278966371252006485979926247516755515749827533149107335503577897273150881742300847711300667952108945897620508997662540432954140262515297178827719453948622414466004699707484889644275576714912870962811836700160038939733/13825246965856248338008505642020865924551841312356941599795598204555044242367569471146940315417770465256727299767064856210780357684301199981462931952006488333486808362544845154245926747293050724822708968518810685854685147327673515845866702399347238662638091232*y^3 + 16470990218151031470392395007866141015139948319106027171527359289183113162774591174295887139107740980479766901770103469637535649096506969666808025240913703398615322062706963644647907355197407062939641855819112633459451008722259987508440171191446195231273853565/27650493931712496676017011284041731849103682624713883199591196409110088484735138942293880630835540930513454599534129712421560715368602399962925863904012976666973616725089690308491853494586101449645417937037621371709370294655347031691733404798694477325276182464*y^2 + 51991535872439725869617149202705779578661449948607035391281040376069745948769391844070778304367510793497108634722054553709051469236386162979785128961607840011453160900204865302373858794890603226133019657684352522318110213415343406444759194336665025699626527/3456311741464062084502126410505216481137960328089235399948899551138761060591892367786735078854442616314181824941766214052695089421075299995365732988001622083371702090636211288561481686823262681205677242129702671463671286831918378961466675599836809665659522808*y + 776248790736039865754043168609610333449403066294366917355708366833977998230766725371000284997601286445695202119510312055612678815847125024437198908094210134513251544422458084931596001861442404524375783518241634805184807337298487171412473462498345978163756715/55300987863424993352034022568083463698207365249427766399182392818220176969470277884587761261671081861026909199068259424843121430737204799925851727808025953333947233450179380616983706989172202899290835874075242743418740589310694063383466809597388954650552364928

# 4 Loop Invariant
-1058528640052274647249335403229033680800586472157700424788590869161984732065353075793942803647683613169051650340063458746132008144108161834841378692313752581969572022116112004549973467556985237070879707771481488921057256650613721627150674391294210377234868004658947766249636716312989197868842074566097913417001478086610485772107193827301470633520068837390533953968192113/674737093079285966393603469900370575230182684735366743746448367704833537706912236638461629432741584771057554353657249915333188429829429693869986260268653232515547776735840732994627676710820942759710344096727262449483153765571155512996827460855286604214057176182777882166004151314985339525731846668977650376582327838633803475189004108488960466574006544169340162928287697920*y^29 - 13790249239883272368835675851485520705307665031974728969106433437312305413930011770481709416382103713284427515654060558556606420155738880231366244612965102628014274484774944802673526579137673457749745936633044666095864346259323892524961553836038442290627939929544048373572635282090247938015946617778936135022878080624690775935654269036438054588213732572527900733516214643/269894837231714386557441387960148230092073073894146697498579347081933415082764894655384651773096633908423021741462899966133275371931771877547994504107461293006219110694336293197851070684328377103884137638690904979793261506228462205198730984342114641685622870473111152866401660525994135810292738667591060150632931135453521390075601643395584186629602617667736065171315079168*y^28 - 198146512545692495222739122198516994844802139835409130027681899317356904426376510714047809857961052023999750698321673930605079711768432763299303725480949491520161786725764084560185602930329861595182760954182279133820630362914088817021136022011012287569596820904798467690512498445521805690899813217752122226786877319994213575564057885605236402100424914922351512033197945159/337368546539642983196801734950185287615091342367683371873224183852416768853456118319230814716370792385528777176828624957666594214914714846934993130134326616257773888367920366497313838355410471379855172048363631224741576882785577756498413730427643302107028588091388941083002075657492669762865923334488825188291163919316901737594502054244480233287003272084670081464143848960*y^27 - 4041368789834090396737351839213924454292482361338863779563349848077954424863632730030781990421272446241747430469157961740604231606115778431388044790470286733088656318980435308108723611155082757784702823931328349270906403129174518822875343292205113963149981542702075387880553504103265363175546238698100078701940666660071768416088548569451132217077791027110514539732377521969/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^26 - 10183769053700773298497353768371166581979150420370639607512559964571636235212924987013996612492845293460457510208291515528247100497388359886419996487881749416324543225726987845793835053851108843137403421422159072228109819233741850963204118680316214681932933634039916044957572314711118903754688110269832015425921616192213244464561914079607622414895129893279734254832215641629/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^25 - 208961752661235650148992861980562471829739136045623865101156327972063477636115778080938577386814626853382208630014260139308224174349695341856999217258652929814098023946783699829069807683461527449784691806627668404755060418909032097159092748705023151019372750099467858046725760438761275095638744038875952379928776588885076901298497378140166490738198919749111691688953759759/22491236435976198879786782330012352507672756157845558124881612256827784590230407887948720981091386159035251811788574997177772947660980989795666208675621774417184925891194691099820922557027364758657011469890908748316105125519038517099894248695176220140468572539425929405533471710499511317524394888965921679219410927954460115839633470282965348885800218138978005430942923264*y^24 - 21666451584930045494433114026803880166665564890322505145090904380873001180702960465754171213788838757669218669225617365425520612318760324760208062335324820957921643267853822658229869745503840490900610133978665253558634665161595793031986389021836435749037162360118491844624863925935507855394360481923032027146291589155977808370420113998073570067786318801813060031572654693/2499026270664022097754086925556928056408084017538395347209068028536420510025600876438746775676820684337250201309841666353085883073442332199518467630624641601909436210132743455535658061891929417628556829987878749812900569502115390788877138743908468904496508059936214378392607967833279035280488320996213519913267880883828901759959274475885038765088913126553111714549213696*y^23 - 85447036934405737068050759792953979852308613402393381762922923284793401718641824889716733644038035631440741771659753408513690838694651285924326714694658811631130141105165322977046432899533954840315374602098902968593865363978919585977867660258737829455064136648007575015004294121167688543056576285334518419511088036474219868623047678982116772357976289759758294833855387734017/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^22 - 2337196941067840160970661842213911546697310951454347286645837711454124278802628925633378167295386435682574255242502659723323070560819701022634389574097305439045673587839346588205901332862318881155874002460358062560048204609529452512804218726705750936634606344626617938904743051430572669376157018626970410818420641231665138307038723252096158379974520749816508480820777896029/74970788119920662932622607766707841692242520526151860416272040856092615300768026293162403270304620530117506039295249990592576492203269965985554028918739248057283086303982303666069741856757882528856704899636362494387017085063461723666314162317254067134895241798086431351778239034998371058414649629886405597398036426514867052798778234276551162952667393796593351436476410880*y^21 + 58710169316361988907637428999519410064194660685652652441282061779624711101671546925452072434884960464047866036007103844483794118775159183839723525918342284532263932883958063393605291799040180177222723386613629323590894456868976669511965683254177517884180588877847616873954957835787565684321037550367552633152883082986166935727909024658277674440337520556924455879334579596721/337368546539642983196801734950185287615091342367683371873224183852416768853456118319230814716370792385528777176828624957666594214914714846934993130134326616257773888367920366497313838355410471379855172048363631224741576882785577756498413730427643302107028588091388941083002075657492669762865923334488825188291163919316901737594502054244480233287003272084670081464143848960*y^20 + 1344971724674420262660215995685882676880650242801756661974596661717935697835094466149092769059644755447572462003266699515359179668876095776230348419371377363713969065579615717994742375599002012505152070609068225801574348465128333744305734017851151320577056811185164284132455947153932096855331312082469208902075361154803267992268406347824956414317360843074555452870192835708107/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^19 - 1720026950640200112514305953375461693826258022979632130266865555826757393365096943660586629596936741961025517621120825269851155553210299696746855359002765223015488067466945919778665691346411112070154377881575890153962876297696282060001531839276448459801888503178904586718405612861427507710595984283085179644307026794125188304531865929794098082660129791106927739527058770939/89964945743904795519147129320049410030691024631382232499526449027311138360921631551794883924365544636141007247154299988711091790643923959182664834702487097668739703564778764399283690228109459034628045879563634993264420502076154068399576994780704880561874290157703717622133886841998045270097579555863686716877643711817840463358533881131861395543200872555912021723771693056*y^18 - 28707940407343857066151354673644642452250261018065151784393446665424330333925235379408237816785805426211312741213143897757644737212013608766410210146845053978928453806172054010794581925631151109266113777017305043527118248463961110698851111326721600399676204769731691434771969003549255690372597067721541641273328373843969163901703478303938474617389435594656628897319710935971/28114045544970248599733477912515440634590945197306947656102015321034730737788009859935901226364232698794064764735718746472216184576226237244582760844527218021481157363993363874776153196284205948321264337363635935395131406898798146374867810868970275175585715674282411756916839638124389146905493611207402099024263659943075144799541837853706686107250272673722506788678654080*y^17 - 1843890467939885343190238893102968390962907427587616023633878993080554623271142861292050871959915983476557638762250403050184972936850790546227365367685670344426253358655603635359281191095809715690514198941453725967685300292416123799658980546773094522250531332576648176785208373009814609219370430422962487833868443819179915147398711133110302160143850942218704187863673387374807/674737093079285966393603469900370575230182684735366743746448367704833537706912236638461629432741584771057554353657249915333188429829429693869986260268653232515547776735840732994627676710820942759710344096727262449483153765571155512996827460855286604214057176182777882166004151314985339525731846668977650376582327838633803475189004108488960466574006544169340162928287697920*y^16 + 72502034566676726039404557181511244937080881449214302933486393026299750806242053242302794468100632613063671337717187564658241862591331697835614755942097307335536515626720532377807110477896316930723862014921771334109546118114495312167434866251517275282644080807062971475711659286824991799766037097305071370295510887222371014449313290866435195591052505820631451932172359754557/74970788119920662932622607766707841692242520526151860416272040856092615300768026293162403270304620530117506039295249990592576492203269965985554028918739248057283086303982303666069741856757882528856704899636362494387017085063461723666314162317254067134895241798086431351778239034998371058414649629886405597398036426514867052798778234276551162952667393796593351436476410880*y^15 + 370845761438793798309477470060102666639448266095969289116648899668024841930971838661508602185410503259651433364797495302062334955697557480147260734082252457140373002230894372678119648972620557991327867644397855856455644317813247667751261237346143054533703008541353691216983998827837457163508522755398789597839232727532667371541637286309582190890253780142649232700562436958593/149941576239841325865245215533415683384485041052303720832544081712185230601536052586324806540609241060235012078590499981185152984406539931971108057837478496114566172607964607332139483713515765057713409799272724988774034170126923447332628324634508134269790483596172862703556478069996742116829299259772811194796072853029734105597556468553102325905334787593186702872952821760*y^14 + 39647319557398840325626624971364124456149568461026872845228244627835985771343745152214237211991331230496345998605447617979289268359433306477036740737485921659344634171051428295120317421541861392203745677395984677462827392431421752608629955797886488775914127288434954234768997128107047804203298832652968785921334250696235131791265854449836797309114882809250652845102843292889/22491236435976198879786782330012352507672756157845558124881612256827784590230407887948720981091386159035251811788574997177772947660980989795666208675621774417184925891194691099820922557027364758657011469890908748316105125519038517099894248695176220140468572539425929405533471710499511317524394888965921679219410927954460115839633470282965348885800218138978005430942923264*y^13 - 2169924046802452149452897456216849098838067475739505970826265689509612915629525172242988140126263931406790802659723685840622251454129470609624163520685068737682821285379279963613048398145002847804317282500217838618515355881333971176742235505472932759951837400082052682722507316508547713661035026789874735401458694569945898075720529899278956260655076511556017315629957337078061/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^12 - 784012417421844134130026324118776149185490121576915113537628991292532143085790872106276616586434021465699807117688175323202860797407058469998322522986612324923834939463401770439651215389764050337511778804486835427044786717189315962405236599323987317351503449557601184869333375650912721080917617654486191975593504075099740940339645594728711499968046743034939069157841501484313/449824728719523977595735646600247050153455123156911162497632245136555691804608157758974419621827723180705036235771499943555458953219619795913324173512435488343698517823893821996418451140547295173140229397818174966322102510380770341997884973903524402809371450788518588110669434209990226350487897779318433584388218559089202316792669405659306977716004362779560108618858465280*y^11 + 2945819379509985463572784757334971337137014131301629997295685593302410845981002339268770313437081758363087657535283313703858836371642258454674145367423916411689537522078644400036742933602866690230934728485264317397263920291471273600981262198112260375290274356351705503206441885304024237887668786644309425431215783597129270247228748431893765774229883153195616234449788049859/224912364359761988797867823300123525076727561578455581248816122568277845902304078879487209810913861590352518117885749971777729476609809897956662086756217744171849258911946910998209225570273647586570114698909087483161051255190385170998942486951762201404685725394259294055334717104995113175243948889659216792194109279544601158396334702829653488858002181389780054309429232640*y^10 + 1165186844758862917268860734864732234429441702923315327530951678101273717684196312682591723634643689409882784340095305577084230896753697497748048328533756091354470619906153056289638016282836450224140655730357688394728387803352155412400502534833912314576144641707508972687426711690842185337846757359061438837918676247681005473341618678444643123582997297274506452284169343137049/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^9 + 353280946149034950736955621917230978923691309682332520259898308921552249234532105940352442559586223710042315510120415827020274896307939248809686109802043995639129461331346640296076869809425574356646950161548172225744364638995297920449027655037611960032882489712960096173155584232692605851074807235835092615033758573313246910135838580733901744409185381977188181297990987997293/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^8 - 70360614979819701290484438424665864411590895164679924323416037824787325392149437515431353511835547852529744151765755130168918022822171918060657732548488931465214310832577328722468112298665793254839307231733268894579328239109058755656071800430962670695525635145736672775547926788148630892023088537565299390628966533613632043178759105666388950138099828601416889079326052208019/337368546539642983196801734950185287615091342367683371873224183852416768853456118319230814716370792385528777176828624957666594214914714846934993130134326616257773888367920366497313838355410471379855172048363631224741576882785577756498413730427643302107028588091388941083002075657492669762865923334488825188291163919316901737594502054244480233287003272084670081464143848960*y^7 - 2085969595249997061155858353081212853603215532482364818946414233324163496018373474929252589080305818681009484213310380524507101341460067558107314639341466564272666117032915562964646997852527873109063537157417747806019378505757818560114427398535399837664526524569296493996358958169971350294304867855461718455554347946080262705616548791450932113433569872509478038614034313519/24535894293792216959767398905468020917461188535831517954416304280175765007524081332307695615736057628038456521951172724193934124721070170686181318555223753909656282790394208472531915516757125191262194330790082270890296500566223836836248271303828603789602079133919195715127423684181285073662976242508278195512084648677592853643236513035962198784509328878885096833755916288*y^6 + 318329821430393681492439233569435732577076914488733999769005901778876380924273842451537844791130892661257671603329509438272325505949615220339371796627367246118892745450898875631650162683028470387568113822831994625377588798414469189803500787730516098435277765371063264775164576530007331700921352410661009454079424107020478247622232330122116610237833745908659962814160029383/18742697029980165733155651941676960423060630131537965104068010214023153825192006573290600817576155132529376509823812497648144123050817491496388507229684812014320771575995575916517435464189470632214176224909090623596754271265865430916578540579313516783723810449521607837944559758749592764603662407471601399349509106628716763199694558569137790738166848449148337859119102720*y^5 + 15051274245986688838207426038078889219354214258059945330365964423197197953558697761634896435967239598545438789616820555615384510830546953619169216936203987648073986693219742028033959985023587698464196829875044758670307806442883862435191690738641723570617153351751245276565987431552716536647591516584727048119050270835228374435639089005051382170975080110907932535984320102019/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840*y^4 + 3617236534232006321449798782963135079322914021560277769897686960794891686179352021763476834708717631147924584416790487664192289601206211646211190212755669957380027914970613484507817430012870982765870295591247146503992891041064498312658061793245495330153219490425476594765760263755952348143121313430068286373711445360562512934566712709691483298574883484120144313634389849/168684273269821491598400867475092643807545671183841685936612091926208384426728059159615407358185396192764388588414312478833297107457357423467496565067163308128886944183960183248656919177705235689927586024181815612370788441392788878249206865213821651053514294045694470541501037828746334881432961667244412594145581959658450868797251027122240116643501636042335040732071924480*y^3 - 1244608794245301885071975366832939436092251882766931057883959020651451167541027502433094500246852905196096924254206294646059823070428520836908700890463910287265191727172360026683256181136624755991164554822027215646934628248233017097678024558156052384740553388811783093613949985628299652970498436933205555767763340612029249368317613034670801326957603410174619899554225713/3514255693121281074966684739064430079323868149663368457012751915129341342223501232491987653295529087349258095591964843309027023072028279655572845105565902252685144670499170484347019149535525743540158042170454491924391425862349768296858476358621284396948214459285301469614604954765548643363186701400925262378032957492884393099942729731713335763406284084215313348584831760*y^2 - 3633543291872693892040306421783271078138476999816313411936592287314855988529959251139232500464585181948669795661016612345950486142421265460661058306026875773278627758669280565849548408168960236731748220760308153839982388388816804218277344467653939776856870876393232239456539827151281435802677531661537229439659771169448532052424800921530440697249170071296036349490439/263569176984096080622501355429832255949290111224752634275956393634700600666762592436899073997164681551194357169397363248177026730402120974167963382917442668951385850287437786326026436215164430765511853162784086894329356939676232622264385726896596329771116084446397610221095371607416148252239002605069394678352471811966329482495704729878500182255471306316148501143862382*y + 1200039200435077957196951267274672381531720850941956659924963459415944685913724788513937891276744382463286024679955429512611320704717240216448927949611788748662714509389998910065866352417007473823725148072443939058386888893306323325212774297719381044169614406163239520765816362873408367260352069531488693795057074992295229559723479962791516120126432099771943069101095917/1349474186158571932787206939800741150460365369470733487492896735409667075413824473276923258865483169542115108707314499830666376859658859387739972520537306465031095553471681465989255353421641885519420688193454524898966307531142311025993654921710573208428114352365555764332008302629970679051463693337955300753164655677267606950378008216977920933148013088338680325856575395840