# Manifold: Census Knot K8_158

# Number of Tetrahedra: 8

# Number Field
x^32 - 22*x^31 - 197*x^30 + 430*x^29 + 1177*x^28 - 12273*x^27 - 20412*x^26 + 56828*x^25 + 51162*x^24 - 290592*x^23 - 204366*x^22 + 1512446*x^21 - 714075*x^20 - 4149364*x^19 + 7051661*x^18 + 1426385*x^17 - 7100157*x^16 - 970276*x^15 + 585801*x^14 + 5690678*x^13 - 2099733*x^12 - 926781*x^11 - 124215*x^10 + 69633*x^9 + 209617*x^8 - 31619*x^7 - 22690*x^6 + 4040*x^5 - 44*x^4 - 302*x^3 + 62*x^2 + 19*x + 1 

# Approximate Field Generator
-0.149984013335499 - 0.497814011658853*I

# Shape Parameters
194917369487750720618964901678875633439773278591589993387894857375621577969255514431356256954850540569794264504744511061119/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^31 - 4209274537934869526932528255192385967042691678745922657344033318881201301937424338456460411870625837537651472559323665044771/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^30 - 10021197551956166726131370669370920264501015995148576468632492438739098905037559441168006019881513384616416593003001856669774/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 + 67198893915612225106151227419115211481955458164976977673369613955378212164699823345046805378401428140928747553795491437256817/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^28 + 252939656665470269172652889717341229416906224585552310275511232341440722492267516042215093786608304639714962622558664319491527/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^27 - 1141768985030803019344675910612596585824772810320230093015662562966534885950262874559386425575304984133311350832955547341288305/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^26 - 4879974559437195021658645275311060493749485588041073582378145223128662164131090112601858858658445716407933231803654007729192161/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^25 + 2222574610090635122507809212097121615029843106244850381661699209189537777820238750364202755137543552472795081401684365675388273/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 + 6563803021792759386654434744501754964187547078616276514194721069385801825396939985222474328121877316840300570228984206706080091/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^23 - 50497348617961626740117805605742177167670965074026936268561872834847402457212493781091535884866598865172932118574038304402532073/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^22 - 59091823911266103786693226118537185567242011003092312723072163510348315740952780813108213922908454350348108958401281002286402959/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^21 + 266201976359145609810364054281618405765466050624834808069394062898192380356151375993445631036881623016694050059673793763492868463/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^20 - 36734008511727480946709275991143448624447729279779613800606944310662929166061016276869984965292387783773486622514838103042914627/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^19 - 399508375802699989866154335218157136517349330827061328860344240012787474143293488405436760252851396122572556027113374189197987675/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^18 + 261742286120940708469189801731897101733331367351753772493047802649207811204542238098480964964595629966326323785259108557945679320/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 + 314254579059205146054040397463179335225395763769737445758653482237185352961863380319323409278930478423256826636613339159301591125/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^16 - 1031173283174053334959074730333120658405750636276146879078218502776373535574397548061792564070240218270474050262817923349578326419/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^15 - 551664717692873840231778272147212459750993142286732087247285415671709056721831116852224161912521723160222020345039007548486520699/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^14 - 51241342467735286276835803076392674633229221087521874580066850840977669463724312366164627914485756003300624795744344673688015030/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 + 978079744310022803111709883559010177451855386737886162230254853402859397005399970175038971005160273354864218295681825214642085367/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^12 - 31521568996925662029952411924203570474928256476522560154523474773733538415297380742458966642174776529381580229015548240981294757/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^11 - 51453252520977976975860818059606457388604082866075558222375766456079377280719749753718009948829870801272419596429301050508909963/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^10 - 17793019451912261480318239957729031599420784944350684813990946055035172272381766784708814114392331882002949825540906778692582840/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 - 6014513447873237332907964800006807359402230809432200762303917993316864876544777038876336295591229711443383473765632878838500415/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 + 24614468504470754529015561909637122594935543102991810315021518117817665580636060170639716191617170038878267885913897425461060349/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^7 + 425972188058992329036284123035903033108265590555442694841078088650615635794694006916931186223037746488674857400854521308522852/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 359747556920705821696344755854292674191923303804672387838106785913568058797348791069495321781698543396467784046705348967245637/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 + 300180551732851808036480632638264102788599725499382137453164762323524996245824296655340003312149883574372849969726306037103631/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^4 - 3465402095906592888282442901518529790321577458517748949463700879580370905874920497922794187484605961550877954674676749207277/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^3 - 31601545355037208791861557514249577512245546089203252768986967337543700738575860298526286201934714151794226455835554037297121/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^2 - 586595680932804061866670389330079462804509849909839029560209090208717986315110656274807403871426000570917312130224433131986/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y + 65219805205914380360964764243084918693930578947403445560117192291131243998350058671033805083332744175078673334374208687595/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889

979536846706720604002331255504907094349371391195209531831586905693230703877641657592447274520791744563909479393544723992/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 - 37474316046373125336199409309802887030115406977397008321733128027866049722101672030038668327302754283938896530550816671000/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 + 152262210483359525911146598288038410070649358085610674429026993723183848735129641333358435327861546547677384835309549404258/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 + 3667364169014041996069396348531802435603848908914201737805341766951949520213682325040957194341640476529191334542931169347066/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 - 4616345799826351747219571073213124780614951383025064669457569708122004485674997119633218539439805064243387045031554110170324/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 - 32268787982670219497647043871945399951902642866403859274450532364594108451384146883465082675638512992035246314153066263254379/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^26 + 168328454254264183628914292831557753959900327887846487620313086677983531585476071943018428067710959674212556990203374713942892/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^25 + 438972143424920757872964751072142110472502608440736353751406924387273417683766396930551320440077101086072024897511191492773232/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 - 711688579830610003333689069592433676236921857796485879464041763157243674424667106411436396368751939752074672714072947374194793/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^23 - 1303107433587017667936502833968321222274733288169219494844511827490772616407391828780571209063819503452462866184674570185918696/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 + 4018480217572225722261701440294591345595215782520753968987814289181749454111808821939984939331180902208010131249840933642875088/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 5982062950653192499284292068927013716314907864675044359878919069235084375964566310037893877002891478997808212543726815805075248/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^20 - 22887639616812625171314899469133351361094839438333357634630114837768662400429223184260683073032434738109801947657321836399038377/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^19 + 661658125232563289930348033159716256203854015513887100196794062996856320547557206885808079559768673134002684741232855160316961/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^18 + 72118885980917636849531058565642644000984374584610281908661120363542401480881300626493977911526555106345859929847378906472826168/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 - 89422703158794737056650295956748455323253986205105854753840728591383269624397835929726305576946853102240909817837269291090315643/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 - 51849601178615593421052899666559177635398556282680394602413943235005873658109137978657937772823545613271478806332590092592659054/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 + 87859569949013541912654914569822895545598498528566325033554131231723425912952238309131117381979181357949707947240625667365524587/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 + 39952569289588910117104393685021406178298166705645516806147940552701699914303880861061065633759267364529053670108065977404284957/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 + 18400689744222336452242511698027746300570348876976130546850522141305706268872622708131271984137366063975954115901878273317523158/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^12 - 84577758818142657307940605752870707016862027605605355197970036720592912681894835353140973875094272228865042574694241714642086915/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 + 7421867665647496669880473272687078193056429168928547974030870662051421056964862163340166939583132949186502262139507011293392659/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^10 + 8489626068148744672277997579005051696605829830972596241380091108235068878963293591064996899424764696876403960174069102434262764/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 + 5894092972515780974982499298110851056387283969499199814210939310444012855576835941618536711255572387589039416217049582474090083/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 + 1800453211526478308517635382565165257298165018922005568057983649042570103413203473870842306250897823039203775794278397873414880/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 - 2250811066304848581953694003573090044917275204023802512379170669542049090934097693852554923312969408055242438273010010920438488/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 70258323353443373965316488014172197940313469516079330536579022909411275953388970086262118179286385716026626600382771886130480/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 + 113990274630054752455688123343255365233721687279523961682097932991989432703544181796119752213137377534952577905917079958075422/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 - 27325950654666935201612580001023617976232959001793929216725708463251847073016277484076008245853417416883483987041628820024923/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 + 2349614725616036199191712442741839884408345356500579315838827120454294683557787913626238389199408444143722571634486204132505/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^2 + 2598790846111085657226693995660694044184373105450393477631484515306815984766290158139900641547935541249838951839747410892684/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y + 249360869844274915084066492532310724329126912271528343835804763675370749686855472430512465807412479275067634109510024207659/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889

