# Manifold: Census Knot K8_50 # Number of Tetrahedra: 8 # Number Field x^33 - 28*x^32 + 271*x^31 - 474*x^30 - 7909*x^29 + 704*x^28 + 55243*x^27 + 176263*x^26 + 263378*x^25 + 932035*x^24 - 3521395*x^23 - 3388051*x^22 + 1916359*x^21 - 3868305*x^20 + 20861863*x^19 + 22969331*x^18 - 27036164*x^17 - 28451700*x^16 - 17246330*x^15 + 8574833*x^14 + 40295932*x^13 + 9724847*x^12 - 16562400*x^11 - 7863067*x^10 - 653446*x^9 + 2047022*x^8 + 1708020*x^7 - 236267*x^6 - 376851*x^5 + 13275*x^4 + 33009*x^3 + 992*x^2 - 526*x + 2 # Approximate Field Generator -0.107945554345984 + 0.572290311214760*I # Shape Parameters 69282181591555627351222026947022054103255252598995776237662794890420146577587134864056821754059625907773125572157942484765778536209198437389040901187/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^32 - 85546084461431327183427868094803485774947448613217987813172298241482853587987964430612002773970121224957956781860995333312568932702295643468862435193/217462455203856144991038585713236831883913364443105752352857764624100437012660307879671064500479646455742239096509624633830073402297979357731741377231*y^31 + 2794482875138666392848724474309945208191066974391175791623133564468634801486320355403325982047428958604289455181105000565112648507261275660009907669219/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^30 - 40661876801468320601495498325705433340840927946364412925447644755207056127971480444518697118761738156313859904016684528540173157020164337331258474454214/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^29 - 75939327633302177026750010973426404479767246997036797962818111465142845248215003191008650997749077321935984004900788085812433589186000841568101362696321/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^28 + 260486110878420449734010094975035016937019803361504386293258249038778972155151986545710496898069879430536258431451066502933214653507834252157416029762750/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^27 + 3720670728635160493930639715616574138501352582587556572272831178982603164152101108251193330426878513285148957771338085567424265435206993152065455448684186/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^26 + 10735175499221207577983427142963228079227485575115399463170203234551391053015960661289722737208526527848721851645538769482359218223065239058708967391069192/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^25 + 13981662728982913192611223719500553181340296842300685701986606883220460826141964708795659889189378956981204568683186707803972465318280611091434632692279221/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^24 + 59008533983147553704241317152583196941078872563927941968368924285732385214951861392836422841337906755869527649430620424013020632047321314477552297474451822/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^23 - 267592186976292505220337992699261671419203512139338564637378260475746903506960829694234776006946362713148556664774120771344246244925843934643289644647653039/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^22 - 127762808444571561022801761354524657185626013401690602854272814340552952751326912824951424716304366638308441737005719580660128818246709981349990938228009405/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^21 + 181304860967428677068941537874541126997663203639280200255034796166713433258426771815011206049988112036623477541936387811233829378063043869357350990202894412/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^20 - 337741365890465243119554172141886758085881075299809854350165665514394358168732972863618605812533783668966277561064931476350825873530107631982726655914675972/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^19 + 226163055422739401741670408658711707056697304653798904836283664446812740011320640496834085482908231945864954730935364623389575568833035028492966212891427829/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^18 + 19510507038319873949467845201803682423786219929541478841918076673940462430990785671623638294170813687152461364391121834742696961987586944155062828473632710/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^17 - 2240382653894475234204090091729905580926325945656463255156898113696560009845684320225176182794067924736642150285140824373925348655672960213312403837946073434/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^16 - 22283332517091986069270156646866338945401480613851381206083884163014551431696030279093499281321348059363701115627592124994992241546213206341984041049912503/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^15 - 786265334043896518160760929648908415878337784356121825270062750825214358959393814260983661239505539455776301595332257060116289188461009200782736733020154364/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^14 + 924049588922119003921592509331024655113271424727736060984597823819162500096009276341229730702632190030709753782721408241354927397481008358138804176586725132/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^13 + 2431759638112959193072818073039659808954901283591687645524434277770812591310785573952703185502838753232394526723029031290736938201302449160713148902108370338/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^12 - 273641722663388506454804926515791536329159806134631955306164189553359424893122555600050620070410693336023549246064522197646855186415513657054325113495013169/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^11 - 6400889977108051176483543810100913979593135253538340508051521203828947340640026998934603690335593562530913174586515724533775946365652693496752400745840931/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^10 - 163209776331857781240650417898516006306609556331491381464417038905952600730457722232951967035758903127550170809705911570573064045252102421808410446693597919/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^9 + 12269041642433475161029262861056553102876956770548943899488525261201757110431866408448076489545642678603405325966867861590753703574795080621213793136913404/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^8 + 142375606420841365221179304661492690702771417560142217258901805073744084110713905412209999784508598726325823252997320159889576856314483350736661677840859189/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^7 + 64210270839458235591286892893069534046877102960054789082481512609613868905629944461078420234134134954217664575874707019839575643400586185857612106143787716/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^6 - 39619622683447801573105223173737344434285794049315664812108308938264289020012116685912902246956106844496960506874234803676173094680665268161306759558633929/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^5 - 10923092591463526570221376871253156449995299186121263988829235135053189962374922263240740063988345957996195821535170133403461009432293601525052363237589161/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^4 + 4477694821853977863483344225035064582541601150396857182734258633272063154913872570448714478492632945110943426730800929453049174702710803702075949556875256/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^3 + 27576426169470844635608738297223018627251875049917578242352819244666820141457918139052116546572228354941223651503307820009737644801868075276209596622639/217462455203856144991038585713236831883913364443105752352857764624100437012660307879671064500479646455742239096509624633830073402297979357731741377231*y^2 - 112099020920179316900220462922653017520815846492371974700791415823458517442737613930417451501549667307145759390643900859805164357718082575917135043959088/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y - 1422109989626366353381972473048428272007964523687185419171599360319838335094981509412465833195163177652744938088296797877897978258743638744833367041676/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313 -65579773442036234144419777504121782777713745490091803966746173425335377715884286923249369181651538877781241161814680469935963015641716971705931944067/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^32 + 81110654158882297219316389008586853941715683251834474388076119593526095639714115264352903871363926872360973602662086718124092803913862886656017721424/217462455203856144991038585713236831883913364443105752352857764624100437012660307879671064500479646455742239096509624633830073402297979357731741377231*y^31 - 2658132413850499865204605916091747633364015764630257600434887650169951252438399746324460984777185707312836157449371042284060017907304102607338799253241/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^30 + 39430191218997250219523268444924460577763917208645976639823161950337333177552858882295028973331481705842022230868335381193333436712432065893416052789049/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^29 + 71534996654957879346046469592772954101394861760741085393940870082110742090551529464614407386152648578139314372603492265692827755905585766493584552117600/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^28 - 269171464617661074209222930642882356468944574979587219530405519025775839105430583825354272635408268383092808695927488606555829163614708509638210992170336/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^27 - 3495440280679534033206973598469539240991883373704797328207290618203388091745179275266007086634893803832130082739041430998151772421871920216572734144747835/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^26 - 10006628794163894900891920245284247070167997117422557787567749907474516014070527365137587349450376782340373462061032538318691129155999179810757860344911201/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^25 - 12849236507483456900728400997539583946976193991266585192029518960416208302891699949503865532836892972733895100172704665718597473179472499568691188224387670/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^24 - 55493536870457728817904786531035628998026819652150112153094686223226534328740286231962545249819293123667377682836832760427026199893583788021758718904526224/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^23 + 255654506807537406380924122910105526151966713064069622400254238174987680658779260453280931451808818797935835051931029077500211979276769467527539539247111137/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^22 + 107244291506418599555706977790217793732041362336148316473237835581440342210814356424148192024751540456779881421414291161755836548984892248493087676368139097/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^21 - 169061249007802066114044508861377359579311150211845091536408651824058249556459639418581040879711365000083455835165249251153881845995430008186261114184113721/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^20 + 328020339885648898017189575151066175589380956659022826514021023623083252194850925285101988752653335344407072407989866883739825845058575493696504567072981587/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^19 - 30978365393404755011140081576601415188546697133618420744724582243486269945009404456681119376300934215380989846533584057555599007571427515562811010366082408/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^18 - 117454791163200713802129133082032025783327289216520542896733685472140623402639116721665511162756079832479272121920613894716933076415550415231685881336331847/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^17 + 2112882352661943537998033399870354010463106598276610169036643688885511739397477230427026429202200820318922059147739754670003060172045142889883631813199686588/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^16 + 132359893482736710998265052186693687488709277191698867512192855139419070767921551256423013757661009570042697127238714321983010356812781951535260410649300274/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^15 + 754723322364372055982658136238474958462937236715380572551108069073660938022186177519931225836235275116770109380275786492017986796702503766968775058150687776/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^14 - 902615974987019160608997515244666794789838847985125068025510935102113201563224754058300406495970482731050024361580892507046769276723615315738676531717609942/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^13 - 2230687342196210692962496062474401438309608650862906659131753062912930708455107624739183153131752885751543594911522397386174676726147880806219965147669868833/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^12 + 332459997867437539099605538512527247681312873866105827360917858285101452999860705820608030379183170683463483205365102736508231527173295225739680330429958594/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^11 + 808494549834187391262258159941877579133856971580859450818797110030607773831940230946179883397059604067833881242170865707389431624110047540082280646615917/4438009289874615203898746647208914936406395192716443925568525808655110959442047099585123765315911152158004879520604584363879049026489374647586558719*y^10 + 129663657716321651983427263393810745660837507991638888062712906756627206512700488951394005947622219823762837169110492249166175880824233866199240051178977161/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^9 - 6885378533971704819386067380360263695822133351290670331310419176129274519801034944894055833638080961036569287698515403175685244517826603870222908247020632/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^8 - 131834095371201041251069977813185903578428912151383000075003884645767300099045854597134164798429430501669448715657354906363207994528126334410346584262573729/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^7 - 53396063589348069624009483936043486790265261613694743926072810376925155624176723901666757363800569002882927927013051898664907777960193718265313644395344590/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^6 + 36905054343435711650547121429513841785723535907048348508823736243301686102586710050099934283726250195899508606176321419791602752979569156675865480975746363/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^5 + 8378433899002061661042112232976027647861653973119545348080509659291831844516959866742283591450126606224721327989691917958018373883825681723103361704202501/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^4 - 4062524553758532231568425543627974864491618946532498050068401227876931741113039771191007416136799667422786972076687977698427478527521157240374444162897036/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^3 - 19342155770929870204158752536509065068609418758687570913974740953122717741674207541762262996944450479012046575301869352032251720294628240536567279315017/217462455203856144991038585713236831883913364443105752352857764624100437012660307879671064500479646455742239096509624633830073402297979357731741377231*y^2 + 94714791295182183056523093473755915835815049826289633511339129627548215738964581287940654124120339906025882523341742502541321382130237214209911102333310/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y + 2124460549500067477593922634812752710206563587479379900317851742580837446471150922529117633140732258044587990979456113271822373244094382809743623999801/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313 10625897984239478525162793343597424903576628341174301637828087721095853141905166038967489701227788282392053208488340570135233473589681673232539404595/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^32 - 13169291597167229372968205153450451281118239165306290568974571336335314267489077390281200834186135302055494676800629817578642808488978875450897680284/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^31 + 433278308471130138531606090080359033550469084807098138222419581231832362967717358839809649493035338804318118317820272206087160430582606749329066331121/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^30 - 6577600122669442600618199644104591363856419860919848566069715632347610581414185189635239337811526712222886669372186228636075174179715105849614806522065/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^29 - 11518487594963399268541767393439511772190326829698391385413009045653059666062665530332769521031233017402715035766402347998476938020588654975740232362932/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^28 + 48006521275792285353374354837891645559652259895339360615572179628544068376535241943357042219558492596384963493378614890975817431881277436893151433369067/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^27 + 560553768959027958977904646810496982855076711457548701053431043506535433867530767118317058854306818414382899426850164131947957887745127787570652574395384/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^26 + 1591777816997293409222066844601071297459382251652917242515254423755568611798362024076673817273542056025371494380223879244634240636984349053207705549478410/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^25 + 2009578538217711850679809203287565466881778516269285854599204020204990695442736833371316118863098896465011403162195275940767790196553428742410200550240670/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^24 + 8928084957755126004143635181077172133870636342894662143582742054945150896125321905239140728606293284243607442937482148706349055675920548260458082813390535/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^23 - 41885449832858871066547912566249276844938685566131191629550770620986280491383739164054774226771103401856733936848724581451505895999213945564769117037939651/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^22 - 14603280037898249333568346897021142689931064863939430079058845522195852841305300792609460561350074658118293955266038753655794989147327531356457764948154264/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^21 + 26496774712739804002686311231896545345462247037861648242533484950097599889054785647526070246330269607913985948049666577236753010469396226234515171855623315/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^20 - 54521298176940865189167105022805450328690871443055855885081674722443574065006169039500785242364996470645061659997764035301692799300844655758290263116657445/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^19 + 35721504504691520202062808508713694742356781373190404956198576094083113763960757721176298560651004574084733960941887277289286768377749874395004865186946245/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^18 + 16557785697154731557346041813354364422966826733674609558635491471635922911281469384901635889809610214378575046006629451291830840085766326910329333631110550/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^17 - 338401554013747746713083769499355753881426783290372710859952890900372235470461003717412752266772448101142850235438849005601800891378357524675552059690865744/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^16 - 18619286413033368880929726226188450746113393102485152961760909725793568495862712320518889020222639124013580160022444472768389263110921498098975853101478233/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^15 - 127617564502671074862876827903671945142946432069862750171534057456867618189276858657149369185092995691942010784955836202098731799028872566967685795739028620/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^14 + 155369039194721080813503268529164526293040607014789913135584468145471862376611210530641161028158555024086751005682107047987941665977859239729667763477535874/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^13 + 347248490864189614749595626464114687930542276113272986067787962133312845856773672015054408034119627529192975338970100310167581597195935090265029235405402172/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^12 - 67098690363063913056632820630854866437821392085965846389019626985384141025589643695473191289538928112550900440312963891340186384588147179533879019225171794/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^11 - 834632377237245358664588681722327758303635478338793126672558058787029701732859879378000642635276518896734249961067748917934207224231455570677811309012941/4438009289874615203898746647208914936406395192716443925568525808655110959442047099585123765315911152158004879520604584363879049026489374647586558719*y^10 - 20854782383064858571176288579911802561320813496619479605746481339088399038194350135427791977333129511158335558160290373049465827050072885904935101081458263/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^9 + 786676803726189410115702016447010084987225962212602923658686907612985025607846962460001985016481273138782768723375734252634677711299893635611282133500591/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^8 + 22438205414308843823533840968850880611998401191075679560313968288869091113643428046949704361804736138348809369227785027504738723765469054097151426688898477/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^7 + 7192919940119229354103244532951198491567951946204462044787075481395157954755598906588382185456610008565280728263348432244138248703850804370946546930732935/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^6 - 5595310835985535932383128387046131702758102009762968392836319555013002275522640215917104094042632838260512072476732534750233979650159037470125752864118069/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^5 - 1272375321676151228950668121068191408157878215874739662546816271423781435202335475704392934406900102875683386471719955074177461218809218174284214500047528/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^4 + 516467254599441518301497979949897146655373893661018187850322943298239157850572788801124922122059550158708469825166184727176311096334146629415279377859463/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^3 + 4393400689102258767623351468364454273521405154965562682089173732441645159484086000756251782110669194699968725197661955140785641921281436455358269395103/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^2 - 4851923871662017413910972862618533025650266413973991508026378068349927480915217460102948057155976634985204283368980824507634213142881615153235391053060/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y - 2009198005861967617596268969187733293810286230421494129453051991003450432804012253903851875676996685323129374694692949517620355828513404927532664206787/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759 -15618108627910008519922647901517297518949124229958877131868343512595260587763274260604782569107144885110744580323847902871764747550632121247702491781533/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^32 + 9504664064568872031148283121751806462969546950520964591700835796249816961415449899743392440409799091634238171482376376994811558801604285199995962391613/10003272939377382669587774942808894266660014764382864608231457172708620102582374162464868967022063736964142998439442733156183376505707050455660103352626*y^31 - 604291573539167075980778164099293303129470852689360795917420503162633372754663919725770120439441266849973924587923129713038001901974672459798184492880645/65735793601622800400148235338458448038051525594515967425521004277799503531255601639054853211859275985764368275459195103597776474180360617280052107745828*y^30 + 3690730162897020718241852337015972973029687636410700075712005922619419408074315144829692809781815677789040897566235447460412851849060504783777161305807341/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^29 + 17647361406146711039270405144541922918947630869187402104409202977049124936956923068177712129197209893550366946177261680847130562784523680677045236354741131/65735793601622800400148235338458448038051525594515967425521004277799503531255601639054853211859275985764368275459195103597776474180360617280052107745828*y^28 - 2545023366261976705765068086788146034485474399102159412374858304976510672540803939919745865217496797190933925155193095038657219310609474365263627700663624/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^27 - 861935883404882590006276190759597055201680150219350725847170334480502294774312135774630136819781576920526456193354815872301638402003053735657799364600563283/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^26 - 2758746629737283780924752061747039743487950163593707448012416105791661519154105938160325755497564759333267285908146771992216228300828799271586859488387985775/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^25 - 1034036225299539594310267957249522276472061720791211085852652033856450765761551985696939648550002352613303322540368041601776171144044074093732139117105037101/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^24 - 14598192655208160174361049526665708471095706184136681426980963680087204329315950474446742170913834447550949815049545154968636684158224313848160893860056692065/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^23 + 54891486467116160868142142703494939238388475223241242663159405447582854761388127803800718477772379363724320638193566609244100238573199368873902476615158490051/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^22 + 53141132126162211684409829317391030735507865708283356426724997835807582861087240470068201687883740937408347988054574995046236209100922864188164492254493047881/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^21 - 29109885456026398519236316094043558044075928845911556680440946802491240397239077072285712724604949526403850637574712718920782900050906049600667409558984850795/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^20 + 60308476781826236252480477519320624876759942682986351229889325812478891161391466174491139640124193062183822907515587264163805144504202415225380627493389291357/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^19 - 46541947637658963137707756906321567166242961321195457650340873886225887362300138775067663336336082970303875048054037976631821229559920287923314972312771506997/65735793601622800400148235338458448038051525594515967425521004277799503531255601639054853211859275985764368275459195103597776474180360617280052107745828*y^18 - 7346275038184720133019212103701388684013611841094246093094856583294714501032301327823781861780562080648251273726450120375782779378337365100384415539330169195/9390827657374685771449747905494064005435932227787995346503000611114214790179371662722121887408467997966338325065599300513968067740051516754293158249404*y^17 + 104271625029434801681384909057136420280210080296121374164670904554952668030126119839290468680631475518200971628374933150712495312263815039803780391143842593052/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^16 + 4552156835750614756421429069487153111784015380802831334487724670379137059909964726996132015542903768630428944841730132354549012945917497977743111485846213047/4695413828687342885724873952747032002717966113893997673251500305557107395089685831361060943704233998983169162532799650256984033870025758377146579124702*y^15 + 69027598886333114090447618005264928624422472195414110833669445579339594282546598229333618840826062413083969809406229085148660363874091033376693350544693549556/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^14 - 131636488126598543832930793181048244225405489242359634438143209830686408885981351779402896615636102551391008037270435248979266915151664526104403909537034082261/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^13 - 314415767294694042861767114832784934675293598422663228561527495215531328238127774601373500970017855949032632456966712878272944402757991115839556423176680185997/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^12 - 157669833961463800658881035704071443262848790555954703721429900781108746048982855193708243489733764242703257850270345043787809533573138115956312863887564151439/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^11 + 394587071262767215292695744335806238348901038339625301609568915903169165759096422154192709945852099260898888663429287592049584425288689833973232024313066245/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^10 + 125871519849834801600460583573940469048248690801628134632629095541038540286218700241609320538256466989108711769613515589296833978168515445225441135406444167067/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^9 + 6109419405440429851419302858124014519250099357221719410151608347196187706246968104954915084528649422453598238475439174907773435432123328228123837460936447915/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^8 - 15970498382088636033851101845111935036235770198572071076493245023362967669860364077272580987180543162894598819344527217747347885317101176367631147308212044591/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^7 - 13430434689838659215759803591309942286124737432628220517790370736717645708926496699648242313030952400788771823691752499743817391157987691233943109064744179089/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^6 + 3268485138414229432855979465862634785716545436503877705670604472051673631928392592809077794895453532388310444885484576766193845414856947166803633697740354515/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^5 + 5870431580904859626646269992587493989702734472865681739118218552193456543086430939904122900665271870660642488061814220914282660597337388847517313198904641261/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^4 - 99679183104750625125255315403314403321177743913753547033453388124484339672983578268875051500185060437523884319671028514523715286005155536832602565157936885/460150555211359602801037647369209136266360679161611771978647029944596524718789211473383972483014931900350577928214365725184435319262524320960364754220796*y^3 - 22523953899417867617675479287922868963372464128079899991374964400159456401936310857167235990940564889191931671175461393957902267662798734238380408742953755/20006545878754765339175549885617788533320029528765729216462914345417240205164748324929737934044127473928285996878885466312366753011414100911320206705252*y^2 - 5996397763568152215767916736307286649768697984432613176153665863073612448362568461283987143886287892716521836885811240602408018848790900027256594810524866/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y + 2169548174386634047829041046604635571108819825014968031571614013649120555824285908010847519257338655947378807643188654397358871138681327697115780347965742/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199 15229615477570815515157621972284669806178357921756458323916826058399296247837026345870763841152540679545474225621648795701495436582724831981451089271865/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^32 - 9268198803973424472665497805814458792898364161971062862206212711093530479042694538373664524119851630680121259794799653968926606413188478711001412540095/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^31 + 294622366640596951514961499526564757989433900166266249051771004063498768845947549115646192932990964098481182158937479547617633385376907978452817374492361/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^30 - 3597888361831440402115530915160171551148313536212018134888553428110809002949298395370836697784914609641480514171819488921950073882937840655527208428895814/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^29 - 8605382364454847826928463863751925639089099162866219512307660184719742854452091100292415634509061952541353070295561010496193780950502135933493346149449072/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^28 + 4973572629240055316573882167511213261637340497204909418429922560130766324281330445921314990589089519556195328295608556244452069106849095734235175746460517/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^27 + 420453592725165054048674287582623352259221829683879331944695922975461193346050241088544283148050913181554175724048538764803974221413465447697579173400525274/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^26 + 2689944938151435744890977808752840047157195017768930795953929734181451842047938004968500038468118684230298671347430084074842035919948717503658585491864806787/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^25 + 4030753364568508628788336720217559853516841057052169044979985066738375164758850314065863417140790611696375178440068868026904202143424478215807203840437207335/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^24 + 7113829015929975514856454905448141603581537681716243833799800795828565913634704233577734070418770933241350720521428340867104146209106366324933490957910851087/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^23 - 53533970119121053117689921738641632139267581115824149953788085449664109510655967321342412186451583141336721772260262539924181200446692981971521348076577057029/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^22 - 25935540790047319750254724790145390085809994432568510339068582710397361352654558620378107939897266800298526771403501466276071089325621335868789980855761130333/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^21 + 14299138644008267039864086494927675156419306338110006934531765775761117678145323023465598149026928351858964057849086395715253630444033574135047668690317618081/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^20 - 29375629109298896994017896073567943431184062435488601630056516598223900579586969400185154840528033606988147952749802755074147853709450621370889671013944785591/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^19 + 22681878255458267168797220544215228970807082688386792777399959105235689655985982101746255630681648595226732114351962926380915171761414205383189028366764616304/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^18 + 3585185996585766756318043618599699940335346441575177361024464425656022615432232657696044857722541695643819520225152564476451885265444125313708459546595140921/2347706914343671442862436976373516001358983056946998836625750152778553697544842915680530471852116999491584581266399825128492016935012879188573289562351*y^17 - 407981996756044873316881260833223161394470010763042018537718554836660686428770966888525737766717746828255540827443700473259394715794733985796828238284078769777/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^16 - 8888405471206952479490714571691503525346903988217487676743326638134180668908714206957180532851976783432301855093689317844436353054975545919725611632016292117/4695413828687342885724873952747032002717966113893997673251500305557107395089685831361060943704233998983169162532799650256984033870025758377146579124702*y^15 - 133772558672216582866995131117746916988039631923810724951764206702559151620254220090088721600736793954118590508400786637856737642682436263888608066023021490934/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^14 + 128815297735734117488017491104057415911058940216796841740819070872753787839086472993841480565953025782656657024919577930472771947732933628190099307124637005963/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^13 + 306927184784841549858584250589474942135373762023629571620662290195652489228351324950643961099490315213228301637727866582770461914216636867856690169141973678970/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^12 + 76493288315805341420777987934297382561015877659838033046809967716325818009713081865820290202998388061847135880474938477090907100889607246055692458656011184634/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^11 - 774727363010862963851852624040223059251189989892037762734977282115281086111395082981846578838475886055730500172115301459668913230962446877266581942551804057/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^10 - 61141531288214087042038956822477535800576337081067085797367610809182439651725639903222796695989575105144739292155740494178474556150683122711775859903063683099/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^9 - 5663963511846497726884122040165307078058961184837387205689267298701198479198196631178988344239321282464914804367882863902516480939395777447002437707800309589/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^8 + 31201110522635548202440873293451008175872089177681041464726746197516789728980128723718767596512942117476262795507383538029681384229637504648335251107647781861/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^7 + 13102573369519294532777821926408617774583600154020170914722839111789504414910982168312295380095029274444095692885368706483073315574304268488665820706308779708/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^6 - 3299108223170366208798353610026957086363398473798357776578475661756761384685837388166444437302275594528860119836736301925326956182850900967529495067386617375/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^5 - 5752971041359448181580210311604891890011376587907049623589356190539870827691363250081283796801171597157860813318998500421834689675776798910187274859761119849/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^4 + 62038805256983066834368925842773372269392813558585829426499340346343205775403408827157376289996418851699002409757558203060177491166930381610233499423098273/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^3 + 11033998949210509891540576659160681378818923544257241636975821817863934799267260066760051468758674501101613987135109572318712153445737915585773261613612301/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^2 + 21706605802766280916990623637704868230879881631416210469898519170907447040055688204194600947784816826073169371416885493988676702952336149193456564768449733/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y - 8263047730925884070065086215490044244284615067780239776342895819319941276541550553940938422139036349819728799993177652379084095385229239119550751443541315/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398 15229615477570815515157621972284669806178357921756458323916826058399296247837026345870763841152540679545474225621648795701495436582724831981451089271865/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^32 - 9268198803973424472665497805814458792898364161971062862206212711093530479042694538373664524119851630680121259794799653968926606413188478711001412540095/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^31 + 294622366640596951514961499526564757989433900166266249051771004063498768845947549115646192932990964098481182158937479547617633385376907978452817374492361/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^30 - 3597888361831440402115530915160171551148313536212018134888553428110809002949298395370836697784914609641480514171819488921950073882937840655527208428895814/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^29 - 8605382364454847826928463863751925639089099162866219512307660184719742854452091100292415634509061952541353070295561010496193780950502135933493346149449072/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^28 + 4973572629240055316573882167511213261637340497204909418429922560130766324281330445921314990589089519556195328295608556244452069106849095734235175746460517/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^27 + 420453592725165054048674287582623352259221829683879331944695922975461193346050241088544283148050913181554175724048538764803974221413465447697579173400525274/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^26 + 2689944938151435744890977808752840047157195017768930795953929734181451842047938004968500038468118684230298671347430084074842035919948717503658585491864806787/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^25 + 4030753364568508628788336720217559853516841057052169044979985066738375164758850314065863417140790611696375178440068868026904202143424478215807203840437207335/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^24 + 7113829015929975514856454905448141603581537681716243833799800795828565913634704233577734070418770933241350720521428340867104146209106366324933490957910851087/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^23 - 53533970119121053117689921738641632139267581115824149953788085449664109510655967321342412186451583141336721772260262539924181200446692981971521348076577057029/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^22 - 25935540790047319750254724790145390085809994432568510339068582710397361352654558620378107939897266800298526771403501466276071089325621335868789980855761130333/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^21 + 14299138644008267039864086494927675156419306338110006934531765775761117678145323023465598149026928351858964057849086395715253630444033574135047668690317618081/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^20 - 29375629109298896994017896073567943431184062435488601630056516598223900579586969400185154840528033606988147952749802755074147853709450621370889671013944785591/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^19 + 22681878255458267168797220544215228970807082688386792777399959105235689655985982101746255630681648595226732114351962926380915171761414205383189028366764616304/16433948400405700100037058834614612009512881398628991856380251069449875882813900409763713302964818996441092068864798775899444118545090154320013026936457*y^18 + 3585185996585766756318043618599699940335346441575177361024464425656022615432232657696044857722541695643819520225152564476451885265444125313708459546595140921/2347706914343671442862436976373516001358983056946998836625750152778553697544842915680530471852116999491584581266399825128492016935012879188573289562351*y^17 - 407981996756044873316881260833223161394470010763042018537718554836660686428770966888525737766717746828255540827443700473259394715794733985796828238284078769777/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^16 - 8888405471206952479490714571691503525346903988217487676743326638134180668908714206957180532851976783432301855093689317844436353054975545919725611632016292117/4695413828687342885724873952747032002717966113893997673251500305557107395089685831361060943704233998983169162532799650256984033870025758377146579124702*y^15 - 133772558672216582866995131117746916988039631923810724951764206702559151620254220090088721600736793954118590508400786637856737642682436263888608066023021490934/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^14 + 128815297735734117488017491104057415911058940216796841740819070872753787839086472993841480565953025782656657024919577930472771947732933628190099307124637005963/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^13 + 306927184784841549858584250589474942135373762023629571620662290195652489228351324950643961099490315213228301637727866582770461914216636867856690169141973678970/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^12 + 76493288315805341420777987934297382561015877659838033046809967716325818009713081865820290202998388061847135880474938477090907100889607246055692458656011184634/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^11 - 774727363010862963851852624040223059251189989892037762734977282115281086111395082981846578838475886055730500172115301459668913230962446877266581942551804057/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^10 - 61141531288214087042038956822477535800576337081067085797367610809182439651725639903222796695989575105144739292155740494178474556150683122711775859903063683099/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^9 - 5663963511846497726884122040165307078058961184837387205689267298701198479198196631178988344239321282464914804367882863902516480939395777447002437707800309589/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^8 + 31201110522635548202440873293451008175872089177681041464726746197516789728980128723718767596512942117476262795507383538029681384229637504648335251107647781861/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^7 + 13102573369519294532777821926408617774583600154020170914722839111789504414910982168312295380095029274444095692885368706483073315574304268488665820706308779708/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^6 - 3299108223170366208798353610026957086363398473798357776578475661756761384685837388166444437302275594528860119836736301925326956182850900967529495067386617375/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^5 - 5752971041359448181580210311604891890011376587907049623589356190539870827691363250081283796801171597157860813318998500421834689675776798910187274859761119849/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y^4 + 62038805256983066834368925842773372269392813558585829426499340346343205775403408827157376289996418851699002409757558203060177491166930381610233499423098273/115037638802839900700259411842302284066590169790402942994661757486149131179697302868345993120753732975087644482053591431296108829815631080240091188555199*y^3 + 11033998949210509891540576659160681378818923544257241636975821817863934799267260066760051468758674501101613987135109572318712153445737915585773261613612301/5001636469688691334793887471404447133330007382191432304115728586354310051291187081232434483511031868482071499219721366578091688252853525227830051676313*y^2 + 21706605802766280916990623637704868230879881631416210469898519170907447040055688204194600947784816826073169371416885493988676702952336149193456564768449733/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398*y - 8263047730925884070065086215490044244284615067780239776342895819319941276541550553940938422139036349819728799993177652379084095385229239119550751443541315/230075277605679801400518823684604568133180339580805885989323514972298262359394605736691986241507465950175288964107182862592217659631262160480182377110398 18668062950030688657608926464301136921667282656055106993579094989201651321444064289408220767682248158100445227356698574374970020114684558735454876145/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^32 - 23025552940900472459683701485488167917106763112102694826471858454639661387254712832572939456331180300431272801623450983802984938278436527892605115675/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^31 + 750629126662797101965608673939750481617306830237615524046708429071682646632418618884840127516868746670709165739715327260801385780721792581275172552544/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^30 - 10789260187828425578728940432959636680578255983092207755677591956531367892658143889411127484551467084763193229517198200241441661564099444922271992875450/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^29 - 20519072109771598628551921483854324080916135685665080711432599926420855138996212549674904217292443682987366206970751175071343508725883360203846769430999/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^28 + 66029435470598424591527027219485368632744252059933380346037155711011449856011733093852931325252025418403178868967974230287802242441498956777449802659631/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^27 + 1005935667939875716735698174465211932243884298405469032155537076050744313061356796881282869460995961570288008302421053267621569596617159894536326657702414/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^26 + 2919844652372631879860355321277209336323096276016210978389255280741646097283602077454479911244811882177443681497161495090962392363452433994082767275101669/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^25 + 3847448516403212843894781230559206258550097815592599967306561817514726762653082647499301434410876899156301019580819456442827057801048676877112929129643955/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^24 + 16002589399023686421905302825277734510936759388276873079646257225639734523537708183610923858219135642523586163074231496145679056280078279633767275552866017/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^23 - 71606087703586846623743692066656590536220349644848332101810304604094253132981292367139390576725095319770787770014252177903744333336382075206417087854906059/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^22 - 36737032513061452740041252134113921956375944822070273839233728097874505786817284069810849756033608874887491382689148117610915625643705209211033080009489860/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^21 + 48857213712333438351781553101667921559062505936942320934001454107739529932667482016308416775687994322735442744003683507297784332553616647358635021390988155/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^20 - 90623029766702065069960613791209388126067353676927569879737672766173342687762736030230719665887189953046796927441571519126525392806557717389903291346318461/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^19 + 60455232858403956316079347651925008266867649973580880713757404108525914488330959684067926807142209735601519276859173276777918012052935151437163565023972720/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^18 + 38894325501997227218351611612529480328468762269475641896805988535026420449977460568786553193525052072860586697781367212856669599113506215034500659415449703/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^17 - 602382383910104098239272697969618659741656276896304655790262828390531966943020751817780321811758362432922443207943306617059501555056993441890687015321109767/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^16 - 43759791798740180620926132157609219336304274062399175185820096710356020506363972123700421840688603195065252644029232094385212137589635239780001161300071602/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^15 - 213024232084746771336763253784226754118465054151670108173065426727060802088743318188226778480722894192871974153359700088226352783280975630569858881746511309/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^14 + 235352671707716850557629388073994703749215460344167168725951334145638057316962492672444025281761170561611030764766316232519762938580121038613925484193393405/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^13 + 663813519590270273109345394072597244784614056846560036305353683277915089140934602582702160850665436938072184991711627327704172271214024290366878962283530932/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^12 - 62008998378749031928634601876568044607158867720738325465956497217728718787635305769756987000198822222081449043386512127923176328187382863376511333703384902/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^11 - 1745661176008670994924011355813051749397289464026702239081731508789399422668263629859257966125171612164374003473695470465346082888074940872934509424786231/4438009289874615203898746647208914936406395192716443925568525808655110959442047099585123765315911152158004879520604584363879049026489374647586558719*y^10 - 42533667141043327993375108628670727247759220171939085946953186940461383417941305194749197840013586278067435595660542224711215986200436384230482604518825453/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^9 + 1180742827620736262634233472373084948651736256295080241958672477863046114966212996687240111907007754689111499802007539906785685924792189109596650839709285/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^8 + 37149032407596637743753201665702573047541148687801696333246475390586020571989828480055407154773951788805511204452591451798573828974266227577180108724940124/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^7 + 18086767165176731938419240602815545317717270954166509271959751562842356124160101822750300996616529288778182387508607487675967747036401800693574917690599653/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^6 - 10855571587725977376728987073694517438271677627915138429532025309132860486413319645808052519040505911580397821035747297291193533699951407437774008870242147/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^5 - 2833332443287051452356632979531739813764374563883473538200763808120281267066166712707952897640878602114710436853077328355135659610697889519289904801401924/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^4 + 1227949709039693174871975464240287853394640738735813932188069393054790702568560569457065807830500727599614299206658709467088876955280621110968287422042865/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^3 + 5670413536305579823878403001852872282535548619987719051734174773939209394531305833952263902565780603055938123984330901423066955105460102614562402921310/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^2 - 21025569802077776041258181412061923379407325510302334489950730148478666908507677400974872694535505473289444083725284118578753254247731565159099288632154/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y + 78333916370530715940657913424854449891718509385711733131672293211292704025094940228246253562098856684305099963291641588182881345183075602947663987722/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759 7040527306862902622562946672107242176897336496854451060234920615353661798547225921093791664176125657881296068221963217867612419357489537137997726922/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^32 - 8625476322828543661577751265074736717315822384053132166216509464932132098376489825786136898301499289231645020643178146115494578029595673037606882363/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^31 + 277672737895591642308157460439832194898847917486817042535770706177951899137637270971948367292743419417439770398964809435512880369379098159682852935303/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^30 - 3695878405890056979746717495001843507570210501137550925643238942641228585713603542753874207013899103103197119863545911850701894231119308093501431594762/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^29 - 7842454727363590703710172114783768604090693734459048540897908924994086064906270866347202424856042189908584052196356984788169472912216178986341416441609/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^28 + 14469214625766297903452510694193890517572120156614016611524997846320786224182289627091028395121300723429438057860907088051849527177888428250023544622341/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^27 + 382689768189954045235320942484136364154678653951935133901995164646813092784323682500782620860566707996884590581477746550602473044055526155245153577167290/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^26 + 1173853810249480399245075204932454019691023911641754296210385884440110424793732976784769288731062733745607066155244587090552514410559426662217537026279000/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^25 + 1671358980822430674642896659586515965654891836477153285946501030817352073718549551943119855591525406763407007286867297501648927584491836012527501847673682/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^24 + 6343949057540093870834924193557269418972632914204017476767615766589333325483537306352344155904447123321900209604852149886141835762473572699166677417871394/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^23 - 25806321585172080041679955542629484395903444538266923416769923519815277514369952214710446044401267600563910124907091021193591229996885216011433531709510431/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^22 - 18840494072493599780971253919763737621996172089593287086138869733870466942910419852106454299052788102199338473801871626094149830825259604847343829272446509/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^21 + 15128964464517820748674053215636836073408120281117276201629415081945557986715347580451884489489789983595269658954719663603480402062992587556109851275203579/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^20 - 31231982404523310035131667821661693459473075465175819617744551581918025892448771403288558169444574354046862064766709515296108533879698331219814617709591166/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^19 + 21922092753640679299726758115853810422606510029533996101816157017977778049232446182219199430489808717131709675729260505272499798536840502911312786443645550/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^18 + 18901041698585396899418245170614916899382591790450619394895249757717731239119630627666720751239614120190282452747806123472587581831994762002532638250014269/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^17 - 203702979374688349193202453847912872084645037661118838460166553775644260062868727614441222781071842610987867224776182085190355622043780245549542618271473547/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^16 - 22130155426091374588435596357409472539071006996472658629066069731932902943440214245473063989018322634167695412148691754960308801937125227850774644876405597/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^15 - 107565458053550174243413985079149457731453228484789369044188239123707749784898766684878245263775113063726789272957884476864963630260982069234241608995771048/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^14 + 69220857021313878370107306260324748522032455548423344513003300257155157428918904237634960790452880511436151037603776080864509506109901815589351480209455141/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^13 + 264363538373330325371172301230432091242084879983237631717124085274828263647702216383862518771618810754135845976504279721763351788516953024099992172414638135/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^12 + 25383012750085275109316898143299447375677024816470744007139833213901388473836291763623976902608248677281202289985264383216946205526164003964755878690736484/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^11 - 642516186927084469971071158281185062871715229236524198300967662486143149546972113703046869489831618823646106952202192606697340077932846267058493221192976/4438009289874615203898746647208914936406395192716443925568525808655110959442047099585123765315911152158004879520604584363879049026489374647586558719*y^10 - 35281041412764254825289545269050409367431233914068672067349857656564178445344053307606296234080602982858028593271117379906289094755795856024692901387185969/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^9 - 5129128704572505488335452771831040985423328340050964513507270881877059452160885173109110046635038342274041675806069926798720782040946099564896207271255284/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^8 + 13477451090355960813878854769898915203985969111349993376369287859304893206536129300820129464182038850417624997670705720718559113338908640573795231609592369/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^7 + 9207023084739329623904503539640027736509766190929339647565623140909023470028444267544256870183132739399495546658166497806251166567082833098901653070601920/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^6 - 2555173387127669099480997913330138527874888058361139906580769454038748700335080585728857067001072236305875701393091326349165936912504154732789555620734779/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^5 - 1621762132005334743737149247587109761777828167240274968434153602163674226496452886376269762651828246693928438997083704089344208276009921248840335655944162/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^4 + 184511542739877712313042261928599861542531889449762695450401099681154157204083232352259043012697212277092642394225605976761874191014847699199026431656850/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^3 + 5133505740242696180690293228943753941098301074264582630567637688280363422012552154975868872673190112010892951046387791520492157299734276762048940088307/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^2 + 9343102522311801494476373255430826893322187648663196146084854055085741464807451366540795026329003620299657432687837182298654777365242441889492909298344/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y - 37420791446027122558334436086438933781520130298209904927664865183021032394882898841370181562977796465315544239217110208171337849833685981515961006904/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759 # A Gluing Matrix {{0,-2,-4,-2,-5,1,-6,3},{-2,-1,-4,-2,-5,1,-6,3},{-2,-2,-5,-2,-7,1,-8,4},{0,0,0,0,-2,0,-2,1},{-2,-2,-6,-4,-7,1,-10,5},{-2,-2,-6,-4,-8,2,-10,5},{0,0,0,0,-1,-1,-1,1},{0,0,0,0,1,1,2,1}} # B Gluing Matrix {{1,0,0,0,0,6,0,0},{0,1,0,0,0,6,0,0},{0,0,1,0,0,8,0,0},{0,0,0,1,0,2,0,0},{0,0,0,0,1,9,0,0},{0,0,0,0,0,10,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {-4, -5, -7, 0, -8, -8, -1, 2} # f Combinatorial flattening {-2, -11, -7, -12, -1, -11, 9, -4} # f' Combinatorial flattening {-6, 0, 0, 20, -10, 0, 0, 0} # 1 Loop Invariant -1051677163194429720285213486270801891647502749843988663820436085980282837119724746753057543586849037105408157042499409547215079857356969508015973286647/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^32 + 1294757595729731090303411594714802138396199436291142013268443539940612591789106229921139855708068931980498006293613099986741497183560015935142418991954/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^31 - 42066561835646988256018249636557071209150492609203959021474296158713506977921993657057133975881683390703892509274154909858784050759701887198456253209672/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^30 + 592927829326068625254778565988612597127166934113294065345664752840848355111530488478003695672200489907873407588543254952127719879794609720152885708580606/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^29 + 1159558887068292983919384798950058424413339789473823509428303166482956336728659238844572956110795463471504056116951263281835319219773070100981361116041409/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^28 - 3278626862956080541702517934454196207064270506654140993603210144554996702742521061341981325818848811025719254590972270217131975111923482432567585193541131/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^27 - 56697681414935326397564465202111419683705165812678004938238593148037445669026405271120806066197711712054225844682750566313437180731061221533506956534840463/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^26 - 167627580667677909010718808918250355757386116533843392343380207012142688952516206144278157320837177018811642673322808066258770486361163348360662460713920637/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^25 - 226555176255075788601682374766855912796587812993779058635075790553419663254706126384200746991083927968364269568515269854604325618129622409741268878560683477/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^24 - 915908597578719361206387113272554921614347108475009199303558990478344038942338352241796274094226859491931937950130778941310535431870575177307505157276859132/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^23 + 3983486546234339746963171124071852388552953302381824153131312429505269850242418837179220709562524562705465183845741219841424099683357173387360454528480699135/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^22 + 2263944859859863293379437704556489870773954319343067350399604717177555728235792424761768127233552061095804288725772255222345656284744452154868371510642833567/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^21 - 2547589146745881745736041011968141934604236263548351735498166692696894773977175275581342534976609330360185990459974182364252759422619504552672862097439917054/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^20 + 4962842143554510788147061733267593055370018849663594372713990057748234674465730996728343521465669697082515101763830578232445254473934405052615129631663858188/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^19 - 3377156272771316370672984962229163303289036415086828791144032639751424299759752610744701845279690418050730595180371808791436245124045894200142008271366721316/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^18 - 2351239012364327857602426422250040305647668470275033461137029525477992449099713283199464844506622166592593719900628881471908689856968980211948831590650922548/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^17 + 32554404451000124092236306677484251442301321966826269200392429696760710234481368991480335956275696205144204476777999849034695169322767466615116991871022420867/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^16 + 2709728916139312198109488908083936315166824789994401291608177344449733016680115810043076646465599774741703036909102362669494806141285480284979477635747746678/102074213667116149689671172885805043537347089432478210288076093599067552067167083290457846602265956499634112228973905440369218127609255616894490850537*y^15 + 13718353846941042396207927178562572375762306598013163558586119534426548015462803438263772139967368716597467653257923724665609349906279826229158708538098328199/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^14 - 12565681069479905924993417280055249725869405725040705964255560250930320757099261779830315564741268990046310400667828439466784996423768057940974545675090020776/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^13 - 37901865109186839351021276755455098640761993208147598147919629464030412036026060170484392537330395742242439673922583109744371829436551175438261445100461724303/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^12 + 1077964561682192230230781847772972475591796768974791175832027637646228378402146484489419268535534833742260446009613506402810772603028018562212986099225377589/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^11 + 95371807021888390442533331830585183989116016236027857525577272370042730181272869346763553882534577170648209351212822518868168085220422219362717711087643230/4438009289874615203898746647208914936406395192716443925568525808655110959442047099585123765315911152158004879520604584363879049026489374647586558719*y^10 + 3603972123195654358463932926977490904508091821635873815051337727518573059061042401395820765278364039351932635861197170140880053994355229870725583803702853947/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^9 + 314005456122606761717342963099913816829401965961682245791044362655870979322207171133308173412431745289466356504422205518020330679068549434983575410393294447/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^8 - 2112404745926482153905806291545092916698530666241916567754656345269160724279569417697737949005286118885725077883638331912292125111456541274180769779193712242/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^7 - 1139688231385951017150121332301873800674150189303041855330013745219803664933069721613565988822766047313515088768243408035117548084719945983529722456406966330/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^6 + 499125057834821832238790335072348054720616991111942364651398350988119680541490878002152045043248133180405405642260717088786954708479133491304324094003735799/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^5 + 187485450780948365821376747645048082931954450911175805108410291733176442297360196912229256710095681678000599697944996741735632202539821089705666413800751576/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^4 - 45857291328730851796713951217343677377073947152029353336998051961569604829602929077687706775575360445890830564133513575576703555331201688391693938379406298/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y^3 - 491795313965972657355896139882740455006506491995120091340492810703509300951706260817139025643845853872665203585841290614617513693683194865252663686053703/31066065029122306427291226530462404554844766349015107478979680660585776716094329697095866357211378065106034156644232090547153343185425622533105911033*y^2 - 35557460126912404196145700873546717185929379267270898055253690448953789748065459551313484617608925264482635417686706665324359440475691769716540931029365/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759*y - 10643598884274054296109304759041952660891428521834823594929104648301691180635989085309291073871943345578976638160293291648679255841694332689597605859244/714519495669813047827698210200635304761429626027347472016532655193472864470169583033204926215861695497438785602817338082584526893264789318261435953759 # 2 Loop Invariant 54302421507263855384087008513807326839713907490115158688926900192586105888683725447857460696807468057930394580194411692674464865552333825412558835743129162670615431795919326581827714076925552221485321592485556846171710631243877324245129406463387490661131407305831/141918824294610589872270920972167331384263672979384799662232605291991544792913137337213355776571579126438983432506609455537271378328931563083913604997023278860183606310111430834397850689435099548284684612496043128056490744403572964934425235557772319408719366811477492*y^32 - 269067416683779301033250859785235204550183120899776765891114393567737644444549762952888943833772198158211330916611827630072098895388097755252991488041555672918484336308957241098482962833852567022257625750655979098414721128490457028520887355860743346193760176089917/24681534659932276499525377560376927197263247474675617332562192224694181703115328232558844482882013761119823205653323383571699370144162010971115409564699700671336279358280248840764843598162626008397336454347137935314172303374534428684247867053525620766733802923735216*y^31 + 2209925806497168040205779514823687906630765218697927468360571639367140582479111810668366415623990386197668689189747897529098362996302979608843233569929991124584975618879794193974303127779154558793555011358284952400839272107983141392056998509906124503218512113171997/20274117756372941410324417281738190197751953282769257094604657898855934970416162476744765110938797018062711918929515636505324482618418794726273372142431896980026229472873061547771121527062157078326383516070863304008070106343367566419203605079681759915531338115925356*y^30 - 132637894879490408121265610797624858550588176069453736529421785209015541130489251448005671847205208682528451614072700721199957746282240855523261722526578364568574512106164115839789209784406160949305277185666137980284717392424843549714952360816257093253618719318141457/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^29 - 79031536398784606030123624629277742097780443387896897554732193894952639017505927610236601264129318745897904256864140007991131509237962173049189540628598051197456437560139389579758163256244570634358507917736618426899324855125955986480056136705350786115928562484305415/27032157008497255213765889708984253597002604377025676126139543865141246627221549968993020147918396024083615891906020848673765976824558392968364496189909195973368305963830748730361495369416209437768511354761151072010760141791156755225604806772909013220708450821233808*y^28 + 980431616745950600198261908680860896267829759533818370786211940313699455649391727049664881490562996895449352651180509819683932592171469063293168090262432029858371085704288143279259573740506412751788681769182211710109809574157373810379672629980772747155668840938050045/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^27 + 11716367433063860361114620300616364570818181982157986976887525070788323293890894524298969135083647624081023052649911997280775171832070552504622992945598006960267918786287357689409172497690218563267184798567646089368958939633613759832343818778933988807184150635639176657/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^26 + 10836024613112461721613438488465977158303836826581000280529831130623801936610570036360952431060755666412014428355259639840714076231001456939516466731180517374186363268860499929766744266104292849280505933750339692773900594259329242821501931787468923564874541327358075985/189225099059480786496361227962889775179018230639179732882976807055988726390550849782951141035428772168585311243342145940716361837771908750778551473329364371813578141746815241112530467585913466064379579483328057504075320992538097286579233647410363092544959155748636656*y^25 + 2492406347031610291716561290598006163607443444877851949396522725718084729528921026388742593161361697478141619216601165040800769188737794265318291455193036380720598488814026532758158544333034176565920681542384682522953177719790925589454369225370464942307454028637070284/35479706073652647468067730243041832846065918244846199915558151322997886198228284334303338944142894781609745858126652363884317844582232890770978401249255819715045901577527857708599462672358774887071171153124010782014122686100893241233606308889443079852179841702869373*y^24 + 89224673700928964831220904682113315337622339255725773500684266761792428823148086361469216630441767365939454493145286185212228281112593721169446950092710684463220914768876846586477488015641247473222663018031150662566888982564736247776563111896329161079442302061495535497/283837648589221179744541841944334662768527345958769599324465210583983089585826274674426711553143158252877966865013218911074542756657863126167827209994046557720367212620222861668795701378870199096569369224992086256112981488807145929868850471115544638817438733622954984*y^23 - 859247882059575115267010921727295882392632837818827669888131611007402459769813108142927317033550420916477101215232725275230720298381858370686197146896910277173235222747736821729333279122957088331681548806306580893646548539692041220640976742396431866450924641328879973589/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^22 - 337996423344751753989411165579971038544652684407628430580354033190615891562347546030299930684298663159240050571088761558517473923625782637175317354277524745587400939644638911295987500079012297890514544195728821852632294369827146538127887834409667489650250342901735753603/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^21 + 671205997692751791929986180121585614170305950381020166020473452236800377403637080790516974257601000834504934012206901736249205464226094118885250172984415887652559784674599824303486926937885444558772094374787185865945943593010224803752555572792040541707400716164617374079/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^20 - 181967479685850525145691082133855448924038053982402101120450432471606204343515204021939324511004581782749452758930188796548893162504493794250172040660874511895356522462179937770326939261079880883898155420854133541519567278941384517166976861644326959320458642484304136061/94612549529740393248180613981444887589509115319589866441488403527994363195275424891475570517714386084292655621671072970358180918885954375389275736664682185906789070873407620556265233792956733032189789741664028752037660496269048643289616823705181546272479577874318328*y^19 + 179681118453918681166871434992389888733384127224499863169007954343567363257735738920364821446223063079112743822303642972718507596663601457735950303351691660065250486205926290848687280463019269510978860291969484259442276152185424429589898640452097419364613250698351933185/20274117756372941410324417281738190197751953282769257094604657898855934970416162476744765110938797018062711918929515636505324482618418794726273372142431896980026229472873061547771121527062157078326383516070863304008070106343367566419203605079681759915531338115925356*y^18 + 8948803193171175114687143662116370109081030558352841377405940308413557054257277659048946669804321815004232443050125629444730941511360291405923797829220971524723425194996556821175156713568492946851243259514230771514811598236344110997129937850264236741640824742828517019/1930868357749803943840420693498875256928757455501834009009967418938660473372967854928072867708456858863115420850430060619554712630325599497740321156422085426669164711702196337882963954958300674126322239625796505143625724413654053944686057626636358087193460772945272*y^17 - 2567606512546331977097012537082695358220865683029322417495065995612090882346605842771200875947533977243416975263019604430834012041941793999450590839497296498982137347624082430277137851369756762942502005819808570463537835583641373055403226212203177541307749736661296162983/189225099059480786496361227962889775179018230639179732882976807055988726390550849782951141035428772168585311243342145940716361837771908750778551473329364371813578141746815241112530467585913466064379579483328057504075320992538097286579233647410363092544959155748636656*y^16 - 29973608296330083470788775231323041917416517364422183477997731546419589169189033451247521761364274015987563327475805142432847705169412838108834095812503372811589279958471776206075140040488641676423884360077597505599342909708203075939527395048820600016595151573089277873/5792605073249411831521262080496625770786272366505502027029902256815981420118903564784218603125370576589346262551290181858664137890976798493220963469266256280007494135106589013648891864874902022378966718877389515430877173240962161834058172879909074261580382318835816*y^15 - 562997106958375699194048944058144186284218740932947358479050230764889349604186333348683069865005147875077498231105251220891592200408900301032273533619752742193749228964771241518269656883549109637323844867046512572637605217295214845460938998058999327667130475732172959243/189225099059480786496361227962889775179018230639179732882976807055988726390550849782951141035428772168585311243342145940716361837771908750778551473329364371813578141746815241112530467585913466064379579483328057504075320992538097286579233647410363092544959155748636656*y^14 + 1647846400432020263897365099310725299479366992734317867992221601236783843835879461088918621658714099327945004252613292156927095199185704701498553999357656302862349031538711554072885677221826308789021000054417365443260009360568134950866148527902349123477073821029601289783/283837648589221179744541841944334662768527345958769599324465210583983089585826274674426711553143158252877966865013218911074542756657863126167827209994046557720367212620222861668795701378870199096569369224992086256112981488807145929868850471115544638817438733622954984*y^13 + 3823291950539134097058042557812516011670240829145204042091388388539212700551464272942739815010247894628771719719059518432057671341810820926385035504246972593231661453974366165426056624173321319265942422876427536147717582368586537999998852718986117371340573724009875454431/283837648589221179744541841944334662768527345958769599324465210583983089585826274674426711553143158252877966865013218911074542756657863126167827209994046557720367212620222861668795701378870199096569369224992086256112981488807145929868850471115544638817438733622954984*y^12 - 593119235273050220276687737571438814359936922633943825169923054299602468102358328382843951734181257374697348551236160989543093668401970327603604655980666092116531864855106305418082183944188088972116555198486761781011503091267451634096740860728064239239433625431955542377/189225099059480786496361227962889775179018230639179732882976807055988726390550849782951141035428772168585311243342145940716361837771908750778551473329364371813578141746815241112530467585913466064379579483328057504075320992538097286579233647410363092544959155748636656*y^11 - 1415606333964766228470038121418552151988207560328097806380487131078857790736325426998041028406342144151525405810458193128627547919237312532522430194689046083918665701963827334709502502681610038730312447238522116103288842188169376559001176813163629359895869873453840913/220370845177966754460048013931936849975564709595318011897876716291912336634958287790703968597160837152855564336190387353318744376287160812242101871113390184565502494270359364649686103555023446503547646913813731565305109851558343113252213098692193042560123240390493*y^10 - 18348969782794093962874625806645492661292886513166067652528412939673214886198999440137285059046073534611584177571566046654044362661001593230286257578542533673572429371854931462854351870047483403439375288137326407673760507604766832285354902959414263739471124486083893927/70959412147305294936135460486083665692131836489692399831116302645995772396456568668606677888285789563219491716253304727768635689164465781541956802498511639430091803155055715417198925344717549774142342306248021564028245372201786482467212617778886159704359683405738746*y^9 + 204641809366489053531375683755843809399751558887983152538762532233775868517418260408544276792709567564658781044290372519972182903556324037345886878909965466966437056444666353013477956328416073820391334464687948164333810902979802067320206001266470251874936970824057749135/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^8 + 61416311843016828610942377496325002925245091388294205964542981071889749157912888100578465355229826950473285769978028045701031045031966454980188821652485389763234765403679289863063882200303775688838839506834208136102704474331090586420119655214543413865161239993506025927/70959412147305294936135460486083665692131836489692399831116302645995772396456568668606677888285789563219491716253304727768635689164465781541956802498511639430091803155055715417198925344717549774142342306248021564028245372201786482467212617778886159704359683405738746*y^7 + 183124805718815100051982085151582243885597486206383000608558807575864689622259477319631317626457610067731363829960351667903531001801165133867194271475731335036642236741944291032941199836331301083598685202118620954009785701559706176238327171916062666284141726114527561283/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^6 - 169565224324599122744123019763183774035054115026765496779058875923140541298650996430806224322834632256766889700062897946024960349887308115897622700202540912840677846369659115009766513414945254105423517333138151692546318060799486007814287061888484090770696853006235459045/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^5 - 31118066191590020639541629683336004095643546586952191946508451719573239768572762584942278408503693618132584422448069143661596551675128503924799629733786110046789040341363421991145589085226265185097542443604031896420557069221094399248713048122055978624030901423809854385/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^4 + 20188976712384618110501957670306030434323621144060657069681176489904199853666280722317572131363396516500736534740255123938296514920352200345474888568254439484438744620068672866554990460471641599209996465262270871058645454086611963505402072243068456507836701661720802835/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y^3 + 40106481199856961465848332956929060619991281230467419050141266067998696783412397012597723374922759005569613203195928033921996229624576126993520324864017960598375245915074331086852652005344938997439561049344459052178442612658864911049597567286031225639674798823367667/24681534659932276499525377560376927197263247474675617332562192224694181703115328232558844482882013761119823205653323383571699370144162010971115409564699700671336279358280248840764843598162626008397336454347137935314172303374534428684247867053525620766733802923735216*y^2 - 553877825646619598094503025078973041221818910989576746771311690028889470913830862142347459394710240546671064728468217787107827262673728032597245333646186188776871773295239137847934193424259428870829481556367795064623920692679435101218103438197480456516900464591548175/567675297178442359489083683888669325537054691917539198648930421167966179171652549348853423106286316505755933730026437822149085513315726252335654419988093115440734425240445723337591402757740398193138738449984172512225962977614291859737700942231089277634877467245909968*y + 1771723338918690121391154861026428980574355230452150615456722976100463877363305414720540243431234323027258117190166682940756871719973218172209328180258113515642184339053324574279369096058282570829661523901488225121805847274774737287498170768356298983812149740826338303/70959412147305294936135460486083665692131836489692399831116302645995772396456568668606677888285789563219491716253304727768635689164465781541956802498511639430091803155055715417198925344717549774142342306248021564028245372201786482467212617778886159704359683405738746 # 3 Loop Invariant 17621936206452002710081325879488607666888446044031814892186444562795318435606830221464657699596410923355477628178115211950110421497239428424920893693957744393468606712191700959875222871120812261052415487924824572907523701513927892195147298623585836669807630590348090865139248974835935993164093438428512827518982614019357/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y^32 - 5125933802450086332201818513993510179246827077069823775517416798585184052473636835935536758388633568870011660069541226338190227446555339093546517173155136924277241250490331243482924166645999850562946638947339818274612368876421942414405380172263403960741463924053781082392100479423795572020683013193377320598205000250689/16735675536771978132297522073500955016245961779624350971259335524694269757675706101326245389915994948385869386733211970175643730626765385174231419651648398642684075833168932728282469213649770491726841587117443318842984467564362406292576003334068141898279701780130225016727699629280774155196447719624287064306640454660769352*y^31 + 297261079356956805261861818587094178421874426295266950168162435025391106654557445482603658991239221895025915253180688996510020220903611323695885731493658175220599875914265580740541298746682545373367522612578077511973112593382146159871691181013521309733038121383825199084231618442974771317512445217283244328745558947958687/109977296384501570583669430768720561535330605980388592096847062019419486979011782951572469705162252517964284541389678661154230229833029674002092186282260905366209641189395843642999083403984206088490673286771770380968183643994381527065499450481019218188695183126570050109924883278130801591290942157531029279729351559199341456*y^30 - 4714694278168364527262851237566434264734781100412112178770387945105603971516932612146313623772697087793067231097047831106769927966553990650455544328155361833197996621179126812063726330359413257007839759426250105334414470282908840252348144693594447108077862991279563047525370844248430377795993344157471953609549521632871569/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^29 - 43021570497059891323292690710929801975116526681072025990745657046624191524609850878038862031753365916433346669351808983847137419243783643640846979457515172262279672549964710057812699978049002480985871841004820743524277181278743300297174609723154142256876230336586870341223672376205267732125383279136218626492236819893709549/439909185538006282334677723074882246141322423921554368387388248077677947916047131806289878820649010071857138165558714644616920919332118696008368745129043621464838564757583374571996333615936824353962693147087081523872734575977526108261997801924076872754780732506280200439699533112523206365163768630124117118917406236797365824*y^28 - 315426047061856631747925708840488677275972548142527140482758075415770471625695832974222738564644553332935201414273673587867684915543879974467737704809828564120537778017536409485738922555293268834327307146424367445782752153505638219138303080551837106863906185546460833420202615035891636840979705069851358123652419878787829889/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^27 + 1007718624550025577966017169915485987693633171730560717684905186824683854429397897000291344220389852741038994176316649033640663260730645617195347305055096472997865670246521487161258781086499482070671092578066219569547953224699823960616300123002835232247390854741486708226404453096648897007032144319266663980293602466434730155/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y^26 + 8551462037130441889240558313705165805140343669413035561033522045812909934586287074693271240233742982812211149360396775557797007138825985600221509025325777291264470833729123952320316718090153906465798254875450697501572249172156647209223207255074432023561615821571326302912804975437215916826917396427856069045114064576205861897/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^25 + 2087793444025880912420371907224711781499274184015622167543868502294431157430352572262241897646254567727307411869332438902605485944880701285184204976741492997641025715999985041278104938552078919717346873606723788291994258261579406048054943135014983499307864060009579675938285126710388737148208346262869829385820737047577998191/384920537345755497042843007690521965373657120931360072338964717067968204426541240330503643968067883812874995894863875314039805804415603859007322651987913168781733744162885452750496791913944721309717356503701196333388642753980335344729248076683567263660433140942995175384737091473457805569518297551358602479052730457197695096*y^24 + 43863883750935091784694513824906943635512619329434849849622946014646797960287132763611201269178347422859327270015923887256758558340645244589964535095921367399032594332827771012701634337841055999419082675200808654640616846795001810857749915028988635152807603656695301382702434056991846271911450441270763709726602394824593836297/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^23 - 20846808568790149818683915784316713166471257940995626945654732145086878721988136463782072065008614518583163674651981886503060422860290246232070577380431805377051583309521296360662695261300119382537659072201426982214322411169879420294339839467342693568356277722983801147844477751235180400910555644281883010508267494816309101243/769841074691510994085686015381043930747314241862720144677929434135936408853082480661007287936135767625749991789727750628079611608831207718014645303975826337563467488325770905500993583827889442619434713007402392666777285507960670689458496153367134527320866281885990350769474182946915611139036595102717204958105460914395390192*y^22 - 276064181424987407860027247154017555092174384252864746150916664200547519366289276156860159947931954453873985850306573734837980796057533219742780937558941996066315359872403301711925362097542517685369401113347586113448156249867268286518243138241845662538059533949685503715715796961561852931082641765697117219112244221405185231463/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^21 - 13289181436273764352968844718971147764247093634171941101856857854979644181468564464034078793830449942642323673162969862759434518694395660884471822351204915057583246489650471427817954800073020210018177471492838244532891937535223587629595231883016852583782477954893874422218679395161947432190496691162374131970732664616235216615/769841074691510994085686015381043930747314241862720144677929434135936408853082480661007287936135767625749991789727750628079611608831207718014645303975826337563467488325770905500993583827889442619434713007402392666777285507960670689458496153367134527320866281885990350769474182946915611139036595102717204958105460914395390192*y^20 - 67189257248104680660527812292449536330625620765578796612994872422016164536336535934201385092297751966426946706742520743533399336036332197742094943226901777355094421124645129402979360078068887263644174525354370235041584542409721633776639454279730943444395541272818172341020787260436287916519817027156143076016664179920648669417/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^19 + 76682068204900384924221926852824644898068147506754963463408184377797660028953818088634140800358588902907545334242426902992173456895430929333556375321721948837641068058695936718358038402326225591861219696699004438871732739403622217904517282700519060081912496817679357450170160115081250770397668395228290472122132045909900544029/439909185538006282334677723074882246141322423921554368387388248077677947916047131806289878820649010071857138165558714644616920919332118696008368745129043621464838564757583374571996333615936824353962693147087081523872734575977526108261997801924076872754780732506280200439699533112523206365163768630124117118917406236797365824*y^18 + 62686859744399277992029043403417724401968693919422824536539757364316387655696725099812962197464880657490391198521682998938607198270068052179717853685119333907740074942834184973159022936229660561000419708940798839233172534167649629896007092905271833682955662564588368248713754889361241734040277293882217425768746841433448992741/109977296384501570583669430768720561535330605980388592096847062019419486979011782951572469705162252517964284541389678661154230229833029674002092186282260905366209641189395843642999083403984206088490673286771770380968183643994381527065499450481019218188695183126570050109924883278130801591290942157531029279729351559199341456*y^17 - 27231913160207750280306565207521231966231108589106585449673016376888470663922985802344120904993931820135683949806842206371716346934432976842850486933307597322813465560926485805674408352460937361428027093665595803217427964981940503550235327094117907676974313632788652389827983800847734400428652403417171946043728890646011554805/769841074691510994085686015381043930747314241862720144677929434135936408853082480661007287936135767625749991789727750628079611608831207718014645303975826337563467488325770905500993583827889442619434713007402392666777285507960670689458496153367134527320866281885990350769474182946915611139036595102717204958105460914395390192*y^16 - 301195048727071089102692649519686189593808319115984877949078293383241383610390551715185925418005105586882646401303732195637535883311794939478314471771397869173583624495242090119396042035012167784855282137636611953653225657653236030869280620986217926606348481404381374843802243212684048738445282362445898069478473984485692615065/439909185538006282334677723074882246141322423921554368387388248077677947916047131806289878820649010071857138165558714644616920919332118696008368745129043621464838564757583374571996333615936824353962693147087081523872734575977526108261997801924076872754780732506280200439699533112523206365163768630124117118917406236797365824*y^15 - 1563052379956230348859623347123813570765989775030762475843289829055862031742715015913414407659512532846440222393693475114180127407949695993654976195024597526486385462306365345564342768760542192991064976753314064909248373040029726135841315385890928694683485917082897445267222379692442452983974646862959477283314332534791532497443/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^14 - 262593427172692828039007644563796747660170969971010936573196774216041660439897302071614399080697725015674868772545118245720807677953718739594587577376666465149126668291683057554226239387132992901607800877251175392442232571330127491432686688038155632272237312050498740765469381149958828095598475426315680466150472721816240455413/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y^13 + 874521849431180781246736264931172229344597433459840839717001581026811409061498678302072032360906145402811203089029519202984939822164393858607022711752742158913209589782226190236863659430466480923141582898522498682360718646048296685460814343306030812179854350469755199036142906210855139175315659724948418872620043613603143912791/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y^12 + 474521887983341749876105567506448647299264448823898796396610800411387782893028292986220010854868571992050125748172441861083250865437010328846329528621363186455260065401814774943623094590110118361786477065037285335468030238879377318681818541896469086875988347060723433341923612152786112948903797135959183321691206864741047080245/769841074691510994085686015381043930747314241862720144677929434135936408853082480661007287936135767625749991789727750628079611608831207718014645303975826337563467488325770905500993583827889442619434713007402392666777285507960670689458496153367134527320866281885990350769474182946915611139036595102717204958105460914395390192*y^11 - 1920699639459475918124271763961972518463630946174534583861740552225690768291915411281605113197161978170197750649376791693765589701237056576102841850984936405812793235796497437494711805400833867670376365275492558026541262563339016490225860395197148666059225783155268762921905108587674264276592822152941968033916840354552534873/19126486327739403579768596655429662875709670605284972538582097742507736865915092687229994731332565655298136441980813680200735692144874725913407336744741027020210372380764494546608536244171166276259247528134220935820553677216414178620086860953220733598033944891577400019117371004892313320224511679570613787779017662469450688*y^10 - 774262805597454205129484707078005025058236495058298871192197123192323369158909569857283910518353026899627838894496274988661464886551489829802066572694320525152306260679690135344725450402416090637343938862574900322319373461653417171737665535126038523623292316469453292471786019411078696429617927454691592048466506077547053378799/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^9 - 4226268093489104356719525071504318582257644067778167136938806877794555492716640680810311918287628672717312237602739516768506738080844902522510075916891825606656495040090253956631484809448377048499931565841361489665358583309295986970093552400323837067596550123612129803660617036766279855003352981237269919975499351472898171400/48115067168219437130355375961315245671707140116420009042370589633496025553317655041312955496008485476609374486857984414254975725551950482375915331498489146097716718020360681593812098989243090163714669562962649541673580344247541918091156009585445907957554142617874396923092136434182225696189787193919825309881591307149711887*y^8 + 7163657511353052901214256651262333968767596134104271657981757737299798754488614071620902690899339891464951343359554706715607735822358947634113253957097104305763357814825572192204018998775695530757323550959025222667904798400054812157645523005765198879070593156728442117169066269344828527249445667642070693606681713114838477717/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^7 + 16418103531659833504716219085939551931000544878222401419102290303286558594435296260827373752582148602025404693193574316406613055535811571310697914555459828153133402426657116530565007271492031631494520424428369207701518207787047920184215667606211651227195646188649599422002915807817107655957557408570645413135757290929515302359/384920537345755497042843007690521965373657120931360072338964717067968204426541240330503643968067883812874995894863875314039805804415603859007322651987913168781733744162885452750496791913944721309717356503701196333388642753980335344729248076683567263660433140942995175384737091473457805569518297551358602479052730457197695096*y^6 + 48277917973595585596916457583782595120622010151285997090645154472139074165396046478154575786747345484983336670629870767671463791027895439775293484216116000610287080784558702330365950008102873660116939045793558243479873568184526904660514805570613873464629863054127261685663194757796608704180480542089447596278801863264932264923/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^5 - 19297532689822347941451470417146068980884198191531221515673560983262400091332765129793998336654854652337220967524314960710153491668667978264682292990891829472061621840519603935430773515616986646820061413383737239100837094274129607528669308959756138153099152645775966764160575523939658911445341266118986752379681720621079483905/3079364298766043976342744061524175722989256967450880578711717736543745635412329922644029151744543070502999967158911002512318446435324830872058581215903305350253869953303083622003974335311557770477738852029609570667109142031842682757833984613468538109283465127543961403077896731787662444556146380410868819832421843657581560768*y^4 - 4196119175586576667709911754623384654320969394119496730516192531532372708301374330855499061421732094817425041343700021189055626566782835744418957353169843708030244033713281120350217545306896773315159107268479508695167982368058610832497300866649593796076333726395111595363876190650187427539999382430951020218254579924607409609/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y^3 + 17202811605179787668753407591254216288243938852120219777981912938985443035987704590781517012592581455441009825425138981640265414046392624339998980743039906632232595987754048134813440381364112808126941878165984721752902071585978923826683588783820679683732483189592617910786399409907263486289092139847793613669634097005872903/66942702147087912529190088294003820064983847118497403885037342098777079030702824405304981559663979793543477546932847880702574922507061540696925678606593594570736303332675730913129876854599081966907366348469773275371937870257449625170304013336272567593118807120520900066910798517123096620785790878497148257226561818643077408*y^2 + 136090077421743082313353943336930894715588799155309705763637236251940498731948688475999444745000692836806268887901522002494794474960860560523660816449220886980114812342221011831489861781466244139576320128947103737418429238806861295811080848617333667303820874374926670713670822601034560104489519168504652749057733212920531079/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384*y + 7955122173271396692687806000159247243154843608558418095462929174591987172706316813872785865421261724979350108200969350404425247112772889091604837865662220267813932571360891401572562437928476938880015775504987231649406469283560189465154285950196706307068495523697886569335353016925408327181214756205543494020162473576400999/1539682149383021988171372030762087861494628483725440289355858868271872817706164961322014575872271535251499983579455501256159223217662415436029290607951652675126934976651541811001987167655778885238869426014804785333554571015921341378916992306734269054641732563771980701538948365893831222278073190205434409916210921828790780384 # 4 Loop Invariant -530490459799372562472989125719652541974485851404439353093200433479626787799363032745238341975304563291787641376577384665885936765768475465250561348475055475752513078811406630817027419908146774436802618033173468923247152447131004073962076697464983040706943242484641204406114824535738407540492507790804232782187342706711292100642097598276550515183653166758655803024817437659379660879851339025721926292702326654042054413540320783016770621667/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^32 + 669804032073220283527499272249211596096322115767562910806774959346218069243028209143657590575327583966775452799798390732587785230706728115439686644967107348494500036785239128904902704078103147815809275921209781046570905458852476614851034553886062789087243354509456897109171627990343053841397523318771410567670730477752889511221212154102321383855086314794105940772769091754079452056332963971877315791932126973855763181960612556419801945373/1595549956253555104742153057581376165678292868168693825807505376171950209425873670867000809211169266369536085373882518383087226296930443196688941223755256118031961163819913571263580554297299896046640150884877619142136517716150953149783524457167194500155152077927682711894974561945294264713325500536059792630534549033237024091582800229123807452030288539366137581003700149267476112249301435216713529798967637020932438702905461421568542243476480*y^31 - 22764111519899591819201363501388955407784758796378214305223897364952530637598865707442225610882379555648346684095008703016228280762293160209410619073805547104730994725809955368040000132919719921619819132798587210882630354066255977456255550522977651167660662354569824519911255178553883704024076561945088989468171974215900034970423476258314174771678476688935488568559101158617178569313713604521571068568508415960713033093848124685681276120903/5242521284833109629867074332053093115800105138268565427653231950279264973827870632848716944550984732357047137657042560401572314975628599074835092592338698673533586681122573162723193249833985372724674781478883605752734272495924560349288723216406496214795499684619528910512059274963109726915212358904196461500327803966350222015200629324263938770956662343631594909012157633307421511676276144283487312196607950211635155738117944670868067371422720*y^30 + 404890153806817454175042947167197255344729965343406878759307700991735613152779552704260716985043104432167803582676422464222545697182093851218009569228101845412772764933980913868804419787179887949041944729832246477114788882260286423071796875475055914793543109951033861971712019263197374003008546786221965924338498697313556139073913412677684222766149778347619145596503139761284683317094785255092938038947725497013432628087206334031004821228659/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^29 + 556372708062629115368097609060352547109337961397824985046578657030902492339410890751518001021199321993880900592349394130000842502163939077634566520238222175192435153985834087485948727432368988322418279340341378369996474171084810458999658853712352013045777960916008656886051315745123378410561187709670855969976632080963400465105607831569990431550038951168257649078801229346537658633851550656626385098715779056097616767110920651619379526794959/5242521284833109629867074332053093115800105138268565427653231950279264973827870632848716944550984732357047137657042560401572314975628599074835092592338698673533586681122573162723193249833985372724674781478883605752734272495924560349288723216406496214795499684619528910512059274963109726915212358904196461500327803966350222015200629324263938770956662343631594909012157633307421511676276144283487312196607950211635155738117944670868067371422720*y^28 - 4647095462668623474664353145064413033869875243892199995452226249799186760008876663673614583447907491034334120152021866516108361379095051201990137526080057058776552748858031562765971761942966870204511302762159936772093443524699930797520466981150170576093992577517247209320176139961789281572967216049830312877834765961700368712516712878659601241648240222927387321443879514447427130933064158133049320127479455638880045643338892095636394757303073/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^27 - 774968446452743752413100904534064469888809837036760905894893291421714377342317509504215592886525468179319912405834860123744928091962582511360340643512914386747720297027048752670724910689942465690488322637657405607938585457598578690248603809126039502292679006105088325665147748015139494262875192847606518221169926219898257162649217797498387145079222621416083620895539350486277322691657904990564011880149242623601484215480052792902397288668717/1019379138717549094696375564565879216961131554663332166488128434776523744910974845276139405884913697958314721211091608966972394578594449820106823559621413630964864076884944781640620909689941600252020096398671812229698330763096442290139473958745707597321347160898241732599567081242826891344624625342482645291730406326790320947400122368606876983241573233483921232307919539809776405048164805832900310704895990318929058060189600352668790877776640*y^26 - 63763037742593045225449668935785414886187406028238094292063921225848680614507727607667061907147712494439697978023952048109043835058862507432566045747599090229644181078447360210651445125505065086493928677027306865830864118329763529860003905419283795334508944492974115040276232611096334195783702616299146906919623418944223271478278201946099602053286107776961020001051201537156076436464830236547197408365063172871801920323353333265807414654513971/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^25 - 24684071723200335817970562683549456822425875420153445112124900304390104449249327641998909083888349561530081548973296729563125327388583373034645411362864931095065564781167448394621738122320932121680200438347563353224901087943171797111241989361738947201823503602196972538624404301061343918358724198237017044696872780757664211413583179395437648670198981940689022454354569978302093188166017855066034619718920516169610100287436674286809278960581379/18348824496915883704534760162185825905300367983939978996786311825977427408397547214970509305928446563249664981799648961405503102414700096761922824073185445357367553383929006069531176374418948804536361735176092620134569953735735961222510531257422736751784248896168351186792207462370884044203243256164687615251147313882225777053202202634923785698348318202710582181542551716575975290866966504992205592688127825740723045083412806348038235799979520*y^24 - 46070384457622940965840095158914316273385094036581591827028725388423389462156196155980677106187068727410888717279747391226816079668171334209962411781104473033367045150114900849596637653863148183215840365995818868426389774981616532692438422677209729305261890489934438638895129523506363557562640495851935082901326885254499405765541807444023312136606951913502915082178472036368296916723286538773517901482910068345425868886995687239839074378961939/4587206124228970926133690040546456476325091995984994749196577956494356852099386803742627326482111640812416245449912240351375775603675024190480706018296361339341888345982251517382794093604737201134090433794023155033642488433933990305627632814355684187946062224042087796698051865592721011050810814041171903812786828470556444263300550658730946424587079550677645545385637929143993822716741626248051398172031956435180761270853201587009558949994880*y^23 + 2357654131675067649403694150119646179194410419788634701315333887198727430356627230737695037750049607603477282537751048476948974352754726312102508921261873777237252693904752737175407379426481661092369320284145391946913776600432935076708877808202033016686518772565111038550938121337111996766762769380807974424320238208502290913155668118787407360339823849339315797471854825368309464006879987268396999329933871001608831895984250312676040252804468387/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^22 - 262850826349912154397908738938439211541560227031479985600266125974645280486192111989542612571457716488186479062188357657738631707207388157120919201080035367074939041993148224529262912085466294672022911190301709213238707238993074998264097205908983829176166262524741799339566536971863557829584296654592897317742234934267669146123233029540965846726351254402328514658241932759100627048995463801988040940912955147080601524747736029373463946824123013/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^21 - 234401383939495853102521801996944049490766561984230689845974816763550940478457626277006403376255362357321116440386796342920349172196385053346150887083550757221724996176030139956039503120324193283579555938621583255777572715562406023537546799947416514093714021945401568694512964432243509767278503508367340871467582962654540699919071096765294243831606426947967635425993693761267711800024077839291399647079205959886902375254529990038370846253283423/3669764899383176740906952032437165181060073596787995799357262365195485481679509442994101861185689312649932996359929792281100620482940019352384564814637089071473510676785801213906235274883789760907272347035218524026913990747147192244502106251484547350356849779233670237358441492474176808840648651232937523050229462776445155410640440526984757139669663640542116436308510343315195058173393300998441118537625565148144609016682561269607647159995904*y^20 + 798944104605899092999339770767743285258254432125985889514936668336758698857849253459795102575007700596234619398673830395354119532255044834016433534515283289322129783961368829101023580170685591823245340540488573904087990842523416890089687376552815532043243864510719854071306050202001308833379053137359894625039814299039546887824486062279216597347557274018086614361503895326537743901478876355029637366238190342823532065825211194149649420734287053/9174412248457941852267380081092912952650183991969989498393155912988713704198773607485254652964223281624832490899824480702751551207350048380961412036592722678683776691964503034765588187209474402268180867588046310067284976867867980611255265628711368375892124448084175593396103731185442022101621628082343807625573656941112888526601101317461892849174159101355291090771275858287987645433483252496102796344063912870361522541706403174019117899989760*y^19 - 321121685195175386693213315455997581663820226519768409779558124204754071965991762501951333280392446854462867573628374877882082161822134524695274800071746080761399195871526917532970007880092486492335251080486797176878705635115036061078093314113092145461352014251325274915032091412780288481752762749442496231905673942443379368305928967889443662606263518156479735657222524148481606509126610584397687580612521566182584292015809921717779664550628737/873753547472184938311179055342182185966684189711427571275538658379877495637978438808119490758497455392841189609507093400262052495938099845805848765389783112255597780187095527120532208305664228787445796913147267625455712082654093391548120536067749369132583280769921485085343212493851621152535393150699410250054633994391703669200104887377323128492777057271932484835359605551236918612712690713914552032767991701939192623019657445144677895237120*y^18 + 804214516008448788190560472164601938860856608069535413159561969427058664889793556917075818533441563134566168640515248221986790479790532315955611017653621282096211721490848573330575934721759578592362263046420133004222195073042239208924968776739999828612349803869555983819122235376131513930649073943869354217566210271935853173316564598146829832258984107553242793091114434874960196913466228555517603081358576604605730656451740639838804631347243/149786322423803132281916409487231231880003003950530440790092341436550427823653446652820484130028135210201346790201216011473494713589388544995288359781105676386673905174930661792091235709542439220704993756539531592935264928454987438551106377611614177565585705274843683157487407856088849340434638825834184614295080113324292057577160837836112536313047495532331283114633075237354900333607889836671066062760227148903861592517655562024801924897792*y^17 + 4752133985706574731732197208201033848172180019330590174514619659328625633741874259410465478963872969119854298869755365895830114275931047847575335047787891242903539748807342812043302228055717057129850207235825678626776429297632995186316193697121033377002474287974301213470342473268269127296074966852296253179669532076040913205299675146927569784837337904156794231888784682137844497841339033908004051777740665544708196597654876621065728537263041829/7339529798766353481813904064874330362120147193575991598714524730390970963359018885988203722371378625299865992719859584562201240965880038704769129629274178142947021353571602427812470549767579521814544694070437048053827981494294384489004212502969094700713699558467340474716882984948353617681297302465875046100458925552890310821280881053969514279339327281084232872617020686630390116346786601996882237075251130296289218033365122539215294319991808*y^16 - 7656175876162315934371338661970821408297927588287323936115596177035670879278375650513741144493350102354340292503598892818302973350994820825630359061237894198309467558087668995125209949562441863730349913253156259125671942712914667767523462241878496993427737467968520375802511848321247707096395944796508314577237815280506722379482176384365138115213206613798283642937244649249732456505470934580084484576577651277850291265378040170577100393130853/374465806059507830704791023718078079700007509876326101975230853591376069559133616632051210325070338025503366975503040028683736783973471362488220899452764190966684762937326654480228089273856098051762484391348828982338162321137468596377765944029035443913964263187109207893718519640222123351086597064585461535737700283310730143942902094590281340782618738830828207786582688093387250834019724591677665156900567872259653981294138905062004812244480*y^15 - 2524120542666084673671067924218893490326173478168063350049430867637610529503499509013614292100906983638630461313189253347522545909596312397078372080891380723559840216403267028533246194999760503422122450032464003775279335062743833991521404282600025004633090584350330365198580250352232606830893956184728052295974661420386915882947321151588979460181747961653200192845010646027616087945218091487126912727032285276855208957574072988595950221885150901/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^14 - 13805988231993276002882251405130382168552621662933755018193541879393333869908151387409843217626013990982212496465219485284886605956006558108395530560481790523041154002320561811377700069765978651943213522798369114791093436229081952720786053081116081460681866444840032620004770423920168595458366556281359166307716875446142850339030932898791720910155842656145209011473726272441913983002752946652702000746952472515047875916073859959332655679359964431/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^13 - 15123145820905688983500288828833514672214377296909532287825584145268206822588087961816055168222412397658358657878304493626469992101493611569498909345588019460073704637003904852228137207759263736325385616189423538418501269900984775412471666215725372943593102180088457561353005671623824445986071223979229362504561966630372777125711179135785996528724944537218542827727683666237395689763501360813858258291178447276313133019496437574647580536717685469/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^12 + 431716484036625804407068908605082500132555397921884223480591222539815004277753955439421164096838296562721197309732151735136367674678136405057263659989581885700936404954323782888889563335964366140762038907647445125518179466060059630518363195207983652947393746609081625452499408984858186989444257067293374039423182061894873254106303411657177153836493148201028720246980188194135281366764975117444875742725347255387197479106786852490222968604937269/1019379138717549094696375564565879216961131554663332166488128434776523744910974845276139405884913697958314721211091608966972394578594449820106823559621413630964864076884944781640620909689941600252020096398671812229698330763096442290139473958745707597321347160898241732599567081242826891344624625342482645291730406326790320947400122368606876983241573233483921232307919539809776405048164805832900310704895990318929058060189600352668790877776640*y^11 + 2845777286485423096572321112762967095962151376502665854446143080171517461083557530184546582784201395358732090406952942084082334531442964861558616717558400407211988877823660350614245733737103706185267930408466705609725783564653194468886511231025654697854198737402970910994211214807214593279195820611280649123552082215248434940052780386467375091662639943293665659890782693951997129703880887586877939614144830329947093414232951857808103435293851/9497321168175923242512815818936762890942219453385082296473246286737798865630200421827385769114102776009143365320729276089804918434109780932672269189019381654952149784642342686092741394626785095515715183838557256798431653072327102082044788435519014881875905225760016142231991440150561099484080360333689241848419934721648952926088096601927425309704098448607961791688691364687357811007746638194723391660521648934121658945865841795050846687360*y^10 - 380506143477537025632524167693149314390573541918538082859988425453010270323232546782845741289439341233727353002072276606656975317230784387382134348391479555418321735655344736890479686283236909972737485825599142703985678201374224303743310807046864118974738304903790794038862352385205316171411484019207529043423804760735572555056849148966202094402229881222233558448768746142994775563123497089894792632000959576554344227020591419350149293068894167/4587206124228970926133690040546456476325091995984994749196577956494356852099386803742627326482111640812416245449912240351375775603675024190480706018296361339341888345982251517382794093604737201134090433794023155033642488433933990305627632814355684187946062224042087796698051865592721011050810814041171903812786828470556444263300550658730946424587079550677645545385637929143993822716741626248051398172031956435180761270853201587009558949994880*y^9 - 506573628669143339001940027536787935550176487362173429754943208417999119605761601783528963021279180158783926461024649053552632906434356432481839635568456885334841889627688760754538413921183933084665696950776035225931823924282158560200343005726162710141426233867221772954446331018850767038190926483174880565811891307174876241121624510898307214693707418539957813368513356147523384176774667169364802460700830129814707719780862739253175289576681679/6116274832305294568178253387395275301766789327979992998928770608659142469465849071656836435309482187749888327266549653801834367471566698920640941357728481785789184461309668689843725458139649601512120578392030873378189984578578653740836843752474245583928082965389450395597402487456961348067747752054895871750382437960741925684400734211641261899449439400903527393847517238858658430288988834997401864229375941913574348361137602116012745266659840*y^8 - 258733934675932972850484531106949253329278430228702122380088959957900583382694758817285706229188892192135702927611868246115203041646325678412884009791816837956842257261373378047580345814408241870760472774492818212160871321784474671097610076301478992032472677856603106514653100451796691507448723405822320574621843950707655581123772087066006797960152309467084102480772395412381271493568458660250246225685623197198348006646544916130003838635857207/4587206124228970926133690040546456476325091995984994749196577956494356852099386803742627326482111640812416245449912240351375775603675024190480706018296361339341888345982251517382794093604737201134090433794023155033642488433933990305627632814355684187946062224042087796698051865592721011050810814041171903812786828470556444263300550658730946424587079550677645545385637929143993822716741626248051398172031956435180761270853201587009558949994880*y^7 - 5663108323518969598684926746489654127262040553537931433545221404502347041932846763021585957978445053722572945259381224012339464834816517263659564158246818746567657608541974645870356661704221152693607856105576694997297576970577769758259377488354934828951815338096813571383182399166202679724176164324513803700741852847624613264197648106122031187379030044349144446551016833442383262166070409837139870669464083668144414861295141786492575556043519/9174412248457941852267380081092912952650183991969989498393155912988713704198773607485254652964223281624832490899824480702751551207350048380961412036592722678683776691964503034765588187209474402268180867588046310067284976867867980611255265628711368375892124448084175593396103731185442022101621628082343807625573656941112888526601101317461892849174159101355291090771275858287987645433483252496102796344063912870361522541706403174019117899989760*y^6 + 83659276537812781307245937769735895874298967338423052179980313286965093571960968859439974840875002328456737746286531127182273756129769394251658490296584705901668306762209954090812419487490762668535176844660772641763238253631560710635306587466954105209836192027854970262529954009628452683274418234262179669987589055423771885810631040507394024987775682547634238196263341429181836987167005961325316774537271560320991534078127330091387506721481471/3669764899383176740906952032437165181060073596787995799357262365195485481679509442994101861185689312649932996359929792281100620482940019352384564814637089071473510676785801213906235274883789760907272347035218524026913990747147192244502106251484547350356849779233670237358441492474176808840648651232937523050229462776445155410640440526984757139669663640542116436308510343315195058173393300998441118537625565148144609016682561269607647159995904*y^5 + 131679433660771964244113841112822303335434491155947876237551914641457998498644155640284719982588509850644291221172514413063863081947366160365772866714352200622986038906552524649978264312437170997140183689530877791165766744148684002623995902511926997362580777796360711557701819493963656945921900521660159049303434092101275524694418877476312451464179842165753055091535717807980505099410376660027253571317254846301827964883497084150777624634005861/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^4 - 84636500861480919910434620620345262769387598889332206053830458509862582276303420364671107706621438874142029241105699951785217830678231645484268589258614720079462399855377641067112073891135144187773424765042427567231806587578053494882062349557815111953422409238216979916461951014499425956735835104155272373507810618792201306879148468404864380403231588254492689967821715790977157994012644961295291502577943138576544619500419473463373715720296429/36697648993831767409069520324371651810600735967879957993572623651954854816795094429941018611856893126499329963599297922811006204829400193523845648146370890714735106767858012139062352748837897609072723470352185240269139907471471922445021062514845473503568497792336702373584414924741768088406486512329375230502294627764451554106404405269847571396696636405421164363085103433151950581733933009984411185376255651481446090166825612696076471599959040*y^3 - 59890333688702161277418895051018515241923298223981840895277625310180015589370950838040725861176880857321084091738590841070401420018115936001716590627437426781440205001874201657154407532649730004503650471397326053104848857797484876008576980407228133534196547051014451214449177459141162077839267327116753349138947373418854305683789723823816271064795020937183752961013807969469885462838992189090071576128736888566580053667095777440159625969387/398887489063388776185538264395344041419573217042173456451876344042987552356468417716750202302792316592384021343470629595771806574232610799172235305938814029507990290954978392815895138574324974011660037721219404785534129429037738287445881114291798625038788019481920677973743640486323566178331375134014948157633637258309256022895700057280951863007572134841534395250925037316869028062325358804178382449741909255233109675726365355392135560869120*y^2 + 210037970910982132582728987070993536318983262953266284944722443282463015908940143045826175659600136417086819793898070801469768254096989986399829976075201350695122993408424865206836714679176008796292214868514469855083580826691123536846928732393412593059206457139869574943297924024916154456680913512477115199392259747237536897607361505172686394418795058596554070957823045945276425796136595820694044902830130560956708156414624042900466279600147/2038758277435098189392751129131758433922263109326664332976256869553047489821949690552278811769827395916629442422183217933944789157188899640213647119242827261929728153769889563281241819379883200504040192797343624459396661526192884580278947917491415194642694321796483465199134162485653782689249250684965290583460812653580641894800244737213753966483146466967842464615839079619552810096329611665800621409791980637858116120379200705337581755553280*y - 42108100841683798221028157947237445812208380628340809111978023969058817722315130215303919231459030986137810655262784944034722652259417045875708188812856778992997651924036770650711064545110350820599216297041033974670975420030629929571374963577563331299181449060082390935355670137041927832502234767257293880871025150897386990810508882136398325547817735589432865117830331394123647587791668911976840510775794439731336047665756743376364864435529/6116274832305294568178253387395275301766789327979992998928770608659142469465849071656836435309482187749888327266549653801834367471566698920640941357728481785789184461309668689843725458139649601512120578392030873378189984578578653740836843752474245583928082965389450395597402487456961348067747752054895871750382437960741925684400734211641261899449439400903527393847517238858658430288988834997401864229375941913574348361137602116012745266659840