# Manifold: Census Knot K8_82

# Number of Tetrahedra: 8

# Number Field
x^35 - 3*x^34 - 228*x^33 + 1057*x^32 + 8420*x^31 - 63374*x^30 + 61687*x^29 + 678283*x^28 - 3446586*x^27 + 8073911*x^26 - 6575872*x^25 - 20170747*x^24 + 82867639*x^23 - 148736069*x^22 + 127835099*x^21 + 79514088*x^20 - 465025533*x^19 + 818829805*x^18 - 796136295*x^17 + 246682905*x^16 + 520008636*x^15 - 1003065840*x^14 + 979961463*x^13 - 624565262*x^12 + 257733958*x^11 - 54251239*x^10 - 6291521*x^9 + 8200135*x^8 - 2335806*x^7 + 171042*x^6 + 61974*x^5 - 15078*x^4 + 252*x^3 + 207*x^2 - 9*x - 1 

# Approximate Field Generator
0.181101930300767 - 0.767456873650733*I

# Shape Parameters
679284165075044604208937277183119119447062475263433562186429508578350472555249517149846329253692878210444336933279811485445636882761745769387612495679/18580715946907264977095163370875574870279082977849971176504691197688218069167863714850048741686393674206126870999104740869213259893471805203597158905930*y^34 - 26816785729933895638641354439326755762313422356801520013433530467306316150194724287628900709128186206576710935285633737634871057840306541800125448379/265438799241532356815645191012508212432558328254999588235781302824117400988112338783572124881234195345801812442844353440988760855621025788622816555799*y^33 - 11082535459215830504495699335819718616751888725779442682469544905113461899932886834283412513987513671842260987002367118805563803519222361828510236688597/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^32 + 194560105640949305828065955491534914502797908973210667533019143228975797935061256571933344651159862745830787409238985770450352436456262982148469768397669/5308775984830647136312903820250164248651166565099991764715626056482348019762246775671442497624683906916036248856887068819775217112420515772456331115980*y^31 + 898866243782457591316578710217115540385551678641537626299209599963609415961697704002223027600699103092373303455000333979162882915341076130853063630554631/2858571684139579227245409749365473056966012765823072488693029415028956626025825186900007498720983642185557980153708421672186655368226431569784178293220*y^30 - 16610983040921014092267410303444956476768245600678364759521054636716498287388785689466052435852237204918883712448241220140539293755235385108400496936474261/7432286378762905990838065348350229948111633191139988470601876479075287227667145485940019496674557469682450748399641896347685303957388722081438863562372*y^29 + 67205546218087600387098164436443416611770273714917877801951513828099320177518752310041103558229543767922495183346426014556946296371767624702028956187028039/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^28 + 131322003628337835044612542788617464947908145348276758296185045799700552605667615393847092650712611786364873660273018548974197959358213188095899772142227583/5308775984830647136312903820250164248651166565099991764715626056482348019762246775671442497624683906916036248856887068819775217112420515772456331115980*y^27 - 2230759432802424236858582290696647902367381963756165161243684528223620497898174552361425631817485483133882500671873778398503736072589601249585356286011315783/18580715946907264977095163370875574870279082977849971176504691197688218069167863714850048741686393674206126870999104740869213259893471805203597158905930*y^26 + 1448807708528940751941277517914545293588354247007764073518493245191504411176144732569184570615836912697758143684232716507911781973227729831224832259386836853/5308775984830647136312903820250164248651166565099991764715626056482348019762246775671442497624683906916036248856887068819775217112420515772456331115980*y^25 - 7462622645573318363228800339324971204885607547764357383052012882744608125717753690806245354792807786914627442982090511304687876648401832170128580144343511369/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^24 - 6841855539281979543808930789545790531415019764231736854994856130553911840940834427188693304369036927722487976064577332767902388480386195110880603003154331723/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^23 + 52815195800267166555078064087911939735182354569495000391071617169507917250105138566420400551887263529137832028776603244766328123703393299775877638406064347081/18580715946907264977095163370875574870279082977849971176504691197688218069167863714850048741686393674206126870999104740869213259893471805203597158905930*y^22 - 506133714413390933080419245762936335243193434230926587413872416704814423179913075620610506661504800674538526683481484837827468758308943769383321797661857862/102091845862127829544478919620195466320214741636538303167608193393891308072350899532143124954320844363769927862632443631149523406008086841778006367615*y^21 + 7541550168307470198585207087176433996201724724254996993540525059276317742503734878145709314261089226013545446715118992137490018817098998399062206151970725909/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^20 + 4072197381240395199574290039387428256565565086253862157705167931818916949027443762656838035851785507729397635187635365012692662774159792144355034281699965177/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^19 - 590600914894070885544243041581022006412427126799730535540816635723107683057644959588468701931832419561506738953600794339578410611884762165510705735542995154411/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^18 + 253170147572141695291439582372931229631637245070860041555594204137913507737250799654159428465122721941156644712112408286986144110492374444032583577377732856327/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^17 - 958453615211512750552933930728972541757895751720511625802500015045835845869090738311959680063010755483740644150945129241156688157402597716635718122065492413317/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^16 + 20720827483433025366100352148855070830421189471782905645659559700694900051588005667487794219882363649882512953847899770335533166409982531387807877227346996949/2858571684139579227245409749365473056966012765823072488693029415028956626025825186900007498720983642185557980153708421672186655368226431569784178293220*y^15 + 659315182680220591727931656036967597118425153178019658114652023336747461649067313070320276715903726999837795761674671414717561542837026309110767708350688814597/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^14 - 175796188310263095964020921382827422408817481705875614683243270874397430701098382839582823034251485065514555868681006308314808556404280308898614371296844018051/5308775984830647136312903820250164248651166565099991764715626056482348019762246775671442497624683906916036248856887068819775217112420515772456331115980*y^13 + 118952901929289715334602200481201565985185421521986059068359193449341174740363582052209040921959528013744072865666522613148501899589789462868344140748549101631/3716143189381452995419032674175114974055816595569994235300938239537643613833572742970009748337278734841225374199820948173842651978694361040719431781186*y^12 - 27004998231178603374668686767401155627247498183378999114458828730935311090753857547269538883272187029920786053597173968695496710864130741206295994288982551396/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^11 + 529402587303953552824906601624416736726280774038318940315741142119794516703361376498014185755668388105685375920325923435542564439531083107257420964629938573/62456188056831142780151809650001932337072547824705785467242659488027623761908785596134617619113928316659249986551612574350296671910829597323015660188*y^10 - 996033017240616003465054703418185911589628887739258893362248085357364283509714562636957606410893424528230485283000606881421412336939509063648169143692139629/530877598483064713631290382025016424865116656509999176471562605648234801976224677567144249762468390691603624885688706881977521711242051577245633111598*y^9 - 4865179852601468016387927800994955208976106313541272866833314082210817927244427048297199599651972862252642945688855242676791227831036493948011510498899297083/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^8 + 8863990341810914864999930760042075856529372450689781270448065189229897342131447752274030935872982898863315799579644357664978650165997680626103593168924157141/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^7 - 2614590802383534116752022074208035360360038943825628337660289150834687207030789949481313734132976682867292987369242505167512593481127043280590813755023234473/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^6 + 56662868189879377692679161091564647792804317925602658860406953532870451388308432185425072390826597036736403351421315419266585926138395177562140293241744657/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^5 + 1513377803877547381438343526629980715151542262518630676307588723761518057116399561215450565883129482783312466829949050681825254445011768458805344832752851/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^4 - 2098404120748656154970027064230457327051591454827474632972926637283817926445134785643523553104890663574783692720101183362444741961265235928976269558110468/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^3 - 122008289450603011791176649681761869948178675666626650936121774483026476115016698867152553837694561936111688459210262629815439900139217288781377237124291/18580715946907264977095163370875574870279082977849971176504691197688218069167863714850048741686393674206126870999104740869213259893471805203597158905930*y^2 + 73407994029633750990053408259965059213907461305299134422224576914232576207629535721209326613966615138692886028121070762886965047672561877063787198196323/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y + 719485551208138417579181753105955328458806196510204120986095784677927989887703259358230548656113402585849496370595485993675346915688826564822324029465/1061755196966129427262580764050032849730233313019998352943125211296469603952449355134288499524936781383207249771377413763955043422484103154491266223196

2909356773941476613410982902140862648317858038909248509274311619334285703314726927021736178162782565195056119807269770148182865649256512978331171922741/26013002325670170967933228719225804818390716168989959647106567676763505296835009200790068238360951143888577619398746637216898563850860527285036022468302*y^34 - 40713052211386830851542514439270970297208285909441769257647765847316502243077016107832882345995499014852556855045878976742022424762449686499247272577253/130065011628350854839666143596129024091953580844949798235532838383817526484175046003950341191804755719442888096993733186084492819254302636425180112341510*y^33 - 190040983528326190725022317808846188430245874428691213072885822079261851333947155330273980912821256782891088809906262503814941235465502321576097501248093/7432286378762905990838065348350229948111633191139988470601876479075287227667145485940019496674557469682450748399641896347685303957388722081438863562372*y^32 + 1200708022457908172677036886466832046822739199435469668710658971256480771521464936751902540400203250862735283391939213347207479949701482533728565058218071/10617551969661294272625807640500328497302333130199983529431252112964696039524493551342884995249367813832072497713774137639550434224841031544912662231960*y^31 + 38658656508982470921974635371270317356928042623271521647055569973461659437824677294196489999240576111877914732896803216191901012419969126437158883377386291/40020003577954109181435736491116622797524178721523014841702411810405392764361552616600104982093770990597811722151917903410613175155170041976978496105080*y^30 - 3589489283284841601445364784917707902966248779439264193350046950982254553618865428918620122408074466899578381304426332669492081937974259221679826230273517897/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^29 + 567220771022022501335331828664816617048642649206157943019194544097476427465189823237276272457021019578726349743900703007273787624802721033089765254948037043/104052009302680683871732914876903219273562864675959838588426270707054021187340036803160272953443804575554310477594986548867594255403442109140144089873208*y^28 + 40233298774978350396046499610884646360694665584718338072464346554133839781770494040307686761035529364747807345189395208070087029718334122094828998274535531259/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^27 - 96264096618240806914234123736501818130143595030361045217177764614644559948469435131732645963620212417472473588002612173114488395620465053709587805358656803487/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^26 + 428695240023639148876452063375997335581776406395237699049896204888048781263577892615379123449459925222036694473105197607932284089005043954907587662035312459369/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^25 - 286211496004143941109795921444286832930667143457706423465712108502076643971718243941026287295699284200670037952765152705307340398241743743450812256530095684999/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^24 - 156510261537273117930996866415776316083982422266133385264811711949519446254094707685002722734478018629948943775692193828274515761139285037134384472880161379548/65032505814175427419833071798064512045976790422474899117766419191908763242087523001975170595902377859721444048496866593042246409627151318212590056170755*y^23 + 81766263171718679298888868311051440157368107466907688211967781140502331526414059586528495482844009633868200964073105239962893676583219468093315513286311535683/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^22 - 294611440635777599930127007892555414595274165496488640247084053664169056349262018448414770225406630814532395112237072438240577999649246329574082398943933243113/20010001788977054590717868245558311398762089360761507420851205905202696382180776308300052491046885495298905861075958951705306587577585020988489248052540*y^21 + 708165651934118200570490166958852072978840842742618420033241387819905956882186036935384896753119010794281805414923846511811418097047232314646398642445333047364/65032505814175427419833071798064512045976790422474899117766419191908763242087523001975170595902377859721444048496866593042246409627151318212590056170755*y^20 + 306095873400467556126855313085868001348966652222492008298525398801573400961975404933660375429955228505547271863240492024440453686814967161844720243454771798847/26013002325670170967933228719225804818390716168989959647106567676763505296835009200790068238360951143888577619398746637216898563850860527285036022468302*y^19 - 26040950415737392405424806985865866585889576563694047617497792657264449225894675897604071645335867772853129014907868630968082422987235348608044165573120716948779/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^18 + 3001562452585228553400247047667328529395109075885691279127411466169815308905473363490303372793745036789648013720178139804408102826645705033909129823080909982711/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^17 - 36569205984277545886538877902779996328147483400796783607408444514568764663435131995187817912893078187390377653969922370089965711090757805065394698292754228127077/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^16 + 389262583850802024455426731830500743569454209977696192794317574676608248645801412665619745101903172965314475409289698310469005453992598428964131509520056105391/40020003577954109181435736491116622797524178721523014841702411810405392764361552616600104982093770990597811722151917903410613175155170041976978496105080*y^15 + 32790064825304484651521604561268995951571278273762609849287205733180038502768449628270348795300008628115316595549797172258705290765399056345940011076201044322087/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^14 - 51768295926172511090316130949669415853077312850747614226576354574449018545415674777711279319953147667452778546055855692007523192656683813208632431515780463569983/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^13 + 11249668896708379862293129547168175048527080343051232446433100346374898359361475275014328777253586595979711691280995960450425118480479873920750152135423006022737/130065011628350854839666143596129024091953580844949798235532838383817526484175046003950341191804755719442888096993733186084492819254302636425180112341510*y^12 - 624703143977154563252334287803079140704750135696260136160889483698090842213156897943708189044934889026644635008633377582594122599015364999977055040079228742046/13006501162835085483966614359612902409195358084494979823553283838381752648417504600395034119180475571944288809699373318608449281925430263642518011234151*y^11 + 67661817363512539300060329796996613831232415778786024791342719542785783530791394274921699626527365555030631980689905464760273553775752757021533672332583825323/4371933163978179994610626675500135263595078347729404982706986164161933663333614991729423233337974982166147499058612880204520767033758071812611096213160*y^10 - 490833760285769233580717568667156888902798502774124260180891909370146693250795002287742505630613022363530036677091232753120655098339746963534947534925552289/530877598483064713631290382025016424865116656509999176471562605648234801976224677567144249762468390691603624885688706881977521711242051577245633111598*y^9 - 166396069644131370674093474902902889546698147290104665570825241797934673526066279001563277009512836302068770087323876318417930753033563882731409744300161063343/104052009302680683871732914876903219273562864675959838588426270707054021187340036803160272953443804575554310477594986548867594255403442109140144089873208*y^8 + 368233250359878196082735587355837954828834537913739586545084029610986975804788234933916480155361417822199394811867623340820812000145858724921368694339085165857/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^7 - 49268631688189275655240771448119118085306041867354255294410787640306562929244706289998300022711706103727000916051017631074389490325013542857987718762273896879/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^6 - 4771547905080294098597061976076257752974355173239662082305861711295050715184907013654811541410307054036938023844963476379997275721395161780554460462083784179/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^5 + 511046924813504504023380920076120694969722484869743448529934935433397229156714781810359129646210303487025276131026418328748284818341563287646129422524969256/65032505814175427419833071798064512045976790422474899117766419191908763242087523001975170595902377859721444048496866593042246409627151318212590056170755*y^4 - 165227587775549970994580139494363594128810200116813804515771253795834552968930990792394680631694242262211665151765350446052587432716022658946320033766462481/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^3 - 6875164887593407030948248373595260878359516754810153723552929738457857129149778449183408919584777931682050975961961843965427134456607314816218548493566319/65032505814175427419833071798064512045976790422474899117766419191908763242087523001975170595902377859721444048496866593042246409627151318212590056170755*y^2 + 6388805989344028986781141486722799387308129820688074212581703092333342640276050092771292145723935581108504815507667483835834662739397406028006597816568933/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y - 31019141361725919902702944849790985985665058339289412725779249020056442843708202494621110125215424221864615912606220100834172476752111466474217862999897/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040

