# Manifold: Census Knot K8_73

# Number of Tetrahedra: 8

# Number Field
x^32 - 8*x^31 - 148*x^30 + 256*x^29 + 5712*x^28 + 928*x^27 - 87879*x^26 - 90511*x^25 + 674151*x^24 + 1061823*x^23 - 3049199*x^22 - 6648879*x^21 + 7923172*x^20 + 26235649*x^19 - 7143442*x^18 - 66341005*x^17 - 23105459*x^16 + 101158776*x^15 + 89914427*x^14 - 74718831*x^13 - 130840580*x^12 - 3868550*x^11 + 84822984*x^10 + 36683772*x^9 - 21298647*x^8 - 17457051*x^7 + 368646*x^6 + 3010585*x^5 + 536489*x^4 - 263569*x^3 - 20779*x^2 + 4386*x - 95 

# Approximate Field Generator
-0.327346342350555 + 0.385275809944998*I

# Shape Parameters
-102702147801725433161206603876066563728177259135862732252564419130602451478676317737127827890703020177844527445198343729/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^31 + 827322791981538322448676289397169124566755390465662723931852740735772018820530568532065525449622986615121711342387365776/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^30 + 15175695495381564892352127302699658247436964014882432059531316567327444286792585548436388084789493400049178800541171368066/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^29 - 27304810617502574135402821816051057035032334012135929775036470031555947587130748901716791443756032797792088513862352811206/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^28 - 588348178126068541757735346354563538146624805550813201519675488473931065791518715367146467270387805182402719003841871947951/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^27 - 57800204813050868220005956137738988106392891804200086380831088699719049723871824308511595773904860916094098394792973076286/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^26 + 9151129416400282288192811251404410298471462293568569192117919900476326849381688772060776863242096236040630661413988257519536/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^25 + 8836373147876997521035849786382848830109228657681335354586385429489879224405447674042799480616882756086708542532732903419863/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^24 - 71534093735420556744857485871899196337008986318278178300276276818361800184769306331317407247008940132314417431853577720390536/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^23 - 107438164620628501796043015031504415338148884198943731283361430061660277893530809353744694454215643431286162747659271413828844/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^22 + 331878514229428772147965549118407618046648965434359468198783624528289343119339336474873621646726392571404824536962103105793394/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^21 + 689506626968437118788294977272140070167435136497975239620034808589177692272571287065862942813657537826278715285893809936591654/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^20 - 901976932820710225610950244738839834332494638939137265421436067744856190473165963984430395021200629051822006919471233788882706/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^19 - 2789970630004055587522280332764688640433139296889337523424448276931251884522256998543274503195747325391276180113494818013654140/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^18 + 976938096401783918440057695132885729302930272103214017723746856097769110980914348527960068856050540476409234529723599436619577/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^17 + 7284050089576777655411847644418359275516953228345224396932300259835263996495457226109776688363595747159369507239821740315121038/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^16 + 2085750001787929072475253339428999400580527075545923493025161953903682817817160057172102656677161668872574310037700977906295972/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^15 - 11654322904089858754632248921944014257393801626780128988153122010600506946783025379942403033593558853814438963326201215387769923/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^14 - 9615667232403647496223427456317077647562712165497460985592347697642189573020195755571581812274540139269335492194882459466111207/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^13 + 9472265181678625309923695223817851253473008357644245749785105142803911873269444821659477403238998118825681677923403202262759967/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^12 + 15286181778518960495156493374666427017127682427419239477626342798977400473591343140727437863068113817126122405672769222136466249/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^11 - 397334753753404353834909730805529331706126973273839746169350031431801619367397140303134616527071426658271185280451058099574662/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^10 - 11105815449870455119251470466291447448858925073473077398095914007994875726522974955251424234121633682059008237821402993853583735/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^9 - 4780524761955686950609031044105567718453159547427426614152845560604690653717180033844665138133513472596369632192079397305479950/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^8 + 3061601905856617800438642502989446804756351797992453500239553632713344580091106669026691854435771967534868558837513440503382799/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^7 + 2827566921213416108772169058747213763506967849739667788007107651768775807771295549499908301223437845099153859364753946354014960/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^6 + 197811622856144373943787199135475490059539637600290617537607392329799665243095896014905303245430070051431007323180027031604270/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^5 - 485348166251667639403042945590364941196604148583396299307140339746788681975312027398886624675796167220737452488419198583613411/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^4 - 183863279088051533803933525261377555840665010649790241400251979666519432059598800911647482561009807541871552379173675185645027/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^3 - 1977420445807304778759839854334389029028179916974693876375480248917395316864290873758307068942390899670854218538696467404078/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^2 + 3338164087194884490682001855112903818448424640475463137719423985495058800019339786818300224477513520444498287135554552039124/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y + 4546069723333266285937118177500952605205312168585782893170659389654126115327604660383875428947964325438190913741665555447385/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339

-1054909034478136479454851516343439631149517231837884759100137146286321313189079509546716438791831128567363475606307885792791/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^31 + 8125025088595216933314364412756368579281002322592558100307494783788418614418212081632387624984619080012171924609737231820358/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^30 + 158545418115695770683820225633121214301966094468263558124027063208251180238448177020697444036629612733356813783846897153827278/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^29 - 222816867537190196586773651939298589993568065341350844052342581191007654587507715728685661436287168221224251364373288040089761/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^28 - 6091786999200270509306495402428487210653180751383173756042417153761111234764086932964184510712480670598102688792323715860187162/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^27 - 2793838674489386431191728291242219268350285062423143105802571782455496184323756422345949027482558434650158569510307294033756038/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^26 + 91863441870267398242703431058826075421908476291401445353001637124909566570695547617386441444574320310453306889800180323648200904/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^25 + 122837822568755564354757749635777976994275710493884846467131854364141508796373247984808284198686146269097193475883819253449449956/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^24 - 674451500283238628582003935228729593865572808657672416807300448579773311522039341523452635827268017038935970170463796641704231346/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^23 - 1320804721245915485015641332091971806953200062418654395052009501022407491165041591129327060085981470734214216859597581202569915463/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^22 + 2822354022265981691833997962202649523289861673072624289081349667885934611398626314626544347252553243161817051152793145677363056399/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^21 + 7852464126506400216113277500071543601397950692478271446920493947339436442831745263732206222628387369704477091360041101015468499044/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^20 - 6016305509081752830309144853316668648254153826200490316035336063458133144565444634321109951741534142848398293709870037960790080047/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^19 - 29456184469347186916578644683950234873787314541934027764999738047210839150539268342393489663926171927653027652696803103332268426074/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^18 - 1240948389601677352072190344284748248060497751535015035653896561757436668531717674245946236961449701536588263406546610626847221633/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^17 + 13914549170620489562805674283087498666072706710593262739141645230778444630131047176333953216984269169495119400233927084533508376044/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695*y^16 + 45075799207177519549429511245522342993928145713452465096887977406818055362204664425000679305485460631709310968080965469857336196869/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^15 - 93203561402763809715346567626690422763338373492985640477391938804284889034882276267671163716779261728390278270976046515677051433336/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^14 - 122511132665809128429120073953914625369974883906094445179931024359910917579444999104116074747569645745087621527654394544881860390377/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^13 + 42257624033090424621213451193311468016310920979345560013679834242074033501884724894679840954007180886430625162865482137723002547381/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^12 + 6016442437014953461479126848732618445001684595927823295199890751148552312203564527046978623624601724980649836239345737354620023091/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^11 + 1953297540496676502812627249856800975069011145961612117700070788652588026932490452554813933588830959197901264282442427802853266554/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^10 - 74763944781191762689994162579262910228281873729602981636400340541663688288726825570445841265810455898680033368301209585672496456944/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^9 - 60809515115368375592279348163323518134472870769821344772870365802265111155508093337501402807289731513761536618596438402642685937857/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^8 + 4345701007187396653302377049784165977398934521422033894481507823177662760706204200085652529062685157524695038325903188896276622562/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^7 + 19625870296442165642148594348648661037455185806992586593564110518204144280722940609042257471114667573647984770785685609144131157231/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^6 + 5414301599154814955671302718434771477250923077003674341534251478857289097347715229815927248181545821076102486085979819121806751084/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^5 - 312568968169984275339283938405615753112136275889704411669914261692241536727507515536780533395047019505423960731585122635511861826/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695*y^4 - 1024388214951910234541713845966913016942592186733721187364077475478643374612537108126199483113279350851752581289884574215924129699/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^3 - 24954497175580342773502158152697139023815322165962465574096653766720760084108297844296576033929307363550001424680995150688224301/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^2 + 14525798755120251416629349672738605472494556125176743988551946270077387918296545503110217269646304282317722751998635386592673469/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y - 228277822578142846660780088120376093602460275457098870393883640854759496712103785074996725964571244265643135998899767030871196/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475

