# Manifold: Census Knot K7_17

# Number of Tetrahedra: 7

# Number Field
x^31 - 13*x^30 + 28*x^29 + 282*x^28 + 679*x^27 - 10331*x^26 + 180749*x^25 - 842052*x^24 + 1782320*x^23 - 1714020*x^22 - 157058*x^21 + 793603*x^20 + 1606816*x^19 - 154627*x^18 - 4388731*x^17 + 2122474*x^16 + 1677476*x^15 - 84254*x^14 - 1437330*x^13 - 144026*x^12 + 1513439*x^11 - 390157*x^10 - 597177*x^9 + 202542*x^8 + 86929*x^7 - 35177*x^6 - 2695*x^5 + 2513*x^4 - 315*x^3 - 51*x^2 + 17*x - 1 

# Approximate Field Generator
0.105299204271721 - 0.175850380008600*I

# Shape Parameters
305390974926377601517650660904649348380989880630910112692442829955263927103544882029505310585207508829221497416868/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^30 - 452576189710758668599207279118392634935269804322477757102788447726152843720153911549654934797161386771380306274597/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^29 + 9929726755540543570382758638269218727864938574882365024182265967974283241520274244940274285065128197592352134311068/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^28 + 82720545936433218844362463006004891414161430295486145766019740210154732109554101271237844883465846568232621942364002/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^27 + 179536951237863635242478866806339156608006348426405449643842908142181657776822036663092705822234178877419185049968044/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 - 1071530956459815258246335000719701268140908122467835002280052480090847519367897530817490989712822637638783903512683644/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 + 56286834989608694505818979321342823671643399712915642562094296468418203525793025374217491612325909770094358815450605103/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^24 - 276195556134453110342768425898468101142392613216762218242968031177802646608759064370247860383990414525093128198348332322/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^23 + 638208778551103080783232543090176146769144404666207468199981191992796360970318960512184179061913541221453853973520497229/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^22 - 741997060876968032744093557854784981311890005852851453319334091477344432337510484705868501517045593257817950226118209738/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 + 209200152288558983569730457235417494022910777134817867893210369924823655315886304385196268646558175442346366648454903526/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^20 + 18322563906781229336870180222632116191167751272458936228908140785779989687281528382251968724581670335630393651817547898/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^19 + 435509314051713040243027858651046205102226357205187719112782100696205196077222669638007959732038907207288584114672216467/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 - 64075869784153622932275571117932927946430843358495888150766250891417173647894261164659968836493709950412272395282430622/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^17 - 115412481036042765452556883038904426876875267134646234010769864310845409797782426598021782697128555286413626032289584831/5461246562863192027622979730223873766186393820573858657419545143325248727080020002702165578116940295137287578109*y^16 + 119584758092528199740984838622477101842066989723302977305609017724649578529680910332555100510092721545790240192306437491/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^15 + 133712936422226308664514869515288845947412258158587832230459925826591165500608189861984296986860089117568333732897356245/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^14 - 20905191699032716109827554619895017747507550173341036830175521568774379447419517597914431966691036237918826547131999862/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^13 - 45976588554572836602024242964156414257475182145829081084527685811696318698356726436149035929156223664447963048431414065/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 + 96284643989497454008836226063810298335816709058963053144287437037168252182801045632268051327121163857890432959140673536/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^11 + 12875621156969468607145631700382120578254076744514360190428837061792020198942763536957104088946643040830661558252703090/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^10 - 262887282222543746518805821580296126038228459547417353603502410552461808395915860582367710588556876559462932892153065323/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^9 - 88694073304066894764321899337017039276780743891050948665326389873815574360201199575124373766262665100185714819674058337/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 + 90189634159763865143735671248414997796097765455982080059034995316821408884839801526995964942335914109277810937907039954/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^7 - 602808356735133712810596582069955640537874275726708849295847935303168569249411538058627763445345884669704820075424607/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^6 - 8325423743848955187895565584213711631995741726297626973235518134702667550857210634530728675536317645603537216804934966/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^5 + 701871981577466979800739713177185287684967358329891206840200921767970137263967533014106270397522853728786017341319757/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 - 3436939976849076939613999669450373349712498368256019213245470023515686294414927507815479702702559094944240574276706/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^3 - 89424063296624578292101820436752814173613069254077410406193122187715939974991379725427469016794769253288612245230521/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^2 + 16295692441797788735020062519418040612562078335927738273256792028230417598344890847943984815376963586051396766514427/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y - 839074978983156227968905701567199572598590200789128406042102737090972496414517521431119136699921018951054935580695/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199

2692317942244419450572942455097930219735965309562310578391270809091248981464571806548616854105795542552960877163/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^30 - 111745437077295682976011400222508043056010153565011943128648834012214412323278725895556836853440766188962277636333/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^29 + 314972404493236060371262470528465373483814567364958469510308570446387506486801176515684722549048335218522079265339/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^28 + 2073400033605180752417844229676526083750064152826637142208171090826053810567499674613013552938756072910179598636110/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^27 + 1207787716010264928941477541592347644641753579494381320134634703416170463905979046150441460066307413971025381134306/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^26 - 87725638782181302946044412202917161240798721348190127854525690904203330357102652818880396604798470432575990010296033/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 + 1530154589065903719237138456126622620395979432800078192151726733919430609757665229404825159899451037585339672653898759/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^24 - 8032524793787164392573236753085175464218017410509740911826668501770206653595445509401906340394513196968221119348512554/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^23 + 6762517999823308322481622229663664520638278731320503579298120878898546080664030169916390646416055210230367459832500939/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^22 - 26951051668239141072062944972495155025848183108047756780385671106779052346731555690518610824914395360252476644793844949/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^21 + 12943082758670502220813603973496737093555225298304261879291715836430082032960209675718051697801275326133389170061483129/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^20 + 4114405395406548264046460929578186990039132219680242937105548313244896795386737743984003533375350952302155101328762660/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 + 8996698499142290042610174930101732133831980124660734959402763672418418544806168463268801427960513646023200233177242937/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^18 - 11468185215103531163417882407891401682534410846031849432529668639753854432976893636642484518441249826858908710050347062/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^17 - 3000209596991389208801156335788336536679164841770876441466343407299105400002165661249369659066251952474216620464155689/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^16 + 45486836785089712846532601332740563124583416500077050410868372861110638652817592912694736856543413889765571233445040538/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^15 - 5454640574246284238621158004522756897594457699684537825545417380219571547061489420415873632793236885995561734562767830/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^14 - 2190538009245238338842293324693443644483117639605632575133021170916893506962067550301936075797205219735997652062189825/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^13 - 3744821443901994762696791906851809836582842753705637619417724880422803081241480535767552795112247804297988098636473285/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 + 2619209803526463316955140681166440683626935487926458401873341939085085251954578134666370817253657221421460238253501366/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^11 + 1056159917811557527784012404030348401730892856089904928893412971819011946585070897862949104403083581714808103964421446/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^10 - 12562400560067227140798845939793781646923575780273524421086289889867362340260148165770376635402413969997144494521720780/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^9 - 187858318168746305270715393016098013604131916188816638320130212306872186909275114346703155479949059578174551149915110/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^8 + 4220163668657738535102209086862690618483487956943100986833976432945496392098273851449786830161867893983643031854367111/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^7 - 863660318077838494683338709118105084760382752786590185797318913152745632947771083402971921148394120273912807293198742/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 - 377264742804967664103391770730751368418491602398329176399406127424078692090337486016205796307613469170593700044896277/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^5 + 141371511727004610202226120281941037878691003008931134292007872371499646161643284074905813999570552826633339587763658/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 - 6893621777293639682318490114342605218684474769362775996180407812307454227402895520158625010450226900593620490215200/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^3 - 4999544079385664878351452168660607619342987717612448743943774071459716015722575331148506890388351968224945499101609/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^2 + 396913164027329741213987690075200488956095932126984852612268087582683188108222291860409180124385094030419233088335/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y - 91075594269650188387893145593238191073017339975640867772364898165012335610390823496023094586893108441907719806204/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733