186593116754801355734463497505072698068031947593594401553705560829086167124300750195638393665294233947831640615846257537080051327440598160442410307591021/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^34 - 265062357431480432543275969491892438612209121618478492959304326762865998622213197251016051862368245751917887709436606263865261993976298905927874498566139/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^33 - 761182684319924467586720684215400010966773121480314322855205238988296691461760533890844914409751726253907461550079530366035461323824020462344925870364072/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^32 + 54414859779084895720913728673931710525625950483327349470732430377659484415450237062009812253751694786851917391720624028476183539274328332313211865417679807/148645727575258119816761306967004598962232663822799769412037529581505744553342909718800389933491149393649014967992837926953706079147774441628777271247440*y^31 + 246322137119068778507879117820507700832635209746044875668558522239898694399579379583910071535853528980965038505913348940905880559273535249521048271332450957/80040007155908218362871472982233245595048357443046029683404823620810785528723105233200209964187541981195623444303835806821226350310340083953956992210160*y^30 - 23139337118827675591535572362862701966986500170283864788723969470633883868593120869746807817725508849117524240036490616532671563787759677732386417759216728611/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^29 + 19366572278624118248398652957724620538294324699163309134241666952312500494474895025027298751993863674739747252492893835741967805856268243636761496403128928161/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^28 + 256068670822158921925978180966154620224311570232972031243255004589459364647544594324898988221822856107039057078872343373397439719925155737321841768488071911831/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^27 - 622755540013685032896902754220709140729914670622617560894864281804437734918716186288269769120211859920167878304281340107561880933041764903946876844206777288073/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^26 + 2816863289039971545287456926460921798604199443117365229676896435510266067874079274065359536235070924104726648085731640804007628134417708830005314191591283728301/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^25 - 2013200623622228671807761267842858688347523922836474721726396681377449107187058450854574946018514879465585317902695785489882039535167797014518360600638673396443/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^24 - 97932007216725773101746252058583912791981079639166799900523556997995290645266605539828526192220368731195101210974514433223387813980151374456886908057771993879/13006501162835085483966614359612902409195358084494979823553283838381752648417504600395034119180475571944288809699373318608449281925430263642518011234151*y^23 + 2119862507510735449288939500748558420339715666098555626063750217143968577938571812192352753002030688234207767149744344606362082424703713888625717532777940482733/74322863787629059908380653483502299481116331911399884706018764790752872276671454859400194966745574696824507483996418963476853039573887220814388635623720*y^22 - 977785574392301935290265707717656668514413513987440501674910058079662705423612088754143633446046866677713457375585604009145481308078380814665343278545501787723/20010001788977054590717868245558311398762089360761507420851205905202696382180776308300052491046885495298905861075958951705306587577585020988489248052540*y^21 + 9944366725492013905664716190112128931565842923474871057678451516238394803318870306152522300453859109184136777921997968180903858468650148643104371733113513019309/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^20 + 4473650575562567275091856968877523785140000927071800678131610101617126025762097030909926891310467488958972005870700415588168253606263463489603390742712359765643/130065011628350854839666143596129024091953580844949798235532838383817526484175046003950341191804755719442888096993733186084492819254302636425180112341510*y^19 - 167776893157304172355747299983763911132835062981235276776552975634839094628680153034479813811148980414931746757590211879645337604516412413265236853771766772881361/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^18 + 2493192386376781894440605441121485340554759443150208012330894748268296200211399950980667352452866341568319983311647852039100994657107605703223811333261892589697/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^17 - 253586241570960617602256122002807081269426625695925717156212412556322928800173134761285097443906421550774634911929068618597789116492667104157858487142460506873219/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^16 + 4067042558245319973034470424609863924932793796840362831643296197367543814976199529795547729845966785055543219010468233445927270050779778086705149773175104918319/80040007155908218362871472982233245595048357443046029683404823620810785528723105233200209964187541981195623444303835806821226350310340083953956992210160*y^15 + 201793741288509979821132088349276779248820536525257509267282266057202832632738100885951633038559400810494456640923488674143230247038250308886730259735408813865979/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^14 - 342593124183497465403404402706677872608318927497711076629391430386905343720555338657387814950486909942399850731799946901302323644900963080193481446995221756345007/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^13 + 156211841953793845810025254282720849789115182855947327309283905191045826087703077891719279538583937585329440354830239455352309162074866005107466800015948793767237/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^12 - 23092459136711631724045558661837996745946183556201675401717664786683124494807287929818501465728650221005939078844672770021527581905283390914030152229134765591909/130065011628350854839666143596129024091953580844949798235532838383817526484175046003950341191804755719442888096993733186084492819254302636425180112341510*y^11 + 568966297183848205494807364541379742089298824608899148231500187236644025517876643720947887264966451169424533198207798797197364430949175513318024115505953295559/8743866327956359989221253351000270527190156695458809965413972328323867326667229983458846466675949964332294998117225760409041534067516143625222192426320*y^10 - 20057708950382362920745530114260875813161740030939810378740753693737991541908265716200502254862809633916381297993893599787570883061179678367891745586712799485/2123510393932258854525161528100065699460466626039996705886250422592939207904898710268576999049873562766414499542754827527910086844968206308982532446392*y^9 - 3876711025381767063549876377343599438246982222972818095607734527679328831291127597048395330317093692860854732194484145948192212482999678856979566305203066419057/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^8 + 497152817677711130085137611942809994012996247004078409386423305074823751233300462446522307579666285426188596892865035159285096858446499309936341240446168039295/208104018605361367743465829753806438547125729351919677176852541414108042374680073606320545906887609151108620955189973097735188510806884218280288179746416*y^7 - 500417191732639482201395259969106977940788370464816184941673977348161992693095168994453532339090026659089395203063651288015881065966014502821490539701065997979/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y^6 - 1382375691818544913497816205368360908674702740661306426732069492530556509405066794788497628971290476872298033713855885402281521956687931654808161861308175799/130065011628350854839666143596129024091953580844949798235532838383817526484175046003950341191804755719442888096993733186084492819254302636425180112341510*y^5 + 5461887348958824375082958204300730517070318680035221084393065773837154515999587606180908951578575782530616713834522719263010016602465992637518390512282559549/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^4 - 648287339127246334891691551243024719443578805930523189232677517501977602977694233999706043605812543143224635696531542180061830811938884577936240053195626801/260130023256701709679332287192258048183907161689899596471065676767635052968350092007900682383609511438885776193987466372168985638508605272850360224683020*y^3 - 119208226542040930477402122560586131654356600712640192807573943214814779309414729425349821014754930102224364647927145445497163285817638813665319484205135027/520260046513403419358664574384516096367814323379799192942131353535270105936700184015801364767219022877771552387974932744337971277017210545700720449366040*y^2 + 39829405125375319259978376647410353471076713686007607152167950324057141284591329287559114074998559199644367500762384678459392958085369833929068088164387041/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080*y + 1274104205443788973812558880160479621324482986264998643830687430487751997237291337726807189073633402651007369775621529649416879282896634166921211704420349/1040520093026806838717329148769032192735628646759598385884262707070540211873400368031602729534438045755543104775949865488675942554034421091401440898732080

4034305646252901584650937642244456438168545950254740997538826325523441008691963851948585777063676244862064627686554815849245544948025550595901269495945/40877575083195982949609359415926264714613982551269936588310320634914079752169300172670107231710066083253479116198030429912269171765637971447913749593046*y^34 - 28881205263187647987114169741516263993632456870033176031888792738888049159835130097576503871247730658680506396046779003678472382919021765083325454167989/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^33 - 65819254363952733201009102252269153917619727919844179341943633485139527058985513555361645735921680915180334224275516909959220020684639789532606435167243/2919826791656855924972097101137590336758141610804995470593594331065291410869235726619293373693576148803819936871287887850876369411831283674850982113789*y^32 + 5912354184991347247616367949225277987360390027554397238978648421451716024643558084192775736892863860037601958081087547736054148024524953691739977543698431/58396535833137118499441942022751806735162832216099909411871886621305828217384714532385867473871522976076398737425757757017527388236625673497019642275780*y^31 + 26576980433273051582079980430807246013162320460577781217160839472655131436916511029921944830822459367659540281877244324792135328569115659506769462535612293/31444288525535371499699507243020203626626140424053797375623323565318522886284077055900082485930820064041137781690792638394053209050490747267625961225420*y^30 - 2510079120846153404734074714637872864360417457537763566751466160168512080867885074619325282145267145976868034335442758923662796306266359257080302106920930851/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^29 + 427854498681958865778400124185759133498817322513409120879031348362699490193587308862044997232493758716116761897104138805557913000825673248847656775641029065/81755150166391965899218718831852529429227965102539873176620641269828159504338600345340214463420132166506958232396060859824538343531275942895827499186092*y^28 + 27691662619922232859295555042848253364416032789204774164249420783170183953621369462262710963955480097806158245101293417490816048348480804878375682446684412747/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^27 - 67627652657707092037957205551013878814630018969699300756370478346613021608737732396995081258060282062787094688823265466326356117673546867559482803630708061021/204387875415979914748046797079631323573069912756349682941551603174570398760846500863350536158550330416267395580990152149561345858828189857239568747965230*y^26 + 306778626880635359291826967088927118839769087671396493996878904673967354200570086922214288485921250637003206407737881164836968560012837071205347179639393823017/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^25 - 221682228528824111933459434861963648201570083695581402508848930976358677150004499033307508663761072899287416563389252180719831376060389510053849473626021594967/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^24 - 211726150666181271489609139990257352349756985082864327820538889696949833045196056047343591116563753036960495419622578558629804463828433145776705797665403940583/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^23 + 1613397158963211885254193737079311849361833892159043789391346422970435050087527148244249368498940939382527887701735555314565230535469170305343392802135866150297/204387875415979914748046797079631323573069912756349682941551603174570398760846500863350536158550330416267395580990152149561345858828189857239568747965230*y^22 - 106626215439030039346045449921090077760645237192170977199644896750019801644826119039316839191289280905524217996084572487336023569938890865001904309791114092567/7861072131383842874924876810755050906656535106013449343905830891329630721571019263975020621482705016010284445422698159598513302262622686816906490306355*y^21 + 99180186445538111701938388239211390270750741114966206433061555206684203131209001252849655398486533784759282859710350245915367379150608466199357957825534735849/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^20 + 192295294581890770422022369033006257359616612627653270983796424197748968105778537937688806279896721998345355899535231098598995660564125157581631989923345671726/20438787541597991474804679707963132357306991275634968294155160317457039876084650086335053615855033041626739558099015214956134585882818985723956874796523*y^19 - 1657967510443661333423540860779193815757146816192410365204021152442455001592680636931530126037976319477973104117833535678621273389814214431453013044745794770587/37161431893814529954190326741751149740558165955699942353009382395376436138335727429700097483372787348412253741998209481738426519786943610407194317811860*y^18 + 7612273142951826455631555544237320550968112026769725277196506680178719926636707196450188686879141378897623129525266031165257815486021541541513081813717192838748/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^17 - 27758669499208545551636255381316927938914848269650564433197974772477088903415890750519461640935101031736761181864662064687708038807965992295815913507628300033251/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^16 + 41515975039347990477756610933542469057114896536205605118726127153920535671930074824712293129349427156646778661663045805149556872695042561613306782766230224113/2858571684139579227245409749365473056966012765823072488693029415028956626025825186900007498720983642185557980153708421672186655368226431569784178293220*y^15 + 3124676147319617324322250434247071161031281577980819957768544385508624986157435098755666131152750566250248345229840336242921504731767727466184380003858388764393/58396535833137118499441942022751806735162832216099909411871886621305828217384714532385867473871522976076398737425757757017527388236625673497019642275780*y^14 - 37337176720844017385122176002119748402038960595348193255910009008143610606098614790353835235612694307820210995954555105937377071861903841733640252376469757868099/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^13 + 17080184221000213148204390343267309131733592276026555285163688392017658435453872703651748711234272708865540752875974712572852456766086893626576906328468799505327/204387875415979914748046797079631323573069912756349682941551603174570398760846500863350536158550330416267395580990152149561345858828189857239568747965230*y^12 - 1014136909667857338252464041673843424646765537244216112978370402213289501543616663512477692761718787458791415796794440866296381445354614068741195098018870064650/20438787541597991474804679707963132357306991275634968294155160317457039876084650086335053615855033041626739558099015214956134585882818985723956874796523*y^11 + 63017091875323494684103595930998580173363711695902823701211731150808678272989967701366598515604395486872040682455464789316689234806602672956799936076470019299/3435090343125712852908349530750106278538990130358818200698346271841519306904983207787403969051266057416258749260338691589266316955095627852765861310340*y^10 - 16280243822923261044352474891675932764454831225373592593556254345699300659232589915518605145585955021707514751504449524188932222668675267383032034557647821171/5839653583313711849944194202275180673516283221609990941187188662130582821738471453238586747387152297607639873742575775701752738823662567349701964227578*y^9 - 79239306515667987629359800902149247617240051245006978029146558735628402236561903945415988898717154143701263161975805724239488149659586353743127186097588263973/81755150166391965899218718831852529429227965102539873176620641269828159504338600345340214463420132166506958232396060859824538343531275942895827499186092*y^8 + 265305038735812432804545249860596879977740070483413471644608747235147381592756799335835856209191345022920949713205300991202177388938261698612565325275099901711/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y^7 - 7853142257968016100298450818032126486154047855531616268352183757137509497074214840720234751075623058546587404259040842234853500914786390797052154841800787601/58396535833137118499441942022751806735162832216099909411871886621305828217384714532385867473871522976076398737425757757017527388236625673497019642275780*y^6 - 131840594812956540918110742013675388837622232217341737516622875077108664268755182000474042524423004341770922137147043740705356967272272802189434185723647996/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^5 + 545321357890577597415731562425251962215643686572040757832536455807797463413977757689447624924448324163671272762044201742592786476498975899108893620276923631/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^4 - 63964280842611920272455022459811280340446258819294415977176458512894691553728605882426811200000203788579932783210913432246750721865373993782471250707121809/102193937707989957374023398539815661786534956378174841470775801587285199380423250431675268079275165208133697790495076074780672929414094928619784373982615*y^3 - 13330208633240289395928832024102568362320754025404100216463169472590555315128720854470751033278730013204939435993897855036134780124156703220957374768901023/204387875415979914748046797079631323573069912756349682941551603174570398760846500863350536158550330416267395580990152149561345858828189857239568747965230*y^2 + 3514117287820381659666852248827156541676316887587569849867889634791864752742213001394439750863040617618995451160970681211400092338131921979888216682505129/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460*y + 525465591232893997203862895132901882817562951684276587000322260871574161573124651976394323158865114946639386265517200379444392103142429202152884436529429/408775750831959829496093594159262647146139825512699365883103206349140797521693001726701072317100660832534791161980304299122691717656379714479137495930460

