# Manifold: Census Knot K8_42

# Number of Tetrahedra: 8

# Number Field
x^31 + 3*x^30 - 75*x^29 + 90*x^28 + 1567*x^27 - 3714*x^26 - 14805*x^25 + 50624*x^24 + 72417*x^23 - 375287*x^22 - 178485*x^21 + 1714552*x^20 + 105433*x^19 - 5111623*x^18 + 764719*x^17 + 10229035*x^16 - 3213721*x^15 - 13610764*x^14 + 6856048*x^13 + 11197285*x^12 - 8464436*x^11 - 4653179*x^10 + 5701010*x^9 + 249771*x^8 - 1879735*x^7 + 425487*x^6 + 241875*x^5 - 106425*x^4 - 3712*x^3 + 7144*x^2 - 830*x - 7 

# Approximate Field Generator
0.417936275055560 - 0.246542021594085*I

# Shape Parameters
-1521864113774636317055960676477708927765746050524675684166573238667303244742613447725419955375915426/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 - 4923713631679594773216161122687161179317365184228818806414528285564925477793170491724897046397274682/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 + 112904919016200843913881013072391434266703146211113622632152371653213871494102053536910298494698722381/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 - 110662463536431007624484072717975155118455091240375406410038665454501514003084223130245878024216638439/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 - 2405215960089891315451926536811156809872283046103021351775063531116924119248514220629153978261437488635/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 + 5081830787702625404220402209392767488528754838332320717217284542522183065888679669582263195832335413611/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 + 23606635487400326584864638367923285816728752630969163625159055956487455394913089332724264389220265395998/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 - 71260225412223611413841298061481487187194704242852565771801672812934488693138110489834460998139942911428/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 - 125768010875076757603941966062878687010343070219958708481631478323016306415873689271274064823057669776423/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 + 538278364147860128594902539432576802581549995770011400555606494408026403292831004371492723547409304292710/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 + 391508674634825080707471858433138684750189410897216897055046541783709413381788687476391939752620077902019/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 - 2492338655238302741147753429011766429777563788419957027739457384204712877920377157913617481714254390108218/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 - 723123709914422193202210316063046319387041035935316890505939907023089209228920038312489513623058986173555/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 + 7494222057934252905695811845501633698192524615153371925235799554955617665986043497343020445165343501389930/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 + 542329093793241933016520839135824263199185566779407709983408431985128884275188237235041454101164913093487/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 - 15099043954963566098648378022635206098837051381388539710687031413325256759926922134378417105220250842627705/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 + 1431527595228636008814499557165294104502658125866182724364584750838221836524533725400531678675616620791722/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 + 20381162920073795187920067848976477866752626514717307965578966240362842739158329881891586097364098871333642/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 - 5704173979230472607277172306771074433953952661463274644647756426894564680269286399752505927163524648023678/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 - 17508069601510771841694384019900725791630670160312722420650650601058328618730091605605085177957596925898153/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 + 8673106779196531086186972366176945877320666631383777070533806655061885401739106210011289032781594257043850/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 + 8398736610325790958576744028963753873340818893161598667055339501621819336232120166618345136440075998891282/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 - 6463202413351278505880408146373389566095506700010466789581395322240858355009226063066454529890600001011320/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 - 1569941118315835399736415784407423949516738725662056366754675891377038593898652537305082964374891778865896/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 + 2301970851144306090718833379860606810118057508704041040913511915763008260835656188820363917948364742775764/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 - 164535433433600082344646297282672809779799742841337864570312283949787261569296755109156430643489324389559/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 - 346691204726613779535612388650913516674007095339539663046717886197824492531956149577683929251282578885927/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 + 4508079022828123839904609448567307869116910636969122410833259626857365586315586138761482725785414778331/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 + 17129393066043593641346509946922308725783785856469182633024196547845949349991437179121703314099629641883/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 - 5619555706214291252171314991584901009322892744815243869913676633625448136478366456988130722876651816391/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y + 332014447721990315628093532114334991646252450676213131541737320338417291503489870370266503942369634693/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281

4215726235835872296004612201934952074680384023018056079911111347017135723173573217926094109286441096/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^30 + 12094777126499903349384772717543211603271765706514650563837992743876714009869430837497617992527595835/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^29 - 318900068202439996072605206160146523041225104325667274805049594677657421170395993342964164408558229489/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^28 + 416749716675324783843810600218589716357599431399128431056737707190886479419933289991873938825826277291/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^27 + 6632683204125853115336179358641901950594208667314019346805158034588155553712911424955949480668514987850/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^26 - 16553202642288945994936137098393451046975426553747318490398997338281378406617092218701927131519418555298/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^25 - 62061072753759034732528346502400986044566306264487879896933018196256775454841766595876457084341313997067/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^24 + 224103610298081937445738276636107652615057904446977238148879035163493205515403104725311306393477419774077/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^23 + 295350010138112549542801854018594833677739865426685103971837513364502779926683130904190576927575654780039/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^22 - 1660880103279762414926477519713387729729680452078859805429777612347667682609574799567382733266056442325504/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^21 - 656631670614260594119336145867936178314198320414477044987711737318920906463134705297781003587191233381465/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^20 + 7634938689037554088651174261930667806016720517766634745619217572264969717381600361940215810011803738438825/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^19 - 42013654131362864194365123869746839721153735581859100582194700159250066220916673490883681220668325026370/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^18 - 23070396952829514461535648451368907374153844833916810098626000820269773812563828488698217189856380108074268/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^17 + 4660721427138742228927736117702658288828200440908140152467308796133374174418812372748438621369024528732502/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^16 + 1519552330982804268303958442740859518783081662608469536698662068141291844608817978335212785389504977409611/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 - 16192742970818418207026058946921953621981740603085088176101527212639640741830874965199589794223208147453305/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^14 - 64381676995779602669518898235392442023148854809064660416050731193698563915358275956168465348253645714431005/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^13 + 32256161834634637082161571337355429692028341945649369857514833301108569700194045957289654103336736243818148/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^12 + 55271457985467925577013011440191730883472972283924214608329230700294051398052460176057612507726736965248330/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^11 - 38984287076837897485964336178216991869922077742921882588135744394508761916888843936987437129316700213721971/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^10 - 25628801611138089565773091355973736592207326525663940145997820477425670484750876671616490715426941025992943/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^9 + 26603800026762099774864550146712738365836417286228925515234988336199858363494405057902336089702376469528724/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^8 + 125510657656006703080012141791671188118801654660749342583984605289552135374677197377345220615580103299914/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 - 9308431535606908818378889156564611874105423187878911496672680467671631391657136592846262284143330080483967/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^6 + 1013021782297847961273663193570281883763348323888246202853502915343280862211721911145514629747561882536718/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^5 + 1453461603116716794112747135952991463035300479880208972893361262709326053814982732285905246771719449054645/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^4 - 20771058061297585189624879347676814891741333439986295077529823187697015128598606771247786906393268845598/56052931569372497781582626092269124584293491048006048913918633278128332663975515959635738524180875983*y^3 - 83374718676209847964927080393621290821484288192545402598750833013185982391073060631889418962127359966308/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^2 + 25717269656564128971360580337096318728404126169018822077863351363949843531423067482469541576800183040242/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y + 106257507590810808871295164986442086431426535842902889501959720603317669172773581577829131525944470424/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711

