# Manifold: Census Knot K8_79

# Number of Tetrahedra: 8

# Number Field
x^37 + 37*x^36 + 582*x^35 + 4630*x^34 + 12896*x^33 - 79234*x^32 - 697617*x^31 - 424489*x^30 + 11982019*x^29 + 21584763*x^28 - 136782359*x^27 - 220500308*x^26 + 1144256626*x^25 + 764259084*x^24 - 5659133120*x^23 - 396435984*x^22 + 16419844543*x^21 - 2229238015*x^20 - 31736202399*x^19 + 3195472765*x^18 + 44213405793*x^17 + 4045041395*x^16 - 43861663827*x^15 - 16579194716*x^14 + 27225794253*x^13 + 21138507294*x^12 - 6243338071*x^11 - 12709887833*x^10 - 3379015766*x^9 + 2638944789*x^8 + 2205059154*x^7 + 472413839*x^6 - 165051789*x^5 - 137638110*x^4 - 41994309*x^3 - 6961522*x^2 - 613298*x - 22001 

# Approximate Field Generator
-0.310699991137654 + 0.295554655905815*I

# Shape Parameters
-5322207585833538817616397031810921020390408836045831255710541192819830660533490623463262165272281775553282419807879833959034965851034449647279176004898519127373472153248140907537545/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^36 - 97567308987291312774827161139605415672341578919705131702403256072236429773179761465414692555501582548850114966081272167263696701737087957306550547076961512884583122253633431953889603/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^35 - 758000882573216292264462882789694559739085753173305831756627155677044712200451191416990227217248949551159943761398829989884517272284019399323333728298185169581602101781987353114055779/1306916497743271751610892042844658942990603927121684909115789028460866132131050635104180601568423529736819509611127489334588673597111659265428422795863659225852664558615175829834272*y^34 - 11811875232772732633124047033110859712793103958349817031025018234991068808399999401217686640394461526738458672818331930341361139414310809690992225875390017833439924550290839664849476081/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^33 - 30351461251709759782963842382073957879086614812634783770721595324805050859993101311531238237656002906086071517697615731273556705642620801933440210532468867559676320823732825504806422649/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^32 + 27630148033778942990777930871216610611091061444315466231014754434443076170976030688278845690106301252767292982356223717767874681402282731792874182761714591265878823054462667827736499909/326729124435817937902723010711164735747650981780421227278947257115216533032762658776045150392105882434204877402781872333647168399277914816357105698965914806463166139653793957458568*y^31 + 3564422577719131911928291010023862616727471687102070073258688228374338980889174138404301482114559561339148076295481894429591922605833449688890111413328241243963901854464422307455949265753/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^30 + 531187172547677933033910983725678452772369374036149867379478600590719548810993235156396646530969237416217904678580242359391650080412572967570938936214046560805865809442456113092718608725/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^29 - 9161074415784202093340370613278439535661310554810659957221053723286456469776942202381050565594168823983958995527729517159230754387759069714912606350274629585695629489036810250536202636743/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^28 - 23336547953233506100736340982627704880360866603759514131791608733366301156548550241209422582635746005982731402986878909439790313755444077542824181288228883048298394807598849338289642771981/1306916497743271751610892042844658942990603927121684909115789028460866132131050635104180601568423529736819509611127489334588673597111659265428422795863659225852664558615175829834272*y^27 + 108475368936326411159899636908129123235802898695201713851528506640346574068109068953920043785549850012168104016698487516639584310608614867922078342403929420955254068793783763707588645292989/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^26 + 131226523472373745167445459440530283151830242362796845585056077719096526671753922728956035687865059644112319357846125572656782207129543768660510083640266822743378872555907492258408364642505/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^25 - 6398411324747515613769559647975582830082620816863782140184379813159159342138387450384559152359801320992847038540785870558743162136586846662135603745235080091476025244093628983462639068203731/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^24 - 1919123234550546042292028954374101943943487626919794411714211733255680257882965554830313308026502253731162075120404924620271045497351804640841111607706867780857883958425716187577805306501983/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^23 + 30763492830134660368520144688580373277984034192974438559924380846905634255604438580226666949238897970760537099179855093694961635720813326575588285484784407276862417333671358727035501404955377/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^22 - 1174240613543367856195084186038185513824023939837530416959273118172187789137440126779878670447359814134564372892287596579435482890265761191427844400901261407286384888629826690172273090781897/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^21 - 42314974019430385788145316573676932289894274700846173620984362721601839340295796877677465898619041791616248812503647032870761679457342173935393952422904915915311091013691491513261146941987523/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^20 + 40281094898091102856115455948505036041534760849489717222852722984230265359659860732122001221846029709075491572603214386863833016777618400757299814514176751939889342450592842939619679551810625/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^19 + 19422690835543855005180720857830533980087178710279593513665039309851491138198987621428072749719497878468728850020339274681663459901064195975081147384088452868833408339385963458988054864505523/653458248871635875805446021422329471495301963560842454557894514230433066065525317552090300784211764868409754805563744667294336798555829632714211397931829612926332279307587914917136*y^18 - 69180294781190984060981314326153079062905213227520654020233529080726571822475258218059534474828875848283857757138883587196326969781193627380796295460125525330685818917090827742513105050653453/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^17 - 106042185036677197661629527419307127963761655685211453845574862843813540218250913293645538310312293666893210090894370597603886153238969409872492813262052653657779956742117926336725597482722259/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^16 + 49684260783559398388415757872222095556324855920483830784586858314235377712014726682041684993286298314160319836661676069974162579759478950267340429380298376267607291698064776721406926143054015/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^15 + 108379379275796064017347126622162120594389220489617835276703550487806886172386898889544912275295061019095711625620655840508035261427263352928285682019697299462236102321818165460284936933516053/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^14 + 1103971605856806049193475459336109907873277160997854605131988828393580985249292949823362198257285525123058497462190801084037478977276001793674280089829478873384448660802119450218852207419333/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^13 - 21441649337595251881692340003496538756144759592733342504220634834403159033133828976757603275490231788967152235092992712181673603659738473491150985211382143084485255697089488171430891721422553/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^12 - 62106561525663727504159990751787975412675443692527015884931474243084596205940913074686015540408992062243277861072861584974016735181688734341993979069274039543854071679315633226835225561139021/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^11 + 27041297598846353657396931751380746847307393745423888068362851064560670086885206383022343936493582642546224090893425971990439935164791348438846586895423954501306675495778163925510682425545121/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^10 + 49485231259737885222260260090121384993764170966049245746685025282762308601552130435164952466816437278677098804610933849915359359564375156560160400087352886574676903436921233677983041331568835/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^9 + 195394135916416628628605422710466449885169253313213153353157936452590679024237747894879966698487732752216977234778735046632479366116577800338066362776324273479978220182986737281536412892991/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^8 - 3626099861274536138475143786960855676617760598513281301678741104641971193489467871856045979882441775098923574201236272428765785089947081364134001475443829386722811558879860714034830860857353/1306916497743271751610892042844658942990603927121684909115789028460866132131050635104180601568423529736819509611127489334588673597111659265428422795863659225852664558615175829834272*y^7 - 3432781078077174741123501518798386545807820265825627593323251291664790204439751952445442159368859293675652317795435494653360793057295469733646769716676488367096786988304031019025934256052915/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^6 - 208959886367574812597829918900878551033552874392982102101019695439280716161278123562130553651849699608775884419724107932300737490929491348347447479453597892119142277487900901024738584941933/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^5 + 16939631328616665673010560727861399159422736656699777605667171599502791740159711816287206352399790862836261123426636695369579120333669765927336031586909588722824710746569251951087750793013/93351178410233696543635145917475638785043137651548922079699216318633295152217902507441471540601680695487107829366249238184905256936547090387744485418832801846618897043941130702448*y^4 + 207007522769850034778740029765866942465203487814229608768864990683637563878904479657358380272929190909914516634313745229891752568839186198303988292982549085420623899914430477723130865986395/2613832995486543503221784085689317885981207854243369818231578056921732264262101270208361203136847059473639019222254978669177347194223318530856845591727318451705329117230351659668544*y^3 + 12069124098598761920732843356839733745911453333115889447183426831906688706209162038878863048293711207446335597861417964088479709320274639131599483374363277822723859051061073648514367145173/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^2 + 8682151727566255830349531227329107261866120320702276113666431257264142644663438985115613111471398833198393857916424143728159777068887603249941692050525361309427104459079891826705151389781/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y + 49814519667409900711868247837583407493817706460524701679392798353339191137659117673448588993731299425838501533307681849202732704173704737559343529946475623594162148220749718195611116289/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584

-34667280403104539306581634495877042888951917415268808783845005130717283111383987549145845258669509236390238614311418059197708776012109791621872117990517112632542507420389343362312751/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^36 - 635516105578773160674070993441938086433727103574382430051578114257265352607381421094321161261105017691735530905219763700652431327168901427357646156555654799735604071205375875532182205/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^35 - 4937239643103188617697555668007882349843023748560786436851484553426114709338502964457472944065767223669499671343205179008336817778715844074582216848555856383194174462522318653741708501/167285311711138784206194181484116344702797302671575668366820995642990864912774481293335117000758211806312897230224318634827350220430292385974838117870548380909141063502742506218786816*y^34 - 76934316125411187856460051602900361040821505721933377748108709983271163980252107514164612023421641140048077221649221829691913225590577774255696809933524196837920995035380685518770003887/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^33 - 197663868927716034407533808119556317794223797590201652047516874085039958823530806031154677330707836577272444139426087764036443928312292885486652590726617171240084078573420765580982177279/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^32 + 89992938335393149068097321737213631270086829283062615379375206429339297825566772810785242344479426363318941042638233150624436866405695802124185759543422428352472877018847458221231127855/20910663963892348025774272685514543087849662833946958545852624455373858114096810161666889625094776475789112153778039829353418777553786548246854764733818547613642632937842813277348352*y^31 + 23216170122592520366775659791171111439450948214065757148747969537181822096669915957771943216586369639932595728094393049260234771775678460803906744041700724676305772122021656029948756669951/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^30 + 3454476559590075281276910424939485705891035816157047551314095401241521942417394276640448849010774855493459972054487215866353161232315101129138904266621927133253291135798096418743763622915/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^29 - 59672771769103188788040392316279961876953694562729394995437645894405634317649495645303483112012762699595007657987407257748553475617756707205244375299082486988682222342097621553092541093185/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^28 - 151956689624198354851446079160694420717313621725081159595987699675055309732216109871191138948123376067993338663242091829206416380321480491866793966212789431007698095132978155944307112613175/167285311711138784206194181484116344702797302671575668366820995642990864912774481293335117000758211806312897230224318634827350220430292385974838117870548380909141063502742506218786816*y^27 + 706614366438796247124684730172258504651722057286613366896513113852393877240098415137305726881671559642952803669850704794657537018061347068920696980513053521086236976182101780784003306488443/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^26 + 854422791396174112547098279862660075143198501260713907963598751627380654012378014231070029442867827876338367154460438662169404205113937982551216597364971104547021596710630929688885295835695/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^25 - 41679917958424109534948777951235925619184956234258327859164547947751479191378901464638179733531592289986667371433688871476590420088445424838493647816146767919231805769820374616587527715420197/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^24 - 12480027728461287283216186223658413975978760111694049597485605708298207815387356147426109092708386545207386670356911294585018012362789904975061523037885740297371485802901172778108287825181401/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^23 + 200387558353392787450137394032840894760548809220615440690186174539466121750616362497774325125037199590621610969195387128706424823674847215231718149503688066823073229151018404205148959301485287/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^22 - 7662627601748296237713981408773508198413140050913932669221651707971509747592830985942974169807710196365784263842642792107351145862172622695477771667623702412368061816647292594644426740121807/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^21 - 275607695408121472424857246558025178288306580734750880593501489766031246625458982933617995854464735180025066960266192581801721204632818868472693513958814676232819067131926359671262471864895389/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^20 + 262642413821182619915489249384273559513169174516156738625842128144051415118654171231523465400741576121102814721102062143616807453128903204477260903064607634079155795384355733937634086267623063/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^19 + 126493365645916518109615214685296142384104892114558235733846848762355477382572458720755639720215808715641026755710018013847866599744391751209003062762302114407237096695338923765946371935736969/83642655855569392103097090742058172351398651335787834183410497821495432456387240646667558500379105903156448615112159317413675110215146192987419058935274190454570531751371253109393408*y^18 - 451093170933639071517799174202438677656243421065642953707426338108700756700955005223995565710432051400385730820794289514967381326594097203002612685690387432991785585922166700518820922196909483/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^17 - 690586634898267957898770019137944795709741091484228586347753772902057830703957368187404736337046472557623108454213518060305388109345208066791567350459389984044655780195184906586181065631192829/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^16 + 324269635519034360923375724479242729791732489003750087796851327625167484313016517935272764916267069422456269163551083039574558055264627342682318923617146557331528331624954722550588589651213929/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^15 + 705830692733002936889275097558419079802872999746013092342984545363421423192451975759642953696024127357206122965896545515790977202681984151966269616098817345253282342026417991673193479668340371/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^14 + 7143461930005233446471395744082621323276253366684812804797393908239264654087890026430138219996469016705254300651206159996078797593203090014803504779897391081720913257491774330579427995768979/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^13 - 139659606969112803235588935640100519488279236710029596413218975818304221887976496626408045450229313796046019222885866687712848853593138325372408383090445226209118121652626808917278544625283167/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^12 - 404063701808690547763959001126738970554640522858652591423417850378035531703125121723797911507170702267473949709087214733096898047744223887234332606982977430228898036056485670701975125935064987/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^11 + 176209377300414903709801858538961801620503445837654878940719190730482488120139448558818156181150020752040881460441185373323747769848066405211993987640935534848189408916386054266092231538148719/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^10 + 322138662310582024664760719313583204286045190842041657639859426974678898764762182318887992178600552446135698667301041035722125357294882279949192849928694902555105727438534810956230643754763061/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^9 + 1253093758625590324583253759894881324479599327734433810384735305540866092971136938113104809398131284308381202639674312771448402537292595239148437273608242562137812652255234569371372635657161/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^8 - 23616217752919119123648332034458922905533313519297686748991624687119752981825231609142875156980009323002379573653733813393650269075302619821415559510884454404777370171992449418699449805781431/167285311711138784206194181484116344702797302671575668366820995642990864912774481293335117000758211806312897230224318634827350220430292385974838117870548380909141063502742506218786816*y^7 - 22336978323714747198588126184964875459481752291619085861685402388859272229629384595208899131205428746620120747836548112165093874537126512125243763340285745220504177684678500285525235983533557/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^6 - 1343946638101578194192125179187209436361219182131403237469712709793148243986573356446109159472113496208530811865282270144860102190370307834225483132549549786683651688757739160518301474712875/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y^5 + 110315966361108351348008286059188926544206959324182946901898435770964543292869286462974178760407338181905043875083873788680824883962341869175456329887148423819613737370658396857879126629473/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^4 + 1346886323073475654784490324639591368912379775371095564562027763407593936822764870076330017303788648277793020510187369516026391269507283879902691793844037812453912638438851569352444130321149/334570623422277568412388362968232689405594605343151336733641991285981729825548962586670234001516423612625794460448637269654700440860584771949676235741096761818282127005485012437573632*y^3 + 78466960272358999107541218558527665722351222810597549295807013184633298672558715642614294150420125449650190362753162033560305467812394431529970627012654421770000852011646758088463495472115/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^2 + 56391162564484181142520791764122785784846683181561709965417887959083814293501312521286680489645839122244640952707016235136435088396106095493663238173168989352387634570099799543514233978643/669141246844555136824776725936465378811189210686302673467283982571963459651097925173340468003032847225251588920897274539309400881721169543899352471482193523636564254010970024875147264*y + 323247780888075069912822388784183854632585536067697912220440221231067511987604829720714039538365737549799194772624832415136389734515101748591920007658431229451220456609006069843031399031/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752