5849948981701580464362052077819956189088189691657288333622833618987449207386478778458801613869083686867007088652302424175215995938409083009599444722151/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^34 - 16673563303746219744172549420118624935649300179895846186107815395225870694699671580271514910611584564527254683264953580485671722369486435724801870321886/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^33 - 190892745734406174948959512694367331387454587591634755057929005228931705965352125213379921391390941800240162502773511063474099740555742924439521410190656/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^32 + 854733258282959824182745016945756555096316307508381540575958454044559517193411661101319894645129576248988964822109391712541916402994772259461221069940409/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^31 + 771452423010830024947169185581248167389334523833781367932826591010896620136460974742750678906127611281839733878155459776693541305221556707114476286109089/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^30 - 363186424663007627733112003979121934285392458888966008676495470897000526623399579387489111619906360075040694493271779561631317541882909773162998849588634186/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^29 + 306779964342024368046820550522743356095505595856915783671617834472778310028703469776239897909550107294681801264646000773985236031222318064221697229461494563/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^28 + 4011619943876435185088731514201446528391545235379726672400545492747096734696724894616035017866487014094819679815367257695889296021976467910400853796028482944/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^27 - 19559658131357246310283950787998057969645397053540258679105502458698214796922630146391311910837154987150755577412132099837781931706832091807658643295053263359/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^26 + 44327228974147204914812491052267297371087226975942713823300455611829255296502690034184115554430443887340609162052527734728511016586847917273162523729012566754/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^25 - 6389882840267439783663386410970113337742192259778571883560467507466162914636993665679112389605904688891526677223701979635162864910990520849118937983428022358/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^24 - 122512544930452623871913253817350766483783929834367923786634649520255295110478110009831411397400900563989599667675851518348328870078301108833288341364568186591/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^23 + 466230994971704085467079577297074728022536468034156206878089978260627518799894153868353197594148291017905322535245098151955155722819694357837718677791087129883/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^22 - 12323454008828388884823391044988620564587621883901915651410369523923011598680794666731066110449886607559579045723358363910494388719274253341437602541325396968/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^21 + 630698298257286092101583553801509212917721600495974932450009893247679648478726069712519978953554073735580120782875426522176535809778821990047543292337561787456/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^20 + 554756136590405897955321013111110169285446039631073796354842660758456153921634869810904016442170937863681961069056948283041681804610789092404008293651413728787/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^19 - 2633476754493628465420923841432074153751553103708679918386984234037548679807742890992166632203210129664694237282248172468840899751057808290371837946311025991494/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^18 + 4399060591042603616608550906842778046532596329393269889081993181657848520108247625133163823460298645894031158168975810471403566065652947047578775962154771294623/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^17 - 802886358477760658258735395178908548669576963326473705572076025388311026091229893794154001985330165380089106330668127766063846648700500198292235899835074635878/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^16 + 9543308362375794212479238437280801034885101054761993577951470827878392218058673434505120169660022369062369339161091957822755844169229019548167032552160462203/102091845862127829544478919620195466320214741636538303167608193393891308072350899532143124954320844363769927862632443631149523406008086841778006367615*y^15 + 629547890507123530531827967661963990248875383409706452661172372012386709643129434599137654378972705148304049165083385174107750162541867268328887092833083704411/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^14 - 5390864026366213217598265678885712015044179993058406528810284416027669178004310325005437984990474859030757367037645356855322963698011508214161954403632021381453/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^13 + 4943739878421330855528242777618764130455397454748723612115252308769137653626980034140123382681096969210579341986339560786107285706365061007874869692224380398899/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^12 - 2945356942783104117886658445315400355581168812545969745658748527314315931830249218871087236893757564376541242888996201206774446456598639896550894459359181224701/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^11 + 9215281063717965172585504008715911181656565553478898749588725334620955241678911288841235863641782331727695919416069489330795300195941243629377598984767285619/78070235071038928475189762062502415421340684780882231834053324360034529702385981995168272023892410395824062483189515717937870839888536996653769575235*y^10 - 4904214345158673697417383193758816342745511349703010895256411708938473121327552998307200731207277889526804816727659648596896761642968680402974337005146987367/265438799241532356815645191012508212432558328254999588235781302824117400988112338783572124881234195345801812442844353440988760855621025788622816555799*y^9 - 55003371260679020223933936055330017259360602833475022242722610718406209977334854561892174603525463391442457846310440026505185870314201039032351257741623249566/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^8 + 38079404964200201760156645814468815197329943875754316266597323444377945618253197426105619324001139231314892686833494639046287029162342993391603721876065705183/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^7 - 8042625736244514469538651374173233326126668836208797430798348928857157481853782924841136027279151960846068044279930272029874076264331821635183499551854151983/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965*y^6 - 2276089181233212193743393500698176142816577441270403594866421259384647062382992848165812001435637707455046012395729360677398775568744497518237128296573504/1327193996207661784078225955062541062162791641274997941178906514120587004940561693917860624406170976729009062214221767204943804278105128943114082778995*y^5 + 59755450676054465729384441163212261984041197369499865628284542849502031568988455834345355527755284331068958472877403360662536548556872569864400218470956053/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^4 - 7042592774524973294924201267194683040498885909660462410026094139187563192836507664257203928711221801456582365860591737537944177922312578046139999790974540/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^3 - 707289809789681020140701825104246950716784979612655400495783245309921728488578020426238223230309083643506976509422144158794961452057703691000252618169551/1858071594690726497709516337087557487027908297784997117650469119768821806916786371485004874168639367420612687099910474086921325989347180520359715890593*y^2 + 11120338663858360709728494677829723753785151274673412886898258045074483302764985198315104352277035239163866987055942457216911397330410129124579812054745/265438799241532356815645191012508212432558328254999588235781302824117400988112338783572124881234195345801812442844353440988760855621025788622816555799*y + 59852611945816698159489579234578834652979674597988069464858557422000519704624547707278708146305888366070036802304190362971466663993253005533866492017089/9290357973453632488547581685437787435139541488924985588252345598844109034583931857425024370843196837103063435499552370434606629946735902601798579452965

33554457252343813222121157592683736234434942387947523728558471297765326289634198782513020746748106031103/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^34 - 96021220235970731234587938657853973175510829875656307627733928370916883055662430076731871544690672522443/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^33 - 1094789338265667483176777381651402763929799910750782261287774007840026996224579455693763029742616849672478/6014557595698374340596793587386287075593390564302298456941034603947138919413909184930274273439634571957*y^32 + 4915193946159694104952555253219038098077220063761495437694436146694630002891733368356254179616515157009624/6014557595698374340596793587386287075593390564302298456941034603947138919413909184930274273439634571957*y^31 + 287248487377724947052370597064042145772106042449564970979229983309628306087425983388996200990465098872356484/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^30 - 2086565645822867054858716769488711487877695197520674507743667440259241153253504886549133728731325971388766493/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^29 + 1782724404504459919288747030266225916325785337782509599566208945334708653939966010386794439740758814962896566/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^28 + 22995351548100313698681398272479810958926676983429959558822650318929097891942576733824945622397516040054619770/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^27 - 112458991250717264746269300870540020711327561482997188814071298266025017183586493863418990015489862958909273083/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^26 + 255478263666456896951108133945341549274992624370554153516201225435476169772384859324051515645169472946257593632/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^25 - 185877156931726910588786852484029812232334247527314840303935507357806672271032652860824714306457022709346080299/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^24 - 701270118683964295635817582867265405803751364772239907607571239958517872163136685189102541083261299211041685499/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^23 + 54749816482192777435346214244551818076937660541259094653137624473451334590153543781570225391829375012240363475/859222513671196334370970512483755296513341509186042636705862086278162702773415597847182039062804938851*y^22 - 4623359673260182628915158544964788398131975511411854732479483223213247511111654582160172784312562680468060487862/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^21 + 3663342764569437529210982553493086623526220673584055908812044871702006214331261032858860122109861896116888470553/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^20 + 3152369820912731219192674453236216563537518796382796781821298775002567973933417110031747483886844017107489896551/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^19 - 15151098028717364461653438981875997009317380252337783688077317404651864890675350705655183204770803221189054290467/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^18 + 3628225620711245993429218759195761671081958534040502710479357263171793153720377376263381161000621923924908694806/6014557595698374340596793587386287075593390564302298456941034603947138919413909184930274273439634571957*y^17 - 23276939448451633777448355302391878017451376919521873237649379735587408807989239122414324042839248433840671283456/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^16 + 5180289435772626198465743855590708434401748449630211414090887426152402625096062251344919527118652913740983291675/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^15 + 18058342555076504975540785714998353628815171538827079163157436728166008749032266531431849506944768842918918928018/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^14 - 31144150882699613741565023905049651180836082436265393674907375997558535908073503410291677282987886939856646485766/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^13 + 28668633216960436435322758936569575294412478238724027307835450282588297843115216304191411581348656170281050934203/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^12 - 17141504581148973777123004896498982964333313473579998275611802620092364156203732278298708046614277786606234448155/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^11 + 915505745582952822642976874710274078376461969766266349218597111016103076974093056249998202855138848167911695760/6014557595698374340596793587386287075593390564302298456941034603947138919413909184930274273439634571957*y^10 - 20575624283736063994530150531622081099663866561236259189932169383629232330010432204869069541229658665802283738/859222513671196334370970512483755296513341509186042636705862086278162702773415597847182039062804938851*y^9 - 325309582779158163193585316202780368560556612305425331513247542641067607451780552114044991015828914502447911842/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^8 + 227476580564899453737269951334277172515699700519230704761352590815847954573487932422671720050502493264242473771/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^7 - 48783326035355107931222880132295070115735844540956497259821270395636551601615553435254480771216604611456864022/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^6 - 54790326192553187922316839245163361365489970216273880711572737259376509516434480236872773353026295926580797/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^5 + 1917597641373569411703792277352410822294387546423331684629952506064641039232506165433735021494637203839066111/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^4 - 254003004640696188356074083488711662510175569275257990632847046802810145765794476419176410405179924996058472/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^3 - 18783437270037465108923282173160843014661648600031903547208614882859696819094098841167755702851629221765510/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y^2 + 3798788211386672136483830086266049857078099525078113497791842131685423269337887576598197197200212782618141/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699*y + 95697606642572095969462344609247936246769865797767515473586541691960276725950804180200239810162258183011/42101903169888620384177555111704009529153733950116089198587242227629972435897364294511919914077442003699

33636284262270269932536429655619341224002257853553276358232580080064283497824188774757012632265668807542092098459590047159905004683213/143644172754464758679837692400935437429992367594950886689216373992458089763541624730436481101731251028972305168434810553905594682596529*y^34 - 470805812544206336207661332210252805149200601536432319338913548584813348601514864051837667213796965022006004604345813689442464621316863/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^33 - 1098492243003561817085419678748220424456915828860743778390198474138648484964928373047014525876898775918101894624931852765955027280589909/20520596107780679811405384628705062489998909656421555241316624856065441394791660675776640157390178718424615024062115793415084954656647*y^32 + 24296232770120696077306183179552228261745658075258600475691582620659192710014149697711424425765391858293804963220699291764510495971596268/102602980538903399057026923143525312449994548282107776206583124280327206973958303378883200786950893592123075120310578967075424773283235*y^31 + 111684977528298114250468585087766320122054599331324195011820211628954341358434639419086561758976184374566125844080402638662046487500157219/55247758751717214876860650923436706703843218305750341034313989997099265293669855665552492731435096549604732757090311751502151800998665*y^30 - 10374083468181909465259383614064049000667768721908334982968623902881802067741522549198895154296057921878900741224890255652072171817030476093/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^29 + 1645577780139381762111295108837083979833093132283645722010186340998031663680098545421443970433059871782581186576199632141000952975981535825/143644172754464758679837692400935437429992367594950886689216373992458089763541624730436481101731251028972305168434810553905594682596529*y^28 + 116162640781024815038563581585560059569337738649291138542986750728637318333694991390450657337898825118844565482378478893273709955324353152831/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^27 - 556604561035719089078773671263146868032711113460372978221162897415900148131370787276234164286938696809420739298822590069846050437828145495576/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^26 + 1241126781296099779422997987687755822492493325785419542310927649434804544070647600458473171181348004562609494140246459942089164383979277796741/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^25 - 833872342732639610532555105823090001894883890767598683781830725915532805945987431649396571120291279153840707856452955372167990783152255875176/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^24 - 3609087404931841367255677863068660472133831820210421357148396839521097193016315379445813009504580712046372184567925527614820402625902753188826/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^23 + 13240683590922055660776506991661441562898880441964898651238696796679477521858173566435448339793304293141834727141072049331307499414525745402872/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^22 - 1707795446081216149013075335729451570864408109011771005981479571396847140773029816575629369184701534362084181136543554902745156027478327197379/55247758751717214876860650923436706703843218305750341034313989997099265293669855665552492731435096549604732757090311751502151800998665*y^21 + 1500811991551567777473279562708816900545903410714945128238391246434927394354893575185170928484369230463907405016730684423098821368065749264728/65292805797483981218108042000425198831814712543159493949643806360208222619791647604743855046241477740441956894743095706320724855725695*y^20 + 3510235986044886960289538111409213475308898390491369899785406438640103715061635668169898130310591733855956143494265344705627236612061230042429/143644172754464758679837692400935437429992367594950886689216373992458089763541624730436481101731251028972305168434810553905594682596529*y^19 - 6844101098364198525311192616524060008492947914142400429858452078982847749818328116477410202019633936812802662944364619702805411147372510053371/65292805797483981218108042000425198831814712543159493949643806360208222619791647604743855046241477740441956894743095706320724855725695*y^18 + 121830567866563659297893009521952943257256826022228957474086979034092174069811014613688641996842143586555851373035551969816453880259936084793686/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^17 - 106434961574392501820253920281783833053588452270279883024889417760047115489570466103973348542466086372759907157451362281002070635385575900943733/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^16 + 107679436518975792901127774020903684504769874191268359776441441725675905189786743866968633206832701528720375449758523399694260059979936703444/5022523522883383170623695538494246063985747118704576457664908181554478663060895969595681157403190595418612068826391977409286527363515*y^15 + 13505924420175173392302326830930315378499535758471469368267041636422209671986806753016762066151841726360308038429556070562494083463147146093814/102602980538903399057026923143525312449994548282107776206583124280327206973958303378883200786950893592123075120310578967075424773283235*y^14 - 150172409085477626021798444073452507163958764488586891487942345910256437770482280636688953358230756105752838462609300661919178753183531731248612/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^13 + 131010831316861017674516846255370317627018072795923363023211008519136421168849841080950135814107437757735408576922503626484472878427383237392857/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^12 - 14609881385274335273699200339556972200181403171935918017582400122922445553239349504596902372310343401930054462605593291250320421654702508043509/143644172754464758679837692400935437429992367594950886689216373992458089763541624730436481101731251028972305168434810553905594682596529*y^11 + 3386051967624017290007585080285082769356902663377528316954566883565004526377008770911344797061094911600006521464007988600861943472673059822389/102602980538903399057026923143525312449994548282107776206583124280327206973958303378883200786950893592123075120310578967075424773283235*y^10 - 43026938629136553611905059845171179689380505949190687173806038182149863013103329290549513850770902097018027423114654105977232409118600693730/20520596107780679811405384628705062489998909656421555241316624856065441394791660675776640157390178718424615024062115793415084954656647*y^9 - 479653177063456782301170747631604443522932454724088912089616087811334992445870951390032169385527968125277267437885169134953170850902532358339/143644172754464758679837692400935437429992367594950886689216373992458089763541624730436481101731251028972305168434810553905594682596529*y^8 + 1063766311660909200074225689748675792293674481591404312313561107437932845648570696747031193658255160101029005154436489912913210716308792243858/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^7 - 19481704405951963170127669209975502202964835483590547539212423313450641460716232636912684550573321491853125294392939683259661597104539869348/102602980538903399057026923143525312449994548282107776206583124280327206973958303378883200786950893592123075120310578967075424773283235*y^6 - 30325703464391440297529769718361149010129935409183111426649877833738033887657997577249561418709717866496857427066574566638194277085082599337/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^5 + 11701674289419884545887030220271452490019978627684314738268592139185677599364531844639849115344480093479764627074362756355279470186562657307/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^4 - 576900887513464483498933541068995987507939058465306077933596830958199070702708688501829785986905129204865232282171822143684411590550432003/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^3 - 241339721749607538046745380859199802620492421628649605337611407564925701280710552030536079792224722043547792699824691965170439505717757728/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y^2 + 17934879566804864403135542854507636905064963843214094731064123515112277186503657041401741542960221029150965716937028413201911914453640822/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645*y + 2833482270193593040581943542341775271177818944827204968642363756432955288671214678810992865821457286072027015687717968702030019914714557/718220863772323793399188462004677187149961837974754433446081869962290448817708123652182405508656255144861525842174052769527973412982645