-239383913520124168189768429814426136929124070851925966070548057299859569225340559870750566175509344762/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^30 - 774536938025387194415485048308804918505103021863271244695322313935197139338015027470005681146853803762/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^29 + 17764940632335355802414489854560812698956459231224069562513817196606370847914533771141840652439392742415/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^28 - 17384051298780307209665840555670007762307765614946398657855348183169989416500737597819028132324164928497/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^27 - 378742270026508512474880552926990672620472581306635522371798779707376259503550761814157765615699952676510/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^26 + 799628669561840445313409621624919535855545911605826643610176170795437492951220182238349183152886991338457/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^25 + 3721962817453367092550666854909292311046592298497750611176479987319782605691952237237365046158008218441645/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^24 - 11225045465624798381230236242881687756465110537926265719655481978444447607894863877434250844569125389715701/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^23 - 19868375292679519801216648844230574609651520832587201834507534772871295881527682262667675048421013760568250/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^22 + 84897258802249584313060289567282080847341901011006035591075809180109867521356901758817775419029171767118788/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^21 + 62050182683304712671573997766194293519559353627170969010402944716806615003194599822915560179265738278332530/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^20 - 393730747546819729138507290656463981805229084598345922647648539006523118243630818528638599211732122954143985/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^19 - 115363449264776418262317862469713611684017079691726248353808365434897382153279020145941952917089624004987380/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^18 + 1186424712588253466289346834452223492845859263621423869584833906198309431789441656377371252503691108874739497/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^17 + 89319600956111805785743680324390180747579769869574050314733366302316783880419474573353300354025296300514537/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^16 - 77321838951972040853258641880671190397892992050826235394488047656682814108940710875199611648152832913636732/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^15 + 218005453398529388712206836077152261533367387255103172034723036307083726142551364287358604673805326477386307/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^14 + 3247954111340073378349479495734248595043998258854796955896241276234778292288218495610968481610109145377548552/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^13 - 890286129511302954729642903539616363089909012078191014480703675930015159428345604599560355055885781609999781/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^12 - 2807762045941018974824027202249064838221828914190874387049525830973188957174182076423791692400817340242916628/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^11 + 1365206720026241617411260115878303572458543388122933820215539039780164225102939020272958982744151186866417057/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^10 + 1365498171591048810030389624287350382806759958028754505013898088836629926325991515215567876175876917180497387/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^9 - 1026433023601837630977805256327052120588735257477858509584824134337098900246561035763454645424427583897435675/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^8 - 8662120062257257012041721765718452741613316422353641760446247049707037825052126535512100415285002803300180/952899836679332462286904643568575117932989347816102831536616765728181655287583771313807554911074891711*y^7 + 371360989699041346734826273489524502386601328466370965890633179495860578747134554304607986649211205865299766/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^6 - 20954249696060348258986646932526199250032930594180721682467694863541865134625223789816264717903732138974870/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^5 - 57961104503093006407736874971711155425571438640904072138585916658816163724295983241110737311782242411642717/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^4 + 699357396981545680836251371978724040926242372690938745338220944521271777798240046904291239876709155214779/1737640878650547431229061408860342862113098222488187516331477631621978312583240994748707894249607155473*y^3 + 3142498545323502771522944776805078577827834754467651805418194820526050907180037645590273224211556535350217/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y^2 - 910257712538009614464460930575418463641373855677321095217656972200485197963326827148578744415481260376282/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041*y + 18022853528983698935321339447143709975635309860676994210997744293947961772225439896096926057609999659298/29539894937059306330894043950625828655922669782299187777635119737573631313915096910728034202243321643041

-31148960723020864603907942527654826334056344956986404284865994291758047855984231390182872892540383757/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^30 - 132213834608272711576188851248323926453073128972027940621818218226068589546501616856364560314636548281/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^29 + 2189060438992547271688723855978072166225516513560573045594939237013646350890959942026082041562416938421/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^28 - 8587437749502206549141143070106690839896496222501375992713920713329557660473339409223258487301268449/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^27 - 50062084771082827640185377108858536007969859815581687218295496773726947214366005514549879256511554732456/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^26 + 53641163184665111379908681927121779880630066232513731018957764175996555689185243202201829731823736738912/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^25 + 11346043167987773859339317825482997103912959290848083415620620293075016864238175298843441363730610777986/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 - 131550284634181508437169163749712581975320479190340683962279765861969808763570625627224765702728534137596/215170930863075072129301048547742768565513723700410316798590882583782954419776980619246867237984652967*y^23 - 3706972060608823669967939844293105473177114773318512836595211004427898738909494223446039914886970288430641/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^22 + 7657477678494553150127874875426999094077075791155252718722792282575824736862616544995053801625689240177710/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^21 + 17059206675242310317539271405032031778813670807294495761864064911198656429629778586593187276842326295632100/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^20 - 5272306329018693598068044469226635838038064789726315929959142015470430100528635414168495705941278249659485/215170930863075072129301048547742768565513723700410316798590882583782954419776980619246867237984652967*y^19 - 57873146961456108395362260465092378721234629720090231900710371263391046726538255079213348398732677497301474/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^18 + 109929426139733463890110559356523937984923435556248928956122312416928463156501421795391976209819141935844286/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^17 + 141023734562989151654233250520622708978560803720000785968227225613904632535429706442325886793652583213971646/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^16 - 211778379519330343701483943469078983240390641068141592043331623559816146001634730275450553919242857839153170/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^15 - 32736043694168731925818625805355680773807799367810331082884905382397370437041051858331799406405693457062065/215170930863075072129301048547742768565513723700410316798590882583782954419776980619246867237984652967*y^14 + 274909110656596446222744731649209204502792508594020237203213953048286233722784990036295081292491644169287939/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^13 + 230595972807461874136571872005872312595334105219885671781787788514015092206645215355209526410766085314323895/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^12 - 244763855106962704713215517324340527505904351173669325240203132828475547379126045116736300034586939533554161/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^11 - 134464516284481198264789606957367319334992426335248240213044728741490437780494925832444768800949247087526246/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^10 + 144639442459148572799559551125001904133175022772929957746790753278089183035117718207160330708253765913460402/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^9 + 6263889929990083479258176650438058430950768480812934366554397088891258992965225083127900335421996938503221/215170930863075072129301048547742768565513723700410316798590882583782954419776980619246867237984652967*y^8 - 52077019355081268480127229843934884073023801311780689501225822396004805166250405289295328222702478048874570/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^7 - 8718792500191426832472443711148508823124793548315492824856754834562550437283685141286593318976207219838842/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^6 + 10300830496173707607515503425360769432500656727593333088311324312287496554203781745376172325721002070425648/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^5 + 1121903448443936304370683575285618115600514182596779610509070749341967328813150928706386879144799897787898/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^4 - 73743125230486322833873781396054041943593263811572457027706938064980249231633280963300744919875497080881/88599795061266206170888667049070551762270356817816012799419775181557687114025815549101651215640739457*y^3 - 129756494378981960491090535908982825572521919660927407309429919014922007251965913212992945317662436675998/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y^2 + 57471926860776110929013614815371031659030933882619493484703087575041095824675174339692803998997401969296/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769*y + 1552830770672476170240594746220545211100837310862942476558095541293637167849456085792627568116131391545/1506196516041525504905107339834199379958596065902872217590136178086480680938438864334728070665892570769

651617175889197348906804583292725180564222271308335896942628670174506063459687244659488169061606381/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 + 2153592317841332263831630535828256168895525469077428251519255546604839019952126797970243577500573611/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 - 48211479970740630481125447217698061067038179988969828984089577144895784463117276457313147861433687003/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 + 43943806287775359585666294579096287947165813346461943016534249555447348917911357932744435563260340830/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 + 1034240627913922472875280221284101104724763624115141130381436812676915456918424249600344506661494671653/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 - 2103942428437659324530340173082049666704959349403419011416076870493260980154640824405523274294081761592/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 - 10284489622504170512170821417638756441764564409452014335739067476363606167682637592102739353508594938388/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 + 29829735262781166326137700092845993289726387415208877622517026532836986451173646394731653535922959421559/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 + 56258549831338388566846008519520358512692728779668174479660202636958441183669876385676358804152255254788/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 - 227131945904457171206567740554912154761678301818091541674939840172064892149024454363838161832418398201484/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 - 185605553296328556201686302613915300230813219973487176518172090267739139714031057119383709422478157738047/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 + 1058904332307825661925255466435257476508777630228417523244442496700290317310955991192559083245120567988616/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 + 392999320471264445227729002678561859357579265006712096786803382306749850614534098276820489794899727357004/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 - 3203537008643331816006710728113704911034276620256122794738636400980048264719498415929716953546070526776681/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 - 487038620998306020778260894594030272514976390609878176799269244771047225965716461273962173333755046828408/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 + 6495178144087222430682050101702407615539428740895119398215549076722263045709167563054925084286472290667271/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 - 85825312542361545627638159382589158314640703405850575812922413488193035682022929891506680944409175215434/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 - 8851709143072623199816834920754716004496368968125889371792346377290126735321813853785244367878051667192312/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 + 1710542089700580226261513936441287994763449492503834218635999790243631018901484535838039173643583298590582/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 + 7761636711446490045918171684068593122796654296818056746490603821881696999933057783945948951973521914447609/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 - 3067769639623827666023067052253696380024409009917089920098982170534150967551184321706262002638044920914725/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 - 3927573691757527053502652945047015706900291866685005808844876692254082257454875377774366978621760421762419/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 + 2443615096200661383413867879506288798956394647874685635558985686658504498502287563202031190425264916345073/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 + 900177959368668588751203397360668596265955617341878925295323102293838660289035402479316754284285942902405/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 - 911692698073121248148521195970179419122568088468523854939193730716503243716318933141447294071181739216250/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 - 7277515786973364357107256733197834401670634187235380345565117716304594941177065937270221827931500564650/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 + 145731980080963159463689298432785680637773609303585187002276252868708084794497186016124747976717255431862/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 - 1257652394843756798369347359147806203751454458807918647575286522784969242764285873622612736306425206575/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 - 8339657252731857612208244941433426812667260068491163645974415364435322881457067937267831728310681217654/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 + 1629225690354649946328289539620682688620807434309275831764220043252714680910452697652769589227737785892/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y + 44557187353954833224208809937192195481755330954565225311256308783639818056016623998289024463146555936/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281