-12375257647610532942724580597625658340817207943494059811155554357507995040945689856153638022587352805333566617527341598261557/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^31 + 270935354231900663767703620056834416703800093526369468363120028076320090733070903373844547263602022541900832641001792797038131/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^30 + 616333271290174566200473943320252653865523544952605816123394402128061450236171080846747442178668660692974077923212860943072499/3886554964864130023945513950646225081893192019363606963586876692726996131101903653108262723407624840482747999898453580678236*y^29 - 5025990633591518276790333167117412145214907547260072287977335643940625357065171921551701488036293947828556691003172848183774677/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^28 - 14793242512136958108390688522672546204641458823073125054206416366387854182973744295157814619577585003773188998007116576550936187/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^27 + 74895449332572368972706078128674491332634495021173162405109934073446922988628681020693686734019636218862421579770572964614907935/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^26 + 8601081759389829289709856136298782550436712423694244154447845096744488188716973623352498139505270175919640071141659022892893419/501490963208274841799421154922093558953960260563046059817661508738967242722826277820420996568725785868741677406252074926224*y^25 - 328641803497884378844092305042828135283213847938113289615629011334436536962722784300324314245791701006649924442134579973124431841/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^24 - 166376797861942963292990847395614747731713430897292151742745947928260247044327165910596350589634611488042974659990163070040952169/3886554964864130023945513950646225081893192019363606963586876692726996131101903653108262723407624840482747999898453580678236*y^23 + 3457343494700004497222892481554164018821640189969451123453681328236450269857901058639484730117217161172462457027237577265280781975/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^22 + 2796154654062335150348893748551751474996584511531530704721521306663465540943490578007454302839352065430147594779583181289078451959/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^21 - 18031814028542348408767681570772467602078511409293337244824105916810877969715229680725534238270644419590665808230388765400959224041/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^20 + 7372486731148520902914860758958796193387764654163809140988943969214360501829920603127718111516931754419859547757391134294653402245/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^19 + 25048091692422538540768896828303738220934811025283970473684242488465737407252262487178146323672750579928149624579275481934494221405/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^18 - 40832948783118152371154758238215829679390204661874259617234835126959104482124111106926150846322487200159184735232732745621456075889/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^17 - 10110466130094163370890014939829222285318705241446548559112514574026537821806763226295056759595783481492781494754942761396933266149/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^16 + 77741648943364538039009199437461424619654485838588797245413210155854603896894056708637459539820253935787127626211102522150821472509/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^15 + 15371235885846594624973944102837965372270361702569308720143720932491230898180724105638868165463771838063188691557964660142573563691/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^14 + 560995311899102654945665826373486986307146091177570486893448731573931891451125040046713641607888907632510049955643387235097146499/3886554964864130023945513950646225081893192019363606963586876692726996131101903653108262723407624840482747999898453580678236*y^13 - 65857150121790670840816377708514490051641224831249506619539406114171828881249033976013575488822417571320934853707931196907386377407/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^12 + 20610350131871707925253350875119833815031490016507506690007453741357132886029255466453982311303214392742816992707932370645648535237/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^11 + 3094799566277922468875295861518893492745984719790200981349653475127765642161759621878212657559230582294746676820860117164583967181/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^10 + 1169003486947430706427730518522346508997855204434346020537261941844153770269780491661549915229432505088819370685878730402841778603/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^9 + 10512697645035649211596008161950570361741810964771293114405024002744009275332133058742999972246349427694100412036091732257187205/971638741216032505986378487661556270473298004840901740896719173181749032775475913277065680851906210120686999974613395169559*y^8 - 2029417683276101113401798198233633549129411627490037485023223561811140150173780661684973306411654460100588288766931842691337784639/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^7 + 187810204695798787375265515071257379649235449183051004209379638365701008379752019998829457701531654843435874737059312557641993761/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^6 + 67082653657842501038855782877713636462895461962714862921245711860168796260077416232323613054836026185667634701028683590261905403/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472*y^5 - 49382015006998999440563293111219124116799035006405765581071946593175349496417696238535890559018015194693692235683483272896950949/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^4 + 5346764302213655249752108650006235634238430691426669980064578830009335560597798574884549933672606763060252695902847273413566113/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^3 + 1970625522415228169804583623833040344508171646204971780808904052005249520546279391662368138020719260161743959231396930068537391/15546219859456520095782055802584900327572768077454427854347506770907984524407614612433050893630499361930991999593814322712944*y^2 - 130968175920424159270942087762692145041160538306004041283804121866128687481741167761708976625043501027850575596086285440055709/3886554964864130023945513950646225081893192019363606963586876692726996131101903653108262723407624840482747999898453580678236*y - 27133965438774211789921958997708294059497958535980827120431711232895822309537012122489398630406914440416143037958009196159357/7773109929728260047891027901292450163786384038727213927173753385453992262203807306216525446815249680965495999796907161356472

-46982709165497580995187258105292860902257589172296759595297896017749351344551095747244024764486636336983396027585404941655/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 + 1006656000703770702822652408343539552530649539508299234602299384509638583782713510137454688250107438995784505957615898549846/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 + 9841373773698632409434534930772801456663494601486294345403412891490251198312550874234809450418154470133580340420306178447307/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 - 14733421033596769656724005411883564938513013349027297972984193182046908947028632549847631364581135353474730311526985665158308/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 - 65304046773536103261789724873901692018395302910458741754835620887417507312919284579339191342454370077690556903650215646417086/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 + 542911174121549259530551163675772723031607146609422981511703943659609468662254311719965147842488354083044585596715076929177616/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^26 + 1279201638302397154673436983804706346056695490422264699942788384210284721471228195503154719462671392752516213580838987716717648/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^25 - 2036249358736446057873386352641992821266761944864147536334751860038763708094510902367360748572279587180140636706587422134220369/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 - 3715589555927758809401270114716058362737284638923393155851115329597915432527834933665387776233870482112092539771698168842962190/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^23 + 12001848352468508585953912044998189542456255616593155532507044609211490744350075798959391286283012400039308106584954649027388427/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 + 16791435008745364402205510536154584801685988670625529628653594918450746598783017193106724331061260512025298843997964301604949546/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 - 63802130065744899172684924724023021228194328322863574624956117912979859284917764090978517312573676187618398755419252968955977128/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^20 - 4194689428189940710326418882766331196199494319794311862788371676442135895950008561984598585225677064233001400046971543929651433/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^19 + 204828954825243942066087914664695749422197744131327525901315871621273964739970540360692350987624279295989512730930611350850871561/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^18 - 222161288273324480757728075676921938402621966218263252917207392131714213306058939991182921620514544947485613119556892385027444438/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 - 225553830965714087791608517265558304973165852758827349957168512240248993014868860828933713145194799449388531421541353225320343543/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 + 267176854928969143551447821391472404153122418674325249330179627063161386919351502968763070110276451139430282541300843858977457736/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 + 195532227443076694002879895421432588171513121493979345506576011169501222943783904921447845748660624694369094324704595305455113709/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 + 30863536386439037445187818304783432960290952903082867155690932886818218910635011094299993389297380622296548556908664819462256714/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 - 244987534019507175254768587638858549366376805550690209440422806913070367451801689050228377396857890828730929356839468746104954653/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^12 - 40836637358207342544671881339387543878668184956370824435054403719104662402735009719178578673242727942873178978769063618799864419/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 + 64428620189559623870234638634544081298102716034153093184664199554203648546316549145273922610690082390137835483915764007192376775/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^10 + 16420739420880650079472577131494464725272065909693008597417261334502670456846821645753134241615707738452340650064700188867859560/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 + 6577512559256822074832357822126757682337145004836213589912897723427677307007645914407738580935405604890580347069554994076400410/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 - 7320541680929269688662366811141918795295055441421223515367250946967598548640841010070162036851047278612852591929893566027542821/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 - 2188831037794913423537173188407197398685694744219050954123720913609225734092390773968130694502903265129853179534477134215845956/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 + 1203885133845802377354047850009526441189375169104928335804665700389218234367619148560907669819620693496256939277375447785648073/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 - 92711764474409482246448237340998180796616353033790844377799021695584787953610249356132320591073534083650598369953225389509899/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 - 45086940701920162826739695950608891663207874531434030037588533470039268186445326858493327842061156129722620951165626064534977/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 + 24232374334283880608372027664152060165916639042997036704095099017372806695273262372422448100192111840545080279212323592448994/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^2 - 304746974148446057565559728860294246352967340400132251163206313633226985702641712083667398949033496000339436617229852621012/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y - 503382826617592299900366706185136084525917011351643123472906565729796099342542056180916732010027536452339770173864330612818/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889

13232027963293450155092059682469636910699166690184428928848659414194766533155660096197212313636401325605543321953676410604/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 - 313105999052557327605224933892854065362221865129357974015705769230513709083798309464542661425796668127076121197690967857624/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 - 2129047987877679034805018531402760475066026494910141432311626223594282530386329181109786298668514782100512800351498880910491/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 + 10159550098303943680035331523696767285318079263184565763027895236229816735571306194588697130918326713728608502228373611236079/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 + 7467413048708440706828206158945653244731144670970093153432946433642099494216289720475228404807233077199867635591097063094641/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 - 190075319396106612479281669220547810257280528874600318419286045314353222024370067590716276305597081569747502666619238724582126/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^26 - 9086619019168419517846598707722046707357846611552422615600603788360060764079809195693790156706944082666877637831420787464906/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^25 + 1273092548464323437612273213645389694548186525570649501565331432717022944376584120229785531699916237654251255010815495725795502/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 - 389723018369565989774934096039362493174953058387867977174498751995905985849034119869766976180170978426360031649504746005882108/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^23 - 5213176839388625415722321333151211022001130266389680820322427670570484432159413241539466723427351127695736203557832837257675377/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 + 3160865804031363442477148757543538927012643291594878348027723243127052061954423784167437842161854620408618144955154492261351829/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 26031658672753355489015923962773256244536247731734706705960791462473488245219104879760561421599725984711858976923361226740340131/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^20 - 40249481893941871196791009613655170717479428016780019618028500895736159575821292731404109402002671309206489394505012335730414314/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^19 - 47334960058855729386784086827074827690766014736376741323152818002002263671932592534343860346759121417375341473701789475322101812/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^18 + 182939116095038560301781184470782291309394281634033480927844001391999983140559452639059191698464277551029488070653957074072800602/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 - 109469326658136933884217697741911227274778679267259512330015153336603865176850172618122284040289261160384388039681630231520505963/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 - 151203238787597758381402406042362204925580413879580554640546559228878299951551172016937499679887112003463019865702883187886607678/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 + 110949510592794079166141670740818701682405795830501237092526733736914203947346315932429353166970235529818059063470473282844330203/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 + 57368352187932015843642232025566395967966879250432225244076435111148867496326368800226671482832835460121477762928679826759371830/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 + 92091281827684511132109301176535718293411565243447726771657549275482488767417900510529062969851752948931679414319124912406940895/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^12 - 141516686473102289479159008361752630278647187040699128092812125674738848222091510574854921079290178235815202799518135351872258238/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 + 3347004931085002217766033170235395421327177649248327060386598570565741741588196711701864996878245011692730122249747956908216531/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^10 + 9037372551173441846107703679855796813311275338222583895534173584174426731850340972393732899285480978119165378583415774308176475/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 + 8354371606811400821394516889094812267342617694984333402960606326120560398006671670842970678118515951827834127338886818447634429/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 + 4727406306141013478654832917492050992732604697075640129507759367519028006017910761645251647048963903682638220934698331422594058/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 - 3485364504953201859176010705711607668253568010395889388839632505897107538115788457808669384988932197559380763381027637423022859/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 217926500589298063838506273363101780545600581463858664047504898136286063587100974420330206512771336509368309958776836284636062/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 + 200316837196276126138473231058140542135968901633368811819623201310759887526199981160604081679156923011663618058479267439966033/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 - 45189868830075986762204314794213910663608150533184897277500021010215107339019725394317821866704922536947091935293771715099525/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 + 1190332106452899313556332091611648488981821502034347887689296076598401133401002916179695562996309453929066526589034569906512/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^2 + 3935771679063915660825904886492762518923795416466754898921953122787066289113642446865439968750855847460677836107665090949860/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y + 390307363999019810736301476268138100082810149147803448501816729222928090659239548263426379538837934972046518805941485807887/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889