62984382078115720665524046084595851360973977146824357716696701315461408436000980113325343340670895244656172167902726023282/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^31 - 205922231076427826774447917430699939579217903151620276950838169335666177282434540890768252874515367323395851688839446327109/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^30 - 11758787237958868023002655111024316364231885381241200354505961468209445000047165804658842405280845106830654579116998178809278/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^29 - 27413163781279595024641665261000048555139851978160623215879110357641920387273782847400091395587266869986449898430189927925477/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^28 + 442858984131232550798086715995477820578257831355058185250794313753658650528469763881699506771602659797712814197890031966551851/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^27 + 1727476643638923975672461863350782481982525208687523051506084909444015498571476735026295273536695993723241830174377757435529602/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^26 - 5524059552147355191984710814964558442383587583482077985414492186831860982746411041305224207751322685992411445852791679814791889/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^25 - 31193906443556625450394820620475910086779585335326629494513551526287767733958277065492019860431135808051752963208011012972521045/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^24 + 20074289837661118090023568067120080574759039995078887945601190280883985386138207128038671602033907870332236381617572625623254792/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^23 + 261073923670451598639914431719079085825424784151887416301093139725542167051334843015208775735642557089987469094343410752756273032/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^22 + 80242963864149098295702346522589798465657298925540888403315553593454850802943344700772044053196763783408957292490700339324676405/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^21 - 1293413168967107258731707605598178936935495459758031647932175491445095348121491312431856025319532940207863111873397616794032682387/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^20 - 1212096607267264352491710237619735055428543410729372013353802389229903918714497069328975645771210231705565675389035116704870143909/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^19 + 3938422229746881709271001646253193885528066147684544274101091071369628457428221688233326277077273021061167762728738266481751248269/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^18 + 6240650220938126902958983953189058345771807447438304527068454707670134287936474885272385498299840264580915381232971847705053813569/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^17 - 6461114144621503975530810642080336283424147938900097915856809676867003912147273438497370886488106646225085236819331648634272270041/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^16 - 579790760517847335871750064369542748579238465896205934940347501892108843410842651838245093749635848874764190999793996661987492085/162418362702600107112914601693708914311747872655350558911596926255176200190434165850310136916861803106719613430556677107865509*y^15 + 1179701559354472685536408276615303876804052690942247983191879369366309753451345134551836982784913644473621640173814310487190874074/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^14 + 29560343880007976379074048840111327289789991128458382535053111566478034701667835737817819055621691582053635576567644255905895340288/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^13 + 16312503169062994612779163090168576928638983525953145096266687253201647193383310840365343589361006606941539861779446958570064550835/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^12 - 23380506943816733917990824994444977570316258065811173895341953526072669178120484434707700745257109146342613224530866837170797880444/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^11 - 919737531971188775013064429281190489823306064581751910188851036887979043905082565382457858202590413016363208243773491534990509465/162418362702600107112914601693708914311747872655350558911596926255176200190434165850310136916861803106719613430556677107865509*y^10 + 1196755866626581585265992983997131990878336067384171779119775080861321108683307945405332258338770686480330588418716589161841042654/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^9 + 16611088321990529247439376977604405034204869213645234662719660777217096793802763024865756466601889356909336444330489597920676125038/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^8 + 7087348883752781433167134709588898552053134607665789610097948474735461786031513775399429373746729341927946805462825762439056168636/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^7 - 2191033732498312101022761269906500295560503023362468969397872321241628343609890626248076890747592222495869047498245722853262336807/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^6 - 2210586779069746053270362987100662284549815706104529150342170694343240367285373155689625186371453531450529871456488701344710815593/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^5 - 437924345965387959485135598621337648333883157123880282434131942133131422312790512042517646437813415162974886359575906360092162489/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^4 + 119750721877618424852276551910275823744956021440956468313851612350897043847786435834195980793769118296263931133331367657082781488/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^3 + 6838166467585888982622075086872801896926728882941767681322022828072666712048787821172300900788795046554429408105828188707174246/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y^2 + 1647725625773214270310601854845946413095810830892606356239112093557748157157840126317715328502267528834385445929401970611002596/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779*y + 3649598886198145958368630070296452011697784168265104279560471053869590587624917832299432144875182879948259953704422494395339915/5034969243780603320500352652504976343664184052315867326259504713910462205903459141359614244422715896308308016347256990343830779

-14428983340046301806686062901885143674968988000294158631097406370908014027010202204446888077475996108573148418454477353406/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^31 + 112300620927242757963056549598781675878452571132074127242414106150255007009233145797973986692829856924372821083516836141867/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^30 + 432029322482099408224438372810976955178323863189514911821243950573090270453604216490681922927987850448295601956941917113041/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695*y^29 - 3227475513449832526377437656861002827551077115876258952908602499985137045228780112579544659045838300024228204352096213309081/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^28 - 83159955757448664711778448219505097552179840336001133311864649983838200476132477944331555990544903899890487351656967899066778/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^27 - 31343832907600803777365719998244341130927430887871743274169896934660065260758931930831283320328600512482710671782950037985171/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^26 + 1262788334902690697411276009027725541159742285159825550770500553172098548964504651071574856951861408458332331118352353450520103/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^25 + 1579533274062573756093208129808828188587841811259674566219019749416662756817023400352897211254995455204256125224555634217652994/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^24 - 9409216321488127461993872940215037403404607568872044046880996994216769942517818881547860024025812927229143634161609355389682237/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^23 - 695076622803905889556115833427842153024173044375206457047903949843725313477877893373847739526131953777897962859420015249651742/5239302022664519584287567796571255300378963634043566416503126653392780651304327930655165706995542035700632691308279906705339*y^22 + 40421276379816727179293455887125066799446193247997222274667672189366108492372544033238067551401937442655448986194942819799241144/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^21 + 104914103400356696674889246636552338791721558205642306197362015681787912817764745066919846013172217939879777732242139837150367293/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^20 - 92489923068087565683445846049727893354166851289099447766005546814345839181637627593159241928321485554360938414633771944746314639/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^19 - 400026765666384098557339220269447645746801390637491397498669725029664172976481043146459828440912130773549220874499332397316515908/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^18 + 19003897556180094399310194335282574324509044687552520125933314186629239991887171586421967915087320051895323887291748139608076644/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^17 + 967203750392840001108371134859707730718346127273262981259099924446040290686434954178745269835300070451740293956556685093888060974/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^16 + 539106679558377683089503106282902903489702198112775619208584780157847995237392162329645930430527207216051960222518349956056064128/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^15 - 1358141915827056790990147299227711773349186377004361765866403677896331345614661220010888190545482280761204270910721198896609002828/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^14 - 318528342408550945576595298671398830433972943892803700309682910014849603780331560825009119393413959420142223725587022266961817428/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695*y^13 + 757541489917537944081315607517798180662058336007413847887274197515186179391577781507983875791273290859436326672779898870548323996/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^12 + 2067135916051809010040345698858598259905954367571100644288008479579532128483896323736777043845397553744376854262193295113490438651/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^11 + 483683724562585834574006548480965173793761916446650036543686471096873296496843045235749250059580933494094843753211714252076770101/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^10 - 1144850959800771552139961800742093185843498502642494082203026033353474776975695885824375316990347178378604101071560866321995240203/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^9 - 155084635574325259219019919185616298811781390670596616865515566710573157236793143843030832406022250787035948763216291495852231052/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695*y^8 + 156793973565057080150373888764587529381113850492646915236044061438716072330263668395373058508339741477523313399131955164996009922/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^7 + 293408294676581120709210344983596584382271455436769090013251855884017831638591045406714240348399624906991896019393565130821422403/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^6 + 54613374115113610800981344190782363912184182789575990878137383696749655278423718698177806249564800492898522919226502000516800002/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^5 - 35801740599934831547593118999312353334670615319652026621333943886844731384557359858866241438599572463400944246784907153460049433/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^4 - 16449001539939930834780065446127012607509966881673044298416005858673399768939695390522522905237800910293177853360985626433882042/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^3 + 1028159389957784243681665324479658046468455573978701805213414492001302544663850228104464235832883007365575501874608824212299322/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y^2 + 958012735477906352183807595529629131252149936297838926814561866222292142579572598385641150958579524141736468006695133121556196/130982550566612989607189194914281382509474090851089160412578166334819516282608198266379142674888550892515817282706997667633475*y + 25015684804468046697698316065944061803619214414975566060861481713520093343033715158921025016996627997398601216395172040093006/26196510113322597921437838982856276501894818170217832082515633266963903256521639653275828534977710178503163456541399533526695

-27060441765525796413626272691661435893002713669160771236954130001430113800078814169029581513931138815556591429447022134436541373182/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^31 + 526226479248123468534164089529035404666299224336476416314912650802363355486372552459024284237872960342455862174859062653264960419859/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^30 + 308568104547572972132732780064240723862873971208555656766457098580704315769085269926397577053800843258834905959697496056681713985459/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^29 - 52871437469472414490401225351020423974715341197562480237618571047610394537174159952842430914371826553601830553894117886917436622724567/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^28 - 77817671241712869860654762120530370827269028748637668558100358446645186635114584108146616193668343954905657620258460443527955785911266/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^27 + 1744562623316940304503559310102129856755858378634217931504472448161203209490758410394895554256743248761455540553677301884052929693053798/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^26 + 2762262873411653277699603928403107363322336705208237502048118398582577675371755072998220298254483220576715809936256671005430992877451586/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^25 - 24617461092314114403612538630131567592411536676217714407007043738978799289996290165395317930071052950479797185789822282950374667209393852/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^24 - 47646020709879272659943735501401241959062465811083314542724814917263217845758304951251412084148710325269162459361033931799297502656018239/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^23 + 35313160641203995410145683607885159165637329599346659153611059346571328788854185807243209386993176962005819065192513997437003096576550663/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^22 + 419879327778220514767316270320636569994977829969687576343901256888065315336621151026868601519086895332692330154569349843389193477198316248/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^21 - 732383604705245911604882198846507202589401740114729366867461530157545722714569498066421624787201280489276790383720933321902562226800960759/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^20 - 2297084433604502078380666616047470793989555363740903260713574033230273836832510474532951668351803121431860438937367079176298237271042236588/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^19 + 1573388801446874412257169334950099722960126799822421141594894576522959516776707819465950757423046889726085659510412800901202104924998298589/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^18 + 8293451264275626962824165777806792207264297131064158904345989078173052334282256174445568217195777024255563263130553040925724044230662958808/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^17 + 149411068807726035985873018221784409555800856886663620273126793073679399099002834160118147390228042469659864621040394494548188305193256373/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^16 - 19465076730424518369514220414597059080844847976853378171225298578429813671400299408199516083938297905880635763621686826945529076628365147109/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^15 - 11000498406919541567293789354657603584695322660629544354731286916847957905999369992028897975965492965112878792667837490177306439361446038056/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^14 + 5438620518517700789907565809022081403241805342360070465447093329117428674719126061210361799277061277313821384417318610729196595751184683483/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^13 + 30750099483124448975938031713629649002068170333051360498686033556386406567026030163685842595779264756380694430251103449527121011723204051197/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^12 - 8451720963647249585170202550218204305060873622302710477365211149743857361640354276027370567031000117121964656556903535987225563338331951/3020015497564912994856662728314815015289950056179857272761995899338291495681684736310274693924745164766732148649567317015700603468485*y^11 - 39506128625803954538535751609104526137699659048848597704505289840739845229336440801476508907783932258255221724680724418929376036917232091093/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^10 - 6303338862144235788992193596200857462077491196183715676782886356477393272801038166018381027341467618103738325212908769423430549711482123321/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^9 + 4551846255454956554192404562735449001706376975760397356481448780563435568240100506512308587755094181292394806161165910193305289748673779969/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^8 + 12382518147389103600165837506035304136904263320931223548209689889505571738797936683799696448935156542338281125964654627817444148355340371179/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^7 - 157298810835508894849610288347175959903939392239800184086356588042356933509090276528048716855888385636603604221030106815074454957568875186/202341038336849170655396402797092606024426653764050437275053725255665530210672877332788404492957926039371053959521010240051940432388495*y^6 - 4835839726741620334822550788879268891521621198765622466462183491879973535364958002111032206611357458473847846683343030705647483500301246441/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^5 - 170389536363923185020059941893012419899333432258936542516401139320702377526007438564214433162515246312669777115209325992383345831639788396/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^4 + 722507597140607493266048525246658491356535041179167896894316398628989087626794876895339527066943720299179567495162854083469428409767270526/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^3 + 145420368483795273838733712163765692056860523171542929891823392574097429559929908054875215923407396272822904576276965210642428023118095504/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^2 - 62830055521474233681073809294704981172345167751755640490879524701957826297971804770470954524188676145192382425285876905467892264013750978/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y + 247005333680561734391390578074385394696771447463383750637938553500307527754394137571972809369931054746634751857906022320959296028677217/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271