1218294857685593490588764965081080997270194289202429482812264509320328687317026765708796942490743437/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 + 3424758033230041553155157854692695562833131050720842905239444863650622828551305901183372676428409446/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 - 92098522879170382749509320799992791701037032314443985990368754611635567312205848108424686506411855463/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 + 126794374434142505710886159605805171735849198535461928889682823222040776076078443915671790702445726699/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 + 1891048901141814897806254138033838952045615522714543231244733279807201438956482076495597845819290474168/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 - 4888327394457537454155813361554916786673934983248591287860381519179065181614874234976634034057761298313/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 - 17238999572767456506929729816680992769559749135873228073235704343179985671003029690797383762120817971139/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 + 65210216561167417818045355839026138220267769484074324819944120305919974238198908505833926205270162198445/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 + 77123269906809068352865515576159351674644063284058119791190281767235002825750418075921230924677246557099/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 - 475648081609010527090904476357795895283716748930025317236971698214854779068205980387846002772863812136878/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 - 133887802505927717517822619506785446228317963661405616641249991912618960821689005738742449034543093318575/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 + 2143194553821114929788162128173407334782722329417490060444351047564115202472643991688804783097991759944832/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 - 258251991409828116191608851869885740096813308808797836776996875180076682065379552569314515606368298573316/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 - 6313096400693350632407495219045339196106491803879212365200860140641884616638127228503167989676512885784376/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 + 2097638901304537183314804984707128114007170060641768690848527144373158776336127026382232507172934789139541/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 + 12470959027705371283973000078456160959548442058594292168517174307829898460134550605171452369898220065167709/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 - 6277189958039604698899435067282998920623844824414595215463669188229288940145162586601633984583684569554241/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 - 16217391965377433596839310835576615407996605699534905446019919831097974054915902787514226040461458235449273/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 + 11561010600362456356003915188839487512022678115480234394544095438786494394031626837835863685433732255533075/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 + 12573766594392467526868898731454653964584752605017177778701905493291897524216480844446910962076595452698662/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 - 13082528479527908552671024362792716931806326449383261406893916416317693077528202105281439559350654873251083/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 - 4160930428594354068076759259083031279141905672078796922746867251641501277645984402734517528297157602793769/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 + 8277026101760734125954018703048010641054655418330867525582891765398110881233289277120724666776968892805036/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 - 797551781278830000425149713760478731152662380975855001323902665330073775722274123651779932127390599156079/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 - 2535034413105587263973310208404273453269627202635678723338646295860463903902734775124391046734011575165128/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 + 913512129119932979167458863445378301904761912968292140209020639819029703342098352181231056297107227274728/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 + 264425065261675387713670322708599696586791224536248577425110546902949607105770343091625009811052384584614/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 - 11233832298878840156935789474898005877036452439543106089427792742976119976412415768496887019428869104655/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 + 9051178955698748460220502805925575257155295743923740631879995506740563482580628968211612333414757054107/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 + 12017422958768213302090424900128970178249257576622304670552530807511941154053969583658205549655645895999/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y - 2023488739183538331153153111823314470338518868639565767475689716943463136137372637798202655893516997780/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281

160525645829822399171200383674632127667426480272678418596195538144824630897964596850286617686349357/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 + 553790073390175743068543829033931321047474142263976378657716691670402743648773976105870560598880399/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 - 11776022326975517359108961622276175578452448008076703166289505135411482184040765325956438036879540267/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 + 9196468869014194175782403916371570629686933146266095392863437382935514918514332494232056951463469485/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 + 254625189414181232236167999674678605661869446328556452966659869339009615102938932560216537641190978388/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 - 480637779787648905374883248900070338940443100454424146738189948978622685227239838554625368920031593176/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 - 2570354855107319623671619062499797675791872422002908288842524927111901660903422212783880699364603552315/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 + 6923384034594110748807547864535738936284002969480508484965584429664918415119655217590296562173429752084/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 + 14519506405955147441293798978011999601285186634598675384851046365419695611498729199252042454460693059539/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 - 53057226253092921584890966804996038567399260575836209702224487760334369969302262547193246495025378182994/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 - 51348563815100875178471801836919147759185711501989752160937271810728342935451862175907663237570369070911/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 + 247215746904723885926712825838329635804611455433829710500292031085921508923605028607605419565802247987536/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 + 124453527556933785996652491805285704756310682249397415017689372289860869879128739548453552364588007290911/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 - 742019485120680606939078635593087172381352294824875921563770569573601322562372519743539283876959698544681/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 - 203916146938170732064719090658456619548137084099979228475064712055120132007844169622156253543289800041716/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 + 1483472283945093905076605247693418282972188930416518958333651310838120759894138868649316543760986367943106/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 + 144504932120820617043410567142085307275953274740337001249425852575868017710408190681979075222397941567886/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 - 1987973368196775840614028404159113232371801507015290442376572889407860956717297447705630649586349910107649/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 + 198628459865230922875050431678326236340885684695096794616388589110815465789163998608446883546411452562746/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 + 1714064267197077361420441310634921164362287528249156102658838183824558837237217994715609065707956692988116/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 - 546557650183081086266004966964079291347750505809623293919525352223160081673281253257242884057663692372624/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 - 851829460776437716166428163149272519134943845558836740541156076182580789067337596324008954387690119489590/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 + 469282075948429903263532144937065956087343994505740215096285979794950998634544223806636704717081261520862/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 + 190175160982716488417378658288074216634429240769100159286382222856487804604272253858883180144399172020037/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 - 173785631262196073018154226523511663288748521374305647059022169742488359472545107006416010376607796810571/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 - 1293542184393943443625251312323630674886183424764226774882179494461900120496557864969005565162434737077/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 + 26632824850391719979053318583723557410524682933364625916985625329831030803433404998123767470440328815129/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 - 230782076046553225025485652177227993682875617348144248661209010187991282579315206008807542656964620665/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 - 1627285731590061685184552012844658306768470750026564603650873953202740070397839289989631956825870749289/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 + 307893719791641686519463372136192511191065659457149885538457125407974189872422317429446799311339983302/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y + 33245553441500525344238103445312921995785706900070730391488071784624389407782593985447155581598792109/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281

