# Manifold: Census Knot K8_3

# Number of Tetrahedra: 8

# Number Field
x^27 - 11*x^26 - 183*x^25 - 109*x^24 + 4471*x^23 + 5211*x^22 - 31576*x^21 - 29228*x^20 + 132366*x^19 + 65865*x^18 - 424386*x^17 - 140810*x^16 + 816816*x^15 + 193152*x^14 - 1073043*x^13 - 471545*x^12 + 614323*x^11 + 462210*x^10 - 92887*x^9 - 183273*x^8 - 31455*x^7 + 26703*x^6 + 11066*x^5 + 198*x^4 - 783*x^3 - 219*x^2 - 25*x - 1 

# Approximate Field Generator
-0.133187735033272 - 0.175553006495253*I

# Shape Parameters
-3860720804568172017461398953235129053387225938960723648525917883527768899372154/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^26 + 43258808811808578863349345729131407709581520987494087551315691891252393720860770/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^25 + 697634339967578465182386338667414926746786885317284176991637241330749528777763214/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^24 + 278075676266835112687655172758686647344395760364077754078775386215081974962525946/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^23 - 17315290538979797127244169897349210999593497817347705443147774800811527856007654372/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^22 - 16568431428729193932988863406166307828279466562188815984618600111555545703951722733/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 + 125230502914317120876016992690461773566211167114690246870552655749729654026849951851/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 + 87082702840142299532896098369839804762018018682677940432486115583164924107767123947/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 - 528408974988996904337998845587398431229796053666170683984365870054734833902806895778/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^18 - 145443802736600049848464351224153870826597697893030965497052767976342675344331853061/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^17 + 1666382575734285727690782585782899930535006810518562442341833313674427119253597697333/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^16 + 200707258766818451358155319152545393770429127648612052128961204158948155691781742403/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^15 - 3188628655013574057509295617599790158665054050034888171850336113314516034858224586467/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^14 - 88558265432484861907388404313206225332254072581121749733021876569674470105513671968/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^13 + 4149973609991261497876507866874047800395088881507254203745573148203451241510927286676/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 + 964320671480794114330046183888169543056026638666304747222509714579137039979890221338/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^11 - 2555657865695093087414435503539458220109236796683613811400342491333088921465172684291/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^10 - 1249839932897211085203745461976718915069526866549755053649402616090733966521933389080/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 + 610285684630352071539616444664274490312743910496032698625595699636363677957634392837/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^8 + 575226876599631887079276315023500350705804931829214154696395186906749737771102176466/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 + 2119133413201382814922715434298253396659597844073518492228098704566710895675284402/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^6 - 102037619334828531166254575743712041635750274228777851634239230496847188429073756847/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 - 21017279149800484065201073805643858942074474121258866826508575257848014699870291018/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^4 + 3569882881145603024456347856250801832467896522479495487316330055388005161085983785/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 + 2224725686071533783283722488877366949153859230689479000001019804136008639359820353/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^2 + 367959274282481307528474475400068423049047359961806385555400705852076137938657033/186756365819839005347125749826273722843923052085505580269990761050408600899003*y + 18605701182415128634962139479115121988124863290171676758501716997791950550401859/186756365819839005347125749826273722843923052085505580269990761050408600899003

1907435766105646777017938420513949080727178543370403143975011211389807469513251/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^26 - 21416736759670022747078149325922596044841369905900277747743132491767529768148816/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^25 - 344193664180552429680893126296964783106274428286547637233930982168468367629582622/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^24 - 129249682669093178682810233208849567008995912149976883843209380560947965755172700/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^23 + 8560685650560807766614335818279449739317275790977120294178420328708729099792659019/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^22 + 7990384670727401085597810162029718619904008416514429942980325816851358149499080493/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 - 62123572249749896730687004675114815835071819683037813373045805290292976444510092397/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 - 41693162100919620788656402309016035651824260702551150182756841732111456707688866504/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 + 262463185644889811332289133810533041235904190481479312051689979199916593899059544947/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^18 + 66403227270704291665742546148685968395362310501792261630573041793096861092531249199/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^17 - 826553289351701823813439138723715606610165323497606491017633253597179918710063424103/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^16 - 81724787594033310294264200849496326090859015373306235533861769716421050989228082883/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^15 + 1582888090249085356670264728934013271080862006207130793311597972972451134023841723754/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^14 + 11571340099251554722000896840710398811555850035384017999270361828643989327734482446/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^13 - 2060748422511642438582444882847612064496725311632572647637798676666744167285525142742/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 - 435796103585698412693067093566464599925310748704397021455903686495315046053977430941/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^11 + 1285368242732532765148206448593433813655290077022608543474789554836956284880397132990/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^10 + 600021014003179484056191673108714649661243650987552702568225402565270225816695925448/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 - 318628466937980644948773405182838626566455290271901494257630329444201373164041261985/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^8 - 284550818439875147366703322498911465501709014505151827141375513837458638997266198188/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 + 3386677923850443888215246855806467165441269278932474461674357333236707658047629387/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^6 + 51734328023414629771485366384579291632697640317468598119970399913860442772075454262/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 + 10145581339747651484664259983572831052342703102454557565673757684977962581067512615/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^4 - 1909790246229879262028231827532556273859125499516136189061212115638410746224827605/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 - 1128243494099611577223166696253584948510934898389577097285302622490245184385427254/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^2 - 183128788371520122333955177943386676046607350536723187393198867031503331349823397/186756365819839005347125749826273722843923052085505580269990761050408600899003*y - 8695763038142810235242176072381185466711431244943308014104573831389763492594807/186756365819839005347125749826273722843923052085505580269990761050408600899003