757285137563582034852217001426879830047505213795726737322852211452095716470798988670269052706063282688833817428306686036027264034108917/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^31 - 6041823757424208491033437757734447020364260576448214088211422821773814645957235545204171605378775286664314509409081632831139874458662156/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^30 - 112208332501755730370189662636230095734737690670007995631832771504201950137917747314622225530226166966241132372501321897051832129970636626/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^29 + 191418285984033416817589898255964855220691254960045657045575771692323457573607793862562899274751113853416365115179700869096631434483896927/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^28 + 4329590673162861947852516338916469652006638457741920017809436521364992778677703463261297793088855559284681745308315358941710533482619695434/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^27 + 796977311886684031286827352968804407629513095234804861291425438510131777159199249468268333194554821534830901847482839247039477432943089636/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^26 - 66525219110164194305393241700931418953347200576443015234740440859398878202311721611170476988124969744143189055724073278370053627858257187933/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^25 - 69980658337692547529985300496404736608817813653442495489696550801588192446425730023444077733844057825965473672193934776557214561945706256792/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^24 + 508904039820043159027770140323278342111861605765795081245015313487110832897047932853499123440273333577243040668323340655739874317582997393972/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^23 + 814957854913617784858769608087607226972087535730872920685196900943440934512533488761896664784204019398295589490116156233408422118489363609811/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^22 - 2290747504366207058013600154966898539451681953937882162873925686278384830790571047611084271500568961734769683610740114542057358972088454083148/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^21 - 267522606498791683474537689776759201652697379882215278407112032322066584352229079044541328328833552465413524776645130295695483260386890763387/5867890111768625949006495681115685574708372959157462680976558032414300376109513442650863730295779855141760564826109296961506272539266355*y^20 + 5887484425410537415898405315998528368874291782136000767204578177147389233528181096648079345054273735115160118055715168157054066083883483227704/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^19 + 19985172099007360248370174479050759335049924409153442131108245319441531694286507064147453687914624994864475327684995551944535809726499540177298/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^18 - 4974284460180730602099009004997419888662815949636224008377247456957114106077574771431196908882620760819597417258113427260173466621516589603209/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^17 - 10062175494528065157823298047215481303606057797662465317271316513344383925175982982872933712656981878297509095402754264866659943037719785043911/22297982424720778606224683588239605183891817244798358187710920523174341429216151082073282175123963449538690146339215328453723835649212149*y^16 - 18568955188262845215520810573580639051130949562257522537275650788813587110678186658780635214549078966631319990351946854706916933512559158720098/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^15 + 76128773379084740372222512255532836339616671514986011227978216193850880953663388156256757029483672421979827055230843141020309012819745399251022/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^14 + 69649914194378706435555451557409931220688070806643212754760441764165796866635101177710774889960898132204975856367954686828326722780547297891944/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^13 - 55003100861097385202760261027569579172673285013728758110280088293055474184365292046143323756719560173957545479481459994477685780382844630300202/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^12 - 10302677519813220284436314823401717163608504693328473717170928284220250933769705493929673717807038378542976574917688535371677189583408356254/11476058890746669380455318367596297058101810213483457636495584417485507683590401997979043836914031626113582164868355804659662293180243*y^11 - 1012905892935179638757593067542180738397894936655907165677104502403242437644745493091897218489059604710078034611804915142965956141091522507039/22297982424720778606224683588239605183891817244798358187710920523174341429216151082073282175123963449538690146339215328453723835649212149*y^10 + 63952151421765657026743142828568982866572409042691258955044396302301568923341493691109045293191807177715982313232000378243444951787457500285383/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^9 + 29024603993019910853238376347915614829970638529450559272277988637903321592316653806343751133334706836746638358866038159704032687466983121911749/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^8 - 15468367470699106824150578448046877838785663277223265662712699612670225296596148904628159021027256405639352008743806781454881474315273311470449/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^7 - 464207079135180401133316871571193442226640863047151552278031316988866606455892175754512369994025245811606464776366115166428939174554389287308/3844479728400134242452531653144759514464106421516958308226020779857645074002784669322979685366200594748050025230899194560986868215381405*y^6 + 23028211580178739792865184521784190844528462111164296185622875272267649833678228332420197515475072066315615984577674644300392147011659254152/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^5 + 453899732865754650410263345907623016481697257456786469732558083816608392135896015950956443442043725802055448946467281855091773954881988274176/22297982424720778606224683588239605183891817244798358187710920523174341429216151082073282175123963449538690146339215328453723835649212149*y^4 + 443186496171034115921653221908769860169347828945889324100299524380211222379813094385138942054349052402898485398278329392168046142858471782613/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^3 - 193051901695766036639204203984977274583121500987310497956291899337623817131274114249928790490092578445679552291796959570192010786870504065148/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y^2 - 19507829529389013541502037835267750614433056645879385824494852061792283874216007167275890927518011718597844254239013758834371742251837340668/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745*y + 3108383276569434126994720979411750615855177829357324525760529896584649309647557259082664211588911861935155896439818828061781924668052635552/111489912123603893031123417941198025919459086223991790938554602615871707146080755410366410875619817247693450731696076642268619178246060745

-49852611475323062602292877207412896962217559325149072219102904855086177261262081707972568996907135385105531147834629586402692431/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^31 + 404133916143817691331352323214819114322923400006891086594730574610820285898108893031194729527060770930296171902465657409307561878/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^30 + 7336159140092667887319040583744519735047169672781289274437729897616249516904737402720769996843875533684623385980496791397510205121/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^29 - 13551624930205025301880097173867192716198153589433592427804911369190012642415119782470155451987081147509848708703781004624695631075/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^28 - 283474738987884894953880484090451238501935832076641073764716755622848031289040495376622625781026513965169656270638590684418072885753/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^27 - 15910048206917861050829125105951441936297580239318012082963335799515267030570240125327586288723102869106951321444143211509245413700/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^26 + 4388835889654101002509867491328590725157405984526219992785648269467549661028472885372191683288979060393148640679762465779058824671369/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^25 + 4050228165126006584966520567430738646359934742144528221819508961776877630318405085971770812766366495305770687721998896559567763487573/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^24 - 34129602325867295457721069038185508831482816842762612717401865634313921723292513172670217033299032377176003319130555043499987984439851/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^23 - 49463606450634280612637583033705090030286314194245365320777436232911811729002243501331464999242775153772426348916196746350754395124944/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^22 + 157893588388351476350540617366142934784574396102852187176608657301633569817847767209475781322071671493202744065611360958255834544889224/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^21 + 316269089253265819856569390134780013136047200015223659552617548120722170920927777875925299493277534272025323109603421903971614762549516/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^20 - 430888817168097993216979651752320158203719050362518887383039795694105088074101779781354600155770492528464851183263759793196819929314761/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^19 - 1271115692501834171080770346367387082882641811936815658560470438033014182487226504911176556975692313119807246801081971442140934090853852/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^18 + 494002220048127540076902195747899886655045814975043396650057760936836237184234217305005064196126251972559319627621186088987480516742958/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^17 + 3286647874275386584139468191392860648568035768575695133583959602615377641897284981978304777750234202180761681535859916014245602994940184/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^16 + 815873957065967628050260877932904231921298163182006001622593420731853595081786790421237500181995761240317985696667675906934651902261248/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^15 - 5198467497019794981196799937155403364638269713678240626112436794617415820563423370756079757045712058413528511591662522911124557393377830/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^14 - 4002943240263316448637621924535268986463385008255998477987623963748246180992411552505606290687489626299557745459589289991665910664330022/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^13 + 4224153944406674414208720917915996082023108061633179946013418145805415088141372997379714991698936875017043278265941565152367684210707008/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^12 + 3207013853787508731683163929430804059763904118810996277223814228221864311222468937650713164884853194252803877475563727337468869747282/34678940088016455128399411245505138833208360293734366110834195318806815130983346573006541814603492734302487783769504702482638841*y^11 - 461608443457689304402498636248521234235898304497872889726200429046934946689080398082948001052918114322627968060648888406949376949948002/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^10 - 4340181957598473816991607522477717148226015297445761269967071584249127560573460812491104374745642366183024953991995933188786304241494984/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^9 - 1472356722334927877637416033032642230022815519229780599978329770622441217402000198194411491615898071946302715374726257681365810736294699/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^8 + 1267256935956021612391294724253364207482584230689620329389745815142919608582773523750866879022304714024052702201373559510515892536281044/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^7 + 28171657347339602715866172814363950567553626452179726429780364039425746314103050272269993843052897820451664353105577990478036243443574/2323488985897102493602760553448844301824960139680202529425891086360056613775884220391438301578434013198266681512556815066336802347*y^6 - 86536071310303875162012577172516441309339461487095613497112855496036082647241568617719652326837561170535279709490253174292697013609098/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^5 - 157449749880636184544316160780029516829721481525304725836364781543171207179856455279896832668834319416638724381446074190755966917935192/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^4 - 20219307266399467359669494379169995323054747841609993756103866700330750113312648330286189747792395066584629622710974595241746621071072/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^3 + 14756072035817751702111004705032447586442895743670247708491660081385669809620285605179375726660858336672926823043006469159000899617542/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y^2 + 640620251237458416638130483636325894293162705441848109336436686826121504223303224192056231472924436820463103531129549628818517004620/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063*y + 1415983503725521243167393131627445707326213079965858068129879739306647116628261193167698891155521928964635348377575393080413431057/67381180591015972314480056050016484752923844050725873353350841504441641799500642391351710745774586382749733763864147636923767268063