-46828210631431565045282956360915785336591675275289704133863122377928844411653709290781851201664273961411303113402/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^30 + 200571811358638410989744230154563487563395915499285470320226822544123557559980052790843282201375081890040948686877/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^29 - 1222860468088853730370935778049609996005787474031171951267766633895995720878871471348125152499818357297849081029148/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^28 - 13359232583819136999703806807058898828267693787045492757318084187957530716186950951874116700980644866767364007113116/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^27 - 33883583783258768657014038401031251660305909946767435668076070522014576760596468996142058490129832270966937321208084/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 + 159356652722160114004376776457693536289752742578623972362033986807713473178315828257223958713851740195460668547771711/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 - 8393481214322108466514954799849277224123626315896360778542745101470349022774756808162134267392400251944922412842965206/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^24 + 38191872153530401718724724487739800845551780346424673380599365427444979203244127499667077867056223985219463392382228479/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^23 - 78132689569425147987267863206608099824520176704476583323278855786717493663458608640436290280706498944517017338846690405/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^22 + 70579329607954540706562568467328819666003529741900956416689705493701500674013178558915140443702576555331231611253511923/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 + 13091696081015835772559733766611515838299704546960876925140998685110227250173558802252977666193810761100092471746806674/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^20 - 9750901565686791033146109246319319985509869845292263339382786485818249005583015945353129043895502096575325519834100587/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 - 81890839775234098067321513959203545995677418244967265165958648571401561678077634084264531431914594443972617055221351244/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 - 640581360845212355358763763089862262080606459786085985716470327743287598164346923681277611385822613087127436071364365/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^17 + 18303242807708076948767124943915764664281838498755382327972333317964897103429765463564696055968311008729852325136868189/5461246562863192027622979730223873766186393820573858657419545143325248727080020002702165578116940295137287578109*y^16 - 22524850484304783542168835831798995946660245869255999305323405811965489347519838973733238135063979378640938270414154531/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^15 - 79663592228527587257462219230382375734352494631973491568392249019519253189787730239150779742688895174481106230450830300/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^14 - 5477375433824849015358750319147749564085215685152760275976499082909348386418842338919592097571743615622527527424239908/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^13 + 7230948778918706263081219888627440799075209718882594729596906217944066535342176241569796678450512003432161633029051840/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 + 16432308352052621717873514769670808420285252492407646372377729103862295032328074495053646805191914239008592502272249635/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^11 - 660851842037253519189379298384142397805297751385424797676515420402691090669732234046698488139742812629502279300645021/606805173651465780846997747802652640687377091174873184157727238147249858564446666966907286457437810570809730901*y^10 + 7522035916027945012293023671499210243721709869866518855081698999199759117007592973990204563276853002450382858148604278/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^9 + 26237637715325066806996420461749686297266396478864745355768380695374406999608988067571606466751414387684897916368642027/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 - 3457273777125660607246375439225680892221841128185187169329965449948770883144214416700523877635912798345286194363940377/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^7 - 1431837137626466413327669629032132212013307792830424230987946834391819769625199187856688566359308200097374444304336525/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 + 440902606217454240592237380607785723856148632134602080006697947656554054613328435912388468857214751180102197332735723/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^5 + 105501462043251666005128474537416078975800279788591908596527439114254928345828889179681511620029794673070194513565324/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 - 49952480254230123216540012694782157197283212601863816351934818856723347140091759746830513572889620806646084882548662/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^3 - 6889379705149776062288850051106758541341774583959236078793603783334867852854961926797890864085592559662876828117799/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^2 + 3512791109370334178225797950294968164771132281107120741003007040733858745420759800505756822432564431266530382057217/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y - 487982841231245306665257870456014416242528458841768132191272674622815286354637803642584110177728509321186067456358/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199