34343027074055057552983082911587136353328397326389168018428356574885822322719622100800324652811880411097696544628022799927657811987842270618744794290723265245764207570955815891897447/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^36 + 629580218497332394527600421287976236470707997627211452200801983288015155281669741128083720941073318737468294880574267872222514939530639349697380860607629150456924777469521676815684325/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^35 + 4891211431932876145320655748791219055119344480195575164816979219418197162620417275062712470956409503687232977657584020885556987630300062313121261781152130289243702546863020070412600765/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^34 + 76219401802121292101245762575335006411964722894801408035930346809924127040987066134485983858815845251743283667753413708248696970359215030442116588358169356291273134955125952142093697511/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^33 + 195851145349474304962312455901949932235964891070141381611643848524968365090763743889764512966291286880093873623446588466115391435391661034377894397377701561183460571115445997773717128887/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^32 - 89145637171227513473067862499607846884605862737755763081349004174270260706394419584495429170820036370031428551118604375943479449561699696192129656453857681134135427975817435478837373223/2987237709127478289396324669359220441121380404849565506550374922196265444870972880238127089299253782255587450539719975621916968221969506892407823533402649659091804705406116182478336*y^31 - 23000426802174007562546549142189301360645174843695244971421542234326375551342419442733272605309098000061503856908398889712245291545749312986970947944569697568785821144801129307837645505207/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^30 - 3427616949045517900153195782351694148811663915059918047348702821069180336354698217757796029500229897674557385359526606376305685086249904263147719903010324967220908322898701355852881151451/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^29 + 413800737294521612050911120175338331285860352752972845495846430019568213981893777148842770558213680708481741526345391693971393296421455510450646934005676886288505189883900639176339940448703/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^28 + 150585458128003802066081788311807192953231034623852531851868822426345564087077686829247368711306849869574049888213433020943989735800918957458172331967405188968625741485055599095138390028207/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^27 - 4899774022952069157896867535771225064335718254485979838814461702343639286129486703579168086046040392603778305314504035106938744022170636601673346903825444925008092621037472106999776319638149/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^26 - 5927425207807857259177235711936645685643855093673483837937652374178880841493977672455912961989957923532809237064846134688394773683989767572033826813784374327018469029977730133837032220927697/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^25 + 41287543642687369954789695301178771126414797818915939977002864520536022629862347502547281052900102036120056929953223619969302697609451789650496205299408356545540866358516626773523511331266957/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^24 + 12383641382335458174634027070649168112135069609273791319599356484709419303916551394871160443395464343057447449464862300781025146761418831542496587404386572236251921530616384578583833624369889/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^23 - 198510058476871973634892948379276040661285432545469921904729129702844840684567956599498966135657252275285343051261654999372902120600709339844856309408807992583156850665254911753236908302047455/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^22 + 53039960976040838623056908593835951174378818864769983428808094861600849551336058904694851011515874058695095053656470906783933194171247706363762505972864500401071269885429647730414320354148401/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^21 + 273049221767550471257019301842226915779372833360522021466115825794522263605160931670863684714347737893582958335871748786225370526917255857739265502148769162731104144886786532548029125769141957/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^20 - 259925371768626498015625389420202828239802151524746167690715248870138060199186260430920221816176221301326544439371303096383595551377681665328924003594361537413343660969469397506336973945136655/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^19 - 125330365546692673138707606183914423184627002170265912031968287162798440288246154772942439819146155259144016100677994922997732988478552475001295172749949392548403497361549366211864510497369617/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^18 + 446405733073934817489483499031456837879965869483186923597000229711531921334410717493332140122940704062068641479129382305334617459185383493719348476451205373365608849874265350947875441143664323/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^17 + 684267142841047611072330231166666635422023915692199719625950707893183769851296352867820318658160781309450196078920636109805401903995854029411855717486455316866155000974298961040301788430563621/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^16 - 320602107432432681369913879012594788910715686557595625220720054404668254135990890443213204834054278909629781895265225392455755286128451072507056976132948167265471440350357739360204506450573041/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^15 - 699348802898471885135688365739872047745445433685631923883824479951813561642787115537121592330450881494709844197615970893575776137925881496267388111512200185357944747468959360929415617760055531/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^14 - 49865766973907303825290206233797896992606447678213456693313191073678670533418466956252155860930772308955866643558328907019541492916922922757836126812102359253765289688057176003970270024133741/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^13 + 968508862622291855847191406080233196430125407295804577678007212705468653523770173257819987137268766141347474542388017610119992788962912855392412192880204611893825730582200245440753273973579937/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^12 + 400760529902803043039483103129520576840781813248734757744578814513433785091518556166757310134792093458358472371299635942009302852105445676019143749572078603563602923947129976620298598194388019/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^11 - 174491831867642439547090503666277173492085882085842132064889068706294933829745461924024912516116871129654828999986505066530081924450556368723448608025869983369520909385533698289987780165171623/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^10 - 319317981827050622775148534516739743698199676174138369231297202395980137969688996021847924507191418723270576413121037037462375921168193907321340977120024564767202409873616665827846691259674909/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^9 - 8825918323624062570533155536439540635359856859740425218570338069583053385398823869658488444448205525698673289069700857020240562025815853462294458191955661517762324687589565948911503027600183/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^8 + 23398487807523799607573489805507714927227809661308424229649353045410908884626939902194348489214378892126013535112162058592701616249466498964559406477481063309721386203092614675511115085956655/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^7 + 22151064941415897997285835061948624047831465676154597962182361310729690331982336354065829552677479887212259051670153505517339986558887554718190633400135177126593730770600966749704801431585245/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^6 + 1348395677876587454692010171671017102394898471238434978660282986947608931679246819644841722140836835768793741888682720086669334283091808994341515797447788715679331121623913049095620645714499/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^5 - 765156792865072179742887398201687945218763717067351217823514433839014456830955961802960864387305322592484587953871274593171950855824858271097071377368816872635733569442886287788908850837407/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^4 - 1335781114368302308716782437781236248036796807855703485814072245726691658440832977572717056831476052999390410581788618504458078708469173972119126169285155666316192798802377850496426514298149/47795803346039652630341194709747527057942086477593048104805998755140247117935566083810033428788060516089399208635519609950671491551512110278525176534442394545468875286497858919653376*y^3 - 545159370967691571398822935454374431871084006791633878499589800224436899476535028042181620128371237508284174622730060490445557024837780128345062181304818352015094691178084095792373071294733/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y^2 - 56024219421349176501505190434497411609733497138855392519246467445731910431886424471174842828322307340045603573836363195603783736586059809865750680895940748674373125638304396967007706938731/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752*y - 2250009071311441488217672386316782820933003028639816777408788803164523294380109413516561993718840738841130071784752804641894100241757521281745988639965820239233847504212050790135894173321/95591606692079305260682389419495054115884172955186096209611997510280494235871132167620066857576121032178798417271039219901342983103024220557050353068884789090937750572995717839306752

29711697319028459471046106488274445146071826143848455558041084193979187029272567891377429515681698642479930535190803989688587480476130362511551720592794509657474827728011563006071379839/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^36 + 544679661340901761494749141489611256149681951276967896003774485557731046930940821876907872259630223327372258694095313761817818370460036767557658185117322272431476821134036347377786934069/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^35 + 4231634392856807453667818946255013641556605174151112431480596167866726407255751225947276263595826599709015705674903621385584259287988952198331645060677511106315917423526384364960112003525/4107638552407103115313033690660763057819468142943455669350924916452502253287892146132439630729555153962823718707773698978612201115721945071241532847399480946854924707727497633169116896*y^34 + 65941680853699216841963309785915951520905717627788483548632991854692134197909313405634432737651609708503323566989998814580265033965113436533805019668770320929595993973377085733909318126263/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^33 + 169446203695792666682711742659825106715350986272664510138337350723658384226656826020120144425632531748537046878194524049745217648187974357531655226378559660958598240153216383318898991075823/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^32 - 154245741897062410951908468203069637044613356614209087395279495898975647964049710364165221760794617886100631382769413539925761986391637782531227172474082536018306830372543931147383678683599/1026909638101775778828258422665190764454867035735863917337731229113125563321973036533109907682388788490705929676943424744653050278930486267810383211849870236713731176931874408292279224*y^31 - 19898955506434080623553030063647296355654165963713899441131210989813288458030783361482577142846231498781003293484016423972358724499188655318320959865533998961876086592210973149675092302501743/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^30 - 2966376185625492847452302145051806083468801283538967590464029448603027225447253268002112482038450596557724847114057774224543302824024519060824364709107134181780417328123531273602690289036371/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^29 + 51142460042562845991742036149351433863443526123627936933766479143443158908559682978985588793536361460432900162593477226647689827190067911728532344500299236363736162775693657251535408592544561/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^28 + 130287276279849132473751355569403866028912563410728616981430608082154695816283443783879664442183477235933066965902822302420261226771927473843298288590726583464384026272415163274463614288271115/4107638552407103115313033690660763057819468142943455669350924916452502253287892146132439630729555153962823718707773698978612201115721945071241532847399480946854924707727497633169116896*y^27 - 605566560813020581011317808279594758283820858039769825030936630967099314227818218841216199224601450252164086248406525055308992804289703020670448426337856784303717646452917910072716823608107051/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^26 - 1631725619604288676368529327978262368696195386131483942106549691491098390370656976489841800247800547265138386032538531922483999725410784243891485888005347306613809182377838315288998655237759/5227665990973087006443568171378635771962415708486739636463156113843464528524202540416722406273694118947278038444509957338354694388446637061713691183454636903410658234460703319337088*y^25 + 35719238161869758726235718552660915314778111113756992150875189544310025191685561296650106287628336260848350596662924967565191247097185436583030990648232332548852137824230694450876571170814008005/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^24 + 10717284266460846839348784138391957491849721915269533112186449247980173458107030562580916749588735427748560926327339857669905807146977915614573884107899466472983828924408749757094585324949396569/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^23 - 171739276385070619291479239099670553907747808735438225127349565760781278073641095859671743349525234327719305310033785433069116684443982047912086980676504754505102473806704039997283776370224751255/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^22 + 6552850138190604684638176910681741942625006855200205336121076711474016439356248537172573063830032395865208864139845965713733528016319738692102566884268909529904031548819810664541555872957759679/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^21 + 236230357499665157817508063718820284172268964784780745585050663374223364043962580376726119484485064621630312956541700535174666717853760896411343993603878489235292730212992165325063701762940609333/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^20 - 224826513796522421878445982605990436412210183373385523348321717484399441660658654671785112097263927267134622374572826588191400347873258387224817481690314518757767210806895499592624585025464161607/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^19 - 108432345600642121173865539191853274280410622550658727526421966448929555907695072913443609837561169973130987869697035097739894487258551841145720125117355436389483324624696831765692369839056259253/2053819276203551557656516845330381528909734071471727834675462458226251126643946073066219815364777576981411859353886849489306100557860972535620766423699740473427462353863748816584558448*y^18 + 386121931665174828865946518128850040205182216751248007235200976479287627920561537654269915940660510036594355456442176892699157648276723432308093908247837561595976788690642327189803241531705815323/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^17 + 592013794315121986858013845923917941417704542363698305152170286970424583358861612731492238451041880404692586672702906463160024366456283083594749517013045012497140195092764599567634128853700185381/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^16 - 277254329520448089087570473627110250849381152684644339059478145401681144347556422923131164154221861386753106756604363428738906308569760499448279857700913904564832026038324311503697007744436352057/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^15 - 605057589689449371227470344290343302342962940351931135299286884974650032063338019873485837306057500892113454449935120308933710202665022289216874067661270026370831135550028189271001630250237396627/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^14 - 6171301397478839881809899345272542555549452485647459377423833029412050213304857803602403813799003028109618029693242168096762219889926689676767238645472424834045652280064157597366818553294986723/1173611014973458032946581054474503730805562326555273048385978547557857786653683470323554180208444329703663919630792485422460628890206270020354723670685565984815692773636427895191176256*y^13 + 119700529073038594409471270161895510879534663891320632042088886978268200749668285006588377029787526894333012951225934885277255977380426188665931815326607100636453042712517663339560725160845519279/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^12 + 346798316696161557501930286850364782550732747314698246860342700451514558951474109725558127492628706865294611170039691222958602766873511871410290641029123427861728630810006528014678271193590856731/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^11 - 150947794477195194718952394209912396679426732658160741342648752955981127938920872439349130333883026487227860183632138792769774067790383272111540301361752543120107435510281509999546345666711496551/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^10 - 276288569574287940990689246219251744039907180985405639446357232286123516714763483700400339982761146863082727408970542045803381164308646602931265420418136787302974811396553163633362339692287566741/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^9 - 1094214115603234611860341973793362401706613708798067613786811292566036413353917177677302413409979980340212801407932669865999745847871385514062979751292980643285132253058570512597371005726974009/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^8 + 20243496563193488560877847764067200649249307596548285686143904248411230374650431602469971623469826552449005442047588730567152076138183593328615546432254087954375728007161480526741101867159732191/4107638552407103115313033690660763057819468142943455669350924916452502253287892146132439630729555153962823718707773698978612201115721945071241532847399480946854924707727497633169116896*y^7 + 19167734828046808345304526451604484914933253141952781204417082870350184193546632223367564246255730936848365062555522697719584476732814360250177389804371175863004097811256356476252474019126292837/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^6 + 1169484865762725339449347118044323184563549339151684082597170642294254230671699306702695279753638336895881227830787884490243066792661246531661380633501693688437250734795332515767493639729207995/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y^5 - 94570776578462623003129500609971791147104310763065123731823485291702542513259222986535406760567777733412370699151131785469920464196360351674959771681370553279286191200710627291642989068520347/293402753743364508236645263618625932701390581638818262096494636889464446663420867580888545052111082425915979907698121355615157222551567505088680917671391496203923193409106973797794064*y^4 - 1155890496989715986282158897077187325715446453460554519996120312971476531150663908749236692395881806580251423549838958882204610005699535970624882186275094408080890989026122240413327148910491933/8215277104814206230626067381321526115638936285886911338701849832905004506575784292264879261459110307925647437415547397957224402231443890142483065694798961893709849415454995266338233792*y^3 - 67401897880668254290153809179535721484732451008634126573217986348659534110089377817875466249283690722620841194187779299173357864741431254014586978745521306629270938792701028433294012048803155/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512*y^2 - 48496483013082782916615966579555083599883475299308298391206189633748018488886378345640555186105118387885419334759877502983709221228762239925092610948606158332334347237033991063252181707333651/16430554209628412461252134762643052231277872571773822677403699665810009013151568584529758522918220615851294874831094795914448804462887780284966131389597923787419698830909990532676467584*y - 278339001265970157394030105237959248589372827021723706417889322817941290972613112761918132844074052927273195474246053425528128367214852709985022507850234017743203630886817078654590094700295/2347222029946916065893162108949007461611124653110546096771957095115715573307366940647108360416888659407327839261584970844921257780412540040709447341371131969631385547272855790382352512