-333134947506231930233357265928968989246141253078782286091805435689639455841858544035724582728692336/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 - 1128414964647583787638905256509417273356751274634572688610113517837117218071952551645038207223800182/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 + 24573560983861946763581789264611701216011335848288356160846161899570714205361538984239896032214733523/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 - 20386840805295984826171142615479086073907178462187831246732878604544430618205895364278208104733014346/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 - 531813428850606345612413173331330512181983391423936465461149705808498787333022044269534049242933182250/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 + 1033413660708187245846352333586897430380564422786264693658993784778417013948255026592111003978608229364/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 + 5372086736372488464828743213720056308419630139704694353703931756270833215930705539628910247526207402931/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 - 14874191488474395642460045177842538052758023559342847937771229963215913033537149550817434195945208246677/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 - 30265617459078989520180318788572394013608489848730999537972879481705846650510598420358241145754492463337/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 + 114534969115031847329994908954420543721238988767448253555659806389045146903662677811875369205904075220062/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 + 105738042206588437130692271004840819933850371386062508376993217643170285936571326057065166607693228822104/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 - 539393131073756814704850317482686825324633079235071210718405656197695383458305296997642560701634099342067/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 - 249292892356610237446774116075194660314678568274869081797979785542689131842182691828128501933005457173228/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 + 1648048860165667839427981126861760218475106800648381750573246104859443781797043496228926746370844273148358/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 + 390135747371906685622151950267644903418023322904577552051935744989723534822877750808084349033425965916395/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 - 3379813222794924270534071987627102038730742895862759981339128070063710810993642760534139230902682235052659/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 - 232368435377558909284281348420632321111970009592552695490301165414584534714145520031738266200405932908329/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 + 4686783592777113993904499582716027282507998582844122318681692884315266578151669581031197154142686496662183/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 - 519913183317123900084365585046869025947165821327277383567424560415364645052383563780295503686049178650710/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 - 4246198042603662455640250395555325084151529794127225978981913869133101748160249572436961404211509822885775/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 + 1301047808454498150136754148513167426691032852058486716748643027938821839769430785445425056001273962356487/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 + 2302891703619359241968104993828522878853440818816485040880133826658071319204552679619431557500494102269854/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 - 1167934725322468330083920955621280682901311972993855485713672640737766853164684640198687265124131637546034/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 - 631465094039805719823382531757795131024837090570889615925406584438168694703289556945027396743080066836501/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 + 484342925047238448097924614844387749054995629610760925274068922076269928919930841744731088892758591510687/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 + 48419949116723440861276041196315016737486404268221583421386073042354235078806306384804554702391380059920/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 - 89522194138181143606002356618685652134296827693049421268730007240212938610341478793967188622987345177613/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 + 481206315565950995162322114100890032810015053744534028212142541645480678596490102182704374445918207852/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 + 5983557274470645284744789541415432727180036226561139848114918271396859381066654654212677587184148737172/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 - 1027477113928481669116223638998123939774951718033957247723537310753762505014614159888473988728725990258/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y - 9331465900497118508457467434327001738021025027440080648287203664948819963939138267741572640335778589/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281


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

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

# nu Gluing Vector
{6, 6, -1, 3, 1, 8, -1, 7}

# f Combinatorial flattening
{-208, 144, 79, -209, -78, 79, 53, 27}

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

# 1 Loop Invariant
3671182582748309239428177243844046744636518161049926941004589966499737127863196075239279116461740764/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^30 + 11169839522204411975419624939742819631889774581105139460522317778395039972906960082768257554103550872/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^29 - 275411307826102720471505847469071309352003860597883050986322206883772541840029479201643654449214492550/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^28 + 316011255713026429884902604807934749624064587321501862222418087446661408744843006635503842757011459195/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^27 + 5803246934008319939449947299572155790216384114635147163846906647697086281948511831313582000492914021348/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^26 - 13364069292186755947560016710924865105316670303689628826092082385477223950457494419380654056590873143070/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^25 - 55802388132451321789981561266931961513730349253397310608510078459747047586340712209693177226311856756710/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^24 + 183885598487906781618542448553741330042349680990587197595328823213377737491941641380666917763518718174508/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^23 + 284051151384956535556471468913104474050017736617919966932449808903499601948508750520820975630393065242366/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^22 - 1376159088108148999445554944946129212298362717990299358789725058576728670531166119100662744459681152729205/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^21 - 788794180411994422481520848865908412797288822330433137413950343975194707000674824293786212694719222239060/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^20 + 6359501008500260401305507153115126400656956564516480732301615191867661637091866685589807954448393746365285/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^19 + 1035853470901976861428034809161339391531734724614704644778807320501743465753738207441313935004059701731754/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^18 - 19215680316744049559609715710272141373162391035802179912662664749801622540317505710325302373065663240628954/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^17 + 616325278028261559511505781254453411865699166522947138447191747205654258847868337088142824957571221565266/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^16 + 39034293157927842480526806063057731548810637348896449699064139838490176373330324946903652507737777059967313/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^15 - 6674388486355664196221117353650691701920053405121429443102954304426962053645895381516045506013467927760555/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^14 - 52979666141629435419122747207234917132987318213742631789951784732350103861388728462071859335538732951996080/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^13 + 17135614740576247835918106936331183000203220313207949863534781303041425380480656847929255134080525245214386/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^12 + 45448445482053912727537409591966038978192189440678794404615730590373443433581581323628902336964619534381518/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^11 - 22960224893643133743542452517792805824682178358538138460532370981798042640838660249438581073659321035522535/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^10 - 21710255534415888881213487288206046772400834271664430943108511126207865108496162460849811909423045935399669/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^9 + 15930889757629490307520398348399235965635366463463406598007636706006963420400674752688943909909257955651125/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^8 + 4278134482275879414316072410550943058996688966961066507207290256550434676019508727022780905370073636555506/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^7 - 5211615382993022761133087712067730695586835830016933300189496476921062438737719171857047967648113067040485/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^6 + 113954393854145129704725617035380560679417886883662362737161032921133562476267313112208025045614144577394/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^5 + 669823194209264118072921420717470592452016014053305509957072995714494839668305161844350077580925464848851/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^4 - 4873099725193702156039065849262310721886901117767447937027821542765720342830441892763624640829171980427/1808159082882983799405891164266745954332048098322775771416730105746075247225016643859217371747770193*y^3 - 31986111508410228757167557200915732116029723760247510434131708848797259365144664354083575377557673990254/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y^2 + 5100465125853733056384171720080724475595561133783533126454767628786230867580555863001321299055065085403/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281*y - 452620278032862823988409411203883695171582860176549991599990836037601685922614867623686719215417445030/30738704409010724589900149792534681223644817671487188114084411797683279202825282945606695319712093281