-11657568134620883919190252145596143009674224676665680754389883560731665551425507183091432116088165925758923014651/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^30 + 47648898868091302684114609667023574742041525093974928324446515313747857346404433768493384242272664898370171195127/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^29 - 214569428886415433520628415701526525966452963571943105318816310346879372026236137638939920255240704600719946267221/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^28 - 3528901640333934267653004620950683333466515555237666270642619456742762996744362952223532084270424569157524383960319/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^27 - 10336016074779506746009205125892323614020564257477444326939773738741640139679682340774860095243611395214943625485375/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 + 38196638091593464611337286553343152043177280591648797986500259960404958122164924788864731375006860651611160672424578/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 - 2018315749285873772582088100390421343131154692330076081138412649621156808364040824416064074571833196960493807043166568/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^24 + 8261073995044401252587151696313272008488131406347157322386659505335380670126321824975705434636911326943273641135329678/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^23 - 13527106281063558741997389933810967033332752854235343186185658940249807467300131627020140339366160947708994284943269454/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^22 + 4569377774593950314306447095971329871678087131381696095283626598987791760909884732626180767199523831408954393905701654/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 + 16905207062069911320881439946247146658958714689114485201622199422715824403505789440166022945273937015916316824594760221/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^20 - 2850865793386603450756412765852987503263752248342288361749699729542870307201752051763672809468571577415915539299521917/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 - 24974787402412739383572552759738240779287534812336059864927703095470140529794589821531060811080249040968990956951945362/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 - 1327062894858330257388579819354321052302775799921748770852074389643411580946256978555556312414430700305905966711532174/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^17 + 4751928172580582327222973545132306328036432527539322800959647797017348322520261204818641066472470150922909947068632142/5461246562863192027622979730223873766186393820573858657419545143325248727080020002702165578116940295137287578109*y^16 + 4144456414790866484601464142878474614142237850268162492158861652483126242433892195200960874941615555624271399958677176/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^15 - 37894208579478417407368426919697544301436780698353728676136195228994112614279147398469934603405583276934414740576946482/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^14 - 3961031575658016041114137038296565128709052955392545930276100854969398407389401235378747659774341145618198592420828643/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^13 + 1871604109542789618134403861459464807096971977876741821185097670099029505319318696906362804517687456353948112690536558/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 + 13491965035588169423162144693103350080650236370984341620484146964605003767430969743094688001963993186572154470372609000/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^11 - 166214211001491525958673227159956021847831147455798677166839261433721817960949658116001444502345120518530016612039088/606805173651465780846997747802652640687377091174873184157727238147249858564446666966907286457437810570809730901*y^10 - 8005985665135580013621560468303745295804749088656966365089013875922368186510230731299043687784640599849477280450378652/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^9 + 10421670565272493095378623150310923705088299476993845702418307602409318577549928782652796552180145271223166079723223179/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 + 2261393479267591152129845385367126390359320960780431246661284488053745108643942572154505425737187908402649109825858785/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^7 - 883086903700913587596614234039577182364540497862132635012493151837726917690084951304609773080729441444718840097233047/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 - 143003194486366079191757867592012506739961354939706413465241932859896763162052268814949472349641573528368398236293946/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^5 + 92098411649398132080143045075108576783037351226314390151902120095456024476073436674657049810253794723179809320067849/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 - 28330452217241717814821077923293386148030476245318401986715592122499353010816919623495445649912444749460442656520800/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^3 - 8618396926853015898871252824531078834153652821352822500060347846981698182087069409278160121621905954392056404503188/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^2 + 2828432235882156879414436732025285341131781626894427462387932764042431435448647895074634056506695677668908288642629/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y - 225728093860940508937794926028399565335418043440615398658298360750647163426541499661269687193193249880794280120270/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199

-7082292652712562511804662340064638210005835270815464194402763744107583963006100200700777913419908180373458024369/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^30 + 31437812262127908283391093272758818376292771454496285689243611564045000123043325937794378073922951015954442361573/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^29 - 227815511816862262640494974202934722435178268048988619865187677444899601204967444787566211716804285187805410714018/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^28 - 1929726751593360178413162923593106893753358254173885433945246638836698338343212838093523666024035598948929849454135/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^27 - 4188234800618733278227150229408729039844900800216219833270612374886385154030085307469286170552285004822039546650910/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 + 8288785358068222192730289956542118432394477309470185331018418871294600505229626236379774554975694892135067376286517/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^25 - 1303478641668204029300873945243175507350472908884366244972553615873994042285831101346642173261248792378395485121372729/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^24 + 6372866531598773308279737860993442417131145658289714657594308409922426787058008326866508064599671388693947414748110387/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^23 - 14576285908844090338894793128915784359810290880283106224252639446878036409119634261235629595274968598055750956106898054/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^22 + 16461479372530844198649565288823683251337913618250873978417514234453537251017251115468162938929137433048456292980873592/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 - 3506866433945765105963253704976879974430806578475451740211734323030288581055283974737139093468557795447757282961239165/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^20 - 1676912182516527336101393545227010397169052504079857134624705226600647534105573678504224734557605866720039530040779068/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 - 9915637960965596677449163216051503945052251488645560288651255235208465760922243171556214139487274349217498998537833901/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 + 1486920824899117258513180892924180471515128903267343275488229693884481904837070988723649940057042453601945207508526584/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^17 + 2755606054714654162582833038659716705793990165265765680543606010356440304348784345556256175202992086510184207615198080/5461246562863192027622979730223873766186393820573858657419545143325248727080020002702165578116940295137287578109*y^16 - 8181653970808797346630617159315951076978119860046614860821776649895089701801102678215648195696491153700794666077889800/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^15 - 5670023244975436867426167443842151972116392283751480155740228170993404411387235034174897612396716836963920561703066564/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^14 + 945572324143095763304851129433030658378731739134810629205527915512379585911332235698959215332189324663959412967278596/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^13 + 1101202870557692879453486983902396624635777900482160504938210602011478437624194640642427193236591568898230311042800455/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 - 1961331251697715244536341118988816598974739945125589494098761219112113243355036171170428925879145617424505021287303166/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^11 - 320419299088825887030095350299313358210127924188384544249833018345790165946903668728768861230793488471464235790723558/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^10 + 5954542651734320706329545974275452867395026896153285016570871552373236075812365062720685198926302530186683338999824394/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^9 + 2839711710780536318848533342645020366698954743098812782399462656679696732474332321444536089282750809551607039586814202/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 - 2370266318011672652911948309093033424905262659267516277732191093237372863715476120193062043761144352866885678031967458/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^7 - 21382677512491943954163665803133555349899069763724196428905359424908991056504744965539065530302341435229720561934607/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 + 288544502470597421094124172612296296780528014101586304377620252646839045276539491412992232872503895074187503375361239/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^5 - 4948320593326760110272209132440429954184999174236656467029835144992653917467835277357657292405525660722975224496360/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^4 - 5070317229695577921627519055104279425637575356232165422054300201128464952070533588880122295588427569353504886215616/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^3 + 3005595777021320244025366443991374055845825237452774492682065541852482073692842377570177258379306025217860332578116/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^2 - 636849354020706832754375694173104086822139513368239197815758882803920108766246270204407173650045954170235862468878/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y + 74898773707480703781268815502396753245699927699433275409404990215558984434428375114143478847648968187178117644255/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199