6324731029398094712040415284911569136669726612757530117408862523806058697116151724116419365087803665542174804278082403635/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 - 123384963345463714752973247128079132296870489514678335918074388746041726055580840402454577856550115490495482300345048464944/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 - 1587063249771099348752474579244182681232831013712406062536068221461531811653919133564049113659138605074824429444756580735974/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 - 504613997869590048302494301962484989359684828415369001792892853999031991050899656810908910457081559530682100445049070664474/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 + 13035891420832626646484000457081638548091308637287499034329242250968086767828492348166892722444984797355129858780553367532485/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 - 57431624462054483268150446155336808004005828093484434663507026042597912438043811307948607799495493153499862205193159329610244/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^26 - 314696057397315564191271594067847223365019063008329178415222491335471289936730655181821686426330121324541208999057785578194524/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^25 - 26168560950211161387193344225426120454926708406188320607452005704043437876749643065219042019441286662561214077107221297979816/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 + 1061639839680687535744700389947098755527160088148426914468458408997189631018433355595315682620377020538366613858310433064323342/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^23 - 809398143724477069940631980211765196057593316745181794234623347366539089516527344685847706586575097135548282303846933230248274/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 - 5423307291772602600860554776016939101332657391368697601677562896272602412218269151194971521367214551039747107759849037485587057/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 4980863246897699319980258303644664861989777027035248448763673128258818308934219503275484731045103272429599373195212361804166320/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^20 + 17231929901755507315560297199438711577362308540401082711119113748136613881564503718706213041168716768076985976702789576025464348/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^19 - 30222534860355669307767283876972841482271346752624608661103699365142458771753291065545973310218327156566886911361507903829788807/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^18 - 19819449703217709546776113803132691690028389322971917170728283218369314314165788337873618803778938104595701285663473213914396395/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 + 96630967791733612218055699329434862209364230508170194542272269966224190027129743621261648000253390933405108525335291895129407806/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 + 1816057006597606841059141319827795294507970203917790974961913218577151725769304466392964915583708173691892396371970839178839451/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 - 91447682396669564006789626555071622391936642993178888777789594514690867565161719644577934651442249183071037130987107652526496901/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 - 37551120993525324371198023758871961438390978374079852670336673582716866681658564972897596330999105745908794655954015422760068955/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 + 21018012575507373047391197689208073438359535804931482868232119669809717061500782384932874001783315709854636038784953144993334684/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^12 + 67227171073173698752542330694128071247708039003112873727142141401277137281901496902535519749804588907828756560315380751505751464/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 - 11680429572363761636783669171005190188516071502713054743210536001503367665194373900514701573095611890448994677140258070705155058/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^10 - 8647622244841745575145364114684967800478819726376651057216121409221862481330341441256325029440077848188073296860186609116815152/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 - 5524634155329142018950657645755521980498196011086423427144523482536169302201575363615168690106805102715021003106103313422135381/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 - 459157579669951792873982350926546414440349917306956498863863799812325235407532632249830241345416847295276529861453978658547387/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 + 1866671985000801377308297394339792568173550894508850493030939430168384602438180607609367810685243452568812865559418784803286277/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 62128179442604958306055143783337342783825760427197250352790389116287361675110476590929956127347454745057267226282606915394571/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 - 69942352536984140464252276895044401090804832201810432780359988031989596714401681554154677277077908461194871308156387518145408/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 + 23252637959899362433324147191707319112575132167961736281676061914945978423057321264327649478093013079862507608574092309283126/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 - 3651902136389751214150162135339938940926471955922592580422422322177504270849345442695175600277395383553930064703912202487465/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^2 - 1863623186244754418814497255499127281081990107906016123235089786510561514788230629113072048386851350547986463273873851232677/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y - 105198139205802061433822146707817528707314291371428371644061953610375919304343388544719594964475891645130471016787168019015/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889

115785650420000814796703224418749321016555237236194722753693742422928930126380546690841448144247126571072117440256391600473/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^31 - 1217469513527465924127150905574634647299319081657991451394390688648757275996504659161948240034762494167761308866773041651599/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^30 - 3154184355627316447655018767359943882923296832422656831109400446082884758678727555770872531841680425834056044115358662295921/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 + 3328867700485375746299453409329533022078027982216356350879669698992190402681296639487525823965032986045705500064573465312424/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 + 87266900774711719498200013227393185801838775672345688017976349116996279491034152954879642699899539175036155665611495732090959/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^27 - 637101562946036710084031864643691352682938929441433593682862674364316455799318442166500081170607174394423228227171309635469067/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^26 - 1838268247087991557788020659802195202167960891211310435347646886887295334754923433845473441803554099261873819907941255885346317/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^25 + 3737407161412440246417549557192632658946330902577846685985221768597647678927648998826762193606471205148884308435499299843881501/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^24 + 10996827745062156730755181569328691929812296137271485210112350461219249255835407568258037315623431488091002986021466303246448133/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^23 - 25934295529991643623023735795149771664699231096426974579392532471887738767088005227116270111626497256786260050550251100528768949/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^22 - 6576858338561985234522995389232413326710527953945441805479810513249892683236881561957128001172271725188150453931152081898606167/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 140336357800529611098965208573849804803904306656403002868552551042557563027531979007931175917063348947549048745322366056430483233/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^20 + 70172905081004630805800193384368667015497418240593149031504685221372012406554212882040292375712703228270102621678428978897670183/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^19 - 248891060618408181570607527175411302179150528088715536167579989391834354597870446629870584734142934309872279350809094048770782649/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^18 + 354661598923968869787887928654360305569533332152060647341529145467209808706252156140017077880220378276615463057207507499570048947/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^17 + 94694563637014180580105780940176282920222571670606455456248454129328007664999818271405279447918817376545856953794097123149283409/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 - 443375365343895174845628885087747351165272974944140085959619823483954684045742263100793970983031320569999494047974983307221131011/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^15 - 349773100206080325414570063172398290720212321843804596308728374522098248826125304335047109745868101811066650980066405609721030987/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^14 - 135054499333911900611897051215577015968260298393790905853706230557352559446202967557643499562861121338889024600834711688663102831/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^13 + 266930458601793167313568222098801469737771968159777191429709389661916181854292208283245751993732872365745898870031871909000394235/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^12 + 81043372746403320457345250408203455975311119673871342875340839462839747010263301986681817819278118054291593754603191129681134607/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^11 - 27034772966230945065488115677005972325061915347320187189964164444750058348323518267114952828759711214003898033835664247147978507/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^10 - 75514009367582430503064206023613862407272412836348050385181166006953493231791230486582469321311645368828144709764300012899579147/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^9 - 19038402873894719825327624130191418986147369812911986784789455219410248936451135652705413271506334529108528372704655180334803241/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y^8 + 8775130488237123525280440500187000914605383494622370845609790119374251162832796523184896413162502881876878426014760312230662827/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^7 + 10301668306395001739448234865753009461913451423505932478770179776428793052568737092782921209697097134366482250622372115031181413/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^6 - 961518672566332574154111668325093251477810654791627905292811935182056526276077529693726949025356830483528544126827022770146895/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^5 - 234981377047925072382336850256939866868071401056870059262617667931805109284189400843586332336771526898409034773289954458705027/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^4 + 14979196814860580384860859265171787849793522969420032153032773941959844713393761537039821130238423094484638682243988404727185/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 - 33681687901628024615758866777439777896372552269517727864555809355867757611299229207487348564815708911949391642274117003899117/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112*y^2 - 5346379316398036577149609591666835559016118920084795941471760831256624222127395333890339152839165175524879183123295527787367/125372740802068710449855288730523389738490065140761514954415377184741810680706569455105249142181446467185419351563018731556*y - 534501980411853370322929703191342083011499313691483578272579884300895718652193581395355371704675917620543590165628437339353/250745481604137420899710577461046779476980130281523029908830754369483621361413138910210498284362892934370838703126037463112