-385825859329383677175152684814246354911655956751024182439699955644934060228141114721886874465744407901330056203865278818437517673810747569709859035261028252944781302575727422243829/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^36 - 28291465603953816926640517050373662815151719489930217495427073423497220434198332422719454698425304845367433848841785617183620652754154607280303263397773183087848884754710845531576311/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^35 - 439581654501173325222905565371446721771804354327561212855329839748963840183928439011332592208181095822642787174026060799583344123625969587625668186218207138235493988971316427025810837/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^34 - 3424834167441630641262392219389985011564539444827058805629578615426495663291223061310950552148197391938842578705026776918887727664485471496834268273396753434604079820646000291294828997/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^33 - 8798799762926538448281743185149828737168620934309417514174723147790726293544914380650199483980082984142696087497266676654356991508967692147956011645817323785580777199681126461302718171/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^32 + 64101862962075043274720810264102148593670153465135538314013955707945811581414321033583735507415558379187284713419886002565447503499024461213266281164490967073079820240381183118176192019/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^31 + 516748528658272174503294494864563748927694266209293140745614535070474234276257669265027392609677338487516901287153813990855570733508210466783365338569836670384225474833629313160764548957/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^30 + 76838574941980344484376628514694375402742160933773140871143186400931065598668706530970986895742748274120941391802159052029334312887318103328428946251187318725997764600173568099798461065/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^29 - 4648839799805409260834558808116326392398415171971823991987221110524825826828162418348676135154702808103051208528489728988730696560902480665985122206176464571401644721379948709616168175719/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^28 - 13527405587050577785835394767001960530258134823547580559387992178000329412813232761887574369342311512148419617037868225899890235340132658933949550144245618973570135179256816114542473334639/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^27 + 110100541814842705772518607080359731335501740176643913764872645434075718150430926716682471783265730475677724154432722025552090796230687335960805810095222126834421803478475629110147856585707/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^26 + 33275743161108575545370896882914757403215289983956279507761244376754427555336342184114763259419085642646258780784020340910575332367974742360608449616735126236140212074259736129384013232289/186702356820467393087270291834951277570086275303097844159398432637266590304435805014882943081203361390974215658732498476369810513873094180775488970837665603693237794087882261404896*y^25 - 927760028178868580418044125674261575883812771260281627261898351646158557088160788240389643198364117792013432134214287841055651089380305115822258752507748524100871891432556540784311456079411/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^24 - 69392743434145239972461880027835817343457284692248140053694773747199138366763276800328093069491741702265972057151718364405370082330428645500858599152321624883580733963468881408490159291821/186702356820467393087270291834951277570086275303097844159398432637266590304435805014882943081203361390974215658732498476369810513873094180775488970837665603693237794087882261404896*y^23 + 4460324270451977076207674686079615325603208585669864320825322564593411275913906989928379427641903139582183502693136578413025569379727939904925151728744023670489404561411870769917300705204975/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^22 - 597456812085523660014255635832053354117939452318950079284434601738016959421112664659984275399850945848355336724891242714729877502278790374144364217623324945340986109811933124322118553799943/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^21 - 12268549791489391933223074261044377166918253275213557012756290061648022743894627987348514349574229540316054622058026854295853843128739725391370118743571202147663226257831676176365637652718849/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^20 + 5848475525162786264293100514434115708488533484294548189590508054241757782717335140767930866810653582108777984058822912849881065086557978990098809975797626290526185187414455761849807458150547/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^19 + 5630486320052575100384392305836092848158515838903608310383144923212433012477926574553385073049788617223889905384294358135673062193311467752587108523571508753886552291615258581747616442364607/186702356820467393087270291834951277570086275303097844159398432637266590304435805014882943081203361390974215658732498476369810513873094180775488970837665603693237794087882261404896*y^18 - 5022245120740913835861835166407279878358884556807775214592566920635572922176896206710844345627231511399787106641968847758558151114040964443095303074972488866651234802900325158336027913135967/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^17 - 30738523594376546412203857058587076430982911347895641875868318728660907622246969756171890481680932825589406486496930154246610182197976947873083964145339486769123634881185350677504098667183215/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^16 + 7222393375124593717176699255285865204582585111205502504839079170575838010740760175544071420589213544028532031770267629160813806035377245554450375091205716172622279413804131414760614819212017/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^15 + 7854251132388872011771934795480194856472081919256127532477928284891239273308934111372081628797244387631497554294865869330810069530079844220944210160528700376299110283770179027816960818839711/186702356820467393087270291834951277570086275303097844159398432637266590304435805014882943081203361390974215658732498476369810513873094180775488970837665603693237794087882261404896*y^14 + 1110680809835526773266158389831273688943907850052462335134719101747506577739906053928147557824382134630049487526935288290356688788948641932681854805768809295702150875024537570544536674048937/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^13 - 10878810721822941588803937521150422718051674877428791831820127441215766283352918507263744191386838790070954733363471288809662540725019567642779454894361769601344002889641313584627674373274095/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^12 - 8990231589823629163131082045541875530180091569401908476505381942239383519477766595109139222965881249405252381877112618075876749223778088764068430828799853777505315163885287842095481865911415/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^11 + 980467096766787361338836283169528875859366302626109765580037005141586729914701529495277926450225878993972624430966033821777567608868718927295864904619443269360506032646843973951367795779355/93351178410233696543635145917475638785043137651548922079699216318633295152217902507441471540601680695487107829366249238184905256936547090387744485418832801846618897043941130702448*y^10 + 896061050246968376290642367600920787749288870327873706378503289546797972467534380161308785450339684247531909638956413878173668650348357515297245500618125276370373022831642159688180765351927/93351178410233696543635145917475638785043137651548922079699216318633295152217902507441471540601680695487107829366249238184905256936547090387744485418832801846618897043941130702448*y^9 + 194917708755460799865832014838510647282544776369117820643476336181264747641016035916992668590872905737891417683258394367504062998046722982522296856793551687292198639190056052493928480272029/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^8 - 1051082919665681251880033410124346679978943455058619240758336183833272278774184521022380572884613826554088007245372589331343899122210452123491310112511141326219040799438572449732584519547677/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^7 - 497069912468724041323534049036239802771945972844257277849988415747092045558948649669120628262296226462430082875294181828044025699763134128846614866710364895067412271992304029367927378199229/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^6 - 14969760897224389145648038344803058421194920780782815808155207221587719298946228158793576349509100409586082757803244501576055820025985817652363168764465676051086161092206856324844379615969/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y^5 + 137461206191350329711420249983064369460955412085606852269234490518714176238493875920620880995246623076710724632903906534075647713925271135053583360128321958999274702925128150024468850028217/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^4 + 59950022440225893461559640504060435442091285140700656400958078222849198560171312108623282407524365561827969766380815627352976349862747198857136845578077517698594293777102506075219032268765/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^3 + 12227508592435242988139618822570675193760986065387430357716918713583058748001070342286966193394707008074604808306765749269312885796851874002487959219040230964134305069936701875729933325825/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^2 + 628016173099053413191955301367682951860132938740080931303540738641836661637488791185104934715178340674971029517858715442925847146307981164805205545016218567811959147532121852671759283695/373404713640934786174540583669902555140172550606195688318796865274533180608871610029765886162406722781948431317464996952739621027746188361550977941675331207386475588175764522809792*y + 50428152173331090358817437141166246093907720756536866495563948309454890162083455987341543802576841953831228535857529472299437562469477332101724618190067302617828664613441147695672710449/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584

-427245829050648393180254951198749147189952845803460220462101151318842320454955359095884563183960579112530305037635023764366200127628790420198060652846349060061074258830765513218047345825355775/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^36 - 7831878337485095854380160176198733299534056587739062786528726287226276550265523855476519442306074463999368321509119780506972419135737858253030995224907356944777604778727849016573919108997548753/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^35 - 60841308233961181510063504083533757753323548920792871507800193784550281590136119612990492570918785859788927691331165565662626761769537617905263485830335709505280416691576763633595428790524240899/90537971894578190820252392049443920438438189848728097295227781671442071533560336865067911234992561736103551440327535695197244222977823646968739169692269830567586482924544865101559673598618624*y^34 - 947964254286208387494347009874088595466240971601732864310428330239025642966537007316647710261286793628820110872178988208216311549495187258779708188208931490419481011540751185838580777085404066987/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^33 - 2434608215812711840825878444387079480890399873876574830979668158915810304626283993235355454653949587182082419458205895956865004229497572754143622204207205930848906499707643921119243042455341327555/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^32 + 4437205304377701971809006308681215819427398164439359685724948003494257003452336332772957970717463020147483426098945528578421326391132344761106043981751766666839704461660159985379177971716440804525/45268985947289095410126196024721960219219094924364048647613890835721035766780168432533955617496280868051775720163767847598622111488911823484369584846134915283793241462272432550779836799309312*y^31 + 286062146226701711193813387504145312474854315599428014481083588169927203463058361481177339316156646735889888769546140183456494228952339256141349210318869980565191356144094394951307970130007924305495/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^30 + 42356946284331252430482991955563336349269747510545033800012600331718475251725202095987390623556864429120167275355850732827198722227681482733016512896162516552386311465069011010685867571938803877947/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^29 - 5147924694568074820292881575963436583929857572400687462989522080776102790836801825007505909053447518098813474725019336746309678622395677562356784478512342117008025906718369037175224177082226057440375/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^28 - 1870710462865394214731515001882683812115488993666678594045166701246075080725393712090031011864807581470266727151003955060151917811232643564000174087904091464966582047209495231010747818783176596042241/90537971894578190820252392049443920438438189848728097295227781671442071533560336865067911234992561736103551440327535695197244222977823646968739169692269830567586482924544865101559673598618624*y^27 + 60968380830738454312807793487886506957867705530711635350935419274028886343859405796626572094927389692471014008332888905965816441240885580800063826784280033653507667471729389861607278313058649100048069/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^26 + 73611267410262751276671743684423495311312881361890527879779128458005286821320768301472869765863325506939029979967454618539627080014138732466230463982038619993805564881404163315409958088916230251621193/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^25 - 27039800647173624485885183490332980701346357252317463252351903563724173109836899148609185395400767642890237632833563935765647616159912376686739146768416038511048252628539974270206203640644765664160415/19060625662016461225316293063040825355460671547100652062153217193987804533381123550540612891577381418127063461121586462146788257469015504624997719935214701172123470089377866337170457599709184*y^24 - 152967748551783907726678329448466934872564288173853394117872298909253503493843635466623248055507705597286950507851400284648773382814928432284020249382293484050492505944511146049619923425549892028739673/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^23 + 2469593429114460244035549538855470411370401862644076027604726796571514734969474675690445548877581579122175940228915514738965729802459818288598648072524258586041770138261236662727498080370171663264220399/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^22 - 664951670874898497743012048850666528301020824633168941365175449073799620893708172471337135701418610993515606567426703746471416236227096175797146895636994601298375085730439371546973141925330340516080665/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^21 - 3395503128172704306520620886399304578063030435720884849655207667808502386891080230366311671726363855403128366823189039921901487097211213506942187902689908193255187358304743964014180690769891688888580073/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^20 + 3246914532897704525911144989714580784799749345056388902605000719093428581285768619931449769969226376798713841669991033686376312342569471383081819695386331568576387877288717408860465276155516395556106879/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^19 + 67734167831880994347231645820957083058840659630166536625791276931634485859775612576785981098702021961393417876427821258948048483319877766284457020358718587208560330890380547782259013531765731196749659/1968216780316917191744617218466172183444308474972349941200603949379175468120876888371041548586794820350077205224511645547766178760387470586276938471571083273208401802707497067425210295622144*y^18 - 5576544412440944139060962592791217456855490947175231314747257423202343945238073118791622654058926329188293661048694940458924293516463914722857441807020299546360949696768079567010229976128441546441945947/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^17 - 8503720628108435047784732535021695021013904222682725113791926174406982739168279612529768009715978714489487922861243824869312167208814289387755901008658747450209406362077345580004865428749976232645950193/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^16 + 4018877044045557159418355343016520099223419680768239014741966113671009876167009974688370167448914227404026937533033706599477547869507898594776876804818208314883655720429653218875837770722890712914143329/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^15 + 8691899233153687413712897456013301239266618986212559671408537508837461568308971126695612086411894051875367284814291937042834390167069592012476301548454995170807621566625316264432321079879073377365157955/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^14 + 604590147564023574856022015737480462380967795402206261950073947464750210340605570101751842226745834983583781464909306078090853447269071343775226940682700632933375243477059903744798712888937365857089085/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^13 - 12042491092241069185124449601750269908683188557221010887222797046873334793311092760661259951985787346000279604950793780800258243264720977017618218570863296175351687968284233875378013922876261660810834825/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^12 - 4962310496671471488424222957752155045126228843794610322648573565645385238128519841576899124959552184103133498384611985513253106903330492786451903842186430021413322841243442759715647164583106654474637155/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^11 + 2172657914325000932150577430678838106004648086623450388014849683159887761941985357413166182534206895690315507115308983924151080549947520858262133054240567629342751883385148087321005744587882284962809199/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^10 + 3962321464008371279264732215608480115419481334591955658989672111302447707508293190903530231053696132424813747848157658041466342183709725605078587141160472057671193751811303935840066569131862714870393621/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^9 + 104401087280922097279668718233664295372861703649121983585970630026297004457860418071535982186820924332766895850881465361394693524749503897390449657968702178512446318274672118146015255069396917149343447/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^8 - 290755829020417355336500230486063014024547832834800895835271062730502065940803696360708018636520348859112965689766529384507685306916000510437689140174747790686302827745224273591090982249325547449044403/90537971894578190820252392049443920438438189848728097295227781671442071533560336865067911234992561736103551440327535695197244222977823646968739169692269830567586482924544865101559673598618624*y^7 - 274541225761426023944937168074964913141926669151555137148852701892644793858615631129746491932295348657642727464979030359540337535866823756157361760964218436194746157065686232248070504234531419619046733/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^6 - 16218974167008506527387477171253560079022007162556708377751231565325683073333532297439539610888570914974940586448816651390362908540211499321488690405240021608912634145897414192667216411713792758914619/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^5 + 4751384998353689956170783681013444658292754339706994456823249959356001720222324827946515483419440836370768618385348024102904300147529842494470535367855582941755009460133999685011847836655309968585749/22634492973644547705063098012360980109609547462182024323806945417860517883390084216266977808748140434025887860081883923799311055744455911742184792423067457641896620731136216275389918399654656*y^4 + 16556472367335833064674791094436712369342916796520785074532865212290218795182935440564884912748107246612844511173618165245084989624282467334174034726041957117133185950831917279591535305081319087555545/181075943789156381640504784098887840876876379697456194590455563342884143067120673730135822469985123472207102880655071390394488445955647293937478339384539661135172965849089730203119347197237248*y^3 + 6748434595692912996530601091614596931604216048977254542644641383248992588188927416223173082538395556424369053767776014427097997261504916144928025867251124166742116309715030240771025083278439536465437/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y^2 + 692753632801759372471284871089144399247960534668226914374128886044502376238375375207877260470211653929610042961661916807190676914743267230113322132618224691671818455144887090601961026526824189185091/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496*y + 27799526384579131590388953518402674024459748897783733482802844098432394670396325920171253951505695201604592845677814741011456441210564077271900372042222035568099824591813612492975164537108895078969/362151887578312763281009568197775681753752759394912389180911126685768286134241347460271644939970246944414205761310142780788976891911294587874956678769079322270345931698179460406238694394474496

-6535520136265081643765213687102063485667475534401861427339279707321517443961464308964220884412721837638290461426567364548791594596900627515271285440006871440360565749276634905137095/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^36 - 119809787460197427371290433777100472758348367632753506574879120864337365205326025543474624517215405938523288504262082802515560889495184464528460366658481100583987848032473534771081733/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^35 - 930801695399977578101277222111831313284670901804272678451849504178171279805847785232618573340726307792441521370471155928795481389832765657136226399842690046313296713219039967539324893/5974475418254956578792649338718440882242760809699131013100749844392530889741945760476254178598507564511174901079439951243833936443939013784815647066805299318183609410812232364956672*y^34 - 14504588223915148993431151473689831914255467422771474779809589391994683354333182085696624644314971737339217810406337495941236441328588065316956054185624480864979381718494335148300482119/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^33 - 37270261096132458358918829616447083047290633628423456744063691369959822771578284129029093136544805258300041882021915940278103608068801798266176991973207880032264263412230519615044635159/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^32 + 16964600194292036185876172295074521535815518270605164072335593290841363693925578545762066538665702991224197910495958596834054555337646278053697659749610783943089651878498682849993188215/746809427281869572349081167339805110280345101212391376637593730549066361217743220059531772324813445563896862634929993905479242055492376723101955883350662414772951176351529045619584*y^31 + 4376993446717570953822441248754807194202709643810220685730177704190578877013827905751878413903796129700266133705245055093596272488190791052110726117474077294705948353665442824497455972375/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^30 + 652212080137015319365608854797380032668214470290829256326693091970783729553440528820829412963083289298177409246149747921658825978133811958980873170037308071501493716626908689319033704891/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^29 - 78746851203244633217182093163320257410848691225954439615138778771286727789566672475373736615971378619495820782970510669597885202260503048661132302641012887210830154635054210830657329673247/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^28 - 28656007307958745252119983339967037751026100024651089846515174239417758138360423395013079970717896738056272646894036187301499725210187227660420215890513033707721990184320834524724820769679/5974475418254956578792649338718440882242760809699131013100749844392530889741945760476254178598507564511174901079439951243833936443939013784815647066805299318183609410812232364956672*y^27 + 932436829150590160525878134903034901032503233738378820483780643541812567935965323522488733208952952121774984233007979197542161580285605304897942241631929193707976156011858187248068844375717/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^26 + 1127968938002901289743894579520667563559462734247772779242388319109815817926986859114685513714415780695505057573227743616957562676874963275386595923338896565900185220783500995854178847215217/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^25 - 7857107669846473039851532412965102255668740534951226881073798373201533864371014898255193112350743418149020028753260049599373824085398538312450648334684354731858305611975598602332885156340909/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^24 - 2356393618458926805899123232831096202768778958834702982056583531039389381683533426454925693683578746267838073278783387558076985732678407272194254061235438889806169095924306426696720415086209/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^23 + 37776803630257850661508442494659001437632020164696495265633014782835602474641552516897740716312992852552026515518960850373079761101051075296174800565970091763307529334689029129546225846933311/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^22 - 10094664285588251526548037814937073467697851264147939252015042685680108313493956398835336287331563154859634377100381254191142974740753492136297390707468586240899954128892875432839710616096721/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^21 - 51961510032692148334609702063018994841394032597874298860521279641515942173228990939996062241285361075234668635615252508333211537954466628870320061042482987922122575889503798625998545452274149/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^20 + 49467109647724941060869945324813731239875957445119659731311746020236919082492391738048434821224097319092736397307371357427179750316879688870154801217088966245819921733020899342560435301507695/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^19 + 23850381401851118680447265654331978472325395132128816893472383921302233622886307232223438126236729405051124176589454663829686326180890927051575854767888888908394754031122697099787079599134513/2987237709127478289396324669359220441121380404849565506550374922196265444870972880238127089299253782255587450539719975621916968221969506892407823533402649659091804705406116182478336*y^18 - 84956975671686486473938515687765247668343187934133335612643074171197150506752250764814597966547698324103797896169609044119531553354483055189734415581823870519098503988207583671539211240326051/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^17 - 130215945077533173841224362756860899676030942634180960238908709190126296056948206268482096574734446498323480748528339733776192656350320416012259074598621702663913979489741234303352672610182725/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^16 + 61018152181497126349690999963952266171885274076777409042445833819125558864596552929782746075749185880882355752808592017701184691607407377672739344495480063104739664397486365350577779000060561/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^15 + 133086430309719901945689908507039542720762670268576925745852324209324596299279430132661907992613099043790311447636961727301115187945865706419480313777401169448927203313058150263403643773577419/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^14 + 9486036316398097643221782799823837696793358412542961314530720846241642451880482396876691964681357042818127402067262581103687369152646350370803576636039308732067521636333528320104413820245389/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^13 - 184309470188069790705104139325483434550277041366496720004510318474854205185803587755230559409043658084348355308898481319674849056226502169032026535881524777558652119604813641911195818013739585/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^12 - 76260798860379961034263416208057471952554303516728656052456062834495607251064739606432078831824216177091437639157521267131340168265641207635854940254188057601905927571757601919665877154516243/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^11 + 33207080918106538234320511286589513302960069422659337244237353874192794976946233176251663888206035926519884149228683085354115599462873371804416648067677306747617706773576993169539695153722887/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^10 + 60765255463537587751315994870078421674494177320837403918562244214264168652846874163957859918442715377161362127029556895347473586934251976734646088369050728807931489448889701482449601404940861/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^9 + 1678175003208946204283609333834006053203127067790651358605423008488088435872717964795921052877336049870167870379136815119665777173136640379633657070393810879500999863965362597271929869094039/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^8 - 4452791240267199438510293598206389610390084968680178516737705243903730042835804467183273666384607586032941081984968673805172554113218219299526618463488312921374742347231536208790546958622607/5974475418254956578792649338718440882242760809699131013100749844392530889741945760476254178598507564511174901079439951243833936443939013784815647066805299318183609410812232364956672*y^7 - 4215206122393726506588642479402864425823409323659801787394456343157096635483870055769738981086677733418666720424372227251165829080508108730703908281211235571553618129872374419096058166587645/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^6 - 256436810152845495371421760496572008688883305751020169136251042000788251507956783946711454172609797831408231794472676384009712494091713096125466779092127067459430197635451437463894686380835/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^5 + 145611085934333430852317793918085049305687849244471853720905757027585135200541014315427484086741246020542196776222525204727507069227580130319828901256677384941174025447713836449542555564863/2987237709127478289396324669359220441121380404849565506550374922196265444870972880238127089299253782255587450539719975621916968221969506892407823533402649659091804705406116182478336*y^4 + 254190873006957905552827128818851991331106856781024206730047461816360200963495845158018049584953347745968176252651205032205264192618188557854933929260763122206658135726536861246536626848069/11948950836509913157585298677436881764485521619398262026201499688785061779483891520952508357197015129022349802158879902487667872887878027569631294133610598636367218821624464729913344*y^3 + 103736358543122245687959956370617141092090968983266038263196687788030280571957778835369740306674864993395000825116256357429155784464283604314448501284973383479366443213223030375265878043693/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y^2 + 10660047024428981903574316989086765031671335977310394472178130742701958142484081603432892566807727366064756357238100546265032048503566680600839240828494812148187566639489519622108368629067/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688*y + 428110562218940845095231104002364205169373149026815902486701461102414859897587656135738113598795167274387717208592629995005599857302057165054657401204269283839760578209648073197898925353/23897901673019826315170597354873763528971043238796524052402999377570123558967783041905016714394030258044699604317759804975335745775756055139262588267221197272734437643248929459826688