19267509123538849144395842354736158032422780611539264420081421697982193553763043365898987610736067997161487937829/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^30 - 6566096646189343303034920938616831927551700883366683583420270481117159142474119984639167044331852023201866717370/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^29 + 357936466242720246920127666284760275487605974446656548613817591429493730947329211928993750947589219874724752466913/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^28 + 5806590457039131556896805517002949507353798777318272648722016705739149326471075481040673696193324144023877429639827/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^27 + 4274074667788329518039302517881247457480852327388213181375743455470272368391113716672214870859958261177241166100233/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 - 15747743066335269345883050502358366437844335981585576940758053173558382358969411351421453763047509246950375256347526/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 + 3338328698099860308992362970934079329742303731415295516168550745347326701004211345784455791434494499022273790870053299/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^24 - 6846628405748033933300842513343418574713690536333450909476495784964273093902872529144538920747854006199988931534178569/120147424382990224607705554064925222856100664052624890463229993153155471995760440059447642718572686493020326718398*y^23 + 22772624386781638097484373912324298010818566080401739299314598282316695899511930425708418493968539996862133015276544451/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^22 - 2301264006326175849353028223274135583529540557614244026437304450408404954886870648405914632129165353804050690576937329/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 - 12389059360525045630304896677896664537459762358949480149781549400350725027744779504905372877574862327629008138977418073/120147424382990224607705554064925222856100664052624890463229993153155471995760440059447642718572686493020326718398*y^20 + 638564788910363126159271898448470410057072177635103629011294118037714938863449388001537201733298361432574946795401313/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^19 + 10148929743401138068156111224328410367147990847210013814133294646676810501073176602107676061517118037424032634669696249/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 + 1739111654080460584138553151226701842263218555302980864984228071028010361762948489642508889865301822151808931933625212/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^17 - 7581482593399297831757556726549558737006931929413879943296079014889156048671936102994136714999255156325030314243022495/21844986251452768110491918920895495064745575282295434629678180573300994908320080010808662312467761180549150312436*y^16 - 553833112490987200177199817962689317866839687940086079009627909687114387472089492130746120525269917517138405821752250/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^15 + 54673798227338402680020843726710516957911931862531618959133314673786583869373925962833099059435684267464614314524639345/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^14 + 3707398365273017019862674681733491843688452901212850862046082948395498050147370408665781704882107504661014170601447135/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^13 - 1364067992706858571850077386594890046386331036515314625792870243472933875448657577331234404235314908605336232735176073/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^12 - 21861445773910920810166989803597531523612213681632402165191120996859685035392638810567673364101701933371259213001884043/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^11 + 187331516304279661729280706105756065336751768414808760264968676478187520671086919749684963093967418607765914817562402/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^10 + 12479362205285191795040203758145807017622257074635126445477108100603774531552752367610428168937251610104560897003857489/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^9 - 3647852371562714048028071155266290319891897743753008468123311130503908680087972688737794873514094036130852216902098496/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 - 4035987375835683648997962110272712734396312115528923112611474550270126078897850426020361606887081930498763413741946023/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^7 + 181582858727690289180092929744779222945054829604080712777436521808869256745619297891942523246287049978424353893209949/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^6 + 443631237398720809151828159829510319479018674706359783847738680735259007342760472835386385749121157798061754610916437/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^5 - 23194641879506010105210148802754428269998430707023037544202641203508008968537689429982596922775325131744253582433902/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 + 6500107407140415223518509689644375426884440633535081473584280738907784182703853297678804254105096890619095102261351/120147424382990224607705554064925222856100664052624890463229993153155471995760440059447642718572686493020326718398*y^3 + 5576590737154465608314366768136728612493178076418130095925354916710872376215180663823667955713943732578957370218929/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y^2 - 2907597246529154328631280083744891086626158465386296029469521875327217579774324751655773928658121795707841475670859/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796*y + 72375547997110643232965412612294789404950509778549559520625021008509325432859630984720733224154999018071366821401/240294848765980449215411108129850445712201328105249780926459986306310943991520880118895285437145372986040653436796

26373312477096516770870203181361748499605231309800322217908335528382228174046860976639873821807325211103811354030/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^30 - 115152853524967281340367202261443235131797462766436111360723130988922227314958273191333197238666429027196854452506/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^29 + 773759941406918047467368467037301254892059828327673980533340538151959848849962926049411575726925422325043478080087/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^28 + 7345485566029323183441461204561028841404006276579555163255395884515251567539113835567674102336384775592447622319897/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^27 + 17215279308352964779936032109107153414779825781300057569870472706159204599584986966355278662262072921602501265479991/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^26 - 91277837144879570582288652596266325832185224178942705053655406986806317266382489516391578793111968568213739733585818/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 + 4794798101286658677067250933679233585102559760325967365057719750707795355941402179325140348207876221343240543021230618/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^24 - 22693551813799183712619185727558728438060710831184164777803390575037824525498669306582100105363956804420363758599277289/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^23 + 49460999575529365981759715891065778089317318284288110727289935232174509655081741609076836564863341510735671093248241569/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^22 - 51089365443761831713299278768952247439071441761088421896242967421513744240227683541514341683938653262856430692677984485/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^21 + 3050885737359018679346483274610595921931743540425583873070829344979575462370083913426284575497516314519493211400182695/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^20 + 6152349220782150149366566870503891216859674459322257100560512844670777262463757638482710044149375013398656839075435781/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 + 40633322686621624051074017566447271942167563971891915769634406332121888294272509086223128205596523113275509765862708409/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^18 - 818624178457422729865901749296502536402899674598617985669996791456336562432416095858625507296872661058413587275411485/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^17 - 10286096148007609488499407560272307403618521002072741363486782399553675189296303585683896264817769615626872694539409560/5461246562863192027622979730223873766186393820573858657419545143325248727080020002702165578116940295137287578109*y^16 + 22335063593608132158906250281145996986417810318414114555981806099539801083861317185512902512575382877668367109789097903/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^15 + 32646397785911737590888868859799633079191894111948869462468518561227388874722229373640357984962740216709700488804334855/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^14 - 945453407814655156801397867984811099310095550292090982525801167023927968479730836866880604763446773123051081275687030/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^13 - 4024662888931844246048669791422318265584923966562404199004606329138185455345035363001423960344671879948749552901823334/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^12 - 109365308904890924903877493615887949945539895461243687821339280014727945457424545360361287857739590360374521920082438/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^11 + 387826268180266639495229757525199444001041391634255741145434401047512671019802594352166425874918082360335960387214007/606805173651465780846997747802652640687377091174873184157727238147249858564446666966907286457437810570809730901*y^10 - 14202454794148429181742481997352110325557535153875544204197482109843457842979849590141234236183693593409535104074319391/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^9 - 12720622011337943892830178341703136651372995798171740285020152989612564583705180188588636410436033645589940084828148288/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^8 + 6080037639968493092446969038403197711312607839981443789330860223736804395213198107140930173882494116392706413133269344/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^7 + 389512142486530910125175589089155045904641868578941567537192861233530103868090176444386052939577471955491759749533879/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 - 836414300768969122218269770470433845921190998989894585192135583157606222259765046799295381505713616957130433775036517/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^5 + 16598178487346139934192062085927642215788917321811466048221938419407773692940559863903819240712372179357515103277068/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^4 + 38043483151855507813943073937614483209370657377085829265818967149600071815972421068312810818972696475851569922588873/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^3 - 8146003963018821299286853402577344056134619232617463733392893860101609947822759130260368485495358590466406875198873/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y^2 - 35187409164175162715311376207238593468987015338648754015280859362566266460485643463583284007607929290408113524613/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199*y + 202476381047199515847500563391478552116858070890474986574892609738522816145393454378112404638977517905490501129451/60073712191495112303852777032462611428050332026312445231614996576577735997880220029723821359286343246510163359199


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

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

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

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

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