-1495935561659079770194390695055356880699355971214650015908724291571028618460419071204082126485300877293/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^34 + 4217471314105068264187319279528591651014594837171156942337301115755115214319200877886105748217803924864/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^33 + 341833129138437987523714511966019281088150559231307170894129105259443382627436169203437577834677299030605/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^32 - 1519421900579851987639003974701476037070004084613136325415662059613702021201358361894385337571801887271995/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^31 - 12869826564012262243042117077113872124543166479670412446594219918256865497271490531784774068841272892212568/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^30 + 92474924826324960101053216844941997566652622806005330759761127338838046378404810926066928281188184118074216/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^29 - 75587260210825377425206439475882643875891271264750869801073424626908354232718899542742832691329507642878599/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^28 - 1028167213946075880709981467463965235761800425098046870982159618984447056794630385483954488485157197721441416/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^27 + 4969869624912035732127103273352955137036060797515600280909515163708068324375670134272141674508243900016112732/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^26 - 11181570102666537694947517200154470321509703455326391913786823445987730630404409950285813994693986032772652981/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^25 + 7825290817745507185607578903570762484821769573534510058788806197389151792899532988093478259177601523867061744/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^24 + 31566981085949274304370105198958814621112012496998955179157888620960206390249333951105765479524658656725165693/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^23 - 118241691838392887719650508209389863331580037684642347953126312108122492729490951948201558268400572344912507603/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^22 + 201183409838634212170338004045146123085179341174378643285145772813354016528583816447877257044904763979116138959/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^21 - 14099642999144988935672599717066785482607603677251353685291369371273889662758581485459652980881485291754655427/859222513671196334370970512483755296513341509186042636705862086278162702773415597847182039062804938851*y^20 - 146582613841781253419267443051586057839670598831764162765333515038531645121629230294107808186534200755819198852/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^19 + 60802606821044914005684647477279772626839336410432849007228893849936769151785762603189065986468110224660897760/859222513671196334370970512483755296513341509186042636705862086278162702773415597847182039062804938851*y^18 - 1104283172354897373022708462904915553828166100236276859440084002212879522724329005523332883478995081613188249591/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^17 + 992669126475555471722465817340026251499768961830886418667198575866238760990420244693796862572802851332230762445/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^16 - 17435924388082935553659027606769248944556893625369455077716654579974263467486336469572058151289875291483014760/859222513671196334370970512483755296513341509186042636705862086278162702773415597847182039062804938851*y^15 - 810541394895335481027574996741183717463199042115382495304454532167071360695343960452961510098544767320345357476/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^14 + 1353599416352700148083455693967641041725659296327375224950841258740933832117150787367363018144843647954409363456/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^13 - 1222939449238790913353279715654241326203721733151097825367564417470542827709687928184561874565537068888957579810/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^12 + 716003871579814155902451572319755674300002179524938545418714839886015801249969827091526435670243151291106889447/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^11 - 258578790513617314314047170141662773053167585727382682509063836432219606677527768518275381911786700914731914100/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^10 + 35799490936254784128728986238093345774005057170791908813212898200629453766731717577308573395061477119409464677/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^9 + 15428293418834152753122397272741767661203391167530897346738011015230634069097183984996899264046375726810288077/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^8 - 9443096569819664770310186484067331144110198894547116142816090104470978248761255470650062687797703009164597550/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^7 + 1828013206030179126617151460041951308688378166144787023194443273756696693893823475422511932222764797445488599/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^6 + 56857013236553132210651254299526887981217406244502078772952355433530398203420389429163146604734198661053359/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^5 - 80226521309295339600948531081689083055875030902633368694395751961334024367635772643290584126129487994117910/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^4 + 8483262873436181788436504532386105071405867000251702204825655708927818778855244727113784721892431100748660/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^3 + 1022294492946605534751487909426243997385424715422119371598493519832144157248461274928500558251370510199382/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y^2 - 120271166495158094820517407081357878731845502180846603252028686356504946749762235226641596891880658171525/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361*y - 10070684469974380549640586793865370949771158755652847161857694189970796845636296940316782654348959400184/9451447650383159678080675637321308261646756601046469003764482949059789730507571576319002429690854327361


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

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

# nu Gluing Vector
{5, 4, 1, 1, 0, 1, 6, 6}

# f Combinatorial flattening
{2, 0, 15, 0, 35, 15, -14, -10}

# f' Combinatorial flattening
{-17, 36, 0, 0, 0, 0, 0, 6}

# 1 Loop Invariant
-588701946134183090288929722558214960284677704129662110778397823562811520685374770635214719594177150279960963637726939372026608123519237444893274075146/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^34 + 445798637048219029503120231141990776520348557735955055603582341157277158313399883429105448165130261294468034383084752106999400527435012320191718402545/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^33 + 38515029886821696492107033551114280552904184843873054449052805586582773606976900648170222581050203466812059179065223395709369266693812889623338058663313/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^32 - 82174626513809680093233361770049959361907717389254923093988874353649349202426350445073218103670317723793344507735256862795994017630220202019919372611240/20418369172425565908895783924039093264042948327307660633521638678778261614470179906428624990864168872753985572526488726229904681201617368355601273523*y^31 - 10331067290256585688303997968525317352410323389147276669524163170683832231519157707002119526289231034938214758263116090820334280449426927310388790375359485/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^30 + 71071450085291853713503906187707652791443349215842659687154020354441107936911219261453135175025792670675135572495855042307165921808093920218322464281184461/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^29 - 47210671649888744410277905291647148862057249802214305329974778795791553815728976858634766947589794909112080097782158684696974244814134567796206225753874957/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^28 - 58512819430960349447444623218567833861417742388115730166756745784178218169200440859382682921310426812385496578337912502211704600258469510424536003727443331/20418369172425565908895783924039093264042948327307660633521638678778261614470179906428624990864168872753985572526488726229904681201617368355601273523*y^27 + 1887373202745949546952393599060425531467497664218425842180468612504481269059868262653226555875087955640659659045023415028926506647596950135445345673126977955/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^26 - 1162976811371065607682391794154716869737227496271974815073287008295074683053733450067784165797706957733562427479517805124401400916157294026953667374316027133/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^25 + 4678981129746976929607770740962988880824300553381300448168042302189943615693025349380797221619732401099576280636024455364746989495410257761537205761175727385/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^24 + 25866406131852796523887463673245478725901530884313868429140642271538031020044385073064309883209192639452545151443291247536677284925997720326077420837605752473/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^23 - 44419930783939871047511839147675791780259672677763533792434142961938797554694313487732257781281221813342422549999680075770301722047187768279502845677374920575/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^22 + 20376831478661372918671348636326803640749804150414758453608770735611835056304384861597074073248599862931608922549690301903663480600044582152622956026141065557/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^21 - 95487321736612287060800076751339765918540644120666641105224271877347809521706146093058020304918020964666535195322653130075776322614008767501007899514859127211/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^20 - 19368635328731171856880518225916765403508509444065402118238645594741329137952589009000510345089559998694029245149235137610582746347832673648230863603824544031/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^19 + 253190219727004951563980357963739438465893911905293236968902836078408476036095855969245437978383298982145866774365641100147393704419569140550854307370405215316/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^18 - 780019687873903038690130236714801788892981844222061663825840545548745842094303272447575588511238795282471065913487576864356146034279207713801278557411891745309/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^17 + 317666219782613963114247058340027574134788173929346587561750677553455385626351903561405383426643933058057848721454384003779597652988531837053460471379064121065/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^16 - 21292768457870794775854673973056927241719333219950246487332887545618612948557581474777295054716637762293748902541829116318905492856532567606168643663419114965/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^15 - 330140424514190824423390921586284540137253138136808619526611604967611104810133780004720267345629261906623205374899622670174859069180709883965604947953456708913/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^14 + 136466878072586164744726045234055258851808944593779455347299186250860085996489591737199601206827177671173637036157938516380005461488976716703973602040054515981/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^13 - 782756309862219326596262155162870870563956410121992999789405327331365124812329453142221893387731545696143802525142208989896793611997993147131753536436000708203/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^12 + 28843876353835255838150803676640630570879063764844424763901420274809823648012113564650058689255908970015337033933798470679668637465512541143271780125596638489/20418369172425565908895783924039093264042948327307660633521638678778261614470179906428624990864168872753985572526488726229904681201617368355601273523*y^11 - 471853680005609146900560062083697842740167582797492499213096349712372565253297795708679217677876087445354640192939779534500691967281195258008334654579666607/1201080539554445053464457877884652544943702842782803566677743451692838918498245876848742646521421698397293268972146395660582628305977492256211839619*y^10 - 208700484212870714824398412888129123128352582666289046233287791657860646805180691127589764965729958881169465989658730049324746879665263614834120841381770865/20418369172425565908895783924039093264042948327307660633521638678778261614470179906428624990864168872753985572526488726229904681201617368355601273523*y^9 + 7566314848165672652895160386381691951339376937601856489871242180293997385336406862627906071594938553777441703640766130629298390046175808795137751359895050005/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^8 - 4813564473153127713020789796419959840128518629658441918981594469998623746683735636700914237863022724203473809402822950049238059139073186673851297273726541555/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^7 + 66714697354732750806336720957877800394792494858877091554933025372963362657579287184341878706949686534352118182492304676430066628380719828586773747501747354/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^6 + 243954281684397111987224044987168391460603032065872937450014328866150700754056514527402420253870269530316795919764080872469518276480680912981331466323132511/285857168413957922724540974936547305696601276582307248869302941502895662602582518690000749872098364218555798015370842167218665536822643156978417829322*y^5 - 5125986357886359876346658463733323662146674825508081312699406520631665136805443206659984924585964563434655125032313904736473524939982443337472519156960567/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046*y^4 - 3469903365940598912435607751072698950714725413717983790841307841046240707456638296434313841985875770092826586432713758658576137999448026992864305562775996/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^3 + 859543682700737267981208001485297774909190989418452639131102120609648749633448991594654205747246349441195868210924570110708615372765177884025700242330932/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y^2 + 83388394878084831258354492972792785262162467444250117635269460228027868074624446093010648687608326849549116101346049070299769233275706806524267831778127/142928584206978961362270487468273652848300638291153624434651470751447831301291259345000374936049182109277899007685421083609332768411321578489208914661*y - 3705535032784554495718075614693702328316665919080789477873020776359572294758780866451263339808125959217018644099334783466107305933434347011757475858721/40836738344851131817791567848078186528085896654615321267043277357556523228940359812857249981728337745507971145052977452459809362403234736711202547046