6013794248265692657325050009673772655960095195437170674419823059777746274084849653587392320774031843529743525816994243256534177103653851275948967374098380177207627189021941769629512402578871969/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^36 + 110233780857209683481293683079057011183212386256051376678896165066890321213335074709536765119346404312259742478176566337115117736349498018282026788346680984322776225437620051542689339780352580979/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^35 + 856284544320044129507215711873197950715357320860020409390657617647428535539399608146045783506743195996548057472173640347275996446679377392283918197843089052586380276344565325107977404542364515755/4436360622834331350192367210422752101483471302587676767466161301900661505144456506388327650514635525069074020576049249064664966925913358701468219314921221697811737663302698389976424006332312576*y^34 + 13340201082254679304795978669016195308872088192400056757310553988134922168558041434569942184146840614172024835536493831994378004837274716211619692924300618536643375609004091811363375791152313115745/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^33 + 34245567174772550471604306539783188280564412540756671493558345549914806247235317189380082520952978507317804033844889983196888783998888638845770236872139463958499578569375387409289389820552449677361/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^32 - 15617509908295089413192227655888057018985174693768301356874267120863214609910466321768409812499531067365310048352268546595645458608980636737532785987276115219442989321067425260693439530457278425453/554545077854291418774045901302844012685433912823459595933270162737582688143057063298540956314329440633634252572006156133083120865739169837683527414365152712226467207912837298747053000791539072*y^31 - 4025555305749921110529898653946704058024551806245527031677879307079259905412896063083206322278941435818348476995356376548164500980802983511919761498397056523587786968158881296612880801740569857712401/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^30 - 592696701818369942491332627054329165652163554709542872749957015161574263718511252150711178389253805082778410944395687039400439799801338751203638830134404799038474624533787182838317615584538620463565/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^29 + 10351385812201994330152095819407885061337898698676554480388238326048725830318985065886813611125241987249593547562977904659871126378669377109881823926564836335063513967341903741276643057120588819503599/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^28 + 26298093335178803796907565871261472491873010130760231723719400332933089865952296949911583033938533912680456078664590494767935961260940692355923181346814853229719015247513065502589036206107925329117433/4436360622834331350192367210422752101483471302587676767466161301900661505144456506388327650514635525069074020576049249064664966925913358701468219314921221697811737663302698389976424006332312576*y^27 - 122615323513700355160573134067215645806806524459410478185965020129970936599939437648418054455412462138283289126351834743369958734426174480594580163977280186220289627887889092993088260632766852005408469/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^26 - 147782218533791735996379350252207806518446137907058571941104646978372629711655051896412550031698411045966916509740550147642129931146003522197975864625525460030672044856394580110591001042799864612346913/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^25 + 380665691522169622494831796634931526946028117324377185174868568244055605416259939345508358472002518796881667122744873541203104885173273450516575916071029948160706475827371328323860573240032616605714921/933970657438806600040498360089000442417572905807931951045507642505402422135675053976490031687291689488226109594957736645192624615981759726624888276825520357434050034379515450521352422385750016*y^24 + 2139144681064512700536125497015413881468557610113078909727017762597409020766780490536622687679992229499414077978498465980561111976503352302237301260796434179463624343590648560245181061986486150730183703/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^23 - 34758860694128510620640554951385836606604763764701553349932400426263564402770803803256895826274948584344360496141313352668613519521566324882513119029110715181527770489382093923830879460260782130136827433/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^22 + 1346193097062914407516703056993965831569568741171470115775320901834123110290840829162493193292866184525564834530780007684107449387744759195677495898231147548981446811270542133666556682401304113055330689/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^21 + 47770710874328390658646402702574738881682124176328577795387417292819940767350661350356669519059037814814157878009447922380465536204305486630601686286133393490724157509396242683467589305328963882439331923/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^20 - 45859789380302282627033969584559292246630541313147996446242187410485827325889269859941579835433377107330521262063641310133706731818624484486314994007249155433075423524327386465250803352190868825940858745/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^19 - 952544893403385384088362836083020965137819592065514602700316034301833037367061606899253698774529313775658162823660282968180397020911142395807958349484605146378653594243018468475650150442035346871976801/96442622235528942395486243704842436988771115273645147118829593519579597937922967530181035880752946197153783056001070631840542759258986058727569985106983080387211688332667356303835304485485056*y^18 + 78749458595993116482893360949658693627182884890942154704342698582924996508359270097962841709549662338833229539092912394129331614501956490196282512497170734875738603099729135960431209687911491774542327525/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^17 + 119562119201228445911344501327806673788479753417258312862946921161596929634287990650352900361094519022306316534497651194861944550898401792170742307913979022245139664178774644497199252753069348578939375603/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^16 - 56894260853591649996084461499546575192080258302888562957694851708497050315895006443248518387713080896504759485690880024486680050943333827885457669141601455680273217981165621794489402452014110157845431175/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^15 - 122213792863582558768256086444993085993353316621291385311474167621072214643824920266012341796896012710707773651647626702557537863554607193449244824300043833765263157393959276185749353580381245087895215933/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^14 - 1191483014937334905596316240624781290356935913202410423687307220012912087821060102754011112402885457738524023216326386296793258454938186806831108961064100427397478919092191356057766766572481124093981757/1267531606524094671483533488692214886138134657882193362133188943400189001469844716110950757289895864305449720164585499732761419121689531057562348375691777627946210760943628111421835430380660736*y^13 + 24196494083085284745760582123467652545195648953214450713881223397077747594205289419594969102402679434120517109452942989656820406769467114749259494540082660791060152690487318342843853006964204431628649329/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^12 + 69587877177273567026572176619062261305350050143034718934079203367545715965885784889170322919775387882804023211865833097734490745187157677322220845968851804887336972109400439057011350479789220770907698165/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^11 - 30584895599463122442759167814277495929800541833961693432231700779827512153628476398723516111856856702669725933174927620123909258873884104532823065543023573393407457030676973654302589636357603984992626753/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^10 - 55651480942512179572050978162626478317544344901059402262919395002629956924412514694033656123583664834543313547560947051677244848902894957223190655082245260367327091289030738037358614231966271213552831611/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^9 - 203158491631751076024263281977212518318418717389398399816077940827340235253477596060458440960902205989454685199229932418756723964775974098006746763300679193118353965957698046498036712405791675504303399/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^8 + 4087311640399056645810668263021537051606178641107843260921090639836074915071319174212817348882496610874552293977072762441368390791307444683313151784204001965006072559317101599916486438956575378909429273/4436360622834331350192367210422752101483471302587676767466161301900661505144456506388327650514635525069074020576049249064664966925913358701468219314921221697811737663302698389976424006332312576*y^7 + 3853746667878861980838100551035119082118932048078946955267206418789628927453095693744121574017430789922941170158061524605504350575017582243009189952609343582721107761041320761113557598107480247239686459/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^6 + 224075436862086643842696423773199344085811411469021766447544600970596302824403429421985458400038017738620486755524744981680925284039531025600040271703320228418478904997355394594540654268832598224595941/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^5 - 19076707357990777772415406094804659805713440861729894071302042989221674253555924076733927470809034590303571731028370959223699078592185661899776469440705838734492589072701354153040769559309854932978527/316882901631023667870883372173053721534533664470548340533297235850047250367461179027737689322473966076362430041146374933190354780422382764390587093922944406986552690235907027855458857595165184*y^4 - 232444354752794290415972622572873424044208526129739503714148486154481527522248988157099101827354453378545801101861296452996641764618096984069538154713241981464265546425595996289957478029692831822824147/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^3 - 13528512496899173583551276054629778242588700856086941159853358630819586750614883824282870891533768040539156672035136515331215132130656608927083137185791408314126087477843599153587708510172890322958493/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^2 - 9718405417812897135065773688984282534873941407547376201754349098788098713665640725818848312662732646778664357229393771473551199317880050615737834903025333021666547301770261518095885257846494954421181/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y - 55706496664983780133728750636261804925664493524363006911266468288360548301862410714395858670721811138610256131897428136042462076809535345742260003444449193672038682502573081913870960584072501474329/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472


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

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

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

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

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

# 1 Loop Invariant
372329236596735779774132892054172817650287423667566466174577278540375162178796478907485418756436625232440390244287228895866082770789551830098041538299134110533548679527121725779152621540767414031/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^36 + 6823910154547379106143749058110759302731991560528359510514873782183846339246414482300765621837148921857834321253604912862621768094035226292011109605567760367301576313960251783566419148558147875653/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^35 + 52997581472439334481714940819207103917915570672131101035041973052721879266939482457875321915979885315064288090906389478296356145543560283318969115078819517194798388824949780421337710019594240321457/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^34 + 825397008556867785772715948939979137806070237464272246129917200419400002805708567982211404599679566317379023390261564733059345451906203002087659873577440322132614232363505757596219888443164170121159/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^33 + 2116174059122114748260895869384656965828521926879483465816599203776282909233325302613171890671625570610097494159512404370614136209742908684711821315971945559912669463592976556076914423076534104827975/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^32 - 1935060385704412213900369338172433128855131544237028057759736470785383077332187499869533694049473508863175531450137268951358324510314086254525796641927492028040352657846963201432931579771221132960067/2218180311417165675096183605211376050741735651293838383733080650950330752572228253194163825257317762534537010288024624532332483462956679350734109657460610848905868831651349194988212003166156288*y^31 - 249071015428021746012717987924684098038403531879993884475067115677734694904222874583942874785687994536017544121021489634840044767007976040618388529297693528166238854362382124092143605300302998642515823/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^30 - 36083578639273563582437418379834582409331734477822477859766871320103841476452595183789889822648129853988903384983692310482568384204916690893351357382867894564179030227810393152288166786547426098798387/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^29 + 640892016065917322533381882596840208647183811254141877619671709058339743481235260772275909487230667907407519030488352074172237018512947198770615750017917442909002702590676392842031872917438615862502817/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^28 + 1622497651203680656285985746964004541611113135483825703049768958962924227378139807462764550950737462288226588742634840006683521238938548438975400385062362370569919369432849142043976350023990556304424347/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^27 - 7595364411276436271549719245098655662732474856066652225955905726243014346970513751690235130619573098498942779706290397882948049287916144125332204307524231562432219465331456912991350965090499889560972779/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^26 - 9110189715808900919132629787336439986687794978393023777030490573371571068121436699457388046771428687693196141319041310963563632826096803674201770767632673404184904891934993160674608007138789514440343151/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^25 + 23581603500553408448812281710350772549384856810713314408122339304661565683648089628662947654499370001669328106984851881171883122461985877635748167604000295567739758249600407298851882449797887474846137303/1867941314877613200080996720178000884835145811615863902091015285010804844271350107952980063374583378976452219189915473290385249231963519453249776553651040714868100068759030901042704844771500032*y^24 + 130110077059958672738793795340571669648747701376518474659830649493760558581636747001210513228030584867406979408091505651216238885595203495312306342996562933256770721183703520496473363874709969036831575513/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^23 - 2152127241697141121034141753975315285692192564585300876736632872294368205630261028970259619485185633441593169897147107665330165094654112582789045095925013588585860507865973885691309593370305278226935438263/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^22 + 84908327837081985696293750684551235832599166160881392395553566496357189957527920981034375970464926438731317965543534729095614654751151650676519934196415347674299511373977797358108973753663635094502093999/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^21 + 2954828523457150197428392495061547388233410110268606022035060115135145018395668076080998909692015054742491826445159157925584542772015894201771115112273547772078113320429664418972947875297788777289822365205/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^20 - 2867978213577320539681517447193335554568144750415629994779183577335371869656413968781190011258743486219291118758853118531313045730358069218521230948433272218272843465810757553698794985725434702510473253927/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^19 - 58859035256472460489930540020996262326357796921284285454656783001074455835984461409738801544753064315385048698541881233961976913693506558123670064605334774114216188989717238340132998050552726007969760967/192885244471057884790972487409684873977542230547290294237659187039159195875845935060362071761505892394307566112002141263681085518517972117455139970213966160774423376665334712607670608970970112*y^18 + 4925603054632390488945843013991747784108541966856791605314503038920738334401536643614107059899547161745306542780285373660689678058911374003923195663981661818800932492443693537201192878941409100890732270027/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^17 + 7384020705669009783620480768014399864082090232230612130484715538084608549029475809261291492089667477090971978937683842710224239115226419296012697776477164689483706480288409401153152846361460097249614714245/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^16 - 3588896180624792347738773764438175105236548368521131414050574385085411116596049826748933971334570065701849241896452318275429640337955658299860888674746275777644528000399617208388961743658293226563066256793/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^15 - 7549597796327853494922393361666217378713932955488839009054806822841810630952956180466449637100864159682813008277356874912899404475084560082713635823453150668650677463514824458655264153243691102420348809459/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^14 - 68852933270505987511208346994673180631845149640766775257779340872408012077762557904484722034749917051196016518795129951739441983181037943621759888020255286119781750972503447298281870985906626953912957155/2535063213048189342967066977384429772276269315764386724266377886800378002939689432221901514579791728610899440329170999465522838243379062115124696751383555255892421521887256222843670860761321472*y^13 + 1496427043835884963342277903539201031824090649158942464640540141151794220575698314799281215122076006825643425631373236904079979197390402167222445279145076040140787703208630592262069098812933116432965090495/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^12 + 4257714284586822282796979982992067078147212858024792409274849262631065084366279584201559249869170759212149177199433952166326513390107861196069109986579909992229930580451217124155004446469155526078031999019/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^11 - 1898357047804282661278265812209040541465370534071573265705633687224442121532699962014359704109017246522294610049106543922596982670201383531946890546944598912471316523696696913402333348443544208523096804175/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^10 - 3423830621002375493219807708262632841628941154551592675169971330914944022312209567438360077836772088132499479869546320677241215311766615554836981820095707425153224763308437225582389900456454289112667947893/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^9 - 10832529295154170998928000349887334022761172655438456912587477383988771827658896947256782006267217121208636293709943079632427809888242272540611117213012993698987426414379686393638866173622399881152035417/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^8 + 252404259613157488308277137769806821243515009527290949656070766175164362152307183799694827012895192326885427058253756167609593725638250740243639528374060710108644035556595795669352519872423771190669202575/8872721245668662700384734420845504202966942605175353534932322603801323010288913012776655301029271050138148041152098498129329933851826717402936438629842443395623475326605396779952848012664625152*y^7 + 236330540420676983993851278310368099671872654693046175666556871174165699643239839957977482366219871204933696016782777561379899731531505262290115081149953387462611295955065364422845615453721536312802422501/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^6 + 12574589423282584192719977577088332299348787145038294550254005922551372170810509464796355185307316706651518975572018949836113751847483434211310040385862761034758880489568954633044885859331609819621597323/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y^5 - 1176420381163289372663268059138881931804068075849885891049756171596226657120915239885783515310836903220792643808086204126520614518912031845398006847250671254100113937903364707919519518431091320293389779/633765803262047335741766744346107443069067328941096681066594471700094500734922358055475378644947932152724860082292749866380709560844765528781174187845888813973105380471814055710917715190330368*y^4 - 14254481270110334409581359072338196291200377369331038798018318879969185665142331207266318663328917401541066668540007514441941710978107631676174446447454097166836807358283571304142915495572785655546310453/17745442491337325400769468841691008405933885210350707069864645207602646020577826025553310602058542100276296082304196996258659867703653434805872877259684886791246950653210793559905696025329250304*y^3 - 826519953117643559494196509991361033611946776097829983297668300549322415911831688498160116763505709773850846666185702822797022746219123569055557295709495625521536630627021173480667950361073765093633539/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944*y^2 - 591698511915878865102042470475619072177558574592220469157882100814654523963897031090307377729443411857608480796251741821337506769827481401307897742253649696865652189811543445458166511498659894059475827/35490884982674650801538937683382016811867770420701414139729290415205292041155652051106621204117084200552592164608393992517319735407306869611745754519369773582493901306421587119811392050658500608*y - 3381757840065324293573317288945253625769529727608456052788047528526739277884384161890208727563725985913047361585338121093661573398432872364726790888029291027315798704540323780771429733627839105523015/5070126426096378685934133954768859544552538631528773448532755773600756005879378864443803029159583457221798880658341998931045676486758124230249393502767110511784843043774512445687341721522642944