# 1 Loop Invariant
1052942545147884620585400645471147056284375446284177729977355314247780507479848081378824880447534760526403589549232/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^30 - 27493749736718906219635806283106103771656191492263850912809771939145930504151520306987671655623340290933306995018771/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^29 + 10113350117462420095676805241289779816481198122375127444601686601330449304156932085843928898699937650282661256397724/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^28 + 294035888403620131824331600949166323003296522584413703263359873662883183009732183668898749133645951880458903916972494/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^27 + 1402467467199750077543483088284990559914443927129520680085083315429120024197062457472047009800034529485768756377011325/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^26 - 10891223294043924605507641671797806776743207686704836566155097382116839343712078896220569218288637161350861417723633311/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^25 + 127324218087499594010428146612095281367702004376278620803855644631782620702204931496286272468832317626938558043864395345/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^24 - 1796438809764595927278403118144480085981191991288201301929550279589453612019964610606211239270708324264240518507276682459/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^23 + 3886857668363008803155583083438262571723837630391220031848196961419708744745996362050849463613426761280517336375506641339/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^22 - 663883042905660852983158848033587657865932998875130096133890800604408333963377660691073103058814740988692904830965901434/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^21 + 77233604547271535776825159320695332319042011994225379945052802425467271053285537028232617718636946877251655476679160107/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^20 + 653814282953683983433440496759264655221369171364928634192343502302798785817656271775758188937427158217394131693838212133/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^19 + 1112066617868310862265486749054075128873510688316781577419182779492665909563103726522493446836691163300419592293302647577/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^18 - 201515538964913121574727826895271044192596213168241185001950943187409512679065433471794334639059967132327041228548062883/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^17 - 270513758996445169061307801946347326833853277081784745985962542116546879046707349952564812195845880872029449577953780997/1213610347302931561693995495605305281374754182349746368315454476294499717128893333933814572914875621141619461802*y^16 + 4935030108856987814544751871160600244846418080691345880240788684006385047814081488344782978270824187384215427078557414261/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^15 + 2481263533077995492554686264264156553756197525387079445705028005465495998096357947635832356006327076010049084774467058419/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^14 + 18884686351387232821184909879182421319904136775675535334676353514021777700262564403734779523214617929699253665502392949/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^13 - 943161654972986914816688556179849904503481356639024487680903541179385827069399678502884917746875485605112764022313589157/13349713820332247178633950451658358095122296005847210051469999239239496888417826673271960302063631832557814079822*y^12 - 63892603191821590813716176395137207091929605374292059760756219384113764861767957092020837585071901723924982785181394590/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^11 + 134152847288556588781273838683814266543192181851105349463686738466196456428759849587940469172319729578915026727734932506/1820415520954397342540993243407957922062131273524619552473181714441749575693340000900721859372313431712429192703*y^10 - 498741305666242843585679153296930589543173175032748744896899106351063597665069451040151057490797985304660851511931364741/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^9 - 948302997356736854541886877059019908861566571419811928142996424017135977710010427740673949750533844495492769453197909051/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^8 + 65388481422510546756178515241926719010804632788441732123143531517119317696804200747187694953818071429460958291423198270/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^7 + 41407288688228184412017950696544760607293927262653227117202896338340016477644764127663428185883245150022267246209811725/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733*y^6 - 7648442093631683085293294990483722739420357728304973743497102243317564675087857213688724679474217798336774059180442490/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^5 + 2512138445368272805896284332115046053781485713346795223231380263254050611063224218644575890378929997964626474054702341/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^4 + 274703988333294780747863929403490595743214969267488232569054582928884688687705726649089703601574759913921881398591099/6674856910166123589316975225829179047561148002923605025734999619619748444208913336635980151031815916278907039911*y^3 - 358671404579061418493839297882794827258120612609825152642910131335739640921437254828025748098877710135375775309689025/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y^2 + 3764395850383839723726581335137724679861793513849317497426531662044009053718904830344644180665015741907357770514509/40049141460996741535901851354975074285366888017541630154409997717718490665253480019815880906190895497673442239466*y + 2025101278872667448911341621083848755440723383002192136103713494743587457554288282132730862742308469124518281126319/20024570730498370767950925677487537142683444008770815077204998858859245332626740009907940453095447748836721119733