# 2 Loop Invariant
134046790007130473951765819641273869415023648327879195400180374603852432414757391127886971990914294544199986530124159703710723861189545250178055459358894926750558560111810525166146552372117986803017972740304227164285221031787255027826008469444345780028569779611833201633222119535941617/1855628570380806259304855595422098886491509290098229088359389048756132159890693551084314298654948825836312875588812172795461631485029304231071158051829448843781367282666074142802141235467832735108777242555016958956376091041249303905721376866050092856671842072385581844010976314520559944*y^34 - 2848456111529458731716107676707043636886101868005736644002807278143223484616744163934024460703099676874300590048660038329347358327318442272466123576171553487545709672346072783270584594839107894205977139176943384023164252652379230273887936723329766554099544078962988190349451944232911823/13917214277856046944786416965665741648686319675736718162695417865670991199180201633132357239912116193772346566916091295965962236137719781733033685388720866328360254619995556071016059266008745513315829319162627192172820682809369779292910326495375696425038815542891863830082322358904199580*y^33 - 26250643508490188641519711436421311185163916589303200411365749534618762962617211307838014467768600756043789673567024678352791636358378602943526134769537539526344256385169067613853210079799394845902570956385884533682750006764077479890536490249495834073585248219738518181029858292275563527/1590538774612119650832733367504656188421293677227053504308047756076684708477737329500840827418527565002553893361839005253252826987167975055203849758710956151812600527999492122401835344686713772950380493618585964819750935178213689062046894456614365305718721776330498723437979698160479952*y^32 + 83621292489863066799834442540315656031813263272988237586249377403631498836563132492703861488805244364643288399808212132049369514325679090929757957349100900627101208735790045246298246366807178793774446155618222611691493794085402985977275415672269871505291902964344454282987099472550797841/1136099124722942607737666691074754420300924055162181074505748397197631934626955235357743448156091117858967066687027860895180590705119982182288464113364968679866143234285351516001310960490509837821700352584704260585536382270152635044319210326153118075513372697378927659598556927257485680*y^31 + 2657053329805410239485939248353002988954321495276842204459757093702928705678824265985388600205373044856827395488693745330718833042699804595629564973682292506145498855703838309111113494265943964926274346593043475079791830471963053708699170756112922650783423823414054604560694748372093292941/4282219777801860598395820604820228199595790669457451742367820881744920368978523579425340689203728059622260482128028091066449918811606086687087287811914112716418539883075555714158787466464229388712562867434654520668560210095190701320895485075500214284627327859351342716948406879662830640*y^30 - 15567986547770339007842643314470173773530139541227074376126379576130389801019877559139200908055109043547316957421169010193692736316931696285445826300095737238866556887206395632533559921967992613908191746823367527846099960463677064175897913826739471222581546014672219064174305929237444812277/3479303569464011736196604241416435412171579918934179540673854466417747799795050408283089309978029048443086641729022823991490559034429945433258421347180216582090063654998889017754014816502186378328957329790656798043205170702342444823227581623843924106259703885722965957520580589726049895*y^29 + 13773754389718299168386946862548195785223777447143664876978570396166945092558207999194862598823534775392246288101030962740101871073651923676597909521905263940815443061997633721590588054499892248897109670436374349825732312502715063889590687202489834012139803965014959419083935401335031915863/3711257140761612518609711190844197772983018580196458176718778097512264319781387102168628597309897651672625751177624345590923262970058608462142316103658897687562734565332148285604282470935665470217554485110033917912752182082498607811442753732100185713343684144771163688021952629041119888*y^28 + 2761689320790624042826331906290068271805648218470694870741214498680063834551894723834321178428386479847284152398597215222078739489294521805963434079968636373350489140358993509167779925428669753394751360893345089049320420484687477648831376753548527124206907128576715659335112124040013332802339/55668857111424187779145667862662966594745278702946872650781671462683964796720806532529428959648464775089386267664365183863848944550879126932134741554883465313441018479982224284064237064034982053263317276650508768691282731237479117171641305981502785700155262171567455320329289435616798320*y^27 - 13399537168386390447202225370667014171945279299458198359649466142839479902200497383121216677551637352151985653553871947173230218567452919423790111845183697405756524020490015884837195951009583133930110474184267458610015403526757742868756904194279117247379680671080753796285101331173951975051919/55668857111424187779145667862662966594745278702946872650781671462683964796720806532529428959648464775089386267664365183863848944550879126932134741554883465313441018479982224284064237064034982053263317276650508768691282731237479117171641305981502785700155262171567455320329289435616798320*y^26 + 10079834624119452178493219823984437452677194888476993872242008008624539044910182899078655149265583796077100890765163948479277920993860071180533526782192739691062718825376638547688933138565792966044630246122732172514793483276838264755531791982631058477189357271956089417856812542404962923024433/18556285703808062593048555954220988864915092900982290883593890487561321598906935510843142986549488258363128755888121727954616314850293042310711580518294488437813672826660741428021412354678327351087772425550169589563760910412493039057213768660500928566718420723855818440109763145205599440*y^25 - 21424200150845536409925548232358729388609160388004110137674246636015067327466803794014554306912009470764533496363582131213173452635890656933602983875301092699412550040817358695651953728730575039951371902650740687166161926342923197998284254592482284208858044330127580961697747959661402786730149/55668857111424187779145667862662966594745278702946872650781671462683964796720806532529428959648464775089386267664365183863848944550879126932134741554883465313441018479982224284064237064034982053263317276650508768691282731237479117171641305981502785700155262171567455320329289435616798320*y^24 - 84642732529609142131243858041241349696719833967964358582192235203997669217125438558380284652148253845209715358579348842564553139370968105951457859558055609348240184676317293113844265436994703057449645188821880227690625696135677494611597467283513225843244654835673432694116578722654639926966279/55668857111424187779145667862662966594745278702946872650781671462683964796720806532529428959648464775089386267664365183863848944550879126932134741554883465313441018479982224284064237064034982053263317276650508768691282731237479117171641305981502785700155262171567455320329289435616798320*y^23 + 22793849055751583901546957174762497638633519564355155564818591208274516175898513744255191300263744396505806152607502525825832455273199147549919626581040675062040937629796263271648038504094714132464816659908727017801889359647977846942507024474062519563247796138470480663524190841883008966648197/3976346936530299127081833418761640471053234193067633760770119390191711771194343323752102068546318912506384733404597513133132067467919937638009624396777390379531501319998730306004588361716784432375951234046464912049377337945534222655117236141535913264296804440826246808594949245401199880*y^22 - 13976429768800916833955100325498785991973345851526434429973584812592704749274753225332200324685287955523471973694864058511078113582449497832883135319343967632891396517569868529370102521509991777770795333171649663951016678489445637816587129730996237976738655130479575703626510799668995251109377/1427406592600620199465273534940076066531930223152483914122606960581640122992841193141780229734576019874086827376009363688816639603868695562362429270638037572139513294358518571386262488821409796237520955811551506889520070031730233773631828358500071428209109286450447572316135626554276880*y^21 + 105922966153559112831444778449899378332772169447378237714502892251097271808493513846214514306520449463557152320894553042106246376470137356786997293778196362814080425821268576296227172315023799142027693449857270418287517788579274564768203380047390703127803717127210707671119229607012658972125983/13917214277856046944786416965665741648686319675736718162695417865670991199180201633132357239912116193772346566916091295965962236137719781733033685388720866328360254619995556071016059266008745513315829319162627192172820682809369779292910326495375696425038815542891863830082322358904199580*y^20 + 25976461061430562766875722284252583958909272265462186018732422443869801112108872289547771439041143410911824582650697051122071042918861123559722664411502632784094403682706878954745000276951266113913740846282966881944855178994689058371223369574513733209234685981060686626771317148614302225755889/3711257140761612518609711190844197772983018580196458176718778097512264319781387102168628597309897651672625751177624345590923262970058608462142316103658897687562734565332148285604282470935665470217554485110033917912752182082498607811442753732100185713343684144771163688021952629041119888*y^19 - 150387293169461382354707176135204845800618412233251237049054749374498195698556685821936499318905891454591393852350278874647318296353312021072691843654101234795526660321362862518775132767345797872234410509246382470415725579885386174250745539174835323060119541068616865715476367725389625926406757/4639071425952015648262138988555247216228773225245572720898472621890330399726733877710785746637372064590782188972030431988654078712573260577677895129573622109453418206665185357005353088669581837771943106387542397390940227603123259764303442165125232141679605180963954610027440786301399860*y^18 + 26721390753336588805079299469007006954766153927024555808398027288138721783055113798644493053482561384667326456514480238174519846977249510688127564332840215115749594204659831158526471634035412267891436128675312913617905486217809657831355975028901119837116401294114973908676310950424279535494627/497043367066287390885229177345205058881654274133454220096264923773963971399292915469012758568289864063298091675574689141641508433489992204751203049597173797441437664999841288250573545214598054046993904255808114006172167243191777831889654517691989158037100555103280851074368655675149985*y^17 - 676345151817809792012022587338794145183551217527016885488345783905056236918928144389674015782420275321206040968087002900439482983577322127012710639682360284848145128666081623096620750937412925700059143636322317263015211173809836020257763215401446163145675103691012457283250992629358067907913443/13917214277856046944786416965665741648686319675736718162695417865670991199180201633132357239912116193772346566916091295965962236137719781733033685388720866328360254619995556071016059266008745513315829319162627192172820682809369779292910326495375696425038815542891863830082322358904199580*y^16 + 20963313037055345770482289678747841794251776218416959287197662278332176346910440038485181583074467881899802160934470621256865831530965985319974762345586949690416746449051797727352593426296514968944005054794486638019842187650435509111363665469248742005003477491377008209190027181050461817216793/2141109888900930299197910302410114099797895334728725871183910440872460184489261789712670344601864029811130241064014045533224959405803043343543643905957056358209269941537777857079393733232114694356281433717327260334280105047595350660447742537750107142313663929675671358474203439831415320*y^15 + 1089434412379697234204253466671729045819170146192559026741711138018691285709504719893171687415463977794174688251519576848516644370579174706042473602562055357336798958889960092522053224279654959719392871780004858501672394428726132951682093881259791980410440995587954692852793745347695760778366921/27834428555712093889572833931331483297372639351473436325390835731341982398360403266264714479824232387544693133832182591931924472275439563466067370777441732656720509239991112142032118532017491026631658638325254384345641365618739558585820652990751392850077631085783727660164644717808399160*y^14 - 458814822686352975637647740625165928402119725441190174338194388595193282706493441398460089765860379866856965705718981382489535614198493476846701534451120372890932816070310767674365080228811949700942541434013171640874119149300360849211896761362665909146769869979702497113944189860526416004073931/6958607138928023472393208482832870824343159837868359081347708932835495599590100816566178619956058096886173283458045647982981118068859890866516842694360433164180127309997778035508029633004372756657914659581313596086410341404684889646455163247687848212519407771445931915041161179452099790*y^13 + 833068343079299095726761963727221293043613689036089333880461443773681974198756447848817742033003387706716510709542968600104840088546977674886998362975575732288248473240665233085143657402138616829799567584982784944546200210366123853898699835016182916196063299513283266544304280671113153028160187/13917214277856046944786416965665741648686319675736718162695417865670991199180201633132357239912116193772346566916091295965962236137719781733033685388720866328360254619995556071016059266008745513315829319162627192172820682809369779292910326495375696425038815542891863830082322358904199580*y^12 - 392173737014966037223456983203101502266639296059041761034378032549338987433865938352663661469012807668870179753952634431223399233356307919406284533272463785235929024237643187380118425288968581943768788153592192050598496005961609704598169881227304559185432154548433407849037124922076068061535393/11133771422284837555829133572532593318949055740589374530156334292536792959344161306505885791929692955017877253532873036772769788910175825386426948310976693062688203695996444856812847412806996410652663455330101753738256546247495823434328261196300557140031052434313491064065857887123359664*y^11 + 249830435889495117339156975145071554337038906804204494511821657353665830039276428333888242035293303223961982150220487944916454007943530780961911668737334154183099118561795030039914798609649576579091738954953837944502443432233064640896057786596917271044374521683684042768231452660675538241487/19491896747697544740597222640988433681633500946409969415539800932312312603893839822314225826207445649541101634336262319280059154254509498225537374494006815585938731960778089735316609616258747217529172715914043686516555578164383444387829588929097614040670610004050229453896810026476470*y^10 - 51738335452005907153027366671405552201012759106224210303686342395432241593822055670040331143523622701012614076067537563569499548667849576691157483943401289608008081655677894623465279113790887557028549369928408943816349424260966379447599075643268088239035852207075643838074744362004177918455/28402478118073565193441667276868860507523101379054526862643709929940798365673880883943586203902277946474176667175696522379514767627999554557211602834124216996653580857133787900032774012262745945542508814617606514638409556753815876107980258153827951887834317434473191489963923181437142*y^9 - 4140743182987932492690169388410722296724327290792301938249563627303546361465235490367310599611584196235049373588738476487746848390029080535965246457063133998796000131247639562718651291927690820997730616414134562548344529903202903322766330331073794954569731673468863569732322926168760398470109/5566885711142418777914566786266296659474527870294687265078167146268396479672080653252942895964846477508938626766436518386384894455087912693213474155488346531344101847998222428406423706403498205326331727665050876869128273123747911717164130598150278570015526217156745532032928943561679832*y^8 + 8636179158574548451973197830730308828798162655616573819097240014037442498503692177556856738834267406106983068476110763105565751506020401898138015166759939252025616706171271330750008591575078770397573436444436577027782706609460202844178782794489605519878201576880183827120935771698935060777579/18556285703808062593048555954220988864915092900982290883593890487561321598906935510843142986549488258363128755888121727954616314850293042310711580518294488437813672826660741428021412354678327351087772425550169589563760910412493039057213768660500928566718420723855818440109763145205599440*y^7 - 1268817288178333527716668851365643836565586035908987164258652930235385264971386722046245332241209359470762920003129510727356559696991051792638447543620983563212920360074227507338140171496328860512221250985325905359326632039325913037424700171513317847837548168056168408452202976476898439342781/13917214277856046944786416965665741648686319675736718162695417865670991199180201633132357239912116193772346566916091295965962236137719781733033685388720866328360254619995556071016059266008745513315829319162627192172820682809369779292910326495375696425038815542891863830082322358904199580*y^6 - 48469905743774486597927402613259775528416765265365803828061644486604923348907081426889947578064919056197154234038528002513157488866436369035612550016921899051278290572145494733653244813202786378262829477942783645031602605825026910885614707006011166886985886596766113357457379072893888489391/18556285703808062593048555954220988864915092900982290883593890487561321598906935510843142986549488258363128755888121727954616314850293042310711580518294488437813672826660741428021412354678327351087772425550169589563760910412493039057213768660500928566718420723855818440109763145205599440*y^5 + 73121634082304749121739789678931267316573415472753661431981255403716673718693815674537490869628412807115601499963706720078817917359372138427180915434519677151167434299785191623971678414123439945836236629146945215168763197130116628718056871182508713984109134887468226958484292839721970722351/18556285703808062593048555954220988864915092900982290883593890487561321598906935510843142986549488258363128755888121727954616314850293042310711580518294488437813672826660741428021412354678327351087772425550169589563760910412493039057213768660500928566718420723855818440109763145205599440*y^4 - 22639948566021500832242581125357545967682859695164817754205503789208714728679790641663404324069365280679557735603992977735206657876588076736539076089124781137867557981417947944218611094085122025282808397112133172662290463359234676218718811997171466943786784639035063897799186068593854682947/55668857111424187779145667862662966594745278702946872650781671462683964796720806532529428959648464775089386267664365183863848944550879126932134741554883465313441018479982224284064237064034982053263317276650508768691282731237479117171641305981502785700155262171567455320329289435616798320*y^3 - 1490212982232273331789229252435602897357211727499751323771646969619716053464556709792845575588157880906105112028740205486101759460317689763655691978726238437755518877283282480223128479665120474502088803637454752321191957213137020289695563802629034260275291049804393959377941285672414569151/27834428555712093889572833931331483297372639351473436325390835731341982398360403266264714479824232387544693133832182591931924472275439563466067370777441732656720509239991112142032118532017491026631658638325254384345641365618739558585820652990751392850077631085783727660164644717808399160*y^2 + 158412909084229072110157777738222103730467187366662544456094866466537216104755025484661774332201414402767099453818437972276947809619569350771492986160099128401348563626765717209949181523190353196812233120878226489682166295456059019965896697708554665155014780853672612069713119642296502799/27834428555712093889572833931331483297372639351473436325390835731341982398360403266264714479824232387544693133832182591931924472275439563466067370777441732656720509239991112142032118532017491026631658638325254384345641365618739558585820652990751392850077631085783727660164644717808399160*y + 68156540289513805092862530243591999163556611196195015692522107900517930501959932042337230610802954263069007888990586001135430039874635914907432295688437007467205616066357590736213583969631619518831845239153024185944038413540007765782817609056552559431450240418909967908845292669732462951/6958607138928023472393208482832870824343159837868359081347708932835495599590100816566178619956058096886173283458045647982981118068859890866516842694360433164180127309997778035508029633004372756657914659581313596086410341404684889646455163247687848212519407771445931915041161179452099790