-550860651874414226628733940771793083852056004112256367994257816303903985624356110012849068619640522438992713737009623893150298078891/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^31 + 4466757083811324528680869665959239687837487841908082841129543926674923951390878414243570103837397397940809781925337466343554828045083/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^30 + 81039935135249238100656392834912666627353728891499070188361131064217835475154415132906530860367776709246065774841009274117283946062756/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^29 - 149806696584554056001810542856902488115562642624335026523226877177804120059044351267522656632993695301774264260402036784678584678649554/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^28 - 3129991279099136375443398219456161209126775474768847393278210308149957060711712916833581616459004652205033150882849251288364758432575876/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^27 - 172399846858336978171227774242127922464377756404571760961254518654771513495359033435239846736364274186143328058778008732977302690144767/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^26 + 48418013974724567459066109019747382283834544534111653014275699521410105778853095432255072851803516513017818481065990203991314403290857802/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^25 + 44628556680971107343279365921203396236709421096331721801807890722885218749390137604358644145529399466160749487756792474660421749707180378/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^24 - 376030033444185109407060308282379933928144750358838195981553215591924259410694305641738572945419290110685898250503742737981253408895074863/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^23 - 544371281950559022866453388533633874963138966423504959611376005131531729493099363385042593605995399322415512362698420465615634325528944802/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^22 + 1736906880017223695598549713305232917361575332066068842188365248862540428613434670286602489128869001384947117024014389316398285440927371221/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^21 + 3475335560481744201872227439890281075363305753380532599521160306854295882213462119724932476388207764768259527658565707335877837726528053728/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^20 - 4729614288466506049731241263379827318656615888331827784434781366006085533744073327894399694181024629931951510885522317267670207797068655606/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^19 - 13939602893417561845635119420530913207782960791561382903812527685831821720885498726173650058058290635902089786838008072381380700107465114095/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^18 + 5395383653123737075063916029625049814476766969405969486747979395450358250124128135368140722378243947214455093808468455803190551377887210668/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^17 + 35935442155655775289635162835974461826166532658213213512002635266884583895978635696055696739717317355630551968972581801095935841379649756577/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^16 + 8978713029693350828784998221200647914686426987981133987373811160641368796680881313458086763554661733486601111319392407139087503854250671022/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^15 - 56554470767436113681746540214533504224072530973604301169738257567223310070547156709131664200526162950527089212508516211445272154194570204144/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^14 - 43655709811917449061640894316695179307490363947479423594687942250895320012737989934416205209238778442381336879458487937123041250722926721805/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^13 + 45465284008352005323262394072427111076480663354953095017483314695285432938729606662152552108255887586734003438790488409528803486323685918220/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^12 + 34650670985693716258587347168662257308138492427905954360298007354285280111801398964190968500717289561555795829090408975889338117338505316/604003099512982598971332545662963003057990011235971454552399179867658299136336947262054938784949032953346429729913463403140120693697*y^11 - 4453746462542603748473164501808019442942285090414284444203051551774309861998223352923833218197148001257652474480424405436649979536114503868/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^10 - 46034323583996362146711778015584440429070758392572789313661522802617143210533644681979572436565951557864509962662756483817433154107841218629/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^9 - 15807995323190709646011868589778863481031704130973339208893934078466521825977577664263497955824583945236986286019728662605872164515008261786/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^8 + 12931911660067142043071081503243250196839375301131167802543197835069691665277330415807565914364965682098141930825702055122392267476599496952/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^7 + 286628831058380845271787574880761001274630033714579961374870661520543453642621912084233774655896894084847720284283342581387688300800306906/40468207667369834131079280559418521204885330752810087455010745051133106042134575466557680898591585207874210791904202048010388086477699*y^6 - 799755300011067292534027409264983904842208667330664837807253211110368756249672097056428200278885925198103624432054402693472338496210212403/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^5 - 1471421233733132253887583766748829622080928076435886160364590760701688644974818730042082523098349935771027426720553948323812084458911981408/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^4 - 175563059999971234628169962342257271670431849040771041371317737377293419967473757249040650735625166043653742853811714247829812831695595593/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^3 + 135180905372324288501569577083949075618905004053401734480174327933119064756438655291789783788686246197426731617074158698658906326521062865/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^2 - 4197250394218443078764962775600030897153735579963288074389697446398952921086402239486850666413077729861607838742318248136881651627012701/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y + 1144152697560835153411509758132589607405723354757249744609344495953526214810524466659216322688378933781989414060981996492237645069481381/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271


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

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

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

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

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

# 1 Loop Invariant
11097420743755567676555223407013896789429620255355418639429091116206016146117808706084993961477266231103273556162845799707726139893192/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^31 - 91038516607713386551976894538427674763898880441983660963774960038148122597789707064778535142624461582665442239128379216463380192302059/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^30 - 1624105143002580283306932468013845929259737407060042261064677952583446424378722449810102100793312168234422093108085574444397598090501183/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^29 + 3173174124317741256621543416161573791401458285084470628280290899574579896135709776459311763165396992774716015646861199978370426082925753/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^28 + 62776184910432362460768842343256306624925278622296667992853450062723819394147111810812211467774323250159375837570447640294445573079189472/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^27 - 2514595031583216757797523297620082960543297948618868706014940079576904331301924634941816670738595409262284813320848424747853403504620160/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^26 - 976001355578673109020517702051428800230207707609958800951051834187906257702136090691468257828385192545983601144071598835778964227246248228/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^25 - 806823288686094813332205861992552979537275010473521303669767449919692645547668391996348156518146853748947787610486877021472560884571114002/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^24 + 7664298059623153518575027198458907104338286040246428532596914741761207433942315634763834907194712371295531666860547867424729916304240140089/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^23 + 10255797598053737888568569704975016090525349282837292686125822570117686122738825033707133093552519010803187670508403098402266199316651354051/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^22 - 36053577020151606980734013619664658087832043887812853377336008654628088430515673646781322391576492486410579663749260697946963024597461578370/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^21 - 66765696763569979059751665861840968411895765320776224734569837620150817866294440424914178583861911789632157298261954985464517293401538372513/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^20 + 101980350945901010171992806662595541913667202865933400749556240284751031535740020499908539116309667565672379493370599145913848666036729877510/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^19 + 272164957694501554017923211615452247876419481573483360523075942248961778241550432625116333017427520983362136416092914125557999138602660199725/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^18 - 135245096645868142783730323721746423920619145313817794370648639048402410081074490182467050299333985910245543360109738215947412818411881408452/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^17 - 714859225029213739724718485519131172146576910836819885662523244388846170836869172367207919908033195461073720854468438407473653136109176558499/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^16 - 113453328509548712353493503725210897981937316906714670397044245536197428268669832909837638013167998401562180043637083712231297345526047540299/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^15 + 1158661002830986654774155324696660703226917584931465331846013463884138176264510965353719629145250907331914140254887409667899109369600857850628/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^14 + 775846181641895448540311332094903162405921235631157821274236272806269200672095960711390907743237877253003378694389496094329105144057883685461/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^13 - 1000228419458560000182306850106112410840780250939006494849109924149328883101490741147256860352903110105498913041994284590955240431842649601693/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^12 - 657438976686451755708192636787993630595308225559099391591666780681770364067879055625939971525781565965080882161211034538419714987604410101/604003099512982598971332545662963003057990011235971454552399179867658299136336947262054938784949032953346429729913463403140120693697*y^11 + 214144732921934658171778325241260411197889034252796400552971927911366250648644991580105432000907004686078743387656337527955994962927755324303/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^10 + 925348652177312129717748311844029792289562082741201796279251022579901993863950096316024901158503477624589941979298067703475105943481286388105/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^9 + 238451578920017200415036146406688465365978683805342694562470536933208162263585032602356304285936500649020638666814192946717736485907522655909/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^8 - 291053556755355647197532236604355707880326715757684896460645926992756142229916567884276434813918190889996862767779309444455114505394903695113/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^7 - 5080690757069521466537989791605805276055782615880835891505897415018714906912487501828379001866360467965867696791367658673462700679478672234/40468207667369834131079280559418521204885330752810087455010745051133106042134575466557680898591585207874210791904202048010388086477699*y^6 + 30360244207183760447752423912191632758602174040086840405046586553416115897854139467186964766981784762315652206784970614823325428861696357795/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^5 + 28943906659206832220250043144918245781905331167068919759270223569998788520576861782847770963439512621725367405985042833593944381643351443200/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^4 + 1153078753181428806635997334518862266264265595383728187664510073546498841417393680368350671145661032956555414609891798582141762297651142516/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^3 - 3194762174134634653816217677091818793660117506147803519256011202310080738509453061682912953310710157540157860193805384742971275697538298284/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y^2 + 281075675243487421892414661925361933032151839210141492682530541545296286008360981882845916105684178588215065996205598128514471923994294268/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271*y - 11873824312617471975215360368471556059619903827798984883720852041416664634523577142401700556970723482030427110394301690839400221481293299/1173578022353725189801299136223137114941674591831492536195311606482860075221902688530172746059155971028352112965221859392301254507853271