# 2 Loop Invariant
-379961500304405340680935657718572726544611299379824146998968359732658830092464034095003765139860247825920872542198215528431941993785063351935550154923639594830473743642792216701453020918961847515872670179862271633129061/98038798236248110203592534872718164206357736593620858095547995978311302346261465919015832422320828384123280431091818439398145708798008093348410640009602423641642659306801798480598441186323051137290347271285374560310366238*y^30 + 6850545974176725719760030694003167948377071611183833199662726934193022782094619755680968559592336343977962661910223519994414063210774960135683464400661746866395128013090863974086326976372321628028231935771427139716996163/130718397648330813604790046496957552275143648791494477460730661304415069795015287892021109896427771178831040574789091252530860945064010791131214186679469898188856879075735731307464588248430734849720463028380499413747154984*y^29 - 13188965091383423397056676456215049732987131923136472922636596011118740260948056900761115620423696041129332816532634579206949479334885227447045954088332021708534255573847141794330747537524318153678908396837824867149155989/98038798236248110203592534872718164206357736593620858095547995978311302346261465919015832422320828384123280431091818439398145708798008093348410640009602423641642659306801798480598441186323051137290347271285374560310366238*y^28 - 407869364356878571223786018281321457007587382599173382108170811810794876484780282276510202473557762464523570058089542385525109473024123442295020706786998515272127338923889795445892036437401441356543246371487566306375081831/392155192944992440814370139490872656825430946374483432382191983913245209385045863676063329689283313536493121724367273757592582835192032373393642560038409694566570637227207193922393764745292204549161389085141498241241464952*y^27 - 1610468041705268233727096347763385228541156015945578960842599936159818218993326697172915484529286604629283530470910181700896882791442215998163839640096708305876690925057760524597893209242896913364605317157832020821694526147/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^26 + 5424650507976024534281531302393312161588706230433340388765537824337690105805198151829044269873668286354771709239868491135057700925683133812135437321624951305855008646318478060054945481092415200636761670341959771905424134481/130718397648330813604790046496957552275143648791494477460730661304415069795015287892021109896427771178831040574789091252530860945064010791131214186679469898188856879075735731307464588248430734849720463028380499413747154984*y^25 - 565643138510285676510636188530034543360962645118160940330711850845547308338063495512890891023096294465798379591537299524249643566416214099954256080994565671577831772112609336671197314902275287107790145846987288446381470407435/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^24 + 2844107436924048582838636326636488955382015508801553132649123007213368618999272499729719051443634930656117616716604960274705672702794816010371356827728867273469038843426201299554948708177946174851026078329149880230061026322723/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^23 - 6712484298391758662599980950053989761406278221770939999141546802006863053102864531735350289492850993325991629259039704708075199009573955725508908256601120722365410519884982193898296529964809643714578091991212140156504444768479/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^22 + 7851590859731519809418168219723199433338561741486062798544047248343976925913493366749807182495635305825629334223540867220016163890117762602183620457451538590913775506318758352150062457352203037946862454619553272116400949312661/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^21 - 466316448770320653634860816844212693948287879478975311725976942829317565497767440219082446021254539514961653153842451416553320642589192763343269274463343311886722003780007988189952277298946211208559548487374856661640408007827/196077596472496220407185069745436328412715473187241716191095991956622604692522931838031664844641656768246560862183636878796291417596016186696821280019204847283285318613603596961196882372646102274580694542570749120620732476*y^20 - 333425925821009506826395880143024933759316379100459965256861111883889610863372738555628542277804809413370275673753015422186779771092168748337649123283925638394248010013057180250217346907456060071889301024690548629784380607939/87145598432220542403193364331305034850095765860996318307153774202943379863343525261347406597618514119220693716526060835020573963376007194087476124452979932125904586050490487538309725498953823233146975352253666275831436656*y^19 - 1835498940964819255020980580518961190443902243815833685895994941999001441987575960475503405822362179965708704105049794814701769407601438314774442093109394498691406053547828405529057147077377861901058236175418807155040664405037/392155192944992440814370139490872656825430946374483432382191983913245209385045863676063329689283313536493121724367273757592582835192032373393642560038409694566570637227207193922393764745292204549161389085141498241241464952*y^18 + 344235417598332934867575706295772687002239983536391791668517024455313932159212350784994467525460777468257159835471167221227203273131405038917617610642805733073652180634783904031176001015325078601615878534928055893006219724461/87145598432220542403193364331305034850095765860996318307153774202943379863343525261347406597618514119220693716526060835020573963376007194087476124452979932125904586050490487538309725498953823233146975352253666275831436656*y^17 + 615579961714091651639677169059636429609364575079954424173061857653161183461131340284057341835502990345628399221146986931435907876916611156335598675010701756467757663860655333717336253988884553967634030320245231278223093392143/35650472085908403710397285408261150620493722397680312034744725810295019035004169425096666335389392139681192884033388523417507530472002943035785687276219063142415512475200653992944887704117473140832853553194681658294678632*y^16 - 2224076113393908141137522910162301506431914542641797231057069838460330209731895957973131078267159910809943357856047927749136914812904349110349873494889570346902228296990553221224233030747170509807390188493487565041631600112681/130718397648330813604790046496957552275143648791494477460730661304415069795015287892021109896427771178831040574789091252530860945064010791131214186679469898188856879075735731307464588248430734849720463028380499413747154984*y^15 - 2701165343973378017886298943715134134868105655528984158764478611397373477583435992454916755327090811030963328533346093239358939902591789339288901496071751788813813362854584446467655741688498692895643772412514286220671754658849/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^14 + 349581114550945152037467380847758520992664416795933965129015823081186682459867569376857816527245591948894035530976272216165775103595044258118129243637202975642565616582050775376733301887481647281589004946833716267536346908959/87145598432220542403193364331305034850095765860996318307153774202943379863343525261347406597618514119220693716526060835020573963376007194087476124452979932125904586050490487538309725498953823233146975352253666275831436656*y^13 + 761866334820197459279347546659931654009354859068851352336233495899922509734376930839554398360369563546358404194350819148702155619316844803929315275232736212914885827960245992425445901078373863128078914901716915831639653139609/130718397648330813604790046496957552275143648791494477460730661304415069795015287892021109896427771178831040574789091252530860945064010791131214186679469898188856879075735731307464588248430734849720463028380499413747154984*y^12 - 408375288685716523447534008105770362350410956355022411031111452939311779507720778511574616836697094700942644087328949387504227310875282129951592770687421709757756968360928449796848124022005984152236809835119635045621396484115/196077596472496220407185069745436328412715473187241716191095991956622604692522931838031664844641656768246560862183636878796291417596016186696821280019204847283285318613603596961196882372646102274580694542570749120620732476*y^11 - 9751698435283432458898915440939953809778614079658254200460212640800665309880019979351805253252585145659862617750703250637276330104354304839052017271812521076765853822658682394071120965242212940911727399587817523303413923486/1485436336912850154599886892010881275853905099903346334781030242095625793125173726045694430641224672486716370168057855142396147103000122626491070303175794297600646353133360583039370321004894714201368898049778402428944943*y^10 + 3475377087525024610399128125633766168013138476141767753397549022198122075599385538385486313567963741126231135561960903769149401286364404134495231932687646645795655048756138386047400036270923660615831741694018489812208534044805/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^9 + 1482868850235218201491423197328677817023143693283566682067581160807637591987248183436473087321832080827944279419358873227725774955972006511032180685553083997646544245561106532049999412886851977272868185402443774343689999647559/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^8 - 780063841056082563314716721520147004825119195134118594089107754752419166770575961311698313426302810215955913778744352963469524481326347846901251676560797472162994042216843682715694817284768974960328747533432029498956319979731/392155192944992440814370139490872656825430946374483432382191983913245209385045863676063329689283313536493121724367273757592582835192032373393642560038409694566570637227207193922393764745292204549161389085141498241241464952*y^7 - 5259951326860721671155107646120520870599532306089491470492314978445981769218747342026917106871911722664442481135433861377774913731891089028602248553211656501188707337921287030265060848033620789758228770904483310721788280231/87145598432220542403193364331305034850095765860996318307153774202943379863343525261347406597618514119220693716526060835020573963376007194087476124452979932125904586050490487538309725498953823233146975352253666275831436656*y^6 + 113884412168597560214602213371106339577006411355886018407387755718713116705908739073025795672869436353805127546872446332144577080473816095834232331145721745670562180587639224963288391191006076153963237808746344177624978123151/392155192944992440814370139490872656825430946374483432382191983913245209385045863676063329689283313536493121724367273757592582835192032373393642560038409694566570637227207193922393764745292204549161389085141498241241464952*y^5 - 9470489421102392372805374087812710924616618397323734566571538007528924846162820508489275191606285310349805710402363640752579478981173589041974622183162034284916733273392761418179446760892484880326931310424789755790396183373/261436795296661627209580092993915104550287297582988954921461322608830139590030575784042219792855542357662081149578182505061721890128021582262428373358939796377713758151471462614929176496861469699440926056760998827494309968*y^4 - 5784405373528008364105569802808708055071672652323587112148269548148536395944342844829928278600202398413897140713262425631022315447966733766333926490805094390344424362776781437161941448840680797625201830804422819091171679619/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y^3 + 273590304418707777406900239355392891998130166319501616305838168749392263436172673273168454439592026865213943792640146411887204473109760837274666579398467429732691347834416798651797110214720123519441491200454604369482234829/98038798236248110203592534872718164206357736593620858095547995978311302346261465919015832422320828384123280431091818439398145708798008093348410640009602423641642659306801798480598441186323051137290347271285374560310366238*y^2 - 582517836864917283397948320973980077104705020108658044691908605950663232466812002626098167369945935300441821926793716330033512639773017906167546573793620054488429956282435314105003144814568557955453183951772030210266558773/784310385889984881628740278981745313650861892748966864764383967826490418770091727352126659378566627072986243448734547515185165670384064746787285120076819389133141274454414387844787529490584409098322778170282996482482929904*y + 7056178102968920992569580271400477406954249210313029304539846087790463302267562694611268932788758784414857790517894686930209775255640744271753969787744684406280795817624270561857585598935936768868093506125832956926352397/196077596472496220407185069745436328412715473187241716191095991956622604692522931838031664844641656768246560862183636878796291417596016186696821280019204847283285318613603596961196882372646102274580694542570749120620732476