# 2 Loop Invariant
-16463205649079991188149505464728044231135215677092124127089570960044413515453724346786678138625189479017014815644921994877973511100365301698551387401282553563186873830125750864662073021052564900584779255319/15105083210948951626688530806719139635552165451561573851783462168499593624360000321716773027968249584921375923022938118533853782181773483530533689370498468604562713332242153923450783144734361522925167397018483*y^30 - 265228980762694598999700548724358432433653521112866075815559770351783646958165962132232024731549773608758700385556626723690975649528971374041506477370384102692467427136215985403070081350617044049538377095333/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576*y^29 + 19756284581938812160367064068318979795624698703657427162238166737359572952146306409179368095785221523235983874296263893870522249449290150040353734851688495661367889856147287873367521904655606212282001188341751/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^28 - 11615095477072073614052110404537510081341610444431588064449546741667599575181140963106841200024492540091075082507574117285867660060697707798827405828154836268428756147453585323465753990896477644394483805443213/120840665687591613013508246453753117084417323612492590814267697347996748994880002573734184223745996679371007384183504948270830257454187868244269514963987748836501706657937231387606265157874892183401339176147864*y^27 - 138152013652366297379016019188234851205922168380756568797525468751351622039672574638250365174560037622947267138958391039851234036163962319518035877178910218168190891367696788540911392179357101102162113581074609/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576*y^26 + 323331405590513830481502497703356144787638364139577886887090866677251141858585760054575432066741586190557160813515188683334986786514385613463264312531126469250539055410692256416960853575093758617046694428764793/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576*y^25 + 986846992884962509653438345693712375730965012349516156901986448807553735944369142166077864150879859208212272620171290690968428413093795575737731595916108349126478512223738591988822709098575945824349538041245239/60420332843795806506754123226876558542208661806246295407133848673998374497440001286867092111872998339685503692091752474135415128727093934122134757481993874418250853328968615693803132578937446091700669588073932*y^24 - 13288847796387053155538464628017723439327138024501437930574778267578425667085232863979766687819859128141021712770928714353226779788854791721145325020797954785537454452288588235142563745154289941844583779688846727/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^23 - 9826357871718996080559655168420181072447846109183326981626740120157849521738666497544512482286545398495338421425028947132713656854387326274967377926419780912540685387560838920540571689331551739422580465383747565/120840665687591613013508246453753117084417323612492590814267697347996748994880002573734184223745996679371007384183504948270830257454187868244269514963987748836501706657937231387606265157874892183401339176147864*y^22 + 16504979024267142409671715776120332020403472619882652832427305013428719264819187710892027810733219380953748391556962931305242076936445639040530207034860253824078489342044480758465377148789561218549579245887231571/40280221895863871004502748817917705694805774537497530271422565782665582998293334191244728074581998893123669128061168316090276752484729289414756504987995916278833902219312410462535421719291630727800446392049288*y^21 + 6379264494620370354117608139986492341396596325036053914015668559582157891919051886743386634140008315065451322721948567621131146942973063014006939159999452036513757530844477668811653779232359521758784377356758269/30210166421897903253377061613438279271104330903123147703566924336999187248720000643433546055936499169842751846045876237067707564363546967061067378740996937209125426664484307846901566289468723045850334794036966*y^20 - 9486965288166402053599500629392169308265665559866583973758741237425185852056383619434354523102500766735963873044360733256921166770697280446664433382472899001697606452298663192965922157537924307209568048887740826/5035027736982983875562843602239713211850721817187191283927820722833197874786666773905591009322749861640458641007646039511284594060591161176844563123499489534854237777414051307816927714911453840975055799006161*y^19 - 15306824546071469100404857769444134554843609708111039219343166595761722843058789693470559340944071855016272906324733429889694800896704157515284827490142051748742787937153592735204109116296301993342418791483112563/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576*y^18 + 456343081464822931097728667379405195798506036668540511856638734547635930776663030832761476240652580131250538346643589944066949499192291655523630135121130510539174260323450495154127038386397413939023245763963928405/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576*y^17 - 36176086512844673789673284816415133792344716689226101363476230988646349530637578156580570522345623291613854390174761644273660399443679184731018219605730105661987706226638039265770025647143629064343544087897664073/60420332843795806506754123226876558542208661806246295407133848673998374497440001286867092111872998339685503692091752474135415128727093934122134757481993874418250853328968615693803132578937446091700669588073932*y^16 - 461755747445001504198839422591321074608480275834543364103791510898486785719201360245441097768105057157348832956027655260142437664295880700023625062881313344723242647303969862236947940171550054529243017435495353801/40280221895863871004502748817917705694805774537497530271422565782665582998293334191244728074581998893123669128061168316090276752484729289414756504987995916278833902219312410462535421719291630727800446392049288*y^15 + 722022228150279819574062168360994116628436520278321771961774599454574121986989899699366055750316413313053084231901328347830877388735763179298727239332810401694685465393555635687028304452539786689898317430303549197/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^14 + 625116333357799423756907371139494180608091993341343635766939062799166851639551170236887715002416761873726445989932942600919037654107690237614160952181792124907769060261183088752034690890581089926479604878921311457/40280221895863871004502748817917705694805774537497530271422565782665582998293334191244728074581998893123669128061168316090276752484729289414756504987995916278833902219312410462535421719291630727800446392049288*y^13 - 67582370698186277867636623672516415308433698514953243027535801507136605319134623255838030187711675280872678182480648506229068293145619579550411929791473188923360223350263591072895499823188628304645434168701383025/10070055473965967751125687204479426423701443634374382567855641445666395749573333547811182018645499723280917282015292079022569188121182322353689126246998979069708475554828102615633855429822907681950111598012322*y^12 - 3195091486239767090537822804289234248347030414312511892110176740571439696106757499305689039067215714630213676517375802861414065500494609266370477795763976256758546017307634833412520293748758014873904260303541531199/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^11 + 2063185237234085287302227010967373081009831665335985268751716349006649471958808815890171270852411940416037142229722242622539114099567933049777305267674243143202024161875649423313557343895984310961344645554176110109/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^10 + 736643816177986448459000673870988250207005912396409537760369104886891421078631311086091533321525846588792141675676439470893422271685308659835274655744582988262935978949053976461408082675981718185876089835072199327/120840665687591613013508246453753117084417323612492590814267697347996748994880002573734184223745996679371007384183504948270830257454187868244269514963987748836501706657937231387606265157874892183401339176147864*y^9 - 356581342742765028520087966675064665802290882235745435003290904358250383612034363021132552328465258058761344332358817543429238280433179223308404210488667338073713463412464319026007353597169402483502364151025982577/60420332843795806506754123226876558542208661806246295407133848673998374497440001286867092111872998339685503692091752474135415128727093934122134757481993874418250853328968615693803132578937446091700669588073932*y^8 - 225193469994373244657825496033205677288093752537632716154675541283126418640880516380732340225345440495366726704681777353312300727106932509412018695369017008497366886356936082753249752573861266331268098914952830129/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^7 + 490869576821457885044071716722472125059112091053166196136791419604690994199093358066801190146988439368262228261462822931649431172820995586960301068626625566918065112226655362029638567085717267787839047991103532549/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^6 - 53067024831994394023629281786755396920041345165563674195961629644642266308038882806874576611086326129153402755131718856381876860647663799955214149554583645314139974027607294606885604708790236589925927871992409083/241681331375183226027016492907506234168834647224985181628535394695993497989760005147468368447491993358742014768367009896541660514908375736488539029927975497673003413315874462775212530315749784366802678352295728*y^5 - 6047084370981383688569489403023214677032399721948075011332393113988956479694857567175199404208462010336586963058313045740006826149431028577317279736110592041133842578095984268977521292388530998300114441533846515/20140110947931935502251374408958852847402887268748765135711282891332791499146667095622364037290999446561834564030584158045138376242364644707378252493997958139416951109656205231267710859645815363900223196024644*y^4 + 1022036031704934101648109030241011149348680651204470946778356761705918578342061133487168944840804023147132731208700206495260893909715069599803027358226107064278500515991655747298607911552496972923051649192200353/14216548904422542707471558406323896127578508660293245978149140864470205764103529714556962849852470197573059692256882935090685912641669160969914060583998558686647259606816144869130148842102928492164863432487984*y^3 + 1870661903979377868959613659355814566748733789039228975525618178439904090269892984908177582297049141664324722012463770407155829969275471615845646832698089658730282964687105492261633404358597148655335224852739599/120840665687591613013508246453753117084417323612492590814267697347996748994880002573734184223745996679371007384183504948270830257454187868244269514963987748836501706657937231387606265157874892183401339176147864*y^2 - 190768014341434905480165843081935537463669538309030751512341075424823914049316340782241663979793630083403627644358575703468140528349516021080347183750882341277769865191228712150099056072004134788877761070458495/40280221895863871004502748817917705694805774537497530271422565782665582998293334191244728074581998893123669128061168316090276752484729289414756504987995916278833902219312410462535421719291630727800446392049288*y + 303717249089658540502217389285806290346823662746152888812527911820427898937269610231359825482822633625141062798997811444452331319753485661284676117348710042842340093042147224166338698170697795694622288381107288821/80560443791727742009005497635835411389611549074995060542845131565331165996586668382489456149163997786247338256122336632180553504969458578829513009975991832557667804438624820925070843438583261455600892784098576