-864318352273794022023033112285226894194980139790741640255372934148822290196270/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^26 + 9675705764499241025061180601137762499548178794136583039183264990158201615369331/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^25 + 156274003926378321685250913445604437539340996937443996417991449047629551358916361/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^24 + 63939805267161567839362900472068667971538582135756581098085326905929563858520044/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^23 - 3874332552832168450126343727913982853634999614372444812968722338766547975684952244/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^22 - 3747649898583535937201300891689141593978185774552425146743718092149712533293014993/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 + 27962775697837790799379915839060634707121082591830011790604746020405649791402311993/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 + 19731094231952135350820873289212238866682093641281196967019080673718049356758660543/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 - 117864913068516048713857044336092467864584398291827974419492327127241050528227747608/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^18 - 33478865801521279294408724969427310914306615810995701544919198228854259034183248617/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^17 + 371784995114165793331715518543619906193808195601574110675624103494388983742357519413/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^16 + 47996516827647477144051803184729136009502553192959708352975356912071669680634041541/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^15 - 710342916487021031070804210289505898965987326807976861907354679457492548263533845031/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^14 - 25239852732417451952411128329347653587374544033138099992035438437463914009429846416/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^13 + 923294660527352356440593237501556146149738900983887537456152983399864020877149453402/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 + 222533935045813385197727953404858079236999518235282051777995567974736475877843116442/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^11 - 562928119162109518261652700099908253281829295287570274075060990165541425906963900767/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^10 - 280319890460490275761488497272418726495121424096507836881458857529031273064929224218/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 + 131338638301892201860714670556395297245050916149281986873504637080654717475021940976/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^8 + 126590224144596762526491466491990460293330073851770678485965556200416804786924866150/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 + 1199523918271793411643763591194816199054254573136168093468811299139724629076352572/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^6 - 22073236384169782847138078952378696759599112591882122695233379145646674046946688403/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 - 4575405020975643088015512136962239503628473924675911879397485475886676216133599453/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^4 + 750482213671817048051722007931446710610988316368122904007864762712886856195303845/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 + 475736140348748623383901007877544496155877613243342484532813499135697497437154518/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^2 + 78452852743522329241733744947097524730490387016471878441344621968558451189010574/186756365819839005347125749826273722843923052085505580269990761050408600899003*y + 3881703845345264711340194636786608319722905051224296822537146862754753255349835/186756365819839005347125749826273722843923052085505580269990761050408600899003

-57144057355693804523615481525660619766655536610778894865845499686243829685535743/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^26 + 319573388345145991259417477713471414867048750592124518078764557438772297151366971/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^25 + 10337883746346081664607053681843247215621515156640052521560851615298198322429540431/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^24 + 2166103620579152351850429751992198569023968386373704851095755961808737991191962537/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^23 - 256041134344193259897588286424042885986826800521022152195928497042367990428269330039/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^22 - 62553849769519334996208479795516835632894526978236941270194557847000464830853119159/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^21 + 461184600480129706881148357773046234590854719787880571097955911565044492597856825655/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^20 + 82510624830942329492920147797609473835358730710781663845086809044373394923122176466/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 - 3884724543719558239682067468632047111870237731786616872758555649137569308914648955217/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^18 - 2275845756302922003683803427529041371989453142618139805865236876048419417835158450377/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^17 + 24516967759701808608677101257714344535503185369179121615943373382079636446449012563637/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^16 + 3377417192561112856195477266178812968722345808970641053050615172107560996105729121451/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^15 - 46797414047518703530851874590780808221319838677097996684268958569577363379102025304693/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^14 - 2035821710414576807931559415849429389581924012073024145939779361486872498835396576821/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^13 + 7597636930486002784688403206399882370424953459628499592831127884761350188741741919989/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^12 + 15168781855294482996706295160719157038193309330091340488547376040386945010270665735567/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^11 - 18383541905766371406899293072638268681988369272927534171450993550675156487041639791031/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^10 - 4660410201934878771446033648859270362429343221714576664748699361562123437412804829215/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^9 + 8408792900726048574714549729146760882504623158222496977854678815041798153119919074269/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^8 + 2072562897956948024414898127414711314052856433433038021616716472042937257136398807061/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^7 + 125698890714961396275715248269277108138989091411234114145437759927272820939187068453/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^6 - 356710866851611689169953471994569411175320169114612234432428629741732013717316511899/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^5 - 149543447442676832086328608064517446950067055360903199976557499077285480374908371873/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^4 + 11879362308270083981920945789031611430153515394965725880457149695487049631023614829/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^3 + 30586691347291477810600961976042465845076361236684226051353359879193074745015832341/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^2 + 2506752036629970318324710116785053665628434368269903465760951326599484618320774805/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y + 228494242547205989385774715666423421532625752651484110678965896863553001866509665/2988101853117424085554011997220379565502768833368089284319852176806537614384048

2155152843964071453583663640796244402976331258484907729085368412405453772953311/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^26 - 24278457272366153862016549632274653989000860210096109961051878398716928352729614/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^25 - 388054253545690389009160990156147645075474373861634118164225239732137551453827586/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^24 - 130865258696314754186105219119185981329819656600037317621537270125720693335933756/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^23 + 9689521422401403304641924250680068149275399971258428237622175571925656292381603559/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^22 + 8677588651424493666380839136127890069003819623358056628567058376856316523863941464/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^21 - 70802854985596411241218880527884940401555934509141545401294390712067764863836608223/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^20 - 44889476312465990603899067601339301490956077248576756453284246313847894642395079199/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^19 + 300118892597627127346621049641120647442113116497516239596903937332669034457332098118/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^18 + 66212201847085083449725315945566181923495331076441126942484142510571474268247766571/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^17 - 944011114657322288594495984053944764137841262747560333378301520364371046506106232979/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^16 - 63181482500150467426410840412411847019128026980060562096249104036580329437770336993/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^15 + 363094893922418648348721805122655291000708853402854401091658062900574189730127060448/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^14 - 39515439060757735484715380781006957209696382037895525459275459874471977952761507363/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^13 - 2371498313626299445024515663791724925951903274103330219263988114394557229480967922214/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^12 - 426468276614878720906402750806136789264416528985189060853924530770501519980918263803/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^11 + 1523755462431638882441512831107732365863925337958453623378748976761152258307999778642/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^10 + 663662755307316277544579092524223177049102453003014269263896714306848962065711631759/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^9 - 402518800434966606809413333042696049716843918596861425924915248555522964590190416794/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^8 - 333917032059200941439217403498679232490877997028104204719491818500365141712136379501/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^7 + 11376733928647068177774087885447451789381967844484321510937778311960474086543969418/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^6 + 63675473426536872188331622678463719844097927914456431699298065642771692130819960044/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^5 + 11850760507883018857479195085859597706039761482918255480294744343314675061694194859/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^4 - 2564378462564365372507964909601237124450082506605808400976511521963473178505120834/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^3 - 1411235376797327719198813620041989532859430335937699747127476655718525216171168451/933781829099195026735628749131368614219615260427527901349953805252043004495015*y^2 - 228062529500642613394662509660733022865099350632381922866418782760882478250013426/933781829099195026735628749131368614219615260427527901349953805252043004495015*y - 9758894830455270981624564430055392055042250654336581432454435296081701961083402/933781829099195026735628749131368614219615260427527901349953805252043004495015