# 2 Loop Invariant
15107713673757417384429247361975296385945661121855790842716464258689186239862783021477725038663333288214165878408678909250142890038307861883451527623093155283540597771403061724651235126886497820575424520453761997910839925834677285500748605/585345128902027452030167617216430159454868163825533569561964292241648643011717243999901680258971279388225389776187516990983752175696472410992046175843128111223454411566322452941921778682438923064494759696164576077627531597625917469291714890708*y^31 - 487913269875147686834549879431345700959285608421829539991515567011170640315963429113568667127518132716651475963647434155573139694570598560452359742581401681541279231090280225041858272047187159939117116778450427188438973201460831127556744691/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^30 - 8905579276323250772905372587027270080962616118185967900287138426272511094306545149058920609034945132761468022849610904445518556044757874161944692240189721462247277832587463064339310762545428971008370385002709634937745214282670335988644690113/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^29 + 16111821199130172626012757054759909355372210580315292091335668620729678510083020498676392068948693749929738681812398504732624362260642052414476399228932865121734250250647657708284147869301872231549960515658369705948123307021477820983870194275/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^28 + 343673247887344176676000820440105893724113283062354825737332881297144518143779490929486986193478745870878217621782728567577394849994592447879221071691658545737110354686257501030998162949053281171331797215842676151208815143916316903947722070937/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^27 + 31174889624742615377973529290049979365229287168888203956482379353700433387204954961034547555519997812547713576086039389046025785718339935845795147699890187248669144336536953946791836119564800117427992833026931727264319147273379291476798971775/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^26 - 5300709962457055391925059106586168979207348776100694074324379221943123583882944280392805722408479256937568668974076799951338467676971289761428907273304316008974132355040673760647702574795709280675764012821813539470950631543660302896762775342865/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^25 - 5074065426975147059740338812537919717398904291513522310468418485891169717492385897270430458307021584547074834204636466829705687917324903253096303848651772356941415743074037131410616913755907065740661178861056866676675369324150301119772683566369/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^24 + 40929055766069597323440635506267922763333532528261810893866052100033567471383138145479917743527346879055353507261895412426105312095644518467728937766761455772028923428589344286718425226672410663109801683384698509221894280097608655127413924907959/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^23 + 60922181271217923976082915070777922341838076949299786542975763819484886814256782164747690426785327074820659907926049101739964954548561561666694475606144019250742618324651210013379648517014879497793927075780745044123351612497261033887509787439971/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^22 - 187380080435325641010166060950385122157901122022841843117715721101733227808867040247964285934259861294042093158067755635061768661106135533888113283369071777105136967562816653331681436578088110590570696723025738553310052958886025929111641468081403/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^21 - 96375213752504023606719114340865995950328780927353923108626514941678803654787739153512022104043927847787490362885539041724710439278836837353659926901419687978244835580425455893889954750604883808428547961654020344182914718642706950966037444863577/585345128902027452030167617216430159454868163825533569561964292241648643011717243999901680258971279388225389776187516990983752175696472410992046175843128111223454411566322452941921778682438923064494759696164576077627531597625917469291714890708*y^20 + 125318789144587167119759609005072291685057878098369013224698899837356005552035458180973058158860143408962709141172593627951174965701516803329034784764155382062023253247188382167252750853861735570614969264612052777023093813609803023981498882221021/585345128902027452030167617216430159454868163825533569561964292241648643011717243999901680258971279388225389776187516990983752175696472410992046175843128111223454411566322452941921778682438923064494759696164576077627531597625917469291714890708*y^19 + 1533545934939819307156143455636421984160975071607073591953154711165379012059503881021646728992910482302821168466727734203539099651110967765577227696237965279120452069657118118422356922445257258239283250425768270000076262200901206348874301756846819/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^18 - 176951638717233171418396273744947796868924682874657307690571223782023124482728532218786673487492952881913067686707607555400070941622693815971600517733123583157061101238649162001355299008931278173485270856170757976162729131780569603661212555384641/780460171869369936040223489621906879273157551767378092749285722988864857348956325333202240345295039184300519701583355987978336234261963214656061567790837481631272548755096603922562371576585230752659679594886101436836708796834556625722286520944*y^17 - 1304350999126899994781145094705487337260268392989972408154239022426032448368617923726259319709338716334339328700511272838791896758675519324507789667294161966276933309014437311689176539737202157517218448263817038126217671829272182190853652295673403/780460171869369936040223489621906879273157551767378092749285722988864857348956325333202240345295039184300519701583355987978336234261963214656061567790837481631272548755096603922562371576585230752659679594886101436836708796834556625722286520944*y^16 - 556260830078238324204058830559794367129654521808387658286136664849248309276282016395427862933333175319931475883170126955161091884963128995761904819058878468400166691708079604861047048911924520419527003958477049799650261545228006045737543413604009/1170690257804054904060335234432860318909736327651067139123928584483297286023434487999803360517942558776450779552375033981967504351392944821984092351686256222446908823132644905883843557364877846128989519392329152155255063195251834938583429781416*y^15 + 3028971814010742135269153933996328408451708218248723499147653419189269620322418535949413423689047458985989904758853870451111664135588843496514749673647125084227795493607825167478264137385191144467197457625630889228480320889351142872817734918002005/1170690257804054904060335234432860318909736327651067139123928584483297286023434487999803360517942558776450779552375033981967504351392944821984092351686256222446908823132644905883843557364877846128989519392329152155255063195251834938583429781416*y^14 + 4914844116108942326395426310912773039059783340813708406436935133290979328387399743267927078108119210038627844903501257796551762490029785457802699587189431682530811607856717773147496501190543773374036567932569844614306808157495645806981747189298575/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^13 - 1561852631375391685273275075495379326618905050051258953814396433077027084689756565549257337274471938655712825113761430873490261793858155208106378101915682902162051486734986868639623110243877452087329542526963433464311240348431457305895591031549193/780460171869369936040223489621906879273157551767378092749285722988864857348956325333202240345295039184300519701583355987978336234261963214656061567790837481631272548755096603922562371576585230752659679594886101436836708796834556625722286520944*y^12 - 236221276892776600372560365487034208811825018521082356896955168632836156074534056777128834864907113169831518986575191002407405916079687680359550258323878697173259043026769021894654721069806843251413513444413254522745258700339939051655724171845/75314607424347330420762688782350766785237797713012553983783362357391745112161251157990437501154307692772180877018465902082314999446277973622239600597417410090511375651868560594688854694086325664500097747833836345551663869998188042883648339*y^11 + 200694986070204097403470637755886080718727191046740311276927960044421990174322612255992629122328770599026481754391370168934332718557157013992212980416380595807172736633303363283508300636583533354343486039962401214652513338370282797035529546353393/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^10 + 805232953731434517737694168681354466915622409824919241941206868991474753746404229683835532910658936449931709327794279751105666148427181920343328890133144460996150842812204210436094125150925373250225691772923459308465998509046575970102123527796179/390230085934684968020111744810953439636578775883689046374642861494432428674478162666601120172647519592150259850791677993989168117130981607328030783895418740815636274377548301961281185788292615376329839797443050718418354398417278312861143260472*y^9 + 1795015461562964376851200800494134176952283653172229385398315557321665679365713373747574937341453358693747224256913972288680737702802065298213516676195332179364386239566959442156748408905074080328114646635788456540629441637612501563244791735063463/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^8 - 212190547490301665609475437427053588303617685663120543393815841061804932804806172569574578602698634568028974766303327456856957684512722740842893103101527783790112823195912656263390995605228067697904532064527851429540429551268425645754578460437881/390230085934684968020111744810953439636578775883689046374642861494432428674478162666601120172647519592150259850791677993989168117130981607328030783895418740815636274377548301961281185788292615376329839797443050718418354398417278312861143260472*y^7 - 14838467904666675466063814234685011492331900787003082940236332130540858426461977301904869382247158119876013752159018272297310980087329478686673166865239470906741302679071427575577407020037257340570512493510894616213964351140473551795230277995901/40368629579450169105528801187340010996887459574174728935307882223561975380118430620682874500618708923325888950081897723516120839703204993861520425920215731808514097349401548478753226116030270556172052392838936281215691834319028790985635509704*y^6 + 73933164558558823407540586135558291517118472870294679506104204754739255859411007597950703349864694037319538471351627030578692922261536143363842956730609946766494463042473590526902591135562783722334678972538411032028541435985114044319947765645005/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^5 + 145560068284926319090268578654116412046096789053437868597228085846776762383598845331965534383741641075158898035254029536155168049803375815248308085251431952177382408428491800198429638435100919878359527784831509048952521338237515116597118402225681/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^4 + 6154127451343963891045552550459908368245238000826643215261123549866543586894401397850170713600315590746297817958431147212262989464588933713989422467480072727671960581629458105684603713987123933801759014741491910043755110249238538098278674124045/1170690257804054904060335234432860318909736327651067139123928584483297286023434487999803360517942558776450779552375033981967504351392944821984092351686256222446908823132644905883843557364877846128989519392329152155255063195251834938583429781416*y^3 - 16197037479351163012888040691595482900286248159636598127521208459596367482167533937371838060712364522815371372495251113074341001704954731487178157971694966542732743382898214054615587845030547325129715606563379816648468271528898121674807689258867/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832*y^2 + 477808645720518269418234324558240354989407574159281120885580780919213618887775710971861901870773347256649052573343179858904843250110438887615486671402601764420239086778753819192019353073527211750530018608945422865806196155577035523153064729697/780460171869369936040223489621906879273157551767378092749285722988864857348956325333202240345295039184300519701583355987978336234261963214656061567790837481631272548755096603922562371576585230752659679594886101436836708796834556625722286520944*y + 188678248690467050642586463139115004001278803539935769839790264048600615537231939169507579347705348425908749969707234433083521222010559109669774045988165257979356365730486352852529068042760671229237972374676765782496605083930232797072216957727/2341380515608109808120670468865720637819472655302134278247857168966594572046868975999606721035885117552901559104750067963935008702785889643968184703372512444893817646265289811767687114729755692257979038784658304310510126390503669877166859562832

