# Manifold: Census Knot K8_172 # Number of Tetrahedra: 8 # Number Field x^34 + 2*x^33 - 60*x^32 - 137*x^31 + 1276*x^30 + 3471*x^29 - 13112*x^28 - 46542*x^27 + 73868*x^26 + 355214*x^25 - 94270*x^24 - 1951015*x^23 - 1183039*x^22 + 8816255*x^21 + 6055331*x^20 - 33262971*x^19 - 11138640*x^18 + 90571815*x^17 + 33065*x^16 - 161377802*x^15 + 35968405*x^14 + 176186242*x^13 - 64976223*x^12 - 110193945*x^11 + 51690281*x^10 + 39926191*x^9 - 20327013*x^8 - 11369014*x^7 + 6428356*x^6 + 1666736*x^5 - 1294176*x^4 + 40384*x^3 + 73728*x^2 - 10624*x + 256 # Approximate Field Generator 1.27209598908661 + 0.432749926778785*I # Shape Parameters 15348483146226013568705735275171146957612832223491891086074935365005491300509369359096223636090931711756898483871033173410256310231347/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^33 + 77758477588532960300364713203171180561627108825613904083020334136626068407707226180075122279639581908175511529487812770093765267594601/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^32 - 900513155635312418884046836053313170046075704666711769943183321847444116127561600887596265607067388819578353255772684710957982098842669/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^31 - 2583611670813778236548329498761776992919771800923486856231090307611499651493790092237154022876152767323120340235198554225534570528829327/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^30 + 36453674354958857087926096365284920676022578838771285488985165012237379462282980639582363764725830711725941858342752174103671155872607211/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^29 + 63045170706938397294333238426779407495406864508481367519936324950796737292041727032322329988884218329670256693286457210787697641330728073/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^28 - 336077499195308664435325513898059345390101657631317304373050917274863244034534374329151129134490839089155503127814884420944832641224734761/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^27 - 20131362682012284600099185981243725344190401964635191537624889262710308549879789613157954816402861063920385280672376797063717806377362569/63654475078758189503912834905454291652755073915097471435889244246725768908620798117020080839440030217495295166265613186750408701446020*y^26 + 708245494706225560324759074994788717937318646019759498079469984914564901478931498921512789642876747825527265591658103846338457708301255651/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^25 + 292331909809122333181422336860611606911815801604196570367315177343147816621644364890581033950236984512422238407932303496191662258920138463/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^24 + 330583957325632296554639914646780341329196454614334943432209642780557942947299559689076380660553942195152337107641383126329359885402566841/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^23 - 1459466534547813506473957967786371209487713214803312380198317784068038406168183683486314751692801529490896303937637148260754832039227656221/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^22 - 67484463842186408622808535784980228025792278816036094470330159144156807103727554595638591962586250272793275927467531106100525766193478157621/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^21 + 235932638969699965421729059741798465248551910510143082448031270444205837988794903887505327149384949767167933230919167557493998035288653965603/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^20 + 62600296758687834939800511051046119736940527416205957050577959913711464625989516856682744560623987707125667751552458224543655996879064907649/1018471601260131032062605358487268666444081182641559542974227907947612302537932769872321293431040483479924722660249810988006539223136320*y^19 - 859483354769698238980690763611621271827699494103212779436081404369246571559562395031198416100265907174752689988364280278447194012422895637059/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^18 - 806475048200805907798216779567595110277705011621688665188066409600525309995865561992116672581912303663322905547925029725505007806266617683103/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^17 + 1184836824182917364367681158627972967554519617814730173799905042323560508432721952913524567370705179533988205744613607221564223831420472264177/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^16 + 1280343831328980106014750604807039682572937193870586092017498964039650291114699512661859339501060901660207820212815295736677603880286122861693/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^15 - 4324542230388031601292249841031334502694471579214693672062354246336825016996297717088044253919479254476715723060740247938974216932386140900827/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^14 - 306323476968968922178836568569625461456009005758274691841524959855636515683751091896732389943043133328284768215254859252115749437157209843671/1273089501575163790078256698109085833055101478301949428717784884934515378172415962340401616788800604349905903325312263735008174028920400*y^13 + 88229521404475401311181059618522035370288865664253501718630891994941328113564396585665397366453122860053488122922059637049225718694421153831/92588327387284639278418668953388060585825562058323594815838900722510209321630251806574663039185498498174974787295437362546049020285120*y^12 + 153106399426366956432803056315175905466601893861605187262659881971300811177186472490762437897786565719643368995535820152556200586564722401287/1273089501575163790078256698109085833055101478301949428717784884934515378172415962340401616788800604349905903325312263735008174028920400*y^11 - 3166264014182704227226151215512326279020929899214141061974150294316838391492194923831229816684013690323950300886506072073125811228849954630709/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^10 - 107779718269356484387576242023206666687128079914712059004221658961429533692801936265512477100227520943887073830434008143430640288250312204979/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^9 + 1240956928312829915063712886074749579786522764869955620062809750214168387696745869087263040561700852127018849972168567506233672603377286430871/5092358006300655160313026792436343332220405913207797714871139539738061512689663849361606467155202417399623613301249054940032696115681600*y^8 + 7215301743074039597825495340723916792724102588824995237173859980037767091131949286164234936529510434082817573323522298465060578774921168329/1018471601260131032062605358487268666444081182641559542974227907947612302537932769872321293431040483479924722660249810988006539223136320*y^7 - 32604862842196239652283357817517137840600270361391102313359803292995794829443317266244859267994712660629621331016281601567435422450172556791/462941636936423196392093344766940302929127810291617974079194503612551046608151259032873315195927492490874873936477186812730245101425600*y^6 + 3349571439080470453763661252923669728452908110144077243030472021911708163232329133861699077237079045940699857707133998212996350871429981381/2546179003150327580156513396218171666110202956603898857435569769869030756344831924680803233577601208699811806650624527470016348057840800*y^5 + 1973905899567039711091719406358005306613881148893554235501672970895674010944106527217798026662974233113221826812474578501389141439673961919/159136187696895473759782087263635729131887684787743678589723110616814422271551995292550202098600075543738237915664032966876021753615050*y^4 - 74239598964786283267508409490568041449590717697704477335556251062990971313687372611332010191598892259691923738803932806417809011170028481/57867704617052899549011668095867537866140976286452246759899312951568880826018907379109164399490936561359359242059648351591280637678200*y^3 - 11696776170026600220049050147665747419734683127192348599406258529223999575899816651179336470744941100504470629238684844589349983099154203/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y^2 + 14306338158754145578818152770174764856749672827480530399891485664223531078827627428582406732335627886310720290483119201217773130600802741/159136187696895473759782087263635729131887684787743678589723110616814422271551995292550202098600075543738237915664032966876021753615050*y + 270622181577563239699539914659080004670754723691486179552552385927717869336350754832235792044190061157212504846843030149422999207415162/79568093848447736879891043631817864565943842393871839294861555308407211135775997646275101049300037771869118957832016483438010876807525 2829269957386246695955681475456555001916971704436783436052969132775895260917309363420785406026302689722881702429103976858319627950989/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^33 + 6796950193146768963159350885618561051520568764841879317441407566080752466419826698644977470691683402067992600517545448446489283922123/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^32 - 83512751485337749008875034377605591095614025086021221572438735637581059369302561325544557509601090049937041133220400241835412068391351/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^31 - 454834730650590719591703389349589110036946196537907444310740879581696972263246832865013613606113796651232614922342843951100149114923957/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^30 + 3427358216120605322829606215701755205422312446122973839630098808570750034359316861673397543084150018370599940350018377170684923921642331/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^29 + 11200636578040009913879342795158533211441795069783524612939360046532409478876701132631085748157942755594754495392675471301311294162108339/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^28 - 32593976525118167100408088822073593455843738279516153845244947940350842790239330992017528269806136752313259411225361582975165413113147469/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^27 - 72410470517744162408493063728128781322869310544631254403179240902420482709681368919064906257600147316790994461298843871152244971435080133/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^26 + 75364590141060073699519778770994024537036596125051403970729379045884017363705152619161368539808419773352770972925917045868395944896713909/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^25 + 532968708151773611670617240866131016120490620200717214881192943120056393797571697078736945360872241086755828832582185857086501419113237445/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^24 + 2538322554745256810684946771871036963184500615438924898052869877514538706747223180802767719023442412341772798787742388392469539255183600/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y^23 - 5456344893237461655321837575874911681256172909654048276823349937990179929126388479856865209915504400765360070346577434097770850413241999553/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^22 - 2773108614222009117054404691042637341338061677002612514122519905809703086267709035681586358985901851830400470588091231965111576803785226333/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^21 + 2839696731892757354472085370745802829485052708581204630762418718559160898504251769315139884917114944995134258277726008359035973590136756589/25461790031503275801565133962181716661102029566038988574355697698690307563448319246808032335776012086998118066506245274700163480578408*y^20 + 13148259840107600829520882379265598228256444116151477950654614212998235304167807548353107201486040728616191561230633189771445659818945904683/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^19 - 20884216781645703409709389421380097418668272658948737164613673364987844500604522848780143554110576952811845902757469668570146891824667393053/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^18 - 65220459071463062962327696691180021992089914877663273252453088293810710085266417015752324486650895938981967666439406228458328098784048175803/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^17 + 230022326418148248088025815977000391943366238205663668593344046804170881399981769937152264666309599483739000379253219601156491867586042251443/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^16 + 5808436624817755971002830179025649147455647971998451666883687542266010436588081383255143839317006302637742804126755143188799344100335684703/12730895015751637900782566981090858330551014783019494287177848849345153781724159623404016167888006043499059033253122637350081740289204*y^15 - 419225111212263485296245656535316187420000552979386604848329225728433269318703904648054032376453798272375470483788513043140803521254862383317/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^14 - 67576764126021476891833223713165619636479544441646223188695714645330210490676263671363310619701931569428265832829736532333617530617445275713/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^13 + 471342027766153706541108703098037670135347932797950419860860215737566353897503803528816702964671511943877683306886807722314226186673733646235/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^12 + 6837478038665174792417087195292590362426188877676588290330320155053268477746057432891792162264376546570700010841037968933989067209107107587/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^11 - 38625047207431712475813351484011919950715029496138297789689446046870730079277688028285542972008236408264750149858953029889389439863727736589/25461790031503275801565133962181716661102029566038988574355697698690307563448319246808032335776012086998118066506245274700163480578408*y^10 + 654596440983315083156853870870182216501231736642044992077850944567019044312447688060190479263779562393746535473737259917144106022618600061/6365447507875818950391283490545429165275507391509747143588924424672576890862079811702008083944003021749529516626561318675040870144602*y^9 + 30320995643370929684593636670221373076381964356777710561820182754201714252441291067519314196940577571906784597241510174515401496322152410313/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^8 - 4098071138310918971948661348486749449379786470112255248232806927569790333676865217914786637084650939764955798740307131113084292425490161677/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^7 - 35387897404991718429728479820856304781552828087777371853199562434567911554057051824989311209920360465439083080172012370114044340267147239643/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^6 + 171652735541324830162926762388425278652411281063044295133132097930841583481441373668508366236749552604534385992939161581034329966765691501/9258832738728463927841866895338806058582556205832359481583890072251020932163025180657466303918549849817497478729543736254604902028512*y^5 + 775217048903077430274308605948214703568160087271599687037471437143420575114303143040011753115822593408334333561416487105398770771870221713/25461790031503275801565133962181716661102029566038988574355697698690307563448319246808032335776012086998118066506245274700163480578408*y^4 - 12804056168240823212980683363289614653746410171640901984487118612757467494969791625277890886891139010649856489239480121041942225972744843/2314708184682115981960466723834701514645639051458089870395972518062755233040756295164366575979637462454374369682385934063651225507128*y^3 - 20740024469749914275646167501800751664064598060993521876760634157761526665732449179409299218106550659724786312531325520052684419883786333/12730895015751637900782566981090858330551014783019494287177848849345153781724159623404016167888006043499059033253122637350081740289204*y^2 + 1097040227794546853623607567720108812825520678021938847418951101667411607603504684960881680358783104757738777536108819449905510914132630/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y - 29511582435069673038456659860274673685968140072489397669892847237074885021856697418041583815966206749488170593641167784758118845686383/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301 985904492910831797356857329159805087350675302246633815291586400072094862108701657075454952244459005714251849315594848101334496899003/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^33 + 1127418378895086319491769796413371824534919121681579723041966787413015659585713974685214616468886179869593347683436666333188954676731/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^32 - 664644554949835695160838331994369115604924768974606199100673181818847922576173677783870349668713534816708556439632853018697008352517/5786770461705289954901166809586753786614097628645224675989931295156888082601890737910916439949093656135935924205964835159128063767820*y^31 - 151811184807711619234426994107968438680147548596189483593530573795711093585683346246873032420093950465189065013007661333156142192574803/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^30 + 27576531361944501417650260076008205275410089084241067490742965847249195895652322251400210654628431046560584283625724896570829013769823/11573540923410579909802333619173507573228195257290449351979862590313776165203781475821832879898187312271871848411929670318256127535640*y^29 + 3767204209841209199600485563449695894844615706446013469407139603997319895118080639678604155749518478768685238960805752481983933278119257/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^28 - 369511348782392444177894681626073234269408050541613078890541762316880703606239708424003506582708440801505073040739856128927429749255211/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y^27 - 4920288799207206983690446980675840126704145426497086514893707483813139392366808893752872934257314010026226473638883058483130713836475839/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^26 + 14627498974828296976516132174282044848848366803720712016746868539577675463115663762240254760822075255173737679254392846790132422859492471/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^25 + 36602107461337470564200255999015254295675391333331386582579551596572834090813091307912931831611071116686985492954636998982125640588144565/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^24 + 117035478621606850112305245904719681905139810202130326997780001985376112948157696922603220799717998907630836312659108477630130512796525/4629416369364231963920933447669403029291278102916179740791945036125510466081512590328733151959274924908748739364771868127302451014256*y^23 - 382547935956931924773337898321777154741819476467335792497960996226802110220336984795586185878848348650787527035008344063932676287521158385/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^22 - 1712743780566089235249750866749158849865797795062867103574159646933357676874346134584263702073674945359980478750726409182742307651290380957/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^21 + 8165590828867614139363404170144863075833645028244144049721650375246782786193272635196176434895327189132707648852367953323457946310733907761/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^20 + 1654011812290502626466776827645218184711590273113212437838269949047669762594182257147785942991790073235545971743467801877812912202641608145/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^19 - 30283078318743831953907337047393955790002829992590243400860397482057979568015276151069203277051981318026256005340969196628072952952385222093/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^18 - 4868027226046757826420236466069650219585661022473014246271903241676564094780797413031400512612057044641727815248362841187570485590130116409/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^17 + 83209761202770758089073540254612973721394104133365405994214420829381916027103420007820628368057947405126837565235848120713973815177654209793/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^16 + 23377634064302599611874479680413559659398716243113730559752124200978369469584955624706912307380372155164373947440311452125227543780766219931/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^15 - 75507741743229454057924791593818920642547241309970008120248380299628342091093688476688251821948525524703297593339496791441960349816468307157/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^14 - 6960937255222169559786069059898042732448145951012501454342375742780467618808215201626631761245714325115661738335234615111875347576497668853/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^13 + 16915820742246538222863929815789383351416085841469506075704244410144765287125388643835566647375300359663946499306121515695834647502402539303/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^12 - 16520831313479193256586884373571781248267264456479753003282760103118816539470935655669851251058065949756389984221141268615119397612324178729/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^11 - 110470197468457771647572598145750545655392910981544376096048622141247239564496190026932566997236073149443761778130884738727367346000992575043/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^10 + 19914452712341166674549998032421842572738285430181227923756785489121702832396281298916269293640719968851366122299627889483711989465187231007/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^9 + 43117316922011957292978956629529356227176430189266587494273451923046667230422750457524795136063484013418386299259381113428346441080452710177/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^8 - 1579137164351001095329220381819723673263050801500663074847977742807586589794687026109974808193466748865483264857750341738164638291912398903/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^7 - 6333275374757170018204551782612079897893598017383489672541361466634417904047784031715549763272252941806474669690020906223184542619802979011/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^6 + 346991092471507811490700885415371007484700088246854674703233426321813215334435256325685628045443471321473868002986546358607009487725241043/63654475078758189503912834905454291652755073915097471435889244246725768908620798117020080839440030217495295166265613186750408701446020*y^5 + 68707264105738977660924918609077428126040892263489704172136625113469135916755129066027788327980638804193291777963854846916216234465711888/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y^4 - 1862648818119298101923459258746750949987818191171326628335122339641315880370949409421668902790699520747867082335831814259346373446350848/1446692615426322488725291702396688446653524407161306168997482823789222020650472684477729109987273414033983981051491208789782015941955*y^3 - 636204850059877722577750316936322046921764208239221930190579190720396827571436426900567865644186645588889820888792739170278004771731957/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y^2 + 1266364419039850033978221507852071055544243805888412524619905030998089312734681407045617878641369678177605740132712476734168340004647452/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y - 69655747855525173855408362222938880579481811692241576590619320524221427305095827205628152081708291676064292089371816814012469477772242/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505 985904492910831797356857329159805087350675302246633815291586400072094862108701657075454952244459005714251849315594848101334496899003/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^33 + 1127418378895086319491769796413371824534919121681579723041966787413015659585713974685214616468886179869593347683436666333188954676731/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^32 - 664644554949835695160838331994369115604924768974606199100673181818847922576173677783870349668713534816708556439632853018697008352517/5786770461705289954901166809586753786614097628645224675989931295156888082601890737910916439949093656135935924205964835159128063767820*y^31 - 151811184807711619234426994107968438680147548596189483593530573795711093585683346246873032420093950465189065013007661333156142192574803/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^30 + 27576531361944501417650260076008205275410089084241067490742965847249195895652322251400210654628431046560584283625724896570829013769823/11573540923410579909802333619173507573228195257290449351979862590313776165203781475821832879898187312271871848411929670318256127535640*y^29 + 3767204209841209199600485563449695894844615706446013469407139603997319895118080639678604155749518478768685238960805752481983933278119257/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^28 - 369511348782392444177894681626073234269408050541613078890541762316880703606239708424003506582708440801505073040739856128927429749255211/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y^27 - 4920288799207206983690446980675840126704145426497086514893707483813139392366808893752872934257314010026226473638883058483130713836475839/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^26 + 14627498974828296976516132174282044848848366803720712016746868539577675463115663762240254760822075255173737679254392846790132422859492471/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^25 + 36602107461337470564200255999015254295675391333331386582579551596572834090813091307912931831611071116686985492954636998982125640588144565/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^24 + 117035478621606850112305245904719681905139810202130326997780001985376112948157696922603220799717998907630836312659108477630130512796525/4629416369364231963920933447669403029291278102916179740791945036125510466081512590328733151959274924908748739364771868127302451014256*y^23 - 382547935956931924773337898321777154741819476467335792497960996226802110220336984795586185878848348650787527035008344063932676287521158385/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^22 - 1712743780566089235249750866749158849865797795062867103574159646933357676874346134584263702073674945359980478750726409182742307651290380957/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^21 + 8165590828867614139363404170144863075833645028244144049721650375246782786193272635196176434895327189132707648852367953323457946310733907761/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^20 + 1654011812290502626466776827645218184711590273113212437838269949047669762594182257147785942991790073235545971743467801877812912202641608145/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^19 - 30283078318743831953907337047393955790002829992590243400860397482057979568015276151069203277051981318026256005340969196628072952952385222093/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^18 - 4868027226046757826420236466069650219585661022473014246271903241676564094780797413031400512612057044641727815248362841187570485590130116409/127308950157516379007825669810908583305510147830194942871778488493451537817241596234040161678880060434990590332531226373500817402892040*y^17 + 83209761202770758089073540254612973721394104133365405994214420829381916027103420007820628368057947405126837565235848120713973815177654209793/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^16 + 23377634064302599611874479680413559659398716243113730559752124200978369469584955624706912307380372155164373947440311452125227543780766219931/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^15 - 75507741743229454057924791593818920642547241309970008120248380299628342091093688476688251821948525524703297593339496791441960349816468307157/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^14 - 6960937255222169559786069059898042732448145951012501454342375742780467618808215201626631761245714325115661738335234615111875347576497668853/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^13 + 16915820742246538222863929815789383351416085841469506075704244410144765287125388643835566647375300359663946499306121515695834647502402539303/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^12 - 16520831313479193256586884373571781248267264456479753003282760103118816539470935655669851251058065949756389984221141268615119397612324178729/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^11 - 110470197468457771647572598145750545655392910981544376096048622141247239564496190026932566997236073149443761778130884738727367346000992575043/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^10 + 19914452712341166674549998032421842572738285430181227923756785489121702832396281298916269293640719968851366122299627889483711989465187231007/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^9 + 43117316922011957292978956629529356227176430189266587494273451923046667230422750457524795136063484013418386299259381113428346441080452710177/509235800630065516031302679243634333222040591320779771487113953973806151268966384936160646715520241739962361330124905494003269611568160*y^8 - 1579137164351001095329220381819723673263050801500663074847977742807586589794687026109974808193466748865483264857750341738164638291912398903/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^7 - 6333275374757170018204551782612079897893598017383489672541361466634417904047784031715549763272252941806474669690020906223184542619802979011/254617900315032758015651339621817166611020295660389885743556976986903075634483192468080323357760120869981180665062452747001634805784080*y^6 + 346991092471507811490700885415371007484700088246854674703233426321813215334435256325685628045443471321473868002986546358607009487725241043/63654475078758189503912834905454291652755073915097471435889244246725768908620798117020080839440030217495295166265613186750408701446020*y^5 + 68707264105738977660924918609077428126040892263489704172136625113469135916755129066027788327980638804193291777963854846916216234465711888/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y^4 - 1862648818119298101923459258746750949987818191171326628335122339641315880370949409421668902790699520747867082335831814259346373446350848/1446692615426322488725291702396688446653524407161306168997482823789222020650472684477729109987273414033983981051491208789782015941955*y^3 - 636204850059877722577750316936322046921764208239221930190579190720396827571436426900567865644186645588889820888792739170278004771731957/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y^2 + 1266364419039850033978221507852071055544243805888412524619905030998089312734681407045617878641369678177605740132712476734168340004647452/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505*y - 69655747855525173855408362222938880579481811692241576590619320524221427305095827205628152081708291676064292089371816814012469477772242/15913618769689547375978208726363572913188768478774367858972311061681442227155199529255020209860007554373823791566403296687602175361505 285094243253110466482228331617976309961422107322410715366585432769599423152524976769015815662063315817819914745843305620673235741587/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^33 + 638206192354644305343384512797341609326361421115473727472207832424995103929816081901146690395259635160929478089590481627935555231037/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^32 - 8475341129332667353239434030026087742118835645097970875697567167984817409273706682391668993183304235819209379033274141673767886960387/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^31 - 43094226720553746548953520782518777586313205889042223889155725517470692618274083923724469008644265156455956315513676108712300965173151/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^30 + 353341678666508380079640986678809762717501992850987871841805145217971742655330796989856738609149396262890106207676856365047249665856285/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^29 + 1073351697238968145277566251402344441134162241867621073600130095722630946202856553020204336376066333375016179532859124041719861954479393/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^28 - 3478980894242985869168796864282217795020060100552864699595144772166015352724936907864719180075495341046686878059239923769575405860817727/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^27 - 7043293211605247515908394566651752865861335005034552934952538313987530191448746998392440541966303352629570545654497490000170385483522517/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^26 + 8836000647053770523836772195737546400448390897905341886890833229109481524464442877392031661844418896978464387881054694862019145541631409/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^25 + 52665841758617982132532248856934840448147803502797459282593600833526245347271591800894122958411423054951008400644530106489553010741700451/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^24 - 207769390737864826274270753204321948248265922705018459303024702369979640380752927014078249363339986251236409723173689999829080328231565/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^23 - 555521213357522774976013910964522620836161926691444907799290596998165957169733723177300439150010436956799283884280234833868345527868929223/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^22 - 234604528512328797744899203983580821196306096520661306207718454964028872068219545302731888751505309512738195523761626872041969525705287367/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^21 + 599070657290360466836504648150712734050707133348558271387085674188936625680790163461647148157487980846340570773465489927931337023234549149/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^20 + 1145187896106581948735511772477679550195143462717033137752297165299238290418437666529757187381980758520331345268411426290466826544366898817/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^19 - 2229211705727102736275387712127689296077571841789218509359038882335113045236399679613783638345908937535895108799022304513518403558973620533/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^18 - 5267576544548631789147598267042844146010240401663500056395448928738148302461287397263672155718443838284355332474641608730068037825792051237/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^17 + 24493913590201975767314227541876469789806344431696913205456673538568950193057137474708552356207111747731926612139665557461310210229922079965/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^16 + 1438240232402137124058782258337578611444941814520859070521789262275135424873135907481285311423761446093682430132764417710010022687154726677/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^15 - 44434270948928260981062802639966966592419725662365177790786562334762728959692521698995149332198960850742109796586497152595938273725012472391/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^14 - 156199359258989570193201583310174077015420514831735087938242910403786356319027307844001002252969349344576748051330096303384762415476360151/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^13 + 49806389197256552409253087045411898658476558154174064355815552756505106895352420398008727211226197389510586069194498561439719376460447723937/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^12 - 6883082623479520889590517569833697878786821992647537028195638108345955022686587785085471572423475567006180122103477350157953079859086008215/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^11 - 8148132276900276385022880371777773038138588815895015391159232267586871491925549059205678439854761467050369117391397877733649167923891934157/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^10 + 1788159693814327567832266770180636247982861515028760419179897537803555639119191533843076113650150707751261870610276199668925754410519129185/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^9 + 3187787257045698669443101236480450146750079185240312855774782436352111528363586266027909742150757733008003820977193840943804568166574925087/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^8 - 1421182082988274274706221842691990932841020730170706683318448503492907254660696710479340955632330142641947616192495523514652238361610536895/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^7 - 3767687122033376611161874428527854256939074982671341384755971831523403229708605790922942028069223800318590740405122321770769436875322153421/814777281008104825650084286789814933155264946113247634379382326358089842030346215897857034744832386783939778128199848790405231378509056*y^6 + 43870236339946196106121144199034661768416689713062791194867513720473423332353274326750416870456969497854221610034344734286810495752555231/37035330954913855711367467581355224234330224823329437926335560289004083728652100722629865215674199399269989914918174945018419608114048*y^5 + 164711932719817488371674814390288424711969529288712934554967623054587819376454516554048699716621602924141672481510981297123397237766428261/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^4 - 2500740280012404800039825622385387351956928268487142862066502758045371964489356730546224814644792506998747497884548836202753221294774201/9258832738728463927841866895338806058582556205832359481583890072251020932163025180657466303918549849817497478729543736254604902028512*y^3 - 953644710741180966356095217717303987839899300119469289520113721048784734510904769523668770366867604241398284523756191645443795320344411/25461790031503275801565133962181716661102029566038988574355697698690307563448319246808032335776012086998118066506245274700163480578408*y^2 + 213928910869205147257236354620075618621295166606700510037477198403001081522959239772857846216280696185856010937546470049945517623296279/12730895015751637900782566981090858330551014783019494287177848849345153781724159623404016167888006043499059033253122637350081740289204*y - 2952198747693180972801247592084664407226140896531369544907807367044453274321138143749172350593709030371305342346255579012055607238475/12730895015751637900782566981090858330551014783019494287177848849345153781724159623404016167888006043499059033253122637350081740289204 21135848018189244617628531983153190926196875172588431914650054982691725929002620474024178168375651220706975799967608972555353514510947/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^33 + 27017773420060772965043668809342820855905856708828669591730658293870093868463858239570884591564979418480297476063492236871018101691051/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^32 - 309658698155901085284360996973393469864619012683157030683306891077850446845457619656835569669162081569705915603892524808950478956604213/1731401722142222754506429109428356732954938010490651223056187443510940914314485708782946198832768821915872028522424678679611116679331744*y^31 - 3586438737843040601703481161441572631506696551236792672696038130086140002898136270373077128825005253181376592305061808810985127244302283/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^30 + 6251495428698559216960269538307342167959464065134662663672010281434588828354259710964633372063413665234664178413241232485820075964840425/1731401722142222754506429109428356732954938010490651223056187443510940914314485708782946198832768821915872028522424678679611116679331744*y^29 + 87375040897348323693058245717391913732925166020146103899064476165550321564170705388930118988431260186614288832951455121026650373432253005/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^28 - 28645579481189975817193334067179210329278938787183851445971095581282423769012796526649227515429918110011797274717106036227227151064309877/865700861071111377253214554714178366477469005245325611528093721755470457157242854391473099416384410957936014261212339339805558339665872*y^27 - 556780301783041229207863987771676696648704820806390219727500536779029812150074258682888215170777619087078430622362795372354650813748912229/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^26 + 236891429838059233317993001639707941097108690766290552931114327098242577867579702960724030695824663003762247629955106569413013727229174885/1731401722142222754506429109428356732954938010490651223056187443510940914314485708782946198832768821915872028522424678679611116679331744*y^25 + 4032290140909927188177916445748031980586203974413958859678708571921408140539867903763056772344795635554017208324982559324758405127480194085/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^24 + 1235367099663745190138599607733279777645370246033875084705049995843536734033530990346767268027166345701022750391831081135073228601257131171/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^23 - 40074625768566084206964525107457949093038729470387690674927434772624211541757561797568841979467809738089000308346101657148919920960569576437/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^22 - 47372661853052068442403208528553913601031832238013756585036075567258055770468515585528800977625424687676131884562400092011823160769243938797/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^21 + 161034841713476003709238788743230335384603293520162740989536292510877323743758320805034971593595840436880772539170126834504969453723883963853/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^20 + 1170370785165537476424744335110724941791034357124947706512586413489149455353512790202922997792521243952980128229458483764510146724561186283/37035330954913855711367467581355224234330224823329437926335560289004083728652100722629865215674199399269989914918174945018419608114048*y^19 - 585507132072817539094227185458905072226859383437982688645680645426061760929114114673333063704215410897162733148872050729473684931081690698065/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^18 - 35442178031084507865240477951480238178331275412212957994537228935663044996090472096960860151456635377286100175765634912279193078547377094759/432850430535555688626607277357089183238734502622662805764046860877735228578621427195736549708192205478968007130606169669902779169832936*y^17 + 1614255225573387696994516037585527235859572578416701900000784198991469836961381774707203540170930747733471288066493766941135306636619183423813/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^16 + 83097120301099367468401504580672244837172593060898257476996982839623189787604066605763908525127312888775173165945446380780576980224783728817/629600626233535547093246948883038811983613821996600444747704524913069423387085712284707708666461389787589828553608974065313133337938816*y^15 - 1472498482733151799510583726494428953104198246098203035539912823945505953335883894021806032384890898955481895524643809162007382106518871915031/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^14 - 902774513613938515794688481732497955379680397543326359067535327669860724421282586817880898661332670137950064487177107559732989906014896937009/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^13 + 1649746793705018377379921650389569325537689364751468527715034867905712205405182867237095220073667747156715117367853878601955282913032486699411/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^12 + 486465728062668773026482322918742537045048795886672011340712847244008072060141490587105530531265963218732760426934740377502496053853115664291/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^11 - 2145416722617968321065721327107533993841438244088105796436576953559776627422098275550667987410899879944638178068488023201212611986070050773547/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^10 - 114178945992785358148327696836448949870092462798556296586565725474643058683610641018226606850989156562995253411470447427818237212855172370677/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^9 + 836360402717044815874979535946205029687967512978084396480764270721098487261863399433463757876032109534767209425352946435433452383333053854253/6925606888568891018025716437713426931819752041962604892224749774043763657257942835131784795331075287663488114089698714718444466717326976*y^8 + 2307580026684036950451206614785199050297427644912681540476186076973728241964137272535498778923286346997922378363995267547472118581170252801/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^7 - 119920309012567251006922753121619859203903201213450950924249899890097487208072018972845029497875017398116427790896482847346590789893116448881/3462803444284445509012858218856713465909876020981302446112374887021881828628971417565892397665537643831744057044849357359222233358663488*y^6 + 225155239350767013933295833900243326391014725504409300103078411021292705417365585249722952623153192681076278437103985798533794853868426343/1731401722142222754506429109428356732954938010490651223056187443510940914314485708782946198832768821915872028522424678679611116679331744*y^5 + 29675180501532214180822597696867637572368377212305223399452889680541894609607349707616377458196097772448773106961927667021246304576261113/4918754892449496461665991788148740718621982984348440974591441600883354870211607127224278973956729607715545535575070109885258854202647*y^4 - 11272367783840185027319731107779677023121749542170318149669057902103005421036099337986766415431004077844933532800179970962307806760883953/19675019569797985846663967152594962874487931937393763898365766403533419480846428508897115895826918430862182142300280439541035416810588*y^3 - 36831563719279470556580993487084781392115983918113176121901249163799763989512588757201776814340460970943506676973989750796503929593958823/108212607633888922156651819339272295809683625655665701441011715219433807144655356798934137427048051369742001782651542417475694792458234*y^2 + 2334639619752250326232889266531018220691495310696172504922421556446750688412652520278391595704469157678968001396256642956829414393325255/54106303816944461078325909669636147904841812827832850720505857609716903572327678399467068713524025684871000891325771208737847396229117*y - 4787001269672043836984681976928760957720909120519258109893095987429007595140482820636578950958138767458119132942861145636002459782783/4918754892449496461665991788148740718621982984348440974591441600883354870211607127224278973956729607715545535575070109885258854202647 -25568683727788096161564103474411997008533789128305869012052753992934265146287205652483449548780147173082060972727793511984013827471697/19295407427510118825622450609886071826086047132954637159620826910571127622627744476490159777366257887019664745672369146354596615827419008*y^33 - 357688088780029149470115035984084428693421783331455094166086844704720134226236681333156099419774771014927319474916113615301879598879611/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^32 + 2061253974872070803718892757031802990709801680914798416717696690391602254823180765535283149493848762980169935575343882015873369042177455/26531185212826413385230869588593348760868314807812626094478637002035300481113148655173969693878604594652039025299507576237570346762701136*y^31 + 47504859491913776222346737374857878825240974421441820978423693785571265980679172602775773044025097365691475466545168169854506572780863339/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^30 - 83316483733936072359082934377096335938966557186217434598229040036173126539306760890886642817184735802081670175798537519380449990148413701/53062370425652826770461739177186697521736629615625252188957274004070600962226297310347939387757209189304078050599015152475140693525402272*y^29 - 1158049753542862457411821957409179268814409467964950520422111853096317279115691393236003687840672069281813811772559140449299607755262150809/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^28 + 382797894834376640917386559320697760029824517307659249009257358370591771344467294905572246572043425657857199487953055615713692505026213337/26531185212826413385230869588593348760868314807812626094478637002035300481113148655173969693878604594652039025299507576237570346762701136*y^27 + 7385448209870475311001517534689703780107705819393998099852675831553305634030941143284762868653723506563043824615070074456994415376390826803/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^26 - 3195265952459164371317439880306050850556179103710156439456310294184184417882459850266805776428559071816056794573195200929480544745650508341/53062370425652826770461739177186697521736629615625252188957274004070600962226297310347939387757209189304078050599015152475140693525402272*y^25 - 53527693852147987077603481415897709816905413173866732395316181397954982280996024505329469464716878798698282120868920404187581907762761340961/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^24 - 15788422205736672565817397382412075605118502585160517522608724012224547528410865860662695220091133853642882390047915761311082579840784994915/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^23 + 533010543979162041312597797102148708873518540915655171086491882677675379186178635980299309672646800528561603043116813828552291538324573927701/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^22 + 623317467523527875472098088362555262279242045286179436102439157934717565168544289582269301761653661627740446606391334775375821646656653621165/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^21 - 2147613508176619709825030207132119477537512272415060188250496591596116042137097822226771233675087729331870434915561547330645099364195148539169/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^20 - 2880804885135512956635429866791818985226263980094705763709395779636774300690290062594514984383899198197423638949665705064704527852077177899741/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^19 + 710433552824324280368428225341356878781269157912373961734629269027311895531445299141349165735352016992043793279664644873448698660100732122399/19295407427510118825622450609886071826086047132954637159620826910571127622627744476490159777366257887019664745672369146354596615827419008*y^18 + 1857042059172536125921174507959696942840614641855128007290913794208796734651868129480457935294965935997180976880262641075379076649175418519239/53062370425652826770461739177186697521736629615625252188957274004070600962226297310347939387757209189304078050599015152475140693525402272*y^17 - 21525871138957503896880139676886406160920180630684052509691181665728093651043444504754355883250613372306780660178281990387574974653565868928393/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^16 - 11846098802571752865475414980206256774646452036432428797014938945182772867427719332892118040217621275333338598146206717416448905230662027911987/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^15 + 1782011658633226169144270110899256817309090322277899793924805288043529810072795189575386706269173471966195202040466164138954553876789619874023/9647703713755059412811225304943035913043023566477318579810413455285563811313872238245079888683128943509832372836184573177298307913709504*y^14 + 11457566291525104772569978475023175966493912207650437265885233460756620117242997369038652127555444104287226753836585788629492462945257008758749/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^13 - 21907883509899015493197447243598990797738932412773366348243255494401847889460981733021219825080891316537500837139982983007237304243937788832703/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^12 - 5884309738238083273340499587690519031529986435440809233697378440022417379198189318062210800083347990566395034478532456639717290625541546004471/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^11 + 28383228698055941780621748762026497214103605554133895748113227669912092062477234124585527755798879104318536677568459312752942415749145342976091/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^10 + 1168077006813863553458950781834627137164722181544428672293165771150311541666717406942687614023267681301272347864442774260326412521402721526913/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^9 - 11016048628964607036737250870069207086635237914912939847133255086644427160423724798834581650112614827759780689491422234488691138122473892139273/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^8 - 399837442697583638765725183495728203989342020681227735495793340817527907841269688155817368307914369027477583261136296004733956677604457703893/212249481702611307081846956708746790086946518462501008755829096016282403848905189241391757551028836757216312202396060609900562774101609088*y^7 + 1580955181260281960659604423638603988787601497069474416855586667558588531830346746770277454194948821661431949549370163135303935984271967619911/106124740851305653540923478354373395043473259231250504377914548008141201924452594620695878775514418378608156101198030304950281387050804544*y^6 - 1523740872670042383473199658351108744133918851258268507278585878454652892209517203713999039904871431628126492475750026941856857701890883967/6632796303206603346307717397148337190217078701953156523619659250508825120278287163793492423469651148663009756324876894059392586690675284*y^5 - 68385796733877307452487498229127008823982357405431353352554805210824783851704329056005766026085793812329565877835841280228858588417812568417/26531185212826413385230869588593348760868314807812626094478637002035300481113148655173969693878604594652039025299507576237570346762701136*y^4 + 162150873879500781786744854695929164123277094067234351875490119607729459611778863612113738730964901261904008847431467561254227762099427499/602981482109691213300701581558939744565188972904832411238150840955347738207117014890317493042695558969364523302261535823581144244606844*y^3 + 86689150429807333022376629048324915211087848211538221246426071768216370587872037979180588661639630168962856102116484488837728966197242337/602981482109691213300701581558939744565188972904832411238150840955347738207117014890317493042695558969364523302261535823581144244606844*y^2 - 64242266201098977709013000558438900325291524090854775184886701329358083387497778817820820746344848622991526158946553234914023841065346187/3316398151603301673153858698574168595108539350976578261809829625254412560139143581896746211734825574331504878162438447029696293345337642*y + 717739666001582173081360630363155517874402992645112781159205953329801482737613351646779366369876438331861751637879327731365875951819532/1658199075801650836576929349287084297554269675488289130904914812627206280069571790948373105867412787165752439081219223514848146672668821 92044356935628566126625722467461012690604500030592189973204411730205908979188751773342757915854630892445675938671013503807669610129891/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^33 + 9123988076052363636827270926402704643275062542070626000706669859898782872499407302491179378864761615321911543406976036863313967625223/18517665477456927855683733790677612117165112411664718963167780144502041864326050361314932607837099699634994957459087472509209804057024*y^32 - 685330992564425192329543113677152459276458174598090077142399889120073286916508357433514716402636064424684084672522023324984712594328683/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^31 - 13591924204367686885053142078835276685584216190530469884049468743662607310641626231917679869774814746830363250573920966064748110382959187/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^30 + 7173272394564942006257715871667247191214400800200653180976644284012259560156641797725503954293222296258318559193564723827113633066805229/25461790031503275801565133962181716661102029566038988574355697698690307563448319246808032335776012086998118066506245274700163480578408*y^29 + 339616623869246837471963748039332840455179852481980863832468920042136419598901567725819179040226369962041432992427652262269521343208044457/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^28 - 285258197277892361418178455388492249759279520099847907041797364143028234709133444613811097298170148559386445939130683774929964819296513583/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^27 - 2237545359774362822778630571996531457704922257082575006839669004393987249426305102042443670594549166885304509940200776862104288576667966127/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^26 + 1487139332274897695515863061531144694407544217059606656977367558378322975385260247147892320395552487189049661248389122903063138895445127567/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^25 + 16788497132958720587155702883867286766739486438668979444920863937292706054323252286659685200459163054163020926148143923067642190181070817745/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^24 - 1212657954793983929146286214215598906566787928087893369183075209250706171768631773968831050735850236940545787661954392936501853159566852297/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^23 - 178604305743373024328961420171434474663341713464178955566482236919380155319262411244692462525739695393325726139670982100014721699423337123029/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^22 - 140847430675266175320347449959492208810594809360815723686572471077665059415456170716425944961845955611715851883216267879603608459691263159073/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^21 + 778899458302097980828565522993952040980314180758006627724238015697212765180139985678343761275061625241686759185607590762758313314382374463653/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^20 + 690300811421596323006482090906776182883909976430335565096702727721467226266628903235730425189154953031441771935801806243110606909903809599385/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^19 - 2907753946424213038315009617037647438458464792576972648906627306142243222951526629051027508942365817372516895618567754385335301796515345049401/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^18 - 11829269770039719041632032396651129174447894559317895584740522179047496633935864257158836381876027777362837741980575923823359744076660810095/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y^17 + 7956402886283272827025058235375418403838964282501969829417871327811365868544590789320744992742406082590175641900699593744404472363987972521033/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^16 + 1347922845433635041509328507127135460639639775644597569077642749980422155362050638132283184976188988327139879469115441130426918111925229704631/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^15 - 7158357830731878258938600873528142971045469568819258482885918268800856968808719688753701983433026315777461539383769732931655752644527486636047/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^14 + 865645804081366024695564999317318497844580325812439431061096070215134294110160329789833665566778063805429962578158327415382868911874457374843/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^13 + 7918969146496672949697029076275481320963359458005088255020879900422647150124997735751824663693519930077507084805538595323203598635692785721625/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^12 - 3243765175427794355465310144531949147499283379688512957610179678918209078865827862115061352830683578628321453874266655967936230348804033730961/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^11 - 10127572568249283822695894671425451065294172292616351373590762675023444203841077913493003112638242111626625446976118348041908295984536922294335/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^10 + 2976339631911806180600063441349710001518444666251821798328164749255303133406940268272091498352191615727542547675836993695794279657419539288475/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^9 + 3819485697881194793385183505246757078638842702353357426927637731892516002794165467338854896176238647127477467076015225751800362387513558414653/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^8 - 1177765047778450590865489002054543921751524807465763175404636193110107154685617083524691634875602002849203991404952512212961425127864322734047/407388640504052412825042143394907466577632473056623817189691163179044921015173107948928517372416193391969889064099924395202615689254528*y^7 - 552378862186100163921747339556522893407851959254177270346050738721608390032025331319004606650950656915350826253545029835668051717013262522645/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^6 + 3049613231974494602814816911082701780080039626123141703538571314414922639403003159698227545474209269041409726673976523595431233592891834328/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y^5 + 22380047337605744260654219225726333563300929229231600520371856116258249505455834716500958349601493388608629697302327442557994853445327784267/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^4 - 478917676969642344997218406218301912684324544811877290954199186580855711572700247226682635977002766511971986511029367295576817400892228315/2314708184682115981960466723834701514645639051458089870395972518062755233040756295164366575979637462454374369682385934063651225507128*y^3 - 56016994552457657896560296944383749296695663037894882313232622978704726966258992519597662195524592736566886313460098667379388438323652937/6365447507875818950391283490545429165275507391509747143588924424672576890862079811702008083944003021749529516626561318675040870144602*y^2 + 7197493075245211275680196627153523790687990619349866865377894148759193559911901033829077775272127754602181411262534366374183777159085615/578677046170528995490116680958675378661409762864522467598993129515688808260189073791091643994909365613593592420596483515912806376782*y - 4092167108460773684451048052072766178927740853283436749093898678814429123058188316712158853254072054330893515596451216336345748894836076/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301 # A Gluing Matrix {{2,2,2,2,2,2,0,1},{1,2,2,2,2,2,0,1},{1,2,2,3,2,1,1,1},{1,2,3,2,2,1,1,1},{1,2,2,2,2,1,1,1},{1,2,1,1,1,0,1,0},{0,0,1,1,1,1,0,0},{1,2,2,2,2,0,0,0}} # B Gluing Matrix {{2,0,0,0,0,0,0,1},{0,1,0,0,0,0,0,1},{0,0,1,0,0,0,0,1},{0,0,0,1,0,0,0,1},{0,0,0,0,1,0,0,1},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {5, 5, 5, 5, 5, 2, 2, 4} # f Combinatorial flattening {-4, 2, -4, -4, 10, 0, 0, 5} # f' Combinatorial flattening {0, -4, 0, 0, -4, 0, 0, 0} # 1 Loop Invariant -138861656590125306209199194322487710962886138856077917454255339035546042367591879016265537394665077557299567293360664018252809508545657/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^33 - 346199644110341214743672816569671865308727955654176372562025751205715343563615350403433045027794334766869722274359682943096751888348475/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^32 + 185482770117051196823518868738919668690071192475272064180300265502634798893331650896622915741509661922956978205160702380503670142021231/4629416369364231963920933447669403029291278102916179740791945036125510466081512590328733151959274924908748739364771868127302451014256*y^31 + 23049429557999874863522468948678126083711831740636019974557603514976312042853516479681096953321306632372408952172747885900777039847972181/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^30 - 15076013839729038859093785077235019004899093775069880828869298481420585668438250126116415308393404073338751288874781584549472040572165529/18517665477456927855683733790677612117165112411664718963167780144502041864326050361314932607837099699634994957459087472509209804057024*y^29 - 563822607941121343358104148142595714906496441403057273139821294857912157318548479518060304370906238214360289383492951389214201303667121293/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^28 + 1543000001624225064767998081997605737856298092588717364873571854940224225150574539883705307030704501846333363633605339062855647441763620997/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^27 + 1806276049646433958928786227103511070365414065903568985101783498316528475309153533237253844272398343867053481122557645833877755540197507397/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^26 - 3348339322396677376217104087757602847280094246701603540519775937037426169602024586956541551735581158714782778930138095024153432158727047297/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^25 - 26321934830326241103068958594868313775916461680176263907161152576106076920241881748144319534826015548064250986875649292274339092591347712175/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^24 - 73107863330876943759873437509476081549673842096155590075043498536971352122629202798818443820706307016322298672579644824522129069340955857/1157354092341057990980233361917350757322819525729044935197986259031377616520378147582183287989818731227187184841192967031825612753564*y^23 + 264686010395675697108747295290792550826721625972749310674058025701885450119389733514291219921519104636886399034176676907559511880402370762505/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^22 + 147449766254575923857492238453723154534120664398394560927345182371070045253539461211456013148435888265231024913468979218299010510882167579961/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^21 - 539651513910229356832937107574229283595435039045782695770644275320999413820112797256329282205399679213306426552709655996870115376286609740207/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^20 - 343503053035027827104268142570565984636154486843638512813139107141906220789861731162037417086718088848348174756577178477981938796141372696489/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^19 + 1971519520705694758000363760797999503235904984409411100641887110267030772213275417947414107460625080769146215233508515683401624062779703395109/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^18 + 3495256530163952478281475181252652336809121958411621036260519409911915873101406452929302932627915848996396600950481723589083668843968222970053/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^17 - 10859061074587561421940032897119430904490672059831229114880450499545910060110025877152812604405514154743405147477529213488525332040427929793993/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^16 - 1342875434099261403116364767640234401452313110778535822967302555257286546318426249482191640299837889972162869754309965161093521781126956880661/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^15 + 19776749435826468676329306244128626948415427433830698254126965519191760370373499102266433612685429763360069233836580552067447874119474480839415/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^14 + 4782200765084018912536803230654723271753208662531202505319969761917413528093544091245969487840380332761744890965828846041348001607938499638339/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^13 - 22138674338012897437879707009214734489837216675756815953923261423627676396631596033778791055160619044412493885659889803856637350881779391028855/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^12 - 1927884159535475579136324037268637530224931949333878736846152497581824917355168993456371159116131886258424345913222935531286454730691417511449/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^11 + 449605172396246794377585070213477205455341074207529027188464334888710176049187025457964537774829967943332465672417772603842858495938005269195/6365447507875818950391283490545429165275507391509747143588924424672576890862079811702008083944003021749529516626561318675040870144602*y^10 - 27069254916376179203417989426300316713078518562157025399081650359970350212125937566305167949217568614397415766481245641670776933889277905363/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^9 - 2797422717018957150827070684016183755982850376459232515240266446112790571510422218318142125320718057397921622793960033177200604558957980160007/101847160126013103206260535848726866644408118264155954297422790794761230253793276987232129343104048347992472266024981098800653922313632*y^8 + 12235242133602326971225100409773890872121599330188120451172230631054316099212057863774273990914271972739988242611992037422234263003566973917/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^7 + 1612168551897649858935335304125331841519832179840589387670952373896828191906342865815830595064475316629232453719716304137002562498294118640581/203694320252026206412521071697453733288816236528311908594845581589522460507586553974464258686208096695984944532049962197601307844627264*y^6 - 23126304900953157453249583452590100801131524837376851576711052354018102468598897282977135969997298479618523051262519835187807244608368492091/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^5 - 69913368263766047186376881931311483076514017582318758786280646096376906950327777921716841829850007421605678038887194014058727763312849935051/50923580063006551603130267924363433322204059132077977148711395397380615126896638493616064671552024173996236133012490549400326961156816*y^4 + 462229776023961362294212291767753737995957696924726348243815039117440100539954197910976696098444267588477792576390257741408269845607927257/2314708184682115981960466723834701514645639051458089870395972518062755233040756295164366575979637462454374369682385934063651225507128*y^3 + 465870023756085722899486200393830732683004557911638662031745631286387480101630526906268175691075532860310458487858061769885789836847909681/6365447507875818950391283490545429165275507391509747143588924424672576890862079811702008083944003021749529516626561318675040870144602*y^2 - 43436649290364362346617936414796992208296408012576426871842050745958278544438582363025842793578607088106220896099067913451176478978601843/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301*y + 1024973393236290802190086879284003380810482603214018149144806696786273864935195391135092497588786373028582665833459523680901240440507837/3182723753937909475195641745272714582637753695754873571794462212336288445431039905851004041972001510874764758313280659337520435072301 # 2 Loop Invariant 351329609934881155919295864935488710379534968632631247951849048824029943878377528314304481971028699814763868091819454482567554203933263893976874218619970368753536559583177973947973892745978619176750533747096109540171610340310005686701295625201831484671/4703668956682899590752128272034410866601219276384835299375259971865839122826073388033927654596563552041410729888098389680012739443050727164705485650464156246452456026159666985072969334133398166564719084893042374131728736389635719236988766291443958354480128*y^33 + 322563010888885188218551806130900176712380136364500466403201426529591612677581073468145642907896107224921997330276880300509289648290465231997679430621880202784677074924127264358338267081751380551384292344681577020035311374693937713961576593035100964231/2015858124292671253179483545157604657114808261307786556875111416513931052639745737728826137684241522303461741380613595577148316904164597356302350993056066962765338296925571565031272571771456357099165322097018160342169458452701022530138042696333125009062912*y^32 - 4493880992080679542397426681545365295403639771096637095833917095457021361467422840103119162707554883446804075573507075530275101190359612824730331404574571061978835496838342975466889908777344766796226537337288289384473566865160680114264102647851343811211/1007929062146335626589741772578802328557404130653893278437555708256965526319872868864413068842120761151730870690306797788574158452082298678151175496528033481382669148462785782515636285885728178549582661048509080171084729226350511265069021348166562504531456*y^31 - 51110783456531409189832684237745056518317290142367877066924603258428604680433387340096565838330865367999441300650182798386767272297151139244495490776458765574669935622085320925064089850507305168909796199477152084523110790224358807562902988904652172662667/4703668956682899590752128272034410866601219276384835299375259971865839122826073388033927654596563552041410729888098389680012739443050727164705485650464156246452456026159666985072969334133398166564719084893042374131728736389635719236988766291443958354480128*y^30 + 1322867851684416850733591759802951278617732660579753912467310089480519445696366606785726603171265485370953219873064109606270380227416288708836967373151485224150321541643714715637553829963575456961421926456703959116201711824545123546798086577815453162004693/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^29 + 1281872154685709429747925359199315583959086501426098618538408420390001136197086871258144438243555278987002639347036901040969246459909729309658959882445263302466322918846669589185472784995474489264875644953879669438170114476841624325522476358693621980575217/4703668956682899590752128272034410866601219276384835299375259971865839122826073388033927654596563552041410729888098389680012739443050727164705485650464156246452456026159666985072969334133398166564719084893042374131728736389635719236988766291443958354480128*y^28 - 13269220439033932516625048350078776841010850925445151490331299175378753618063987330889614244549822492774091568447503429753109545515637885395663759416761197654131566625240953448854016621512515069567959328809612440800429217447528895446268365613407325442615311/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^27 - 8486608248118652510732822354182909310075431232038424514453279892247999736548376723103490584645331674671726935544110400873378927085031869347401742145278047776167050782435186096430678028596761218084749113830563043700128894818793386930603154944223006279827767/2351834478341449795376064136017205433300609638192417649687629985932919561413036694016963827298281776020705364944049194840006369721525363582352742825232078123226228013079833492536484667066699083282359542446521187065864368194817859618494383145721979177240064*y^26 + 35296509694267761225546161784410051384378386400009903389792646235554400470287961782616209004191952474338168619799519765134419879495286110930253519195317123840976490112652167959602653989184003477662418831326037387320268223722431246472672304998992850016739397/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^25 + 64027218566287141095062147467828294314558937998162997971411754781569646524419145244157222543252562915597305477107443718564891362378506933376780097738006107076080717548652879372744409192998990210916457792866849838209856509942628479069783240308112544699379895/2351834478341449795376064136017205433300609638192417649687629985932919561413036694016963827298281776020705364944049194840006369721525363582352742825232078123226228013079833492536484667066699083282359542446521187065864368194817859618494383145721979177240064*y^24 - 1600976961280596351958425076618204203628463902695030122131129653066266945058988179685924832209416296214288539561476048118420497010708802785942016635102487824511335107528721778190263867884669258338915358905258260269005140620664098620721717516523800357000599/503964531073167813294870886289401164278702065326946639218777854128482763159936434432206534421060380575865435345153398894287079226041149339075587748264016740691334574231392891257818142942864089274791330524254540085542364613175255632534510674083281252265728*y^23 - 98138504021435962293047421679097805740236967511791389350738366041518655527037461600162287127485323252778354694776817537141172381549605959302874593883634198456150801693513823553250818368584823756493372565352699282362654907536021120716697202913252385443476609/671952708097557084393161181719201552371602753769262185625037138837977017546581912576275379228080507434487247126871198525716105634721532452100783664352022320921779432308523855010424190590485452366388440699006053447389819484233674176712680898777708336354304*y^22 - 128125171157183429390815770035976440756081358822807198535676130096713184109628373405504648736548610426994374297798703984624476466748566409304726524493035249103247882903587492285893802985474828045182538162902339059631263850252702055771014410955741281604571805/1175917239170724897688032068008602716650304819096208824843814992966459780706518347008481913649140888010352682472024597420003184860762681791176371412616039061613114006539916746268242333533349541641179771223260593532932184097408929809247191572860989588620032*y^21 + 4533128046253640942347514059040027016492583410559160366183339098132372129609165517388805058632907877282683053898454438092730339556528933165093171629953902963393030623117205298271400767791661014919692351530785007789072419724684285525282790026734070838781910183/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^20 + 1913042310985705418457912606281977678129527571967647920254916756118867182430403412845950902237226119830037650549598084413026387796780706900001018884584213782187896858194452035110650706541913563960204146703665321438556528445713873689624665386845370553663265421/3527751717512174693064096204025808149950914457288626474531444978899379342119555041025445740947422664031058047416073792260009554582288045373529114237848117184839342019619750238804727000600048624923539313669781780598796552292226789427741574718582968765860096*y^19 - 16975457041448876745304413176741134975439831710704123346979239133421222273648709411967890506738318016248019170233995045004517362295356916924056119549921721815381373538412091748714661415082549504809044462522433537237178016147444960258568495929933656426421307987/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^18 - 16481190250475089688404926876084338418368377281259372347744621103464345738099871908345344699364467812899628698904603387686205231289210790741996782061020180531120267982174954369716357286892147775005444379583966503302197873169394555996124977678791876780720303801/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^17 + 13293987828236703281052731120768229781507260966232011739167615197918885577018485412821162548155240570513695062553772005827863068114015039594110094553153666449096032631002084826092447293306089849283181286280051841504256112553996896969015506233635051984799519729/2015858124292671253179483545157604657114808261307786556875111416513931052639745737728826137684241522303461741380613595577148316904164597356302350993056066962765338296925571565031272571771456357099165322097018160342169458452701022530138042696333125009062912*y^16 + 2164546082112510903943332776914190123854765385378090409552815444696183360469819722718135953138196363728769091305411951904714491920900380185512897678151926962529458240550057406626077303598080026706037610254373390117159605692086716847500266467229885953042179405/2351834478341449795376064136017205433300609638192417649687629985932919561413036694016963827298281776020705364944049194840006369721525363582352742825232078123226228013079833492536484667066699083282359542446521187065864368194817859618494383145721979177240064*y^15 - 56017416253501888232214798801888862936096283394432626440454613872087664270627392073294670026662514717350540953048952868729425501689196267360518238242355031708048498115567636760342945492411048385169481767375104144906566517293415032073412587492423365963194696373/4703668956682899590752128272034410866601219276384835299375259971865839122826073388033927654596563552041410729888098389680012739443050727164705485650464156246452456026159666985072969334133398166564719084893042374131728736389635719236988766291443958354480128*y^14 + 4889054171843252708503206151682833451288585639238055853495470567842258752040931820609285632853952764939759601206248000249839642239788102406333607800664020580590511741293333363144617769587787608485906471335255188652164620893858378181135958069344016000259369029/4703668956682899590752128272034410866601219276384835299375259971865839122826073388033927654596563552041410729888098389680012739443050727164705485650464156246452456026159666985072969334133398166564719084893042374131728736389635719236988766291443958354480128*y^13 + 187345398109549817827232721535141181092177419393947051934319843573863478565180008245814570315019854335972664390521224711600491002149207554607527347747088322927086252582875364360844569989024558441688044772856040529927942776909660443493031918835183667891771594701/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^12 - 42876197177186654215303915594797974093294176919282287719652000469664453552205717709515175157136096117870728432799941338217379322949966439257175939954407120312229827631520055013550389967541981948223059279497225392827027830919412095685557695775072541921602816553/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^11 - 60803772933867686332757693634505357504237829359800977001583183627170432401936136637545953482457730218799613523948910175584934693647801841212477466750412443674728108936642607317257380750973623762459413496032038315316957464760551723046171436192001340614350985483/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^10 + 19104497722557010873667224992940483740306921299834012088711611884259052058421388097602540588517514507913301765708144430867607349527139580287095799856382172214432529587583724787710868446754964398989034836385774034893145064289750896065903909104722966344476600905/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^9 + 23478652454249600233528725697345171895585722398188831340575019906236033885315794160124334411297166850175185100164457452625760364443171977221782484558955939503954226194117029705131824205562473390367586627595172821115470805455808999771427593806955545766581635967/7055503435024349386128192408051616299901828914577252949062889957798758684239110082050891481894845328062116094832147584520019109164576090747058228475696234369678684039239500477609454001200097249847078627339563561197593104584453578855483149437165937531720192*y^8 - 3832842553908378535306078365545483927402900795443076752315103029397960932026005070158850442920122442212392568242961603328099842406842180003960605542193103512914006414271506898178869292277199768405726209323092511002367854172259981160325863276038714550710699403/3527751717512174693064096204025808149950914457288626474531444978899379342119555041025445740947422664031058047416073792260009554582288045373529114237848117184839342019619750238804727000600048624923539313669781780598796552292226789427741574718582968765860096*y^7 - 13859753390991353372057828511759648915138015393288298088000679286198320440609771430157549650962280073999249021560645450696040997287910860471651469104637667258308209432445630152988310114213119508867503796232187406198262870292046043151031822134085562920916274413/14111006870048698772256384816103232599803657829154505898125779915597517368478220164101782963789690656124232189664295169040038218329152181494116456951392468739357368078479000955218908002400194499694157254679127122395186209168907157710966298874331875063440384*y^6 + 227892365533398994688636934818601238371502194314898461015173692439243170392201592288400281110575265093012241244979623996147156412113762160498423961761940191165876949251350494562935782782319527139482526391769041142332976839645076121619443669167253037673161613/641409403184031762375290218913783299991075355870659359005717268890796244021737280186444680172258666187465099530195234956365373560416008249732566225063294033607153094476318225237223091018190659077007147939960323745235736780404870805043922676105994321065472*y^5 + 197358081345532021169256710118760552965527661746706243887279823610732856707887984872644259244978229682515898238818264658279285992388564884268482897837390546053015993525636412151495345980457777806216217405353229383234300980508741231337018447169129074850530973/1175917239170724897688032068008602716650304819096208824843814992966459780706518347008481913649140888010352682472024597420003184860762681791176371412616039061613114006539916746268242333533349541641179771223260593532932184097408929809247191572860989588620032*y^4 - 12352458148113159878859635835659524625287213935130436557427262469155918661743335016297840284841089368584372124665518927357000406367024284603225525269503470595420374315586847135934226951107975562248494523666652596380906785321554767926993503927489863732037221/160352350796007940593822554728445824997768838967664839751429317222699061005434320046611170043064666546866274882548808739091343390104002062433141556265823508401788273619079556309305772754547664769251786984990080936308934195101217701260980669026498580266368*y^3 - 27788212421188351473216834341031306143582399385188498291763390674569781874960444529253222176431530297558048689919253703098028780034182644722780962100637442774751642062671943605162881248781330212292752090244216594563417542764092616310761089489610268470325/4593426715510644131593875265658604361915253199594565722046152316275233518384837293001882475191956593790440165906346083671887440862354225746782700830531402584426226588046549790110321615364646647035858481340861693488016344130503632067371842081488240580547*y^2 + 25738126459844464084183565620975232060808238811227857073302687104213552841769900891515974282609391510698462314237506766062306334945576342018990239474333112801662250538954048128829606367651089140654191303431406367213536422789475724208030613159873089205481/5249630532012164721821571732181262127903146513822360825195602647171695449582671192002151400219378964331931618178681238482157075271261972282037372377750174382201401814910342617268938988988167596612409692960984792557732964720575579505567819521700846377768*y + 374212829975821455211155409000749522870719392548773741390253921965292735164229948372103772803476834009111391250791521049394017938488129868574792634992015379051730212068517801981848663884661436979120853543100668293419843238747065312604168947571134456548993/55121120586127729579126503187903252342983038395134788664553827795302802220618047516022589702303479125485281990876153004062649290348250708961392409966376831013114719056558597481323859384375759764430301776090340321856196129566043584808462104977858886966564 # 3 Loop Invariant 350815515892105798396587544197793548875773765000135407492008997526207635899500967339605430303007776635273480888293164229481655313927882575766122444125598349709277311079185653200255209732566354048528779654939043474838733852718433252136159909246207741337185551077736285787336188369708869253125462562646798176780425/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^33 + 215797409161857082237058133515625272239372824625455720719184201764553679703128494645912134114522594145890586897046389197169724177611085658698974151521959269448510195603457292861966163981057405418462210208145136772366298337022656437348350517916401958645644327648961193268497876317022291075268008754325756384079609/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^32 - 20650599497012885576125281738493631569701594847606635055959315875857526645630465482712536910863438205540886972983869761584411989932848950831888425880766533506713076939410883785268621166211509043535249417556522877486394538089604985032589051479375927568484419544201112531502681695271111269861564015320820978804971991/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^31 - 28783201388635767492976571018507253969447893959790748852407023460210307845484369815017596536674548709984087218494857760520712060981754583795674477917682256148236796738047824623551004899217549913657081592241681765248130522658383805836380671257746663319408797315607376840046187690576074641061083194095255083809060359/7475232348967190009612290648885497743474333910707625134343625718500843272036821650346141350019001186468635631866098380745718186434190428075972385950566297130125282106646749179924642905555153584250953124880370034805018746373806656191911452592975640561312311081770714345376052951789650786456770827695085729334381424128*y^30 + 105272740542420418985971744459765937545508899083256765355973868945145516488483731747824844377268953851303457429224089763847835987146675356956606379444335861603245011388680417178025430848875631209657325071901786081728748749676716117736152003380606607854291041692520681634865033011216120461937415348580004188024635659/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^29 + 100805072168716422725812958611665561375413780349456876754720181670912852122205938783463941798381693044012327169221302771431806861430525074823066550366811217286514606497532647288716531653078115942498407109477191872881171001712349939361217961769561405728587780648415060036615284270118315654163605845907383172358991959/1067890335566741429944612949840785391924904844386803590620517959785834753148117378620877335717000169495519375980871197249388312347741489725138912278652328161446468872378107025703520415079307654892993303554338576400716963767686665170273064656139377223044615868824387763625150421684235826636681546813583675619197346304*y^28 - 3949580499241372073708432470709588069411617102394179885257930763095177497763256310026694409571404892091365842646357754331459332521566709361300744362799986588419502000948874409406690484548978442894137560663536428547306773124522447728233090688535498188642639327578025748167333404013413039281260459427054158927355437263/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^27 - 18139289858321041279404852725221376945666951686961157369188433948733734797148880430713037929684033911694228674425403812891002898061388898350825069568381886597449647327283413309256763646733853755081442848557157274530657739780329623939118241043173979791418817000449413541526602537331164387050180492367097921541722831935/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^26 + 17565520800275696408009513215686779676348166732336961285003480796017862893915961704008059170586076454586137514430655519518935907856207709106281796587984797297692668780230548237038967847584316460632710323278098822756781812540044944857873054964364187579022059003846251288524745865545643566940912345394831475044997665007/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^25 + 4736650321920444526893781734626314313130639407821858109647829350840419679078236072414385716588480760024886853466776654410990188790713740889175771287537427760706686519812134739463070507825090954482611864565855370347852672457422190189173736476118463955941256433345083563235810545589951147651997942099025756777515977887/533945167783370714972306474920392695962452422193401795310258979892917376574058689310438667858500084747759687990435598624694156173870744862569456139326164080723234436189053512851760207539653827446496651777169288200358481883843332585136532328069688611522307934412193881812575210842117913318340773406791837809598673152*y^24 + 6966830128245520420395963050250958489723098626036549028454793499948908995532343978762812481295587361995568756450131411613124828649903331240552165146368965159210580783202115123925166810388455324377570514304772502007408239591395566941352653620543878072594164972261783184895777853694915630255180006045888385939383939235/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^23 - 8716448547021791875498549309564615161598329236102373349227514065318642266025991304687089215687290074063407738042114976581156151880193535963762069669987362243383783228314420270601781971232809637317797404288296570695574140453641973806636947079989529719604570715036592587183535255350999661923833005667772333714121387741/194161879193952987262656899971051889440891789888509743749185083597424500572384977931068606494000030817367159269249308590797874972316634495479802232482241483899357976796019459218821893650783209980544237009879741163766720685033939121867829937479886767826293794331706866113663713033497423024851190329742486476217699328*y^22 - 103252307846423409642076764048570919059808160771202855213269824393782964258922894485566752805150417946506383748898980367343131174333270808010511850299239189754806728959522073510630874104771358083558535775563695345865732682187485364241777051725834019070633781048919161628478490422770414190700258799686090974753438052755/2135780671133482859889225899681570783849809688773607181241035919571669506296234757241754671434000338991038751961742394498776624695482979450277824557304656322892937744756214051407040830158615309785986607108677152801433927535373330340546129312278754446089231737648775527250300843368471653273363093627167351238394692608*y^21 + 689738987623103268868700310899708580869026223638237141891840595890211087917171087432632580444751058057887542504839398768870328012405713731230839405314753917731753637732500475271961047379429708338743511996343336492918621285579628516720802321113782468951501557894951923240931002258334476700740060972345212428943695547135/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^20 + 3386905419090041523784029368969448834829179110958423123531747042723532500534585705258394216188503708270380895438778846273401303529379127802269395825330686603302473739558499927517094142040888607917476560160273028395216980935674230642728898375427396921116863025496027866998495175135105309155820793533740298344981896118867/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^19 - 10110943184435458054890957902325475030802035223997007614036685258096060544100692635066037718560502473172279270459410483858435405231419588779185629350286598387094647136851994854404105201801808619505235971196454430856289552945673179887370207530769280677975763118821396980016351221975102487320525590678237196207810245813289/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^18 - 24236538790354595336739844011803168843542785331654089451713209386365733152388104295796290354560058131995308502199475020887056770334873574831464229487735058518542696246268486122751124594965979307028560548796697078362603166958209942409698785630383288771123882984509501712832515619354694408375591522520651180126805323211/42472911073677215963706196868667600815195079038111506445134237036936609500209213922421257670562506741299066090148286254237035150194263795886206738355490324602984557424129256704117289236108827183244051845911193379573970149851174182908587798823725230462001767510060876962363937226077561286686197884631168916672621728*y^17 + 2532500891078969814067918277237596183386937601347536479640186817434534342967115823712469462183499222084020587844700031949918884076527305882245797611467341660248901410182659043246641914995168216755389141733212409670638043552984141623767551120995645291778966833723429523608194478619401928696624856297030197441427716437017/1359133154357670910838598299797363226086242529219568206244295585181971504006694845517480245458000215721570114884745160135585124806216441468358615627375690387295505837572136214531753255555482469863809659069158188146367044795237573853074809562359207374784056560321948062795645991234481961173958332308197405333523895296*y^16 + 16238933708023297862145088372080162537066437901427877967598758166351865634984209009790867297189657180995947936337208109820799916644532270247715854346212605266060334549974547992494585606159073657988624620327523706891291720175308795891213640358863714661214511883437641314149859918543121834457756290069556699620713875405/19069470277977525534725231247156881998659015078335778403937820710461334877644953189658523852089288740991417428229842808024791291923955173663194862118791574311544087006751911173277150269273350980232023277756046007155660067280119020897733297431060307554368140514721210064734828958647068332797884764528279921771381184*y^15 - 50779035434745785487668889358121677517528312247750164407060077888657172442976352750578775660624853348200186935986638092483518240812768849726210179650678107613881606179322410263101093093344190398561072178862796244280822314192216488868549912967988648255384540647761237464477643426522751131764096614898601625259248991640437/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^14 - 1498927913564664392745250655650004090065123119559692395693856227004373214603755092712723328171813498048309633485117844663393700620076716048138371743693838568160178252280383826729761985212950863324303512081352999842758096468632265637217802004002303372154391991616185446306627909800103038218859303475150693164903513688201/2135780671133482859889225899681570783849809688773607181241035919571669506296234757241754671434000338991038751961742394498776624695482979450277824557304656322892937744756214051407040830158615309785986607108677152801433927535373330340546129312278754446089231737648775527250300843368471653273363093627167351238394692608*y^13 + 57012330460928109382748863943330223505028808469533000574345393814151273292390004344568777362468119990458504409108596583165447380020081711609358043756323527626823157617041681306816206961738742121618175159461506416513901594605406258128304811632532442773466595876853071969670204181694440814361230633640406815488413575979031/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^12 + 749401170360406444937299018119955357193830096850701980291626698968977139670907627304556450210256917520584170293786649790499588063571895133670825429932509484913415147167169310459366378931553989248441356278242395064977312835724792865418756468319911561478471050470495265165784716485342045345528730432161024019273250156165/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^11 - 4663290046427838817854897744353139133090416470107421457864677656179673881966582327624197668290852511775782577940842743446366514116792219521987651904417941756648341321433470298997590655758931769712888699415470932483916300879320675265407295518883934701252821988154638117152885742689951212959108529019877994851170573224071/1868808087241797502403072662221374435868583477676906283585906429625210818009205412586535337504750296617158907966524595186429546608547607018993096487641574282531320526661687294981160726388788396062738281220092508701254686593451664047977863148243910140328077770442678586344013237947412696614192706923771432333595356032*y^10 + 718940421487385826182172921338123849171553750852991054795410186686510903334153488223761238404873853385198018574553713735891718833808744871175247095235241274769558718525505763037185557423229094983790211038582217087892453641319409933094915061872087587451484095975999467048691294571723076767632987197549937094242868926927/7475232348967190009612290648885497743474333910707625134343625718500843272036821650346141350019001186468635631866098380745718186434190428075972385950566297130125282106646749179924642905555153584250953124880370034805018746373806656191911452592975640561312311081770714345376052951789650786456770827695085729334381424128*y^9 + 2097890696109474476431302745654404969618423058085628510264981139700513429813791454700931176906658596385272176557882068653033431505852444265870916894769936238979097360164585192873961334373805535362611226033256983012626900714486427954775195462540936823815059426220190537592944382900292055879839041739815051402221493187399/2135780671133482859889225899681570783849809688773607181241035919571669506296234757241754671434000338991038751961742394498776624695482979450277824557304656322892937744756214051407040830158615309785986607108677152801433927535373330340546129312278754446089231737648775527250300843368471653273363093627167351238394692608*y^8 - 94516068409982198313920879531051040826578316294770227819929346098822446616703976680338781498348826928556391588783171338833190352465350017743133486346954534005894321867288335524885345632195293774529081375385325928121299133214279357436428095411271256499546976372166498043484834102454240122912446016269846182975315108781/2135780671133482859889225899681570783849809688773607181241035919571669506296234757241754671434000338991038751961742394498776624695482979450277824557304656322892937744756214051407040830158615309785986607108677152801433927535373330340546129312278754446089231737648775527250300843368471653273363093627167351238394692608*y^7 - 153563866451716453426662128068839950164778224965874399227801449573384787597657272340236575033907207839616227463800998101154101590766849533650664598875307333038026165236548033703607691789065410238916301891081137402442531339702867472329301118351338512714156610040677008991646491511379023645320658698388995252815548114801/533945167783370714972306474920392695962452422193401795310258979892917376574058689310438667858500084747759687990435598624694156173870744862569456139326164080723234436189053512851760207539653827446496651777169288200358481883843332585136532328069688611522307934412193881812575210842117913318340773406791837809598673152*y^6 + 192433293650985156939699670987009939872448089270930651410895286032082489267741266463384969110101087879866840408012201882043208377528359227199023413538242263477307243593279763606216845602875650967377460219428834201570116330488713565113805763585941248766139578704457809109880122066100316883124995000742252212117120835331/7475232348967190009612290648885497743474333910707625134343625718500843272036821650346141350019001186468635631866098380745718186434190428075972385950566297130125282106646749179924642905555153584250953124880370034805018746373806656191911452592975640561312311081770714345376052951789650786456770827695085729334381424128*y^5 + 769904638890491628399266039223094953928046326343289695482721898904079451692763381751783870894360690290623421616171607619957313965799809218157970089408788601745099426736206376380693525199620272611094908162094898292420937498535776467671995792097507372715977932726526363908350345944154053010762145654454517072045369390217/14950464697934380019224581297770995486948667821415250268687251437001686544073643300692282700038002372937271263732196761491436372868380856151944771901132594260250564213293498359849285811110307168501906249760740069610037492747613312383822905185951281122624622163541428690752105903579301572913541655390171458668762848256*y^4 - 5932094459661920569237565027931009431339639760963627426457586924831202335203714542133671982050048384190137463909264426497640070498458744506769039762919420809981066563699391917674892979360010725352169697600609479736138387313629060184588978234987759972631055666652908621163730917508458313647248248338778988893178774565/679566577178835455419299149898681613043121264609784103122147792590985752003347422758740122729000107860785057442372580067792562403108220734179307813687845193647752918786068107265876627777741234931904829534579094073183522397618786926537404781179603687392028280160974031397822995617240980586979166154098702666761947648*y^3 - 11624870649754184446217707141530766576707243040938465748880032663085721626049581786462433232270214118310635564344095276640677726588109039034950295580045380070494332269627182373224834993462235313218421230869752092279724243156739766893605760381457937697384581912849066637238396444558248656677330192402027005242494990701/3737616174483595004806145324442748871737166955353812567171812859250421636018410825173070675009500593234317815933049190372859093217095214037986192975283148565062641053323374589962321452777576792125476562440185017402509373186903328095955726296487820280656155540885357172688026475894825393228385413847542864667190712064*y^2 + 550918624457924956305033676317468016040306167974973677029964944767280943965723886532282077910703374883430726493219122584163655178283232764779592616910716325420337528342585026882533389737470424822518180035239023515643077274533441731653132992169704711953415353809112599295924433309387854730994432020070913053866327163/934404043620898751201536331110687217934291738838453141792953214812605409004602706293267668752375148308579453983262297593214773304273803509496548243820787141265660263330843647490580363194394198031369140610046254350627343296725832023988931574121955070164038885221339293172006618973706348307096353461885716166797678016*y + 4427124080839333101619952179242841339400550724507084291865339983952682135700850449034182640459921366639763700288671042735261601515414974970190112066296401210746733362324359241328075480398282690054005209774799484586980885600266754676654117686822132704563368747430902082740784425011141046250355937874154012394217597/116800505452612343900192041388835902241786467354806642724119151851575676125575338286658458594046893538572431747907787199151846663034225438687068530477598392658207532916355455936322545399299274753921142576255781793828417912090729002998616446765244383770504860652667411646500827371713293538387044182735714520849709752 # 4 Loop Invariant -160807418438751472553181006697962998388654922341017718256855733903866245843810465983963646374614083205512496007045575050463999977863241895745678853960673386865426034248215983019499867442928576881725066099612521676437988792905561773193453260457084317093447335270951092844381621238348283827905852475216742484621162467173073467724289595663798234084755988438931358346055671644267049843166150430692470353216391812328037534028325763008931149/17754848943844523703879304046256759679884309044822175384582247541594969745800917475527059302820962961362052157078715550375785517421278507927875753838808024379217802342588882942770890124414901513081524174696725931710001568863207392870318409114365892515873535451028219879114509273167595762553031796274254838997394294717625422790210800577796492348007892723384858620817210382914194468811986313702332914399442297104977802426406893980932368629760*y^33 - 23956981412511787461856196299703215667422398127374852942182099886170206069000259741135982769511644496542749594365136351107045235071260296985891277112223609768045231600980040359831793926442032942868504269220224844733000712247046664298912842408039963825983325974346891912116960920728068128299758637957313576274074659448836289203946648187954619498486581615831295633878819631027395343517461496238929598445369819234551265881783484319510259/986380496880251316882183558125375537771350502490120854699013752310831652544495415307058850156720164520114008726595308354210306523404361551548652991044890243289877907921604607931716118023050084060084676372040329539444531603511521826128800506353660695326307525057123326617472737398199764586279544237458602166521905262090301266122822254322027352667105151299158812267622799050788581600665906316796273022191238728054322357022605221162909368320*y^32 + 16406056943525464881568643927856497871887818557040843456689292445722743689276167224819107387096077040941071719115713353998863772823736437234206264064198565436530844983924044838415642446234575349775596002021840382454083669433262525244096252025372252684373751671862766558317416909164969038642386581400513344295405671077121543037797786319029884394036383150910426436865601024132504331878603393152046055282553636444768036767842988664774598913/31070985651727916481788782080949329439797540828438806923018933197791197055151605582172353779936685182383591274887752213157624655487237388873782569217914042663631154099530545149849057717726077647892667305719270380492502745510612937523057215950140311902778687039299384788450391228043292584467805643479945968245440015755844489882868901011143861609013812265923502586430118170099840320420976048979082600199024019933711154246212064466631645102080*y^31 + 2013070156470975752858372867313831510264998647756981879798612063672195906784183672885881778638808555699278900829087446318631582722370450647675050701766784213216274889148499792516843753311461748368267793297755333106810636051350556201163974146988581640236153268643466390850254261503564229261106407158416911564516803738735560192096310720265335751285031667897770647057711505296642833218170741626371316044266986268836497915404806053007813289/1255393359665774403304597255795932502618082457714699269616926593850149375965721437663529445654007482116508738379303119723540390120696460156516467443148042127823480973718405864640365968392972834258289588109869510322929403859014664142345746098995568157688027759163611506604056211234072427655264874484038220939209697606296747065974501050955307539758133828926202124704247198791912740219029335312286165664607031108432773908937861190570975559680*y^30 - 81805493484502877534217853906287863206611141318641847348342717304799655996310908264740924492174217814426256910116760967706638983970865052412341762099300273041034751616358268425795451460339655115275808697695653715461518237684222408948633056861141300036402900111267656554837319147986189053626839072126231812741953729269805269552218173362808259686033016732186181030059467269415419334966147950753348862595998692162039806478175661640451206971/7767746412931979120447195520237332359949385207109701730754733299447799263787901395543088444984171295595897818721938053289406163871809347218445642304478510665907788524882636287462264429431519411973166826429817595123125686377653234380764303987535077975694671759824846197112597807010823146116951410869986492061360003938961122470717225252785965402253453066480875646607529542524960080105244012244770650049756004983427788561553016116657911275520*y^29 - 964511308565773525389590012488930267509169949819062893540636749787101853730229438821838052019808600811772339905302999849221984548773480460121945922105670840025984042925807904482339102888582772365994952455158455067330644454406169600304895718343938849043206068659636059485181279493167755561983911120116634319194972343308596768027524658785019808786895961406391423084411567604659121844577905956454162150919636623793834088926056586793029732345/24856788521382333185431025664759463551838032662751045538415146558232957644121284465737883023949348145906873019910201770526099724389789911099026055374331234130904923279624436119879246174180862118314133844575416304394002196408490350018445772760112249522222949631439507830760312982434634067574244514783956774596352012604675591906295120808915089287211049812738802069144094536079872256336780839183266080159219215946968923396969651573305316081664*y^28 + 582190144382891847889360583383100740924025679826860606697169636670252585982371832878035114198931156257809192864428148295566593979778261434432030467217443674402241288074717418293282971144511684212688583902896445749720957872411535795262134902417876968065681505082587834864162224445895266233824303521714564645100311856306234882857469319891856335499680283374885915511255731813562018418808007484502627305529865416153805194290008071633019410501/6214197130345583296357756416189865887959508165687761384603786639558239411030321116434470755987337036476718254977550442631524931097447477774756513843582808532726230819906109029969811543545215529578533461143854076098500549102122587504611443190028062380555737407859876957690078245608658516893561128695989193649088003151168897976573780202228772321802762453184700517286023634019968064084195209795816520039804803986742230849242412893326329020416*y^27 + 2768046459404041448350948413275924129995488715020871234129120474199757158153559640941452613919913735394690258666207751045613971573101400789134113367854606406582592647145482065582053334412622863121230385460911614783718285188537018688393354405066183321974106072028488117041676739087925363935642519731536897777599723636308511073188723507096614043712699141682818806589904629672102053036763911110066866742726221794323521731152950493094758644859/5649270118495984814870687651081696261781371059716146713276169672325672191845746469485882505443033669524289322706864038755931755543134070704324103494166189575205664381732826390881646857768377754162303146494412796453182317365565988640555857445480056709596124916236251779718252950553325924448691935178171994226443639228335361796885254729298883928911602230167909561169112394563607330985632008905287745490731639987947482590220375357569390018560*y^26 - 1544728380540967463376094240865804050412886256548713236743163859599093886686114899072863791396547516023091376460225010025843229401307408090682785809697895124627357101382804045548175297391063960215125367125285759480636024105970870595808439067649486029378605619230035190086965272306228350863358764393441419492404363116538654499634059277834098042289183405972694208073075224306382180088420305749067907596234084391232711292539870978176598662731/4438712235961130925969826011564189919971077261205543846145561885398742436450229368881764825705240740340513039269678887593946379355319626981968938459702006094804450585647220735692722531103725378270381043674181482927500392215801848217579602278591473128968383862757054969778627318291898940638257949068563709749348573679406355697552700144449123087001973180846214655204302595728548617202996578425583228599860574276244450606601723495233092157440*y^25 - 3969665089235710795820768255833674583379259298751027065729393899909850716756861876062073673615304918184751964752671927884589816354164526907585774138756046424484575076931616360674817743851135721542007262625047515833168986654348031259612106948635725175281442413683502653157190281583684944820090206575985244476172811602472159534105276761158992220146255195057091122815729347781100741801212229023643722674133420769820034724273132487429977785971/1129854023699196962974137530216339252356274211943229342655233934465134438369149293897176501088606733904857864541372807751186351108626814140864820698833237915041132876346565278176329371553675550832460629298882559290636463473113197728111171489096011341919224983247250355943650590110665184889738387035634398845288727845667072359377050945859776785782320446033581912233822478912721466197126401781057549098146327997589496518044075071513878003712*y^24 - 30716389699048609725856782407565186244889320565469304343740203823103619255819540409335386665373864380377092338081673179474806048837798042193137446898651202604986235454699306439416402770719239988856275213948970401528140834622612262092685584080319256772915244365097178613888722404137116704374489472997977909173730064283777086859941835735279288018890511377047979513779691345799169129057502566980530059988989873900487917890006763381913976863429/20713990434485277654525854720632886293198360552292537948679288798527464703434403721448235853291123454922394183258501475438416436991491592582521712811942695109087436066353696766566038478484051765261778203812846920328335163673741958348704810633426874601852458026199589858966927485362195056311870428986630645496960010503896326588579267340762574406009208177282335057620078780066560213613984032652721733466016013289140769497474709644421096734720*y^23 + 708056873811985352718547677097612321286019627656984862084486826526929856516254196059689408983171626641716035360022371075137772533493063043411451433560088019730367828317479060168794539345089608890103307608131677340929136138185502324726114600875034578657600759109635289794462786475927210699682819049756419676166574196601404331225215148320185996612502521257205101388019139269505762770534188865613901538677600225373203963944878336308454727539767/41427980868970555309051709441265772586396721104585075897358577597054929406868807442896471706582246909844788366517002950876832873982983185165043425623885390218174872132707393533132076956968103530523556407625693840656670327347483916697409621266853749203704916052399179717933854970724390112623740857973261290993920021007792653177158534681525148812018416354564670115240157560133120427227968065305443466932032026578281538994949419288842193469440*y^22 + 84552288356439089500811021558910254493831332256358128440321742526201834439671153463153520136700634915011969113214728653327314694146470693904658763771464236570548220924133678017880780282341054641610437200839379960017604069366354239550461711457147792216759822876597419563003844109721972602983434220837218086773953987294768989520740441357949248862429821939322108270013249306010523792432606626440717009327036591288463199013361962556079803468449/3766180078997323209913791767387797507854247373144097808850779781550448127897164312990588336962022446349526215137909359170621170362089380469549402329444126383470442921155217593921097905178918502774868764329608530968788211577043992427037238296986704473064083277490834519812168633702217282965794623452114662817629092818890241197923503152865922619274401486778606374112741596375738220657088005936858496993821093325298321726813583571712926679040*y^21 - 251332736302824328039845674989363162204224525928766434195769613998257639509269380472436086234034756204714808756199764034549750436536157192670509938949212647069342771660835125749875615719689312793413038360516558969391326426346942545393389543824477605078215453928062767643112808364809297776028989458889403546908734109483599484069576965447058289415289673070443456897553813132497388940095607751718730542635698763388611719140713789454636858885697/3766180078997323209913791767387797507854247373144097808850779781550448127897164312990588336962022446349526215137909359170621170362089380469549402329444126383470442921155217593921097905178918502774868764329608530968788211577043992427037238296986704473064083277490834519812168633702217282965794623452114662817629092818890241197923503152865922619274401486778606374112741596375738220657088005936858496993821093325298321726813583571712926679040*y^20 - 12759024399401264128390695973529944798965637611648697580626178835522883186989214890943790572153768601529640998542375414795705025189125245327656213231386057439727971809414603076842508999778394717130836982140865992744310321215246083823324381161866106321987579159306812614718531662675631435103201213825293446542133786507090693244730583837386152198486713246510414964746535395309797360757374147507147016862050441459644917309358500728081392254448109/124283942606911665927155128323797317759190163313755227692075732791164788220606422328689415119746740729534365099551008852630498621948949555495130276871656170654524616398122180599396230870904310591570669222877081521970010982042451750092228863800561247611114748157197539153801564912173170337871222573919783872981760063023377959531475604044575446436055249063694010345720472680399361281683904195916330400796096079734844616984848257866526580408320*y^19 + 29865676058937143348722169330794745883007562187819235698471566515882459426585584736110574883299671103531703348843777878769224369770918396269306752563552785703990484550840161433858991354028033937183954217800475360814016412058535825651213427129400677181704940469069136842321092189593239911514006550981856208398577152528027646606885956910141047735310642280122835305029284863395356349356112061496714215535502870774739166555979449905350390114395917/124283942606911665927155128323797317759190163313755227692075732791164788220606422328689415119746740729534365099551008852630498621948949555495130276871656170654524616398122180599396230870904310591570669222877081521970010982042451750092228863800561247611114748157197539153801564912173170337871222573919783872981760063023377959531475604044575446436055249063694010345720472680399361281683904195916330400796096079734844616984848257866526580408320*y^18 + 8562160356904285355881682342247337583262779041216653827341900175939883051700244391305103665533971125039971105861588929824786327818303142865457849771925910740406424430447425490387244144915716408946102843348172941039337922279611360713989813160404759004216601737381154357366819529984953148582844264631725527367780913285917530722304955619167750849545688454516994555757262338839898547258589304484456233291059323211292204650511070988266332634155883/31070985651727916481788782080949329439797540828438806923018933197791197055151605582172353779936685182383591274887752213157624655487237388873782569217914042663631154099530545149849057717726077647892667305719270380492502745510612937523057215950140311902778687039299384788450391228043292584467805643479945968245440015755844489882868901011143861609013812265923502586430118170099840320420976048979082600199024019933711154246212064466631645102080*y^17 - 3938585883600653161406302245415958203191029483119471478131593479984733857513565325309172280649978210009090675914246373272936918461776824448729300405112929336491972370991449541495435399141068883631180467097296826261035419441216005583881339695615853377062345747746614911203723096032189078482363212504435871041565321995013501001401370564201970727178274789192692667186359317444570180556386579680319479729172968645957840095598001168875772539581257/5918282981281507901293101348752253226628103014940725128194082513864989915266972491842353100940320987120684052359571850125261839140426169309291917946269341459739267447529627647590296708138300504360508058232241977236667189621069130956772803038121964171957845150342739959704836424389198587517677265424751612999131431572541807596736933525932164116002630907794952873605736794304731489603995437900777638133147432368325934142135631326977456209920*y^16 - 6643412204571835553305046179344016520867368151960345040494160652982332024842393843253382721477512834793669025782175543901190019204577081470952447604412221503887628904977110771020217697959060251048295704815598510706984593518264490586732388257302002641980892374616879675123270261497640822043537934093868526795037882788071869578544585751843132464522265489824055488254044454269890448055735602958001096950727557453199131861497597398404961804862207/13809326956323518436350569813755257528798907034861691965786192532351643135622935814298823902194082303281596122172334316958944291327661061721681141874628463406058290710902464511044025652322701176841185469208564613552223442449161305565803207088951249734568305350799726572644618323574796704207913619324420430331306673669264217725719511560508382937339472118188223371746719186711040142409322688435147822310677342192760512998316473096280731156480*y^15 + 76081391929057924810699189574673467882522283484368490297152827549828607379689815982829755503580387836945345791924303281248999895012373271230030187551214456040240156606457941815170520068116753119855300163814665566184641308933044796698030597880237706613891373952218139488424560119871679724123508129054936117762072353952048470028715480588347096671713620706564428364633255026242915584453922633746999741526806927905741475116921837362668998265197777/62141971303455832963577564161898658879595081656877613846037866395582394110303211164344707559873370364767182549775504426315249310974474777747565138435828085327262308199061090299698115435452155295785334611438540760985005491021225875046114431900280623805557374078598769576900782456086585168935611286959891936490880031511688979765737802022287723218027624531847005172860236340199680640841952097958165200398048039867422308492424128933263290204160*y^14 + 68180126039496693911272696255654965977173161519185986677670293719330819602926902181674316845932049201594638447637683474053796825867228659889097070805023594899324679464943421196974775949013261944777344496259102675531638600771579037988343579311720594725736436114253211347461307233666672089145347043948422961539920581113321329451313258605197381019405634585629378661520447388038336747377189966957140939069570388195807465678982554053558666454910081/124283942606911665927155128323797317759190163313755227692075732791164788220606422328689415119746740729534365099551008852630498621948949555495130276871656170654524616398122180599396230870904310591570669222877081521970010982042451750092228863800561247611114748157197539153801564912173170337871222573919783872981760063023377959531475604044575446436055249063694010345720472680399361281683904195916330400796096079734844616984848257866526580408320*y^13 - 17225261579631112973720080986426844982966191296598394419747797134553734608051400420511516164827882485268554358173572267837059461815562155126853304972041532038971095194326706421195300019210908678710779523301370015275500598365755844666467669425817991235403420720761766431659868459790804280822936384207042164729505351368676097828499295779886854349223688963036838037102497647236584705461314925038954032945100320011588933820299381739792903015319597/12428394260691166592715512832379731775919016331375522769207573279116478822060642232868941511974674072953436509955100885263049862194894955549513027687165617065452461639812218059939623087090431059157066922287708152197001098204245175009222886380056124761111474815719753915380156491217317033787122257391978387298176006302337795953147560404457544643605524906369401034572047268039936128168390419591633040079609607973484461698484825786652658040832*y^12 - 4383789852437765794387807887467885448618861648082212327974759358189415303345010522464568874751747149022688313087720458125480389660593689897309541207206550738221550347904743669975880309013461512339378410324644109635600303996769034738909156677659135997527422902319759366599951805595172871339327064969018019836666689357541413916790044597617496962416167101308430068574780733622450362946673077130191530258271589722166736281540165042875458272399073/11298540236991969629741375302163392523562742119432293426552339344651344383691492938971765010886067339048578645413728077511863511086268141408648206988332379150411328763465652781763293715536755508324606292988825592906364634731131977281111714890960113419192249832472503559436505901106651848897383870356343988452887278456670723593770509458597767857823204460335819122338224789127214661971264017810575490981463279975894965180440750715138780037120*y^11 + 16265240971287256413123207332786519539268051239177827028432955503758320035894037627284480955139057292702861451282828742575994343622845808110824261864466120870462587085151705006636020373622720128741826642797837050671939316621012931420256146894287825507720787611528527066458352156185265414338730176309132626289284321672545745308841460650241214645487726079352153387213359722448247605211287088095198744555939552098652564122963291306399890995073713/17754848943844523703879304046256759679884309044822175384582247541594969745800917475527059302820962961362052157078715550375785517421278507927875753838808024379217802342588882942770890124414901513081524174696725931710001568863207392870318409114365892515873535451028219879114509273167595762553031796274254838997394294717625422790210800577796492348007892723384858620817210382914194468811986313702332914399442297104977802426406893980932368629760*y^10 + 584128548386923071341705515056130269950408706444451827008374141113326428566598562688059314176001357429659686999557376734197368893702519611770233146036300218293000526270887220822576799021059050299806374759923857789664274284647966974742937368652075850290872809837997934186893950419528071709118357268833524369400866464511501611211470429720168949167806477210357983780889258756188546791167296269072563956128607237713347452478185992393685958162691/3550969788768904740775860809251351935976861808964435076916449508318993949160183495105411860564192592272410431415743110075157103484255701585575150767761604875843560468517776588554178024882980302616304834939345186342000313772641478574063681822873178503174707090205643975822901854633519152510606359254850967799478858943525084558042160115559298469601578544676971724163442076582838893762397262740466582879888459420995560485281378796186473725952*y^9 - 45632487915451687745623165543706944421731534189182438745851737498571661052723077009099600248549889291770024828234571504429361919113771531635410212637102335985974354560812835027461349615274412173036312685262906282622059790624701820508953713157131178960759445598568401504124290878335906110693879384517532516251883676067717041865939568581614484567306394160678773069934031037424969065928072702456227525718836629124646026516667083742841631810319081/124283942606911665927155128323797317759190163313755227692075732791164788220606422328689415119746740729534365099551008852630498621948949555495130276871656170654524616398122180599396230870904310591570669222877081521970010982042451750092228863800561247611114748157197539153801564912173170337871222573919783872981760063023377959531475604044575446436055249063694010345720472680399361281683904195916330400796096079734844616984848257866526580408320*y^8 - 7654983199434362948543794014575633105964192309053246933831885061046252471224235105752888176532035222762515735330606091608228148330901205904417519163535898950395094199390393253292200488557181093503981265868143613039149490045406166314703824566573339609571704201273111783330498812202239333620560010830641802166922927903706639837890884419239235564202226508354806203820518597794344068080734518124073227571647388452940228665482632046961914670116373/124283942606911665927155128323797317759190163313755227692075732791164788220606422328689415119746740729534365099551008852630498621948949555495130276871656170654524616398122180599396230870904310591570669222877081521970010982042451750092228863800561247611114748157197539153801564912173170337871222573919783872981760063023377959531475604044575446436055249063694010345720472680399361281683904195916330400796096079734844616984848257866526580408320*y^7 + 441591961180743351139333498322116728175394444071189659981140284369045011773611259082275404913362433295379591834799186295272099362900572724598765091900327703798681232971467909196849504752247342829378040187213417864897601245676875627633655422145643410845257727975820924300835900384488660985333419458015350893846351403361631395592727068465199364535704531514018894502677523467199823705065806693882141204321808748528144798712009806454115870665245/4142798086897055530905170944126577258639672110458507589735857759705492940686880744289647170658224690984478836651700295087683287398298318516504342562388539021817487213270739353313207695696810353052355640762569384065667032734748391669740962126685374920370491605239917971793385497072439011262374085797326129099392002100779265317715853468152514881201841635456467011524015756013312042722796806530544346693203202657828153899494941928884219346944*y^6 + 394344280787289849191187422212478887798605080300249839826442719523076607025854388357441952140766094661685893922521028537873722638288062056689520247002786177302106667278932986161458888170949098808853565731604494531388180531899022662588946385964485142672427401107178645134369563440876607103123158774222993397600153609687087270619797829596282536693393469653920688240972561785603292483342398406246883150880457735412647121001605453640285042315943/31070985651727916481788782080949329439797540828438806923018933197791197055151605582172353779936685182383591274887752213157624655487237388873782569217914042663631154099530545149849057717726077647892667305719270380492502745510612937523057215950140311902778687039299384788450391228043292584467805643479945968245440015755844489882868901011143861609013812265923502586430118170099840320420976048979082600199024019933711154246212064466631645102080*y^5 - 307574839578078335059251436061926153589960516910989034561747796005606809644712773718843983361279628184164399559829619673054952592525032460448660315330665070452120783079190294861310513417291144915766561729370462726134848874907760276654530842078783830094782333685410688315013038093924991295906147967796004849851538768159483064853286763300142185384423900928781925080399986493717756609791504417730538019544702903031135528271930697411448197854293/15535492825863958240894391040474664719898770414219403461509466598895598527575802791086176889968342591191795637443876106578812327743618694436891284608957021331815577049765272574924528858863038823946333652859635190246251372755306468761528607975070155951389343519649692394225195614021646292233902821739972984122720007877922244941434450505571930804506906132961751293215059085049920160210488024489541300099512009966855577123106032233315822551040*y^4 - 46572325932686028310815765341409460910811099941624654901375726036013015828364677658460660835516855916689467337652530753912985687374564445725233911125368533191431382659877894447748928978420250921395163977467907677971639820917977950904816885282907788515647526996491512316327683214827768509442676278382823002368798166179126013913213160177906437063848028124688687948708047412624720347244020699921798217747074735511493199289339443423324612067/88269845601499762732354494548151504090333922808064792394940151130088627997589788585716914147547401086317020667294750605561433680361469854755064117096346712112588505964575412357525732152630902408785986663975199944580973708836968572508685272585625886087439451816191434058097702352395717569510811487158937409788181862942740028076332105145295061389243784846373586893267381165056364546650500139145121023292681874811679415472193364962021719040*y^3 + 1166486177469612652508910828705429372961309874023518057485805808860888120488859822964165253672617984814362278629980436400330629108609780968787416674346718183271161801605208336809053793564805074888530591875902669039254082332508252365101817895208513312770080637193964087218051013936303358106770100999132197629333443320360372117305097384041417880758860758804431991455051400462907929024258623595440365496431661643563979482354012227828109919267/776774641293197912044719552023733235994938520710970173075473329944779926378790139554308844498417129559589781872193805328940616387180934721844564230447851066590778852488263628746226442943151941197316682642981759512312568637765323438076430398753507797569467175982484619711259780701082314611695141086998649206136000393896112247071722525278596540225345306648087564660752954252496008010524401224477065004975600498342778856155301611665791127552*y^2 + 4059317892069049652997858176864111666050669901136879782729706228496807739320182735735190477248710171314379121986395741245899727945832152285316413476621836119460343657700641897757069534160196838328717305430240651875819526909556405122102570437033610108354488675234831740539994121656182714962632488372900959005929265439286997295475552663105239864166854080094186770949759972987041503136206482897026500260176366082724585714153714601127527/15171379712757771719623428750463539765526142982636136192880338475483982937085744913170094619109709561710737927191285260330871413812127631286026645125934591144351149462661398998949735213733436351510091457870737490474854856206353973399930281225654449171278655780907902728735542591818013957259670724355442367307343757693283442325619580571847588676276275520470460247280331137744062656455554711415567675878429697233257399534283234602847482960*y - 3002204954648240357834704976594066065326262838145181460015500169862111715130740080369348803919644041823358966285471770168697888626288829150826402947885837024893394887178996639037427862353445515833214748629703112831224854238927513335653495340806017426641769995555459916078276290196552130975271828208428798244352750466480578496114603162530216993045964323765647085637596896797189211993265416534872704445377061583273217409639431753660944669/107885366846277487783988826669962949443741461209856968482704629158997211997054186049209561735891267994387469704471361851241752275997352044700633920895534870359830396178925503992531450408771102944071761478191911043376745644134072699732837555382431638551314885553122863848786080652928099251624325150972034611963333388041126700982183684066471741697964625923345495091771243646180001112572833503399592361802166735880941507799347446064693212160