10562145777660132759064658644676012300886598465681192633228618328862467761840769/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^26 - 59739374872942281607289718676323100838224021566242619444437413642211255011750269/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^25 - 1896495010612319989373227982312610416517516717827489838185647542183101453339470913/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^24 - 275026953443129936251734261407127505054948167114856625366633972585913952119511543/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^23 + 47562283802443075387726355048150147072463893365821056065142667477014737167914280137/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^22 + 10089411714282813971727746609481302152875913782391975026971537041835701060237670413/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^21 - 87509127774285311682377732317564253293517083171834729404385830029890083819720968237/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^20 - 12844924468459396861953006852406289231709294034429659231537867925361741104604609531/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 + 743973790714925215632065131579297674470656888125406052236838480393015212201326631159/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^18 + 265829834748337682118021514965336755211308809077109539406665152233362541523240734839/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^17 - 4669037523694131758774818687449458900620420301193135133009089638712432661914558850379/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^16 - 121233694470312895090371432916803425999329884828022895528500897858423390681461850405/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^15 + 9001667255952392923413818071794970639587126195372140955188010593910495692585203255115/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^14 - 536935293237724809926701491540389452871729294412020940882429441735336227322394916037/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^13 - 1472151583812019007172745884412309988709284460129799186370967513645362707349410774671/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^12 - 1662175064610857737437552687988128447065609328511545312231182197597944790175905335073/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^11 + 3885456971317859151538088560269256806314241345004903168473825481865133384650128227585/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^10 + 775213211281929538482369624168180723559822582264269442612721971421416886279890128557/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^9 - 2182711231922278538796987635993553510282834427535128312281236375825216369411596998595/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^8 - 417941858352096806253652430780094421655290203170204005964933108175881710454834931903/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^7 + 99074296162644905514290315201437884927722117659179891872957859154840929223594897733/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^6 + 83317310953188494171417925608481381109419014353268212658082825343350814637580447073/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^5 + 29415986294753854611679824249103624217205928914398562352633003859912238400915268215/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y^4 - 3539276390554192782847490014637449858053730982388912157150916593783960974689663607/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^3 - 7501044487637002554022370220549568397640693781220771044098261778088429464490778107/2988101853117424085554011997220379565502768833368089284319852176806537614384048*y^2 - 600053595672569561852306161237546036316881331308994130483585797646271370135941955/1494050926558712042777005998610189782751384416684044642159926088403268807192024*y - 57144057355693804523615481525660619766655536610778894865845499686243829685535743/2988101853117424085554011997220379565502768833368089284319852176806537614384048

-13405136936073735685040488398946882606775326341820787515546043186252724609671559/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^26 + 75174667030976194122749011697653799582528436302044088861088791058339645264709111/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^25 + 2420740727875588169402325245076232262001311054000953053752215260023606736276664563/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^24 + 469138267043772084660766653941829050977996651598185894313326070086309756745371235/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^23 - 60145468610851179806418516611398465280783970448699013060345995558763473184660564523/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^22 - 14220842628700778313116234386812279688542040913246768344872886031670090003765258616/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 + 108939392552229972896479741902024747274418598031572513043048534491025858835515345588/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 + 74522622409420997080195268412472475888852777313363469535364315921864746401680790078/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 - 920007672705308129303733321654438250846437239994567401476690834349203668114489774013/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^18 - 487704274888210867879789591860638496043663039221455296614028881320142061984644629049/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^17 + 5799410030891851717792260628319132020315418622146885276907023612481062371131187774693/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^16 + 641068126297859626842974070811696368037826521146760061524308711048005571010512935779/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^15 - 11104856350502864829593759934145729329303426215100630616341139172719253197565631870789/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^14 - 205820937031610954396133107325415766095319446649432992190002590456853120285214061869/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^13 + 3614836341816249781713738194769580112720350777951559228276589978752975740878060091863/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 + 3221195046113509735392196760009869987223641806423068693539833716470528059038925929151/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^11 - 4484163177106992104700268843764713864286974234641134407887418822829435716212022643473/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^10 - 1074091282741652613590942516112494154398631146497564500972180550818205697282745467944/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 + 2182336773099104256294446077127275413756165630632286850821122757694490242828581587409/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^8 + 502073857332362668445746528985394461637175561799552323792823392483572537882595525679/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 - 5738757960969294210470382607542257028599015140663660162906896430690329227029754723/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^6 - 90197941951186399518251833293455581853701308492438433749111394851216590914468279237/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 - 36582107541831635804603149498418184955321398769477590450713537409363666772950623859/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^4 + 3225641270163339554060073342267528169829597960623617568501687570780159603315522726/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 + 7914624176833204969599042847365006373311382413879593683738167461267033365086897101/747025463279356021388502999305094891375692208342022321079963044201634403596012*y^2 + 652013848829515671596301921372254137525819703036850912376598351924381672775877997/373512731639678010694251499652547445687846104171011160539981522100817201798006*y + 65629982616558624873964456975043308966036875878250308892467636271782337208850049/747025463279356021388502999305094891375692208342022321079963044201634403596012