# 2 Loop Invariant
7268834342858198549285944494813642627261770381094643878374193488224019528611793062006316110079571193940445310662830735167533756503136589382420967615026257115600712374872428409660777828721435587242334464132878589671375554513004320798706308899362109336651523620047259217797379395292898600251129669963572303219669599845224230264529139/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^36 + 133249971173117276506837089216850836163436341535814656163238661498475677360316586949122135605538890316359988740748923646872868295459241499416677766776464066490986590009590648017307894406817703438509881820864784707347439282219261685149793791923438438674696404576291463500627123536704290703605460819340902059175386307480410188581367997/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^35 + 345062439179773888827478791498616168067660915222557675613342268294593755263948366491479377945050764657209453558378984857211092206344613459686534978295274744744070404886095441190284975109153350467005682286857666811949427971505517318183097811790715573989277191762112308394747509735078699605795144496054588229232825997404624191012368457/8344751625888463138418870194244627378744618717074691196298083643945247359818941396096611686588505838077589952870283268153745166998493338241638133438824203440300223515513149312941420102682738295356585029528879692361859959961210969512255729277731565487280572742322291076276893703054744208065208072050254064523960077425926229019288576*y^34 + 5376800378135603442721562016342195405556541158567176061174531867463767461394466975549319267471439010144298316798310542823141471320368232058980081399131964580927885351262266192768693964136065631041847461289900236501618892856125737113688097418155689376347730299264089535444054897141590650449584029412216542891959195458749222604441025861/16689503251776926276837740388489254757489237434149382392596167287890494719637882792193223373177011676155179905740566536307490333996986676483276266877648406880600447031026298625882840205365476590713170059057759384723719919922421939024511458555463130974561145484644582152553787406109488416130416144100508129047920154851852458038577152*y^33 + 13813169667694244595492945105955046766064155715530367608423597519994885593046461418294647444883218646756181622686952732847515099158431130265849921630264448999633373685795735968658368709088997332956759252050423367847851368719194044852435534924225156356126796679669522220340280195355688775798063080358533356381273319796122592879394083189/16689503251776926276837740388489254757489237434149382392596167287890494719637882792193223373177011676155179905740566536307490333996986676483276266877648406880600447031026298625882840205365476590713170059057759384723719919922421939024511458555463130974561145484644582152553787406109488416130416144100508129047920154851852458038577152*y^32 - 75479659617485049567831870711091901946963394633553354337511728435479527772041843537941867658827301612176215652052989023411415098594758622501953542385929438243661159289042429260366557774455440605609638508420799356222250296428686437708270113437955573091867855890852846416595752690604192995414809952948094436451271828121816464057178581873/12517127438832694707628305291366941068116928075612036794447125465917871039728412094144917529882758757116384929305424902230617750497740007362457200158236305160450335273269723969412130154024107443034877544293319538542789939941816454268383593916597348230920859113483436614415340554582116312097812108075381096785940116138889343528932864*y^31 - 4867587781213042466878093946128549283727560604220742365903103718705190143031234347458610593222457515145315840800561671335818941274106559133467082678129910774797164186469446725455672981915633168092832795198225526231016422043082020148598075981454189629056880788366012636427422078846620707262725835838953351360311742523184032254282096978235/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^30 - 241162915992451220276048651435657568842237364509314841963330156471499577547052429693579298371502296411261377324955113230564542498519010973314743976892154209580709522290141777629661933457298788806077903137735899671798757683513936197259803201235752384272412044527167054745248510251088347947683019089748842406414650489438099408648760337093/16689503251776926276837740388489254757489237434149382392596167287890494719637882792193223373177011676155179905740566536307490333996986676483276266877648406880600447031026298625882840205365476590713170059057759384723719919922421939024511458555463130974561145484644582152553787406109488416130416144100508129047920154851852458038577152*y^29 + 12511744119760375122234328575822475916260858074434085442934644586991351226634659457488117273659008220076192173549604819204789476233172736478215127670645364509643594757497105401890730022103033792262603675167436174704522725669741245047917805573965657296408079544277215883860267589694236869256522661897294316249452223629515917113694772415133/14305288501523079665860920332990789792133632086413756336511000532477566902546756679022762891294581436704439919206199888263563143425988579842808228752270063040514668883736827393613863033170408506325574336335222329763188502790647376306724107333254112263909553272552498987903246348093847213826070980657578396326788704158730678318780416*y^28 + 10617751642479135268941966398600061784211768270574174531900601269841343195806113307524025723735103223557610757463484136861832583681428634386665812720933451170224617233214509614711263775038355629575327924241164904945130870894458366261118968974478143988761730335383197634784193533365013152463207357664805900672903233710066429839227030398943/8344751625888463138418870194244627378744618717074691196298083643945247359818941396096611686588505838077589952870283268153745166998493338241638133438824203440300223515513149312941420102682738295356585029528879692361859959961210969512255729277731565487280572742322291076276893703054744208065208072050254064523960077425926229019288576*y^27 - 148162273689770931301138949667290382223673609941424888157102736251070924685656768625127698591808143002845205933588952584050535400721961887452928703212280194039701453899425222568641024430206943151043418380225010079703728658944940599337503576849086598447435939112069537951791038263434680263351983846112561765595868030166634497820958457849287/14305288501523079665860920332990789792133632086413756336511000532477566902546756679022762891294581436704439919206199888263563143425988579842808228752270063040514668883736827393613863033170408506325574336335222329763188502790647376306724107333254112263909553272552498987903246348093847213826070980657578396326788704158730678318780416*y^26 - 179091694342000798076571108177298023764513716547212351725468692267572826662715902392104540310672565117576096253665893026257230311959097220140365398347506987847834167600669714878926273356859811183049701075274967707767068286739265526320980966159907856617853291934896906976633322332637891105657509391134149853035008667249147472219779644416195/14305288501523079665860920332990789792133632086413756336511000532477566902546756679022762891294581436704439919206199888263563143425988579842808228752270063040514668883736827393613863033170408506325574336335222329763188502790647376306724107333254112263909553272552498987903246348093847213826070980657578396326788704158730678318780416*y^25 + 459967499201514428436209355568526874208649208019135149613198930158917309447774707000874896405647578426201329355163479532725691646599844898149580415361752092394863075159872961259117998413172089424633641838316185116948740505439747951344413944082013316864111035276929819790472439975866253775385952350136787914692124965622456594359209558805779/5270369447929555666369812754259764660259759189731383913451421248807524648306699829113649486266424739838477864970705221991839052841153687310508294803467917962294878009797778513436686380641729449698895808123502963596964185238659559691950986912251515044598256468835131206069617075613522657725394571821213093383553733111111302538498048*y^24 + 2613269463102595899504125226716323908462598184091288873507102734877887263506812178503648398434045766751058869369413317745740871980016216763362795748329962954357400219467894446868913890041390764343480553700209346339350536989114996515784007777084396837127318418840566997882531125015888916585204231688322300934255288471244389462951203047914805/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^23 - 42014620778400136211955493221071142186851722858709470412607568791165943986023945334733446962475766896781330789393896894374157407176358626008970008938030116764198759170306967480492838995315993408467906331580354711960007418082832371449693347398828720204012056167941630521789236079468249184412750444919504379273439918279857289625054819331157267/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^22 + 536279336700928766058480872668998281493886909241499439786999109303550546795925475898732516289122237518133376832611350485891336340736690168699062002910616540367268706664740187011931659315889432347407105937093267668126609294429303326968787135927257677341723653885196133040160531070883526915564081270225529058550697424741327769183760998628817/4768429500507693221953640110996929930711210695471252112170333510825855634182252226340920963764860478901479973068733296087854381141996193280936076250756687680171556294578942464537954344390136168775191445445074109921062834263549125435574702444418037421303184424184166329301082116031282404608690326885859465442262901386243559439593472*y^21 + 57780091176079265872343165221593448064534715262929330819170082959109142508669534508397312436961199736194108516708408467960483167318483974136241102419726286899583590199893030749625568044969976992236876596313813259790013219367977561358693706836926067613112249011682529010460576400880008756489858525533086493683979706678949470940342723315529061/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^20 - 18368082993071228430356544084290666902329407393901433232669362397856072313898351196447082388967662381884525667743054535411246076605378240557237085358045682038974408665945855446170450026407368126913919790835579622873280397380795479810576152229472669158994439134101075070286272897810337406833088775677417195738808900798730809982448268614582177/33379006503553852553675480776978509514978474868298764785192334575780989439275765584386446746354023352310359811481133072614980667993973352966552533755296813761200894062052597251765680410730953181426340118115518769447439839844843878049022917110926261949122290969289164305107574812218976832260832288201016258095840309703704916077154304*y^19 - 384294481206523855994078093739552630187101867193110595086329643739277310333568647317023584225557807928114472234555055708564195539926104318405117671340971197267053086674835700615051807023583243002102121975122172521242559386669620115623521340168262254341187259963764302938300973054488733070887612949042112541106696954954104698980048431109873/181407644041053546487366743353144073450969972110319373832567035737940159996063943393404601882358822566904129410223549307690112326054203005253002900844004422615222250337242376368291741362668223812099674554975645486127390433939368902440341940820251423636534190050484588614715080501190091479678436348918566620086088639694048456941056*y^18 + 94633527131313674084455813629706490239596864628501666533094782048196637302215818718650620577322266420886475314928377763102227605516235705031556032149470075566608523696206091048916016755303299669552714140027552530934491293801554828312228347749121586389218497485580407308579375746553454844615116734622830134716535476574747107647681285454392831/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^17 + 144757533559977808600688541010745656019110355058002636787525334703342270365955368401648074043783944039544136489583164101316588450957866112247210771305057563370186976318361027243686532268888027048631907762476256452707568815708855307944458544982131338212010514207483243955428764869885078787983181856724905186041098829929829295859811809614415405/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^16 - 22683557918361529491780757423633402491813529253040992606848120304694109215510493470866444529976684778734399554879619767049450336191766256267668245265129457031624641929217923750394260894414340856355391985868654663218247241636360035458770792272370895442054262328985431727499951978667107542877164732386003730464285270252592448015621539672835071/33379006503553852553675480776978509514978474868298764785192334575780989439275765584386446746354023352310359811481133072614980667993973352966552533755296813761200894062052597251765680410730953181426340118115518769447439839844843878049022917110926261949122290969289164305107574812218976832260832288201016258095840309703704916077154304*y^15 - 147952252554143438553148635123099841119704401972218564734890681227528080682693559883985000114056504429518804519737974310887312257619922242685321199528011097207750427032664699709180646668463284172425855813132158618959167803774290012859145024257794809823384025075075038859412717437794421504501150203754804208321709997023432321451982878641607767/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^14 - 1493348585532926528215534808782591666251464683031375769386111823594714944223918188678560763685025207396036090831841391587842360284021713955553528605778791960902600445489164248007329817360306841477677398650335511622851582982436075044694603785834234287427257115305247993091599663130472349026162570139356829210972480723061626162031502049069039/7152644250761539832930460166495394896066816043206878168255500266238783451273378339511381445647290718352219959603099944131781571712994289921404114376135031520257334441868413696806931516585204253162787168167611164881594251395323688153362053666627056131954776636276249493951623174046923606913035490328789198163394352079365339159390208*y^13 + 9758419282966085120654428017902179174024043499944486597831371033707440176325384062819416538179183913350165061560841526492532724627155654805367351623469685590305286152721326446927705992025187969660784125999353915116374625980600859788458291354809244097558284536220220256738701051864422018094507427841056992162330927148738602726316936945489889/4768429500507693221953640110996929930711210695471252112170333510825855634182252226340920963764860478901479973068733296087854381141996193280936076250756687680171556294578942464537954344390136168775191445445074109921062834263549125435574702444418037421303184424184166329301082116031282404608690326885859465442262901386243559439593472*y^12 + 28223370740005561844218215729065216151555388544725709475118836090366423912243498658533294816163790505436199866669230669191095865617000657444170006137975685345904360546066656547123976878765654439122029071936800841633785413122156393586072732615942471625459350495071808249715593227631874696297822547479031724748373466040974165790947754256020717/33379006503553852553675480776978509514978474868298764785192334575780989439275765584386446746354023352310359811481133072614980667993973352966552533755296813761200894062052597251765680410730953181426340118115518769447439839844843878049022917110926261949122290969289164305107574812218976832260832288201016258095840309703704916077154304*y^11 - 36938182159295646091171281660568927376516500971517218224058403131098288513011051735719596809436155667952628961155556658192474160549143846063771432629393615260716789803124184068965839510723858474571382028914310051406610676243581265959061957162598257563763600891487096801274929789691719112111852016758719132490328591384403075296001291983357867/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^10 - 67515996193467510494517834721138617114556716865361722237592682251013905464366035792926947547070054856141970188042480655537898828463037320990214905401111125204179905882495161703028351981521429798508800688186107444185275100680517851835628370844738836126693750816428977274110276487886434239777570791102358242385751807766766966296048764108285281/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^9 - 262435989340053915047375174505651549629709578428121455939893442984557874832105914430838884479007784038292700375680783391924577496845714506817767051638633799055325353443606026167088765836835356988206955154093560044981284228127662051010146812409945270420890788594741650486284313756895351487277622452074246510035181932799870746730460658874253/14305288501523079665860920332990789792133632086413756336511000532477566902546756679022762891294581436704439919206199888263563143425988579842808228752270063040514668883736827393613863033170408506325574336335222329763188502790647376306724107333254112263909553272552498987903246348093847213826070980657578396326788704158730678318780416*y^8 + 4949691004319843886829136942218392034695910658685887942240444161387400808948453972444769736111849688243232256706914519811946574028751114586168871963439570613738672086427233189851711434603148738240810487848216239485509574442161448785426129877727559851315867825004112237416702317436259310154168662396536492470500698439888323475900392304949415/25034254877665389415256610582733882136233856151224073588894250931835742079456824188289835059765517514232769858610849804461235500995480014724914400316472610320900670546539447938824260308048214886069755088586639077085579879883632908536767187833194696461841718226966873228830681109164232624195624216150762193571880232277778687057865728*y^7 + 4681925848804108843605014326440820032620274499028350041196445788645010889852678347756032604198713847864528891424378922925853336525893465880579999960295000166697729958712643534682562969762297855519193381721867790033902268146839378923948664249458695313560193152627900795697800922617741186854291079777474441539306638562589078761693456506520377/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^6 + 282407392497830311552812521573201790153338129984635721501379157033033023594421232232741966978263235307485435422941359455011387315086722293092385055889454186550669673289726993713425776443947039406064173227071987094409271199952870183855372550579237609294125783808403722097554811212594638883207125950126710414397735114885943737177969340065983/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y^5 - 3853096795411148529471686090761251154164828249368211498048310411808232823515384476596860355953124289836651062259094114521478322826581785009726715323551749980571402277745807631424497456415484583085451805233844216535876451677312218075156492052139173478401240889924750615699010135169675316377414671859791336036503134345361422420098765133565/298026843781730826372102506937308120669450668466953257010645844426615977136390764146307560235303779931342498316795831005490898821374762080058504765672292980010722268411183904033622146524383510548449465340317131870066427141471820339723418902776127338831449026511510395581317632251955150288043145430366216590141431336640222464974592*y^4 - 282350359636276695403868114818886918233529940769672724976679571715911266991320527874523355544800667017920016995917743267518820539244375400776665767401323900830728383695322117745441218273995861710010029555433905212346491480239913854248727401949590237886639015952177546903839094047836046435187444970536412894061487427794278223053739791601117/50068509755330778830513221165467764272467712302448147177788501863671484158913648376579670119531035028465539717221699608922471001990960029449828800632945220641801341093078895877648520616096429772139510177173278154171159759767265817073534375666389392923683436453933746457661362218328465248391248432301524387143760464555557374115731456*y^3 - 5485364205917095084835728176144713892409019978116570157621325200318736090297657212797797195642845001756965978993761136116070590484743194777278319535007634865342265379450051351716308956893801095868250286157230046570504820661624846682062565581684983576032731036690810367020413366555492194391237884525504092771099027519507995800495224465077/4768429500507693221953640110996929930711210695471252112170333510825855634182252226340920963764860478901479973068733296087854381141996193280936076250756687680171556294578942464537954344390136168775191445445074109921062834263549125435574702444418037421303184424184166329301082116031282404608690326885859465442262901386243559439593472*y^2 - 11834642260530106385902656919757005348899042105726684504571744153830552133695236658258507027168507270604907573755300790592846333697297972394499954924651036609975102858687232259065458056309748875207375001009871947851421818842909207593934700125333074836368764026235187505877152981172795779906279328450573132506038265783609621706261955219991/100137019510661557661026442330935528544935424604896294355577003727342968317827296753159340239062070056931079434443399217844942003981920058899657601265890441283602682186157791755297041232192859544279020354346556308342319519534531634147068751332778785847366872907867492915322724436656930496782496864603048774287520929111114748231462912*y - 22629638273476984331375628505280967464965835111001120987708671279622147076799761090532871376123973635270970308489799681133300926852903966271151214812587491110149842172117189264755407618791423886996058950081600856254362507827506275292677278534777832475652571425968643059063221300746769419282410469360537136978610380268672319269721473793/4768429500507693221953640110996929930711210695471252112170333510825855634182252226340920963764860478901479973068733296087854381141996193280936076250756687680171556294578942464537954344390136168775191445445074109921062834263549125435574702444418037421303184424184166329301082116031282404608690326885859465442262901386243559439593472