29240470998548301911381329387788951664994623622441629450471392264153656775481213553709959914022380974197388184382330974153/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 - 652551555813855079277210090719085646785689098516199695085555071482065340222942006971905808408523571493876544137809362093848/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 - 5556778244372114422560334770490974690425845220320644345023447269402219970587741619556588491935070038639118430219700287068792/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^29 + 14400394520782926011384831672970133371957468872600955815955520603318643259001370316037872761111677630912698160716069256419790/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^28 + 30481006257522878221887671643327651148917602629037244392352069857765304492981579646930650883393399694764138477217615981434907/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 - 369671283877959463669453899797408335464109545854365876441457651764471127578894542796599986897474970008639910252440198134523975/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^26 - 483668852770744150738555339007747492880667563379002409058947121247847416202465505941288298550440031910381872181324213375040604/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^25 + 1851568307403858212170703512016468347964413788103011966276766713939131025127592290405684604799530959701572734966977756670935076/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 + 982316632321365072123488707936128140266645655073412477854862429865712252790497350008331519949021980970790344755589159502047277/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^23 - 8960533209454763829627624949941460751311630321320228785199447154442710573623998485038539135122290679045606264584888708637304776/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 - 3331455936647586472845515165976968846841383224351155400485566678548733072406308923335501384594748472821573114355778970282907556/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 46111171102471991802243843525584115878696354695463860683965876076581345831445404058017250060696993851496354949262129589039328456/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^20 - 34641430645737435210984720126749681363855668960650357394792929794067734536627548598546290823671610358398908880807215569459979099/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^19 - 114725888945307889112569760397682677598979656619448997396405874669080670558701088560197994934231614793922248384744572403467686373/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^18 + 243603010068797148526773665738940661561041471952554026085228923435028043660246016741562683363247116081609335521405915826083005371/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^17 - 22695965308412468311360413505059846374798271900196898259378682415867759512723063503025233780716404941322787224531963559082203039/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 - 218604552453482822000409668123863791070370477882392073835089938393748648206840229203380840871363312015769939622912420144658872605/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 + 32484559722466944639913761148825656631998757692814961384313509238932575993336933290711820015851554213618368225443656145386165489/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 + 25048315562944170666541408665981285838308335743493777812738608488294539882431880478214154388051602402781220080306674447137864755/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^13 + 165717366318179499453694799933411875707046105012440579328869549875997805720330936653550747931135656648697300275185371826832196910/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^12 - 112307867365320608214519213010475578022906605958290556909362859607603066045088463339414855427791813232923135551835529265558520678/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 - 7986676201927338543068935141049214260471462496211908895800982498954438265486111688469322671010884802131662095134276907671491743/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^10 + 1040309402084747483471193242838764480352474971466346941588870946319058118521550480269288409634139411375950660426426409612185566/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^9 + 3861757600572439028970861290159882503916032525821016288968734513999056188294171562076676875518741576518985741723168629189032234/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 + 5971698633190173073153620469256359587801394488671601297616287883686456484767884132946370544548016887252467797514829475368799736/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 - 2580345185460844491046445029190050140888317911767981254703790787495657772404396782448442531161965896323254412725556815096768660/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 332565188669025856868631601051051228290812017153193869199970257772156221987573946535991979902159214063712118444648936005937741/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^5 + 213783521576521838580884172175906420516979902754041671913212056595149575025536992101694173446071699541043314445156697407674093/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 - 37044973005225020576077953719289939533130113566364388962702480512150470154525691829303211506349816093749868023568427572339226/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 - 3329633135067322765531935236261231052507115687024665623140859318544531359472621138825856820467763951852217061158644932868470/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^2 + 3243395009464983963291201380493768034314571783094595796861904832215282167024474978987601787955830783772033449185073398705927/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y + 178876315814376350292069458761714303633457655836332859731772553496743385298295197684240012794482867107582560513026433377743/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889


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

# B Gluing Matrix
{{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,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,1,0},{0,0,0,0,0,0,0,1}}

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

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

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

# 1 Loop Invariant
1169574222513673406466929401766824531876088666923495803120801532488680182013982678881586084353304890185777256313713359351753/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^31 - 25372653240749199626875765883402878546177436816157924651300222830590643982951942934405064029663524810445995321600204394733898/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^30 - 476314464590065046788311297655612800155061490130824007335946824615796198279034453234711183088173598764009105129066905359722107/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^29 + 859443949909631994394874980467323080296992361278773123931302882614712621716244382289257737810316794706614211133774291863283277/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^28 + 1504606023308932808221867040956572783484579840155123513840770413936431565041081599886366685144936797089655722169175164786280602/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^27 - 27785306182988353370489729414880429828457162735355133457851114505312466759818945861314240672889864531120504786940832718116321377/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^26 - 56195774696390781927277185963264758911097610306349578480469589126709424785763504371173147934771996853372855423751342963762626347/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^25 + 57715213720896933853454886191856901317950584378681721670317529152784884209317351179021115668293268039889754642315614744173697206/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^24 + 153761179056963108392506674968521625754884319752864310431581491907162605501272426302567107947917941418893766250213312284787872017/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^23 - 316107980852704329045576470242030741276892142901538672602395346991169740981640913686145585464857480179287082890008796272982148668/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^22 - 333667669753494174997968665834426436122946744198282516103335148884565155918334986505287593680070985148367427009705187649292297866/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^21 + 3328185645228354396076440032094331894390958571668394240682262783954249438512434779918794023097942316093504406423009172030179908231/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^20 - 672239403375524253310302067615563663215578901496043103428815955456459034250343272093817681530463278564354502370729995439087424179/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^19 - 9880741818884141199661980148583167904349467379732267302860936993801351034551832099501274883253691575178228716844051018713574229827/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^18 + 13525569191894321313707119687072436052097135949181221975626211707898266805332562467520389230990454222158665268662917094270660112303/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^17 + 3665672206857749452619062735438050229424358116179556717838351583871912552336956541827548201923002783858430334657767843042236569060/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^16 - 7187159102262856770922566071527569017362275711029471113188158701123664351507777147089298276717674661423780684210214037640142557315/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^15 - 3151813839500896860863362167193822826788405746231394482910871164487027379961824178942213536909055520098596731010682679302302678529/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^14 - 638518539363189984214125286028201191168049887486244516483534892245973909409362192607243726487169859471219938619290496433969131947/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^13 + 12768058858462099493808169066553060051335618988174475839350752759933457044546457361640636812243863971920227053532182155600554135619/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^12 - 550961276310250555565014596633266670141671076112103405063875596874628414523083407669830328547407913984935871603366005263435859821/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^11 - 2360094466223483270764979194092427840912154847351914761946618036168904740773574542804184918300275243240098598124296073952482807629/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^10 - 785984408517095873354182585314891607691037929943464493667336408452332729500864897625100599119113882888313093632227860742765910509/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^9 - 75949292766640841608392724643116801839285779948133713292523149398908474171885999357131284979026585475658392854360399977838100984/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^8 + 202831323513034250215973385949133442479535336340798556650022639187463569557531248522934651985861637504082420187049777912825482333/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^7 + 16144885317630415389052874487305031618954959197706035978394987419791096842685769504205298537518942638835687513387431307404874524/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^6 - 40619240572753835969199202271460109312853160419813483664440206510169976106066270910612607288192921647210863551526316059123781861/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^5 + 2346547071284198067291975158562708441649338622385806695033966266158180880923097296478398290611883115965123153045271107069766193/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^4 + 347793221662850612453583772280916129708151920984806293240407708450197205265036504977841628765843838068017836206051147859170386/31343185200517177612463822182630847434622516285190378738603844296185452670176642363776312285545361616796354837890754682889*y^3 - 786489377800989460132529156026152277734453318264486696133007147553637019842620991465740743329381720280174470798816051144693771/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y^2 - 11324752238387717174793932521270327397873274706993660540084284460458340078181932825272434049589365254329393666625944331258709/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778*y + 20143116754525246141507241553025916315609306159573775364640196841221789945588559188703281767632944704000913868862809451989211/62686370401034355224927644365261694869245032570380757477207688592370905340353284727552624571090723233592709675781509365778