9154024054259345205717750177644291466124943758563589265779918337669190184489832/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^26 - 102630139301144401990709984048743230500815897935902153829241693151605106239332959/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^25 - 1653475987900833715890501004449056595150783917937708710701289001317178526371263357/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^24 - 648183822663960469921520717395093747393833283564421027157964842626752067598230106/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^23 + 41063533380924763079769558046161983767205782144519738698093644539387271277051017442/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^22 + 39016625651297445815632802663705258423993668875741867450181284506157656539864144390/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 - 297270368039483507228604090651448497322445104458685675961283323437896989474699264033/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 - 204648425401359613373228294046392329235451053456653985289624796374285519985775642617/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 + 1254769928153015674069588036559344448750566143589140527512733569187937155093660804258/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^18 + 337351462868765347584773876433139459111500215138248333874867901335100149035555040262/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^17 - 3955404115112375510945272597641118530719108559115910704513207947464804322182886431821/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^16 - 451942577611412795859490488687894757464537401939177990711698947231770477144522462193/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^15 + 7570217904903703928012211077504754149771740463245468077811193620119375688033811979470/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^14 + 165839886560690689105041749569008506436727191148781829266587622239357600557668088824/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^13 - 9853076312350907905177646495436962033199611419246962920143033897106919732705887382024/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 - 2230846831288763851991542507695736079117720532272053872411750921838622549444995825408/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^11 + 6089375576946900513667568804800110207682710758407833764562953679562485417673915084653/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^10 + 2939436491258526819293927361495022937213919723689512388627397500153848987340528247180/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 - 1469467320394555449835733497842243447929161777562190677362121335153543397211406726076/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^8 - 1364125032056052701045415649761450434130651407330598285611893527711202593816028866017/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 + 716199353379288437346010583029388962068408309505069189550407664766996415673032306/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^6 + 243577528273310334633852203379169794888657023526239799915863079003310614126263284973/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 + 49549340749796613599923158456661794726263664802526067942449183587738874282545760047/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^4 - 8624798578363703913208141932364734380770078547267925790363324992148854350270948234/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 - 5315961816920990737793177222312178199312074953391370102268366993728378133289456019/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^2 - 877113043050122139767135874239559806735822686553129241108204023259127900403892259/186756365819839005347125749826273722843923052085505580269990761050408600899003*y - 43583639186226032378857134342222489408970743234852150194258022455917350611330790/186756365819839005347125749826273722843923052085505580269990761050408600899003


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

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

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

# f Combinatorial flattening
{8, 6, 4, -3, 3, -9, -4, 5}

# f' Combinatorial flattening
{-5, 0, 0, 0, 4, 0, 0, 0}

# 1 Loop Invariant
-362945676724197361872804846244927364312855894353586778462265604365175438758186813/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^26 + 2033107220508896066953605156706695753269134904751667032852339518118398676603353689/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^25 + 65590032000200942667786111275032271438601417823431736680572032761459915878297541343/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^24 + 13122234657930477466556063603589656820520490163271431099301425394700529265371132118/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^23 - 1627680671707644963105559475599425137603869174685807212368892607398420117730945749641/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^22 - 779980091436424212914977543878505768733654350815956137157444475817952170591114668658/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^21 + 5884222542525192783963152889512917869545610657091372789410006470719219393622219100446/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^20 + 4100839013457061237416039412973435246976765678281140378311319971048461941183450327196/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^19 - 24824271944414933081794517655299543165190786293464078029140014921060950215708948303420/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^18 - 13733887488322503594804570917223361312428118251965124156742216217742787024710634935367/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^17 + 156574142497911386210072564916998010037520708760041046646638616170350422554911784073375/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^16 + 19074780978431385936354658061787531747910539520373869922033585700293745764898436560549/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^15 - 299538490443467447409123798514524622069219114476338984783658377979936587866645305324593/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^14 - 8718662527296821197544000784856901580297574237371084547906746442315813407007827335373/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^13 + 194880905535970342905637754134563995065355892939558369146913550845049102851598527000942/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^12 + 91178713436122967378807728843693137486215466450360205928261012464739377421574474057797/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^11 - 119830596204926123971410505619666374038493720543864222824120935488431144877642697824589/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^10 - 58840468559437273956773304914470175142169186322239704122459556010753950527251141775966/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^9 + 56969876241010006116191825297671080378570969015291315401120561568272962696815359304265/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^8 + 27006355746832528252230781281583567031870377025662633772909803541131752124585772112296/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^7 + 305777709996960365778841046384332958715560029472792174263237288265609885188184530641/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^6 - 4773532699271378892236732458039169571794350577865667058821911392026930808535363472221/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^5 - 992458130666729822722884281018841783456039302419531851727971928535951921420816354292/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^4 + 164196521412387065886522583731049336079912867035588828377421639603769376141631950495/186756365819839005347125749826273722843923052085505580269990761050408600899003*y^3 + 209069516002371775561518045484254989361097457664806130836280383492306076452744237307/373512731639678010694251499652547445687846104171011160539981522100817201798006*y^2 + 17434631229349060482071072969873118062574827346205467258682442374527888219492681408/186756365819839005347125749826273722843923052085505580269990761050408600899003*y + 1775714209831683570745048669584478822037803336387126825260238722762495468994297653/373512731639678010694251499652547445687846104171011160539981522100817201798006