# 3 Loop Invariant
-8859123792788910030836200979174916559776724396364457540271048087345679703832824525561751998838676243106118136616627966219851155171840732239259048487410860012340197020997116434728525028779633706280535448680380759233454419297716078179746326208801155127966122655/32604684666894944892930520265371130853198280906988447006190119220320376433477288546600691806232932949462515703350514983548927112100426645876367433509890832859191302394907501223571377009510947796694478959565034666239374315316164918114718766919817880930147507555984*y^30 - 116181051924888257670686985986233372643520179699990469778727554786568233290926698274950853693894416690577991690086939342663739846407814009179847617965159658023699765484657275147385035305259758148326459016895795098696236839159123458850219882811085165406353936601/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^29 + 2625186371182681165876488825499364007390015325288092613406199591369778967460093712714328277004680728081377365166265361199735392536889777009112712468258430785763056910920119927451496497492418035553649226612498268097960163622633025090121266574980643459863608317499/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^28 - 2459196812719681002361853662256803337701686741248031130591287524544204451623430686732994788598721883050416876398368809960272664177348399696510557243244004191471437144977531980032900214357182442318693953211987939087905233716774475906484599397997386760501753432695/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^27 - 14050560340277476908785558088887199987716939108215775945952069335638988851252663943839919041808620642288408455206140502746424373909590773276964454260286373941588932148205163054209061774982856374844116234369692120831030733199435901391735704514652454222678731478005/32604684666894944892930520265371130853198280906988447006190119220320376433477288546600691806232932949462515703350514983548927112100426645876367433509890832859191302394907501223571377009510947796694478959565034666239374315316164918114718766919817880930147507555984*y^26 + 115986275054255342458435298258476357580498281781314372233883127784629194827435945903092132135584591741331725892109998995567880017255082598637969844181421823136732461594313700193091237353010114892596014524873559543623108018945763299304276407022679203703788028647707/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^25 + 556610815660127488348755288862152906465112066622608208141741056283690657970225758939246240521621325081921238580982211506222144730548087626784186709877000278591590092821795958882956242718928087702311256651070108611007256026428180014697540468822118709414822299973023/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^24 - 1639212317189859060570102537400813008950883534131626660341205318667252456007006633741234296345696520737760586589936753723867233957468258811944120805805158585042893172825969664179709155545280031057465846383577379887907974311693999325888499726822775316659266446570955/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^23 - 3017981382564206733109215431883154773679874445395921592629750335944506777586843129558069893583501484321572867985968435253467844381888895936969767391331062198333251429482685073737577483211589091144484668979250244205730880570637878597440918406628931354392152832744801/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^22 + 194667093704744735717771887659550625951471580970660851916482385660116851409856745349443050442159028331966163484708120220859823993520658416446118012779277753400667313414065359426273864612915749090786487300141544743338214051008935991735395945163021618257880196214689/2037792791680934055808157516585695678324892556686777937886882451270023527092330534162543237889558309341407231459407186471807944506276665367272964594368177053699456399681718826473211063094434237293404934972814666639960894707260307382169922932488617558134219222249*y^21 + 9752710113542446699163460779300669952648800173958473658551711020006811075907330490479822567790615084901968574593788593924457144230326067637110224626332567448685567034336574454975703959474924234623099438016127759347764613534488652104169071806674161009457524502033683/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^20 - 29012108903983511902100955054219476311040610807241997970247379643903615869373547123959956859019750601189465616822252047198442541503079413494712268998218876599710490090998815140944245754115063868595120897068486832642708981970858311191486450058173925909065650244081323/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^19 - 9823954360242824642955819236794891872522390359261352542487279766807726895559968315201877992447896286847741183940559737211089156174853867023682000619905409667232001157124724890617947915377885345663925142857103240600140269478601847382789310009435160598748162077356415/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^18 + 43878666051559494412045845830171733316632414660356212958892278659858509837744826292082582415621350590533233225963158426947542811890685100549338815162204254304475455909267272073763998091368850495675775601814849610772033066808738669633767247648504960137339520794367157/32604684666894944892930520265371130853198280906988447006190119220320376433477288546600691806232932949462515703350514983548927112100426645876367433509890832859191302394907501223571377009510947796694478959565034666239374315316164918114718766919817880930147507555984*y^17 + 10389922375704505595408319782953105816520014022527854567815645841562736710409694165039923077228436730445718935539958863238044539546468872326836336877809623730345898723660552051460364648376960173023925318456931799567000482993101643243851974486838646587550302239995195/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^16 - 178041709346503975259353612262618970892895649531598622871355532127784502556852545055964610256339223260191151703963033596061636240526328872978473700364558697426043949821338605343280746732511773346568329754475677854292228310893707631858640111261420173503930535763304801/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^15 + 2181982727260673829501277369931011994408049250974067980094075446136567236670335307092320151902094069518200016769462345170656231959039773898965701058804298791210379770667666764422780884203594716642488502635001058153189948810595427632108364899710110195935286184124443/16302342333447472446465260132685565426599140453494223503095059610160188216738644273300345903116466474731257851675257491774463556050213322938183716754945416429595651197453750611785688504755473898347239479782517333119687157658082459057359383459908940465073753777992*y^14 + 242835128857986677954795202466725748879057357647315924959912009677229118105338418735091460212464808853683712242216345155599115903187927634066913182297924113531152035730763470473699238735802862324978902182185533467666481094832016182286273217777665111077141502124302487/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^13 - 112701293977450247128182510831020617405877877959898670801268910169593438141958888329954348698987314901838653740060755144986551983118606322582785222063021387578323167876495886993557988142814951904498155380379843192597376209052830346684941128848911140685133466211455797/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^12 - 425486324500345347491533276418046650956202201648333447123410126532303035136027774195927159914356063648391188232191223258747338460972201854023623251498608087423335460205374639418754158332945587943710453973648133948639420961337013820687035839195910220638400022989470303/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^11 + 187357279896239433927542947961183311827262550432041179274274869170035358434355818940803326115400897267106904539855396961055499262872521064155882425505626114632127523679410192718536426020270927513735593986069563652601236638937947706856580862637739052457804161081329097/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^10 + 6669002752542224090422123914922605521324485932255072289984723354729215603511378177905058605373404063645882942633658013571791893393174632098113744848633069617627612450609612059153632867947830259150605012018061048115009556399282120027271785466883175916991164043820295/4075585583361868111616315033171391356649785113373555875773764902540047054184661068325086475779116618682814462918814372943615889012553330734545929188736354107398912799363437652946422126188868474586809869945629333279921789414520614764339845864977235116268438444498*y^9 - 146715117802647222224348015365601085342701108557040561201433784750367726025355863711855838489505470777834000042623189775286122102657244048858458365060890605295049471743711482689292274051049777353142624990344584189965377582696908224901195330795220270787026344561455709/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^8 - 23162768731352858653919270312307813220496662276286567144188552494958893596424072071746746017484514252486076388442487433266019530577771303819342653891193529681320859789194870142555874578570239461801641686408484458848227898012242132790279865702138955654581742643493809/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^7 + 55032363731850275730703142543655165688324484731704203998954829576346348909562142528364529938958238127271697145296855058826699715775336440155416061754136266939990490910764987970626669687521040991798057482603161089200386918760162618303890043702465855360085233046634761/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^6 - 1498214235962637354593198115954108771397048686986371844817580808537893177367217834449462255016968831900756119156098014380727464941587863631669982644036844853510257284394895145009254407146009646249221735450916752967656598680219531130931724925515497161164539498569035/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^5 - 8960343361949810434514330829061112573793883142618228380696530323476391465459983749505457855676987049556694145809926441934644440986147194177880186207258062562616267204235180465201654282460662051877628181384677434089715784366775177672640275530594567570435101386835133/130418738667579779571722081061484523412793123627953788024760476881281505733909154186402767224931731797850062813402059934195708448401706583505469734039563331436765209579630004894285508038043791186777915838260138664957497261264659672458875067679271523720590030223936*y^4 + 24659277022766238532617611222702594742728050974372774389441847359115056733974176590185024755239644052027267475996170317661810538772591961881567462975728652416758327537518714797140661415804346539751041887915327010596267641981811419467898580042006188196856066421669/1917922627464408523113560015610066520776369465116967470952359954136492731381016973329452459190172526438971511961794999032289830123554508580962790206464166638775958964406323601386551588794761635099675232915590274484669077371539112830277574524695169466479265150352*y^3 + 252481640702302519708052266272293677239965807388147819038333363421242289052170798503996832881583224780597158555806348770218751757164734907940435566151719476631703725645697015816442961458958787802262175531759368839036292538842861134406983545467816614690447299522549/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y^2 - 70440117737997701663234066085147684040045357541462841294363550895457984968240690999973892915438204196050328289496113652355316145863233032611183540981412347016086213783719719543705103241149997611572375205957254336493294384923170610495717964169879000577544423538337/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968*y + 1467662424273350790253984734490328683322883274708899034543146698521140165734989680345255929441448195024892485601160945015345162344532260074210083017066713431152733992845109898577563691438255649013939924695065148576474237806561327326397534051450871865735644780391/65209369333789889785861040530742261706396561813976894012380238440640752866954577093201383612465865898925031406701029967097854224200853291752734867019781665718382604789815002447142754019021895593388957919130069332478748630632329836229437533839635761860295015111968

