# Manifold: Census Knot K7_31 # Number of Tetrahedra: 7 # Number Field x^34 + 3*x^33 - 41*x^32 - 257*x^31 + 287*x^30 + 4575*x^29 - 4858*x^28 - 29689*x^27 + 109554*x^26 + 53026*x^25 - 963371*x^24 + 356533*x^23 + 4126757*x^22 - 2361759*x^21 - 9794945*x^20 + 5896708*x^19 + 14187898*x^18 - 8022006*x^17 - 13445120*x^16 + 7137531*x^15 + 8267975*x^14 - 4522903*x^13 - 2968947*x^12 + 1810658*x^11 + 599469*x^10 - 414847*x^9 - 88090*x^8 + 61671*x^7 + 10853*x^6 - 6326*x^5 - 939*x^4 + 398*x^3 + 46*x^2 - 11*x - 1 # Approximate Field Generator 0.352085190601779 + 0.0585281503369621*I # Shape Parameters 2870341956802386939305591306404263143224664074210192563478240098425485045412409967984168454489553783203/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 + 6417698877071572470226144611532819579767010885173929081896944708794532855727637446319584350275469039261/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 - 124071474758667826747820161335140705811673628677724863372333317192405576658067184302085735072826817292166/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 - 647441552258311447406410599160241846380654551098750621047207230491852528598580406307069854843143775937918/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 + 1378781131920683319611411850485408653819728478222502903966207229225889246309824257160772574373061029172655/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 + 12463804231867257304180647417048664741050359963342609442877103339037775059813410539506237907564051723835301/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 - 23854836210888002850938017812406233067365988885853393043500479354888846794344405669026072580217795152636431/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 - 73758202533871208688448659724559869193866275785985338204031546043169833078315562711817075112456705595481427/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 + 377425251398948247995907318951887936265512130929735304383606566995676755451087696528868358543072716918334250/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 - 92489091567602038053972210353831415964906624641957704266076433288872899286306750594951565408495951517648534/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 - 2852643437636953007352292535477316530788457264639742137589371869054131205178591909422947433300969645979809238/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 3117266377952371205839673172561250804442613979796574191906796634438364474979980150966600320470258778090425957/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 + 10865018914010604739909514149871891656008636364875090844305280551550592417264300472556952741317757955977498425/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 - 15507254451099713829694242999584723132599927864239501176690578090441417689453835090662255420382331178163737248/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 - 22241807779013261451966160162049404614156007977467215288826303489154920350074220505264556109050942562770155893/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 + 36883167236997642116356547927821510448688163214479316336463679333785966089230893074309725555169027815931846973/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 + 26544923191833965569937862361800873496252337252970464128549191884817132013662931023975004749045039728804810132/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 - 50533098526314586410248281727169681365903219111413888263356128525991981926877212892846663607796220921470124928/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 - 19816370874290902583589045591263677746033937953973541396664481529325131909241237350879791882274247720723237299/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 + 44976319669674669523694902620423952891764090975265828775401230635505714400538719232635511371237888290923642834/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 + 7524923050257131567408107987384683188442119971428662230746475928904803536565633191829636193005722757556113659/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 - 26625143186617077501234832003075325675016533317493937076977051073350510726172125700373357479308661319092534334/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 + 1246489320356799375764029450100867678014202867052708672696358922771079129178648681098691489660530435578367120/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 + 9064601417305672140476501024258363787817995794264449717743073085750852281685742184511678559786702788272802294/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 - 1767354189085075841411730902182661542187573405781604837693536821397044370449467379762866878926333627695445952/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 - 70406956441290250611720082722502102437204589732970048180528125291838714594908506677230505915841839289429533/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 + 17026314903555390041468432911544274507196576302912450403649475313209651660469186156777520609580997110168642/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 + 214175510767547095553308315098283383204803287050876445959838460032086606135692766309036992263786432418781541/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 - 50207367772718864620145339988337369594424969260468324448649875819725125412114021001425016646335405499361759/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 - 21081714809379530368839262617467487440434781558774230636005508681357002420174120000518217436731658155263383/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 + 4446927488393585956239079650743401031937146002397677765776983737360195501313890396699485223765580072036003/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 1081830697176477090197815560178151102159888428235579515326956489939921208542597782153991896265923171039538/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 - 174335467804477109028395122509843001280062322433060563124540721617390037654932088943289560450861412364494/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y - 19745645570640361825206992654495256795139621971795609875303980497962633422029865360000229476433265377584/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 -37418518218410900532055589215038870635988901259079048118776748937348324948934394529227551666198943045714/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 - 128951604111207632124587053721044132430031860589702644118649193048354145286796846906754019500558697881817/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 + 1477013187635826151877290243955380990521168621789893483643433001847550275735596691435664167482993718238965/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 + 10276813161946114311471797416047319987085877493616856748541176674524452250834954478801517144746124501884252/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 - 6169518455075844445894133917068122286596445973576286461581023549788158912679339530046639002572739936116120/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 - 174044658661367280248715264653791611871524969814589920480430107610046198506489902584121080980065366750691296/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 + 104221074878568650755632070682400092126787231715715391377851056718354473115607319138811806173661837892161593/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 + 1159210484643526574810650252399668071201950658074887464180352254916165535725162001579370786716838609754559327/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 - 3583824446777955446838768939223619509593151070546077479823916901841378566417483167381761743172003587371359358/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 - 3594812838520818034662720165586192072249011096712363104163068573225443344450670242928969367105236310470683050/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 + 34485475142435701771820205852647444808097347713440281761497148225364314850903695591864808553865671982269730465/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 2069760078892950363153597800951757077861979029588237861817301155911569209646953847757788661975400323619531285/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 - 153863280199215564859772324573799717317445043861598391491861884441679988654743470484641100705200660103969930262/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 + 19826327827494289290935617214903519992192483528670395455995829465537732639754769984774824994980083392615751304/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 + 376937312191275925397611342144687046797418759200291915191877231627304958358096979279271909089436759154381149237/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 - 53213348626175367732281712756299207432221427405592304026477736918039640555666564821691860639271045885557591157/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 - 558337308971821663557001671740704638358782693158730168183283767277270769912622398787849506038406709242735746602/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 + 52890698970542350526361255071222077799321510690607708414408087727276738000626130393915968253367026663832202923/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 + 531947484513541850007029477316088673337520453195386137692829244232021321509856120208865789713695117470008951172/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 - 32112005007815829390481776153694347308841928534296202359260007828048574076431016494925989563857490130791887379/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 - 328513460826026731273623214325691769707868665616498394328396213495332145811057082425947150571576988858046632055/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 + 24679629429799622334563762685693965711714825566873556412152074433396234035718428076856720899462109959129781494/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 + 124911151458472997611407518998282575679460361733732090991915726136492083761128520181589017336903228718434265480/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 - 13259816102902790303248247107966214913567161575435401982841209756692292019752972425074924516079849902227369943/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 - 29266505467388390312721037238687101968023294874151903671138626816890630207579446676023571667683517681069272944/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 + 127272332454994308936768778486864895178953363024007820102901110487881590300148973821302713713552922299262103/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 + 207120374939306374884372020871707776336183955294125472407128205182410723779198997473271253362852297192385668/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 - 270180916445457398768326753087959266619474349948195120870585024707782684178296561711352784612269676402656662/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 - 549245604980547883587184865816268955923580065922882291306697087752303948298843077882776550470776084719232921/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 + 2370332006473725946915137752547592102301481516709458816827922249835494377665873277716543067681498174575422/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 + 38657470353199253754052088103484583077323931622015830764130541674774614064780715370126989259787285672322400/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 1498619490369785671191587240728374158355176547220832898317301902933627527785780535420208888053095821809998/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 - 1194846245371767858075230200782449150013202273356752188656040170142888216655603356384381169850882506766512/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y - 90379561921162732431458133349374464309579231280044866646500269575462579064208159540676212353942034032014/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 15791792201965736981458696782876169577426437437290424394164678550854786672748555825000672833347059754168/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 + 42852887005646286471569875055735787879026091944879635389380208293639568392107000475409666598319083501408/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 - 659394361805182509950268427730576000341215247645857726975101876904625558271982126807241868356088770054423/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 - 3868566868531761515814747920923670813052036985034490514070296322854504482801517856808953970533238942942598/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 + 5626375835905291141253865006984892963947186745040529798397359385475499580590284132558117602980269038032907/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 + 70546118485116169915468234664171007755729274775819251405542605060511484677199365830838496839487690864420927/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 - 96839632265024761334193875347955930690945645017752610480132332494702365925839796361314371380259085110042225/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 - 439545799392572707418993099521890784064178050014788801313726345727796885263190626565461708510662552886100169/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 + 1854563001563552232979111495289539751364424707255223893428090949184894208392003877325289954685093768375820355/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 + 296103396759971819371902083265864360307950234109351588444102544265156311640681151383506249869325307393841386/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 - 15262757608527047603807884829515813765019950080672423181650119083156685287745224219625788636710435167865520006/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 10024229748449917283164881363183122388935075011628082251623762574289670981094927989558376769431440983303818197/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 + 61978379733814832880056466023789661255379531464033231575619244379549977028848499783245299421513096845519994500/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 - 54977918057185183129656304528412750943087592379393360615658732785997402553549159880189125150502296336260894716/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 - 137559583469084289784276883256121285070384538349163200279890640793772996328057517570777704253347578283391410788/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 + 131963942277101661246526809732934539462157241316621500863621401749866991766440068311632580742978658493961049339/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 + 183013559503802781240451565650451573335454788645862024631928685647100899102333486838206369207188316417347341126/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 - 177745024628427623889171096401433277737945969312637666125828548883850605175828327227356744104703684043284590405/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 - 156795367238039138993417326482376862423048606448585235063951835983838646947287172128415827825800783667693466729/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 + 155915758500910473325217680804007607223123526190227401633063518594372577624902730339583183505949657042130325899/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 + 81674843131608374961500992984156988091160124975440069365603023921257379622930708410265162307148606460418860225/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 - 93407593327733118623302362444262717688968924859133882753566702048261522286181668799205343156177851741945712843/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 - 17660715886646852950064672943724376185667025507059417889559890616017370566727543649609811936056212932944283616/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 + 32778210386002525857366481487105894822059920464716511432968308958036407127061630010356315074148512313421379095/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 - 739509033849914529830252643532135682457675428844032372982858524354144572319755428155032671931920855156176088/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 - 261268999894567292646690130567286387718416552236676794128729232115946688132662086670296078139335005492995860/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 + 20789863047307643278346968117590915265090026887020551155018765802220175583964109550626350884197023735970964/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 + 774857837299014799030978905177603563137527956776824552604957141637069502543894186190292173348019119001599968/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 - 71217282779304166224159033023378157213485848503112222987497264229949804811554735834510234585581261494528374/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 - 72196130424555936192425971406249380913407866707813060003118462046101478477817987899369426667120010585469762/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 + 8012653618445547763789854782681230735874765108801547915721085261417700234832686725154501920443227459220243/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 3430625873618351827738743077280826725049460544842984872346280551397920061718032384109703302965908026063473/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 - 372278200235855819487139690966139895246015255060444969887278828763194219065336771139573171614537401147603/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y - 47660305113227772833310685449743367609930543880128575576690901470169676260436332928070586132512221184443/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 -9527263821994942964212026870172219546913609037749218156462434423389684222846925364078691766827834177382/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 - 32917339113012156261546513367568128380657956760750167590421412361257084878709172634386225977089489399438/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 + 376313824509423803949391401982358999651051313135075870042166114158154588637309918871482733851552930857670/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 + 2621829058228820075787416482802192443522729665382780217544130899311610499543732476262467450522228455494558/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 - 1568700676897349089668873487941734092193377408200173229683964748935952742891285599434940830690540965291206/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 - 44476436835220493151051499336234116023501429102928434327047227090746695813639768672806563537293289217394661/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 + 26222450625867488131140930713201955464102049269648432834193021009090861072240768054518676285007843223548956/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 + 297873160847096533183349025649449495393545656420290023304802620799426145302677879626556528952122287707462655/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 - 911245094131401918244837691838478429128206213678948573731903171976520023494085423832381897675804964463550019/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 - 939821303423640705409205455142843838281974434586723898085648704629474607236175950384721921684507395186001395/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 + 8822908117480942673796450975227738841076368706978492565550103878685052593185634823604557102660505009453935221/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 657041223934781865834547866625346800714940970433419726668042368282377939745781461052339443828494251424682148/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 - 39658311404472911183860413766081586334771666012840496249061493827124659333217304019564019519892032370881895234/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 + 4653937828265666931937028738841476036910087256026019632796295120476003414036954522265301203407813436177975033/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 + 98172243171659367767095988603473674211692861856594557839371819524917725633228895549630376130028111931133893692/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 - 12887257120204912812950668967577647684284939559130702734842508046780747455006488531671313684129371135754503799/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 - 147466140872764543919067950408642052420524132201480876830020805440096991755345377783248620660784273361855288633/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 + 12707537655978251916700890354608341676016895566971922645227455263348011178549625790924047343627399034744356257/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 + 143032153371685779360032797518466153938295400096205031066530768110103593608662258397459137125541704961749047113/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 - 7330269738410435609928317676164270328738056091095634534693754582664330045089267526894307909130151252464634774/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 - 90549142080089421575929400223496145153654419244874012142287550469340567383384482701130359258648033819127898039/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 + 5644017612947715760043111320780996805905823097223607021120393842843455262829396599306559421099181166399026888/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 + 35827050261959406473757879984427439531321240091414789682258766297139483444128084945258665896143914230070350611/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 - 3251455426074506897033915858129886143321795977286597317499365609089776495267335367514528860429994665995215602/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 - 8842243700198073428611330818390138795128656903010748631633676389226972645673296481875371115928644664948715070/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 + 34309990125495513211558604219294007690392182632214036650120190344376602293385976268419388565029746573384197/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 + 64909262084772567299302416840809113458979099578154417222190030506650285983933574794313339787814588550192797/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 - 75621108373664028087039216810868235312494363190561239990850337916962719815412633001896523310254393229645334/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 - 178936328139415735949890330496966500456225904948564519907771024326503098967702168978510059540297322122478064/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 - 367079834644670207192627888649498269726989328946083419030337022132110559803376484288613181725174988331297/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 + 13413135508146855983945589303139603717167895197262376633285726780819335613208315876684310182410171270072577/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 610698958424324484952540024985977946122479503285878023161767505098157392648459868836545681045930943203006/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 - 448967713140049843701479763075195193356603521274875420154029491460904560496754596823179938058546815306514/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y - 36127912671847508811747080716490027188451460347118825878604485798100059329109481246825707973261670104152/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 8042637507695811060443160873057246522788287963798980905533319840498859302504368218183247858401328439471/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 + 25354851333638507301100349619699986404925822181727300880440635947355037866133752685079492451562469274166/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 - 325068406026821746109040442013385947303983923232885962977625348917631540170704276611118754027377359627499/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 - 2114079611368594570637395137055821124187013843910323182270721989064887142425260687522270318706381156175229/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 + 1952631696198445088920454753487599559008257255442968281449544878083991698198095697533130780393723858690009/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 + 36883219682003501663732785475744754233081969263877544740937732450755078388642723959038455998678652440891153/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 - 33223661036735314320554881074837544448730362106895288539396320687634824521342186289858542833085057660005967/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 - 240145460710545219951752367946725314256809643069271179900835858207507485433181492275779165087141515511136408/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 + 840701980393672233280497766075602696140124380079040037601470350647357031631536508823239109772735732163395024/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 + 530856854861029902400215876353930918181722374692422148610282141786621911762062452513683631948223506611263536/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 - 7579533233852144501717381934102319664404706256423571109438445730812569850563649762213354852316817031607283515/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 1755326067328541550679936761814370438021367495194876256781618179674924854848594822110041339160974680337804907/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 + 32686986354379516179475892092354716534258183282611639108787216916056078589303190803185879795941535987510510208/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 - 13746404722655595003544835086026534846948108677506356888752840246928926046164167832225657792310122029633542356/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 - 77595462453730676621010536714919798087132809926705560737436915233001468805830613713879326212197662492324588915/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 + 33837255300716703389824592631306929466985215000802102375031023331003317252475853058409901401146757046054543186/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 + 111593800308789070768513943235123565895158846173935580360679318253234077433265309228831394957185972351271434913/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 - 43225343774988752080182522942979811705175912941417123556293244136319079442765643142154753320915654913202488451/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 - 103845115500715422809810591374564079783177148772731125145990012973619343485172628441965615323510711830824717922/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 + 35988839088322194555588919672382212960562119481153579240140504508894660637079853977345534558137036120000213599/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 + 61988654610105795195601741752982806593426323406076464808762184785247467185213662923794760380264966079140311863/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 - 22180405142788547599087638917545162654920972465503773377332241690850793341703391902358536150483790888367258482/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 - 21407941340554558913038968667047119852202511518642090351381866452185346623710404897286224833972662655523333222/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 + 8415115099288149239993403519060111658230477050623517451890515153206208707544485315989481933020392336312023434/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 + 4192924363832779396012968068856725459998094496899024528238037725731915953429561632755927826440429832393044841/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 - 71190625839497459546939274191001695912997725066862896824184742766113513897140373335276145733654031578290866/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 - 27309393779742756361594387553532804010921495751919037873667117694193322470522243658837657678253713679598091/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 + 197882950524511408258106303304127389608175584772660967312045699585832766187006548589201287586967315459314767/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 + 71503702038611843329846370476094651982455030476569847018366524868246807184197693957427275246077283791324864/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 - 14869621419061684317887877292127773829647911750626495668057389021908247495941694204115958939799376894805109/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 - 4687760731674384548920631648763261160128277045147058442968965856616761009312054530170216760784808027467136/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 451174078319021874514290437272103485272849706133015714003221731539279915937131288637359562230346148143649/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 + 127998697688513347633227440489012124619797198181235495285591991184557725907575094243885348743861741908644/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y + 5292521176712782916187734600624398660081843811340089793913855551558948033569788602057585274902151146320/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 -20682582389608951650662788348342131405485407265913992734708029308213008194426492827418578555119315831437/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^33 - 58375402131671693726805898068464099697150527507758236229495914905363595818891506905418072125841373744222/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^32 + 857543558360722368845018341589987078387848319977769335828050577854136533453572793813726157156535901639686/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^31 + 5161040643622516015534970777640184562164427105629961272671733658559844705123084070498526377822738865938752/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^30 - 6818201695884249947973296312571922687044888403190775718129149540254114553638685099493668730076306161201648/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^29 - 93216774330547488784112626559625380178077344501967324310360019044142091763742827199605394745626728739029144/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^28 + 116715270759568769170949453921314644372295235460566242743715254229898604544068437122717955514741121828200154/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^27 + 117938320158008690759645444655619961096093381425342047379053240152860907494794288427500849664903282188798791/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 - 2365266263789047577482280066935099359884569346674345818413129079695154192190192546177381013193801307014631903/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^25 - 653884531039086908694408269296284718461594979443304876697788301421892580037715975518869506839772219265206326/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^24 + 19943798334722087975440481864676016202406444825405988562212682585470980537442389271042549253200534942342493559/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^23 - 10927422764596095238054212890431594318226232180179103481954312600300437808495184253434472642717693131416995344/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^22 - 82612917261082632786901314436313497694944213533673093749454151010029511504050168970349617601685031067712165286/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^21 + 12590153836285221798403982491927662141525896111559648717176377910761420683710719044753769175637181372670299983/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 + 37624153819595919944618504941114635574869967350452663821144563735067966323625032899619514557234493202523895974/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 - 152274818837966410066685463429442678088803556692659844804495350929355334651403958472832523046086147865131429356/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^18 - 258904201296383160885425665824501340124534772782076958451480167556734121081149741197709166711788344097264343194/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^17 + 40880225424132457120102715977774233096250623047232763117380855357475802085287013523896947306700113790528070851/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 + 46262759959069113300509206731004445918367655377942440030181387918633066727288979187446310395184528743313803577/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 - 178479563304382570807110450124327904669559636271808294851897908239728676595438882515930709371590245239598542407/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^14 - 129645523920313446969718557727731031843111220108836354598509368012539870174494155419832397651878372559632183146/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^13 + 107571632543941913267056424819198371025792581614296302203821492836282297890413694821670802323475477513484163723/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^12 + 36595277003079480049327753739664756966059501774234549820968418046212998536158479990935915001076538097662891878/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^11 - 38587643770638738529407333510238649671955402532384922814839511872457841313946866447464921295938543106614598112/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^10 - 3769380640932192329940059254527781286296710020229792949804276805209189619681149370496786526929208047112320979/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^9 + 318973095314034754494743118371419323121245432204398411846892234124693720086265129452431502066489513299819054/145969654622892461644692694909267066340761457403069052174751258121309879599637767122511366264843276995*y^8 + 11614982747259189429021206431487085565984470648806855323541158519432815364763762418331839745619464041569117/145969654622892461644692694909267066340761457403069052174751258121309879599637767122511366264843276995*y^7 - 947787904854535264577674252224420950444317790595651465203283674167097793081979953645445822826701233781924029/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^6 - 22608230818434325155780142228355441005540559033409833424436826317569943805265426655043005867848094903454693/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^5 + 85119505576962937681994053355624659823703596098886838007101180542985145088854286670998203374520148202606388/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^4 - 511992803688013976533976748546420325500649169640633089798817415216311632676373906373719864448566474020228/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^3 - 756332683865112637812597799273572546979362677153451198034210086742298494309955160078602352661621101158614/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 + 117742770938708869164933754541467256783006065486297173505205556178613243606382905325139390294273637908798/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y + 34594371744009345762298243344800682513702092294749888304339407767060879552065905808261531413696106507431/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885 13019412636171469373335598244877096575103187713888768352330423896109826722182116245075783374176473213678/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^33 + 48504239109422515938198776299368691356648685576077809141449960737851790031860102725834652921687037520388/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^32 - 502545773855588110388331634546850955237412341561090000619294754604330306027908833714658766110953926593569/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^31 - 3722984977496663791898202589604490402761467708044477625524310876106577174867923436944890902508346062368763/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^30 + 1194769618471691110413378645124369675845365978545409839461650271060106230416336106716017215334632799921562/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^29 + 61464623073755639306177370741369659498636745041090231248230390098194542135993472786165582968430208866600476/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^28 - 19618338315913191025698357529243330039827906630255919902580059838961589356320727745049939901932892134060921/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^27 - 83761300097592556305322157747832722913584763288751816142732894379756247627880977534774044817192736128512676/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 + 1138937068418935403723761021219202305112441412491137366560771959799772810972880422988592080428777665867598982/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^25 + 1633804369992271599167427102596936948694969642691528567616239239881042875152585261171463169285742905831385754/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^24 - 11770241118981643345869348240800036890057296020640251635866621459262996775063349704025378369820536879047402866/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^23 - 4150858612431860076934479117056021326587751163772678667494665164293439777263339688703895209362018673243826679/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^22 + 54425774057679552789409139288869371456287997248696614796830560131526736286564825738347165334481537022938862229/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^21 + 1565779510514286527995144469993391809220297841869917416221652412456181603273537498289572326496551718848172301/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 - 27555115088525039005068943161690675413373227804310198833097124027756099738125947484334036980725379650885985374/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 - 16258099521746667863749812286921850710804310658800450717779213359331974989089365776878586892289204817744426316/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^18 + 210525117661833912114494818728598577021485615980119682967437014106074896514457102136915196094926780148393046561/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^17 + 6255164792192308180593897326069109643890401351599358483223748644558663475514813002114730780958390243480419377/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 - 41201182943501151699600949056736531948166463038506345820028276620075436607251366289295408902007777002676290781/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 - 34694251897044143145497948895165715188589409012317402557083823015796076826970938233134741273555862577671590212/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^14 + 131879128001690460987683045234615683725637262077684382570017017920263134673973363352086720355530266543323714554/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^13 + 18456032307997668965961947405272414725458554077161114795964578641257475653334767398823654818524707054249211348/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^12 - 54293441786631290068599686845761972201493515242569836046970330459347883455788657401607296187315517571183915792/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^11 - 4448975401971773420983887888135475335649521968822843930194085132719886783668214187501567380574165344655291247/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^10 + 14269048752496520764311711641251610281900572924172261959158762486313487988208657462334875806884048606111382156/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^9 + 27700492026942086863906356132675783048641296183054215634867043286003504210322840214014397941643186550611944/145969654622892461644692694909267066340761457403069052174751258121309879599637767122511366264843276995*y^8 - 106486916646922566114801022106278443670166714934713259113872037688242304449091593656865666957824132977536608/145969654622892461644692694909267066340761457403069052174751258121309879599637767122511366264843276995*y^7 - 137118613134571188947897982430597394143259409694516677394035289918657347232842334666358031935977698462905614/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^6 + 287371096889182660384441629272747797301022067946239094201496327353065238529859808834715973450987222758342797/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^5 + 24245339658657966331593889189041739092227834335041139733933025422174442682496197196560745394577477942785713/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^4 - 21142793995708227327646257456212641043241708476218731269479356935872438303658110146918496174297689076566083/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y^3 - 393494282437804186354867886879482593807728499213758662176645992737148183082438922002589635184083090480284/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 + 706201191993778444478879296627768837023477432449744440859729470294557058630215878317136372528361983160173/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885*y + 60061975156871613992329018909368939646721777832932251620191697500769769560791105749408348875593001067146/3357302056326526617827931982913142525837513520270588200019278936790127230791668643817761424091395370885 # A Gluing Matrix {{2,1,0,0,0,0,0},{2,1,-2,0,0,2,0},{0,-1,-1,0,0,2,0},{0,0,0,1,0,2,0},{0,0,0,0,1,1,0},{0,1,2,2,1,2,-2},{0,0,0,0,0,-2,2}} # B Gluing Matrix {{1,0,0,0,0,0,0},{0,2,0,0,0,0,0},{0,0,1,0,0,0,0},{0,0,0,1,0,0,0},{0,0,0,0,1,0,0},{0,0,0,0,0,1,0},{0,0,0,0,0,0,1}} # nu Gluing Vector {2, 4, 1, 1, 1, 2, 0} # f Combinatorial flattening {25, -10, 27, -17, -8, 9, 9} # f' Combinatorial flattening {-38, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 159939010368763456263728776031198067296029727062301231979755467336191262624675360634244768496621592912852/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^33 + 424544282249875519336839585806315596265428907720616597361447316682731850437791316818069046498103955726849/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^32 - 6713885964999053874328590550297952581813017218746284876887820597484541122546742917304723699394240412378377/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^31 - 38820182966447157797842403221101554578406732729821317864709994483656350713012771810295954471651747545142170/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^30 + 59689172918468840642127459632009848131272364635764315289504706976234459114222120590368030317396011282937747/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^29 + 713853395594431011290832130369910605179145018853303373386130000614213157828443984332466117537970302246294343/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^28 - 1024470471715729564033850434086369235179914838354431675075268210894046133147955932319564833946726674842277493/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^27 - 4439468575164086576915120746206780974445736105255603481178380099719313498258767157261744575187073755657950192/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^26 + 19070159210742521402354432304653794090661341664633842693192398862006163397653963420387746528622442967150244744/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^25 + 2192056175354148263384075593828007078770861932998333680768347898173874790965345221066558963976906673762953712/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^24 - 155676835108988525935409955620756511706545529078229304582754452098137762386230883157419071400152203165920713809/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^23 + 109668325674881408628224717714683617175061076940399487143193268984429404683469007528611071101146064878552227607/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^22 + 630668496548149751202229043700366141133261525196927057639749968513511496352558115476458482877436253475045150809/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^21 - 592753344427966718215796712930050228279198972749208847801833126946928333021957430187881513911157979101071327669/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^20 - 1400263799218506835058163296771692830466611438540717036744128182422980830940461316370629697343685666210297069014/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^19 + 1421145500551374155086237794559371846702086900841159060957978098984345446764428162560744189235827966940902557120/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^18 + 1872014110012653333611121426438344354506379946696184054265553624779576526891356755920665417633530219773397634112/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^17 - 1916550629986377842909349499383190827250344533876487932594776079616619558055381057104309282141947872988288679573/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^16 - 1624224999734748325990866996985497760553931184430939849682649675456196196734188862084374440269185177443073122558/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^15 + 1676797100388882235860945811959607023826240898570792848941623882257979605121324495705871426048635703914475469172/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^14 + 866700175533251235491970473534002050753444936027383710362504432510960955011103606023116456163114905099800219872/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^13 - 994928376184536080426333721722776266115872019884064776280769996016312331984701238290380958290709005432639046722/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^12 - 202178734060650048072829829133135210371810457519872463725172225349955068284461808983809633815100247540591576403/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^11 + 344898610518209350761312985871597786918693492045525507690812194181057234278844965335860781030112097260993859658/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^10 + 1426248007131292332416304752672589374607388249985581083320950630447466557758899539096407261582586636622653800/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^9 - 2730057377453837986457587058700085825149177179005255387925861899303552330314704694912763503422681472837831774/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^8 + 103049622041883493048610671758787291688669776273060998499260529899820498092293419280541285300273326052392056/29193930924578492328938538981853413268152291480613810434950251624261975919927553424502273252968655399*y^7 + 8127212825092294629112150651468105580041849457510233624182121214732134117272585776752765788219470802064443683/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^6 - 335768698932295449935479278847630585807943663912224934986903011610260391899445415459758233697970838797478851/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^5 - 724854630774061051940464594094080969278813057732424974504584273637730640648606126904424129271847283711500125/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^4 + 40136274832267662790126175079524177155416705833641723264754343042858251800284651981477218373202447991639087/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^3 + 31174435420162065977810724506867868129958992971270979004505827099107787701783803464755421722939296937929091/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y^2 - 1828390203893062502758014229625062168737943097254252075350251591701529815465916794644772271042548293656287/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177*y - 296086518171386115815455548872546665069510787790475463795660517173469985594843841717202908785526113658606/671460411265305323565586396582628505167502704054117640003855787358025446158333728763552284818279074177 # 2 Loop Invariant -68707174369317932742547146166837463088807654727046618486661585053107112826450949724457085420300965447044707616166476952521501745190684191593204644261782595595314946295530590606449749924719451548072207565725337219216300364689/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^33 - 32863366881723604877375042354501731006749704378451775208573357579902228297297783276787829997281548050363342989504302543369346546794424245438008094356787875786710669885044776932241537654839438624238170996409482546728630237221/9791634538373265259351558604140382775913384250595780548557824829071662331517620811141904190137804911900751024672655604737531526691236979680299503254905295751676998065697858348686846959387595269583614028047026331293248380296*y^32 + 1418647088190779738389314275438891908148787885734600423490464468981876134637571477470709144345530926064383088012714579472704746062768788063631575042231466591776367513315666986667401788606864479148428103312219421134198380968863/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^31 + 5757459478297068394788345795385313448064665643754897850704164286536724958832433193237429787777684864006808754093534191129447931625678330826076738136360776355805950506237505217119636599572479238367951415794235581904102945678607/19583269076746530518703117208280765551826768501191561097115649658143324663035241622283808380275609823801502049345311209475063053382473959360599006509810591503353996131395716697373693918775190539167228056094052662586496760592*y^30 - 21747602335390347851903146910185642457117011846023453700770913580999792935734332158652674391054255557154741363933328613144154450941257501755302864924293111416949882598114286941809631330912653182817610318650099914045637247832081/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^29 - 103375690069830569732813577044782754818820691641516400948342914115771027482459587821157076872951035812204941838753033277404492387807673692192766336996532477283525155227321338459479930977187383841143013296768490551093499044921287/19583269076746530518703117208280765551826768501191561097115649658143324663035241622283808380275609823801502049345311209475063053382473959360599006509810591503353996131395716697373693918775190539167228056094052662586496760592*y^28 + 186316484213752704237460497598845980428049084458500860427978439751572158563200583640026810484450769919572644828226895772354660623205921925036002213341292084900090155665884205259563065178362765020523573109451274621917797144510009/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^27 + 1966945382183034103296752908645075841374678281470595848487273502926364500360987085306436346143225016309574221293079041218268658213883056249368496954100554036611015075913884907818679595381626515291971162296536112068334906996708181/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^26 - 7757443256039312560786091473941420430220653349662699821423300891305654263271494170320562259676472842017312715082716077129426306497021945754824130469435771430563934352327210107888011823040742159415669709349373799568319264859841011/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^25 - 154790583505713148573963837446006703332145855414018603472962739575937241767550671408235339755564506948100275321818930118895300342729702918192474194191809238957548863620306852506563674944650567276847861453589117931853944023838397/3671862951889974472256834476552643540967519093973417705709184310901873374319107804178214071301676841962781634252245851776574322509213867380112313720589485906878874274636696880757567609770348226093855260517634874234968142611*y^24 + 16482365168136204744209773017981844606845839943043613341201377303261279281124221458819255443989747697092391421196102976047763193033311474782100244996572929981957809663916425963509929593123467660692265258788763728624897310110762863/14687451807559897889027337906210574163870076375893670822836737243607493497276431216712856285206707367851126537008983407106297290036855469520449254882357943627515497098546787523030270439081392904375421042070539496939872570444*y^23 - 33351031171951263263832119550976652216321457319320002518480081516477265065218482545656878993006055059128891282726453178887097891839521875101596562120235397485479440543626053772755280383461073066642248138487148861730437979087136195/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^22 - 137045653275688951325816718892716537023346728786226027777559851070516959734726655962519625965730570890134316456268054093897733283185585007012433850781880624653819927697934453991371295853490325009264714657508727990183157806150886893/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^21 + 16337492905660369334803320306767418057179012648029552205696880309281635630970132313964153663259567562780454758500091959722257969871175110933969455860275746283296537501108911052836596268454525057693090815164273770020848020021137821/4895817269186632629675779302070191387956692125297890274278912414535831165758810405570952095068902455950375512336327802368765763345618489840149751627452647875838499032848929174343423479693797634791807014023513165646624190148*y^20 + 312906103778669963970397036854785699905328260340380176277709648903659104349652084377984863991035754263069981239751559117619742412489740578100663536580149413031805937985689246052086013655505563379022247440144795828470175440303565209/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^19 - 39526307664830208250444431560421723751206599763443060373368079911710891642770723052964494506815582171203183651335522341773060456760674298958413427346883154381769729816943099605374205487714043304565707880279820891728357644379996441/4895817269186632629675779302070191387956692125297890274278912414535831165758810405570952095068902455950375512336327802368765763345618489840149751627452647875838499032848929174343423479693797634791807014023513165646624190148*y^18 - 862502195465899904091721134151161052912017924574716045985333124913844660723111928435352457790287985268806498119911788572216125139814994363611210133975883257437451843330538395622187431360447448513092378939399390749058477578690339875/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^17 + 158370028673835613468188848184126775653575266534380134688708486035080254929526654505121398885429217547048463656112661919530622748994091011919465888247574982565852229392690712266703712764357801661071316586817395109789529067082666567/14687451807559897889027337906210574163870076375893670822836737243607493497276431216712856285206707367851126537008983407106297290036855469520449254882357943627515497098546787523030270439081392904375421042070539496939872570444*y^16 + 96219497091877733259488325340187522417387886460344245891224052539180030840613212518393577200127077308985710099591908430329031972317788235966520463893656273549749759518110672864281124275194981706133792162291948693117665184989756019/7343725903779948944513668953105287081935038187946835411418368621803746748638215608356428142603353683925563268504491703553148645018427734760224627441178971813757748549273393761515135219540696452187710521035269748469936285222*y^15 - 275594285322229462615425686648497292538768855466407426927403621219974310798655537173047636173527846370278045758027267807950962640387725486929930203945707215834226072046473635747188539839575753388103613486678945242264191538565144927/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^14 - 215310319952995394064764026236548640940112201374279540663706581032525370252767796927528297398192031349518784078767709358928776972942715083491078447257232786260549060945703508312997324632674314317666234158802370222696165707922677881/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^13 + 333052725825465774789734627914501997152817742909755961629793524594165781348496739969084256689708062993798510678501314652012376900290610370972732150284474979976220525908327191794749106408110740149738036366043432509174350198767868771/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^12 + 20364751872726152630666165772383788482188102255650630983743425046595037299359455724493400450594204828367371550842064492188752482719137026342235580129392126892293384647065011096339406486761188886384853056584225399833143034303851919/9791634538373265259351558604140382775913384250595780548557824829071662331517620811141904190137804911900751024672655604737531526691236979680299503254905295751676998065697858348686846959387595269583614028047026331293248380296*y^11 - 39926042885800305702515805264373809606916087000744646751600192906688803125335030247404423337179873659863844749785555675190394757148896342200193882383959849763717958394301352011914236600935877867682100790289034731772288359943560931/19583269076746530518703117208280765551826768501191561097115649658143324663035241622283808380275609823801502049345311209475063053382473959360599006509810591503353996131395716697373693918775190539167228056094052662586496760592*y^10 - 4371780161624371376324741438758292831606235513981901540886002929327289613250932779056940747198392047693099695196577625185197856440418057929649092807536181037554965776961515389276291785925229344705507977224582298628083849313784295/19583269076746530518703117208280765551826768501191561097115649658143324663035241622283808380275609823801502049345311209475063053382473959360599006509810591503353996131395716697373693918775190539167228056094052662586496760592*y^9 + 492529488814486168799670958649060793659237949199466381999153966324050352947260933433088592736564297150320541191644984352657675379968417046818943591591999255440747267357811894561093470344401149260671067709076542381549128583765571/1277169722396512859915420687496571666423484902251623549811890195096303782371863584061987503061452814595750133652955078878808460003204823436560804772378951619783956269438851088959153951224468948206558351484394738864336745256*y^8 + 43198324286524079062743006084207555630052472641380576359595531031355154943669344723851828842667427111641508414674561728598828439002418507262379482062384448469886538151449710506779764352701681564292164908300901153679693688562689/2554339444793025719830841374993143332846969804503247099623780390192607564743727168123975006122905629191500267305910157757616920006409646873121609544757903239567912538877702177918307902448937896413116702968789477728673490512*y^7 - 2907795808701984244545601336177078848968774604676299020490090757375730119607122630826223947186567080915351974090151517188074201449538319910216615896447465934658351235960910374322476651980157627506399236797957613497071959749179431/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^6 - 38930407594656709847903033036090007813508767006288228494792494970196400557717077864070368648359672987783898308502096236871774994835950900641744895744498772145694910184664705281537647938558954651598720772953405550197872429349147/29374903615119795778054675812421148327740152751787341645673474487214986994552862433425712570413414735702253074017966814212594580073710939040898509764715887255030994197093575046060540878162785808750842084141078993879745140888*y^5 + 260728512298719868744202973955292003284197589934632529166447944391180744251876239467811129391604829999783822436084342027695458443923556246217790334103236951467264678030552877160247679458717966240820310681131291592239895637790791/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776*y^4 - 586799425093353766897446878350488486778843817426436972691008699936827677967514487772396723959613446262840913241206110467958733256109568842103568997964097038488429702571075890209979431380312049986853772547661439314775750427299/14687451807559897889027337906210574163870076375893670822836737243607493497276431216712856285206707367851126537008983407106297290036855469520449254882357943627515497098546787523030270439081392904375421042070539496939872570444*y^3 - 3867879610008230554749209467330137167893371345630624028166509913312877261020433809896761552513284289519629889597835522336201759221406574242147867828760294203060042893326124478804108506786094544335538684861342915186997333767311/19583269076746530518703117208280765551826768501191561097115649658143324663035241622283808380275609823801502049345311209475063053382473959360599006509810591503353996131395716697373693918775190539167228056094052662586496760592*y^2 + 69734122049453381986814409502540357267259152878631625765204740826678723385154355465200058132584354144144794525514734546111749083920742337668627609525600719502953207721899348135046874591997421140464705727333912814838373091881/9791634538373265259351558604140382775913384250595780548557824829071662331517620811141904190137804911900751024672655604737531526691236979680299503254905295751676998065697858348686846959387595269583614028047026331293248380296*y + 7420382681134475036108421073791342079833898779108343000144147625238735765776291646625316576074018487381013343065429645937790960282838459457218023485722842979342305852652891780938314762135289218924127116633620176217179820298991/58749807230239591556109351624842296655480305503574683291346948974429973989105724866851425140826829471404506148035933628425189160147421878081797019529431774510061988394187150092121081756325571617501684168282157987759490281776 # 3 Loop Invariant -1376350313579365335787053833208164438574748347195706741733021924367693216752528970907691492368070978741563404507525145574032114337545173675296327360781284036984785793070218691980179901665919672082134416059282904462472678714134582592187220653249368526182944514262046398689429193356435/6609941229804547940181118252418147812012462760466408958086500447574553759389090507348462423437411297336885768557980859282411945290245377290968488824019384956316520491050944167843680437381203538535227375865978354600130646457545984453046338075296007344481667288786578879703741883011932*y^33 - 3370405134739524818900534046738176335863235122002416712115401102705223197368587801977140702834441805854433065564417022390030108135031591232087982597005652013503280193355638198987849797132791319989429976140448020300123676256043850290643352502192148350564798876616901678859775876655439/6609941229804547940181118252418147812012462760466408958086500447574553759389090507348462423437411297336885768557980859282411945290245377290968488824019384956316520491050944167843680437381203538535227375865978354600130646457545984453046338075296007344481667288786578879703741883011932*y^32 + 937373852622949437028543681254590211550214948512530658051565764586631437269521218843246932866363805209314130339051884904434178918023756623225631234463858827716227769095368286027552405003160460051226611526401989932769145844454083854379096223014700746770147292975952029772108029507022083/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^31 + 5157337779220958835080399949287894209888491334884914005034836476491552904329705737025729169129119332733534653386762909070675955540242046694759680055666960369124658986108159396021645306745068285866759387531151081606341854771566936856268360926605567596453817787088166827533546477893567631/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^30 - 2339299837668928316073710053244745984129109318386136283420702503890762323773436965255699347956445070778527666988494471811158727491846847647008214665021871043383955033180616903121147624632228522692032191409913065422316800747837374991673578244767088651856242787141302167503093761139522531/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^29 - 96821035628466592463076792687952369216935501992865946978235562716121149684418048587387450579423245806901739979872477730290129697291419801878249476239367548974308479458572422274547128394449142680089362582323184633720508567958083230665084228005221256106854731891109013786444203173566206961/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^28 + 161649831734703236369413760366379642122555154521130903871111256909451625332987535282960448640172590447890008683424306022603516268801682117101528785936889179159465990660926281932007602753960484257780415832749230698293968633956298170465590567897722690195209749481483325568647114360385553997/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^27 + 293204114501581013557831235961491238265316450703445042501576779658973304160653713344495694559862994855214111721665109498129021339232788653195921323689459639427065434125421813643912583501148446581977136810345904512035835889298487703993191680596088665399344292403410192485136072156733513417/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^26 - 2757984959220488853845054851904714639740681865414071559224403086107926961148171255346482439192851447616332814827077995803393677931798220351649579344890240773269005005132696802029496293041993209542481065521352440586780876251790405738149265239888063736464860818417333395388602992545414534987/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^25 + 53140780521899790999856961571420481207981286744089599818628261900902680538538443113288626193727114678808282652491128042171996199697293389758362313955174230059353498421111857393794525852579838393846352535342499940726667649742064725681513815612993696709901656597296164126460539259064727869/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^24 + 21612139493018044353003990730066639954040278590427992389171280459886907050573213720147429674777785987222652861824703718329213554488306690658466224598706547655482197979088981988753397710793451224745593348801549921150981450962421793600835749285277015038389280031638254410459045204539819586545/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^23 - 19507476335800084318125966798644198196325648590137971575643296809643913325400390016999037228073949660619765238676043124590752679925024151088151940516379974686133364570352488191068089051365291838855829799612332442747351017145085092007076004865750690252783739346095004871072221747703531399251/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^22 - 42324913114291388458540844250726136561085754430499446991758349668728868598634782299395323437677048746451519250486710809173602610690652597502233784004925463343864096835347029770374735395379525836987558516958265632549162987177020618542454082751439545241181149673173995433013455298588835124941/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^21 + 25056880218198857803402545909343084974696582108108275165937920131959827245784966000900416480707742217365073700822606754864828176036761733797467251864645907940615901164139347602697016244089458786910343338478247455219577443376418762399974429114831931956043841433466080366205338980833143520023/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^20 + 179686048928956431102951642571762565286002217391962764002613695330290238251642248166313417807250449054913415789582684305120932878860015535087166140018805147625108863492045904566915043652643196924754604587549121492275506230270406517305641372056740902370743338586466253807671594526645383644381/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^19 - 119634709878195689933402078719985469795256160873493544017524253535212195793811217806780095235415700392749873467484995836965792041422382934170962173849755072889051845851670069539653822595724349829523800624284731209434451032589397766867294657312021029513780800111825222935148653708209148450217/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^18 - 112768581017940775631422085360228793165153166840839237851571441842327560184391685043101457131959268312275725387856271198112309119007297742042441661360293253332624512696062728236783967870307529583161711902321019473872586287276590927261104308658782149899927499520914910606071018342234365187395/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^17 + 81569885427000562341734122926936714813861223030121232647368019356200213123563456862223507989673189524120492237609929286995618274798798071084747654774275100763490477196505798085958421372381814732893612436685294871905928921322526114780136815553635254851797431565059103763961647070044573641375/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^16 + 44985099149981050912118758109154983762259734419815840554997344357581070664519779753947578073343595542089017068926754434050559983519959788654248795946982292671909999320039355171491522111431910368658389190570112763583846229651384866225514881335641676249656087064384275142808599933793745149049/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^15 - 72370571299108568336015361269565827122064401434015705063528931449061006354422045172290612606081688834341715914168466999152909054130138829157679417750296479944466511762538644841557991432094712736407774225601924381040070023393179425205840046595506927737525111668986531803747423939808943466607/26439764919218191760724473009672591248049851041865635832346001790298215037556362029393849693749645189347543074231923437129647781160981509163873955296077539825266081964203776671374721749524814154140909503463913418400522585830183937812185352301184029377926669155146315518814967532047728*y^14 - 80960019333404766918805295940525008356032600616354461534086767801776047295776938976479316582743704402005980842380835552246153472774583914392310463232079372007785357411349186387852961151598360097205753844782159823737957938833011737252247241415246712881844193027829517203139600839752224213147/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^13 + 86236693090472180067343015177866884650191322009741259482416989101817198650637770869280324374679591530103348938899660022823184537227303260412654569459318052253616939417729203240764155694078376410698879633338951217852545115117766267804305408751094727369188449899076093370498517979709429915643/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^12 + 4481421068225662675936794699218073020679575011431982221188078154234499852121680365185592165370321749115731331798945260591726145366289805594807842564564490513932158276418622317952008003093565753021595344228575387825005020514094138705801359932779344007077252320396588893983896178052137590249/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^11 - 59556623950007875513533240312604273868287126455105213987446676342545364811381254229595111848130522730799757588738575005327033223235502935275272459060728732344008193491451974136483805676193939514370843195072385524313593637040070884831015377304802601965895355901677106689927260664526150768563/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^10 + 4254584501529983018932340123970163414619068085162945488272683176089773481635145168977826459024906928891037119776532817162664726923556514753813303906134600765567388596075308268625931533280756589653077642015479456494287150016883794578380507489014142113167253246423176174086593970303762525329/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^9 + 469108778170962115613651610187491429539062003883757303754015898189304545176627288199156215701303841622503474092010415216977449869509591455897093862006416468781507286874902974534160221938724665107531262181628561477579988778221937099976548070959593371285674944387348743168998300732609375225/4598219985950989871430343132116972390965191485541849709973217702660559136966323831198930381521677424234355317257725815152982222810605479854586774834100441708741927298122395942847777695569532896372332087558941464069656101883510250054293104748032005109204638113938489655446081309921344*y^8 - 45831728487131838668085904009863445638622152720007704066452611979170689706916625936234624804097106453345800233893338017970383072686205336286780961845404223756318810964310950992296450777411119690870933062083607020672525430056262747510320297195096231435714939979044817831350123885934176723/2299109992975494935715171566058486195482595742770924854986608851330279568483161915599465190760838712117177658628862907576491111405302739927293387417050220854370963649061197971423888847784766448186166043779470732034828050941755125027146552374016002554602319056969244827723040654960672*y^7 - 706513016911080570657383988972774073429846890744820020720493003811272242360941133152202337394428493862927686314709754645027051165568443818882626488664785052308952848659768787035638016955524339563295275508235287517016955300397304503770953091154350644093243490450967679113913848928731861747/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^6 + 278296939068320867316808997410698465738793620658595914536090007626377921106925751232962164118218063828605884332224711757569233895521576745005180846833149359503343739468062986710664912586125462524781177887774664334810719978385822669688730934633796625655397456248484977559461392681905971657/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^5 + 137660717720884594835120069109447919566320163729570562791227596321909914024099822490102083883134534220604539006477041723236268222732124534048835211561574036065148192652862176233872928423045145491399391797419084151256983514103876786185144576763196435755390079821474752090935259976225139325/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^4 - 25863949292850379388801132464773478720344990868596139207561469633063514595865717323003202831100173929354024279746159833046639356116019158440283977146988859648940142954114999886040270545956596436151774204544941620611378096911674678313370894769888485566608118689064053972420120929239142797/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y^3 - 3504540567186512721959913861776650482891714825683948933670902840370751736280062522779116675863479096638188243876758307309572971414993440190732498958261896969539531721637384932474582342403638066045253125076823977140002518576189874865778696957740769058701484514131318199947380904008580829/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456*y^2 + 1066300842214393058592422734295465049649427069075454593094293185756054746353727005236939465335107725091425488538661897519553219297102406643126473595636930429780650289900374568880299990554747846330276900245558553156241804721009367852350131947336192849648556680443673421860828138487053709/105759059676872767042897892038690364992199404167462543329384007161192860150225448117575398774998580757390172296927693748518591124643926036655495821184310159301064327856815106685498886998099256616563638013855653673602090343320735751248741409204736117511706676620585262075259870128190912*y + 59309705060023784508566647700349185912325779704993059533579326226929383081876489572539892262833880691879134199093232211692758879969386354679202697414479093996755308439228927331873594005697099699982785555713239872189386422070329251267753385002930241451693546809427946038121626610188129/52879529838436383521448946019345182496099702083731271664692003580596430075112724058787699387499290378695086148463846874259295562321963018327747910592155079650532163928407553342749443499049628308281819006927826836801045171660367875624370704602368058755853338310292631037629935064095456