# 2 Loop Invariant
-2532595951375824842385484185376019838578731606331642949774166251426426909629126667473907938686489761394100327783233668791281151359405996512770035835211241476004960025669/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^26 + 14189082284946324198730688700221490836336435840124704579729980715495715745642688310420479908269464080280136836179453588265424401313692863839752002638226464856679761844339/1145913966729075321784695949891562862789916879427508559213497304140843059586445016041777689251050643376098028036846004561193852676496982327412358400352044321511111692004*y^25 + 457633229926617685802107947390142653412045971869438876685215924807326627288433981265328446952501221022462190117934029632039873322480249461195206340629709027760564658841049/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^24 + 91131431057543634406178018695579741806478682235538961976090697817753862145172029539109857966420611412388280144131777895559267956690937419799671179634635546394692814495471/1145913966729075321784695949891562862789916879427508559213497304140843059586445016041777689251050643376098028036846004561193852676496982327412358400352044321511111692004*y^23 - 473285804667537125160653173700716184218217086256390541088131648983310354393626100870300701020741283244966256725979161298019362547516719553828979911318116454608483336506865/95492830560756276815391329157630238565826406618959046601124775345070254965537084670148140770920886948008169003070500380099487723041415193951029866696003693459259307667*y^22 - 7243525632305041308321828724138473347699586880453759190787130895054138612550623231024192041767624884225234839755859155694660131235792271318456500829639414430185774515662229/1527885288972100429046261266522083817053222505903344745617996405521124079448593354722370252334734191168130704049128006081591803568662643103216477867136059095348148922672*y^21 + 27385545660494854384592606689025118818870481937521999436594213909528020936124823012129843226160914065420539684083246016394581977069865345701073249380397865757746903778356503/763942644486050214523130633261041908526611252951672372808998202760562039724296677361185126167367095584065352024564003040795901784331321551608238933568029547674074461336*y^20 + 114209480347717824298756089368122478275196926541723793153166844561193809534332788429668803079633670227056831540794574824258709697849318385040949016083138773758447629867634559/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^19 - 57778329352883547460451541719658728825270255796161580303651593885514379488693156350192262942052712888448897246961687324191079320266359322450620889358597490707933920200850159/381971322243025107261565316630520954263305626475836186404499101380281019862148338680592563083683547792032676012282001520397950892165660775804119466784014773837037230668*y^18 - 190662580540964215172150173041915116858092930752346327094902521932509454200876016351686777943214655416561551138079834592482104484131432021872630845629484728226883993665401119/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^17 + 728829541149143310402275431522688115293938707743150182255350649784975032670751732173778439233585513917566029253575719963797302023602355401910340733331403178962331680038400309/1527885288972100429046261266522083817053222505903344745617996405521124079448593354722370252334734191168130704049128006081591803568662643103216477867136059095348148922672*y^16 + 131404647460438459044685128661746571239883818438243035953395881165605456424904304846165917803039516356422707335741824261865052527744159671741451149816827396211178897282154659/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^15 - 1394683314240167212289902561613169917465961902894213852490636230591852176715625330118846099650283547754871655088235492508760078460696963132160703328351877442791398427646409133/1527885288972100429046261266522083817053222505903344745617996405521124079448593354722370252334734191168130704049128006081591803568662643103216477867136059095348148922672*y^14 - 115332375853631190033141591462040778396920630851601867649012376042960842845151752333078241495398209988704026049181000305007121085891729168468277835615450564999875438038309421/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^13 + 907622439532428530684111055054470326047812844799482269490004119961988747470684622021000124122077880700009699354596024671145188313240578985466547242256030426736243172237775653/763942644486050214523130633261041908526611252951672372808998202760562039724296677361185126167367095584065352024564003040795901784331321551608238933568029547674074461336*y^12 + 632111208874351851315248799416038570500194400083679256263081661851030995951839609048045024718972572265726499635508861973214263439246732217105108779043944351536874179803510965/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^11 - 3354668405843794067052883666820614941613190579067136596020484888953219129223470176400923350590495936604486394544952314024396193156648437018953123551613518677348872784840788973/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^10 - 820010909984297794999096679559263427181175245086769473066540973869866912074892490284526589937218694795061661821317461332579949996635984299630773450161367726500969911728649099/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^9 + 400813546244288955951530017001072234100542950834314106642877496663501147122070226061725991346672408011013653575919086147165028295510934634348010627972539686652900123868694141/2291827933458150643569391899783125725579833758855017118426994608281686119172890032083555378502101286752196056073692009122387705352993964654824716800704088643022223384008*y^8 + 251781510335536601407030150053136674661315046766738092873063985032162881465724345048125614381004906822531917561769707819220088087477024839565383173334248102148804433158200991/1527885288972100429046261266522083817053222505903344745617996405521124079448593354722370252334734191168130704049128006081591803568662643103216477867136059095348148922672*y^7 + 907720049387382669634332526414763685132899272520846892127597878032764720799944085996776489297324710429648877832574306999663503598559331955778204025052378621327559700175707/1527885288972100429046261266522083817053222505903344745617996405521124079448593354722370252334734191168130704049128006081591803568662643103216477867136059095348148922672*y^6 - 22348561987031430801306587299739310230584391533719211778867517242690560077638554069736963295881293901204303185537819623523805002114706839423978151717381969015639413813774065/763942644486050214523130633261041908526611252951672372808998202760562039724296677361185126167367095584065352024564003040795901784331321551608238933568029547674074461336*y^5 - 27647386669614365537251727805658453388573105957701510650187994743894409132111957989139619268351986991216396192337747915273532624976214106038300878963428442774195493063901841/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^4 + 4698167557310660958353888992310736547221297488322187631071642860717416311953378931629711190374352473681700205396001347984750622799392194400323023207632485091136074318685867/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^3 + 2932298029273253969894900324110758330845274158260099654890922329399284270785370305589849703873904963304709674545851859467216785348023743709916639004922486083503070250754633/4583655866916301287138783799566251451159667517710034236853989216563372238345780064167110757004202573504392112147384018244775410705987929309649433601408177286044446768016*y^2 + 60461016716548378562917147332073566023258007510713906776554522595998516589170537373345869123894460021184918380871717426315958331617425647025100477240414163079613535881025/572956983364537660892347974945781431394958439713754279606748652070421529793222508020888844625525321688049014018423002280596926338248491163706179200176022160755555846002*y + 3246064662308515609982618173722584243108602663035216958792930357405694163456726677821850645609428971798580229100937863357835933673932027978198351683566481333840128872061/381971322243025107261565316630520954263305626475836186404499101380281019862148338680592563083683547792032676012282001520397950892165660775804119466784014773837037230668