# 3 Loop Invariant
8070463113504781146741060040187449728718689157265401231922221283248738921310632731842695214522638577883619874164706918134939688044494555746860569824870878857910139519740872177456629534973908212321969041308941567911169703622063335279166763571933287872853253131602494453735253479172167721061699213573021956421954859058743293252713792648287313294686662993/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^34 - 4653049422092673104054854797540920106135869334341058386764843510484045456323492031165924563104822267592343102994493474773960514053774053219292423880909703175157393887836526941977967026472793145099880631329869826592073369592133400132838118843085414128096034718785568091574704721162272027925873482556303173104943610556609084919758333848687798584849107135/165863317367677385647267684164778384576576516136882204962340770886057182763395629163666863448633376324388322369603841675738670021125454750427298993627049912992133426479135332253380173330800797644602728558414506963272773688539052173536907345062305004585493535900486875186549702965197661991675093789324278797857798537641367842183293661931823626503395299648*y^33 - 37606375583218642024650199984413894566499698847502870096106093468247076230572931970411336374053366271740443363299177866158587846886964637034889091806149707883079170567598447235939952061462579909384601454210549211137987446105720447148595719496891145180521513389427949173547074739071474739889973362203084286888307064216930149428857407402587043918497960699/16924828302824223025231396343344733120058828177232878057381711314903794159530166241190496270268711869835543098939167517932517349094434158206867244247658154386952390457054625740140834013347020167816604954940255812578854458014188997299684422965541326998519748561274170937403030914816087958334193243808599877332428422208302841039111598156308533316672989760*y^32 + 296935284566362423494301393256796453441130901875118716088673409503223553112102588536461113478710316579419829330299830585163955229062102566756179316731775549686303370233421485136494081145871304075123299560036165054324363582466203712326262723720556166363776724801933178501869991817438909139211636531003177456711578479111622826617692571279150516364265044811/29618449529942390294154943600853282960102949310157536600417994801081639779177790922083368472970245772212200423143543156381905360915259776862017677433401770177166683299845595045246459523357285293679058671145447672012995301524830745274447740189697322247409559982229799140455304100928153927084838176665049785331749738864529971818445296773539933304177732080*y^31 + 5300744151579473521895428058796131586953201462425051137729863506310983177665375838468881647958613083010610900853022214117186532416681638120655410879688731669283898690110559611859299012469103788836609032843340429136626299886451559694129340313122869514220404059653513725897483138505555262554784669589834178193912447606803501289246872496000011363856087725631/63793583602952840633564493909530147914067890821877771139361834956175839524382934293718024403320529355533970142155323721437950008125174904010499612933480735766205164030436666251300066665692614478693357137851733447412605264822712374437272055793194232532882129192494951994826808832768331535259651457432414922252999437554372246993574485358393702501305884480*y^30 - 100657865101139474365286876662197607780107912232448630259319605897834400826338717769496985626542271830113971398840827770789667677431325163517776694448271149508119349414127377840026830978549068150143511086035721107620475224312155427283311711335740900841528284927297522556105032678558180747330483111243239631884386067178695917792645032362129557841375202409243/165863317367677385647267684164778384576576516136882204962340770886057182763395629163666863448633376324388322369603841675738670021125454750427298993627049912992133426479135332253380173330800797644602728558414506963272773688539052173536907345062305004585493535900486875186549702965197661991675093789324278797857798537641367842183293661931823626503395299648*y^29 + 439498888365167254020747358635756633315240147626025772669672609059194959386581482740729046648614061011772987889800899892971425082207458988333902665545740298599876520616819220375733172163995802523634698804584176521698280241192254543200107905360796325631490029756676180840827304407594908983745050633430107624040142067671204300120253811237089329004749301026269/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^28 + 1380077748635221176110857536355779913462600597274190405991011597313097278388645655621138228680363877493773026635144357227134236788727252869242390548330808079340867956190786188061683611046945510679861742302237604453464033224349436534170680219563394054255936726450105845964052203943599220196263370659620447947981016791743103096448229333512716544165605298502289/207329146709596732059084605205972980720720645171102756202925963607571478454244536454583579310791720405485402962004802094673337526406818438034123742033812391240166783098919165316725216663500997055753410698018133704090967110673815216921134181327881255731866919875608593983187128706497077489593867236655348497322248172051709802729117077414779533129244124560*y^27 - 13581098086870149152912535001842894217610966045906895078639735945830271228569777478179853043584625606903612662888123565480437418155766121662971102609094422319641057937034180030720088420308500377042061008147101119197999442695884356248236687467525242340426002752553890779082278637420377856234317561884255080988381902963635676935098639474285691260400135775930653/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^26 + 7753675255491069818832930929448773299934459891946865498071167515185312457960696241974766528205145735699306761336778984336892411326962818710360208276191711343899679912180700893527906091284163880043041290393928600383975922585629496880942056464980863734082660022932268221083068379878669420304339999252470764070914978067263765276092906482022436898466081990229767/103664573354798366029542302602986490360360322585551378101462981803785739227122268227291789655395860202742701481002401047336668763203409219017061871016906195620083391549459582658362608331750498527876705349009066852045483555336907608460567090663940627865933459937804296991593564353248538744796933618327674248661124086025854901364558538707389766564622062280*y^25 - 46089285175914714348001956150148696723596048324624479818397373681451685849718175860444225370078118461990216602944938518697390877128240827487768820834223567472893587900482918225064558777191053578846145670453025617183920723994317742982975263821370100718695356481408379979148878717331544882664028524186746004068320408403097962079339901103580516998474711698663239/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^24 - 167473982057878052954969311585687802729932920747515580257922589655413847002707080031103400097741273074501390050077221438132772049936430141599057607424095985903565605227695515200127032538581387693535047031750503194396705991101569007735501299025436184456322814243157951989430385288378932983349984222607562750718644279277305500991383823313270337138949497020330087/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^23 + 23159451525164058451631165202443473244401688215677316885715364496853224767170556750900753244042409991373082242839373225362886989238743207570712227126827600128524248119728260861528661567778912254706824650982787193972479126589089655344039867312194716336731152497747446143056742470977590389290236104901865661926604761648837203584803307172842334133544141729151869/29618449529942390294154943600853282960102949310157536600417994801081639779177790922083368472970245772212200423143543156381905360915259776862017677433401770177166683299845595045246459523357285293679058671145447672012995301524830745274447740189697322247409559982229799140455304100928153927084838176665049785331749738864529971818445296773539933304177732080*y^22 - 43302112694840224177883376920803192879632236989798940867072324324122469637580778473827483276333139829045910351520621065144082807259243091248499576372406483845843094709094494687984896995796676147051320560952563318438135021437624907176366650354577087708323358925531336547621282413171814432235990402666164920987201685024058046502773734067798628128155952100622613/31896791801476420316782246954765073957033945410938885569680917478087919762191467146859012201660264677766985071077661860718975004062587452005249806466740367883102582015218333125650033332846307239346678568925866723706302632411356187218636027896597116266441064596247475997413404416384165767629825728716207461126499718777186123496787242679196851250652942240*y^21 + 181355476600207308224306109967776983708736686602136827014107423085877408250006821215481470802974522280348678986407290335654346603948326365945520230215574476433242274863606360148941483340320649544607063999121509071893519805520668187523538641477182312865065224402244631495420562169883103748606008163895969153554623906951330825807735922468291697816188134435438619/165863317367677385647267684164778384576576516136882204962340770886057182763395629163666863448633376324388322369603841675738670021125454750427298993627049912992133426479135332253380173330800797644602728558414506963272773688539052173536907345062305004585493535900486875186549702965197661991675093789324278797857798537641367842183293661931823626503395299648*y^20 + 367225694566457353207611095924455559514126076258818315594946019908282688330444398624926103434918148166035273412781746332605323089552190434233048497855443875543263856961144034267452600878605629726871845713454188166335315614019295883260074371849424319278408356546938214044174080914087946942796289340465802302011791392884488087913395285509945960153184454884591213/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^19 - 1826895321858579568107713036190037326399869963570539772491884538323248242450052720147587796969351498569155710502083415095727679400545962496047036894934311609288943987282180743346404593114217667857317507700578132427887763645154278202357887645575058540889720957726076979464369322333385416392338656102833836371062907955245696928928565580032982447412978960566790363/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^18 + 13803842721322157743459317649247592036853520019561641987989826125924306924821441934315654882982523167506931042785377204436092476443164998298288654572230524579246283471263365922196580889500304544077976065728247374882959459590881417763687772234984671907819146766643076618837040688183373225637076551996403725109483513790930192119225222867628442825259549123212866/1851153095621399393384683975053330185006434331884846037526124675067602486198611932630210529560640360763262526446471447273869085057203736053876104839587610636072917706240349690327903720209830330854941166946590479500812206345301921579652983761856082640463097498889362446278456506308009620442802386041565611583234358679033123238652831048346245831511108255*y^17 - 2869704342356732938629945523622345613939619554526808911564804309807383104354516667814067930979895675991642439540514758470575428037006804639906645729692953668120831908898152719005640518602920781261293675548057008849962637939491313636206158386474794175067194985120199844930129370921649871948815417857932077983836393517568930839767802594134867261298888239756455041/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^16 + 53573781597019634960411655837132783401409361745160836008805326854331977564924744712406032608057754474167085395440052518274001662464750985775067898073144161393757741823587338230068158170620499581476477348524355157019843804633926058518216665826633906005185509886936537065574548302545584799378037053331863697140196451530019533895775519056237343278492356772747527/31896791801476420316782246954765073957033945410938885569680917478087919762191467146859012201660264677766985071077661860718975004062587452005249806466740367883102582015218333125650033332846307239346678568925866723706302632411356187218636027896597116266441064596247475997413404416384165767629825728716207461126499718777186123496787242679196851250652942240*y^15 + 535074578442556912670041967470310679243881580794576201939487394759147981271324643685690053293907964139830000169339911116561662272118313134816770104594937000470930904751457440361422671353590613751343557310791556640013201668390117480685801743019596225142587302350278862056563121696125795162848960083530844962561358566448992283619956184543904677119928287123968839/103664573354798366029542302602986490360360322585551378101462981803785739227122268227291789655395860202742701481002401047336668763203409219017061871016906195620083391549459582658362608331750498527876705349009066852045483555336907608460567090663940627865933459937804296991593564353248538744796933618327674248661124086025854901364558538707389766564622062280*y^14 - 7559221533118428410248681396642662785363267324156371174903377938326519892146488280332011040080108413864788699893291433550489600890596979039997996907686716036196334251011837916679963465315595160975805009954162896535489133523729871240342089990691714812469462178594406295001582966541036893293636389415447506924295084865940527148943153212364350681824599410880598987/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^13 + 176522203696918605112827742608998463464888957056147287112413344135773719276168812586313967435030652572837537324796756916257158589002657914215709222200177176365253014711078379580388632534305681030108810030587873020140330346064068831936158771818757950011852100103472647873011685998336624937416738437462032270506490364236432535377846845875748617087443368452142409/20732914670959673205908460520597298072072064517110275620292596360757147845424453645458357931079172040548540296200480209467333752640681843803412374203381239124016678309891916531672521666350099705575341069801813370409096711067381521692113418132788125573186691987560859398318712870649707748959386723665534849732224817205170980272911707741477953312924412456*y^12 - 4304128073455340531621213239880247624232499702345701531445000002226448255122281420220654765545700809867101487984971332990743964986516889909577458378432314761724326435160751558789952118520613241847210635216619101946509900833532720736289302224165967308350816715105422804151186241079208009193707372506796214430757198874807622968013269320123696994098786246889983093/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^11 + 2811921958181494279428484523403202941556605043477752153157687640331938305912530722472169228522187735676988952490403298289482067854261599489138013566727947710186061582747151835571814639027412527258645965746092558578878890397970727762335341562823635090693340323470974169358940157527418548399862437237986456637062262899322525346539491657341215877584716668575407/1393809389644347778548467934157801551063668202830942898843199755345018342549543102215687928139776271633515314030284383829736722866600460087624361290983612714219608625875086825658656918746225190290779231583315184565317425954109682130562246597162226929289861646222578783080249604749560184803992384784237636956788223005389645732632719848166585096667187392*y^10 - 1263101681193105386371470429381693724120680505730404403023267612340598643369343163210642627936815487236957398010697875730084835787784281122042505559008936971098162526118929545070415309060363367700600237063907673977127781543681161751644820137244801661990051793302157804845503989151706455710346972010485654710982026240621036270376596698539555528637078199993847/3384965660564844605046279268668946624011765635446575611476342262980758831906033248238099254053742373967108619787833503586503469818886831641373448849531630877390478091410925148028166802669404033563320990988051162515770891602837799459936884593108265399703949712254834187480606182963217591666838648761719975466485684441660568207822319631261706663334597952*y^9 - 27838594371935799121013639779122192380199583301839520557937103011177060024490311557621626713195633897650968933960753456496394540424792118245621252365877568775157999379415413510201897849853414409737187545436324834650503676362559993531817696468107391630166702214215101050938248314679514188182060272125132236452611690238202181181840148297757440974218983528865739/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^8 + 25584728636511645713594900803569645172797583523675576570580121669882166459872391690569760135091960642314158016294274360310725793355184628237519159906397996327755920435775297366116106780808437363885277722281268962965136492987989839688741591157458537823389237610699952880337937563680050889391797992890812795438065474941560275463571683146522074492532277047510333/414658293419193464118169210411945961441441290342205512405851927215142956908489072909167158621583440810970805924009604189346675052813636876068247484067624782480333566197838330633450433327001994111506821396036267408181934221347630433842268362655762511463733839751217187966374257412994154979187734473310696994644496344103419605458234154829559066258488249120*y^7 - 3146464020565952284075337079510327028987455207577526280435723798418429560529994317128097624953887474535896515447444811548332867997459374052563868454745966546160865980515730174154336322810890323727582519382349178865424053031891520789899350152690097326531265932873975713989426976011387646167619432276908800287691152799668541834716469239713367475352212309599057/207329146709596732059084605205972980720720645171102756202925963607571478454244536454583579310791720405485402962004802094673337526406818438034123742033812391240166783098919165316725216663500997055753410698018133704090967110673815216921134181327881255731866919875608593983187128706497077489593867236655348497322248172051709802729117077414779533129244124560*y^6 + 85320033222921173797747270172445600534224590560712978197314581334092148889457951605827784378059687703309544963486746407961836021253801171858385879219931555394340925374176998543231584902126653888611071830139714735615206897508152200507401649226965193304744306018805679548461135610426414203910968224970468053178807062522905610502546452266313039751280291355661/103664573354798366029542302602986490360360322585551378101462981803785739227122268227291789655395860202742701481002401047336668763203409219017061871016906195620083391549459582658362608331750498527876705349009066852045483555336907608460567090663940627865933459937804296991593564353248538744796933618327674248661124086025854901364558538707389766564622062280*y^5 + 69269826167239767514121704113533664359649553645546341727747034552425850830317379083392638916180195703230552913876963162893668564519353228355229228238563325790126553793988356724668026159337309889070269096517062300644161898511547361021995476240787475521339522018508296671310344847189276950353028268378939618333676522718187382922762754709668404722071322655987/207329146709596732059084605205972980720720645171102756202925963607571478454244536454583579310791720405485402962004802094673337526406818438034123742033812391240166783098919165316725216663500997055753410698018133704090967110673815216921134181327881255731866919875608593983187128706497077489593867236655348497322248172051709802729117077414779533129244124560*y^4 - 46092866939839394565043097873961403412118092975182482411574939916946321939545903671211658467488394409624070214988879428225948916405110254343293819861217099440925634346584261306128548481663657784361261220217825521500989857169266444067998085529294314363729777726924225296520496692254652933851285921659398217282277770203510869394081612368164664831292187627477/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^3 - 1166611022447936926632986024418778037730078503028889676540020286045386762491908354938039454085887831946172514148195211981867046214140706971063529765018856388930328889096039538636472528308715239226412808178077561576777270697342702315522784872148365978573145132999134157053071097191174218204664775596974607351143748762994983445139294538498836574647551933187/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y^2 + 62666384177058729979021535763198798670807022784245496531419143690736360991334712861894213726137471679088267437346651791600070840801588652756926487452602340072436263755301795490412737198609803484552265646097246265941941200054587093542077787132821561269181849078730439505034039238437032073628103739956265205247886036479480350426458287527500693830880150833/829316586838386928236338420823891922882882580684411024811703854430285913816978145818334317243166881621941611848019208378693350105627273752136494968135249564960667132395676661266900866654003988223013642792072534816363868442695260867684536725311525022927467679502434375932748514825988309958375468946621393989288992688206839210916468309659118132516976498240*y + 9906419160412418366279896498683336992563160038116931108022003205274005736112325801006073550098931522788732204079077235726095546450113501475804308235540849553037054928752717774313802237585432891326563114498046883362407756705827195824366197098235752228350226812006241473256981398207771146587581849409704523164573353575573151637995538983436464696112267113/165863317367677385647267684164778384576576516136882204962340770886057182763395629163666863448633376324388322369603841675738670021125454750427298993627049912992133426479135332253380173330800797644602728558414506963272773688539052173536907345062305004585493535900486875186549702965197661991675093789324278797857798537641367842183293661931823626503395299648