# 2 Loop Invariant
15606562507723884477954640537621159362842670222855031549641095361163688708757212029710445692550640699121100779910290653621468203524698579743224015996854156087076635377401154671479322960792978384199375737803349303837111599993218047203999/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^31 - 343903303026666212676126837274074268557695202765969148385677805271854668952892334974093316824257290618161432972389776445235534297388326641553687406540782498679249617914823851292212005400227581892781604254697565448375061877176456554396657/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^30 - 382738557628548599916256601731526598598119840351337970906146386195200055082318342447595370506446619349724981453880447452879967586207835310875976697934826711938514652799991495877058605175695382617114912717399392489073232900776121696821673/31872717181275257862404634585548635215054111512960354666331040431756854814262305658349419561742246679175587471721252432714739666192862373078845963719376583279164895618363640897696707428412292771870042491416299026216931700698053513667094*y^29 + 6814772812881381664736573989196319386370793835807725587480164858743928531526863249734868292119076608903709392128708629493796192716869675840601840684411591469168408902573781504095487316461652014198398685761747470430483235551789900539648581/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^28 + 18068032292464918009180832998546962591692150401727347660359087943539923520732801389638063110637667237547328300194027956103736650226919115803246059428220908814026420247533448920632239206564174359476738344341942020580801514027662426308906625/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^27 - 64036511973015225053962701167416044681627685662246631008640522606982264970893646886449207983745724964289093988260346886596313405066875197778146000656016389610322450031639314140800503561953094040599284070125456594693983425328678090531801475/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^26 - 311299539391810412681383343854326935763776515413183111113024300703911199916286088277837738575181130458110543013901471172630757898276542244244153161413420755191896434455776710041072398566950867878813175418717982377425100982159491281055913985/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^25 + 447495365193227611078343786526481334840365257669889618788541044157559854668652729880600650604384162288209775176296219240715321159556536244412040257960147330411584280258802656481831066797699912215466972883619370753793441841175511894838810747/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^24 + 126456575110689204271537730976232311186926765438205962978303429187399121873721110726620247375123629671358863011341024965515957229472967054992005744143913884170619959845686545009966933236152960691783637862350006744661207600887926994653361623/42496956241700343816539512780731513620072148683947139555108053909009139752349740877799226082322995572234116628961669910286319554923816497438461284959168777705553194157818187863595609904549723695826723321888398701622575600930738018222792*y^23 - 4551686646913300568969808564735318468333153827645877922713903223425522025636091747155620833291071814723565930922719262034192926678470305186129388692094269875098655630570762846314260962584852552216240100135270522788109335546075511970134264877/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^22 - 1001332620338630859890358469159853955015875430455772159843330401088161881050308466344797414142218015619518564658948942001266736851004692469765849988174728408886958966891355486229613168457911547656591463647499937750693555223366578126267372607/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^21 + 7882044924462231718045301729019453179808798817014898197301714052135570538164887823395919518492883648059470716678902844262257175916744621253548153783287395548573833352172275935694176325355269341296548481316765900271195088491667915902753807987/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^20 - 12094769602812522768740774857759206516172361058152070763563319737635048460368254430391415356455761673169105380073429479494836289851640468837063977957773440875773303287036693668685825393366851660617525015822387499473391358450060545857654320145/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^19 - 31986936643373512331951150805802321316675001052249500889343448579833849590915988364803589815280452960302966639820074710034841883310094833253040324577527933653447490602809085376636741778137732367222933938827343780063734278536533254903287047701/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^18 + 7025611969633055443655011413039661747990318190999805465483561063099754852469630462392804414834313396428534211965274244485462207784707398138026384568608297961194454516896774898940356234448226707615945989634474179331886850795958702392900925195/15936358590637628931202317292774317607527055756480177333165520215878427407131152829174709780871123339587793735860626216357369833096431186539422981859688291639582447809181820448848353714206146385935021245708149513108465850349026756833547*y^17 + 2846486203590110328704278427867562804321156507290735128588743978789935125390290399887330050391461273099903274871027825157868460736521288394282463077708675977551080409817806196912206612989340797793745060496589813963293402711545433243555246345/42496956241700343816539512780731513620072148683947139555108053909009139752349740877799226082322995572234116628961669910286319554923816497438461284959168777705553194157818187863595609904549723695826723321888398701622575600930738018222792*y^16 - 110296401311065194187803396696330112125963022494452940573041797533991206393271664275971704034459382914268923867967367563542158279886088074973801352880117742365354313655430977282273341598374204557384007129458786498487176298992200451217526750987/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^15 - 3259656787770187129476793244610437049364479721229881075372492916176660703330403947646654107385634636272223273162307181642054692247373785582092112459204281082673861797531299854944895198915882841252727436531253174573336028984795358911207388303/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^14 + 4077210413258706098753513384557152668221651365703298838754567821705574417629259741688043885809955599806927766085729912131400128026746358495883583632767480032032264611997068575850150318258630122518365542082764028397440321250862104328875891759/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^13 + 87258954710332477220993910889662150471080952077531491650567960494876924934881481017309144399281670010800025107487982317851041361195877385554756606291042772938026760508887742188727075645441358565555609063533520865292196967472716853743392112103/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^12 - 1510334518827662712412171277155717383905627307494570123089759237511864992834721348174314241277489826673455471195813345655907555809668396352732840970529509513776310714246346984383737297306542173565920781638025906220901934174762637762259957501/10624239060425085954134878195182878405018037170986784888777013477252284938087435219449806520580748893058529157240417477571579888730954124359615321239792194426388298539454546965898902476137430923956680830472099675405643900232684504555698*y^11 - 11831265025110721568884981920170216932978590437611229479143768428945519925399940331029334790627862326850067768661930282022161309635347949884120689876796615629107787632418793515770212076640653656799461427310006440789656621726831804908300140443/254981737450202062899237076684389081720432892103682837330648323454054838514098445266795356493937973433404699773770019461717917329542898984630767709755012666233319164946909127181573659427298342174960339931330392209735453605584428109336752*y^10 - 370907979428016286304392549137386422522024876381334709803047305561869768468646841171002300047737414214667136398575230914900223200508826703445795434286433007603417322639475688534478569456860393722329889943395968279712498400311988052110671127/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^9 + 51682666953176705427982661462544296415028879494517614020468268297333808617919433961620098359530750506243168798141769375463550382424294121202225876267064632947660924180854203767511511710492156353751213190132900479670586902287228015922899416/15936358590637628931202317292774317607527055756480177333165520215878427407131152829174709780871123339587793735860626216357369833096431186539422981859688291639582447809181820448848353714206146385935021245708149513108465850349026756833547*y^8 + 195046639497221688191006453291286179792536137829283170237184405204597392945881751230175447563282936489748374675332459740984239857710649393618218578737743978925415686939805167137494903488312289962866676446147015017096255756295530837729866356/15936358590637628931202317292774317607527055756480177333165520215878427407131152829174709780871123339587793735860626216357369833096431186539422981859688291639582447809181820448848353714206146385935021245708149513108465850349026756833547*y^7 - 334124113026558439612823925757554209881245974054586814947757855127377984510481862105810373439336791412191953966980547517796571701959091048753620383957648696449337463841206996253716140820452037758995238301333107412624223074866450107546410907/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^6 - 12428236483338029772367065794643324889435400273683954801267968216873432167122666574821291205143777512284433169632689430952647937216370385497031859472280003211392095939773455565085678981410558937941164525136189340236583432681051413575836073/10624239060425085954134878195182878405018037170986784888777013477252284938087435219449806520580748893058529157240417477571579888730954124359615321239792194426388298539454546965898902476137430923956680830472099675405643900232684504555698*y^5 + 44233040486094229536221017260678527700617925321192853567895903333082872556167871719693411620364449194978677832618253810815745421212911106399882745766212167190360482431362159869623302499514948790347528071546978871001510694134114800686277079/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^4 - 2634545343972073964250953496328763636348411428324530323768674226750923989698950747741864014037878034484353104075338096934586176424966513503177485949311856569870249059108554236322769705058407510881216587981924654420514547203089183629292677/84993912483400687633079025561463027240144297367894279110216107818018279504699481755598452164645991144468233257923339820572639109847632994876922569918337555411106388315636375727191219809099447391653446643776797403245151201861476036445584*y^3 - 1925183343448368114218973797793683067407373268002600969767999710454924035871950644703556140038897135668554164529394969026715540560082461024129372249899207714639367269231065471751373052451795900353155508243521543882547061782555869578595895/127490868725101031449618538342194540860216446051841418665324161727027419257049222633397678246968986716702349886885009730858958664771449492315383854877506333116659582473454563590786829713649171087480169965665196104867726802792214054668376*y^2 + 111713694652768773465305653151046736524462591756339659889273291957905188607949794166084573466700879426676394998307767382719580166965123526000371055528975748226291961134010925948962064023218494265293747359092994321139033010589247094940199/21248478120850171908269756390365756810036074341973569777554026954504569876174870438899613041161497786117058314480834955143159777461908248719230642479584388852776597078909093931797804952274861847913361660944199350811287800465369009111396*y + 58643784207027244325619372936250686379428578659173989661477682722076368693152340728574420620871242386418717757152123592801879172958535739375999291363036516667521396910226323620389915429774341631904279447049371806413370817917910952568911/31872717181275257862404634585548635215054111512960354666331040431756854814262305658349419561742246679175587471721252432714739666192862373078845963719376583279164895618363640897696707428412292771870042491416299026216931700698053513667094