# 3 Loop Invariant
-856884586509004006853384893803222037822973775572473853605298329138230467933694242660005628521603410948970369561356206389371941648499052780166848911900915917288084213192000812837578967601441899725240218507242230199/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^26 + 2401582570945523325727729924621813032650497413743704158696982226313048180959285198265898622759492566851466767528601473588812872323824874295637464329995642192810816706736698121379671504518215677783425285921222591147/1092542715257172038171424269761043498757044379694332863740724718382311855370645101961406485438735990441717875162328450410581661879989169324258242065949423035639623495078808842439230647759381063595763326528020954224*y^25 + 154784868736289344965493524913343857539709618621546221986278044947795295373686629987794757581095261903584940482070982539036360082658987472883437450389353152798196710023570866947448132514006327511377416453189454814135/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^24 + 60781282017959455708572559998929360330145860177609095499260370537811663557183140747590409105726736469826618498909857996552286665222267278858723270430118407033975438081134006462744296441034875255314798397259745776321/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^23 - 1921938862369569469849049413943993634161740936007493630649808472939701398745842789547052765596923278361191776278578298945489932255938616373495030096515509631355573380766145689144857467330477927678722520389658592471741/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^22 - 3655037972940456002997512186441746139060589744416080220628479895438711045509133437976018942400033466859032524117452667445790543337243024560997860805524208067369727472074767672753639786411674386781305525382432445781085/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^21 + 6956448286502916566726530791262366365722238126004818636963085402629145637147312331829159606139035860195772820526638695714136278347015723574800332139954088455937623334068131983575741489802833358845236253071314750240899/1092542715257172038171424269761043498757044379694332863740724718382311855370645101961406485438735990441717875162328450410581661879989169324258242065949423035639623495078808842439230647759381063595763326528020954224*y^20 + 4794638675683781179155533678152984512766940856637807912861602585662867837055583469415288227903204731384716428345712647655359049552256623007620174740222987870848368481346721209285077722606998165772043351769342247647403/1092542715257172038171424269761043498757044379694332863740724718382311855370645101961406485438735990441717875162328450410581661879989169324258242065949423035639623495078808842439230647759381063595763326528020954224*y^19 - 117453905159905036167871988853010010060179864066305712491319571720179272782917953400550278556475734405240782863991097700100556866075402658388574209562209009742952758060430614120492943296452226283241922280652994260097531/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^18 - 1979623862347949754280170256015117263066195437698319417396087658535363942230309798117711520318762832298747329345249806813529051255423267198225806447069808276836509475921753513163556084395794912872234054639167212598299/273135678814293009542856067440260874689261094923583215935181179595577963842661275490351621359683997610429468790582112602645415469997292331064560516487355758909905873769702210609807661939845265898940831632005238556*y^17 + 370282019984107320858246512370948188080056198295338953056950037675750384936763188192340342947689493668640062207474204872891695546779346807570623048374710608454267312699004222226019759962567841432218856319836109731786521/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^16 + 42595550415086936162871887288755834532345795390029746161777359572575247379956169324609745108533643956189211851096048488595838291602499902125175147371430711637468082771330861067494532462239178178880198639033180093131961/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^15 - 354378598890896966002348248638686621433091030906747932750344298669158869236424778773880732129967114844821036061608037060225182866820759702429088442785073188278261397386494488525406123034963830646941946138903003501213339/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^14 - 8042628165656831923984493380657773362901693504299732341317757442240169229260251461447447951069845587375415235109670711827064056052020774838829533652219158695720692736102942107465659792053560455778316738403965971543215/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^13 + 922612522067938544361484352208911735120719958199540123997941102498463755577063391536650601929507138641900764528569566807160259613066038007745375914428228257952232282166434269635820892629967150699881074190898444558069729/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^12 + 104776182295194847214242941769409675232754699337450144753052965778331871588167473368778900482520371590027398751961136483481599008286778806335457425821598968222642033818533302736531732141006769014933110540655156822015031/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^11 - 285127440127169408659598596774170023863729878550303495069317420087499430110752407388566265855907673679960044745518287936492831008182754230388878770896439993429489526403040843598608966337601319175526846153010815796370111/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^10 - 275726058581470815541419214807317360062465086862671937916412328758521479741422123639571362683992510559348382832459420499238537327914613034081606885231281843540862105323296631731774196450696652960048351278864443774845361/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^9 + 8597810478920243946783635599208558005407489611526430035159806116745324602903103825514417397123323776831535602938299201114538442227523864966214586871017961674641540346217531882814271093623842710447765240107351419038603/273135678814293009542856067440260874689261094923583215935181179595577963842661275490351621359683997610429468790582112602645415469997292331064560516487355758909905873769702210609807661939845265898940831632005238556*y^8 + 63967011081314243765774444092232767239148502319411772937893490919194780072231603950528407009604926571840435664214946368511494297253241089616084029335690054409526085986195393014928329078302583718726564757652541423695955/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^7 - 2336878673679119955855520293774995680765342671107712096968063827343738232828949617763418129890768176898758345550961085344197494352214175575554843212894547960328655458750342612017806356498993740745878398612063142085/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^6 - 11424702791090299475384824114026848469936402355127888768008623267277900399421233908920965525589032422370208813865614314679508591180136879730387704558225370269447092242041208865603633828576291475944229317089045787509353/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^5 - 4659602055056151195463617670839680464381426462387781432066245368305586890622059325788152749969131303152780884055913327190017881072127650855243793957679399332039961759460099963762140656012220887425661922920778885672669/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^4 + 810270798692351859525660371897487566387563694931172005110104437554803620321470028647152108986575295189041996805887390431716083854217073036189622159946010190188882228614248939863614878057235408233731615488131551006613/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y^3 + 249748321536485490090859464435866084158164262496063432123860858042419008763217923647731579683589053713462696890803692010087898634810900695119509987576671591956064105528600179841876368726431803446970102584886024377397/2185085430514344076342848539522086997514088759388665727481449436764623710741290203922812970877471980883435750324656900821163323759978338648516484131898846071279246990157617684878461295518762127191526653056041908448*y^2 + 82286445757783641061025864478961845353601399791301255246151204762039678887444944088832389113161600919107055594446962526649559279178794881606494574610858770394863960549872329126287273537927599676065889735846955541799/4370170861028688152685697079044173995028177518777331454962898873529247421482580407845625941754943961766871500649313801642326647519956677297032968263797692142558493980315235369756922591037524254383053306112083816896*y + 1025120959938632289494803338584438379200138754739139730701624535518513013181310833809193962739467719808429708742686155939582633128182783085431357449405302415886297640365995960585777740300188426780000414542367374111/1092542715257172038171424269761043498757044379694332863740724718382311855370645101961406485438735990441717875162328450410581661879989169324258242065949423035639623495078808842439230647759381063595763326528020954224