# 4 Loop Invariant
-12078591798607281462530961630395279283309262099384447767360246231935189582809032237045781914503329278863346403039802127163149549647455344106986072226565217342046799321473355252234448093187656709700971764213955702745569639005633155008152203587345273550295554354039569532569598083150438418637094374975154996443627374482335244739820292083642234046926645932102779924219951886980593037923619812559398664188907298356452382821708196156100058568538214620331939661038196400470193371207231350016937/6211696404051188286838192690405208211908306566853216567548495555154594676710279061786546237240301645839714020132738686929753429982772940780115653123674846646076627523655236667521286942243163853511523547520028284160349889246400684775063797742414216840814673424639111164803822811089480336368137418211845531696708279715689258878242769305249361835951994337548499969236074320423602917338658898845033943490049488459495361979209116792211310371878892938500355747624783948572110915679558102569414400*y^34 + 1574624902108748970472433125310760585881377272880600161326500731339051399024747962823809177112521806795645243962169679649803060617024731197624899332871071713524406049509537788945811019143902749834458890142006310336378010135259795783293453227105572364275087424040991902665125674203741469858724706216969933322905475067032289881921076412670157142352839605800183463642303984145055387563288763340174660156965692557911909078136422545422142541809244660711729502182096802042203487201299257991471/310584820202559414341909634520260410595415328342660828377424777757729733835513953089327311862015082291985701006636934346487671499138647039005782656183742332303831376182761833376064347112158192675576177376001414208017494462320034238753189887120710842040733671231955558240191140554474016818406870910592276584835413985784462943912138465262468091797599716877424998461803716021180145866932944942251697174502474422974768098960455839610565518593944646925017787381239197428605545783977905128470720*y^33 + 527217903516812600610565777923762560963153457151304786172083563073670195826546315774138325592274819178453686081558962214317966879394315495236124039412200195345197689275046922392524027334779113154003260163809077351157211760684488549277071116825423564882689731092353966969218258667214053377694268638280470463660695836274679171672322116190659661391796962008563638980612650200049457181854937383547844631663165627307120481547926302853576671176848035619348703954534220301870197282369388730193831/1183180267438321578445370036267658707030153631781565060485427724791351366992434107006961188045771742064707432406235940367572081901480560148593457737842827932586024290220045079527864179474888353049814009051433958887685693189790606623821675760459850826821842557074116412343585297350377206927264270135589625085087291374417001691093860820047497492562284635723523803664014156271162460445458837875244560664771331135141973710325546055659297213691217702571496332880911228299449698224677733822745600*y^32 - 136268471632693973223013391094526177667776812050360769565649177922611093966820610289125970546445091391993168576545715075037254262336900023861383766305166443588292089467366997827587685485379736054910015909347044910894209313652124645272145192683905190831382319307787539944501349881390244202840312532475799373284149335907583465162035227158080414524456346270586651776801093212059913236487153098562077977709612554707157438311697443475107417059621407480324688036412322732476951286213007807551051/72439608210509484394614492016387267777356344802952962886862921926001104101577598388181297227292147473349434637116486144953392769478401641750619861500581301995062711646125208950685562008666633860192694431720446462511368970803506527989082189415909234295214850433109168102668487592880237158812098171566711739903303553535734797413909846125356989340548038921848396142694744261499742476252581910729258816210489661335222880224013023815875339613748022606418142829443544589762226421919044927923200*y^31 - 98452463039264394032167156573863702016661182579236951143933840352385213940293980388017094624686058637049122383380512573307405365060089884425512771893051472735556709665773445163716106467586049759363194207091066735252159587685218242173907203961434322601838718179402577059845613187681975183526658163594389340569682723775195798551363561008500785184118611725074077774139518677912308235860333654982998450305600392764420433570733361822791647347831891153766259902962393538897318577329039378400379753/5733873603739558418619870175758653734069206061710661446967842050911933547732565287802965757452586134621274480122528018704387781522559637643183679806469089211763040791066372308481187946685997403241406351556949185378784513150523709023135813300690046314598160084282256459818913364082597233570588386041703567720038412045251623579916402435614795540878764003890923048525607065006402692927992829703108255529276450885688026442346877038964286497118978097077251459345954414066563922165745940833305600*y^30 + 87036306729939703902447722992991369191481507220285102718210637212103528846552398092708364261828508143238105978149830332747594829355165507097291821911834818431710819260863780293862524033045105386024818824066773202485618384149689437103473922523096147444846419247121058624495308830345063207864147900241231961998020244057401169836208750808991254534526018651572691707038623746223654456860992831144502770427114619534777287442405127124678488603055158081884027897737360927113452561463994216642795611/745403568486142594420583122848624985428996788022385988105819466618551361205233487414385548468836197500765682415928642431570411597932752893613878374840981597529195302838628400102554433069179662421382825702403394099241986709568082173007655729089706020897760810956693339776458737330737640364176490185421463803604993565882711065389132316629923420314239320505819996308328918450832350080639067861404073218805938615139443437505094015065357244625467152620042689714974073828653309881546972308329728*y^29 - 2680862115934681916495351541990386867997913373865962358719790054443290413215788490512548488487322754350835602582395339225459117114002059527860454729228765381380360553374702902549833663749005555014778898379197637151226727044797264407174438550329522669262463027533427573735930830446207001459857150590546461083059372812278012919685198051580974656180480132002617916350303112493075694132490361518949162866577213045324261044278452419803087955913742215465458963707706980664573218712306100052386524511/37270178424307129721029156142431249271449839401119299405290973330927568060261674370719277423441809875038284120796432121578520579896637644680693918742049079876459765141931420005127721653458983121069141285120169704962099335478404108650382786454485301044888040547834666988822936866536882018208824509271073190180249678294135553269456615831496171015711966025290999815416445922541617504031953393070203660940296930756972171875254700753267862231273357631002134485748703691432665494077348615416486400*y^28 - 12706136878371306993818855335807753500187889163043770506957421848006946959456669304341211870280356458076852120914240192234339919188238504266383560611522832665491384428556642930514330328161907427308649454158910707575406562839182508441221695526264690486068094104295538673595662877873865170375309062230115620847266657449196355255656773012469302121184861003101763491499291205423936673457632353423739553331232329094424424005009836078735487386578737910630627360162687940119820392914208868155761723801/9317544606076782430257289035607812317862459850279824851322743332731892015065418592679819355860452468759571030199108030394630144974159411170173479685512269969114941285482855001281930413364745780267285321280042426240524833869601027162595696613621325261222010136958666747205734216634220504552206127317768297545062419573533888317364153957874042753927991506322749953854111480635404376007988348267550915235074232689243042968813675188316965557818339407750533621437175922858166373519337153854121600*y^27 + 460892324292949644818111113945120960096138683433391342408352253606770385151718219134514167267985114783863995690744004618503500655756714360037217595862294751339872908029936289692810518936945851953750068615573933736120527173914727985715993414359798597310572364523613963073080715369099022782635684656655022787199588246134128269100189024256205425097167164376880412462302799887042240854126975997463016632172534006084162955847061003533818701721647330156689424331988696616064065852405867961607202019933/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^26 - 488116335294415073543374648208975865244588905360890133896196297665350153546957111759869239565986240910130733953748149017411061861141247623193296215069607071117070985585437154412739559992830846654568626391502285659559923259494625853658564666830592884062095872765477682645503347268623275924161449040199076547898286411736489002060254569096023970220720749047886106745103338411221000250600807575655185570535076542930269087006754944331443272000061313199273734843542351026133445678095350672997646085179/37270178424307129721029156142431249271449839401119299405290973330927568060261674370719277423441809875038284120796432121578520579896637644680693918742049079876459765141931420005127721653458983121069141285120169704962099335478404108650382786454485301044888040547834666988822936866536882018208824509271073190180249678294135553269456615831496171015711966025290999815416445922541617504031953393070203660940296930756972171875254700753267862231273357631002134485748703691432665494077348615416486400*y^25 + 125649578675410970323185203288176331890956824328805896190200953235488262006684633343062485035545710880422004043105370598480439524967399908430850219912969788491414446937902369516825865102530094279329360050057744356585295777422254414464043146458116292001103404154131044828098897951643385462580936410543602093355030975418099215203448232498489308328780275284089255690466895028415860980899072286861444714819643689717371424403955983933582737129415436877848061839501290641588180060747906711050458970263/18635089212153564860514578071215624635724919700559649702645486665463784030130837185359638711720904937519142060398216060789260289948318822340346959371024539938229882570965710002563860826729491560534570642560084852481049667739202054325191393227242650522444020273917333494411468433268441009104412254635536595090124839147067776634728307915748085507855983012645499907708222961270808752015976696535101830470148465378486085937627350376633931115636678815501067242874351845716332747038674307708243200*y^24 + 1640031379166021382885991185791254005003474298959854860596616123898910317248021993810431033145106217365961577663315848904543034692221065701356891489075900083558696492164156160163959599779824082168423837308089289416798454063042968150917358201313531719230361008024691654135186234581375587191468111726198308659073384542500973128559720672558805326529130326651940746965508667289433069343182415719822530214136773747469206798666204500168056657798196254835023576505034043227382990110567501604738557045043/37270178424307129721029156142431249271449839401119299405290973330927568060261674370719277423441809875038284120796432121578520579896637644680693918742049079876459765141931420005127721653458983121069141285120169704962099335478404108650382786454485301044888040547834666988822936866536882018208824509271073190180249678294135553269456615831496171015711966025290999815416445922541617504031953393070203660940296930756972171875254700753267862231273357631002134485748703691432665494077348615416486400*y^23 - 517026133918466745212790671903877211603144640648443078925586593037845002407624226735643429866571459604809389601279680597249435989292109971062343678949428606482410317618820663759037671871939358333340984743719351548159566929577766905986578571218039073251409234767417292234258330812098972080693643194670738667137474756636816106238543008767230719801080497294066203715306468384415065223796581734656177636578636718499760228278016033710352254776743583912865099110235499952533187410327436762883973691831/3549540802314964735336110108802976121090460895344695181456283174374054100977302321020883564137315226194122297218707821102716245704441680445780373213528483797758072870660135238583592538424665059149442027154301876663057079569371819871465027281379552480465527671222349237030755892051131620781792810406768875255261874123251005073281582460142492477686853907170571410992042468813487381336376513625733681994313993405425921130976638166977891641073653107714488998642733684898349094674033201468236800*y^22 + 72271066354807504333403776723199719168719851470631975032611153221409083290936913090724306423395692416554565716121567952500456279660511909972550526940678628399624067893571842667571924456600821496845944562777592738686723030455932410388697422872939974892379230143563285011019859021944284634839916293425317209056760747851070389303713968206575124845782203843385617621007291965213001258874803649863404898938037194617343765756761845386524013794186577505073874435926064870255773933566708292383771458511/318548533541086578812215009764369651892733670095036747053769002828440752651809182655720319858477007478959693340140445483577098973475535424621315544803838289542391155059242906026732663704777633513411463975386065854376917397251317167951989627816113684144342226904569803323272964671255401865032688113427975984446578446958423532217577913089710863382153555771717947140311503611466816273777379427950458640515358382538223691241493168831349249839943227615402858852553023003697995675874774490739200*y^21 - 684630640785769811314374194357598107032739444171978827611864898641287396340420749051024861048330872400257798578097734073874256279472011396491910791233903285816020250132483801394606858816170413503063777027947078373048768838211687499644192792352448430443475802870361269422896687442822019275925680474770549639471837683826267874201761966706302347056537070461288246238067588060026542039352201155599864121233675369933307627822122606013082444952544658615604273087984833785096888059563638639705430899849/4969357123240950629470554152324166569526645253482573254038796444123675741368223249429236989792241316671771216106190949543802743986218352624092522498939877316861302018924189334017029553794531082809218838016022627328279911397120547820051038193931373472651738739711288931843058248871584269094509934569476425357366623772551407102594215444199489468761595470038799975388859456338882333870927119076027154792039590767596289583367293433769048297503114350800284598099827158857688732543646482055531520*y^20 - 18506096388590272189588028418335648258737090675079117301785453791317465815032885878969855266602274964546910015203583394377571531669006157847959710971038525499369762202222657272321005638547267234867448345142697038515412248735203321668006457936768913364632557965686017481241066382764484476968495148228955403346939387059244265423313091364569025330550086711131020454462390275395720430195809585330684833062447813683758865663146912836662247449402734918463832954060056833980488808058801032225477582558123/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^19 + 62742049102241146619989224122287935555100044964093376371974709834689095951890818355875356338978824023599622703246612727735420557351236151187692046466740952372252523786104311783295732890677986831165221205162673396995790601511009022500973514998832385349341835710407104436382230027408078773171164257173141861940235551799618742297113520582530233982801081095514345725284110567754008782146159444163285443315510531857083157952839299730649971357245025952417840665019149991611748067513290604015328110168283/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^18 - 13233218117528490331789494773396478031170819721719107566504065768361491363380008001661737682028269554636041047623383312824703833584238366040236972381846397781405527910412645122453374299542896999017333777361018589219999942280274131906884220381609122078434821094437612047605013527036380402904609724661521984372194676636954378091463754584041082389206769464108065155218758628284165291475448265872275157507013611273449114440770529741942715549205970404422768706947931692643139343069970434392156223162417/10648622406944894206008330326408928363271382686034085544368849523122162302931906963062650692411945678582366891656123463308148737113325041337341119640585451393274218611980405715750777615273995177448326081462905629989171238708115459614395081844138657441396583013667047711092267676153394862345378431220306625765785622369753015219844747380427477433060561721511714232976127406440462144009129540877201045982941980216277763392929914500933674923220959323143466995928201054695047284022099604404710400*y^17 + 69973280754176357625936125004260143969501027540286056523682276430563596011704432248403470191802408644216802814532632531673934378078523540402879462242673228128656106192855828899980419167954852633636868474823433992887898970946417341607655984746544829138423193632644031232337455778786671427314464242471134109184179170769801320771986339858174336876355705855047719231414712397246207639530724404757508043137092239543961113842652609210549164941363341668015059876137921864117182128466074750557380057271081/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^16 + 204021734323835979777593488928274082159684531173278326471534321846974598191209596041959734775264048819756049473427115596275413413056780333005002060675541203190351283433339124990824035693754314005056875238005457979150580390392067359409051875430361175992356301926385986361192816582209818624596460135338196599186924115534975856947694355421060243504105929685551368295409489637268087427043396813997330819794204762391564252554608009171946808458102564785178916638197638527705535327143683609964170259941/1911291201246519472873290058586217911356402020570220482322614016970644515910855095934321919150862044873758160040842672901462593840853212547727893268823029737254346930355457436160395982228665801080468783852316395126261504383507903007711937766896682104866053361427418819939637788027532411190196128680567855906679470681750541193305467478538265180292921334630307682841869021668800897642664276567702751843092150295229342147448959012988095499039659365692417153115318138022187974055248646944435200*y^15 - 11047509604631426336834800823094379749902824473403536877915573988080805142657364654712401963677847880310456620884850955862645667110518480302497483689361291552766786137022942139314877011022044813770839724181181585013317854401498709712822963444269589193240003685616923276702623111504145799531660159873787100516993500779651016795548607962257118381801839302546530497391914056241339380075799287942959164419819029155998152516115245851441872442017489600739997194955162193254384869244243965565259820115217/9317544606076782430257289035607812317862459850279824851322743332731892015065418592679819355860452468759571030199108030394630144974159411170173479685512269969114941285482855001281930413364745780267285321280042426240524833869601027162595696613621325261222010136958666747205734216634220504552206127317768297545062419573533888317364153957874042753927991506322749953854111480635404376007988348267550915235074232689243042968813675188316965557818339407750533621437175922858166373519337153854121600*y^14 + 116203204345782551953660224122033645983012301956273939772868670883808454016087800204994005483727674376043655764454515991145777965862937266404396052866538693842763939792422156072214007283105447003570432082087967050772493671184941464991977409230921444446254339760126172469540924161645705329172488052489315861380325978174523586902345630915533706803656335700014291854945238506466479021002575266511162919264672801437968673110973216874931755345784175708424139785551946623973285532121961631797306222932311/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^13 - 2887886169081179580104436628749716637302390926247904283353900689552034034510267890228670075842598632802354473872312036570913399412002973609816057375648177667299288582367978193451562501768580381976121667232033443930078594097817633061356848079487992726000073753684090468735625129413293301928947656072434760185038535281032033645040712135036326166679678102104761390779414799819127921015846175208195491238707886390150169549639020413762388878526983755105548980590765645446166498557500912912771014212847/2484678561620475314735277076162083284763322626741286627019398222061837870684111624714618494896120658335885608053095474771901371993109176312046261249469938658430651009462094667008514776897265541404609419008011313664139955698560273910025519096965686736325869369855644465921529124435792134547254967284738212678683311886275703551297107722099744734380797735019399987694429728169441166935463559538013577396019795383798144791683646716884524148751557175400142299049913579428844366271823241027765760*y^12 + 36702201916024567835837656830958278429570480554036842247754646138983635307590440220206013639474372639069601111569965938189800797141901354188849790656671913151305165373868027204766867834733006424703630873569711120751936315382735370295628113145103643777523867484334202622165530011957254973409192468891084365230810383140055170495027279271847906925142909394333176553987250793870149351611374183925290185168518231570208290566207425474953128084596977645147112650077158202957409030762249740104112196493369/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^11 - 2616206959790332245152936570542405858911061550108984218831266127646044390393477805006295481183931623030169781777051002893803976053300478368718612623080567323839119765785531969244726771766833727445798888374065601684099024891621001946618672397827528699769063776891853275062042518911689795085984833279863191414851198580009811135217456238113723168760865757593768292555623381408145662359585385822570977412585667362706052943799267224337224481869475942879061711869930587017316274970079669695860461383/62638955334969965917696060743581931548655192270788738496287350136012719429011217429780298190658503991660981715624255666518521983019559066690241880238737949372201285952825915975004574207494089279107800479193562529348066110047737997731735775553756808478803429492159104182895692212667028602031637830707686033916386013939723618940263219884867514312120951303010083723388984743767424376524291416924712035193776354213398608193705379417256911313064466606726276446636476792323807553071174143557120*y^10 - 5184065155892748329696119890963126972640687936646124255259034230940117070056980904823774342449956649885325483167480334635331676422081384261185299020550069435238662320900367937780406963145342031874852631883142223317295297632227743092801097295060372703324780091245541084285415517779511369172691419801691412960852932964021838883103880868689763109639940196497369541013581497817233441629171943654648383617711176974149091073729869989580509735370723878075205079556144728349343185433320294878606554059/60849270896827966891476173293765304932979329634480488824964854417840927445325182646072289670925403877613525095177848361760849926361857379070520683660488293675852677782745175518575872087279972442561863322645175028509549935474945483510829039109363756807980474363811701206241529578019399213402162464116037861518774984970017229827684270745299871046060352694352652759863585179659783680052168805012577405616811315521587219388170940005335285275548338989391239976732577455400270194411997739455488*y^9 + 671337519092014060231637955861588187889887602857606075222243564026036792000541794243233264246535662684885269346884079216880036042096908898896712323531002825599581869962368769812858110251195432590940112258564373999539867155918405305807284307378111725591076633389988613550130882157584181853454157659396434924402996504701931326484818320872121533134881364498522501204467908811071142703261069952638909469490581762542441013492453193578202509982469157929714895620773623124671019268191727012862195699779/12423392808102376573676385380810416423816613133706433135096991110309189353420558123573092474480603291679428040265477373859506859965545881560231306247349693292153255047310473335042573884486327707023047095040056568320699778492801369550127595484828433681629346849278222329607645622178960672736274836423691063393416559431378517756485538610498723671903988675096999938472148640847205834677317797690067886980098976918990723958418233584422620743757785877000711495249567897144221831359116205138828800*y^8 - 316445305549321234832985231167249381099277209896039126916014223449225307289761871798387678153457887728352439701596164075475039391006768936785894909425333774432851348343823881448914832768133631397503925414617355657096604805681180182007715975643403570214674958424487758077727844564616996832630412820059467794123979345123718016595578795684945397078381936916735233206469850078026315846098633560440852836069704498202226207992267613898315685752225769026943175343005335277705000486674856807487549733191/24846785616204753147352770761620832847633226267412866270193982220618378706841116247146184948961206583358856080530954747719013719931091763120462612494699386584306510094620946670085147768972655414046094190080113136641399556985602739100255190969656867363258693698556444659215291244357921345472549672847382126786833118862757035512971077220997447343807977350193999876944297281694411669354635595380135773960197953837981447916836467168845241487515571754001422990499135794288443662718232410277657600*y^7 - 34594928977963959269199501255799998202056406078353802664271237209914977089544769231117680165216410657215553922309393667448388673488223057921033757568428208272151805142926760635251763375239212305845679225571646818240472944140108130711694832346133893115385428842717120717874236446647477654954481413121687338886824208761015936293505341628917241319733001331254501312757752417887173543694766584534457527360434209054391458556756378380099116262955704856849553401978368232115222345560944799274798959403/37270178424307129721029156142431249271449839401119299405290973330927568060261674370719277423441809875038284120796432121578520579896637644680693918742049079876459765141931420005127721653458983121069141285120169704962099335478404108650382786454485301044888040547834666988822936866536882018208824509271073190180249678294135553269456615831496171015711966025290999815416445922541617504031953393070203660940296930756972171875254700753267862231273357631002134485748703691432665494077348615416486400*y^6 + 97675681621148716697405965794468841127488449084918269564493469426665336818395327299790646869416344387406513724466226586115507305176754247390815526462060688460829503547217934325502283971899180886129815128351196627393337276830783384828963536434767027252993953802436378653054315425552320348583930339322514080873460751837007779798364166516917947068549528278740167305924265098945735634718661684907190645437342807184448235221276239497959968819020849116310832233293925765938213352806429985477049737271/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^5 - 20697035679961226250640951278826432112052376477520451526587398170075015381445546465410969650985387071476873593865015956140566929102860734980044539342531627675086488358435427456118049438527310722779869497763653032091774569647748213810344535021242146000671566806308474970367541410984907546413879955967401809221083053674105463134694321951263572399818617377089133880099752066386405342379115675098078467813684069544490095267676247837476709435381607019322686573369098364470191817827945599884628093779/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y^4 + 34527339775840757797332291957820218909121921804697793591033252934781430551826958050889078448936024666652408591922368721175260385555499727503779373710454123225175356540908756423774657381103351429674666219526929617221924287903961124342582464778415585854045880036706641232431628712185764747669693491984827770541839923904874885011540732872506884332972140279644242467621526129803141763202769429055286226325820561634644007507918065495276654035292085253037576631585342145378436047051881897434505169/18635089212153564860514578071215624635724919700559649702645486665463784030130837185359638711720904937519142060398216060789260289948318822340346959371024539938229882570965710002563860826729491560534570642560084852481049667739202054325191393227242650522444020273917333494411468433268441009104412254635536595090124839147067776634728307915748085507855983012645499907708222961270808752015976696535101830470148465378486085937627350376633931115636678815501067242874351845716332747038674307708243200*y^3 + 265582862878980676664580510257800652358162955124660454755342825445389546605236696858953780301561346131572579615879166102586761070701964808905194153072838919207632794364979373329079967981836105680750278825545197661479382095066451743354242798423148780030158589935792606868731365214803832521972043200259809419480568359712110204971029412951209753445054924031198965011769536600262875898369889882039268166921055606092879436742723838441644870391158534644030830943488286876793308970004900357071233533/37270178424307129721029156142431249271449839401119299405290973330927568060261674370719277423441809875038284120796432121578520579896637644680693918742049079876459765141931420005127721653458983121069141285120169704962099335478404108650382786454485301044888040547834666988822936866536882018208824509271073190180249678294135553269456615831496171015711966025290999815416445922541617504031953393070203660940296930756972171875254700753267862231273357631002134485748703691432665494077348615416486400*y^2 - 43317062659428766667271284892786104944747321077671711844189576669078303277419731229262223465261443188752244499315288280053924066239043972138711312479124367455130848701672790358987783835575768144071558906707767773204865112939109257805142450802375731414362768357989543930981120195100299812361413845445806654906754244714916329366105551675915420599509674125270975992877086153534324071596854409895383377139544398782030963057597105649023067419944834287394305894510268321982480020175197256294404539/74540356848614259442058312284862498542899678802238598810581946661855136120523348741438554846883619750076568241592864243157041159793275289361387837484098159752919530283862840010255443306917966242138282570240339409924198670956808217300765572908970602089776081095669333977645873733073764036417649018542146380360499356588271106538913231662992342031423932050581999630832891845083235008063906786140407321880593861513944343750509401506535724462546715262004268971497407382865330988154697230832972800*y - 154834612042108486307725881296630250824127033107810095613912189679480296552526122054720336860304423478241792993317311031799081188804974122178946304316831569455143998311892883566230798371930351198987540558554226388846686682292109441856954935936582417970271785979458236416226414141911230612073510230904117051913849400086859400037344323700828783647794335385466976738139357764805145857726018414306499390786047454424537258190843245253230639849783858795005454088520085410809885293592264413335053/4969357123240950629470554152324166569526645253482573254038796444123675741368223249429236989792241316671771216106190949543802743986218352624092522498939877316861302018924189334017029553794531082809218838016022627328279911397120547820051038193931373472651738739711288931843058248871584269094509934569476425357366623772551407102594215444199489468761595470038799975388859456338882333870927119076027154792039590767596289583367293433769048297503114350800284598099827158857688732543646482055531520