# 3 Loop Invariant
56011620474040140517492666624784508947164318324022460481511272208736448205423366924104291541904215150786658500612432097169581541326871099105006000455654054433402302217440868217124484237681147389150461439459162020377938206766406623917168901636427639250907487825336112398819242924088621457927829/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^31 - 54879382316391629670178958436270404031421324141763310540191692314585303462735532789327009040649805277086998418292312847930000651034254554305454667253909254135999149047788643165435503443798319125416973809141228631067485105176653111214609181938252998944294144455035350877338025152394368434044193/79557320372159974453249096964676165746211019345632505809227257125588987653240240618805159398560089721943916340469909803956438992226043973501053321415651944971735313921335942622044217520819885163293139557730198870675476351522676253471421635876827588509774323780610756777395819558292490399709316744*y^30 - 522583891043249445170777492789445644826552937164083759740114612295964792429634350108424538452711759628813726231742014406188829857700690196044685140380550994542758670909912710071765208568031092775405434590565503634268316339297874743391715107187599013296401775655940244439430354250900591857550951/39778660186079987226624548482338082873105509672816252904613628562794493826620120309402579699280044860971958170234954901978219496113021986750526660707825972485867656960667971311022108760409942581646569778865099435337738175761338126735710817938413794254887161890305378388697909779146245199854658372*y^29 + 6495847197569771395387870789350128572393999101067141561500350841446719943735580228939915193026489569259497633385767574851124899318111908474083066757197081187863097064661364364602990126095164274534238752051862234122343829207943563733563281483291348407149918078346606435631110518488653485876397451/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^28 + 80533183302544881904643530495158496100628551607997106394844176836959767739828411722966655626462003001859566040129655774997477687958620844626026145891505512683115561218227279229989004522123426706800077330397781494821925609385554914267878345662037310522155068146337371071891385099507775112862725081/159114640744319948906498193929352331492422038691265011618454514251177975306480481237610318797120179443887832680939819607912877984452087947002106642831303889943470627842671885244088435041639770326586279115460397741350952703045352506942843271753655177019548647561221513554791639116584980799418633488*y^27 + 51964758581225976747420976325775781377286579911545667227785809144808732887859602889344039496803033855543531395708567026809926898604740134348213267190265300519762324671740988238562115159182698107522153326531476216858921899100548775820524846391782359947507687820992951940815070913249953027086248321/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^26 - 4909047137784022496392379062938463070971661715149030537932568337743638476425899043241559751991202683530329686864975512385287358504977396981245168703704187395151468359550146213685194724856077348245821929509813305594529099101643954294194270641311963387630573085279556296727530611643551880534224643141/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^25 - 5864758643950728649437319956683745316057300929252032871793306495160035732961485861934377688207638549885246271381806143022443970468135087408756726365337486166934929291548843533143054096663221580017521242520505986493757881798918232906717314041724175012082746708812576175190605257364274110159645815501/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^24 + 576048977078371350801759667778239654979080214795579427282086148547590166113169584715115145155818693685924737436346982581823173220111373707870763976384540713246121576950211593697204870697017061374560325540208217714350904482079208414011140637824507420052430462152924565210055354912098703416012007282/9944665046519996806656137120584520718276377418204063226153407140698623456655030077350644924820011215242989542558738725494554874028255496687631665176956493121466914240166992827755527190102485645411642444716274858834434543940334531683927704484603448563721790472576344597174477444786561299963664593*y^23 + 2046968627953806377285196935604467654857952983246080162607095869734963300606524620027118071588986997787524386677664067642492228700623087102864042266004993932643746231110999149399114939432875862492954916461947586618671406273676323324944442104502988204247290519655674461274489819452143807793255819179/19889330093039993613312274241169041436552754836408126452306814281397246913310060154701289849640022430485979085117477450989109748056510993375263330353912986242933828480333985655511054380204971290823284889432549717668869087880669063367855408969206897127443580945152689194348954889573122599927329186*y^22 - 160616123050216869722989036744279967052016546542857622330219533383844605265048025459028409240537419046465074715753275611236783873790847455213608724977787736428062207128871156203984133344541166577860240197397444846275845710811790468058564099501459964761094127220556544505528151694019793423152095862895/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^21 - 399133079621014827160942793538208982931076045662265970850827515808776998073589207543621965842945489881278558134806025243063325808861641501045207030714956666186631525868086089930196039006001248094785682206747169874492412998105346278839704214783467312021205982412700208896614926345063170510616925135475/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^20 + 95272474931897524222096098073206247181030303266802338870780776942773102059350294261547444214937748223962582537895969869862817658831906026904457195404914624892243858036503873417035818974237296232590071440877031894598541538531076505404029917167488977406191264514253554474983625219849265101595765868321/159114640744319948906498193929352331492422038691265011618454514251177975306480481237610318797120179443887832680939819607912877984452087947002106642831303889943470627842671885244088435041639770326586279115460397741350952703045352506942843271753655177019548647561221513554791639116584980799418633488*y^19 + 767842946779338917851889879650848486706208122694818188340732157722490913680622516638346694311073427146240955447604543002780861343880094049945166402034322694928999284850407761978163793374570154727917522110550757200392106747078481917929597794403425999657193852072684802642751265672987393211266231177089/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^18 - 78140493116298258913527328340386466858329378483152165879771725167231567141064805151270012733983214756201007576781201782434431677220609910816004311986379841222199057265678590296883110206289650301504387192768352924501114365217746971396796743785440282131292128490113515077840225859187481430256511311279/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^17 - 3758807939501216569159783462610577173473419981741068794647337760884701206325724947958352548297352534255990429406261479617124880913361827624562052029034019347420914460818324666215983581194729813924549218991390202544691266898573116565351863181275639880146391436125886627249917991505195101870560587757643/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^16 - 1899510119418922533398623007007240267688497752952376277913292233413829137994861334998154306183398032318885429520746987595218962986724568000686852567332782311409596922787354004818356346987943947940780780079333770600238127765466613712686534195646460222493651302915265232418003641081775347747991866801761/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^15 + 1350688669976387620538483238352132687541013526146249870613985286800088481113139872038198417218209726817819758504436586585632876113126404263098804415364768781511655360902302519954890859404786535164155573697298682948397721379483332951466412344126536620241746718659011926397140017820692541863940313719717/159114640744319948906498193929352331492422038691265011618454514251177975306480481237610318797120179443887832680939819607912877984452087947002106642831303889943470627842671885244088435041639770326586279115460397741350952703045352506942843271753655177019548647561221513554791639116584980799418633488*y^14 + 1482446367342031922924331173585282597944743596592192546146475631004138453792815266893132251071955933017769561716538123214981283466670772489391536281579770238326641756373525269652144483032156172369756605276562210795477718568872790950035036477759436998017702402820607513260231441731371678118729696338833/159114640744319948906498193929352331492422038691265011618454514251177975306480481237610318797120179443887832680939819607912877984452087947002106642831303889943470627842671885244088435041639770326586279115460397741350952703045352506942843271753655177019548647561221513554791639116584980799418633488*y^13 - 411408806711444361349184005842250787494939621390341683668538496147702371900000568952031937943929341433661447101091663476421684218673026243554257342475601350464654240083381757934146668677431459451026751213834834669721224513847350538279529214344665386582315470935112427370873843634600163617350446008985/79557320372159974453249096964676165746211019345632505809227257125588987653240240618805159398560089721943916340469909803956438992226043973501053321415651944971735313921335942622044217520819885163293139557730198870675476351522676253471421635876827588509774323780610756777395819558292490399709316744*y^12 - 4079362043757677305206081504100318011008612993830814281891770563074645598652153047738039221831523769522159629867186819087276778433710728157889856778413192836092158130928123445146886182942961888866274292518054279205508666886062100091546161813378786438297348352040744174344917452779882974129802225095/327564880585321562339677187708393888816103013260452931793009808031246475154874897040885885326032278834560643707544662085255538825428899530627085214269282326183161354282391940801005527620462728412941387782728559426352964905909114785265760724145455845639832521999426687709298279190087454038947264*y^11 - 1453902562344730642762318395129890905233416473344495045338774756054265154049574176227678383768795288088728035928598727633826855235666918224565311016374543596338958498257890284057152181722450170317720901443878313745989948362995783559586850592108443909871618676394527395912160042489906879124160299709717/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^10 + 2303121791092784871236741267219617103552773476651522429556188667488488050783593410914446598858686595378913615419089105007529179472732564175341961725153015418781263129538054511811095975568288538970109732232260302611855165952546130401975375880556133417276385141949203031600333437913203893043854751302231/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^9 + 2808180806137935475151286431331936992958063281197852772493073028271689610557711499992677104142546108069319192606909110938087375220981975560927453226844534336513750192648278638461549211069937750497488695233433979663621896559688072238748016083120465443165208084102842562372044110660070984353426455528115/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^8 - 397259582381066153488027036213610283918461526719253919891074354475581070647141087365339939953417707128002369542229203993587669015021412608397685766254649863307204528350242757604655199152859179602495719230510763592049939316821819247367561049858262098476567765544465746194064081688250603034184117037091/318229281488639897812996387858704662984844077382530023236909028502355950612960962475220637594240358887775665361879639215825755968904175894004213285662607779886941255685343770488176870083279540653172558230920795482701905406090705013885686543507310354039097295122443027109583278233169961598837266976*y^7 - 39102966457758711861807394460513540614905766934292232938229564542363449235239086112287365108846854187169603571162869492100431883858982686438521110699205243319013375817663394466801043091739473326726406913781500390703398727558003491041478496499559925382097906440902704128464339963869718369636853008163/21946846999216544676758371576462390550678901888450346430131657138093513835376618101739354316844162681915563128405492359712121101303736268552014709356041915854271810736920260033667370350571002803667072981442813481565648648695910690612805968517745541657868778973961588076522984705735859420609466688*y^6 - 150604448106034767433831742082379549265646466067705532811149588914101962693828940861722989506318926298233678831124857747599918490393779121617062454293992702003429086767189758330422053527736672985799019782166985265708046249984128130050932803620170871481009757826563412510690420903482936358815435428321/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^5 + 39120505580135015358699357463313489420771020422872482546267217680452754571895298887205718958496303756183994329947387494301756769264687955513663110728738695462286911212812534022965491451152573348872049780197065451345420745633113927516206787726139686994963317470750933913737667984458584560141203767951/159114640744319948906498193929352331492422038691265011618454514251177975306480481237610318797120179443887832680939819607912877984452087947002106642831303889943470627842671885244088435041639770326586279115460397741350952703045352506942843271753655177019548647561221513554791639116584980799418633488*y^4 + 7000428664617042777784739889789915689845025379766207132492831606263722099575145064741384455521761153114041089814156641268982140914155357190067216825465101965683274734497824968155719305896492769382384613730558028272575686952812526051801817619569403174572117619300093447695181654661878339428157116281/79557320372159974453249096964676165746211019345632505809227257125588987653240240618805159398560089721943916340469909803956438992226043973501053321415651944971735313921335942622044217520819885163293139557730198870675476351522676253471421635876827588509774323780610756777395819558292490399709316744*y^3 - 7571240683382884745988750760825538260793788835622233737745509596040432743564580785857383289341876567812945428289141295246701952102288888788560016510466440714393944785771477790489505476827142121106441242806188925932177242856666559089190418024227479335658720709327726849256261061949379797896461364529/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y^2 - 2867474477216203768765272509505462084264094351572370804605194146808210915288727317545433554785452622270730412388415648855956564027823191884306280601789113730944674367542361251500762850827925383754151026471048355136012271831780397375704761405854373104952705757966537685670958313194808876988701904815/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952*y - 96740619041745987248650699982299616393921641186563203036303975072934241029513775589567303917013166055043370255522372881794379861447128259407361438708709153359784589059687550215945174568560605774678904484254673166098094993876368296536569044675671436815055702740696250219454300037704847321868958495/636458562977279795625992775717409325969688154765060046473818057004711901225921924950441275188480717775551330723759278431651511937808351788008426571325215559773882511370687540976353740166559081306345116461841590965403810812181410027771373087014620708078194590244886054219166556466339923197674533952