# 3 Loop Invariant
12154381603109410793351796743573009908616301022972800774885855976636957896917807968203218467472270559068339566141827271209009489090771925603692998859668243481212461409299955298314024965213547737466570110500893027793863763567911096469010081164024125831216917630967441144341613/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^30 - 51697361473624191952589365522150478402167149703558142834939677067314362423470787155317997426959462926426996438599497126559312706355540578187724724037716892382001054785811242881234024538557572088993901752645527003114691546102743113024438100723225566999235328131302999007911407/944644628748989703111523088194284785235120748890595190247656758371608754565625767246310762459778073938266210910941334247761580438258956977864469277650275500566704367043119653985265977341319392737063053495176261646813552990820426933955952141294306310688616375933291840766393152*y^29 + 151348679137204805444690132206751928709864950177214337126932257517068177084476208965179626805770681548889497940840749068684477421221749533362632269304388539234792951549161398688227551063152112265830496628519835062313574811321237038231965367412881358421603292914451140748321507/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y^28 + 1752916286024818849319703197080660354000725759397283603066865685644075613369338232790997409133760028370687007444870819986469029767681703293718168394041160923656985824650361777167402438160644460024726338387615745399352283498003915293286111979447176390674703948472317372218662171/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y^27 + 141877429912432514232052781830175071376040321330731610693462818644448328370945125902440212080528650373449334400094956053682308395382850216967204434285486457155506683174745621948669393939624964277468468364352886386942119146656786217690150839223046123975883461656152939395700334/44280216972608892333352644759107099307896285104246649542858910548669160370263707839670816990302097215856228636450375042863824083043388608337396997389856664089064267205146233780559342687874346534549830632586387264694385296444707512529185256623170608313528892621873055035924679*y^26 - 1715377710162708497054647421700344656485950405199352698502752114133162731375354730054121588411147345343640410393971199019039683083276302960826203504029299934064805626528370498363551442059117360703050851237355239762769979151144214625013448230500837506947402732957486370636347515/39360192864541237629646795341428532718130031203774799593652364932150364773567740301929615102490753080761092121289222260323399184927456540744352886568761479190279348626796652249386082389221641364044293895632344235283898041284184455581498005887262762945359015663887160031933048*y^25 + 541751643382290680402022893138703572997536290096262555827042484906306799068650407278957620018131626856635278460477679365190166637726744569928112577206948120540909102520240975699429942552121100330463305511221013423831953437231968966575624676833167393600393955177258909973336929121/708483471561742277333642316145713588926340561667946392685742568778706565924219325434733071844833555453699658183206000685821185328694217733398351958237706625425028275282339740488949483005989544552797290121382196235110164743115320200466964105970729733016462281949968880574794864*y^24 - 9710423226767009833719637030849049915363855709973900767495186944570472340696966884594535206648106156665614288280328967994051706532601160651241704259559489415294603835171256878165756674065792219132508561502996052309997447971076443423825546087175732202302111521201237884724000027491/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^23 + 19255253770939686184594813992365141968894726493242558078698558917452589159232396597022175201321684371748139484053868575121738162242503918983159296041527733955050721250611110495976003624944628250755078742500522888701239656698569910734135601048429967524279897168257773172787165783285/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^22 - 7916613997487825293583180449892246609607924449591321412279732451253000072163184936545360711977898387521853363398783822463160727193481803500139668539648586868947348375546742244653267017644717796092739264674121031680014187518493850356692459962200155924158150539712956510051194582121/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y^21 - 6570589833276452130676033656378919505758178045419286060851161670577980662523893284358271538000656533781733680300154341991218689478455256424822971660844182942139148447816816567397340213004924155005588607802079922451098073222119029641405892491084044667019021609115336837402906289779/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^20 + 753658181141233284651791889482794630443225783476243159011221649726094816989592723940403646891026879922699235594662826595003376857647859310059823478903340501038466524874988499585102979543843147460665082880782079496061116748633377809960060880735895323573114454954762883229759375919/236161157187247425777880772048571196308780187222648797561914189592902188641406441811577690614944518484566552727735333561940395109564739244466117319412568875141676091760779913496316494335329848184265763373794065411703388247705106733488988035323576577672154093983322960191598288*y^19 + 1341666893533071171929761580503265713196060623225629030976048046427419237454972250308659586560300797603251880583936396097805737773220226558965995003603898559659381134015603978465802007427935782982453521334366069039560708090292151484603946357142262923879864562047422959421978683281/177120867890435569333410579036428397231585140416986598171435642194676641481054831358683267961208388863424914545801500171455296332173554433349587989559426656356257068820584935122237370751497386138199322530345549058777541185778830050116741026492682433254115570487492220143698716*y^18 + 63685722481509693389934744438376126076128543862940691052164778208726220059547808260215860040410391814388808746080867617852550522689820202279923649587705253653913495676360039001991617949920074489904856599847282929429770438717146242076823540221008989711805164303468815761288250525/59040289296811856444470193012142799077195046805662199390478547398225547160351610452894422653736129621141638181933833390485098777391184811116529329853142218785419022940194978374079123583832462046066440843448516352925847061926276683372247008830894144418038523495830740047899572*y^17 - 2420974281388338779398551703267622755283077499997846426788570679556310808677516884957085497382598173097809273015956668382319923136450464421840407859140372162546001065423058481370799319158744535839405835083311686799746018966837358397383119871299822569176437604548825542639810447015/128815176647589504969753148390129743441152829394172071397407739777946648349858059169951467608151555537036301487855636488331124605217130496981518537861401204622732413687698134634354451455634462645963143658433126588201848135111876400084902564721950860548447687627267069195417248*y^16 + 2203657507420238237138076869465618598055833187037540492380137472087510260024115516739144146576600099962813725809372301431856092008393565567273113204416898595715949217623069674563157463008163188943985025476165510588206264035815613150922411585436187829901343952782704305457420950307/472322314374494851555761544097142392617560374445297595123828379185804377282812883623155381229889036969133105455470667123880790219129478488932234638825137750283352183521559826992632988670659696368531526747588130823406776495410213466977976070647153155344308187966645920383196576*y^15 + 6336527573202972506306540144711381159567738415803829110199565805119090288637417765583900677117148519585543011430541036763482278930183299056338228378360953894764188652404819971255377620342094233088071500886162082141673974612250446551103164452617023169325337259740060725444676497101/708483471561742277333642316145713588926340561667946392685742568778706565924219325434733071844833555453699658183206000685821185328694217733398351958237706625425028275282339740488949483005989544552797290121382196235110164743115320200466964105970729733016462281949968880574794864*y^14 + 1243707637349086854578632197355334250988149265901442917290737933590485595170439563692853023673894607438803777012269713691616508754277893226936961359553303689389282713692929507842118360508928574998877235728646746916024411222268106877998062021907105617665245611944266055873363090643/944644628748989703111523088194284785235120748890595190247656758371608754565625767246310762459778073938266210910941334247761580438258956977864469277650275500566704367043119653985265977341319392737063053495176261646813552990820426933955952141294306310688616375933291840766393152*y^13 - 467505099241918657872642804961877492255434522400402602706005250228254178396745950905962878156107398396132968493152416268310099061802096887029067825813798445178512687198758285243087894210635258025903679522867638192386050112107686119937807540755766895210028456449225255664900761115/78720385729082475259293590682857065436260062407549599187304729864300729547135480603859230204981506161522184242578444520646798369854913081488705773137522958380558697253593304498772164778443282728088587791264688470567796082568368911162996011774525525890718031327774320063866096*y^12 - 5787752856925852602996313432960487288941298959559394091527654116860717915094503046242385597130217513687273273046608754408580676577948575252816468521085849336419261222157918160589699757049848292714419386482408247335503796889059312452971908356547230824940130579448425312303181729097/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^11 + 16657411256968612886049339561799564313742347249445935754952317524000437227673700611650451156763036217025102645598575252543488819411758819433613666414981820340148832977720356352780789487733614588735190001545922133905852867327375477667013758958550268102873152814573127253565414443/2683649513491448020203190591461036321690683945711918154112661245373888507288709566040655575169824073688256280996992426840231762608690218687114969538779191762973591951827044471549051071992384638457565492884023470587538502814830758335102136765040642928092660158901397274904526*y^10 - 598795732583319841995173189688058513367304804149882822733046054152366338052502816160497580754699412741462908846186000518959144549270107885004325658773965777596712813142731325806750410271798494347315499904533591556035870037723233424389879065025864707927280568872042819507614117681/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^9 - 7986548574344232909361444010119280909039083483653277466163661615737400984915654736802080439142690907379210336039870858310995816773006926189484518224213094910739327962400605350102223346226269661671199754376002399306212121139593671071561233376074766311098216526651770085058324335981/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^8 + 425302877073300767068105436661554536262672968685353751699117114219375643796027476321994489961485104703593185615302520698453367445856605710209365174924580637908870065264426649601141178238986414626895963857193741197915170067827585716405310195638422352833807525070837323308904295869/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y^7 + 464954896006366977204579271479136720722614009205354370146018513377820215787605610585214383081925328103029195402694603775675496839565165533460603734520011673945604838303037445971747161765018061514035086620845382105126015224002332122663383457482080092228672094047344380808684440539/944644628748989703111523088194284785235120748890595190247656758371608754565625767246310762459778073938266210910941334247761580438258956977864469277650275500566704367043119653985265977341319392737063053495176261646813552990820426933955952141294306310688616375933291840766393152*y^6 - 190966611646992441006899616725794817066286849257315723692011303954223816492354440983626162685636691903859247075231222555891502179834027229211604875360808862907244873517238243497740549135769693388564495090962848702797716477386825837716441747783278196169281366405059692955463294357/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^5 - 1081926555232182783835321908574647535169426220523617230066384040328976476714203400282744118531383490306389033896346070788304067713005511243735437798952180136650290303236527543583028145211639299654517885610140068150089098174504454849527498071697295865381683523478643892586547685/39360192864541237629646795341428532718130031203774799593652364932150364773567740301929615102490753080761092121289222260323399184927456540744352886568761479190279348626796652249386082389221641364044293895632344235283898041284184455581498005887262762945359015663887160031933048*y^4 + 9475675252782593109505029615460985386699133664077625550805018731899446737662373347486041273750968449735901993375168659161273373241134330484777107563243636209987965922537485298313803400082443123577860474443510955574117605276685828872758604411443215948879162191284782148339539335/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y^3 - 503278197876703071193630351302171590822358575311664407136795756614386792312386963816272971493572052662025540915754014751761291117276750987165338082537246518499195708881098845687433741153823584390851797264483721679121164493913628264447366344343106715734965771917609479489239333/2833933886246969109334569264582854355705362246671785570742970275114826263696877301738932287379334221814798632732824002743284741314776870933593407832950826501700113101129358961955797932023958178211189160485528784940440658972461280801867856423882918932065849127799875522299179456*y^2 - 340541471233946286573706869132466589874131675117023302256646819466412538581989180258724418840851602720580474416606074052778374666914087782615405128685036350428651073953275903113091883329878485037716292671723546660891883225018738599634475341248834260645382227842304625878989361/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728*y + 44480234384832190993961172630683098583884953694126458186885743131303436154180161493683599145190931940170430763693246298741523599047131541768446513983144543489988085755778328436587355765114615484206913655249970495447075532588191606254427901661282181076805219113872786254004617/1416966943123484554667284632291427177852681123335892785371485137557413131848438650869466143689667110907399316366412001371642370657388435466796703916475413250850056550564679480977898966011979089105594580242764392470220329486230640400933928211941459466032924563899937761149589728