# 3 Loop Invariant
-8711835985101799446045992832605937020510420225367688627618468156620339702359257138202598046306177059221563304949729026874964016598077669171014627432246665585921736517841793310041254926358903164532986477028372750093751449003470257090330302406110055707602578613509241552251209646104295652715649992717587406651753857063292747730592546131229176539584570348540222458560111079164930006422428103608013380813/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^36 - 159699312915226777383242627563441918661956138737282902384450090763285246459947277581762175097330523778732762349183395525247496158535498211165367743103221672448563984926840302402488883895012749376841688416201437686194446948773500819184027153869155253432712248851528677079775313641014236507677400650768148495867524718000772947545988804674506478452966816339834813221511716032874807606828616416873966773653/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^35 - 310157873224371999206595853896171849209374959542683890595551890282053380870261019244524335323303165191079792209325630116493498167935651145023199394222814862115768184380007735367765280759110028706027685810550547471808623075426556617025051245730968882910884536525749413128643188920992032940876021461313685256722058755341799912094909880444168042937950016606194541910541119793973222119341270206905005961865/118480564782307152078687959701493035118704409679753953072646025404899882214969474628469310365337769721464306317730460693871124044576682689372195264373464765101713883660547213155958240536030084847325437342549048990521625074048807231057392540712402278263625776784194376374749544110555486633506465618237809924283009717528362883671996246744535494665208257799248249130059622075693612930611395601374901171584*y^34 - 19330742394036230999113536065155046992555066773961910263693059650143940590057330039891162943210924745951128412984202591805865995856673842137566947893779219962829930205880173206325636151028852449270587831346413590267190226874299878535647749302718847544559698647918128385211455300433316203774227842269892673171508745673080648135326417579032700780065495193140882099456779895850376313916166738931123495909767/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^33 - 49651894761227972682001629043197706192774980682178159008057391066900365676183782958948259676559068582054529383796118573440773999954768659786633599480292139918143616387369185113348556098068369733506008530602731904064276261388228361832658227609220912097396710370659317165311488072369911080513553636915917155150722800397647048148627660577314827935786847884829340205582658109215692721060106728302916103876267/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^32 + 180944385343774062676156565038388135281981692148220437608023015803751131063586707980780609043892226796318556949818088745246506474736898671061677296771240606821561709028453784353283858570386212417050577589212531758207177792808639643202709689358176356572857337885772154450930478930258368726003180892440073611008714625994858014933555337334091402453184350254848501743728442274165949904400188524903643511909671/473922259129228608314751838805972140474817638719015812290584101619599528859877898513877241461351078885857225270921842775484496178306730757488781057493859060406855534642188852623832962144120339389301749370196195962086500296195228924229570162849609113054503107136777505498998176442221946534025862472951239697132038870113451534687984986978141978660833031196992996520238488302774451722445582405499604686336*y^31 + 5833325845674874654399634151176462506829077568128847475561742649244273034980974162196398573365312566744168441959140892977008524565956692470613328724014496188193179775499521790694618596280043523684984891537222462231879575430898081158784870001176829452775766638594313918978916849127701686947790440069393941485174214617087002891139929302187042408663850134487281115674694746448171003520525755904319263174631913/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^30 + 864979730610599162693451040048697204759881610626407110132399395061499082369224140171202966851430756447497593070368448581842265371519088730882950911079559615070828753905768750896232960783637926542800784870520995356936074222824309002749514142304691340656038594984974244057972969444892438124973199772829353808285708844575149631352789665536413962049584995219842031953501843761476662158160841555003944675647733/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^29 - 14995570813255760903219143299541543295339659247134605885425203712303461368920378594785485805437397490568310778612183381046127677631525305656715634142841210800625255711460037149491560308522009941873458593918500657628596845468763164619061689897628403057464818615296613293229116350611069708956369535674890860422509088263056346415141327679602704953802919617949701243758077890376572801958733269097448241450109299/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^28 - 1192397892102952232878001012467441144995768829178019036447272395605142227408663931221893317431322929665076623772732574438182815780583559072356647118849337871265798396070369842211636359297692115586786981004961938127110851857565431653134544230934988364928113664163166939036768248356664353186375246204153780394311170751392595693450309765014209435727808734417392686767177417072714690158775672349477912548192343/14810070597788394009835994962686629389838051209969244134080753175612485276871184328558663795667221215183038289716307586733890505572085336171524408046683095637714235457568401644494780067003760605915679667818631123815203134256100903882174067589050284782953222098024297046843693013819435829188308202279726240535376214691045360458999530843066936833151032224906031141257452759461701616326424450171862646448*y^27 + 177588577294984823362446916401610972640812813420830716663906407014551896064191445102348436041080598463831899001664666324821783011244708611840780703459278496433561374688102343692722196179839366531383919849227084224881282017241571254153453201459544551383476314550648301294610713221994427452020527113915061716815440601438052255698071850023497197795036870772137455075586784781297116895844017065060962228616374173/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^26 + 214505394035271081261285604384416461276373254032471913431569797871986198670322979080083936217022538745307962409326285125114635864175227323630121260827083617807420556691808707043793994613939096813226784642480736892373293367913506284451809995588811907487743137091796600115730685309942266605839398923238972236243610913085222793457012238791094149337334648036247427963644425246023124751101245916086401445891675733/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^25 - 551325331603837751551815193919552275508036848288791956242868723142062081621187022890399181484960065040692598851107094851672869563744201185761389164897061193166650625499829322628588993358937196069168586337157591878001071918571164404762599564533991463221296940798409762359151464363048660342690552336899990277694259160812780531951517195950183023893255667523808751361070222805636372929219785202510619979213777633/99773107185100759645210913432836240099961608151371749955912442446231479759974294423974156097126542923338363214930914268523051827011943317366059169998707170611969586240460811078701676240867439871431947235830778097281368483409521878785172665863075602748316443607742632736631195040467778217689655257463418883606745025287042428355365260416450942875964848673051157162155471221636726678409596295894653618176*y^24 - 3123784303862823421328116949651513714094944628484805047123518090252705675841678583442310914507381393323500767778090970960541525399511196086933615259841764939742301868389232131892825113475964468987390656885603038553078589246833764932680368016563053534195103982238195856536801303939469385022027063726793960587614308099488744291969715586584148434350475968673435112127449034222694451712351607465865985833769798515/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^23 + 50355358302359176519441146475299551324513038206094072672924000101694365295136344310427615444253701462393917437310897199542846335498712291552407834682181480047975231388088336631075311368799952456900443536279629648532039944708373582788834321500909162230572908532423327155174999028262284726485162603763962432793663823652833653216876957670484983150055647348214125801716649339013263933662782055474171038279839706441/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^22 - 1933768047733498460183251436041744018017409740854211071545281298602877312642071260601504329806203415946781441779047985456167696238002078804878576826160132169062638692160432080477472519279118130414542239782046655230982114164664943033581078078107148141343708052010528946798069469456587564846368592278371111741376342055138374137164384772305561048925540589254489661353005311808070432081010210862314164706652507437/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^21 - 69239718231457540601500279098967079879552511803727013581413582815833235055535827976281400945074669802211544912750115878044767919413421295542192406384403689617266424920999930953986545299391461131040296022556567204519167491231445489702005512930733023244433080856063166079109334089775788085111135617809029663613787486988962175590604418271468207314682498046051704648283302936001235609149774596399273161562827264665/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^20 + 66144927086113778387334577638033499023791542649073840781400187948017869562026167318187298056407911480242820056329847367211744526262782562872035675718846302975712522012378315290544979512266279614019784112741016467677892231813795771378775821416666881372915633410445062544877437638027353000966663614808955820154744765833794308399784554001998537941737948794737234237607054545734128623945478566418870275714075007817/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^19 + 1381307839956578941362199067277289549957617637987572211076358541793018394023726907828583898319402258870426561340023096210962975896188883633645175173947776830923999530695633711659505606552374129378932587119958518874843056989108881873126814801093143373133804054513390446595252250623466602402913023380519965419921404893183964669691205358177018670563151445503683741659021825428838679145128491630969027737351290999/10302657807157143659016344321868959575539513885195995919360523948252163670866910837258200901333719106214287505889605277727923829963189799075843066467257805661018598579178018535300716568350442160636994551526004260045358702091200628787599351366295850283793545807321250119543438618309172750739692662455461732546348671089422859449738804064742216927409413721673760793918228006582053298314034400119556623616*y^18 - 113595127352305377465219326055733098496202940957348640624684927374376469836462827493312667739849877813698195228667176116141019732546220772760142929761580087381791945968552000587915774568468648141624294306406804005661285754481211244510906063910664329572801524205664012519755822840217972202192018456324301691580437801943110154747320969393250494717591129987624866242558276520670644544734149253841738958366840335857/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^17 - 173422475280402834203970882535188031214283730642996361541393677046995641935685473779192621118036765664727229405105043222420399095468360787154747342894808001262680888937991576110335978492119816390556131728610483399129871633961120408273110728459157141151164651982653769799284799892974860299513031694162879358607856036875013513885209636174950293463977283655870999291970965051730459984457113632537423503165443707829/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^16 + 81789711258136949969651199234086113819486526530977621410491152182650661618390117312690716957359604272590422714862151216634457799897119029148518446127238266330636258574146435123520346029849144363384567887692070219433753668522470679114051222587413493545000248700517270021653262483536843482860741733889137702995584150635037364692139558516583479205176716540932017375122612833867802290640465482549439141237013248935/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^15 + 177253157141324271958105630411862897968461530582650619674605062519120776788602425294965820130160594575477608242617103823600963365166991325160690779413854429530329956415198051093455781614428494863278068817849077738555692956761466370388315165114860501905310644429617322860877916292018345137531590090670075773493042768083689180120135564511494978279862375732592568986169583926485598181325957933803055674036082142057/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^14 + 1772838378882687998377247759653386603565563078568639847675008224514411146962443915501384866138850518287982825467025535798915620236408823234174660305650085343650838825176940741813155867910848690840668891284703893991150084066661109055981278901578858557575740823528420924200042182995106612562927025564887602560993609533315029915993609882224898959224834670118467172064913226351235401251711755977271359834197397149/135406359751208173804214811087420611564233611062575946368738314748457008245679399575393497560386022538816350077406240792995570336659065930711080302141102588687673009897768243606809417755462954111229071248627484560596142941770065406922734332242745460872715173467650715856856621840634841866864532135128925627752011105746700438482281424850897708188809437484855141862925282372221271920698737830142744196096*y^13 - 35078063892614917081490525992812867916640560148129995080937135706617606595171871991201369380784104772694920580129735989450921163467505368729207352894717230446592677548707559115031589044725232809656852617940298270584417965811715638627800397438667753142638876303136589126285075841443656771131756871484434248796598217539814210282358136269299472082759141445234518154836256825248577615595204471330206242966121781917/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^12 - 101300998672329134742751619279520850710290851381076339299819660744711661127971928444540873850980366186404091468219045389231479654094603209139541278377880459420392383969284633417560471303749918042337800342494366544160018734192858770440128177226432486614136245850632994730476405481265888716273167090882703421103398850395497938955418146593904837768969061517084312357937083426874044019731755007034311509919348953109/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^11 + 44280117292783182679244721933357514603624584078377925150346451833785788273567086092081531020878283465744650636298312385397866712724803256911658689327635978564249675186945903459504242349605859681661657877738094737698525373410728405858326925508217686770014649390021246807836323407639598518423927377758641151359444700667917530791263366199592333112610075622740879292032185797536433378049295180840934292226565731485/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^10 + 80839242597647822547671343857206470715392870943303502465298915692472892414643414741291746712686237129056327346293808832349987011192051841659197801778780317446977244004445667530774535390690124364772510700959151702434004274182354466450971059018335894019230292279891902079011405596719618611186174662869727767017263477730624330391652076759500553805982800692858975823442968952721623412523310431169354058833721990967/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^9 + 309343482459039360523289685380054273201657077180027624894440364777745830098875612745547901655789255754371683782182249457857790219418356988878794196182209024339344629644134449768589772507033990513577389244418227424376914937474043826784201839074630500404151519049677790616645384226228942967240729713542668211133811034002229960062354332036723752010264096965983212574062674459885943661470263520455883397156616239/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^8 - 5929110452243540086331278649293423001264686273721409521104569334387451385178919604838785002795941164007901423749283458725820032001599087102420182134137285761088414071463127219769115373594146782193492184514272135620878062894347764559822665115623119280343729435385486627928778942698899078267869228658143057855242302107279946353932063187387054377257967679993136672037331077971474700150081915747844169690721313087/473922259129228608314751838805972140474817638719015812290584101619599528859877898513877241461351078885857225270921842775484496178306730757488781057493859060406855534642188852623832962144120339389301749370196195962086500296195228924229570162849609113054503107136777505498998176442221946534025862472951239697132038870113451534687984986978141978660833031196992996520238488302774451722445582405499604686336*y^7 - 5603912342021976726062770939786179540360980774074658696526599332655711473854286977389027126529295129479340146114748130311182483839902243875469184555777282787948563420018575577621740441045962740670194625806704339362173277440137422484485256212278132123304173294691306202346579675616071408640340988997414266511418647313910974799051687949150564081556682300593940118650559949232389676556373355281147553208717974827/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^6 - 335223585101029339639867890083984738515951964256262182507209159840733601915252054412268348283024809573559788844379908085664148471890918862490124436158232388731334944951664019022780837448645335079717759917002297828104045329984817422781622592704687142964771832393714000091789073395464352815307592456453297519444032770012756108934947388247868757324517837976154247709092870874683812631477295916642438970932002369/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y^5 + 55373954068133759210794321778215551881835563894409097582222914133136879320162602939121185577221019636904739714139116756395285089523765680704490637750084567284093415730646245738473323002249944282136242087150224690229414031590288643821024116969869316852717552278993794311227857684566977416122223544696247210037761108263301121387790561853106147678044520620082655397897287182395875218128751719398971585310296505/67703179875604086902107405543710305782116805531287973184369157374228504122839699787696748780193011269408175038703120396497785168329532965355540151070551294343836504948884121803404708877731477055614535624313742280298071470885032703461367166121372730436357586733825357928428310920317420933432266067564462813876005552873350219241140712425448854094404718742427570931462641186110635960349368915071372098048*y^4 + 337979858183072890874892953614782384423465485577178011132913029620274554578868301220544113184940276246452186654959913620867509734424553826208229658659876562617202771105245860084607612117295147652797065672221168108713657558812523078157448187964827112826952090556902635136614600736264438397338367745660323902073082624347908380954236295875866721728081754437735557971717520067755123661093636097469529082253117385/947844518258457216629503677611944280949635277438031624581168203239199057719755797027754482922702157771714450541843685550968992356613461514977562114987718120813711069284377705247665924288240678778603498740392391924173000592390457848459140325699218226109006214273555010997996352884443893068051724945902479394264077740226903069375969973956283957321666062393985993040476976605548903444891164810999209372672*y^3 + 19693957654293493781838112307765660744438611931238372072772967534983777789629874249459954372524421431827739392886351299759637550233387347072376627939195549491993452475593277699185646453531468279979342792765202631401693266025668148819306354414268309822835920265187520794686507959888967781601870110142849935130390090954522326700719834316589804291574141389445423181649362447814959061938289340372386141486802877/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192*y^2 + 14162022224288063577205560411191549337411079913773532289485064282776004886386356137872129062861621239928858082785480308214220367641791041661140226206486483888479433187879678657187293154422075147016082358214229348769671703226995332748424075645448335196553630225204087280108688010058820806460024995906307697068150455301275314443932778582548848076255632591030814846415631590849069254711710768089984311144262617/1895689036516914433259007355223888561899270554876063249162336406478398115439511594055508965845404315543428901083687371101937984713226923029955124229975436241627422138568755410495331848576481357557206997480784783848346001184780915696918280651398436452218012428547110021995992705768887786136103449891804958788528155480453806138751939947912567914643332124787971986080953953211097806889782329621998418745344*y + 81246439885414068880636317253422611955769794292215842533376330053472392015204967834649210170579194383808960266068135019129879249086088360888751502650100586531003515811885671942594416448410556454138165580604914814809410636769776080898609515660913100264236782590536831341395324587913095535959494658450957383471983499141515302226009900826155006616906584824793171773234923959738536164479189961476791819656217/270812719502416347608429622174841223128467222125151892737476629496914016491358799150786995120772045077632700154812481585991140673318131861422160604282205177375346019795536487213618835510925908222458142497254969121192285883540130813845468664485490921745430346935301431713713243681269683733729064270257851255504022211493400876964562849701795416377618874969710283725850564744442543841397475660285488392192