# 4 Loop Invariant
4442360598669265847036261954617362834580175866228721191926710428398103696318574634127413697139201120808011838194109225554376510874068200225429420836593898891961940554512230143719988387206459955784182273691427169250889259349908330878339930440267013006322934560958206072102921972036236867683196325693693276251831277069803713141719266723574698487541306915836668560722479338689027047986203731750045825726687/19046773839862158091141923097298472625700132806490555186798664601353815918324388909899846906743597817239865542310049817646403108483891960059114638109762355419699340001292787376138868926082230052057507368870040226690851548561621161704751910256496406841364309004013179240512621922323259886310783350646330781835456019314092941683552963684035806260800995794269879326266811209981087567889402846625365054595445760*y^31 - 11519030131796256154081262602366128207567290569463697436462666155873688769785842689433548712848254585968257476164123940173127097384572734808450395219470681612620388552594177979562707621345543938261956416491053451286061378848684552134100313037786431407042136936491011119561129978948452302176004661505049908871426075273606001415544147951324424520373595791555221377755240464424817484311897426995380937909111/6348924613287386030380641032432824208566710935496851728932888200451271972774796303299948968914532605746621847436683272548801036161297320019704879369920785139899780000430929125379622975360743350685835789623346742230283849520540387234917303418832135613788103001337726413504207307441086628770261116882110260611818673104697647227850987894678602086933665264756626442088937069993695855963134282208455018198481920*y^30 - 332607905648394114895661607775033605049182601030510471263575116715647374262301006194396361024505136934872016742320801544302556949193732949407772523585659948492586685118958260016964471310233468680700717959910268070397268277785522281691645927158833260203763263628412042041972676111682606140904604444964504769641029030179409201022273752863727978475723907192477696341068192464761911105629440257475475968154111/9523386919931079045570961548649236312850066403245277593399332300676907959162194454949923453371798908619932771155024908823201554241945980029557319054881177709849670000646393688069434463041115026028753684435020113345425774280810580852375955128248203420682154502006589620256310961161629943155391675323165390917728009657046470841776481842017903130400497897134939663133405604990543783944701423312682527297722880*y^29 + 110119847825380742887724843839570615642758740088824532530768031820144007336982364268220582358308308731623340052897368000337942701767356525620005935215446305920314510674525620583343778593440296094168717737171634412608861435398027137927357686693570211077093725626663705624922956541679083296559284879289278833918677661550086431994273054080885666537042139452209817637097606548828832092833325573618008596925721/2116308204429128676793547010810941402855570311832283909644296066817090657591598767766649656304844201915540615812227757516267012053765773339901626456640261713299926666810309708459874325120247783561945263207782247410094616506846795744972434472944045204596034333779242137834735769147028876256753705627370086870606224368232549075950329298226200695644555088252208814029645689997898618654378094069485006066160640*y^28 + 71139184107608443782052726052065088203511591377430982078663538474789500247098745610123107520414715739423783948724954042414833300612642145333247343081438260945838813653315382981516394717345830898957423670275821211146110757604008593392062658407969022475192965570315987878552278277787023031423038079436626626203105986840188202772766118026911617410960838316534964555427483003951912115185589823737218957812835/52907705110728216919838675270273535071389257795807097741107401670427266439789969194166241407621105047888515395305693937906675301344144333497540661416006542832498166670257742711496858128006194589048631580194556185252365412671169893624310861823601130114900858344481053445868394228675721906418842640684252171765155609205813726898758232455655017391113877206305220350741142249947465466359452351737125151654016*y^27 + 542093423034474578267512884567735132784115573221839125937965486098110205858292121949280836310515631857739374903998933006648996564335729613135163677722393130455016166726535599830042083245856979021311797279484063137946779975181075381438384376620370701441158620829596551813110075020618059532883928059604463293623400938140479355374740808400113447482205345174010747004014902604430023778937220022443764731792571/1058154102214564338396773505405470701427785155916141954822148033408545328795799383883324828152422100957770307906113878758133506026882886669950813228320130856649963333405154854229937162560123891780972631603891123705047308253423397872486217236472022602298017166889621068917367884573514438128376852813685043435303112184116274537975164649113100347822277544126104407014822844998949309327189047034742503033080320*y^26 - 77772379011238652720098687496699765463690469108066245306858664086757232686536835856160453366062814042162314879674467193870964084334604224045234114547964320889076754471619374425388028248034734006578259234174881586288953548108122768990420754682729817224139059448146321066450647380017006773392058061026626251297880436524487778593250999085132999503144968363883772148370730128802327935282777806767212790237282381/3809354767972431618228384619459694525140026561298111037359732920270763183664877781979969381348719563447973108462009963529280621696778392011822927621952471083939868000258557475227773785216446010411501473774008045338170309712324232340950382051299281368272861800802635848102524384464651977262156670129266156367091203862818588336710592736807161252160199158853975865253362241996217513577880569325073010919089152*y^25 - 10171751320924298401306292005663042276642499038540846722520460039284486257829284026303922633878263805915193304721404093105001206015177656170989157240814461699209416294112267347789462399125768822567446695298837266557992683036725269843447536017873303413739621282458358643897736744513726761219630452244344058275997062171566461624634989125738672173115175607998755674236322654854468053283792151270420082234402423/396807788330461626898790064527051513035419433468553233058305512528204498298424768956246810557158287859163865464792704534300064760081082501231554960620049071243736250026933070336226435960046459417864736851459171389392740595033774202182331463677008475861756437583607900844012956715067914298141319805131891288238667069043602951740686743417412630433354079047289152630558566874605990997695892638028438637405120*y^24 + 2896478856018862746641027764933020561002437905215599921922818470556411660167284477962275487171609783069003840689243855856170197871180545119686062959471155471548343728321525259539041087127965441312220226150491670899471877260813591942736564760944988641393027046751770813560484863308617268317973615410401315950034063237811601667937854815410899480534603232627988169627283990062935065769395875988493538964339264051/19046773839862158091141923097298472625700132806490555186798664601353815918324388909899846906743597817239865542310049817646403108483891960059114638109762355419699340001292787376138868926082230052057507368870040226690851548561621161704751910256496406841364309004013179240512621922323259886310783350646330781835456019314092941683552963684035806260800995794269879326266811209981087567889402846625365054595445760*y^23 + 8388841973451791508831255241235867055710309524987349136640331039846986493126553034949623148478642120434534070069998592292033066886344658192110228372472234303594390995740345404672900557651341894634285902020582905167403820700695874310408246904445558695665048569057339641431659037827933845517526934184262001559186649134587470564626156065519651812011911319770308980971600567283655240245773743163997273057535795/29760584124784622017409254839528863477656457510141492479372913439615337372381857671718510791786871589437289909859452840072504857006081187592366622046503680343280218752019980275216982697003484456339855263859437854204455544627533065163674859775775635689631732818770592563300971753630093572360598985384891846617900030178270221380551505756305947282501555928546686447291892515595449324827191947852132897805384*y^22 - 5395264360897458933109020912706644950711123778770975539819970271318036794166332780237752641143354374405262522651198103377238925705859842665128714617686535821932006728051778777386368109496216327439798629727860017543697141946225317153091100318095386434723815772931135539554818709095513774937816587353395261072095030147562267033485903428538852312130709345922899557769885205134815467840288042394025070914222727/8266828923551283893724793010980239854904571530594859022048031511004260381217182686588475219940797663732580530516514677797918015835022552108990728346251022317577838542227772298671384082500967904538848684405399403945682095729870295878798572159937676580453259116325164600916936598230581547877944162606914401838305563938408394827930973821196096467361543313485190679803303476554291479118664429958925804945940*y^21 - 32414097636006655261211316744385272105093155787413778245701376797218436599304440461463769463517180730894638013723326222391788474472907546040584100778848978924643828090991925419670914214967451766409142253426286494472839642979114621995402443496994223938452024506804640820191576290599436839443574631484852998308929171972598316472389237809743494749835452160764436459996521386021399944348023601646017598901035487369/19046773839862158091141923097298472625700132806490555186798664601353815918324388909899846906743597817239865542310049817646403108483891960059114638109762355419699340001292787376138868926082230052057507368870040226690851548561621161704751910256496406841364309004013179240512621922323259886310783350646330781835456019314092941683552963684035806260800995794269879326266811209981087567889402846625365054595445760*y^20 + 14171952208271273233971928559121984300655306108377004398124811047494143579823975008758335384068940976899000872489771491153529185009038933270189996189854326449224047510388021499560417283748484703126337795790002554794288213082039107192924966789848255476375081406245686722629175704700249184343223021142908912644277492887821698435464430709161989325200616182324219196684500130135688926215573669393030001559069468291/9523386919931079045570961548649236312850066403245277593399332300676907959162194454949923453371798908619932771155024908823201554241945980029557319054881177709849670000646393688069434463041115026028753684435020113345425774280810580852375955128248203420682154502006589620256310961161629943155391675323165390917728009657046470841776481842017903130400497897134939663133405604990543783944701423312682527297722880*y^19 + 123603438591052411563626349979940790736923419781555942285354894010940177887036015607643728303967288875538847125259886143494580701230868162736101570856533963308754549976290525453237403013668224084601262758516391755387834579763109314766748287028149239961507161575802317855582604399951464931048301861270981502375731370587032665594063313659713796534415324374463994153017676294463729666459489819675756113349204118029/19046773839862158091141923097298472625700132806490555186798664601353815918324388909899846906743597817239865542310049817646403108483891960059114638109762355419699340001292787376138868926082230052057507368870040226690851548561621161704751910256496406841364309004013179240512621922323259886310783350646330781835456019314092941683552963684035806260800995794269879326266811209981087567889402846625365054595445760*y^18 - 1027877918342355497150942703020459731357104827493523066420380791628879417549415465103610918914700751688387826522439243673561219212988139221640571393764662829927400218290005667996487354296505609936231290432956181325933589738689839442756388434734408658479167667109881694493308263036723771359930514533532436298774361754229217463894536423571706538063995356577279143409722265776100174498706228943868818409676781055/3809354767972431618228384619459694525140026561298111037359732920270763183664877781979969381348719563447973108462009963529280621696778392011822927621952471083939868000258557475227773785216446010411501473774008045338170309712324232340950382051299281368272861800802635848102524384464651977262156670129266156367091203862818588336710592736807161252160199158853975865253362241996217513577880569325073010919089152*y^17 - 29888599208994514156034435011821298637727510444706475651865754025867969518612153571574070668121158820640365111150032396513888324168039101960605678631653878059521026848297548806775417947441618523810769134909301304231176030708606009924976357618179956275929178922252647230884420554150893561424071911626067989209583261565797185259734468746612498397753092150844769509251080226689739013014775267934403044299906983747/1904677383986215809114192309729847262570013280649055518679866460135381591832438890989984690674359781723986554231004981764640310848389196005911463810976235541969934000129278737613886892608223005205750736887004022669085154856162116170475191025649640684136430900401317924051262192232325988631078335064633078183545601931409294168355296368403580626080099579426987932626681120998108756788940284662536505459544576*y^16 - 936003803259534082297881869820155279770066352564092251521372427634461295179153275434659568119357266831807248036093973173836206194310189850836053801793426173797742777820473646856190868024392500432365017801218967348235209060509871479322599199515878344678953420049777494694117678631261535847632896604555860317437431122578809648361782975908358690964787024433259566315964569205292477402471358680410228861779244277/105815410221456433839677350540547070142778515591614195482214803340854532879579938388332482815242210095777030790611387875813350602688288666995081322832013085664996333340515485422993716256012389178097263160389112370504730825342339787248621723647202260229801716688962106891736788457351443812837685281368504343530311218411627453797516464911310034782227754412610440701482284499894930932718904703474250303308032*y^15 + 69930154750590201588251659241381881466986452792643082732031976884295357961054284636258281979108327443292726510915623580550934800148939624511369032907290014461895644122687476481820068139881649749072241918326839134334465916264922151350670048728929104036014804758033887722386645897375448001293974696570558117476413472638319040610235358222336614428493263203884685525288464299849890366850321748113009100683757235623/3174462306643693015190320516216412104283355467748425864466444100225635986387398151649974484457266302873310923718341636274400518080648660009852439684960392569949890000215464562689811487680371675342917894811673371115141924760270193617458651709416067806894051500668863206752103653720543314385130558441055130305909336552348823613925493947339301043466832632378313221044468534996847927981567141104227509099240960*y^14 + 165373537039877925623966435363813806754728953645437098173183973330224260785486215028355618284130113457621243965991340857946388349271854745175379183237805586935734762830131969594141213623956430929173608069975520022249730849731005686111766920404189481993175535571844356174119626225915916535681317392191595091897106790898586262408109265993511495018228805427701458031302937459236523236390308938954463693737197776531/6348924613287386030380641032432824208566710935496851728932888200451271972774796303299948968914532605746621847436683272548801036161297320019704879369920785139899780000430929125379622975360743350685835789623346742230283849520540387234917303418832135613788103001337726413504207307441086628770261116882110260611818673104697647227850987894678602086933665264756626442088937069993695855963134282208455018198481920*y^13 - 7765146965365879465316946523101838012879878333843819787113709686848552996169399638928342643032783664429972341916907540365277687958783286133991694111516490935123661789499863258851885214933503482042798826357856748605969918701898053340798529959416532209179762438929120663659291681608505330280614708851454310760110871879582484873690610332518549242338372760720518654455506934875491188693674493011142298237866501227/634892461328738603038064103243282420856671093549685172893288820045127197277479630329994896891453260574662184743668327254880103616129732001970487936992078513989978000043092912537962297536074335068583578962334674223028384952054038723491730341883213561378810300133772641350420730744108662877026111688211026061181867310469764722785098789467860208693366526475662644208893706999369585596313428220845501819848192*y^12 - 110617890200494793283846162647484535083813416436673661200953113021729860739866043735315466280884924553965405025022563851117035564651536006088524983725791115865222486629309784506091093376305449890730067436239477298298142700875401245787683241276242406661349980975938938976912231383814496396924350762717252096141910227809470513983442322722504836069335856401685565083116653774557243312646060477863791063684600579/3267588581208124565301410721787351625613335530363793993274775193232769929374573496294363854304957594311179540626187994106433883768037735470769366634030254832681307257041136966227289230756944596338567055904964869907505841235481413914007876180562087294795729799967949775349566293073127446613618691138502450134749703090425963575836844001378590883650882791948855605810055105503703477078298652706358732989440*y^11 - 153212525633720722335213893061067387355717493144997553628845831586748130432180026451319136659254901732444147620160144004545389417930197279556962560141668735322598399055895827786666081401755823634214459622703004060462309815093992589320331075853357368803270574068679723074079954629141842572631475143994949659181031480850195949547903269549599690231180409001642991358371838601517428716862050724254444198870884677479/19046773839862158091141923097298472625700132806490555186798664601353815918324388909899846906743597817239865542310049817646403108483891960059114638109762355419699340001292787376138868926082230052057507368870040226690851548561621161704751910256496406841364309004013179240512621922323259886310783350646330781835456019314092941683552963684035806260800995794269879326266811209981087567889402846625365054595445760*y^10 + 71812103930398994600289132983408981907937392107739425226516616732669761860875404567075940261691419338687232684462420749864135415505393883989743332087121683475110996837869867250356704394019156323722857284533604046271095853203381047657148548614230122580570239499322776999810887854272561222021146799495555114658236121807581552301500296588155073875050505410242077300833858662517389539848629388928792481851870139551/3809354767972431618228384619459694525140026561298111037359732920270763183664877781979969381348719563447973108462009963529280621696778392011822927621952471083939868000258557475227773785216446010411501473774008045338170309712324232340950382051299281368272861800802635848102524384464651977262156670129266156367091203862818588336710592736807161252160199158853975865253362241996217513577880569325073010919089152*y^9 + 61314806217469076236706704328468815114883444533440381157188185599435038926383947415010505465879267893593611639785327945768465852826392091109236747227713878022858261586729923789539533033376501870120701672840794538133381792354349573133152745751082855239678156125902863467030724071821531781885714956896429434243903749668783954312114184716944672215287318748275773845584803557508995484531473211576627479931610816931/4761693459965539522785480774324618156425033201622638796699666150338453979581097227474961726685899454309966385577512454411600777120972990014778659527440588854924835000323196844034717231520557513014376842217510056672712887140405290426187977564124101710341077251003294810128155480580814971577695837661582695458864004828523235420888240921008951565200248948567469831566702802495271891972350711656341263648861440*y^8 - 5545885540056047442014545303182376132744969817732455117924925804113404273144115335569169161336949682700028417623700420399643105518442348816836607087055769452438157029935320154215991240177336823292884727538239056086916332566065465405019635670665279039333531812383352625223776260160008041093310094887623132969916463574493119242442811441058615320897028768260542340458704073979740167430077770239965616476964706157/2116308204429128676793547010810941402855570311832283909644296066817090657591598767766649656304844201915540615812227757516267012053765773339901626456640261713299926666810309708459874325120247783561945263207782247410094616506846795744972434472944045204596034333779242137834735769147028876256753705627370086870606224368232549075950329298226200695644555088252208814029645689997898618654378094069485006066160640*y^7 - 216624661132025398331821076607877039955062849532670173943945007162732278550649516721939112679650823460166906758006936874293358351840403724170950083471399301815200678121327982247517763297559629716098935704794206496967636164383425632312496466492941961656535172486161685346357191328005357058938123751828143493024369255248642954753991323448602047289382924160919123860621508202463285964616621574049749624330416463/43785686988188869175038903671950511783218696106874839509881987589319117053619284850344475647686431763769805844390919121026214042491705655308309512896005414757929517244351235347445675692143057590936798549126529256760578272555450946447705540819531969750262779319570526989684188327179907784622490461255932831805646021411707911916213709618473117840921829412114665117854738413749626592849201946265207022058496*y^6 - 966899379462193942064564486453066264366176781784102614075975581955339952390354335535241512339816688585148611567360192364749677831680440673251338173269085467108331962372882727961728127843538412409307469836930984761271661624175235180242602499243565328202544593730371500567176284054369562470200096837471144972860273669511293688163565291752751360567231256660327722913625816378983579576873799613801116617111179843/1058154102214564338396773505405470701427785155916141954822148033408545328795799383883324828152422100957770307906113878758133506026882886669950813228320130856649963333405154854229937162560123891780972631603891123705047308253423397872486217236472022602298017166889621068917367884573514438128376852813685043435303112184116274537975164649113100347822277544126104407014822844998949309327189047034742503033080320*y^5 + 5920820391637185926819874213130094758286364846391371009947763481456551846470497903772584927544364150648910751615904366078194964372845708274019767801788686304402653487967354069149039467937120521568152906974188950441827699303068834340049038760385913621464943851861113553830749262244651075773772471063526466454498009650401101004678107659092716218849490897056702004840837838139752403955486936040743834863701618563/9523386919931079045570961548649236312850066403245277593399332300676907959162194454949923453371798908619932771155024908823201554241945980029557319054881177709849670000646393688069434463041115026028753684435020113345425774280810580852375955128248203420682154502006589620256310961161629943155391675323165390917728009657046470841776481842017903130400497897134939663133405604990543783944701423312682527297722880*y^4 + 1747624522086814654191839462138641915211543719170908375870543357462503942631649761208953273661012001018804154924884909101200836803063019988578373018891551024403506506500083029387260420422320719523952194990419422172342459645439829860222381905583704986693905579340730736093984425184690596625805041522112353897666680356897851753803969851403271528867964997541608792454836806555932029609292950854544362691619891821/6348924613287386030380641032432824208566710935496851728932888200451271972774796303299948968914532605746621847436683272548801036161297320019704879369920785139899780000430929125379622975360743350685835789623346742230283849520540387234917303418832135613788103001337726413504207307441086628770261116882110260611818673104697647227850987894678602086933665264756626442088937069993695855963134282208455018198481920*y^3 - 69478132592516477938600789479706156594036359284348377107406436871063088256163161401121571367133905093009630562358553141899356429452100334307698332122050780670419207728413877270079274964846034955826488205404556499804464761747374457881220461422955996775935353676068059003219325216175988366467590501953592376901342674892319603790363625519928888874040344509183619328954520526982212344161500840189208920990401905/3809354767972431618228384619459694525140026561298111037359732920270763183664877781979969381348719563447973108462009963529280621696778392011822927621952471083939868000258557475227773785216446010411501473774008045338170309712324232340950382051299281368272861800802635848102524384464651977262156670129266156367091203862818588336710592736807161252160199158853975865253362241996217513577880569325073010919089152*y^2 - 45805656581507492409042005188840993582542066505690062614174233363926611927175928043894521675618739685036622656635990622609084824551436294691645700577634474726009355064770651620176913985055025954015046969810811400814839681337984352591754503418114836847588528981599665073267616487537465154077321633082096080149281073892713443737470375163825447919353919999524153030514141254459117566654349028905110133666040339/3174462306643693015190320516216412104283355467748425864466444100225635986387398151649974484457266302873310923718341636274400518080648660009852439684960392569949890000215464562689811487680371675342917894811673371115141924760270193617458651709416067806894051500668863206752103653720543314385130558441055130305909336552348823613925493947339301043466832632378313221044468534996847927981567141104227509099240960*y - 10557064285268500168138783076316131057158373620472353126822230760998108609843736074409569716922143247680590290007612007604554157932175467004115462887298763133564930944089273732040568318475034291262344341060065528722668817448464364392870539205393523319866501763048626986404933249396542307635625332797195846097252238754407211707361607950602902485145847863640563724917343749899669781320511138834834771330392609/9523386919931079045570961548649236312850066403245277593399332300676907959162194454949923453371798908619932771155024908823201554241945980029557319054881177709849670000646393688069434463041115026028753684435020113345425774280810580852375955128248203420682154502006589620256310961161629943155391675323165390917728009657046470841776481842017903130400497897134939663133405604990543783944701423312682527297722880