# 4 Loop Invariant
301009459487721791264455211552537448718664008499493015342928979978619034692651125467525214832720480779629819309987046442967344243911370424700655213296800729820453411736313584725786572379384694473065291810173324829628162212397462811142794493814989943077725461091665047954318579845433228189943569110146219915538085691548408716677021094809551297705484150609683673524436347/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^30 + 438570613601079602919628782825886224645151615696734567432613493811795662322369256123336397402421717014066338942083952655327910689121359065048947950486205769265855244835327145634006775759447408737767508718078274844728790433138883701500269069538473903677261901923288965288425662822703707069893742257815018563625407500920940883975318478992830102723606811011481051132461757/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^29 - 22714163624745640657836567448903236160896250118931045021713301853892999640657634334847736985826392852907564610121747116703945759606537101373239590210555704380155114098824134440127374426490199013322793907848037304783328033387197778245533736640869084724473810324394574847340306998890691969823265583099716183289309604396045039863052549689740883303627328740484629582382196911/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^28 + 3200727947200772949421043468906878034817781523274170828962431178312965858056173417781875210622614506981206332383485788284540091585663990210446628747625852297153406507035530966500348802600913705832893767449729350702157236855177525766453532909222038307382182523742521250939631378927816712057121306355910043255155725095930459024530246615363198853324237403922864336064859813/100530390592153054712566425983124027285390573168369970921052936331919484361335735785371495957868708880349355571668728931349550222567789734497278070448881260165548486257666614323229378078212774348496068726381170351915481167506938915701217334095361423040811105953832895960365678214217966064742188800401569669280881832451320194681390180909239863818594819495792376098244899840*y^27 + 236877372288229451373992367443599047225759862615165161249566590262461710190642017246495488017369969063880219630029934112285028956756824459317807917604353845090543575865388772646467269116087500608467757376811826246076035857682300282566709831641430052324568614360563675696008320043824232434772821738171587626360301991455285049887863583849454534546291298237189653703002562227/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^26 - 290204751847081630430933910493287271140354045101947089787831795314220522617615182910761628587904595675544062154209989967176501212899253453559633014214335184585501800341862733961388635564271533958645181240148811381773640939969703175161989963421591815354306250281344616440665477943084443528005817401192350353630618310969622742123812233090112403296186850377079269329378594207/226193378832344373103274458462029061392128789628832434572369106746818839813005405517085865905204594980786050036254640095536488000777526902618875658509982835372484094079749882227266100675978742284116154634357633291809832626890612560327739001714563201841824988396124015910822775981990423645669924800903531755881984123015470438033127907045789693591838343865532846221051024640*y^25 - 742924704920009351129537378462433327572498393619842433091511675446369174052320197195637680101482568779915917148578456252025410128618109593384793943648153219911538648298420885867930917983175116452327803399717069597748993102873158378231946355014901970048491924834525898392273824691959538974533728024133093289483824265353131754813290992239980047219309154718168606232976893971/150795585888229582068849638974686040928085859752554956381579404497879226542003603678057243936803063320524033357503093397024325333851684601745917105673321890248322729386499921484844067117319161522744103089571755527873221751260408373551826001143042134561216658930749343940548517321326949097113283200602354503921322748676980292022085271363859795727892229243688564147367349760*y^24 + 15777889406504571235003934814416581417224517975450678092525935451747163211580607286066444365477258838758981233699528479166182821149298284002244951687176249713426522341790413993897022792682461761590861221333592815986436760978057079274248963305430063508452389292149632791615940943063904060937433136137470628635850195786004971938314866020591549080286643807275146611177937181909/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^23 + 4301432767132852339799883250164773880384417055987017849865821290079912866636463823783571491609470112085224689072630781132595114469340497394686037821768483558682342664603951164894745083633002965156273905142638620021670392015891753303400132028178063803964121821034814351306851792097431314646005979248531467057790154670029360777042256083989988701441478585142331217222652310605/180954703065875498482619566769623249113703031703065947657895285397455071850404324413668692724163675984628840029003712076429190400622021522095100526807986268297987275263799905781812880540782993827292923707486106633447866101512490048262191201371650561473459990716899212728658220785592338916535939840722825404705587298412376350426502325636631754873470675092426276976840819712*y^22 - 14649758931759675634258223670775616147820522802453432969990923141079839757716567046649727413152188309700804940403193695618617253763703815872039874699336789291093111883917210520799230185801134120686737954833244058798815062743524255382308929382938564102648709158495888935439636531828855512526808069218178175650592823098654970348243080839988792029256675095961635551762812124763/113096689416172186551637229231014530696064394814416217286184553373409419906502702758542932952602297490393025018127320047768244000388763451309437829254991417686242047039874941113633050337989371142058077317178816645904916313445306280163869500857281600920912494198062007955411387990995211822834962400451765877940992061507735219016563953522894846795919171932766423110525512320*y^21 - 5575912427800103049363471782186881054411243407292264234622438853209470663856640421331708719447543089025373197712919016884507856872264877969544195267832329137864947941451209411741095145924989643978816247568058848375414199288469990462441076514997184924288317242237560316367014375865718447424030561423585825349614806641188040363843606269737740297914556817344071922483479465021/100530390592153054712566425983124027285390573168369970921052936331919484361335735785371495957868708880349355571668728931349550222567789734497278070448881260165548486257666614323229378078212774348496068726381170351915481167506938915701217334095361423040811105953832895960365678214217966064742188800401569669280881832451320194681390180909239863818594819495792376098244899840*y^20 + 269638903981943966477628791915472380965645181270508809828456469601390839834864616317350681110613012828857209338391767778100636083820421361314236772653692664003639092702548268148734453842365133339425959072313106788692509628832124467086595874227785236424526947388896670596835296094392794391175471399792649775219896914868635595250542652827255938388388164032736058440623217455421/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^19 + 4006131310998090054995775413462524026628248741303697549018471595250311909987402048809695560685218726181998950593221111559319543315361411195244421209494497399647201428405593685111543880813197100568874832864677648617315232620870946030528772513431445684532357031866784243892176045256847625364234755309544315064361176552152814682645181828447832814399326064113207346045131694761/301591171776459164137699277949372081856171719505109912763158808995758453084007207356114487873606126641048066715006186794048650667703369203491834211346643780496645458772999842969688134234638323045488206179143511055746443502520816747103652002286084269122433317861498687881097034642653898194226566401204709007842645497353960584044170542727719591455784458487377128294734699520*y^18 - 814640885619379049189594324555559542908553224578571020494855241857236241601003758024846563357957658190954470895432747934879666432940908890419828295269519614791394777809215072277417783800599084212689868726483400081872664673071810476301491491935466841605042269656228581995738133395137247639676058839336369638762502025535727950801716893327669505847953066355699234227340609721431/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^17 + 290842473721056441429476580365484523085079542785655706484618800514325514541392455552787356917045210535413297652795207488385740152442710178041861569501381476012354222124376593627458397473835140082948096051090375547522088679447993392542000542280051111579103219741458861520958554724505516195824103857172233253763743863476018497377159826100569277441894924815680052339808586634677/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^16 + 415638006166183920611592991110398506687402701406466053756520061522721416172483013744168482172807579286564348295774225588743365140678380755909649437557746649370676342443822580996884587717586485647862454179483518805965268623930495828611444518111223390243737466417977145649254589106417398285231656714654937291743644214548071283572678977304194636822210273969325905440621188651529/113096689416172186551637229231014530696064394814416217286184553373409419906502702758542932952602297490393025018127320047768244000388763451309437829254991417686242047039874941113633050337989371142058077317178816645904916313445306280163869500857281600920912494198062007955411387990995211822834962400451765877940992061507735219016563953522894846795919171932766423110525512320*y^15 - 1080760728396790871882013480802702172951325961136653901310204782825494998455979280407231464947209587226132472412812012681448000275187076438815633675592305417905616791861219630412583798593593023640488513928076091193487531319075798257613682390931900700495121677254053015605791846699173059327698937099119185632635821712490667768223386684542173022216825178239421922753051378538589/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^14 - 4546827296519662839099450466095978849809265671594330457139793576391843881691115427110369023188304539688905686127540800279503077070119524134082132869368169986052623927487692191246658653413462473369654425712160307301647411057380158223943250452629044285401941186380467384004713654739039902499206105922018530256109882563518697060189432052304171478171884430613296282142412920054763/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^13 + 1106067531503888803780467837677968295615407200937623048310324399914276095130862671444956939149995372082207435458553326229492426188365537973675307277145260547044914745913807886496079634632734975081111946455610089669179508338143099734715775636239626913401576220520702496089093539751472974689553127239834028833289280398485284932832755541403237473865821618612278766449513547803119/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^12 + 260922062897943187732439069976115154801688298043635941526710016646047851209580655956755552850379520264432011465314296431342346398028968313531108276619237886375614312171716354448227776562441520359303117004184076888231526083434181218776550435262145324887744352252359560528307990025417770890827853373729820758969117635797464154629184766320735936999214533868087813644927791026783/60318234355291832827539855589874416371234343901021982552631761799151690616801441471222897574721225328209613343001237358809730133540673840698366842269328756099329091754599968593937626846927664609097641235828702211149288700504163349420730400457216853824486663572299737576219406928530779638845313280240941801568529099470792116808834108545543918291156891697475425658946939904*y^11 - 1355583633217832511074868622368511421943652989533539997076873927321338619696047866249533108870546306488942712416352917611486472030002374332940954735893263251983947393067311816886818271340365297811584273826599983110771393321392992798468966909702183368088061063969864167348559022609913178071175332034155184109311686892975986375615342406672960423364073126018981187785565381531833/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^10 - 912771234585294643972689711133091819736766476547550324869333809489119765999569655958879842695714618959014128720964416624077874717936668808345686312215144557814318130781432229208705372249165557008651040390831679188353872981061410308221570559524929144924491986969010148392321246902546384569519918814241161568878423885162245443118980382647320506778078559208353772502146146586907/452386757664688746206548916924058122784257579257664869144738213493637679626010811034171731810409189961572100072509280191072976001555053805237751317019965670744968188159499764454532201351957484568232309268715266583619665253781225120655478003429126403683649976792248031821645551963980847291339849601807063511763968246030940876066255814091579387183676687731065692442102049280*y^9 + 207296754266567975357467676332403488158562279532586214793776278033130774613651082108506329575524644443938395936438905107905356061159900901057892775131916740799730895099566821578028827481685657219171903087941787128543882753912514105838934630458744274220114304845164428596837989062432945176803428651877567478716163292793405532913734518459945016952791101465805191048080627189737/100530390592153054712566425983124027285390573168369970921052936331919484361335735785371495957868708880349355571668728931349550222567789734497278070448881260165548486257666614323229378078212774348496068726381170351915481167506938915701217334095361423040811105953832895960365678214217966064742188800401569669280881832451320194681390180909239863818594819495792376098244899840*y^8 + 18767949579010096792150819824911254717522461802349914465778988198251527454683171068025200905181241152694840093010361725640708602643725333172006627374178276868746828592282895454541911917061347361439421818768919484553248954271284755424857670934078967068613913993808757083328296382688515825775040988285122138008149962642893985537035241230853149824544821139661921436532462279317/60318234355291832827539855589874416371234343901021982552631761799151690616801441471222897574721225328209613343001237358809730133540673840698366842269328756099329091754599968593937626846927664609097641235828702211149288700504163349420730400457216853824486663572299737576219406928530779638845313280240941801568529099470792116808834108545543918291156891697475425658946939904*y^7 - 109380963659817502156539760614249163551288115506831039169608347642594876991404784621075114865324472986249331377009767345102806210621698632616033873296400076386992360570971319429538234430350034660525778339908101864074026870687718290829623176692519503214531113462682341450185051747429442237804022151781405246788053172226661334170065154128419802180106756714451593338694736632947/150795585888229582068849638974686040928085859752554956381579404497879226542003603678057243936803063320524033357503093397024325333851684601745917105673321890248322729386499921484844067117319161522744103089571755527873221751260408373551826001143042134561216658930749343940548517321326949097113283200602354503921322748676980292022085271363859795727892229243688564147367349760*y^6 + 71430630678105428093466292535978204591131602872842071034184667606792146850411673211202928034585265130766561409153806418755508963933967538562979848533429258266461368335050427615497948546870195387048979129803399150304531894308816027818559140513081539795410553461173584968394541300383263083715990643641377376411765979193596244268215244519101932119426778400700876514464298468199/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^5 + 102242384688116199363123948502359217973587248727526760330835901430531780347068735679347037882483395749690142620355392699772412518612746245269387351652517254652651692959427077643803081471581800517113078066913884862070331286177670152171317952380159733370005482138767758614837034694680343791419435266894533855155587178429932725648752743529475187311972838995599764381893100234373/904773515329377492413097833848116245568515158515329738289476426987275359252021622068343463620818379923144200145018560382145952003110107610475502634039931341489936376318999528909064402703914969136464618537430533167239330507562450241310956006858252807367299953584496063643291103927961694582679699203614127023527936492061881752132511628183158774367353375462131384884204098560*y^4 - 122637877890432477015435799768587905389068306048420044988558114909109664455391984092885667421263296725402880727248574849888974669538799395766552592825942621809182762063228277961583476574039346429122520236300962615077389764213072348030152605646059809946725248556090350731013240054384832671354688001155784525201106741928184133808794783325456948418203512336748259756706569981/4435164290830281825554401146314295321414289992722204599458217779349389015941282461119330704023619509427177451691267452853656627466226017698409326637450643830833021452544115337789531385803504750668944208516816339055094757390012010986818411798324768663565195850904392468839662274156674973444508329429481014821215374961087655647708390334231170462585065565990840121981392640*y^3 - 1924029512859336664570381140086537108472264912548933118092522360397348167830636791669772408910648377733919359028799564825241988298366279712550935984256963461118137132421582266301786442845598251743524364869370737857842243467746797637319244161623978646206418459989619098245582093282512364013230266980632059515853460993765617000808152371322733278330510765077630904738086868951/301591171776459164137699277949372081856171719505109912763158808995758453084007207356114487873606126641048066715006186794048650667703369203491834211346643780496645458772999842969688134234638323045488206179143511055746443502520816747103652002286084269122433317861498687881097034642653898194226566401204709007842645497353960584044170542727719591455784458487377128294734699520*y^2 + 364699881506237291615965451250768368504836197065501290143126337864826304773019442934790651022004315360627380704024659322298751386107550553716509688871437977991282722068367296175723803138109684115915238573731267438438136503622336990170656688844890305538943583251698821957771336066883406036653115661519338723431515859927846525144761549041777926374901112125545174736509431849/180954703065875498482619566769623249113703031703065947657895285397455071850404324413668692724163675984628840029003712076429190400622021522095100526807986268297987275263799905781812880540782993827292923707486106633447866101512490048262191201371650561473459990716899212728658220785592338916535939840722825404705587298412376350426502325636631754873470675092426276976840819712*y + 4613328567853358699738708478508642435996040469261117899620060959000172544001821011855488469057005937870036458892432367777018870431957901492819158687960487116671983919921854069333181907362745070846858648753819615921169920320307442763597380508075020721570775304133951490833973299359887122515522557470455103822971099809684462777051819140136272112789351825393018700392436739/301591171776459164137699277949372081856171719505109912763158808995758453084007207356114487873606126641048066715006186794048650667703369203491834211346643780496645458772999842969688134234638323045488206179143511055746443502520816747103652002286084269122433317861498687881097034642653898194226566401204709007842645497353960584044170542727719591455784458487377128294734699520