# 3 Loop Invariant
-127982428577432260294649523175017854020779549235212100036498837593999628748595325331806424493865479329300314468464280173607599594167667944982059258442020296549969149731219517145910623122085100544238382185875102060480533856554336502081758402637849227263998480579529113061544167110851552414365/17495251123072153689593690117111551114452610137342605106493067879948893986795265574106774926915635192981114852754020040758062578934212293671784659915148517979781027100231344276995566860936650667561023252317475066672648434943015989736232640108960938202832071750311524029354177868152773192892168*y^31 + 354568440245537062326754937562840721105568453774115178806234654080548202126303321818032352027015683144530201521171564952205187918976059341336980186056009473767012060021715167234081484597069160085974055466853608371789108026014052308326078798417221494225868458107692512057606858580833810808528/2186906390384019211199211264638943889306576267167825638311633484993611748349408196763346865864454399122639356594252505094757822366776536708973082489393564747472628387528918034624445857617081333445127906539684383334081054367876998717029080013620117275354008968788940503669272233519096649111521*y^30 + 197933741006752240810471476874581693886930040800531055049232533998239940861474631798345847874846578885648992919067378806975557769673899468610476886271393800133778766125713066303707351891704812134892571361334204163049285428212506634367867243288352789949170708480495160281589688634621475097348527/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^29 - 471451675502876702291174420425172985065102126727238338667803115744306859550276538272860028626954884539296720215878072371960201731916314929396052652769978681236548011998163973679655825272008324394584057884397784369899781639469376273278607727384341310981349386338869147973462976791130994493466215/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^28 - 1116729317469364867642830209955016850969206034555230086756245641003192007164171575957078779943464600305297211960862862228231860972253145373438609643711451420166429164784807528455254138836715295460489564597548028323431839039279109720969498585587140825081156048024611716976382379969429096981305413/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^27 + 12729437585839430112479270265199481495440497993921066857127886103024360024101222996223316315040041281086174422515817766810442846880513973275443276569805423889114099236587944516849625385469359632292922099127774795314730912497529564151026168053641599658375725223662365305715896354440833209200977773/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^26 + 18746701581358550438811755928052780972398492626550865557375935853333185722790809439006055985357185618558874820092758147997730416943157287848350620112163689533780771120756454512862963656173279872121371670249207771686909538133022942232101723014460542339028451797332999182861621135026398383726420551/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^25 - 60607942285505706445264521418843076284371699070227247555887488062564075631943637334635936672541270996312678098641191299574877932182779082802619796193578676827812676918600528056673071760754031834031671166550091361069472014826949123840945945179785247038874751304877254455896428291044608028893412023/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^24 - 20556972011641627715950244111070692269157719753142982760686548203977913531449965542396193571889359924845228197357038991324107922449830351483538867328568200406396233009114051620733226274996576636136223164217347240753500436401185672468817016425046139462780149370288540854712005719827565528225574109/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^23 + 4714906447253262296378187361861620367974496410947578486333268814724524202875193611251829710912304958223390090792960752411688199849070907240682610049196192190531937471339246600029091650273255022327437562761906030763310522300731167325140439630503786427085657686768122576485993428563752999920193053/2186906390384019211199211264638943889306576267167825638311633484993611748349408196763346865864454399122639356594252505094757822366776536708973082489393564747472628387528918034624445857617081333445127906539684383334081054367876998717029080013620117275354008968788940503669272233519096649111521*y^22 + 78157474688682188600502667131717954577770685070592192316443400213279995200339522399926129835964078192060652259020000669519781329725900634214669711806504661254250467866678894939856747991228964327713151075596636379666717521241077204055890236513469953950257181199630480639874078647230456463368320507/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^21 - 194991751875068078004073602689297115832803327079522736431847447351138368652540534123284516934431104174745518900053777698942308015280156111376686715399210611195660930158208170511136568431738655132254776016308343421315982008766151756376070922607282707559415192411637321933245207347507666654891678997/17495251123072153689593690117111551114452610137342605106493067879948893986795265574106774926915635192981114852754020040758062578934212293671784659915148517979781027100231344276995566860936650667561023252317475066672648434943015989736232640108960938202832071750311524029354177868152773192892168*y^20 + 250602676256487928884897163802121200837507303500353758237061997363106116928597490717831738714401662190626471204903331003074409109606890873112011122771971638268328937216367732350859005790692803912474414830097805754513474463280075526415927491163393612193446960589013243723758904696424430776931425313/34990502246144307379187380234223102228905220274685210212986135759897787973590531148213549853831270385962229705508040081516125157868424587343569319830297035959562054200462688553991133721873301335122046504634950133345296869886031979472465280217921876405664143500623048058708355736305546385784336*y^19 + 4009873940074784639612747883175161606792162985705893995939023590978521347621214844475692412565855277768934151082179870085281514841925203422037910228244122136624950536358158805803452570227426016058753632493252366231529077281137308127560468813075863695445358882652324053056758139412257893368008064007/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^18 - 3931556393543127019398963844187373124837225579774907784291346404193495305526802778849573093017047861829973701842032760021830148308333074377593650484974987258986588690795611193349471924760085709368492919430793023016091491761586222297570726551051372330971576436767294212808458253920096901546038862751/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^17 + 23433207373048213073541893887765771458214670687409652945340637401078086849455475898958524905573929802922309567798696300791156008062284348952333372855032418603376925637773608576230176001324765674234987182123572669028841996317773659082035541992715425861815387740567902844932321545261666751338176485/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^16 + 870393265631255066251272499708412587385147498406359956757332858635002548915441188318280261889723693790512448476044823881090584441573894554090703674231535826074010332208186818021117600179458677448230835120904450108232959762433218688220367796609720649905842933646089822016079669430824272355015277471/17495251123072153689593690117111551114452610137342605106493067879948893986795265574106774926915635192981114852754020040758062578934212293671784659915148517979781027100231344276995566860936650667561023252317475066672648434943015989736232640108960938202832071750311524029354177868152773192892168*y^15 - 153170922971714013051402785285091829720812240862198935226877485814485578849309856234025236894736400404157308943243766866638154625773982031231270877665088941287225031378449647516606603665393855259703296037831004083584295350810115619676449157359917921308656586678673969960404160455612269789493730419/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^14 - 267970385561589202780847111643554939648679940093345381767314912519037504739749471184907542515780706802517107288301379800109158574389286180101942944112743777464990010491360151591973094833954758289598792842959620018085660315062342463571628636101119171077948526648449059339303402477445738987802424929/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^13 - 5642497809909373879925706503116829288887218428792652912547964128192132748832030113332592490716735577516148722671705152525226730299756249508958576173003637074932579102459830815076797227180823664740908472948391617511191129510997622726979244576510485948724517647649571637180584278173789416525703414653/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^12 + 3136825328574908007282363229755680098043373726859267808123988879779927846877476039805022602421798302293751423131821124276382246299390976517755876102799021822301806849487411159234762782198319562127868746466554335696075088493936742639872331528357381123112758854175987063442469167115928725596988072735/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^11 + 5241179221545599905652990541528532523565985451503600078625714483559749944663847560015073285169465081059606366053766670978678795836796440084191578647070321906361082189761934416617697610861973387487539038641387493884160319584712299786335830054651358199879570915142087284879543237640410483550392223/4373812780768038422398422529277887778613152534335651276623266969987223496698816393526693731728908798245278713188505010189515644733553073417946164978787129494945256775057836069248891715234162666890255813079368766668162108735753997434058160027240234550708017937577881007338544467038193298223042*y^10 + 7518143899231788286308335616690840623471550412440004849353966606851524214200790252207093132460719254401716921609014354339862456936435485175842718663411842566085500806274065361550310994957810896111654541835965348315761689353436407384127906805004180558628945802421779628281636442694313741360649331/8747625561536076844796845058555775557226305068671302553246533939974446993397632787053387463457817596490557426377010020379031289467106146835892329957574258989890513550115672138497783430468325333780511626158737533336324217471507994868116320054480469101416035875155762014677088934076386596446084*y^9 - 9061881044244004224379802689474238761736755129961112030785573582419428628056045919423303564065092853543578618873747666361593811208952102328250755812269756386909953031517945626320707885745889112791687654169276229088233733300222563837547667539407326368845981452519886135386074471126174386848765831/17495251123072153689593690117111551114452610137342605106493067879948893986795265574106774926915635192981114852754020040758062578934212293671784659915148517979781027100231344276995566860936650667561023252317475066672648434943015989736232640108960938202832071750311524029354177868152773192892168*y^8 - 184347997833531135656807929969299216193914262916534539849888293953219545664618236432330781424637100573402367305256551853669463668185651692539404700339539273211168933635360292918288064571194764696684599036041377641594226801370594827016359691328267724451156997065884250539418177124570014508072415519/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^7 + 34099858843221044712101104040420984862812233311691852975999222331281395100452725637922239071302381914157593739129822019436026344569158033548386728475183217472671271898255005662105561345917705973907548664051558337712113160084913388454864423017357356941919783280128254948073635480915434715720780135/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^6 + 2871975049078802882993646791414444654905263517254498855850415352846082011691645138377950965277242561341591469117037712485285887248589146868708281280156068896748058756124124029328192678936916972271431751600110119450733208409680791864666412317241438477708222674104120872892194599473817754835528177/69981004492288614758374760468446204457810440549370420425972271519795575947181062296427099707662540771924459411016080163032250315736849174687138639660594071919124108400925377107982267443746602670244093009269900266690593739772063958944930560435843752811328287001246096117416711472611092771568672*y^5 - 4968721217997393973423625140364877892299664432595504085406283833512610713162860621681499912920627851918330519971697420144257909527455151418410603497406403484460409958815994225104677006770859029318084264268130404844142179346706842431431844114785462254202993362608336390070755441065369276827341975/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^4 + 294587295084274564950690038397985615882320398392443863296865517635839318240662623257823859985493331019936533292754153599202887965041537519312549246793534462083650080518223237813791929851589229231669143205681733001796656576900060011422637166198882440022625821112035114599997256023551526551270781/34990502246144307379187380234223102228905220274685210212986135759897787973590531148213549853831270385962229705508040081516125157868424587343569319830297035959562054200462688553991133721873301335122046504634950133345296869886031979472465280217921876405664143500623048058708355736305546385784336*y^3 + 49161133832426706094093527142486777121160503161676302580113053109293600054758043724258980607420783075377084867889227660538514818326535085806959443077417007579972950379360403523724336170917367151231492144603456594743445896548623444525532109760614645200120981053122950491677294190440152897639049/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y^2 - 65295240028199739292291357613036842015092161439851683495448238519374023624300988915693774980199713032615307305888402383662605897599108419332916670526988237233036045014192849375984743210235226956483641367091391957137268822853803597763081807044650189391802141599038262475319211788934656300778595/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344*y + 38360252624073884985637079943737007709070472421954047770693016352113422280592653523755023013257649822895138850790164313549251409601497497950303814688980822151055231862580194643678720545227556324612960033247928171494194277933569511774469550968495594974875236587841329302164437738542004507497/139962008984577229516749520936892408915620881098740840851944543039591151894362124592854199415325081543848918822032160326064500631473698349374277279321188143838248216801850754215964534887493205340488186018539800533381187479544127917889861120871687505622656574002492192234833422945222185543137344