# 4 Loop Invariant
2391840946603339264925013073812045451575189682577080976130196917854641660900983244293723242237104950525661623619376339813239550199993795705729366670499721944231908089386403452608608680295146999194287137376253410723777010954760468746965862342745976174005285797991708887149289249674170087368686087217525092463295274049148564836626030167837828302949165495324744973663233641587429960171884485049084602899987986561885077556848187802531622132245630922197216530581047015137744837869706297589917091057921308980424802955270643252657156781254319667739/282781288719584067011456312943224071880237832635886219868058483486544236695574560505448486998788215952292109888323000871572246967747284073324433559715518671179053280921361279929271082236851865298773473169762570755666046443345386551637233258479331196497234980343926759406050171210646674440477951785441061882954014316388311847708036119349090108137655128653802138629646967267518560171880472440001924991708615826447944577597265091473071650855353298383380892488822735509773610659850270544742520079051666582125500496142871482487420924712613493276672*y^36 + 219246717620982199103732762366650818868405398332602098481509462337027204219967999534730219766962883956707657259111630250453107763795488350062191685250147340830321867002312215191509028611877601273655159775922551255216164306307511395064314849080931375222473997373481636185315478139988402584291565189976339386066530289415504615397159242620013701497546549613767857138918269592463231596153749202821586647040401006472447229396494739135020783897197370531945746324020410703137150161645366799431244758573901348179510225487353187917772343935603741929893/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^35 + 5110272971054939269115683102564695918930516425398332853736148370024882246586148168721852522305363793910549035483054796415067200687824981771098024767473578088501477759966308931669539741059822244876241508144653831594164285381914576909842066704410965627075228642497550246594862757332147195908221448465939470859007771679331013700210304836730920314635953854650420965276649173915184005346685840913497998401967182052340964283258091908784194416625549148078041101188801454494987690654479273247713016242985131690157601581907302063453321085774601534090903/1060429832698440251292961173537090269550891872384573324505219313074540887608404601895431826245455809821095412081211253268395926129052315274966625848933195016921449803455104799734766558388194494870400524386609640333747674162545199568639624719297491986864631176289725347772688142039925029151792319195403982061077553686456169428905135447559087905516206732451758019861176127253194600644551771650007218718907309349179792165989744093024018690707574868937678346833085258161651039974438514542784450296443749682970626860535768059327828467672300599787520*y^34 + 15928112273227829686026546450711492242682550211868915791446278209725204306094733870437165306308632300502204795146281397376287499182050711572603461991728129074363052179692578707948100597669875846443956039526238262783396870545607639111153205524960844344987005894365869330111100457133780293237950788587384798664169330673286836379495996823892073133078093143350932365339188682901461907686083107348532511343211999090603391615535329824318234998379011947019065938722548018634014816918922262055118054701133096973960174208793166125209750673443105933794065/424171933079376100517184469414836107820356748953829329802087725229816355043361840758172730498182323928438164832484501307358370451620926109986650339573278006768579921382041919893906623355277797948160209754643856133499069665018079827455849887718996794745852470515890139109075256815970011660716927678161592824431021474582467771562054179023635162206482692980703207944470450901277840257820708660002887487562923739671916866395897637209607476283029947575071338733234103264660415989775405817113780118577499873188250744214307223731131387068920239915008*y^33 + 68239707802729366022970189654394724132890121584031495290741349437641625002072333475128433124513341278508101597240635108218915462320248150469497412987215694219151974543441217479530257724159753755574365592265393830445704933811593088095809405159556793711974471900909299651665695472931344447982694594468567104173263391705263850025807360029952774386404549569059742925236868190279357332560833033886365014130562077359904359076792075668800888540684359303533125182926553324082487740522055846943320780041616377245795796020609618343942171458499567993048471/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^32 - 31037443940542366338183578121566770822564102206650307576278932545179840666578141710128314258867611085259057578505249965650080727968087759089670343653970260020950770518683557676958442831004083850187906735065438789657673559046646275491622020973476207792089805868587307247537676939184316865369429512285843138745032189047062908150010580133458833994469802002791911937916629377913269620517256583481061620999713605418188062483273242976534229522059467852993046040034678128621696900715566014496735004730903725464658528749870523808524695679481992084493263/44184576362435010470540048897378761231287161349357221854384138044772536983683525078976326093560658742545642170050468886183163588710513136456942743705549792371727075143962699988948606599508103952933355182775401680572819756772716648693317696637395499452692965678738556157195339251663542881324679966475165919211564736935673726204380643648295329396508613852156584160882338635549775026856323818750300779954471222882491340249572670542667445446148952872403264451378552423402126665601604772616018762351822903457109452522323669138659519486345858324480*y^31 - 8011002156178145655425479694499733853590257565550670571158449293662669452298313886810441651034162286075237353802140463358565675341926504341112089796624599917837054162831912182893373307473474491630674904763482187052364616976067897088633627313942293517425578611284572478880451546367769660764508362838045761380408066963948521594758977643636759524695857986581269790028263318645621942446840284992677638096020851016644403298708936988348303036479900268584871391813496378237042442773925273382421593828399360879357652351301924044363387698548921071873459287/1413906443597920335057281564716120359401189163179431099340292417432721183477872802527242434993941079761460549441615004357861234838736420366622167798577593355895266404606806399646355411184259326493867365848812853778330232216726932758186166292396655982486174901719633797030250856053233372202389758927205309414770071581941559238540180596745450540688275643269010693148234836337592800859402362200009624958543079132239722887986325457365358254276766491916904462444113677548868053299251352723712600395258332910627502480714357412437104623563067466383360*y^30 - 3598318247627828434953448756110041244029018905687269950803119309149791017714764605545627335341625496589235380327768653724552541222152900245828637361736055211445146382039541621153007375027536060487710867907413648085449679902077899261564247634822206709812672729776263725473018887579935802032002657896496921050086093281053396724289524112053333518636280124385081040128888563404032331685593682421098260409325177207799644633063772817629757790493473318790914164630946473434445661131611578408753350333639127874558315333444650731906490355243091135973476241/2120859665396880502585922347074180539101783744769146649010438626149081775216809203790863652490911619642190824162422506536791852258104630549933251697866390033842899606910209599469533116776388989740801048773219280667495348325090399137279249438594983973729262352579450695545376284079850058303584638390807964122155107372912338857810270895118175811032413464903516039722352254506389201289103543300014437437814618698359584331979488186048037381415149737875356693666170516323302079948877029085568900592887499365941253721071536118655656935344601199575040*y^29 + 20585462112096753189998692687399155684595445143985052032034507426212643958988114208195873285003572025726386862824763632940016601451191960220142026394280207669332446673799088097220088306542975281105186133514852518253859080004847531050068353495339961317661600438167032533940566960839391652737545054402468354768443610038078241830654873226797217270886820584560292710933097749098108360820350865664572071140144882480141980949912698335260255953703180519259582742752024882855643241753310554155873742512963024385595909402410343353892029591546087257510060137/201986634799702905008183080673731479914455594739918728477184631061817311925410400361034633570563011394494364205945000622551604976962345766660309685511084765127895200658115199949479344454894189499123909406973264825475747459532418965455166613199522283212310700245661971004321550864747624600341394132457901344967153083134508462648597228106492934384039377609858670449747833762513257265628908885715660708363297018891388983998046493909336893468109498845272066063444811078409721899893050389101800056465476130089643211530622487491014946223295352340480*y^28 + 10498714631880581630064982906998737377798066653898286903722521073559134535522221279791455033980115723598815880347685226444991392776084819826827895736015014619412483879406556243228247514226265993707292614546835460469539287141352810939283553025200581488250793068285108018962523477919599310985089493811465945283788528195019870996114756361420686542159627286006055150386381893374314579672032223034978342007232950461256866167270251758269991189162733228898353348314261695991717521821452432365749468402119300482196374561852266001502419021095055098528017139/70695322179896016752864078235806017970059458158971554967014620871636059173893640126362121749697053988073027472080750217893061741936821018331108389928879667794763320230340319982317770559212966324693368292440642688916511610836346637909308314619832799124308745085981689851512542802661668610119487946360265470738503579097077961927009029837272527034413782163450534657411741816879640042970118110000481247927153956611986144399316272868267912713838324595845223122205683877443402664962567636185630019762916645531375124035717870621855231178153373319168*y^27 - 731146296199056761584227356497877765448412896780021394280474141354644187475400608196665499358424487122544338093895300342906086853208953274114178524008957619914129778751386551167289741108080974387809943178715969584451592285741486515784418184612137473163399368652039827581649251786212719956955043283055744134488439967884885190173573807223011628378376520628868774083153841719062640292798006058059194370782970167226689683134326224484305599667379083889390294407418362320849645210847831926952556444975410244633684425869124935054854111808495286247876727257/605959904399108715024549242021194439743366784219756185431553893185451935776231201083103900711689034183483092617835001867654814930887037299980929056533254295383685601974345599848438033364682568497371728220919794476427242378597256896365499839598566849636932100736985913012964652594242873801024182397373704034901459249403525387945791684319478803152118132829576011349243501287539771796886726657146982125089891056674166951994139481728010680404328496535816198190334433235229165699679151167305400169396428390268929634591867462473044838669886057021440*y^26 - 295260919924257988885521273124306573867176776242864212709521148010017563819982226263084906033188154447242782263700497181647145083221033208675414053658354833884973843037709458956394267172151549485621311932510103357252987281924057614650476345045605760839160145707787475140644601312587808808569751652208852612091101976849719773916855777081570665464531970981503303775101085149918737822114234271343841045294357888632542908527970363085281645290067885999327748077863888146888978730041109496556561128703165552272938195170606429120877454527684431962416067591/201986634799702905008183080673731479914455594739918728477184631061817311925410400361034633570563011394494364205945000622551604976962345766660309685511084765127895200658115199949479344454894189499123909406973264825475747459532418965455166613199522283212310700245661971004321550864747624600341394132457901344967153083134508462648597228106492934384039377609858670449747833762513257265628908885715660708363297018891388983998046493909336893468109498845272066063444811078409721899893050389101800056465476130089643211530622487491014946223295352340480*y^25 + 2269806677032998707623971840578127411345039545393498889104574733770989934171100207979647687058699720473739332080340222998137122521164869039310893991357344248280667801795876089237420665585367990019145212471105163530664884558661110760815019069286872781225104593133494055543266892880096309839995667063917870952807209447653699558613337955017867680332279986197534183885139200850838159222724836773475453433518473867774552088810861928458702299711400568917802664238795979876645069505024782904547659653369887008135013971097204939130465987102441361050852314237/223248385831250579219570773376229530431766709975699647264256697489377028970190442504301437104306486278125349911833948056504405500853119005256131757670146319351884169148443115733635064923830419972715899870865187438683720876325305172345184151431050944603080247639942178478460661482089479821429961935874522539174221828727614616611607462644018506424464575253001688391826553105935705398853004557896256572401538810353640455997840861689267092780542077671090178280649528034031797889355476745849357957146052564835921444323319591437437572141536968376320*y^24 + 13006121924499273374491706360798367702993208032792870954174662558270572624401563833539438586568406779551148530888706526318480996235404231327801390263911307995458452421608498314305639184020557832603227753017872203725415303576103095645633052927534601591989693522338232936671870524004095752345406075237610488130584028719485475735787367172623774190539847124142645028534974599824392298964748376794013353426636933149841416132771606744524591500037605409316832109447569533193390868211462577797659255702250114740752413907833113527043965577276898049573505813379/4241719330793761005171844694148361078203567489538293298020877252298163550433618407581727304981823239284381648324845013073583704516209261099866503395732780067685799213820419198939066233552777979481602097546438561334990696650180798274558498877189967947458524705158901391090752568159700116607169276781615928244310214745824677715620541790236351622064826929807032079444704509012778402578207086600028874875629237396719168663958976372096074762830299475750713387332341032646604159897754058171137801185774998731882507442143072237311313870689202399150080*y^23 - 69129814415456850717181564783514386802198596757708196559291315486501477590777278650022185044404756641735303227012492514792227369008833748819231955843594831589340005207104190975299017005069116676591700012503135675609446895406990272522053353242483471247743819606607876257125914845889190466221777708011463473135350849445614793134649038076731069047868816227034133892638457107559258658289167631307619782254897700350275262061776881499215571440369399443591753084674473582061342513557719071801113390606678132519188424559941044248973628435246879444150639740607/1413906443597920335057281564716120359401189163179431099340292417432721183477872802527242434993941079761460549441615004357861234838736420366622167798577593355895266404606806399646355411184259326493867365848812853778330232216726932758186166292396655982486174901719633797030250856053233372202389758927205309414770071581941559238540180596745450540688275643269010693148234836337592800859402362200009624958543079132239722887986325457365358254276766491916904462444113677548868053299251352723712600395258332910627502480714357412437104623563067466383360*y^22 + 7870586854644128112367109234704578259390910989082990316925782951952219488670669145529159606926949571064533061956420421203674602136592277293902729540690651550329494510032652644480115438723150761429301134607296006687261774831827978220932526206104690870676814442632400740774013757687130559424206735987373898462930681296722961196315265718900199763808471432799973411787811892080982178670299842095028351495834470759517686523694705462448842762273235179144707887323690599824577165397448120358494318389532017278606738486351015334170489240887644942684201472373/605959904399108715024549242021194439743366784219756185431553893185451935776231201083103900711689034183483092617835001867654814930887037299980929056533254295383685601974345599848438033364682568497371728220919794476427242378597256896365499839598566849636932100736985913012964652594242873801024182397373704034901459249403525387945791684319478803152118132829576011349243501287539771796886726657146982125089891056674166951994139481728010680404328496535816198190334433235229165699679151167305400169396428390268929634591867462473044838669886057021440*y^21 + 285359329197106110843421458359663978528222691942711165239286191921226213024878348338139377355170343021883184267796351611333865949991796817616686338250798594967494638120034399355300519015158579830607899949341207391652941554576977476456009404144297101131114546572630599695686181276166865079600929462373571678702390490581635696969708452979370784906755800908706626143939904019309540899174303372565911507897878330689167931260126691020886835769833873085559161865490991004242858733214570025762504764606168974965010177282401204182104550010847520942536018656879/2120859665396880502585922347074180539101783744769146649010438626149081775216809203790863652490911619642190824162422506536791852258104630549933251697866390033842899606910209599469533116776388989740801048773219280667495348325090399137279249438594983973729262352579450695545376284079850058303584638390807964122155107372912338857810270895118175811032413464903516039722352254506389201289103543300014437437814618698359584331979488186048037381415149737875356693666170516323302079948877029085568900592887499365941253721071536118655656935344601199575040*y^20 - 30083679657961719528441783038904875379164840148096554112976665849289101524189073312009670732840518874353173971648429466882270295955775658691199066264928993791919913263460387472843837149572361194739442790467031856880585531648816085188697597132069026354688232977878872166515909519563050605098094937743250447000020478755018212599099729584006255529007515769316544885640473487444881653918235397474129392862823787274979052122365699331184723233832899562953002888471615475850064472728466606147585415746709996193663425406382395657387892222425432776468620630309/471302147865973445019093854905373453133729721059810366446764139144240394492624267509080811664647026587153516480538334785953744946245473455540722599525864451965088801535602133215451803728086442164622455282937617926110077405575644252728722097465551994162058300573211265676750285351077790734129919642401769804923357193980519746180060198915150180229425214423003564382744945445864266953134120733336541652847693044079907629328775152455119418092255497305634820814704559182956017766417117574570866798419444303542500826904785804145701541187689155461120*y^19 - 43674715120587932414270710790912216389978333686736562111237707927317753168861491332697702517637982190152893890658290336950525260409643786674210470176933478285119358194101580901608623509683132031939511349407270378805552532986392421213465230946004805284120106672538734042667619908661064342915399201959487799383624949380278405828399369227642950511043177618858590411395846555137956702308223994399574973649164652834602131647300586049638066456636986947747665074983407945304028732237547030960794341728599476101234038691196087516267207035543424574648683412753/176738305449740041882160195589515044925148645397428887417536552179090147934734100315905304374242634970182568680201875544732654354842052545827770974822199169486908300575850799955794426398032415811733420731101606722291279027090866594773270786549581997810771862714954224628781357006654171525298719865900663676846258947742694904817522574593181317586034455408626336643529354542199100107425295275001203119817884891529965360998290682170669781784595811489613057805514209693608506662406419090464075049407291613828437810089294676554638077945383433297920*y^18 + 465055590418605999909731120615893582276414152004938904180931304317962221583575611294841207333473784325808534476267026593929858195116449871977749794629855527625352837941371582076958929353688977404679732873701740588050196694992599356510352225778864221662670397812520969106957204014321545299616990432196712255497831428343955884636081726651384101372378062513310962800342304901549432475545401294420412974953105758072935274621356803209672877698596047306759366421610605042964111992855850385648228573799219905871474730405557639553930720994979418727109178974697/4241719330793761005171844694148361078203567489538293298020877252298163550433618407581727304981823239284381648324845013073583704516209261099866503395732780067685799213820419198939066233552777979481602097546438561334990696650180798274558498877189967947458524705158901391090752568159700116607169276781615928244310214745824677715620541790236351622064826929807032079444704509012778402578207086600028874875629237396719168663958976372096074762830299475750713387332341032646604159897754058171137801185774998731882507442143072237311313870689202399150080*y^17 + 238490799750520094291528630015018933296963913510059545730954393560003952533088892703098647566288798465737161323889200459239913130939148520532306636435964267311168263669067721295177305161742645528447358669957866477468993271748382848561499015526953627707820987068167974688352208782537517602006149467398313818030943559603849550305437583589288038810070955816877100220182721182733605023031145777949990705358402452359905872298815123654117995733276019881966735917858514214876591065846715154893697084388600211655114821051454236607123240714993963004952043859493/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^16 - 66651525399235995877098973224514349051911977727263526756379606950077350890509480008224403408423811058016246739233228177907351960535586368405986534469443196185399082352046493156841094805619456790650698363631146643816170947801883828686829234602065821263185872531441787418494991297190119146426995364075136547451984417871235866638831980225603567202603101153967311520414133707711990313913837789006420065147041107173455099585337732542957445914154479504869054039414230987213205758817111019158019636877897795112170543301152188697156160937372229045900084278615/848343866158752201034368938829672215640713497907658659604175450459632710086723681516345460996364647856876329664969002614716740903241852219973300679146556013537159842764083839787813246710555595896320419509287712266998139330036159654911699775437993589491704941031780278218150513631940023321433855356323185648862042949164935543124108358047270324412965385961406415888940901802555680515641417320005774975125847479343833732791795274419214952566059895150142677466468206529320831979550811634227560237154999746376501488428614447462262774137840479830016*y^15 - 243734257043233270739130406755116682246891121929034654790162464171533450488947119008573721802675273265286224025265079180917774318891911439361652442148209443362842442267170508279230552194049492295977741382595540449320697252356594502851518355941548716551994154146853918995423322256750861199376228772502630640239910053938158158321500311420342039121740496727821278231255600461835944665168941476843144573398044096567293213110306353467564915850365765755881129686333865042125664594017659257615184522424301493710880606920187595120494163110879044660066477544907/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^14 - 504412623080273124065436959277565976448583924300698623599896495041113792836971343063629194532556481462969566714261834364362571650915265138430206584989569181820892569679879165475102922138220563340288791006632992069967732900399908715440317507444451042183692999713839809579094757937314995191538895998616067652364158414707862798122732610122204833168832785558740635021592720460233969069682345314813121474605555640101387339727924397406503101089239690449890330995164419288959464105786978472468856056843584828852490639994570517859986181914837470437429335183/20198663479970290500818308067373147991445559473991872847718463106181731192541040036103463357056301139449436420594500062255160497696234576666030968551108476512789520065811519994947934445489418949912390940697326482547574745953241896545516661319952228321231070024566197100432155086474762460034139413245790134496715308313450846264859722810649293438403937760985867044974783376251325726562890888571566070836329701889138898399804649390933689346810949884527206606344481107840972189989305038910180005646547613008964321153062248749101494622329535234048*y^13 + 144620763684717798132044855103859752933120009367450427564060552451039676333804436871491741047438236726757406529850602913793482247431345165172311161643966481964194095158820463096973661439314874681786548141163981135426456938963467353953588095780982921785676749295454636874189205698339104848485582290971482450365610298003126360520323681660221415426912227414451022710586973002113384178947438922276078576379939004770418051820511002502226155810495139644994014798598274608766333077683410723068711255723690480993359076187926318411552311066757886000614798202213/605959904399108715024549242021194439743366784219756185431553893185451935776231201083103900711689034183483092617835001867654814930887037299980929056533254295383685601974345599848438033364682568497371728220919794476427242378597256896365499839598566849636932100736985913012964652594242873801024182397373704034901459249403525387945791684319478803152118132829576011349243501287539771796886726657146982125089891056674166951994139481728010680404328496535816198190334433235229165699679151167305400169396428390268929634591867462473044838669886057021440*y^12 + 419985574408546069171664745018468066591616653131035602650769542632150688585470201054614127266630802069626010408460282198711823905568314790782036102455509257095536889645757983628311017370939961688957337181003818131232310970250827383653301826167386121891566141586408811538489316726135367498098240226042639794451384159334621611948154982502338943085857022097068246415720766745354217664592421636235492730087071789239038765726784009065513032447298964414599618577575210674362831052676040230502604303870719596173261307773239096997862575821941255095384496007801/4241719330793761005171844694148361078203567489538293298020877252298163550433618407581727304981823239284381648324845013073583704516209261099866503395732780067685799213820419198939066233552777979481602097546438561334990696650180798274558498877189967947458524705158901391090752568159700116607169276781615928244310214745824677715620541790236351622064826929807032079444704509012778402578207086600028874875629237396719168663958976372096074762830299475750713387332341032646604159897754058171137801185774998731882507442143072237311313870689202399150080*y^11 - 60746568970374226644621560383870205282794643470656658856588282511724388712703777143465331347440760766047273523305286924631938206122321619429090337614711288276277068501414326464930352138981339706158946633353865272206501045584469163547504839944619515240181341217082745825165607232374380617234415793337592458215699786904884629280665122029573476007086215756813615810909116321476921903473241566372192546059798166863921479518858648486602540171196548777863275261137695776842620191542646449164452104265875287242255728461767459775788309996970235863861544211143/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^10 - 334183379337565577239648270346492758127131307245899647405911466525115377895615810721561737867534794765611364059258482812873756467133533757327432664699170853623959087185976395827606864503412322016665186591968765348358414591045464203152507304212377124262970570976985087190755458438850916627498329165314677876793018291737965801094131579276248026706947172296449901255512430631030763173882509889408415239560457005563445450325345027340969978033089771898044407200341481298210660812294680777397958235482684165618358784187316186048406028145013717112123423562359/4241719330793761005171844694148361078203567489538293298020877252298163550433618407581727304981823239284381648324845013073583704516209261099866503395732780067685799213820419198939066233552777979481602097546438561334990696650180798274558498877189967947458524705158901391090752568159700116607169276781615928244310214745824677715620541790236351622064826929807032079444704509012778402578207086600028874875629237396719168663958976372096074762830299475750713387332341032646604159897754058171137801185774998731882507442143072237311313870689202399150080*y^9 - 271004095363561415502021247503662341713380888986511335722790872353194117923765551923919452897707795649552735498448725213166266203214705408380578209038032386841200411769331378390710747093284686932464048620578905460307243907767627465029118412026134806479019996026341921154673389420095687596461719430121558395771139837892400899143636930680301849630319393106174241964552875165188207427622358685587785935991710416396929576387992158146669525919452397810248478844526256297412770387193889372481619709541247692882600068476266172768968363212023232759721702647/121191980879821743004909848404238887948673356843951237086310778637090387155246240216620780142337806836696618523567000373530962986177407459996185811306650859076737120394869119969687606672936513699474345644183958895285448475719451379273099967919713369927386420147397182602592930518848574760204836479474740806980291849880705077589158336863895760630423626565915202269848700257507954359377345331429396425017978211334833390398827896345602136080865699307163239638066886647045833139935830233461080033879285678053785926918373492494608967733977211404288*y^8 + 24467477161805048151435020788031147252207956755392605053925013452501358742995018194244219468510644379862637585627129828725340953452569832337644673822735341632573588012865326607900951983511891772039224782855540588157344186973795558770662975313150331933709882823600860513655747838915251554856890120918047586937645295247512975311596025035557605565721385970212671318819216376792366530503314006367819521684413704425009911210557984627579194173716415781724075186837388645279157048975538644768371660533938430193858951082062832634233177742910979770350170270733/1060429832698440251292961173537090269550891872384573324505219313074540887608404601895431826245455809821095412081211253268395926129052315274966625848933195016921449803455104799734766558388194494870400524386609640333747674162545199568639624719297491986864631176289725347772688142039925029151792319195403982061077553686456169428905135447559087905516206732451758019861176127253194600644551771650007218718907309349179792165989744093024018690707574868937678346833085258161651039974438514542784450296443749682970626860535768059327828467672300599787520*y^7 + 2577353667744020182818887111036759642270130913087022506799534999391397759304800903527299772324268471674461365144995327736264305419097643834233308217011616749993489191809606649363782102125192121338199721169352420796669568017685362874387583903255166673546883493273177298171645044873359816865642243828549814416386952416285270358818508502016424908415584324895529978381615397539610807721085889871975227170979592726245722028549244067852525131612974274963422346906026730794089865064525847151101059143024573778307595993019789018341844444735231748713383593759/235651073932986722509546927452686726566864860529905183223382069572120197246312133754540405832323513293576758240269167392976872473122736727770361299762932225982544400767801066607725901864043221082311227641468808963055038702787822126364361048732775997081029150286605632838375142675538895367064959821200884902461678596990259873090030099457575090114712607211501782191372472722932133476567060366668270826423846522039953814664387576227559709046127748652817410407352279591478008883208558787285433399209722151771250413452392902072850770593844577730560*y^6 + 286840630179834383105364560853836148926697399556852106000103811207890637464967156464944373178648798452473239986335201162688774687949216446879427402140833982846774430387669792265238100666477764578708508460707048492450906658552758578550391746978210838220116555513620932668994263727666535290558923874613192230185755691102813557359579663234513218847570095603494157490777033069507170365571752924939807139514217965124907891413614785034436081332378473802874523421502843957303874111176606395180227964988706145719140091030756605747943291486179370930298598037/848343866158752201034368938829672215640713497907658659604175450459632710086723681516345460996364647856876329664969002614716740903241852219973300679146556013537159842764083839787813246710555595896320419509287712266998139330036159654911699775437993589491704941031780278218150513631940023321433855356323185648862042949164935543124108358047270324412965385961406415888940901802555680515641417320005774975125847479343833732791795274419214952566059895150142677466468206529320831979550811634227560237154999746376501488428614447462262774137840479830016*y^5 - 22867571272872906017504253620950086677612470862439311499262284275850498183153257819130815252332403919083075904708205818936771989501505565590757303580762683517620478977024932503322658628981822965898151458960080977260806557824299509740517027472173173395483479165626170102765633891713277135934926364028105114555060367488640884533981686924848025096855523643487647357247675227532394136570196345555457077212706593251682747678711376291989372382561930839672103101128462881246204807004593048852638288221739937971875406512500667799051233558145465369349331647/15148997609977717875613731050529860993584169605493904635788847329636298394405780027077597517792225854587077315445875046691370373272175932499523226413331357384592140049358639996210950834117064212434293205522994861910681059464931422409137495989964171240923302518424647825324116314856071845025604559934342600872536481235088134698644792107986970078802953320739400283731087532188494294922168166428674553127247276416854173799853487043200267010108212413395404954758360830880729142491978779182635004234910709756723240864796686561826120966747151425536*y^4 - 466223955656380906718388846654329905675986721268830964895061513259856200861133023914516497268251071727305529408760798593356811869735437632893723017323653107419805480499682220906256277175735681274391726145002577591832997660744619904591949425459091988030784754020232952761340865268681840373134385831584007888435107284439763819939204352167714644504002526511487694873928132567264633703000900004575611405130631455164456328717386009657957271621016349376870083421030605419947906177647979388189240532809873429474779285326799937969404849068325891414803810693/706953221798960167528640782358060179700594581589715549670146208716360591738936401263621217496970539880730274720807502178930617419368210183311083899288796677947633202303403199823177705592129663246933682924406426889165116108363466379093083146198327991243087450859816898515125428026616686101194879463602654707385035790970779619270090298372725270344137821634505346574117418168796400429701181100004812479271539566119861443993162728682679127138383245958452231222056838774434026649625676361856300197629166455313751240357178706218552311781533733191680*y^3 - 16319373233797606896183991873800972282978611461862154786514522086194228332911956838781337594976386622450413871050156535755549869740381227057710776145590873877109080148461325096885567816219061858791216120144690146315301194923927182805083646301563595364378989462873694119805987971109518527417150134646532077878752498624285246537434062179998104739677715262014647631266143330624865825681738600661127441946747926718137179310173989088922217627726970400228161492495887635518121127339247478703453825121654722402100220620101098004022666639802492344021392461/121191980879821743004909848404238887948673356843951237086310778637090387155246240216620780142337806836696618523567000373530962986177407459996185811306650859076737120394869119969687606672936513699474345644183958895285448475719451379273099967919713369927386420147397182602592930518848574760204836479474740806980291849880705077589158336863895760630423626565915202269848700257507954359377345331429396425017978211334833390398827896345602136080865699307163239638066886647045833139935830233461080033879285678053785926918373492494608967733977211404288*y^2 - 1305079949651457953770783977634638413371139858642958087626779454397078561885335263052224336435792116624159858158701583860412696346498271017534970450302054119090808882500861676641412860136473003749827556899009947142745201755651815026218283383018080576941270787267269244205888979169315595294471163070022765308949242152271540612788596468558075474509418027001567439903288078000066188067090573795333351734077454121397742603991228262981288212059195334743103701886528306386575749632986728227015662749350547619390867534309897105758637058943610394197104709/94260429573194689003818770981074690626745944211962073289352827828848078898524853501816162332929405317430703296107666957190748989249094691108144519905172890393017760307120426643090360745617288432924491056587523585222015481115128850545744419493110398832411660114642253135350057070215558146825983928480353960984671438796103949236012039783030036045885042884600712876548989089172853390626824146667308330569538608815981525865755030491023883618451099461126964162940911836591203553283423514914173359683888860708500165380957160829140308237537831092224*y - 337095067415500060892813766365524945089825078697782559610797968273233767131218619114984808706522701433976671265545153684893765567569059883786326083877649493394468894311652198803614548253224728796420651520140401758964562887334942500930826834142726955942578391983281700002625873434174853054233394347620437223855998220375940690847973370580577832420427266961301689420625391710574573691707709972681311164551193598401230601351051176551318048946964310306079581523557882969228218772828846991106745810536754939685052410247791998929901187346835445561474413/605959904399108715024549242021194439743366784219756185431553893185451935776231201083103900711689034183483092617835001867654814930887037299980929056533254295383685601974345599848438033364682568497371728220919794476427242378597256896365499839598566849636932100736985913012964652594242873801024182397373704034901459249403525387945791684319478803152118132829576011349243501287539771796886726657146982125089891056674166951994139481728010680404328496535816198190334433235229165699679151167305400169396428390268929634591867462473044838669886057021440