# 4 Loop Invariant
311280490153176638373960295937907661242756418652677810421440628859346704469066919512692477326994649749054620115156187248534335707685641705550969586576468372259264617893103057424982010842543404033406556640867365048119225153495211022554066647858439843904482729714523295547741210515115550428247506072476879669/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^26 - 3466860952955583804218218477868770086596738846511338280233876733623052928168918339226886632241192378119365447818167745390163438171824570059530637289266596578975868896637357959892801227789678083285517311330984768021597617668265023461390073563369595906285804290187335975071372579122615696831714128617002028631/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^25 - 7058955908286456492939678069630206434840826948588297329312636534534454025368300903142674718595324917421043946027027168452023873531705669312211825833280300896883863646609488343411929609303721782240133631792861619641016391009349921557553111008612018950475382653927515646148270338110362478936546812977594737067/201111209971131132317551499421772210091755804917237430158996267708930903586417238123966023204595086331581569605710905797518111040132115659912845994928928215071904919789344638098522611222260916809462609763583808130098491932655060993783571690832308580365245320483123243922287326371725485183589857588876568960*y^24 - 13171328066380658961780433460448381011716688040518452741830386577870986517902855574507690988276836759900541863777031377294133567213423484103877832861168272432458410573989958824521048764073827823830353107780121570046155849491280176387967395086530180583284201344114880464576070504424602409215629524134789976983/804444839884524529270205997687088840367023219668949720635985070835723614345668952495864092818380345326326278422843623190072444160528462639651383979715712860287619679157378552394090444889043667237850439054335232520393967730620243975134286763329234321460981281932492975689149305486901940734359430355506275840*y^23 + 464106106198205340858530691398720444421797742742650644739143535153474874957324421393448470175307240942627053454551029197691098859300340750393330698070811632053515778714721418221854889008880693212834089396944928008428200385262499635541884687877150807866364249004317670045171263043452893746963712335647858655743/536296559923016352846803998458059226911348813112633147090656713890482409563779301663909395212253563550884185615229082126714962773685641759767589319810475240191746452771585701596060296592695778158566959369556821680262645153746829316756191175552822880973987521288328650459432870324601293822906286903670850560*y^22 + 713947609401908823245361731984199517699035032038893269044628004836619315453729625041805703185206416344920770937087760145773637580099156144080230725473919082137839173660972059715151342261559030232384489669161177343774477553233305946480414546150807002298607221710283017977101863695768180052962086976942069069429/804444839884524529270205997687088840367023219668949720635985070835723614345668952495864092818380345326326278422843623190072444160528462639651383979715712860287619679157378552394090444889043667237850439054335232520393967730620243975134286763329234321460981281932492975689149305486901940734359430355506275840*y^21 - 9953818091785738048166255827173009741941535475553381555053878860836955407463077345537155275097702843629672200804223965786297387949525871589266890022774342912679903814528993725756332223136429868150485297033735814824473822351740535089527148205295429494989880666257209575026409161247189604888249205967751238935641/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^20 - 2540271637365262545874023885328126914233807107602894681491421251927058460526988057565280069068007222622597948113016887665561726727453931459143280483928469040526808381021452961620427319773190557347300877196894258460437329877389491093418689008143412689962393975753134011936559350962557536984534816586321635967583/536296559923016352846803998458059226911348813112633147090656713890482409563779301663909395212253563550884185615229082126714962773685641759767589319810475240191746452771585701596060296592695778158566959369556821680262645153746829316756191175552822880973987521288328650459432870324601293822906286903670850560*y^19 + 6963870448628200808178433227507260468129193131804427551251433317926343811212020829286679287183720416039824808686446297297201484185626025026139435439385112990145527646275627266852973026368480180369598906360419552576199347661624546573121414815935207950603193957329147143993303129934603007522771527888808599600131/268148279961508176423401999229029613455674406556316573545328356945241204781889650831954697606126781775442092807614541063357481386842820879883794659905237620095873226385792850798030148296347889079283479684778410840131322576873414658378095587776411440486993760644164325229716435162300646911453143451835425280*y^18 + 1570511038993307970983993998571572006537530466605209116406889608079069978045591854656275835718508886135532266473849229661529257024780072818538651888066374628555822117344097117736779422805166605123331394940346652182162207846503293111231289581621535015725851064119075878232414174844410494991480725366620955649703/178765519974338784282267999486019742303782937704211049030218904630160803187926433887969798404084521183628061871743027375571654257895213919922529773270158413397248817590528567198686765530898592719522319789852273893420881717915609772252063725184274293657995840429442883486477623441533764607635428967890283520*y^17 - 132166630882267273471696377339530792961527449364359187381923760995846495379531874572258718765565962660329639491515673513237652448911513746168174801340937202472142395885913370279850979762219342877565574024112225288264174181861001029794679458162323507148616703103661097527720441467719792543243501690053762307641911/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^16 - 333526799370429777913461760935329503489413476734483873834912617851939502255192292157387395251500061500777149470650902949366946510358648699095875565098580235808893161842616170344933239961726563584916330936913115080680078947561447119717673619826510319251288001804297009243735532966802059490562644157495353237487/22345689996792348035283499935752467787972867213026381128777363078770100398490804235996224800510565147953507733967878421946456782236901739990316221658769801674656102198816070899835845691362324089940289973731534236677610214739451221531507965648034286707249480053680360435809702930191720575954428620986285440*y^15 + 251457637650961431305805922594484526620183199600060010424099693959859826048311899050819218761984477970607160973337721480055358799723069504510064640455542655449620818543974148393107082304300330907006433992802315005173476393467717015799443176557378988267173061120405617540352163141970714832946174401312497775065753/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^14 + 2667162013251588209689686543979414961309200351426571459453849893063896337041374185970206380928823484647354713621579542927637178303839845271881118422521000649916812316815961946788177407496336532586982084321049185621763477955455020142653533416716437610258634922486803064164308863446198907903413093716392150742583/201111209971131132317551499421772210091755804917237430158996267708930903586417238123966023204595086331581569605710905797518111040132115659912845994928928215071904919789344638098522611222260916809462609763583808130098491932655060993783571690832308580365245320483123243922287326371725485183589857588876568960*y^13 - 325869797605032784018721308523180721613912300115963877787676046130178125931572573257696076970868600500409335422266070712655742179349352188635737535257398609897011194316056667097204455191811894386889099228064049777110099556862220086587372767664886550420019886180610575165383931444196661221813170519622608154707371/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^12 - 47738877188616205972094113009723462208188438733481090233770882685371443352277098890472593931562298211904522766548732074580529491607564190405629925391627268912936182879599113330259288822395163263153498937660726037539761779917849509220042772793079634303607739394583444799176214855757525725915058166743830779319147/804444839884524529270205997687088840367023219668949720635985070835723614345668952495864092818380345326326278422843623190072444160528462639651383979715712860287619679157378552394090444889043667237850439054335232520393967730620243975134286763329234321460981281932492975689149305486901940734359430355506275840*y^11 + 190495657128011101222928591117423006975281708155984755450305358125742812462495144661148422339779441581877748153376102778009023049280869896756842071701450691738824524853381844611395530675464737674596934457908706845188408987912943475765965237690478412271220259105775316227986912531868887983244940602226681506398747/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^10 + 21188358307296456942184666845826261094030115951891079309110171685457018385493326465883504437923499128703491960904098382463774372296275508170740385300803866817606630759804975059836593653256367912937628938500396942098864123287922575591635770377082568011117106064447267987852610269144889476521291547924574259975195/321777935953809811708082399074835536146809287867579888254394028334289445738267580998345637127352138130530511369137449276028977664211385055860553591886285144115047871662951420957636177955617466895140175621734093008157587092248097590053714705331693728584392512772997190275659722194760776293743772142202510336*y^9 - 122649297033588303288160787297746334147755795398890513287407172528684807379756792951824119285356942698903255612194770087124482715529038018869746478673938200803532327480877213742861776303866986255469802505383452804118231587592847010018131930455168374045424873542417870512378408963440638917158766049181625374911/5027780249278278307938787485544305252293895122930935753974906692723272589660430953099150580114877158289539240142772644937952776003302891497821149873223205376797622994733615952463065280556522920236565244089595203252462298316376524844589292270807714509131133012078081098057183159293137129589746439721914224*y^8 - 3670384260600362239186340171921990905549756838959265331136018529222714711041461451549409797558642944166944357863682424311505274632648817585574570559256904855016259530496918815500967229991014647639331676947231626789289865530017190740536594914368743975357617174569544032437762089152580284352348630484300148462829/134074139980754088211700999614514806727837203278158286772664178472620602390944825415977348803063390887721046403807270531678740693421410439941897329952618810047936613192896425399015074148173944539641739842389205420065661288436707329189047793888205720243496880322082162614858217581150323455726571725917712640*y^7 - 230748698816816596168937687337151197908334814856566451029363386330156369964344397628695874907952950823522355496433747714916267629398530631286144557834962287258139042823524825658902243437214304835587985490246016873212088148839491165548463742427794018825917928763985866022452114652523016475854581376129208122549/178765519974338784282267999486019742303782937704211049030218904630160803187926433887969798404084521183628061871743027375571654257895213919922529773270158413397248817590528567198686765530898592719522319789852273893420881717915609772252063725184274293657995840429442883486477623441533764607635428967890283520*y^6 + 709962769078326895436504673724693832070404287595322549102221123567642424385046743395124505671227684736355118452402509626096095833263891693555007991032221557447679014720318943949344207616431967748962438599105638597833418649209392142567042196106350260171066869058344541456821226313266084881831885559868827734301/160888967976904905854041199537417768073404643933789944127197014167144722869133790499172818563676069065265255684568724638014488832105692527930276795943142572057523935831475710478818088977808733447570087810867046504078793546124048795026857352665846864292196256386498595137829861097380388146871886071101255168*y^5 + 2825045017375798476752830432329402559578708267381517708913824719747197046120540705433093185484089630645884235874285520407407704146486699997275783077138402977804678184686885277557271092415436967835362779910926469973987100344714492035797544556696064833235573078632183858056755917855262918638483151155528822297/2793211249599043504410437491969058473496608401628297641097170384846262549811350529499528100063820643494188466745984802743307097779612717498789527707346225209332012774852008862479480711420290511242536246716441779584701276842431402691438495706004285838406185006710045054476212866273965071994303577623285680*y^4 - 50082124303432918827803777806206810208163182595158066306190101358671614385628145882227051163465716829833953696291145375918461954905761780435865653679564126477796682452653550965536369094425298799121167252599290615967041982089756202917071659140423571980404612053178374798773068881479491561760812148987559616193/402222419942262264635102998843544420183511609834474860317992535417861807172834476247932046409190172663163139211421811595036222080264231319825691989857856430143809839578689276197045222444521833618925219527167616260196983865310121987567143381664617160730490640966246487844574652743450970367179715177753137920*y^3 - 148939893606260397178601958704113213901756131711359390050336940185686597399402163501895636153527809582049994517778135932541824391994310492912078841273651137621814752896883408938195083317110291747363792390705796858187373459134566285323344410432189745206388893735717469290098764734846732364003428243687572271589/1608889679769049058540411995374177680734046439337899441271970141671447228691337904991728185636760690652652556845687246380144888321056925279302767959431425720575239358314757104788180889778087334475700878108670465040787935461240487950268573526658468642921962563864985951378298610973803881468718860711012551680*y^2 - 8459556917785714310505730179131072072640722369448339441028988358779809233972619860684134692167669455203394372391606245038032807198777435586572578202897152755100847919373957930306442247901005619810870826192651208403480620153838076377785246786377325970921958335527135470366611183036051799358834143155542080187/536296559923016352846803998458059226911348813112633147090656713890482409563779301663909395212253563550884185615229082126714962773685641759767589319810475240191746452771585701596060296592695778158566959369556821680262645153746829316756191175552822880973987521288328650459432870324601293822906286903670850560*y - 7043114717086838506038116950850999701792456886267624277217771600357874135093189824176473214816128919914909557863958646731548982827767240105860208829846745341796595041534465467160752001933223128339171254981620033246931647392102635799528962108187840740017557888574420868608567108652482508289914235145545067/8938275998716939214113399974300987115189146885210552451510945231508040159396321694398489920204226059181403093587151368778582712894760695996126488663507920669862440879526428359934338276544929635976115989492613694671044085895780488612603186259213714682899792021472144174323881172076688230381771448394514176