# 4 Loop Invariant
39013291825836509532892476403073791903078746898730496451435270082149938835423160910270108226654934047181221291921925243828994725567397548509150355948081353420346255876753896798188581766955399172858874067215689181097433968468868140053436963199593430422422947570917956519620147730849778097214968073514754009906601430392476159078706802698411713404696537663935357753959391745378207259636807323957965331213042301/4269798522341879149986286147484972204561146137505879302230063739237739146487189302637415392558264375625209956279735343238064764050554999799303945664163248779956930548537426276774442831717985596589182983294375832336421059156677269962324731780700895050112358654595214250764472012779285080601793735157430120808337212545254500891510622932905434912435677533475445798046642068101202268943595707857727995438221630720*y^31 - 107453079983605598408461252548265978283488982527948376964543053569099312709061321166731788527186862270637154634099801463585698579681963637932950763690559833653720195970930121041465616732243970795044127972221369638732204868929901489941459828312469616871541053944405764876537788037780612169923084095682172078334340544850847154736870449750877632717152900290890558163634534573218839441649345738279595474453102403/533724815292734893748285768435621525570143267188234912778757967404717393310898662829676924069783046953151244534966917904758095506319374974912993208020406097494616318567178284596805353964748199573647872911796979042052632394584658745290591472587611881264044831824401781345559001597410635075224216894678765101042151568156812611438827866613179364054459691684430724755830258512650283617949463482215999429777703840*y^30 - 1020486388100239715238937574632185952072787032838520946259641128811506827110959687668203140037709972440762937076629913598702270661407245494310888447146484344350353066308434693919052906534074922002740272307548150580988538125834451707199381143059656193525774664251367381292988208758206479339650156669734199128601381920732302153022440945308009340585166517548581022633505626560494452104103010015523417270146691437/569306469645583886664838152997996293941486151667450573630675165231698552864958573684988719007768583416694660837298045765075301873407333306573859421888433170660924073138323503569925710895731412878557731105916777644856141220890302661643297570760119340014981153946028566768596268370571344080239164687657349441111628339367266785534749724387391321658090337796726106406218942413493635859146094381030399391762884096*y^29 + 67921677153541604824238134474834220498782130906274158688007061724289065064522348565299080782536203901184086573317909961857276434212253272336443767608646747351433152477992512622507060683855195567687250564857979852960242054254831299155749769323519837154787191023750171506577237714126357458538788235282549368735646150961338747735039785407024933509840476536059986612051962535384448123669679819985526505263746114319/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^28 + 7467340770907021795574371859027480060725551927146949100577613837102850469926422180353081435141922995803144385538819514598092330283648945450597389493350658207981764771114739156177363354638223275418006965900914669613588661529935501484369193217779047169350453238820534587271302903326784609838238236640296419675411933188242876425663211462203872162216017196963840275103937019256106902057089718158167024885424303323/711633087056979858331047691247495367426857689584313217038343956539623191081198217106235898759710729270868326046622557206344127341759166633217324277360541463326155091422904379462407138619664266098197163882395972056070176526112878327054121963450149175018726442432535708460745335463214180100298955859571686801389535424209083481918437155484239152072612922245907633007773678016867044823932617976287999239703605120*y^27 - 106534644833963830154166162130931395977632103884755850556207010622860751386458927452476327280177371557204011023754425823574000276131903893354895890569913271910944189126842654794483212419889568040731263326264526728611064647534827960585796590130505347412974736876333327425266078187065596550575978786188534358508226448612821999257481257111835001288757161804980804666217085743500914698144207500961994721990320641883/948844116075973144441396921663327156569143586112417622717791942052830921441597622808314531679614305694491101395496742941792169789012222177623099036480721951101540121897205839283209518159552354797596218509861296074760235368150504436072162617933532233358301923243380944614327113950952240133731941146095582401852713898945444642557916207312318869430150562994543510677031570689156059765243490635050665652938140160*y^26 - 172582048168394030514532787678236404984136247379836971760566239689381423790173714007765718014999905313238167867628342355379098412171809327977175209506428148157338128337294456966029486559304315579318861275212082816963742693967693403209414966734337910742558461725124470752141023739361796963041239566463963430046410297957272319789562581255503933395012350864453826361621116553360633765119345475531464879996468015069/948844116075973144441396921663327156569143586112417622717791942052830921441597622808314531679614305694491101395496742941792169789012222177623099036480721951101540121897205839283209518159552354797596218509861296074760235368150504436072162617933532233358301923243380944614327113950952240133731941146095582401852713898945444642557916207312318869430150562994543510677031570689156059765243490635050665652938140160*y^25 + 1106355378512329449719440523328211581911445817062009583532770150832305881385549738557196263789327020295355878271718279789557674714334480347234728110745512048305305677714248749933792200980991549405190267293583064241837628777220968667380391406389951494735789078530934162488456392902548645617792278695358831308492081399862212843947421677441262529576026561527088972714615347990293222154622458758683563307980057935303/2134899261170939574993143073742486102280573068752939651115031869618869573243594651318707696279132187812604978139867671619032382025277499899651972832081624389978465274268713138387221415858992798294591491647187916168210529578338634981162365890350447525056179327297607125382236006389642540300896867578715060404168606272627250445755311466452717456217838766737722899023321034050601134471797853928863997719110815360*y^24 + 7426745198501278137473874038209976957767008042142115731645155899319858495081740479180485792962835237819952092564549693147442241030607560751382120229717098148008732174668584411194354690779754509049557217842514530614361831141827161884989176856344806190287816616129937855061455041377405135250675665793137388916977471810310233182738063126686320713784726970236560336702478639219597202354986418611681411384173933516251/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^23 - 11276826717784054786395662667083166122840991061091864357643965442293429441634470211745552068393114385795504222714564696692247994755837089794288559709471819045315001360761549167920434591988179236757730255865037747545648453213802877831095246076079870615456588525256452704487094470608718406512239836148548844688182887617842379699567254706361610074968323652002288545167527930798866019682883149157201500269662826515877/4269798522341879149986286147484972204561146137505879302230063739237739146487189302637415392558264375625209956279735343238064764050554999799303945664163248779956930548537426276774442831717985596589182983294375832336421059156677269962324731780700895050112358654595214250764472012779285080601793735157430120808337212545254500891510622932905434912435677533475445798046642068101202268943595707857727995438221630720*y^22 - 14835299280945454989992091112503392904218062872600178403767649454241054589794055677744944691647158690925102452079202409375147198725718514818876950896259991711860867258992036321196484678167944344378322969362319900638992564872237961004765146519224936256764193502051085327704826005447563240218496355956381889522901786536504355345891706592749446452167552805909094466506067295117305123064687036990505616758023971012153/8539597044683758299972572294969944409122292275011758604460127478475478292974378605274830785116528751250419912559470686476129528101109999598607891328326497559913861097074852553548885663435971193178365966588751664672842118313354539924649463561401790100224717309190428501528944025558570161203587470314860241616674425090509001783021245865810869824871355066950891596093284136202404537887191415715455990876443261440*y^21 + 78093046687285107106545676837762066161812831049925945420583555719449948801055222056807826736798829216342905861749117256487569063760218067959072744212571000913084904918166643169797386955871751697134809492317147040991906495216764458789250757760110461840976961803660810626194398807698153051758684647874786443381057048171883216763505185977690871052626740126302659335906813515612555319506364818268660205603098303561053/5693064696455838866648381529979962939414861516674505736306751652316985528649585736849887190077685834166946608372980457650753018734073333065738594218884331706609240731383235035699257108957314128785577311059167776448561412208903026616432975707601193400149811539460285667685962683705713440802391646876573494411116283393672667855347497243873913216580903377967261064062189424134936358591460943810303993917628840960*y^20 - 15307365789269816627399037029036688679533314765235028913819454271475572773747184530203669787966615630004559327207149020203848578639353824516018531377581080490185961759307961231578287581546672138596501997656830847712695163933630129319821314958680103481804851434719243498189493685235210234753433197414901414984620217295093406213220416733129749582877619343537951448786865857177112752839887492427811659109117877155511/2134899261170939574993143073742486102280573068752939651115031869618869573243594651318707696279132187812604978139867671619032382025277499899651972832081624389978465274268713138387221415858992798294591491647187916168210529578338634981162365890350447525056179327297607125382236006389642540300896867578715060404168606272627250445755311466452717456217838766737722899023321034050601134471797853928863997719110815360*y^19 - 628834032923151840220368876636784862467768996651928213918907182361374321217532037181860005825130247943419911164665955888868926487081046627147100810575234838936738003751033442097420658416543263422225337872913914315159324727256884556094051561747415044876021473901851643933542023994558888157274374815546390612541707861908395893359289001775766123478183848534552552187856534427341521704408589904154257927947145031607659/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^18 + 373051805116014004666768306018837314230787955904547562831915528816317508491029921716644709586149362475350393126134079438798961098466370190313548263263105043838051768590856140950056725671931331025277578369897390985989043312347046545318685224883335757013118490045367346759968300568001987842677024926781651248821641313540300566212211700398945772559766201000889103172316822826437469122832342659685829662771408703304363/5693064696455838866648381529979962939414861516674505736306751652316985528649585736849887190077685834166946608372980457650753018734073333065738594218884331706609240731383235035699257108957314128785577311059167776448561412208903026616432975707601193400149811539460285667685962683705713440802391646876573494411116283393672667855347497243873913216580903377967261064062189424134936358591460943810303993917628840960*y^17 + 141444877353274106552481812275896469447194170672163607579884481896124657670731945638712611569718791638420202734103928362238069790740151856306048374529160269337011595416154245513888086296497544895950295965903817596747976076468097056006496001326157023948264509685512801478288546732834604431215640875087811011877969191441239035616590036282977598965746056660186127037099971350077244669735441491136567472677620696640467/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^16 - 175696095148101888893154588476717064975611025179509622203391753020289447151381661554995326116841577662539633757851874366242337611662484943786187699147938627019996433413568944416475829735727768358035918058024665810940784207460757041088021713747900378384767779690330623325640259352393468139287211947411149680384766097022143257063818672214732567499097264197450719786316780003668610119844664254085790741179787128093361/2846532348227919433324190764989981469707430758337252868153375826158492764324792868424943595038842917083473304186490228825376509367036666532869297109442165853304620365691617517849628554478657064392788655529583888224280706104451513308216487853800596700074905769730142833842981341852856720401195823438286747205558141696836333927673748621936956608290451688983630532031094712067468179295730471905151996958814420480*y^15 - 42228470080360646843244347428655752326405096210821808352753095701665507387394901956554824751678879492309051982430951000578999844191150159920079999867115126814669011550620179870336474002339358478380500921653661515027147020692831354444816884084608828456652704511479852744694711641398603217375164894888567417582906449074500123891202341718133517065837962019732457029270728596592723023972307083845214136939673328935509/8539597044683758299972572294969944409122292275011758604460127478475478292974378605274830785116528751250419912559470686476129528101109999598607891328326497559913861097074852553548885663435971193178365966588751664672842118313354539924649463561401790100224717309190428501528944025558570161203587470314860241616674425090509001783021245865810869824871355066950891596093284136202404537887191415715455990876443261440*y^14 + 7313686514704661939619658471635605029214793938573631220593666200832308623999955870971924952633610047327142776035905306261067551459261981389452607984838295297927922849090428294879794435189531821418424049772318750048346318538330984816705562390109605355915308386065328274909342182695012300375142045405923198109972558668771639823297160507863062338238763208892100484199209709324832699758168882673587367924239191628679/3415838817873503319989028917987977763648916910004703441784050991390191317189751442109932314046611500500167965023788274590451811240443999839443156531330599023965544438829941021419554265374388477271346386635500665869136847325341815969859785424560716040089886923676171400611577610223428064481434988125944096646669770036203600713208498346324347929948542026780356638437313654480961815154876566286182396350577304576*y^13 + 2985146754211629525975917778764677228511444560936235841335995461912859648027555227191931587208660118385450334306799953483059741266811898507690268632458939810017841202300422552574706848646940429185775197257379287004387345486484975103443465045288062506015755954129045481937664404286078207460078137105654731700091852992952522997763352610583543373756709143880989826810219069606456881530195267951356433543709801902597/59302757254748321527587307603957947285571474132026101419861996378301932590099851425519658229975894105905693837218546433862010611813263886101443689780045121943846257618575364955200594884972022174849763656866331004672514710509406527254510163620845764584893870202711309038395444621934515008358246321630973900115794618684090290159869762957019929339384410187158969417314473168072253735327718164690666603308633760*y^12 - 45750707145191088558094832562436255920252657332262542196001519960622998866983185349884592917508246477162931993468911908381927762778186828576009160017577050557720961875515702501065863426339642999166660020783089047538809463089125704175370256424703940667193487337034130765573665493192882589428506518901868182482184703992881544263378129808879280265854139248417560917796144741135694437608014265964338669715012809349573/2134899261170939574993143073742486102280573068752939651115031869618869573243594651318707696279132187812604978139867671619032382025277499899651972832081624389978465274268713138387221415858992798294591491647187916168210529578338634981162365890350447525056179327297607125382236006389642540300896867578715060404168606272627250445755311466452717456217838766737722899023321034050601134471797853928863997719110815360*y^11 - 7835839589020933982680736175937413161853282651018802375558501699834433093731959382453306380319745912147802603450600085885999408904710978786257892237906114538189566055882944625472942661808874485313696906256301523985443099303974876321911265785533140454697341636851755970860200073198485153311566557988306638906991770611755205777141021727271940623596196665288480724999317552874372099116413920291031761811092338469577/1707919408936751659994514458993988881824458455002351720892025495695095658594875721054966157023305750250083982511894137295225905620221999919721578265665299511982772219414970510709777132687194238635673193317750332934568423662670907984929892712280358020044943461838085700305788805111714032240717494062972048323334885018101800356604249173162173964974271013390178319218656827240480907577438283143091198175288652288*y^10 - 20984214455461266689636822464197201923162326529077868439359623289290127152944333814906362875355141951831444632149501192384855243577472630695446050650736589096473984502680317650830172252705067074601091092836433220958954503195064766532737237901089269467712984465109260441531258753286621854054754636452482892546933998831201848667842080890522528551930359819602788445094905345750553104234763124543223937601376172982273/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^9 + 5743929067894838071337409892663420293979206480100968690964776829134668683108378949678658419747229961277324816121095675599657075092431156564265501943292284712503659435670162336223839657817897178177401822540609104669786232569559131566150856341534238865557221572622872852642477597710912540825349582064764317241354358257555258171344817539635874378930905512315762919595100975628645581115554008931279021009431586345981/17079194089367516599945144589939888818244584550023517208920254956950956585948757210549661570233057502500839825118941372952259056202219999197215782656652995119827722194149705107097771326871942386356731933177503329345684236626709079849298927122803580200449434618380857003057888051117140322407174940629720483233348850181018003566042491731621739649742710133901783192186568272404809075774382831430911981752886522880*y^8 + 638933387600502289946130329730116459051089284853951157968713935383653422800935876998806967844316417577054258802913100516237327724961976729909938427084247121143470535958946877008084856438463466536285957951318903989677587324274851814124307199703120090822321244998719548113277045705137986320618429369077597281350770379563994842010836870565726611242394190626972192818517622948907324240180151849313214346166071678771/379537646430389257776558768665330862627657434444967049087116776821132368576639049123325812671845722277796440558198697176716867915604888871049239614592288780440616048758882335713283807263820941919038487403944518429904094147260201774428865047173412893343320769297352377845730845580380896053492776458438232960741085559578177857023166482924927547772060225197817404270812628275662423906097396254020266261175256064*y^7 - 1174863656240170875311692180431536623941057741586811361511949881274840579667606215012544684468901932543437069127786455303463625918474865764156844354259658875534717502396659114486390659599373960140079282041438250629984732951733932066816425596772377608072340755845506822752430836480165635761547536376198066312228304945628622219124922373627736117267063407257638779262924403730702292297139771703263286700117640021411/2846532348227919433324190764989981469707430758337252868153375826158492764324792868424943595038842917083473304186490228825376509367036666532869297109442165853304620365691617517849628554478657064392788655529583888224280706104451513308216487853800596700074905769730142833842981341852856720401195823438286747205558141696836333927673748621936956608290451688983630532031094712067468179295730471905151996958814420480*y^6 - 10380304424785044925104318803575746000877831005660265436591798432086520782409329731078304220750338719221351383574456141642238387350893544522730285883198898306418241799862684118412675259838750702248703021866258311678228024542696048898080954098180682107581603573126893174307155424144856000244458146193092452751153520399462831900356195316910502837033091266631864175640438528172398850624346934080350889162429446113/94884411607597314444139692166332715656914358611241762271779194205283092144159762280831453167961430569449110139549674294179216978901222217762309903648072195110154012189720583928320951815955235479759621850986129607476023536815050443607216261793353223335830192324338094461432711395095224013373194114609558240185271389894544464255791620731231886943015056299454351067703157068915605976524349063505066565293814016*y^5 + 373320112665758669865950494625128341560776153273255275720413437740901258666018036346025603828101166189531517550133905831125996275203315427551869282759294762963993499213145739974580621959287754822163853029034826439482479216267915862260222290048187205516621999639165380189159226631765275781677362109735610883217635126408895014134140633150111219252181638728402525512631506257380566910162191623265236957353454314663/8539597044683758299972572294969944409122292275011758604460127478475478292974378605274830785116528751250419912559470686476129528101109999598607891328326497559913861097074852553548885663435971193178365966588751664672842118313354539924649463561401790100224717309190428501528944025558570161203587470314860241616674425090509001783021245865810869824871355066950891596093284136202404537887191415715455990876443261440*y^4 - 12194758260469169025030736915626844388052735335846327987069886793319207393615946879314066238809967134741725077452071212536894152864114396400719664466986454407569136378618583878615734868905922427874404366847816120484182193199075727367907943488951233242535050611973765750904404899964321682102375992746290111095711720032589910685354478664302501814912063315547742981936316055121772712535479914319924694420951835629/1897688232151946288882793843326654313138287172224835245435583884105661842883195245616629063359228611388982202790993485883584339578024444355246198072961443902203080243794411678566419036319104709595192437019722592149520470736301008872144325235867064466716603846486761889228654227901904480267463882292191164803705427797890889285115832414624637738860301125989087021354063141378312119530486981270101331305876280320*y^3 - 11970351742954190775891257342836074403915852064359698177429321591185345192413389912821260954081304504199958861828818461457693338418310281318868845935016111814877198684420869462259325537983055839520519192874710476212260903973886285896715424124666235400224088992359940495431750974728369347097698498554764286181807599626052446981941525015605971145339994666615427510776933775296324487174037344588903529084105775231/8539597044683758299972572294969944409122292275011758604460127478475478292974378605274830785116528751250419912559470686476129528101109999598607891328326497559913861097074852553548885663435971193178365966588751664672842118313354539924649463561401790100224717309190428501528944025558570161203587470314860241616674425090509001783021245865810869824871355066950891596093284136202404537887191415715455990876443261440*y^2 + 1150343548292628565926528546762766045421893101907523811626167235539060397025991487530170845759944427909678324330227861690382481514328164466752772007603282634778435668937675829956137129020066046146451167975965034837668465609251115702448763409528832754535774420535129321247698865435341711686858500793068985928156822782858168067589349583630742850254307830098806910838149772327207963182538936464962329284417454789/2134899261170939574993143073742486102280573068752939651115031869618869573243594651318707696279132187812604978139867671619032382025277499899651972832081624389978465274268713138387221415858992798294591491647187916168210529578338634981162365890350447525056179327297607125382236006389642540300896867578715060404168606272627250445755311466452717456217838766737722899023321034050601134471797853928863997719110815360*y + 106305080807568651129605124828907156555097925940788034356992300801969223404099497386901644060670061603968516714047293498654934801363020862791329455985786948594361322891922442148117376921457278877908166831848221680020124982618468841231915846400645945292234833161163912290090771182725445134381553306610896626771323114250880907995801019465113030541625029115636090040347625199589056763665041068809113527894880729/1897688232151946288882793843326654313138287172224835245435583884105661842883195245616629063359228611388982202790993485883584339578024444355246198072961443902203080243794411678566419036319104709595192437019722592149520470736301008872144325235867064466716603846486761889228654227901904480267463882292191164803705427797890889285115832414624637738860301125989087021354063141378312119530486981270101331305876280320