# Manifold: Census Knot K8_112

# Number of Tetrahedra: 8

# Number Field
x^40 + 14*x^39 - 58*x^38 - 2191*x^37 + 3534*x^36 - 48818*x^35 + 83390*x^34 - 262597*x^33 - 344957*x^32 - 111106*x^31 - 450610*x^30 + 1958256*x^29 - 1123032*x^28 + 9153878*x^27 + 12481572*x^26 - 3538403*x^25 - 26185819*x^24 - 62497913*x^23 + 68713783*x^22 + 36444192*x^21 - 159148488*x^20 + 106192735*x^19 + 194290033*x^18 - 122798622*x^17 - 136692813*x^16 + 35309528*x^15 + 55895362*x^14 + 7852304*x^13 - 11534171*x^12 - 6504221*x^11 + 335178*x^10 + 1306908*x^9 + 315765*x^8 - 75574*x^7 - 54459*x^6 - 6002*x^5 + 2862*x^4 + 761*x^3 - 5*x^2 - 15*x - 1 

# Approximate Field Generator
-0.127004216716460 - 0.410286230358018*I

# Shape Parameters
475010988808681671598771129294550561817760907084066617248782491736930095687290778517762959341091264717285117299284088917288060318211236279336005603/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^39 + 6483354041125096296671327300424959131491326117917535516581274192520632503005406098262718115263227490504841027921332984429885020903746661247261308738/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^38 - 29827640879482121193370732127776427080751895492451698965717995884984484433253586840063119163762612507588153865338319579160058929340465757221486749523/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^37 - 1030280546685055784722645466930303210298519266667300599350265228392094230441571839355884753220331678285971909986665774673196392586157226362701934197182/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^36 + 2040491143288372479780209945205864102808432802337053806571035690313264452905895110562526463427675289677387666933503137191490702497196320443620376471219/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^35 - 23904768520863530025612734507265672375780183662340346298275506291120046175289731459750759622247687490351144681895110025680819000079837942136018872129623/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^34 + 48004275141715559729610312997587410759967515746031568017349731631491326515466408537481892898355145313656713196947090055429996076882446772615341400392641/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^33 - 141575029724406320223458461521715810838587922378587699221304517116723344307091991752555399592898283197327141192228553873588826578331365869834304137305706/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^32 - 114169362728652519801032633047439874269491478540910983806234566418383628880337795591486806843150345403616198147427889500733801271065083989692580898942085/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^31 - 12595466272736419263114231754508829346964194885670095436733652938448296778938933667388797322424244063280707157299259570435640314199307839232740240830177/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^30 - 209458126487008234793865284259831674050231752824957427993258927413043685307071440283144998079247382385104655535052477476154536175885949775924180791221154/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^29 + 1003844456288820345651205046559250423636404192869155986388183508768312380274795822750571791277080315760113624757503392890494281403697340789383359052550598/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^28 - 885732659169013164099883098243672435846268821061300290140757786121051529149825048775890553375931899221842710281242500765372434472449620718427815610517307/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^27 + 4658562916722835454163582927009298003411580946608420063242794280842721746334091066445850606554788445914419349496102830300978034610010093130904672207093030/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^26 + 4293229722037271257314181811112337110821464740458938298639808962193463191481660199077326095721834290888737381909790100112037777334251786047604916467545951/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^25 - 3191737800170403241441190403220665987992251101049489318831102094587716525448353721069627313451682758725505255262595959768673280097442246936849776807672095/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^24 - 11323764438352711388578476438723500808338115328669312584062699104044194157471873652840177465114290946645258117596962574552981527472055022114575522355368638/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^23 - 25711705024192418513180758553286410204951407184920167640481571365353078305698993744465548853252636240005541653614049713958687695794756228604224273742524482/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^22 + 41677607183895899140494496939353271428153297021189791354467617455262339522227302220380658985159968625729645229008094563922314875153786274048846478008722843/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^21 + 2703028347402973229447847152520950232403556680936517519014207206915143419335211224346295384333919877836922683049279251934871449043313180071238739681164048/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^20 - 76562454106365442773986801963197562836365269762441360531502995960416459793680679055889548540403773267913370088850719062410523785448522393061074656777182754/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^19 + 77309291491088967214517602745485466286651513036535527574591966935701127739914147642497888659823622115100972295495042326916370151552447433507701974130078913/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^18 + 65197362659795072611030277691279238543907481699192015286256045580172406266239220439975112087320989949970211218988316199065207414402769247656145067687022866/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^17 - 81248059912684127470610232959949730987711869467509410889730990618224666208103170033518749133447850084548476853768990882090607016417259765122024157321902911/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^16 - 36480287790819248360578549196183277228586679069777895096188190839249524450891400553614395582477294070804617522351539559438809063884147703168195305643126671/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^15 + 29603159081525090631984721148563274802574656384019082542505548414792492669428524451683672116490364321908674259254880529785229634382686566437269244289040679/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^14 + 16208158433112079853489879393748726324848556847783144824721175095624842788610859183436192749529597834424070530606688011430715773960301173416927966815623553/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^13 - 1957642485994963527909437265452650532915016677865687141647260955594268152901476123378058503283848709904201236239518507455923770536453625529889739415127577/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^12 - 4806172931592287515924348427712337056747754815157513682548981913155922367734720159718240061881408241440523776334411066856016406387430882435603516538169527/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^11 - 1409076787945584445810188734695352034708628117468335232739868037523654004992109325411021998905086979437077617895179362023332834579777653147233324138975253/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^10 + 654539977982022614821388220931711030801988361543660935203129372336212353586717906369047363585597941795885009447894832342834805101461927070901719678834844/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^9 + 392909088123573885175234116420089432824297315120552650503394236199028955131821443836644001081686809019138024570630241410063493386898954622702605179626078/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^8 + 12581164194918848529308852812806740072976704341387319544486406650059196675799078027639166847340569803337028615694924991019041521271894946519325410180214/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^7 - 40421164831679755366278694244430274707262548713430445781881328076284052428223965323590942877713391964352723933577951931088012335517157875839601461012496/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^6 - 11771057132238731287900691037727325724099511913955192899751130429598664047865880891366213027666891603582975206430470682953855242353658038085659274234418/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^5 + 1264212436975641832531964654536604709608084212854744883553562686255596744309543434068582880368888016837324235139807054090173621526120554373335358094565/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^4 + 918866535850006801306068742223595368976978099103721606883267381318638608190303952437765156393996624222797636968335915331570308785919820142490500076020/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^3 + 40449321752809925673696977830932251541982789252498252619636520135894012546774764629286244975974601041389930143704706423869985245219106463026752136495/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^2 - 16581757802163702323228491484763755874017019804324760024699541442578126544061582605624063838435903580565061434731999086065018974917318598704981784119/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y - 1291951196135703950351160233951534621492804813535320623156639697680133149163165191092406592470709809395384022955779173008350385894471005506593182281/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631

24909229891653278930811775356641699634397848828602072127605494253805424463914675851202859135987398316278337323577095988751515250597514424558119578057/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^39 + 340475602771248719627982161366598541901576823295506811688295671022477912598785148572368297750207114880949343008609842170117425883015759501630348516814/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^38 - 1557200086066400128628450771913180066390896367630690247366803370615696395135404603144476275799959946518967818472203988657603068999329879274409246217562/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^37 - 54055202492526004968286487052900778014622032888016385585828243254028898701045327053325279877355324698996663833965950031360464192499514712396119565711461/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^36 + 105920418829016187821007835508069483099935630834470958448042144006160740311069507709673214619773765273310863288651871710554003493381778077249586338669098/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^35 - 1251885310749510492663249949441893516335527088870546096221451919193368445324884322482110681057388502309315358603856591121917470969684602430545527210863512/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^34 + 2493159587319308921275524137526229446163883105005377119315936600500022436368448979539712701499569324601636898794402376442620276106044817738107666886285365/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^33 - 7384359721802069116215057594625401995106942049741702663556059840631317408512063266438955444367543673907212318477190375622079738388860564471508171524410825/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^32 - 6117864067778480867463703979206236187962057705542734952451377543354901534020977199556701072584444106377045388667633717784705509948774320816667445162205568/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^31 - 833109133491743321340779802254378831118054447792994016098243453550247978778069699167843214884899376424802660669117220925359160380402806750640644152627602/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^30 - 11072911634242862972591608512312500036103171374060970937608695764859449447537456493136362241042043980461344310124305972777305429258616878084081552706469231/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^29 + 52381898293104783982487211699577148720969219628986030672050947233176738271088983755916551871022723165225489065469686280625022304605883244021121554446548148/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^28 - 45516922001687139802397892826795385058878372691572990513404928594232992652286888871849193527928625379053847122206410348302595401454911182110477565838922718/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^27 + 22159600708059774621126154520098458033779428453050126104068046823826908409395412890503993104547239494640793278934143694277621876898172275443429258085873085/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^26 + 229767936945421560753636578680144908045589740448902084601871327796665009711055073528489256476400961504088878302796376617647866932510443553412582711662351024/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^25 - 160980718710969089477616557299046819518372479593889464653936261929549945856677816785532662760956771455788742523760555931152971915902383109416595158680227857/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^24 - 594315079201355104340066947089161668311759666081294639678462463611233952184019276231882385361856714951619983501465616449579138644661099938406793230184026995/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^23 - 1360119333445749768672605459082843230772285845403720350027685977723895138863051585091236351589042104793314070276791224372265279297001791457952067537980400564/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^22 + 2153898293304661324431666894015626707386456651500778358529740310318627275566538850229823718948849120336734507036243143217310253969734155289803699966545519882/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^21 + 171463079753738491472882441931963215926959388233730667700835379505068162511126776351623153055233467367954411501184369965095588662882592720895081692575137921/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^20 - 4000355970550601757801286961873578571379404695890808939725780084833302360562761785686722972312255831246111830348528469529245566255858131970329020730308726602/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^19 + 3981309738668785450730567068601727246042917937214475196893751087612634273186547246736245110947005272754068568827339069209040472730221691663084265790517773470/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^18 + 3468738588324977528944564447693276702255583133762545667033190880025760721860670829301578258854189649000861123610023575135709373581276441497851255085242951675/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^17 - 4173534134064486513181825979373298883361018209950756507582455250774226084625040289011274211511533815140589179207833157486366702916907022611431995948416883160/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^16 - 1959500415234600460436305838967444686409710473130578627196494922093060203508491896179069026618513865594628960083950115155228458036465747517412445109417209176/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^15 + 1496642615019668556590913358548841205134429182074040276055753032992467909417705002717846142697381105546893846394980538514366736101217218393270987535111399056/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^14 + 856485622022899144372399615031506660213887684304114218026986283692045453422881317989357867420308259087886472044888898374633461940100832819059877052508450352/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^13 - 83999759522802655649572735853139959131363045839916265532711342950623038267764698341045015524261861600868715435930622503917438599174639886183892678881435467/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^12 - 246302691529658030054264798306295067025718367298124071856786388908745949944696994381839985547852746770783369143407461798351600778974786978143823719852132845/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^11 - 76256690589671487230515419763916095584591451055741395415365246601627842999140995193831121407931420337971802479652835439221174497982220116255565350221211674/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^10 + 31998764887458115644239491793719989063866143440592548520094455071912937644153071095671996098754645291954110208990827270793807559483006535094373048170777766/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^9 + 20308777259763580548223350229178961674500349754204256436535105204572775962184621584348268298689239193977379870744635845453446896158745954901618728853292808/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^8 + 920036472321552292295095691639303768247450252694469741715188075788312638955037059036079013566833254730903097367434720370320692645549852757350331426714160/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^7 - 182328125148452423865548810284839883863295435183214677841391396172839418744155434909340832515028243858797118980180464045254832660608211741286473455349440/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^6 - 611385968595858463144169802295507354660649316000833362018648885942717100568383912650256263088318750690570226010224595263034204411903305643867660547706398/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^5 + 57371558589623748499958874770551911511423235640267895741122603857720280174158514765825298113481712060865397287433872089453291315838252453988748986225598/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^4 + 45978942167623933248435639891998715776036598728262982779665361538468512368402051525786217889109125532645784856633761890021768366411460874314643909821218/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^3 + 2147463375749729803541274038242939512082294925436026350710562738327582809685476864081203897091841122520503592861502717047421941573343166715117344566520/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y^2 - 815941266995393946946488607449072536608042417750223674216084106731458522049667763158148762686128359553078303878325214938533550619147509555381868270875/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351*y - 66750395508397762476862938959952347212400208077420563870024773242039863974476203878948298018505536202108900662992171259738019772200960626653850954086/1605042618065094542752583384377500066525524611725576714009167302453444832371879085370767862288869832733998436018417117034960711052038797818995617351

-4859602424665214790105036893156009635109112795698190098129277240054507147933903511682055044066081182198342426696104645903426665933116434556714423396/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^39 - 66299537419722365162515493984737393962368248667628662235434396042333947971574091745683813361450570706433071352376110283835709686836663775774297790050/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^38 + 305545273177981459677778712220194908066229825261562136027236917787112865453903192178237741552374032481466925392701158364430775189059002423582826747315/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^37 + 10538574286999241121892415396135617103637953478544838919653604151416502014899095657236283328523786906742186046518585035537285069062971742998141843871780/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^36 - 20937280070526449953939293977809747069340232622148336395904008748739297384839009294210984717921237023298305621549266707170805213606878437525083550161222/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^35 + 244668949184462312277732469522330045943655897648823331078613135178382972416669671642772993042465800722675157219204846536317071327102178962566026362806900/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^34 - 492518418784852054848982645955282390522418465827831299039407153353792236761416256965884268397921026134526236362795616062808256564496399282924740512532021/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^33 + 1451001918720250282558971617401040195786806269146134413826878981378415819319132092337250140508580443845698328763011704695148594543118151538198857754129475/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^32 + 1160035297400883790853187358731836952353220750700644572839770143475699760822265578558776706153910541048144465031766627943159320051636286464828212925215730/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^31 + 120502881498109473035852440387183965777846777451324010728808232824214841906421562866953014794522060676513894672629511042639420928944535713357150582471488/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^30 + 2140835834150319332839435761870179473469294272638954611281535449300690979306403615060357142922196537888430949895625126377766107591644823807133206024646720/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^29 - 10282730777892841760425517213746472725937425935248054278858387787273506536031230270167259594145009785651881413760558845227299122604325708960978720671769305/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^28 + 9119318371508270004052836374127103211927410902939076859573116096330641742352891408410759787025982978890150546457296265167008721868794753163086999045674633/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^27 - 4336529006229201681511939627237193838664841732346612473672235431781734890950400833930456320184819585459744879290109021428898593351721372569222995362438654/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^26 - 43651984952532892574066287921247530008127440464863915350758245737892813563667415670263977421728135883345581054575998506667484228446480260872975674654545510/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^25 + 32960798429311398502545961515669216266043451976851897861814249752768071082583250993200796217382883397434880537897782803804549291506442727204054702692895869/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^24 + 115704769940288387535029558249435524985663869434351530359399257265674099890067270394540419236528145982297887851697555183415764204569356544030683004991577001/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^23 + 262338257023106973686052806337436432804023168474264893912641069451917318034760803453123348195688724371343311159720380228772158413864266628343435137765785593/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^22 - 428045489949970100473003532605903804620892987842788709471417544703445510638668384929626278415125122221669226003750366640933379584460368359948288092364470351/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^21 - 25444529685262702762092105636054556327063666139712391178336899741871480189090341910549622117632400173804586710820609338186302487541045190273511538249453738/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^20 + 783859889770033501345452709474910493599311067085662768390210892118875619619363526530085363347939293507986545804753120888899256587081747151221495380202396727/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^19 - 795460782962140318343579070874458390452657697289708339939150749217950865689204446280174246479802019155382965932254614483379263946664258904102526164123609151/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^18 - 663153475100087324201609891872830202284834662392249835949333519835199716901514949871168965698739302094297403027324474325915990489423351653111917319961911808/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^17 + 835880507837674698274820835781720523292937125796430939924305633376594795144254614579780510344807113015358321901175700398892214723097438276431814003711548906/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^16 + 369043075168024966349051298798585820454240208901473404292809471400092548630649480254026041699153801728411373476831479806787876344880696294660050665439962620/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^15 - 305788297242895439374654645059533414798945503749726308714694968373389231972598465437731391006156179562260212753549245684083335778000799319582472488058116028/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^14 - 164476788535375626653934998084743115995266085690413124401744192224448698315236492823347770279245312251075988383552620167319874550779006150654845925212848674/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^13 + 21225148650373645844847213435790306025479661976909706035430101609156150212780893855391729611461162427052019650871100006817976655382630721363216211099682879/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^12 + 49247527348530849930536449472903325525436604976078085742100256622965917936995460846950102506952827783176580043832549799234500511533658192928835960138067446/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^11 + 14140681388069421481365489787180247151836037130975670895951226451763359613202737574947102642247853893056432172971720089226245352490971652924206643275985877/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^10 - 6828961327486845679218370725361034455178276341183443751730311693152846802538295735671351236047976167671335154219023059538572560124104107976809973627424333/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^9 - 4002921813124336351175499179541182896764190420354308322874632051305189960599322902765186836451776543837023798802391129337979347105792508259321530181833940/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^8 - 102632339736994973110191194891742396256195672711522217277956917909821399390834503235952480299861661985192953809014007737576684991295443889597514276192122/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^7 + 38072776376753278731385102810306700185194756105534358168174145761536873674306545493145393147190611539899412575346313228312683919199514602180855211049086/13264815025331359857459366813037190632442352163021295157100556218623511011337843680750147622222064733338830049738984438305460421917676015033021631*y^6 + 119109630504258779711111271899929772046329234513123957793039772795203780654005695319997666560902655887270595405798700557953915047191232000820121979687720/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^5 - 13808465765293213717975152188431914627914725370924214896904863460156787353273874023716700450824270111357132276851385165154247277087943762139322337786739/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^4 - 9483912063750153041757849697955674364004336713848434852482874847771993079842298431175508928654145356517718423200143848948077793365252531537396295639073/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^3 - 384575413530496718627006941481026654602186790603524911148008378288646349820379118626893092814292531083829390668043556144819056366741960225192891930391/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y^2 + 172875740608722360687534947163229389758473025152711191676547598266060188824632912612483562889959339067162025542735510984013477558679709733646581254473/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941*y + 13712720127196588255149305299989787880597069924341737026572313599077002547374622082938294881626556499786683413217872357527411281449595697744840689054/145912965278644958432053034943409096956865873793234246728106118404858621124716280488251623844442712066727130547128828821360064641094436165363237941

-32504146006213070740689803634785059394213588751562849296968574690598051145640065254689330084757550616826397157305971680123430136452122919950440324906764015385892632615281446903682580/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^39 - 443873086531427004760002582099220964416651173934869285397211040511099275939520401242690799077344151521636474319582072614693490993588218861596261464528334204198662864097457566632362086/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^38 + 2037985025866044144105665036962051668200511801278138030057020145996048364500866225179811719788150619087176207794605748812594905420355191048859019961024652073152224451956699595914438048/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^37 + 70515347373758865735088108879249908061219630709883696963950217922932448555233256770253411380671011518101212881249252026870764698280564757937601060251277841734778547951970124541265281549/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^36 - 139134881439560438846152863562780787559996698209473716952149364792660389467388270349162146230117910624356549187727541476902966477945553740066860245252015456235480732535707436524671466635/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^35 + 1634656418747488497554005696269002910466113645431720264511716718671912311005940563204272734786166788349967479872163607189368076271841796570568894507057915121418609818266558258896438544294/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^34 - 3272996973797703708023924046256471470882119199791049850240066001058625620836250762386589879725044225493854091029861193886363010878969495467369675338980054650213802839812399704100332389996/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^33 + 9661546572691137277850011298184972353136769890316550211602187873794388946286830212758908100248925318186201214456439286938991723202738053935100341817073281069533084835610227899300997744881/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^32 + 7888451256803249745613215971025011476254567253165756281835319361016043175503246622391323211671998347619998092433790417424003514254845795399107496743739642083770636378038150396347364122676/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^31 + 895486604045109730048097619974808741799700326458469715596650722684490764890783026209198993966279371500507222059269747408091754137354768779296944366712367686250701185003603486485254703924/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^30 + 14338364445165293465466545083319494374116293693277907831733734605744170858674264042046229860664071268010708854840986412675396788455317614866661065463558103057906910684596963867332077385936/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^29 - 68584668639720233257944824475908135553747058107149527853072866305231116988005879212448157357354860786243937914484037614176440743526449538357190897333891949778410774821229661790759239613499/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^28 + 60102388045261334031815904088428682137379888027127318884801281070330090166717587831015194614016734512325139347166110090782282565828958890785300970523895170446999692931636055032174452295833/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^27 - 318210882790473173037153795333728108489762923174745622575817314218272006530038297413163586934528569005523310455015554814256643530353927025937946815549670921172552104881141353164100289008957/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^26 - 296216571405838955362310016532642750562331880685486049475383651856717589824916056717824082284196683782162522350986890656343105119912279051371714790960598004992297615759591543267603755105534/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^25 + 216986549542573453534257193528025969849038405754183374925653436549345172724380985384049961584525217921575053046053044608118470860317042440591871332647806538480291922514782213356816820183463/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^24 + 45675892276603334681884010194227251559842090076912148959606594947662236826121335667217070781633344801838969275842462206856114794877866586781302137593819021602503929300950640484470751842566/5674482748492596313341744349263567758704566589092391817511343597361802938641801029593849427363271962214218829187798690304694126293416052472776299630857174115753378463826785334937*y^23 + 1764186233253693477398343266881150006700578553123395545166626520793590421500864332863258175058937258395699661484965518048635522548639853482600232976750974357813424533561766503860870814742145/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^22 - 2840642343191496307067532250832544169405200539893591882660867118128843792544912387213177374665837543621352402592172036435159082094377277587763065402077610698180663024553108314326918290300046/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^21 - 207250355942207398373791355799637145557083863611571311974036924227765867006167535633291196866890657607147987380036310855520121796892917215669463607879691486855794559920104668421314198820191/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^20 + 5244818238110407931528501882440242076621645043951535355487474707638892431260324107286652058587360393013256028431384235224456076049232125630523925324944931882088513611929405758380623285601527/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^19 - 5256660892454012653936650516143946115300158123107057067606779359770380506193658839289051914135902697630661620598312174509359983275152966544750420310923487164990161131925015629016403890950964/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^18 - 4507056387404302455984918993233426138878811223306028989001393636436223161665575328694803313287112709620885561670939442388312464031904361187599545194291820358103532362803596677754001285289664/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^17 + 5543443401227501385987882488040187452590948453348060732365099999925321367507633252803891120910737744937459837436254159735985087331200456623551255308187217260445590784506452339032653688697951/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^16 + 2535733837929469115062556672587409461265255827698875251736862101112139592818230868793519448285980653361573076527121239969401423948568018297983105991606600131094620019762846529697280774692464/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^15 - 2021375903797120651984137450753055780040460177060461556256149358832553074801971725572577367210629712904986182663375685723505525328528122771046563481947799912000806870665569130126586795761725/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^14 - 1121237021986675560139468549183811315980302593389030811460223279926432625053224893054904820050938353123437015251637739168854285471889942223812663643834685128124611584626393472054232051796855/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^13 + 131085873748864451872859812702295643666363771640444618973138622814617222746531345840092648253533428662329678623865572999533716853223947166247126023659906222113155718155619827988713869602176/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^12 + 329859047768683090271808495074102329656089145406287218301646000516102052980076848111198390943706756210144862042234120290679773537047839933823566158383693218868260323576841915838975435052938/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^11 + 97807677155598178608249502078488756492587697363073097702708552729589343206656148825087021467904400768285508792317627031539428845933757237749005330897391847054252010513420971716136951878410/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^10 - 1939401184362985787477877994202776581832952529139028369359692241267776074362678686509135006814428294043145109429696918932474416977423816086920095034971375053395213397739917880302215715476/4194182901059745101165637127716550082520766609329159169464906137180463041604809456656323489790244493810509569399677292833904354216872734436399873640198780868165540603698058725823*y^9 - 27128014000957796159499448403917365040119672520606110664217686104939370593948057598293533906315294770893113688702376239405758966175382728345566576040387830942410739629557637199556683955671/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^8 - 914268152021352009704433003527775192713132111786585259057774677736648798747044758994471615349820792943807359330954126452266050081445120164081155023225832714920730682825072966315896698112/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^7 + 2774077761791048685487946865696071289837135312270259883201962523759915193103760885355138057009182270942932263703532115725980209963776861060898970136277162837567646864396328067794917224614/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^6 + 814441934996260554790143370404568932192135056120717804780168013456070901755622058396951955208946784125962395310462694931792997671466255410389885510526124583618373127608096742635313352063/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^5 - 85786642972498851382958770640035003328813753528617516594603235728404095501290510024375622671922755274196677762035736401268329172647983204213663466812206774022741666365131961171068902247/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^4 - 63560299688651205256624461244065783581003677437817579509037973716252939240705107097988086067872437575825910616895313858064286234732723351099636126164910704356101947759962022839564553216/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^3 - 2817851371880145809112717767855851396169384053523665360101228068017252138282558069818313608258639204891896689551359657324070822590530499455226890612597022657187290767519628839072908655/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^2 + 1140776332585030508205199751712661522696309127554069292171589379142795795028539855159498560897177569892990948325697122718309871623671670727646075863540789231115492222549352980362955760/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y + 93932677988785889436954358606964462491456265169509815413250099954740605151327579018623128278939472533393220211417451137745631098087906484165151401721065891907151720567620387910631193/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929

-345619487083186634447433293093466257063574852930101774194612398534693047419091192072495257565577672731681579377305782762714118709954799823895521766564278888579177403394020571786196/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^39 - 4736485397046560451301833287789117808062893674964033159710410668770232482328997668697636388588490688588944409135836990236752024835650588196935327245431269283506094562724655560159618/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^38 + 21443993621335296258828892571737112982283792401503716416378114105396893885593624679499645765392889295096946086504526299826803799919383136954271521531470244514910901259348522586013021/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^37 + 750880755283619709198182872178827111894821868761670725379935053982473144410994723776433374841878709227413126030815932485095181880902741132794708502936855987339547460523239031179582501/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^36 - 1443270724121969768292307218072756813986883529643129300097031568541884535221243908360935232596532638929707429161736595183478247110519952103068467654061532799331792434431833519114598092/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^35 + 17304222514273722526974827092879257645997363375754788371799908868689226770340598407045004249717335466945684978387106076820449754938846729758816089361840762882733302441004724847637279123/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^34 - 33949111969469839902806943328398778668552469406847771799998701681276636396959142667684215982433058382389855080226272849028821429731971775365439147457285428816623193682575356102774259310/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^33 + 100917337250210980980494809349766876946406081889911509270865454589284999265201865295449909266516391729704278588976425131965026515644259035902309502841005220087150849565657752290495931849/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^32 + 89112273744106496579303794405516858514501940109561414937255560712411499443152156287873209955622496293067377280183830266549728740245181693779252311332556821719606435298731090382554295397/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^31 + 12824494730856197562223130077243294261196538915789743206174236260520344182423339772174100946733326205273188009622467771252793598982515462435990648883890831239575381293465204414139949996/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^30 + 152292163901945735049689109012603681184338611714921255436950447545295482350998609835478036415600520327057630485798180739893996301484739115162957425652526622324511758583860686165852604516/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^29 - 721950219259950640887292221624099921166580637094569872421103331602295625026471392811800206670568141124305461328517354312645952266126706831373121843470283758405330136766524297615216888819/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^28 + 602558965208942291228449181198651871129400371174616775308285694540090049382180686190135591243442780353436717200479191410401958492518442667963389084779867323480988031801403444976557352582/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^27 - 3347244454087063769520306721354908143696131516087476650150903710052338552447758813087227352605524795510805305777658371299844761225152730789834247604027600057928812519259338430261266423436/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^26 - 3318354288192908378726541599825069936089082902483792713921512982963566729571423759429186168228660241587804963805551286644680853256563372355839987568214018566936244589837175304105619881545/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^25 + 2179683577897364276089750558155191794693469245303030994357558894449398136953274803967978575114912925170281643790348801867203004315048865491771621045315342795058090213159868769969753931495/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^24 + 493646496235120544301045298738846921084436905947786413388748873647602556323854870993176880521707438064941758112327265116436758079582239661068282786651267048747107975071944778975326113088/5674482748492596313341744349263567758704566589092391817511343597361802938641801029593849427363271962214218829187798690304694126293416052472776299630857174115753378463826785334937*y^23 + 19141812086898426302193459890714151846159670058371837727145518936029149253528977710363229310528379455445566200986769523795945146117842873240277338446151915000077667227867695582365223352641/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^22 - 29355390055711788498663025621257184937196907815544670954823143381426379204913333605212729936144931907358100478139844274004071791319936602313261807188271662878523905660261966347824220806756/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^21 - 3805131503094359805613126664596282886885958099910518197829599213413875424564864713895050709712415202566403950761045946779992518413389000981766664919243039966495684552361071296779258175544/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^20 + 55883669821748113494180968444038016430274709561663862407821194852513460394781510556880916193173414771731921447284429916076672478559691860971085923976533210557954069249536139553978157991532/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^19 - 53180315005779130977112533728669503860801751346654443071065022956694254254878745962749336405809877113334174525596939797346255645487210493333770482286074215373378331606994932271381001346474/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^18 - 51050462156385398273782615692696619563757138036290567238372424081081719785590830891562549313136535576704648383436695355238241540123686488909139579020044824929077829168343538802093360772915/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^17 + 57045963861749251346981789507827032027896835516455298517089027231734549017681679216912992395264663247610147068888641624356069527617263250988242119082970493417827017391171260318590417140094/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^16 + 30168369788313875441969002006491160984610962346379104935385211412639614475937917243900498602153195550896418626937133995118656817541818055635863367615846763670831282983216177692753421528331/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^15 - 20636766805870425012356519670298506520288477299577478431813129933761791938492832245350005994046173282142562977785375944481907135641924287259179298795034818905163729305398160821886334271506/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^14 - 13137685800658594319305164149909582170582559593029353008326013128937140935182303549140452681138002353489020092817040977193937203471397807721559520796826122944702422049602293517780818111225/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^13 + 983223991544649056386875951434695598458745081695785554195192400988806116004899940657165007176441975771892572537272234041974237619675147330312813290576490959205539083431184406933786521729/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^12 + 3644998505894388356861258361567397948372325572422443419843114848271286322096902997632762688183744473298299156112391521464288158525010278090123093018541456254813548046145330221531526998246/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^11 + 1195155327699363594127890525782465190685593305901116095638835238163124929475407001447415142651272017171745605727898661691159945141770744527057935962410579483286276576732876709946708753490/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^10 - 19402942688777016668834787760937176902486836951428881536299807918060356919157716986202359868248421427976077663153491842157430619579352228232154106451164599192506336537340305239830608406/4194182901059745101165637127716550082520766609329159169464906137180463041604809456656323489790244493810509569399677292833904354216872734436399873640198780868165540603698058725823*y^9 - 316836367082399378300660791919975756378716250206075624807014210747656535342733019779974649970177394952122294993015085973832828781501043452110667142480269781548716114398442811327415691361/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^8 - 19855663546052996072659742496836990883924313483521000001264788591704110483025809035568733897310739280112102275185062984072575036231561156363490727151223494435138851828799376274592945099/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^7 + 30615740288556886489865243610797260463334469251456702240241943343061720031190312287636679601409446490459026667929461581483467395465292730531807585306429864935066700740851667429045664447/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^6 + 9975930205929235413613917540844744937743779336041534083802246906947129716842962693129825714229269257186757029628116279490336266780430988273994164998206371209545463093581514658860154606/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^5 - 685848535750902435657031683771548041157665253574005665957734626697280162024481814482734842547421478953800032440904232749692535503075648239883027121866122539085682298681006613789667303/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^4 - 758743960947214060078756207423365274352881919413726270417494579423425847282155413411409904191320525322547405753690418858423592817079306175857985398784135328554856736626879851293884997/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^3 - 50646575022866375312921575973878463031090603667393969322543671933754649060375202651901054628195846797866786376951640232319972550838119261739193938469865158949574302070289214426056116/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^2 + 14013781543375993693579775646942840776520829922879796612912233919100601604876236484697104114581321204011971243336003352246620258673452239387999033744501204447573391287825308988897798/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y + 1355031728950286218048261280947283494702176599935676256902052853430256879316477859602834050584329567919250578564257892675110783801104541639775798861838857869739847992786398497590890/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929

-166316205810895851565335107836421304528237093857271711933536362862441578959570350232220841233913304201609711439607652814315397711155492253814028523020013319490521258715954489848153265/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^39 - 2271403459602058303617982994295366398516221384517213749787494686046138776007152054157414114144682771885349593743649993964211389129376288014524713334107916104643681827156612999729631321/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^38 + 5211359594166514550101061418857672835527449186414154371577914834958172601074972017707182657272076467365726653835185409706339825228245476906174826032809904582825017935943406927766335549/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^37 + 90197829616966695471273778225324324990123969100097708412963271736130472315187251611157773919241364458179818327628131706987416664628788640036892409479910097266807102010142849225294776421/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^36 - 2504681401296558655354880738167813056297726068930702713053798754858646827453742745509025751197298619542769317301208205742551508056105618151183052178149548812527974025427816144344201948/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^35 + 4184190378768909112596786799387800720247132610323332706046044001964543657420389855789624135510436192604373142377941375688883239307486873971545295974565433188992725084261378292427408607835/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^34 - 4186483626321143746755318341050018658647391084149644440319689278603123288885044990579093826987636918284339974432571729657765325986238630876353294038346311705728456890926989621968357581503/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^33 + 49532308794274742418568905489137723626244074252406183944268397605366322658847735148218066417264393626960377868145431012598801432166574689337762038148497381991940429061493261130597782263979/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^32 + 20103179844624058744127232297360099160878152405300553538675689570286618808021382385873463587802117935242534441727932397753547649875938201530135726819807852781932186339744241504664283481317/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^31 + 5311931391764203590826644574283786209473837834982379425730130186887954019057291846855001057250687977462217034619337299107418994642176148879645077874716260732740874012335035674829379362983/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^30 + 74018862599091929191362056996762958920512896566708165795424420856427349378056208528085602680314237977045278215968828553009627795591050709558898340575013774301511328609345715336255686858893/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^29 - 175284781042975685117125292421594695572321109423378774783216143647613640009379544354762730727670938538729370357438373243372610662557610959342921252670455258362440298019996714951493509129277/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^28 + 308267126424125486259139083588162736236226058984045182497774004055130823719476266666090405822382607225418287193762133417856078480898251906397605997683078082684136123046097294576891763401323/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^27 - 1632549574882885496500088129352136448637897338791727834311145122600403808973210285558624479561190523761418462813760142203465963983580991814311831752657538286687228240400259405503289633787027/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^26 - 756976855999592426970984762286819084010830843619711397204250083437904184424076595195207154563303080436639965749515607731462824473638700735760744402453280377201379789445519604639916688908451/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^25 + 542654279898113935521980810163331475182591419988551213535998049588511745246853392578804595079237445773425026461877906905894657612203657269028917366053751345023988533084253120923840926867837/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^24 + 232349485415716928434610163599232718411164703925346748049049844986183944406481044571259902028533281008495923801586119173774677417449746529010974279835391344337305525348344885253519437326459/1611553100571897352989055395190853243472096911302239276173221581650752034574271492404653237371169237268838147489334828046533131867330158902268469095163437448873959483726807035122108*y^23 + 2260034248499682836460149376122595305197521501144788220433142174257156169637414402436588153923410849549184077765103949095249398434957186911674085503219454343370088682662235117378046802743233/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^22 - 3617471422002819965703972596561786609691002834288565043879887471353800713791324073235413876642524764707430435252750554893436464344371139132277237126840313230157463219585389919933159672821694/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^21 - 235311900973607720060551125274050899577683301935857140946902743391714763584177192176911284507439415030072328744053042605250909012583035115474310969623971023105034291570377777111199695133051/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^20 + 6665089377843166953912267746522373249320106043379359483532412791042573282123520793126390505935902569496149563706859447986500874891736610045169426996148647654184181696477060402949735521633420/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^19 - 26886553476986567439313463347272709606666184513848554806905230452934206639427704458104886753413667611287835155648221215632155492958511736435616708965147480514632509062508642231437372017357583/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^18 - 11373133209203316466729117088466487696696191972795358140460567289547859179500408226646334700301609582162164543041852632626511012674519136320175722460853205179218354064725358063926632423885523/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^17 + 28009503947183027670501164454672559350061377975082194106319296975576447300044510758997404448469050915301603914108880149058448926651002113234563056433176228844852267407815646901767609656317629/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^16 + 6341851619351787478124379186422497216411317657174408348234244086248965236899182919732764802292978377512452074660862831828115276464183696717652958307016206259917019541842324053838338049756819/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^15 - 10028172365434954550176289289724139280051019616008354135772212457981827296786576518789599204282572075038473597657372588539718580289543949279078812342582189242775963276952997384443590693735521/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^14 - 5566794185853723524873337962777392142201048288113492374663944082110240918428544458032459545211176654783434387506068199877371837276550168422880267545842679821619296520081821896613424835734095/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^13 + 295937801094185128681587355960042638957226543739372794646785663851239783416817508754879822908652437082677971564218119966716095836133995893870192963457946761711779654771995339293309527785809/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^12 + 811575443822394022557872265234041266589663579695496667822544020043872929793606757793809221681415545597857330689521665010249497417883171188566046107208486639092258937250016413352399202498135/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^11 + 6911260142311839271978008076806402083972926836803674888859722107220067008608133951887948689759330650122379350288840958646719141565300585327762927449488081592427407360063805349124216781575/385864826897496549307238615749922607591910528058282643590771364620602599827642470012381761060702493430566880384770310940719200587952291568148788374898287839871229735540221402775716*y^10 - 9367481641845351545049593158465960655579038274794502058440754519326960882039454344827517508509081084114927124314637311566512344268879097227332008856252192758300210032755087796838318409091/1191147943900967608731040944271500223435897717049481204128033342959251503815765885690395871100429436242184717709508351164828836597591856579937564113816453766559013531450248678133732*y^9 - 65907736993782317495415789126178408272114892872912142190583363581566647795560970338130166459607827780124205306455280803138973720663500908288988641305939706904733525335125106041639178330859/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^8 - 1269121219656832140413145961852911257865357145399059933719309448268008672494055655191555178542900270836642572312985370936748009049300667981784920096706438708960272931484634888586464938099/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^7 + 3320112163570179020960828420285976108582750684024039752246408817733528057110311777920014938868775447134720831337827330405855568727736110852056651613002555299661411091576563883776604630439/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^6 + 3937847361901479898560031579173643259815341495872989469919495543300367984025543837482021312488620865498826815769803860399315377997999491490453830577626257758236198142570241936986792840463/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^5 - 410651132157001442500679859610477054855706967680602560531402727791288189304172010078126136604313916863987646649008590073489971312536747070547110221976009057678095987185275730296206605641/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y^4 - 150163245127104393936652813381800107277804368840478120985785677290707421034222867850382612205173731583612905917456327713737599513962610752564397687615382276782009536037463589683008294687/13698201354861127500406970859122252569512823746069033847472383444031392293881307685439552517654938516785124253659346038395531620872306350669281987308889218315428655611677859798537918*y^3 - 3322327153780093860900341851239288528594677086929904368229431752751531998737850358895516306079272988845276394355824653787147172883483119452641944971307506645630963003587798337262558726/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959*y^2 + 5386588127526993515835837278161577430248116821896411725647670252036936919127312519370821445233080503211299667161430758073957518923234140494301454477531319939304308987809831264317371583/27396402709722255000813941718244505139025647492138067694944766888062784587762615370879105035309877033570248507318692076791063241744612701338563974617778436630857311223355719597075836*y + 121208655800348459495765574405717747537479484214000231188946339861863461626958332468913829375713539721879280435394417296214327088223282120417759496959506150390910621093642808038445904/6849100677430563750203485429561126284756411873034516923736191722015696146940653842719776258827469258392562126829673019197765810436153175334640993654444609157714327805838929899268959

900948564130155200767525935280163108259693193087276423692699173559252920071647061899187836049784403535259613989133773961766334807706435392623795779659845625031495043380708632938/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^39 + 12304232015359558936901641750211182084321700482025832441369123397325543641774237313741911015439009798526518056887888160396507578349407777356399434509919609235485407867008606532672/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^38 - 56475670757962100921767897027848404752584294510759181874625084510020329930864341943006445106411523928428052613785362377101975597755106134576039203230215087092552110812113604702781/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^37 - 1954605667037710822782552962258986904984453566318500526325988055618357988744771061629636306183385332916073009421284348298024340606334894773148459701091163721651198367829150279052502/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^36 + 3854430504971928325795863009556283351652255788498323125230060828311449093907932590988005812860878877836229835643986575666626129843272781404145739722959317185708279944224479204464231/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^35 - 45304684202607928184150514158652078494978435659491729649010069286847710757209342727234543406070452715151241761062188268240855363501795797422421904074613170733915351902780397622804779/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^34 + 90670763565127858081828794499992883492700303193958389271156416065674436885266480650140380570149867062436123798105489860885103962466366378572266147136739853292496067736546506300528244/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^33 - 267688991130371689078031920976357761703192469199458873462179485198820760637219302723138869320437947675566115023514040940081529178354335551118496836611473077204607825350750086216753327/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^32 - 218963946199741812556035054345284303454235042501156598644621417229745173977038891546530541226010191967339172456087212294630309164525849913429565512886736518258238680966451310391186790/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^31 - 24992277170215294435295750231124295594951843054252340574116655486013169039213637460901954837803592149401221595453264582466358052766679243324030802350033526833453133610192060981689166/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^30 - 397404525541349190553280054353615869921375159634938647870556267890065832408402736964782686930755989517578590225634955166259992181765350412901272762304106473991764598537028178324311253/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^29 + 1900607633210565087928830327534196030578397680694616867475772447689046926206471480385441076502687827232268943490374373365812650734765149365686665397683559073337089354011447318604873201/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^28 - 1663752194907561862778270738846768101145691068070401026462542352387258074661696855139732944895462735447142812912191278938925176994986282797613872360628843954775713503462768189390999770/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^27 + 8817893100352999833215548927965099000255033648721378485243975532847405937455099951994081448738149070463725983785871999014659273249267690078045288499967324439011921013980340378283782494/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^26 + 8220485837939394270350246692848939725913453190944510882884449265990150091027391496464399443347078217229594748002341869180898352644062511261415083457291306608276197697397459954742114491/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^25 - 6007699576841722866965661547580040340757029527442183847804994363759783855863150934458720878560573356264242303854669427589781894945892126757722057089735694848895545448094988928384540748/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^24 - 1266543764527610458581467078829520427381706351329872411178612775589440676762299842852361964732994104278829317885434081610389274714864447297459073733394014674236593296733695249875717177/8703234445085784617631284115208456110541254927695053531705427474914459635001082872457771166682165657532502188181538703866266449528780120879047449038656886635603198272119021*y^23 - 48921690610724798618765972345773743105928962481609990189149258527764258108063992993500712614697775182707090037530055465018950974518042413284150432593984245944368097538632810795865877100/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^22 + 78688825152279595873890044224219202552776322178768873356035738553996860057230397240656591005095473361999142394388847110414137914819412237210845851800484462700891069061504435864948828567/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^21 + 5841839479918117866163434667646503832589288493804005545153274541981824566759167089909507683949379427300859731432362321499873275335701641505619262598642829105221397385438489283745720902/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^20 - 145388013305074212395537536556788196668575909920000425589195480497872272668667783848142597102739165098571714304598140265522229299873292040807095207304182832689612204221634550925354871599/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^19 + 145545903444774740473673900802361687916547845316396483782228526528418408475635716598263683861443094829983695276281020904330844879670185220391918886025462723474284701218410460233423502897/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^18 + 125118613402302110915767022089118570528474747757460022350050582684128791079439447780293562662062355372717549176747155959756235604343407360899152746959637772395615054780616897179164669236/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^17 - 153553129059973023210647844118439579964712820715660429751428412609095077712290185449304095744131426857301733124836987158371384230916532853279448969525011485352186474420576354341717472119/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^16 - 70480009233224042959190276233756122416940941147405874570253507241181992347667472954571070456107300948675242490245166900036432825249320094529138126754122577818486147900801577708111216850/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^15 + 55987525086493708979269748485388222352924082207106237181789614525295985372748593325412812925510898785215234470005718091907986628585062565149406604169459433678075478070762766020452529834/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^14 + 31153402732001187276261416024133004771655654628995375604585036981762250234550845093318323519141693678283467635827125552734657953848229889597421123775068002613975462617831156742963938837/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^13 - 3611531523081873189992203610340969387611541116125598807780911957008956336405550058709075522722420732136591230138420274472843734738247301726927081770152423909621951154087395241019383971/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^12 - 9152695272837618310911410086015826716471928739466553482720869834677693979166681733361382723596221712283454436788474843979641784808198385794676725281347981106641346700120410963896782101/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^11 - 2720389536153582877190183371902802301496297912872707567484803688884893310407418443935636877805021425950087010246292725628496069849131861090505192364653759981814403008913619059726939319/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^10 + 53699594151095065693690652970216697690718969007435883331229724016876243683427603724743452041302620845497533570763806232403652659795819266626376969552899193661232597131342199299268038/6432825459411232108683992606893206690400057990035474349521402916241122338913843862251396079721600703393588573873311215901153462695185306736687244941615959687184972635914059*y^9 + 753776117626335395183288598711660159671789067808610730067175279631200483346798582259639958223408236083708863284220041861749225712575820420779856265596199668854271285245100070630214458/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^8 + 25930657656539783198309974012245136099827937399264000183245647559274501772387984685138211244022478383731900456263248570017932170101556513851662814359723117075539913625601309265626098/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^7 - 76979619690561970032902210651350408678553141439074568423949270861158120661436515261152648205303514462340687237320049585736284054955708802654196870623418090981059561970256708308745157/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^6 - 22658711238966945176124702773325895981607743467193125732347472232408842480177999599025079267130697075688040988507838876159643784710721330401549886070078919948487874011571302145526496/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^5 + 2364684331264133218935739058669145298316829937998409523207423009869554744334844241400628159038400497447061476803305629553026327172100228816737351596847565101681915323662366534893820/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^4 + 1767274286382102740586112244513792640445651091760572871294631639792789813533221642849946174631816260954947010916361398526333737312684720784632510806670466228330033063540199044643267/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^3 + 79414359865559642716110604065918049236677588052821994955370032390187937135451996755285090426267900001066175743800416049918487235240668337945972451366030849085755253983091627867902/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^2 - 31740160315283891149800268211460271697562244318609136650436529070285246440158432013998428516789075881068118748896772349370993491880085663923217617652444539457662816526340054298132/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y - 2626463899820885665147195756006739010538508790747464814193120821355240984700364793420426761566812729310264873507385761181556855813193391469346626377701178792528119414774653380416/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357

26649644622924649952377411573508784298432447533444392365548517675139607653529909379406265903835391670369078520887951441980238596108465854477854026309640459212081532127138354649/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^39 + 364002223207502664632134953226331073422265489027971652002244581839831563407405756917697904052909743505651598006341432790738637029718780506960554125825909164735783307476397030904/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^38 - 1669862359257962683495448143058293784915595581635804752234337689400516395966680725879277425350775348292736868961992327766100081424032018905849947339007795260219075877938713592206/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^37 - 57819428524229686488733328377337097269101485196705976428645804147434651746970692499689053324099417111601792792096994389843828481521597253932198331419401310451851111078934241080363/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^36 + 113906855839413458331092698308303382220682681281917651505801660514606086719985521987847770952899120779366323704353318163921424859413753554184293177333135184043101445371808547075665/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^35 - 1339877120729218405920307675956139951121579495082905257302462288218354584891539642564298519268941101548831604206739989205167045052003763234737399981117946940674858263577011699539936/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^34 + 2679534239337649204195444381022184983883501606814191739857299704819992451852937450926216523869874529406699278931404005809952562978483606035855898196585712847640165513323490346134263/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^33 - 7913060188861279852644865684967409055853713665441795782403104757951817437299965203965879766758773170302770960486254028968273013398422151187123487478559483947271535439902003454100996/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^32 - 6491712917638831026822657229455516647857211444295277210636762925798585398261120015250327357064764394999520937706232054054041717194979266795744364316239418464032160830382890530218075/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^31 - 750028291013137437656071550548353311311201500915445586355720357706582875759240483996194984100743734101404164544376403987810073205157858240531229221115861969751668724099639516696598/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^30 - 11756231747929210529158952350709201855082777919493917523442257934532178073663600420118741758540785248404234380133960404443391396459882201769828928146088036572339454093774554377441778/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^29 + 56197241087451542062471007654201735706339742824073568094793502535353266872167560916609052204352938889846249768097171517338106181550100784725460167869821668646673883658807894158215788/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^28 - 49109104106807385847810218941562976462594348751982016121425358445346297773486324313215156681214224989813336504796432000843071956436570028554907293478615365064017640573533929296400414/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^27 + 260732206969628695300627496855102085972221632946371183928451174039634270933113515621944790230120100887092123841534221804670566489225494735202560302633003277015743823062644294205719114/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^26 + 243644168250998204008128683356634356199563029405832510260488330270557578397789185072574244946904273187764538368353485988290595805534730051004246737108103220861243751332808868494961297/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^25 - 177293062767371906456577356442769831503782294193582634046874578170267118582460718772668532091352078585119153051395358632170188506111179325734090035796180712365618568453908138362473325/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^24 - 37483382052749365751429118180113112339290376527244806323029495241448247871894752561344231482327555426835477273771576059712528476328600261505489699691176962749019003636262771005565002/8703234445085784617631284115208456110541254927695053531705427474914459635001082872457771166682165657532502188181538703866266449528780120879047449038656886635603198272119021*y^23 - 1448207530471814679212348939470708538088978209821857788155883645882612879471341786007601652485527534887684986471727349004964901367914352451245135357178535539474499243685852688651095549/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^22 + 2324995315880631839712185440047412910540141497444356841453824226260026642545818443448649372633537555796650179278169300756303881880494655042405890168442080412033395939403803308264852370/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^21 + 177168128925597257792577138000060047921289292734930678867919231343462490092451765091294889910366930166835920649320822297651016477587224631817855052343348225569513269690138991981280048/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^20 - 4300558022394513577451037024276768908660085468198689247448883600401727266778362621106432255663716120532077937245546471593487007601659281154692544885650804310416435567708960514798470760/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^19 + 4297461595078019157019365610844576360101364400699170063252772325981915933422124506136289752995644524721429676628132687882139313522245349263567446547998370036501679022488470503145389206/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^18 + 3709306844616349330313281175410306222455330053286058519919605670525403414655958386698109892013348750440077224847688334906887947285800345917732257468337013476337181965255764738422350545/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^17 - 4536038570573793439827762711454126317838213410024036427809711742760042325278642573567133530704308636689805048455478454200270583292957694344053577033292423105530704226477877580485030542/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^16 - 2093184066578207774108494514239377955577778358783373117319301387470732172789462731613442774554791046008218169834313399297882284591174681136467312061051557723764658374028206971078861361/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^15 + 1653033901415985959708907641139236915113665501336264862853533097004576643631145799738047504428423686984012457411745500589185172795229646153763049203190993171241073862521270061515934065/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^14 + 924471012260552559361148324922069744700661983649455147282638550202811415738482476962108474621617547114518194485769177591802641471930242433400063249102299901000244328197077886457523513/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^13 - 105472058592352449840722741209255657061530820681763010256105915821957171902303887345461331763511451703284936141532161180178712521509444428424804775665325842451264880696054012854795772/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^12 - 270939163230632100421776360462769646889853367272237027387945555425128315462607253919679948200854355643896886355411255053493523800537435366493204595045869778645089082324993177641179915/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^11 - 80889853197250301752066595732787253757792486408587945443021571813837856280786162195221536530980276260907086017319572791423400290447531319209959438341522317496680294115600880749749702/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^10 + 1583381787458331519223769262836791595119999735543607407147525793962559594215965126863067244292933781552257715850658473401811956973643141836393291450361468962618324585201784208020810/6432825459411232108683992606893206690400057990035474349521402916241122338913843862251396079721600703393588573873311215901153462695185306736687244941615959687184972635914059*y^9 + 22356893593709527717827105999562416237784354865170805928243918361580971482057800372128270333163661549929321140043905313270568713996374472867716037381077188987697027030439657300325533/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^8 + 797472329995096501262617028249695576859069085027822663073078680835644959717795806304197615762586973629191863838367492258695008104053440298821104395868258958876411697117549918470406/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^7 - 2276867445241575401336114842585434014680041525237992680477955837958088705872221809920261371411647567215957017003383911244733961345005956674793195863721693248789196580799543821814506/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^6 - 673297895729503395451268557426171049389442138412916515871083500692763128441074877693886378202979910852530953708327949134253389683647144844985284661649033417731072196278429814743849/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^5 + 69157532004912702405048388609131342147279801274780553065622224628301089972337656848505554978099332679551788040284097936395778951668511925854951351236808224811781938780775901446755/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^4 + 52407052357089627339231054177045932126697128838476391151327162203897560879345694505685926995136313150952097812458384973627627346320853529626619479443659615371520811120142414705707/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^3 + 2404010767083483021104257892211697584333641367227804061033698768321970093190025969103170355448239943177976334508225743774847819784898592739502125095098995955814789171674826649228/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y^2 - 940718397102953809268309609649822131870132120639538045725250773656651219176581546064895486297777221145739461875615098889731466465120799205992707527737942827816422389334177677664/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357*y - 78274368262409825972790985222220239269532472310791827127921211073724231321689166053982230127578697153296008275963045718211510988369300304572804270263923390465501289811377479004/147954985566458338499731829958543753879201333770815910038992267073545813795018408831782109833596816178052537199086157965726529641989262054943806633657167072805254370626023357


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

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

# nu Gluing Vector
{2, 3, 0, 3, 0, 2, 4, 0}

# f Combinatorial flattening
{6, -5, -1, 0, -5, 0, 4, 4}

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

# 1 Loop Invariant
161685032656281266395571473588897157976951601019305013308242884892113504042324385611418017763778472584858997823095041726903736749288671777597381858629582691268615878186576996693949887/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^39 + 2201236138808724717271789059821998205693283824295011499453121023411634369514139808943423312463464802114280110257911129736493281551505487516128359611917528769575126214554422661926378074/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^38 - 10231847182720679096720504132167741294269083746516793880668044751191584821259269012980187915354477460991793461753166275454024368218502411667381969571044459340920894585542553752536577097/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^37 - 350379359032289493020108207551244300741205187508891739008334650210429734023150020724819385663358949739218442003246926033387729767544298041925153075932050409797726242129972171625360998637/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^36 + 706812639270677669761672424496688089342725108521065352673232039277169121099693881402722330199539651254448871111343905105560017543816696841936234822389025203403501138893092686576867187535/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^35 - 8154306520047905981507611344422414773975690210218538304579279440783031771406995906318179042610698907209150996610335668196205945019457052335943736028784940378415241214540571701748331416142/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^34 + 16610555896468009332594559492305421742627947222790553734000742670144438085679524309691298181492671110312435095410614968457349859934304611018652027611624823318139829199774627061816885853525/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^33 - 48610022867615365528847244377146740689275473481041057482044030426816873995860915747951827247781296325517378216224761168148598795168673939307733206639037483336280134730288143425729992947797/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^32 - 37436536903247739988308688514356420211225972359118051371392301272633202624351863021051626679996255269610272124080839763633846385403339691680462643403849171929994258036524401138843539414849/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^31 - 2165093148925864686930293308125624550243751787648429635276545294650792307599774747650771649042096410289953085962303450273038071568948294996146991738953615459535852138632657726170308941644/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^30 - 70142761279471186788076936192428177681518561407748010018512911774983782979128766713651487904569464315996617252163693792223112191364004124102723177079570007671185711991319433015966416420791/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^29 + 344669122273523461392049771094104223739612797822023281399031481537968785513284642629832958511530372442252722785032370138971422611277151191109956359138921376849722322095401385218853446989704/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^28 - 311745753693046511408361329207534365533615552278021266474238527794817341208174068146929663604631480738709907047099364942847075443135097792998953420026965080801094427794607165513841732203000/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^27 + 1590551244192287767194818126051891939104704975243154894554481162394142755342381838734123064585318248436551783799642090768021664319147862101801112791901417122816871970996789341483756201158088/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^26 + 1409908885574264384702217400315378689269341396368005303627911534435099127830745244881662062666057379975660336641754328861440488960037147475544269365900806864211859247202009574112223118123176/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^25 - 1164414062213595724328636338251738147568989676746711272487897209372698681310964389255467500905214274882299901321045807257253227336400336350220119700289595617732499285884424592668433313097569/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^24 - 226718851340845842874925001618664762425884729489689922301067601403537601753037497203169807886689837308319874275808165774862679796209122614069419148174206433528524424532877571865619712096250/5674482748492596313341744349263567758704566589092391817511343597361802938641801029593849427363271962214218829187798690304694126293416052472776299630857174115753378463826785334937*y^23 - 8615439855488192504542883160264251874304883590227552704447419633430016247772725404775014882979394036219380328015391873940020796626297373165728354628535365275813253286932148248963816065894350/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^22 + 14557970094288891965764357800334965624611051586808750689971317644966943432758775183002476953870571465626410987255593524908122380585576575296240712516605148569511788748957798647180109324674654/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^21 + 617115448709328836425460170532486158376733546086041962975849498723396851486342967999186071809364191613270499436070356850931227998301541609553394609715867264395391473823606136759260626412245/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^20 - 26270732412853304608323260909138283759672638819471840854357044598076282627567499511656368157986599928336200370837852380319852294982930445390437376896392244830871051390445071574088221454669947/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^19 + 27132716250960766722891555931329500821073268070724449443357138781384681337789652118966394728716626413308728978574517320013248441606907520725861797972990044355980554899665609056446190098417187/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^18 + 21713217449853605013504948435933449257898758317957201520287850188481432696807023901835234911485051361225786201257807086939608509736235047612611034472570913308766731972429066615121584151756221/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^17 - 28724418411298094077359584250231226875624768286806964466432460316848692893670063017480049008763093957921429282490567410297874178117139939406569072687062259561505960497106805583625497509866262/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^16 - 11968217296101581780699637808070935294932648249394078457404302274445669073320080983970901956546174543091646046847206177621717096213266872429035308391131800896123661066825536816019374748260878/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^15 + 10783870396408628929915519192499717559594703173057195730962623653114679507281425243724519448205725270022546096183615482010951616078367569918177029262225808934417227095725662388231603980503055/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^14 + 5489957555991469985697960433551669711245245498920663275629196127945622297988987489996669770256598383172064999923540414427953070664020339947153239530325707194474995511607943615165880544572002/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^13 - 895256776134954565605873588087220805798118391201902042587593964736243635736864377511133999564105518802067448365472152665330861838161990557200881901374842946599997368176504327198338435810399/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^12 - 1719567194097585467785590830244254467273607107925084151845895009385348342029370220959711942399091135824407673264346919786054534632960158719942403985005412917827357442895698184211254036332592/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^11 - 456959890189954977304183670282173238486245572986922798213815088667182273723300857962247090912198779706162652658472579782852845871290259742457508595899763813216062706209580806701429824882527/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^10 + 10973869560638131930510354638771052267414187752848217758412604678387311318114999891142891561448037493412324862631926524294820546512178056307379795343871963665059696663204357803085131645139/4194182901059745101165637127716550082520766609329159169464906137180463041604809456656323489790244493810509569399677292833904354216872734436399873640198780868165540603698058725823*y^9 + 139305303991736914950029984121850438544658002356058642948175554209965473532461335469968083538259038843054191600636872396722928200316932834413014577476277194022705840308805801871806143767027/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^8 + 1469692426001254567204405442671732084768658804314782375141065026305616283270087226419970527903128270142956992110371535191751860239014744276901577103994575896813579067867331965065356595818/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^7 - 15284210663779372033346666655511673087587904585683702814199173071349992149763509487303737894182694826532963758089075684972957526898374316550027293404042911469655579722343002822820653902388/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^6 - 4164996972789916108479024407356000293689674521846469282829833508576029771995936491378105351358229073954444089274641300173609758502225386975085432194812651428827283123793255790517721093021/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^5 + 527456907591097272335433001464728140883439548581789040877490276550875940513429056422364411770693855544746261699349977202028124121470114676143566298230384044121726687366036909970223780306/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^4 + 343252601200474252376863843494207730564864949492916247019373190606128465319166495998859208581743605220677503614260520772395450626880538696636086691028333913889924388164646930982198535270/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^3 + 14126857298622275381920106132440432383773407300823625914154636313386874135566492587264012667563098949791957471802032689571520963655289265174816957879315896666580296284097436722831273754/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y^2 - 6270832254863104921507666551101163013293946193465197805804644946716534172780348467788971422773668953930652305487893240220404031235090872552486415708416978781000203903152927451252839328/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929*y - 527573239620283614694540114550554247137937230460292820967833168380360004482976842556752629614964852001797649204450776206088632289617745454586923757422956121474405774785998875004945765/96466206724374137326809653937480651897977632014570660897692841155150649956910617503095440265175623357641720096192577735179800146988072892037197093724571959967807433885055350693929

# 2 Loop Invariant
69355563849438798437907155265363979036568708786325218636302387641211537826558500400020449084610891305166279961107307165247879204459057602627064642354834445048093110397914575070628023448518655529297565292041863211155499345392099413479074394114107159385972068670905256142752156699089076371110965979496792410975281059580817402398641/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^39 + 1816676072531961731882379586688487484889908861248221477622138765346251734256150868907627963623427712196380319792739469301227472438010896194272516633955657233226433340972459616310226325261035434395407905620180532430905534721543304428819792059689138656530931722660333661415654554331830723239126801980179120797027170819299311815821593/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^38 - 9741688693744289395956367637468553397474016778518889626082824065741279911700510940542708639801028417976766632371198203669538878374142252684534518840733591245779045619575599459139647377682075550904537459928796585287442400178150665584739520717002501903391836658249601195016392306635373403455186195469757067287296259841793964352075519/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^37 - 49310591451144982089821042704455462390084365266891191524403315847337993186332734466549980480022165363784215754934937643034708356842067221327778856623840271493638245354594620426055216789182161137569607746386026106261261034728911845211497247373952110785606391445734769120376415521906960815658315177581470067371813757978382863527145963/1393514008193934014596504804220701349628498701259539706854923446200044694009224916878744865366041839839036504370157478589169243136243196471556618687365687697614071418343659190566007455552090470107885482272518368896604049905185712457533695129773753476622792174525498131621581652054124958177206314742865825101627931428623537989352128*y^36 + 5359925704664751303074666741199970228065770037942343234012801081045744859063532458580502113840210545321149802348453310004609417890942228981605870547412215296719637401597808773060380060033812766292148929022783890257654915552870985748908674037380300781970898791790824377149948157765892233652631104073212548545914255389531672436026703/58880873585659183715345273417776113364584452165896043951616483642255409606023588037130064733776415767846612860710879377007151118432811118516476845945029057645664989507478557347859469952905231131319104884754297277321297883317706160177480075905933245491103894698260484434714717692427815134248154144064753173308222454730572027719104*y^35 - 3669556690841598613009779670286974585506929378111510121943927542809486654898350908061648770153192058904752842763598129722260749574008985989648036165333320549883590551788688825519955436772454980536429554427066386442541573087671710696731708515842288096357936388596117625573106177423874650471303211437429439986606882579156196187843905897/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^34 + 2987645287383031406240047241790003650792268213071813552124423603037375690454710437188827706482593647698651870728455189359822751384647607894744354553655155928747564432680177967976459210428643944732067388947519349235025635131110708174091490363323497671453006600408364039025224071053093917554161796932201618326963051697920671474414774695/1393514008193934014596504804220701349628498701259539706854923446200044694009224916878744865366041839839036504370157478589169243136243196471556618687365687697614071418343659190566007455552090470107885482272518368896604049905185712457533695129773753476622792174525498131621581652054124958177206314742865825101627931428623537989352128*y^33 - 12439039675888560037263239644009351798652571729900270510318185655264105635985468314696349184743268613917204258697321198607102692564734162136881892298408347268845912023985268275459483785819196860435807930845208226919708657531552951228186341134313340899699269724093869829385727569302956397345587529166593865980624288394409413190560416911/2090271012290901021894757206331052024442748051889309560282385169300067041013837375318117298049062759758554756555236217883753864704364794707334928031048531546421107127515488785849011183328135705161828223408777553344906074857778568686300542694660630214934188261788247197432372478081187437265809472114298737652441897142935306984028192*y^32 - 9239908685088663163512916141632536951707278312609776034193881278407560450224161605474339165795903666968941260191238426497196530670317851970135428603727148914608064101406990593195046706323080796187303244456951181104789045221280291410627141609126207170310584601893759641989665245580234185025982948190242528480652423692121175994910189091/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^31 + 5438186890222661926925083975961521472050885442191589129059984913096859227331191828353568170593017668167147920754948252007071938126785768936192889746105135199353837934919070614562087008657510902842214884105910487463507782359423888216549596287449831642438965790335254052947930864690001704698358403765132508103249012593613026307262419605/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^30 - 63017900781612221795061149489495073355477181897019489059855511770412944797454681865734239910576933915011465547015431030527417948096808622359324379938034843188784959204897913770875353491535141760762025956735916029368327152164630591010139751898036546361891184862157308501705483862555599875384992352315498836080017889201682993904486316679/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^29 + 326254959189988790137998316453981668336519812268099476376426726051804275532025468426326943745838663652926623103688544347344910693779471420117583164808137025552520825682117032488703516147185945083961549614211790200166384638081313003022634404974491552012498809074274112203982999326212062023070417175512982672799577522851013497876111541465/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^28 - 71124105129493393711914681195443430945937497834567354667524458737522409654624936171862159267481479908255578099959322324459991251341522099057796430809537882986909180897604599471655282172236316607565095893024836683313036688906445827701945931086766870690997266006099114263048640339642041759953204470885405021452540234655250494677676669777/1393514008193934014596504804220701349628498701259539706854923446200044694009224916878744865366041839839036504370157478589169243136243196471556618687365687697614071418343659190566007455552090470107885482272518368896604049905185712457533695129773753476622792174525498131621581652054124958177206314742865825101627931428623537989352128*y^27 + 1530938497666694250412478413683185891814960922069143310598127985265970763075654111514240649490771224255122935899717771138358273024454324300994420541146074874561039170416457055249543295259019306644566570926805131364368023425663109894188116254286272678684542558829058077490052316899064889056260539506299513931975429431565464895135346656807/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^26 + 481337276435697783366763034113298186793548099435244925925024776536479500937738102213726408593974952229576779678305726598222882178563105484022927597375633307590952488142354164964207050029829028426192386436183199687906820677719819687117437934059066266135446948542260803125259026122490990890121345610196559780449447619007572328168052559311/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^25 - 186886597212635196664397385551579048093260960723087852692155538342084149318908652050984826277631258584938203894942251247584957831761398260666113129998371103726488767341239641485708604098862540199912121999465981604789200547959516039589549141123022867786374593743478649424544568827264098418665634155330309423833001658431047499873196314835/1045135506145450510947378603165526012221374025944654780141192584650033520506918687659058649024531379879277378277618108941876932352182397353667464015524265773210553563757744392924505591664067852580914111704388776672453037428889284343150271347330315107467094130894123598716186239040593718632904736057149368826220948571467653492014096*y^24 - 38955603699312564963420786282210577969304134225892556393121101562216318428316011002940800365978178416997645254060184119629716574584724702290720718023315232770772926703750396482091892534922341419451168733514966054361885449814747724559186997521894862453558396875277364972577018045006349402517826443409397705943818081169968442156003159407/122957118370053001287926894490061883790749885405253503546022657017651002412578669136359841061709574103444397444425659875514933217903811453372642825355795973318888654559734634461706540195772688538931071965222209020288592638692856981547090746744742953819658133046367482201904263416540437486224086594958749273673052773113841587295776*y^23 - 5761496020395508908419123795057095058982387263897621680493602573289339745066923654874461945059138239914258427742833030480682599099869377548164018650122666908260770903502779846790277719816557247092472401496146186927864506375288348770598227995537386120445840783850803967651139280073773965258945598983481629792257515761416838579455940437483/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^22 + 3996549768061293487842443414465365044279957901904108939253936495062379759882587371054161252199735720165281222056813134380071770459780618510678800167840096897013318935946865850080997671845776268501650627696680376661533966819424673346690450871183822271518533956301742183072448076159638460010664612559580946703416178518421375284680750541175/2090271012290901021894757206331052024442748051889309560282385169300067041013837375318117298049062759758554756555236217883753864704364794707334928031048531546421107127515488785849011183328135705161828223408777553344906074857778568686300542694660630214934188261788247197432372478081187437265809472114298737652441897142935306984028192*y^21 - 3350977384178417659215184721557145886282342368974658606066614693739026811596522230243208157617689487306232076286505467772339077493295152766960806288612927278476910812780962847978691881001947412533434577175201427551024872345607498530504958547005284189909228669765285360577037188305946376710060837412206111269814747354728863437427120525375/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^20 - 10850463050692262399463787346392531238176959418907635594508265389742716857237078125377438543839688489864237528951982380765198836004030795701654509756153077952759665720920083218099804833384012494751259289376597536618416676854463143972139972196450453834565283949089367003902254599258988028838611941839981198245503847071057408411317445376949/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^19 + 17575000138398160705262340826100391457936337416346940478085682722047850317284350151752401432941333421705526569606218720069251216593540018325860973803638599678282278702542907090536951731673018136927256401536456460078344769848915092483246327607651567298643269905222811282676620900356504300542833288113450399696667214229013686850566699102737/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^18 + 1444919011270740233770222231826219898923481383155063521370680767544083207396526255879047194951617748152424564697241249435116059394576496201196876867635547706725143941316548203967120678021340357729048204460535912189814295580824880161079651255935758702284599685397637367222102217003730020471604754981310893490261764050457466452654269185529/2787028016387868029193009608441402699256997402519079413709846892400089388018449833757489730732083679678073008740314957178338486272486392943113237374731375395228142836687318381132014911104180940215770964545036737793208099810371424915067390259547506953245584349050996263243163304108249916354412629485731650203255862857247075978704256*y^17 - 8060868372249798319718871899969122706688330647895170223606380990189137908326936286781851889603649991192083821024045724341877257375759870201767628798879533912105075681731848398182051661112868227692552308001413562529417344725079558025995225698439940267104583826011741552975639624359227281190184124192160807962602847969413383859136796016013/2090271012290901021894757206331052024442748051889309560282385169300067041013837375318117298049062759758554756555236217883753864704364794707334928031048531546421107127515488785849011183328135705161828223408777553344906074857778568686300542694660630214934188261788247197432372478081187437265809472114298737652441897142935306984028192*y^16 + 4623112782231337027604353953173074237245125483276663704193486296873449747994002115293794813411295091263015281419712666527950812294639963944752667482640738137318066254696445068468607734697194268331302719254879831146731871005940427968447418087269650797131917144025848366234837990150530279398656993379520073209888381506331137953658155723951/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^15 + 3076092770395191424615877588503681304353702465189885218491353434889944665189128414384275134952994936849261473053993030430047257287137512738482030166378410185823732994768356908948171080584826257301554091346677981329102489470374207478904660716018028556549871009104488464620528981501222434922823317010847817776547764389387738646987623386033/2090271012290901021894757206331052024442748051889309560282385169300067041013837375318117298049062759758554756555236217883753864704364794707334928031048531546421107127515488785849011183328135705161828223408777553344906074857778568686300542694660630214934188261788247197432372478081187437265809472114298737652441897142935306984028192*y^14 - 1268013630323395624139100098511523214973536141578179254095242603842644921479896629734095810648867818192932836315045381306761734044394740127067221903252116456463781061214050703702351689490676949192533091714533579013956714989333527001351344584900902092652986687876464687428819761348466088267005294457642412718177255942439778747406173278957/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^13 - 2384621663835244293338561065059193227503256175616811581254079500035931259528342811285277379837835369874520489815640565953361213773618942690834296301086406120712400771184606961017624958248089147861459530487931993290940907082755470733355213007105282349086721942173898883850775948521638987098675188494104323457015232705864010921737860326851/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^12 - 309086572951538421837780644343655602217698156689001962621076907098951010831803366128720987828500701971956649564630155897526880343761721250001873842615411707513790771172243753644102388195018102525108466887930324876109586558528339443342494869931220278391193631877836273415296062170533395422343036961974678707846652439268731264690701000321/4180542024581802043789514412662104048885496103778619120564770338600134082027674750636234596098125519517109513110472435767507729408729589414669856062097063092842214255030977571698022366656271410323656446817555106689812149715557137372601085389321260429868376523576494394864744956162374874531618944228597475304883794285870613968056384*y^11 + 292838833770182566184160452755999624698980881321709286805834862232016373031014397860645139364571872477304990302918753484889946674546918776917468853719763501388291277423148870964919109942941029189129834321395269506860879753894688968054086040846867060486459531394605451537549825014133483893260880308740898979718095424720094404141580141/7360109198207397964418159177222014170573056520737005493952060455281926200752948504641258091722051970980826607588859922125893889804101389814559605743128632205708123688434819668482433744113153891414888110594287159665162235414713270022185009488241655686387986837282560554339339711553476891781019268008094146663527806841321503464888*y^10 + 12920624533251615146631708136414131703998324222121179617466435467832847016994755164612906872880243377543645518451069006537679049320595512440344815095854169466094640681733323031518110188792745834674287103697940115656913107332792264703036206799426978986436223614519150994141158475863329756858069420825981146542314179998860771544165725317/363525393441895829894740383709748178163956182937271227875197420747837746263276065272716051834619610392792131574823690066739802557280833862145204874964962008073236022176606745365045423187501861767274473636309139712157578236135403249791398729506196559118989262919695164770847387492380423872314690802486736983033373416162662084178816*y^9 - 33737403752714927697583515381489026931863195723933133250198054071940971741208025139569382690036269690624480585297103347933788874378032443717197720736339331893774938052448493517315952961408433916959870109904169225397982481042633226130163885353704569317827804532492837562038578808222882567669995699604615101853128480972330728671712074783/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^8 - 7322090265718997583519270364396014479145290218974056208515119937649095782291992472626848010898956991545159681035752770032542825870759054114943092894777797368496207733710696353055554538624580837818379381097942123933782234557767859778938207306097887491316858408290554198065377017425303194618855856740721060483093261605439553746596357981/1393514008193934014596504804220701349628498701259539706854923446200044694009224916878744865366041839839036504370157478589169243136243196471556618687365687697614071418343659190566007455552090470107885482272518368896604049905185712457533695129773753476622792174525498131621581652054124958177206314742865825101627931428623537989352128*y^7 - 690845428059261457596624016978286833152383611532236637446917926933802029035794995650107983422050324198483965504455429110707160832955773280004075438830407084840815926437666571876391251357792948417820965914763449261395318366393073938635075480606440234076693415056051933799132733995090737712756371385181242027690797566989747488823851557/1393514008193934014596504804220701349628498701259539706854923446200044694009224916878744865366041839839036504370157478589169243136243196471556618687365687697614071418343659190566007455552090470107885482272518368896604049905185712457533695129773753476622792174525498131621581652054124958177206314742865825101627931428623537989352128*y^6 + 835078516867142882503708181566025680967089335303400178004437786105503651242781537593826264709642184579840700182473906833831058218418716928062602504152789563146741817532645743200954551607616969017135857484944330729631081712516795255260706422454080204737980395624228143264739890593782051386843367414584052635646547665326056171732869101/2090271012290901021894757206331052024442748051889309560282385169300067041013837375318117298049062759758554756555236217883753864704364794707334928031048531546421107127515488785849011183328135705161828223408777553344906074857778568686300542694660630214934188261788247197432372478081187437265809472114298737652441897142935306984028192*y^5 + 1352245371690199574865893752776353829234050667085931432794502070021232580369551992455570499502607109774477611982070989696052101963850509634152686570323393915047323061830657701369197783650079857533457604543648250529402741469277678482293921443799100989593213788859103193208345828343435246766311511861119936855821794801360895599128612885/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^4 - 194878487876968722391268960143216253783742293078983345712520072830452079306533982131069500414142357002434950641535300506247561636355434090237947638709406408352334132921934933091117316540108820631748265471564662033803561011565655557151882405158177728837642397957915511042887834674299566611175072933777566860103542905481201567499356397/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768*y^3 - 7475984618016790419887028155365199046622295758524654325988737288980660907117505424210182092803437793488825844615447019429440901347160398132447227255344806872040696494602538074233091087318175660605130788732359904148438963990041912461600323676281992112625131606728981746651734178681414193894274883932341907984503510426599612166217653/696757004096967007298252402110350674814249350629769853427461723100022347004612458439372432683020919919518252185078739294584621568121598235778309343682843848807035709171829595283003727776045235053942741136259184448302024952592856228766847564886876738311396087262749065810790826027062479088603157371432912550813965714311768994676064*y^2 + 144159355740332528794951944495270395869184228999709452944499570302984091237993134336379764246806013074747505163691501543194621707304371237549187091705066087951455056443052644121890755029984398191566847242942776700817706184323698209649282988755766228501059157409939306805342596341255633451377868032143274658483141683249711646090391/174189251024241751824563100527587668703562337657442463356865430775005586751153114609843108170755229979879563046269684823646155392030399558944577335920710962201758927292957398820750931944011308763485685284064796112075506238148214057191711891221719184577849021815687266452697706506765619772150789342858228137703491428577942248669016*y + 1501113648234832494444300627836562894594812214081170744278533013485514279257174371024827497385869547881895218813706492171136249977276677648945085128019873549960394479813046060386201434208538717428215814564783733626681661704578335398865463338080339189418161481437666007237918739971141419352730875933065293219581808063393946603582571/8361084049163604087579028825324208097770992207557238241129540677200268164055349501272469192196251039034219026220944871535015458817459178829339712124194126185684428510061955143396044733312542820647312893635110213379624299431114274745202170778642520859736753047152988789729489912324749749063237888457194950609767588571741227936112768

# 3 Loop Invariant
-25128003832787162964887369622304794956258464041610051754181054574724286499989464192273590825622316940537175069287116579318961590378346264180103517807155952032083402425625842242320948121449781457800532409568088135051722834499036596281610323701423617656035753980043367983363392605378750108646747044781645747833303057507918764258690130819000040438139089923260590182326926763623732193489573484947161268634296215285/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^39 - 687932966684544012977145141567090794213649203368132048515188218363503475613080949828569567578155356599427034042545440163824862812625677103473396352140891534378502803203270583794554646752458963015990048774836953335902954539901204312178970556983619689590453847149562885875306734587726982869189099880794682401732757243129290922298433641478758068723594815037678850157348552278987231549496460059839877020836771161319/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^38 + 3129008340338952236151426132645282024391949979346546232757426320250309445802689167088859010169067846054225526969348705830255967640900234121185239892662329386836729336016059735803456841636636744452464063191338098951808310184742206891151419050098451456987947988097651469282779273193870927813876076677922472031658242411411260812754206241632055281580622637182354167493068596535812099513438734528653668850070187781287/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^37 + 27283903478833948230088075959984961514051890369555834055857874049230194871282426432956800323546609972943279973860145441035796449243170796958263979381751089768007284655394309216731895421824650901498665774102018727643358521284521977587322253885626977019502764714899554353568431705525705382132487310955206359964458150055592600382680618240600460278523227555294117488008281249629557002719367469104630639258866838466891/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^36 - 46563288067936014511943661969919626968234456616648803172386185011260022348164888692212149608937636965279659477599487559974048775733834669949509281511274720591065674824234103291462218354696464199529668832974388594876680671034605316062588705804711893407572631379362205641293329468948128431085568224751110729374886420527739424041707828760491600469855146081058091931242783768236815548355983302865340741872545629303/627756452366351437314150111311264520115367595108411912302114687535619887525639132019183042563191392301929478819807688059137814354801594160819929213063391593480377385579148951681762292976728974896297408391424746841823761708920554286317008396593635073317017263697995146788618989223571131057082143833999711024882293348791119276471613467185180931772643461507799097356045779563060035659318380539614417305442382432*y^35 + 1259726146358686557044199279042826561433490381664952989485464288202453527216568912292111573083096941263999096444226911416940547223807803001179247530361484642721339874492770020922569400169146408451423596053711089604010149566878947980355039431022801161231163046929921002340754279396488849923447954413672264728726912217364294214526661400876688876747379271696810074134142424519772212626260303986001445419719551014045153/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^34 - 1244110412194566667607950567264595742479985020613994084274103232178632505150792806573025846291844359348062547657982270967946958336885677140762351575740611175383207596993161614290526996613913207562392962162596001181466116589779228196468718191273477029556716443663356476670148185794176782453321518404681614129824960851633679094591726749680714964217852896487103870147044124434484893583385206448151225548270925901711927/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^33 + 7375991916833421312543189807605978119846277561516826103850114773049330917060892802194984433460893596621202221699783671472022773199097706371453896580847162451513440881797310209616369455164888947197930912278304624409685108351272407065378453116626281296737843302078190808447349867921237055547370358176900350761394353197130908949296299083495157769142034692683462113685054460555322797184510272380088939515399698676805675/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^32 + 12719895890121678380726396841585761631512086132788794227780623065769707566841266361988121446659446531278236005445476563230199928593897278335457843604077589379435165110180227400333425973772621123968922904578250241958605604476017912018111991397055841570640016795906987528547432193861917237011445034101528979129122000182751267281160578060109175257791045360885388125867955394787323253781253048517266453192052297257544401/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^31 + 835145777155398424004249423859129149123454533203366291380694479321352364165513363391450426748784671360148279282147155469342068146605291923905670422038605148038430180391920255696797129322132018623689991796425354954209012330631327002244555419311574876538043984603356909688062409691984493632813807910673065371541023959477602052718890106716582393743549153067463718335650940511496672962342428335016506059701566099084575/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^30 + 22068827761530558763878464797684595220303255430956287404326045203406426652476533411382197428639581749046437034851643021552869565865633943579986171335988886082262628855017369117741781134231765417609830071581088053380280443004073853186737937514368826244901530341169606728409259448355861777124556660724607269375760887793500640577099782830319246657069602212135474259463342294302761360950670815420772130790187813591382715/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^29 - 105376894066380371791573661130387658933255845173442932929355940835917041949125718946617414323241308345659389550575682548842194149899583894036378635443676422682811734017034898419005310514123303452071955689063446336184169495617739550938155252378233609206200598661807585858461046862019186428241431714332418655633577058333806238285094186275938094320408973864156093373959508527562192925438749946541172610410866986580803919/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^28 + 5577755371240115573046401186194283560395898391037312963574345347394648119374758345842015278794028599110532542558130942825083856426968671398553957940200961242647682451907985263391911770546125721129369479832975771579816659242056410963937383764365530636844009986908626196215770488170311093075743091237029484751317337210587231348140958220219067871727613002387737916220163772410152421308168264038201810761057141604109617/178282832472043808197218631612399123712764397010788983093800571260116048057281513493447984087946355413747971984825383408795139276763652741672859896510003212548427177504478302277620491205391028870548463983164628103077948325333437417314030384632592360822032902890230621687967792939494201220211328848855917931066571311056677874517938224680591384623430743068214943649117001395909050127246420073250494514745636610688*y^27 - 488153055940798994662447515506093417160053741394257575605016053658331543633749665468554932066024661292040391127666971606284102116580567854224110211247288064536678150382255665110678925714939983617587800846261483824120391313397621436247936037684273208238494419083977979221403886183919733609845438217489060144156683614574011837733817995295402973447154365502963204944823193562864861218763131793760870188349288979293514385/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^26 - 474562192102250740632377076194353947781947947550813378955087883495573821095633347593558662391558563366057793029865728042824428796786751830227508021663861235740636359498512820026388563561390872362535361612325812883359008524903180097275915512680080608904774232137223440767328525020167482693018288489841199501309108129956174048127245981884273755991728935480378899453880928740720584628969388206693847004451351044796595725/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^25 + 81117272848083155517074938802093890331702054009328390772414635575961870244591204907320437055571220567032052768849893642116740012189004647684930408349761836188930045073888399056952898949798497731930515833038298980816681339979183251025259295545573902026692077116795208489498332340095942295900079670043668020048010411054434738397500208593504427798623360900375209376579984430484548256535197293699926072594723706488573931/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^24 + 35790774316565971177902884682862137471175303165888461589853900117774652887364226248383433221770725534755654477518532216142194804692024379701522782168942027445659605022998264107384907289513620143049448649179612677095788848271570964490392054195439434017364097076869775918478507526762329121129736311343730234771528136193052934106354634530364539972966227593925012395709359523558131020252521945467285425009967662543082153/83897803516255909739867591347011352335418539769783050867670857063584022615191300467504933688445343724116692698741356898256536130241718937257816421887060335316906907060930965777703760567242837115552218345018648519095505094274558784618367239827102287445662542536579116088455431971526682927158272399461608438148974734614907235067265046908513592763967408502689385246643294774545435353998315328588468006939123110912*y^23 + 2765920593451031554388421358791223489500240101456437012229955300821251878586462268746563478366502648209115335749347518529584399798252874484443414836495695765619981762731144375555238767475610945121897706048852848261090581295644708152232131652534815070115098172432976671323450967193740618894654103866476772607235356302279412303834819551644785439470864434048947073250081970076316310444818360374935357626656206267650281211/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^22 - 2156542353590287136326609507855232384614425604408702181363581809625226031974822898154497559359807036397318745883360473435140726446215737150386761841504190785156060322367659485097835217750553542995636596261024086671259660111011453470554792790705290472649238643244987313848833916937933631259807777732552422038044061709336259929774772639415286705424746313250035770708184786425235742272528041035236383717078065750919862895/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^21 - 122593135663344856199256292956630481156520783829925956715983847341338022509365095566310144843535754364529098440368394917059284078137340779877511673433110943923303992783819682849160717250779967395669637472490364598410707488652672893773457752984723414222151562475249957498808487445693207819512332808599720917846635633570481959402685620279396210829872694229085793754172812990938869059840351576660194563573262963862904467/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^20 + 4063074651035386654244903906223562940357414561202860642971762780658727682891951693025723994206793023038762486023048348345321315319487483090644621732160592022991317932299394880957217094810472704092012759613817964378531882426528928467266521465525299118852720446152830825481176407380558322797016990660135446468754264869312466602042217482532280032036286102233484153389166849338104518522829051147206662798932897298929493369/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^19 - 1962592511703277016209783202626330859382231885676708396054251509181517117964528644904802677802403787059205382585709708420164732497697039140943684024480242672994080762614236621969993320783738940681516580703062972472366121936783463609396797559361000666483435809036836480624124640231513994503926305783544772694746751850469562277661566379627970849939784361149102235529840401042417309365335916904174896724426703789373995559/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^18 - 7300082797485547279191593454353094408159744791434580319516763837822804239314954388653354657280444302877651942600135168690314051268193636596915246615147575283637531743341266560736032943394689235180393406983084198028863414841588943698905639076285377332668871592285079372564275469034788692700342859426914057471993245094733411978708984631268585791461636000917172342834093411743411769132536469541122950876014415720354001611/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^17 + 4195277944990722351309388881520643131254451025999013959531914326559364465863763510470716057429961340443219792276341392877145250743442512772109023027661356782510644612273371275765135398023194308114603177590931962384911960957442442282583208963938497435341955780768583297668802975866108816196315949404287516229205129337067490397337697952167619818656559477318877736569568844268111545073941560223325400930297280745587985783/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^16 + 4276789444177547636562328207133823978820416936529760538313262571234967046191068586841946643760971882412280619227863342380205494290856945551373652621331843655318246889176321630339670427813024532925559440916428084170256199847799694527948655177158511789522165619928660133175330504185290655133403326534115157475139396244416477538781793979334844164914897192853426985531894096675565587431684560798707714037743431183383740833/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^15 - 1523521998455277214692834777515852165906872925339378928081341915770546074459253598679637006746571810860026531285887679128001327369103847388708400662793847820402342070424194651887881655116785681068531301804876287066147029955585406448689446112385848311386455282625420537441014906179585405164469522519754910892991858733446634170605411626940530016766758500539323758527820386447043465309934212519395448299914817793804392011/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^14 - 1881924312436649814644327199907240356515591233790787913332692790681732583230119200242935549038100298600349649959361907039457672089611079833796420031035770239704424535708782053487058633304155437445528295652733752969301919589308685307900361803297694323877718748004332275398924064546761955638858966654281617554202702880818639109955207185577139599395514017646254926149386276282077842320735334729496467799912747873812945131/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^13 + 159250044975044225810427420118361460135700931065900180336094886781881875225395471280229899717493817734701575435753199436580551543078649270573047081718464440626013342117889544261924438787141609566199740744154262467729386945562854041607374537024400089854261028517341770051446092843675833387171514078619678760036360019814328873177984364896910608923362268064269692366986600062662770150724914433838862270998165833024635279/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^12 + 265854424226855275556502973331349509096843196046408207607905326051270920953836924145384945124480542864498645669181001439047444535760375292146813817588029989269226970321519376542654579320605530519470817008600281775630519011582433076722739843271861945183848714719988012468898284398293288677233020915431079891905518602388234642291650662651079886969142810882006912764868088385481996137609628655992327748131328436300373235/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^11 + 149754280524451220602514596418576782437037848566736443397979071492870839590943613134837531911023383869195641895432090143861222833342607281290990612063323543772895400778272278606066229246565393559322235466511083298265949640571706483415634558257927032417714155507926756170978914171767690867545793437674484832514380542603836262287890364514018582711513240650805123748389566633473440933058960802836032828117427004869633/2511025809465405749256600445245058080461470380433647649208458750142479550102556528076732170252765569207717915279230752236551257419206376643279716852253566373921509542316595806727049171906915899585189633565698987367295046835682217145268033586374540293268069054791980587154475956894284524228328575335998844099529173395164477105886453868740723727090573846031196389424183118252240142637273522158457669221769529728*y^10 - 2886450890004955934889341506724915401983517855329276275556649897269812068581781258830525857261076393343133470443314013962903219912784851350740491026182390820561484405012683696475707381679102264025339748814669463297503667471666032244860887189963537467007660069588174383643833086501869407607916269093560973789246566976985435580673260073621451136779889432402983371410802946720188705073265309230644565447732041405536183/124022839980552214398065135034712433887140450094461901282643875659211163865934965908485554148136595070433371815530701501770531670792106255076772101920002234816297166959637079845301211273315498344729366249158002158662920574144999942479325484961803381441414193314943041174238464653561183457538315720943247256394136564213341130099435286734324441477169212569193004277646609666719339218954031355304691836344790685696*y^9 - 45745039283224131012251730715522896692224387515732186319650580017878160848677361313458969959662765589029518927704510204498285897399490364026579445102539173902516406872434909645518917074569114437819844355073852047545210149766815896310635319580194956091893774291658497143432909727518269179803573410351564291922633005526805136962566564133449666630410407037899350932921201219730880145439763391303142530040520629378623545/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^8 - 341011351893073714321631860867016305683932707914347831091019226804717667615865551094298464365357392793045957828542729389117843682802350456358957537191371859360466194988866099945242989563174156021027570148569032290162352037141232222329539598594970935556958736720339216533171827391560931134150707140944841083434760916704552550582850479241644068988159771032719439318994177316158240843887120514293209352015439364668913/356565664944087616394437263224798247425528794021577966187601142520232096114563026986895968175892710827495943969650766817590278553527305483345719793020006425096854355008956604555240982410782057741096927966329256206155896650666874834628060769265184721644065805780461243375935585878988402440422657697711835862133142622113355749035876449361182769246861486136429887298234002791818100254492840146500989029491273221376*y^7 + 557885430459568894810076794326033653164083417697000814975452550538976885655759660943244960649931940869300599149300417359442208513188667944495702306818296755504554868925265638282755717695134672702219376461065180252811641243018609359233874761492725924303418754518133936991230594442771554270909195763331258417580633524085477146858304757119958661131801143717790653756896974267733579502884483752739895300859027439496545/356565664944087616394437263224798247425528794021577966187601142520232096114563026986895968175892710827495943969650766817590278553527305483345719793020006425096854355008956604555240982410782057741096927966329256206155896650666874834628060769265184721644065805780461243375935585878988402440422657697711835862133142622113355749035876449361182769246861486136429887298234002791818100254492840146500989029491273221376*y^6 + 358731785170748607068503013116181790216438276870900114370644398477413957482084523849946182421093758832563207694199424394188134548138879766967015706757025551902292231628515713052215110444211906956989730173341398505572439029105786629996320563511659507065793374299736914876312865441279010904135499048414710532938468566566409107090154364200365278241476643013137204650922449437553478025687995140159398644702322635695227/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y^5 - 100872986574504377076966520963663685482825527372174061728130093772415973028675300819785116765311904077503095547895563997703512810043559987979033442845134074910191054422948733599356274275326931132106211340290086338433281909432067236812949340129416748560007478898781202246227924617621788341573206403216749801813654889671742169722058877131706798611761413637506227693495124904584900266371514393466870499578504957886849/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^4 - 108116728225254844703289507048259628061809629724777841683158638743394327190047513363164452741001763367156352682143316642740153163862324549802379650437145199704869684288629464921527169373694057335867079085634977272412018685015207457346317022446350098554819570141736727870679338499216820648446994700771258290516852553357954316785062805731632402687248465029044247829390870107330340161834042117970789134498479908519349/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008*y^3 - 3605994529127700994296598589477300199046280752940075915451563033402596668584989065300233456024415534053724264446258140779942957116121907061508369251268195921825637166595674303570527516100428366989816012664263553624637191669645322334479779208929967044728679836563446612279496742421760748688788328361306737037742804350868092854029330984794921749957536521562970208337676434150183620840323498015368882139096067586047/1426262659776350465577749052899192989702115176086311864750404570080928384458252107947583872703570843309983775878603067270361114214109221933382879172080025700387417420035826418220963929643128230964387711865317024824623586602667499338512243077060738886576263223121844973503742343515953609761690630790847343448532570488453422996143505797444731076987445944545719549192936011167272401017971360586003956117965092885504*y^2 + 482023558435102509954926314965444146594371694050392178841994201660556742724437028830155387305798687589335311564786454691881510102416110717624907136858529212418752320644902039984577514297887367737388320624601098492659266234260612942176699044749198478619396016313316478669594172068106232854627587567158354434652654287578245050601197797235683240030708144724057768197125239962190709151626274724424804478863992452977/713131329888175232788874526449596494851057588043155932375202285040464192229126053973791936351785421654991887939301533635180557107054610966691439586040012850193708710017913209110481964821564115482193855932658512412311793301333749669256121538530369443288131611560922486751871171757976804880845315395423671724266285244226711498071752898722365538493722972272859774596468005583636200508985680293001978058982546442752*y + 223158425662902265603015032348715571050815271395205862327422784479950416859013107100162749307995507391684811570983017967286291157150429182421955617497441898332775333787157312767731472941012552024297967238566965500706370309956383494511261519573376558634750110743054477679754793820920943225920542973424868780170744782569870181616996983591753012158091970884122718582256463735207135925694355337818797991268447684041/2852525319552700931155498105798385979404230352172623729500809140161856768916504215895167745407141686619967551757206134540722228428218443866765758344160051400774834840071652836441927859286256461928775423730634049649247173205334998677024486154121477773152526446243689947007484687031907219523381261581694686897065140976906845992287011594889462153974891889091439098385872022334544802035942721172007912235930185771008

# 4 Loop Invariant
-867667025030177052307803460175598295745005508437386599281980087882838275831884523195960682656772194004156554618326868141774029479726962050251724945959686548529395425799796263248580988691517745088689083808273360694754907418428643100888888012110939725927802995906449805937254143024280100780425264872769715578627769765350938226626730258547947385806286170513663116906466738359793508324412307281854263234454788105103896636502856412064785698108807390910571704596666270679542131668682388431172786680037593704251728119239413317859758359417436484561236318959226218098343597/11434801575641865093893759677847995399652757667549696213606354363437874871906877803452755835736529285551874278710548482401115982303784749929861982111000574990090768291415134323059122114494808432694917528257709055394989022891152757084718107162126714739040011241086062404608577197781023596447072752953644521744624985820819665211998526585856250496088120120351899239813797344910170078398377958798144456108425955159612926628359917388362663315943299742910738287950583907557691123526155796182941939554865143172515354293797428721687794456409740310294233643804803403858903040*y^39 - 222132816671718007221080109573086370614557439081545246124856613089701961016065820511288574870573259192930492545279803684555488479183718130156420569931621963549476812779976111543127700487761886688123222179988986882986151140272471021235008536304198942797445890362667127542371561022804488743763825963588962373914431214910733919409252697643100487885236777814530440330454592017168226066293972395723486341260741309342857438511555768353652570987890493114980413750658323511384263198292757652851188390850719523976745710088416858408761939128477546842845527350797762910172483/214402529543284970510507993959649913743489206266556804005119144314460153848253958814739171920059924104097642725822784045020924668195964061184912164581260781064201905464033768557358539646777658113029703654832044788656044179209114195338464509289875901357000210770363670086410822458394192433382614117880834782711718484140368722724972373484804696801652252256598110746508700217065688969969586727465208552032986659242742374281748451031799937173936870179576342899073448266706708566115421178430161366653721434484662893008701788531646146057682630818016880821340063822354432*y^38 + 163253941277246838101434352144488049214138298565280814436867608513039682940239288546218224792880203637744090100886090050024906593576002570919480975946516885870914586931581992110417505417346849263718497869073360271186444530044826687814368131027229365511486202060092321338715366209661737590580222520217242697795906742119982395337584404417845019894031930044598392710335364388462427290374377835598398539075857725685495062386105294903099069531728250729961768179038878627293652619041515016585993811652727870052328022256017542327940749208226461961726275499619289120382186361/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^37 + 564639836479667182826867226350062332911963370192018921270030178886802172258393691559593608575927757475544174856606129314823232176561346598858996357951806760228542782351566210057981492931417019703450359642374244812160004415316551416754380366007475267351204427645201749196016769211910669202826523373655752514737527758974241955466065454884155916041105844695718809441321552781013153005029547464373630961005726343050008539143745953589849802486890393619423414130728574810609315468992165374025022815199182024474716636691095516229654758409688149742490676684701934961616560745/3430440472692559528168127903354398619895827300264908864081906309031362461572063341035826750720958785665562283613164544720334794691135424978958594633300172497027230487424540296917736634348442529808475258477312716618496706867345827125415432148638014421712003372325818721382573159334307078934121825886093356523387495746245899563599557975756875148826436036105569771944139203473051023519513387639443336832527786547883877988507975216508798994782989922873221486385175172267307337057846738854882581866459542951754606288139228616506338336922922093088270093141441021157670912*y^36 - 39267763368139529317140512975218733013909700538533715558914419935395235703009980570197891494637220672772242696721701885046128602272415388257472485800479912861999826410781605042040226834527059761781693587867097222033103400289542005082676318646300816932153748523632569390827242135966733625558940746133250115065379834011680372502982365829510357867202866233666886909527042152525278956558050708384892724231633827923796813119938686333790518466460340923838190719169144672971919763446486513278778946547649864310091686570315744367414820189458303327018295830134421854188838053/120790157489174631273525630399802768306191102122003833242320644684202903576481103557599533476090098086815573366660723405645591362363923414752063191313386355529127834064244376652032980082691638373537861213989884387975236157300909405824487047487254028933521245504430236668400463356841798554018374150918780159274207596698799280408435139991439265803747747750196118730427436742008838856320893930966314677201682624925488661567182225933408415309260208551873995999477999023496737220346716156862062741776744470132204446765465796355856983694469087784798242716247923280199680*y^35 + 13097521060774326819945980400214184501979670849315924270532031669460881543696820781789962320517712819381140476359525846916610437990504773575770645890455776075117476061123117136944743725317283752350058516376582639149229595915927395879604939191302759122067944535539258817379429339743003704166729870162567932969916167644275355050504502526507831826841364674365175302622348773231492324281416739335444791349438768393659881179111736116180964243653278260115692699949763943353273132881668631224910462336081529227480768768120601312086074540932146245128016941614655728197340457549/3430440472692559528168127903354398619895827300264908864081906309031362461572063341035826750720958785665562283613164544720334794691135424978958594633300172497027230487424540296917736634348442529808475258477312716618496706867345827125415432148638014421712003372325818721382573159334307078934121825886093356523387495746245899563599557975756875148826436036105569771944139203473051023519513387639443336832527786547883877988507975216508798994782989922873221486385175172267307337057846738854882581866459542951754606288139228616506338336922922093088270093141441021157670912*y^34 - 131210654338331791491916492856088192834859918920242372499521891837466409740984915482214817152765580805627501013421422754060087901408916820022819312629456277909218283467752031924086780260233363474681671219466200363446339657689279305633550415049345855828699997836184947569052680542859976513288125328730835765146254094781240224040217124404947172908641720019416121443926273966326133737302883511954140768925802830711975169012412420829111512730166965144412515564925613564179563476793287217173512323407622294734768741212589885887595055169155023547853554682828372700429761848581/17152202363462797640840639516771993099479136501324544320409531545156812307860316705179133753604793928327811418065822723601673973455677124894792973166500862485136152437122701484588683171742212649042376292386563583092483534336729135627077160743190072108560016861629093606912865796671535394670609129430466782616937478731229497817997789878784375744132180180527848859720696017365255117597566938197216684162638932739419389942539876082543994973914949614366107431925875861336536685289233694274412909332297714758773031440696143082531691684614610465441350465707205105788354560*y^33 + 17227394030976370741836543819831455697746783087813316375329046640853030542153480810916323023821482727856299648697434571525584085806484726266298215710201247573507931983187466876352776355681772903726977821115474101515101746849422060417076391947182498717766300941138869094856194729788263592148676392757872340298847412346010196974401454807714751053657852900701324234516175419940865367316499131691015366715802650359302416457818950604690879575408901184344564031138325568973103820378401548660228289607892985472036484430521396926250097371983717476424279703609151700328112046413/762320105042791006259583978523199693310183844503313080907090290895858324793791853563517055715768619036791618580703232160074398820252316661990798807400038332672717886094342288203941474299653895512994501883847270359665934859410183805647873810808447649269334082739070826973905146518734906429804850196909634782974999054721311014133235105723750033072541341356793282654253156327344671893225197253209630407228397010640861775223994492557510887729553316194049219196705593837179408235077053078862795970324342878167690286253161914779186297093982687352948909586986893590593536*y^32 + 209609395802327056482902209785075533903047191697975917007006990525441933935355322212686116780018940523394629252997098062036335284221037359352498308042124187786627702502221549819840389107043662276900016841068826104216395002510190023771898763814290672039124642598675867209008155365046149079480444720192292887348022955759461748152246497544567440620560047692883550824847290134989593169047020866822007688475453085870986396758892709183688978279552680779759431702936546914242475548164052666066884135650601472737902948553430255538992829182026597603727064271889347821410683835391/11434801575641865093893759677847995399652757667549696213606354363437874871906877803452755835736529285551874278710548482401115982303784749929861982111000574990090768291415134323059122114494808432694917528257709055394989022891152757084718107162126714739040011241086062404608577197781023596447072752953644521744624985820819665211998526585856250496088120120351899239813797344910170078398377958798144456108425955159612926628359917388362663315943299742910738287950583907557691123526155796182941939554865143172515354293797428721687794456409740310294233643804803403858903040*y^31 + 75389386493649294839500374896318284464642177632096557178120508443022921795733338092714624624914443824911844257408298611312183727963605794384114976624881996301054582196704163827515894470207468650977802346622536818644856070894882094372145238264094496125500552141516957422761346826976190865559564104937451834757309980526841426513679819064077336586261861825987611653934928169546928661728910150561263291338832465436325548066514200626488281572735568856596647640393730854211931726172306828126390828924504771001683832165313039174145867142113733276252849424663118142112643110391/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^30 + 192938505610251129901216398309290731544188460657908700994598134654409379226478049993715800563227002842217981643056150290322102779615313772912247015299741426196769978601715101672548403937652864207853146936851984475050636047900190860316210403656498450836391604005026240012986844734255967542603196307653794594200442353595402722622576828162223931995615020948710271520364015061416242480696645168804851442875510418735010755715135882370077861502908995131479856395024905128944756395638221579496082560552257140184842589262991026380612178415647225176134492556599910260816822057517/5717400787820932546946879838923997699826378833774848106803177181718937435953438901726377917868264642775937139355274241200557991151892374964930991055500287495045384145707567161529561057247404216347458764128854527697494511445576378542359053581063357369520005620543031202304288598890511798223536376476822260872312492910409832605999263292928125248044060060175949619906898672455085039199188979399072228054212977579806463314179958694181331657971649871455369143975291953778845561763077898091470969777432571586257677146898714360843897228204870155147116821902401701929451520*y^29 - 1830117795435060969700484048748863941478628349175019964648756001461777627935704002529854635289245660733315182894712751463689790540264333310060174818265192449106522842629703326849092472686930173296019680426408802439228716778713818311289363557844627575607961562409794955881886329259746406357028987103589689635042297102199655791765992164058940804936255266346243316620853226565254260682139511127064555467766487766257923095902208018955502900346791203493799455383823216150621911058908444104078825213812219193147794537822683424900427446711057412106134744561071283147894922821559/11434801575641865093893759677847995399652757667549696213606354363437874871906877803452755835736529285551874278710548482401115982303784749929861982111000574990090768291415134323059122114494808432694917528257709055394989022891152757084718107162126714739040011241086062404608577197781023596447072752953644521744624985820819665211998526585856250496088120120351899239813797344910170078398377958798144456108425955159612926628359917388362663315943299742910738287950583907557691123526155796182941939554865143172515354293797428721687794456409740310294233643804803403858903040*y^28 + 4835399229474698846080809284875290547649311155461918576982502294310304012600171427403054363662566611086456728281847830219636593975108068781137798790520215454617109458113619291532519443891903583004068297686041102883437153111210396817405083775778747049090291730523807884131040296423971864111033710465043675671131560773553080699789171090972721320241541555305864377808161698213968008304444988192666552185241967419375130123582236296500128331206269209127631531060640812858894894714296052255626839652927944332854125109878655742477476198160026874078236545587059151256361467480703/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^27 - 850982666570416676278067339677320247266913757053154682906184062037805695831636230738659202681796321126862108893346941705999138485747237911612070832387852594766033888733950634469489366192446365910949883384337246293830565089748780783298414230496311987369168420119280007667724696526995865744283184267640048508868675924157034291400369300121753835875106520275577483522073820693795841642812689263110322066711952747746906926801496767937378939084181523608953214568664064755880756655282647177891713849987576161378550425328536892162343034087297275906097458516841484721238457755949/1143480157564186509389375967784799539965275766754969621360635436343787487190687780345275583573652928555187427871054848240111598230378474992986198211100057499009076829141513432305912211449480843269491752825770905539498902289115275708471810716212671473904001124108606240460857719778102359644707275295364452174462498582081966521199852658585625049608812012035189923981379734491017007839837795879814445610842595515961292662835991738836266331594329974291073828795058390755769112352615579618294193955486514317251535429379742872168779445640974031029423364380480340385890304*y^26 - 1577500574714586973816259236026177839840838625208637023233249843636070176123859973735958103410220270267275910291559596048024062704685746195231823052987468834023354552632793002785607155996949389241472887850737946202865289858546872253059203007615461689847260704770822622441973749078271164566318591597708072586387783101149967271145820592605946553173659639635963996935598731221677437125408116194580606359883320754673170795407204550723733658211881951371682728585351836630059323640002736231456109825797468567794594618121111733666288854654870685872730051332003424083280157477087/2286960315128373018778751935569599079930551533509939242721270872687574974381375560690551167147305857110374855742109696480223196460756949985972396422200114998018153658283026864611824422898961686538983505651541811078997804578230551416943621432425342947808002248217212480921715439556204719289414550590728904348924997164163933042399705317171250099217624024070379847962759468982034015679675591759628891221685191031922585325671983477672532663188659948582147657590116781511538224705231159236588387910973028634503070858759485744337558891281948062058846728760960680771780608*y^25 + 862028018364205640688264846851455902229364516818960916997418151847515636833931140226128129426700446811705175978823713153362852676963177152759928173427171504208702806993964410756865526114750832011594561039200981687940896714742898916595788047722827372344377828530979146163667988185022098085779759214552343587083079716786662323306019023152776301727583960644232417666201989123454097752689179163556483500801793407994696371530276987874836275216200181456639123681128189379549809751152757742028566682927141397117309170202287667587874340745889309908097972942506970773935909031847/1715220236346279764084063951677199309947913650132454432040953154515681230786031670517913375360479392832781141806582272360167397345567712489479297316650086248513615243712270148458868317174221264904237629238656358309248353433672913562707716074319007210856001686162909360691286579667153539467060912943046678261693747873122949781799778987878437574413218018052784885972069601736525511759756693819721668416263893273941938994253987608254399497391494961436610743192587586133653668528923369427441290933229771475877303144069614308253169168461461046544135046570720510578835456*y^24 + 3635719213941881455050823189757886852025070885426390830770977112335246543553046486332617260124027433638644315261076839345610843638670590246880266148083742977785708859555600709357799308642261324901639470965542157166824620982608609455316832735635248063946036497620517520942595805925397059037771685560034324393261895908822498901578223138391477888441098934748874654681878959071554394290111815972319579689845252322816305418251474395627154710276159258088801667699549908410922615302915441865043790536311621424128902601560236715175488637702934643587706019813407076659069257200223/2017906160407387957745957590208469776409310176626416978871709593547860271512978435903427500424093403332683696243037967482549879230079661752328585078411866174721900286720317821716315667263789723416750152045478068599115709921968133603185548322728243777477649042544599247872101858431945340549483426991819621484345585733085823272705622338680514793427315315356217512908317178513559425599713757434966668725016345028166987052063514833240469996931170542866600874344220689569004315916380434620519165803799731148090944875376016833239022551131130642993100054789082953622159360*y^23 + 28231224989726239834452197454790483955027252992623980255278150449467874182578761776712997628754144045799718308960436652277015993974724685693403157500891326679206073788039860584611060714292440576066704550929274277485391207279290033852973563931314825507154752562225604899640252637844863296567626670403087823184046734861613778935538425379064215897868106206324245770857882515877975434277797988754153915969168156861266452681604135966507499733208191553876161484395580788315775082840851828041606544472274605335649325080504017356067450029049053874086306278227809517370937792434263/6860880945385119056336255806708797239791654600529817728163812618062724923144126682071653501441917571331124567226329089440669589382270849957917189266600344994054460974849080593835473268696885059616950516954625433236993413734691654250830864297276028843424006744651637442765146318668614157868243651772186713046774991492491799127199115951513750297652872072211139543888278406946102047039026775278886673665055573095767755977015950433017597989565979845746442972770350344534614674115693477709765163732919085903509212576278457233012676673845844186176540186282882042315341824*y^22 - 18934969756799653447423546476536712845267821993963815408772897935236023559417574818914707537143226477742889989493089254972353285989628909451687897655849620981711901014284904395118160073216470703715028829425197806585065355580285359410619982328197979973309850712866715480363072886017926169661611580786356165191515927397747706028554462618966676690039759894913093795301044645099543483277939424895689618434544954692612779661905353916849466505844703293019723292993516618055297704205501808637217897273871508799673991956554255948441337861757800498250673398877902429669550632211157/2858700393910466273473439919461998849913189416887424053401588590859468717976719450863188958934132321387968569677637120600278995575946187482465495527750143747522692072853783580764780528623702108173729382064427263848747255722788189271179526790531678684760002810271515601152144299445255899111768188238411130436156246455204916302999631646464062624022030030087974809953449336227542519599594489699536114027106488789903231657089979347090665828985824935727684571987645976889422780881538949045735484888716285793128838573449357180421948614102435077573558410951200850964725760*y^21 - 1835490123253248739568599956906071205074027425492822282292765215078301540814042970063737542334989374670869782288381202356957461752175159844844424187914319503454986003671728002849304541858868063602025168554855349069290419539372711932219127537485049009071496608087057460958246408556844570866669813273628440405251074129168288786552063604162954670898557297719895022780863191441885317314623092066773239973669670568815715606306879708969044481969149545688564980299170031830322477522540476807428014342222218233789415632788735437253020574534052333032953069972614638971425982121617/4288050590865699410210159879192998274869784125331136080102382886289203076965079176294783438401198482081952854516455680900418493363919281223698243291625215621284038109280675371147170792935553162260594073096640895773120883584182283906769290185797518027140004215407273401728216449167883848667652282357616695654234369682807374454499447469696093936033045045131962214930174004341313779399391734549304171040659733184854847485634969020635998743478737403591526857981468965334134171322308423568603227333074428689693257860174035770632922921153652616360337616426801276447088640*y^20 + 52381848967168786683728273103581993684511339240349878772602702850507190193086816575322267166560059773654756343371327376436995337785978976281073020576551673467076556149662981926617835399109106028242002786911633835838703224902840068136391893515311970491694013823712771439526026149428337641695545092065774720707262893956930346471679677661784953013226578761274939110426597461134343392993565295928534950776419232420588255654429696120877933357837044912796990916612680642897439985368233240415334580180081769301157357988056550152804208942911292747915940040652625461746203265589673/4288050590865699410210159879192998274869784125331136080102382886289203076965079176294783438401198482081952854516455680900418493363919281223698243291625215621284038109280675371147170792935553162260594073096640895773120883584182283906769290185797518027140004215407273401728216449167883848667652282357616695654234369682807374454499447469696093936033045045131962214930174004341313779399391734549304171040659733184854847485634969020635998743478737403591526857981468965334134171322308423568603227333074428689693257860174035770632922921153652616360337616426801276447088640*y^19 - 422987743590792363210733523527082885210464328675050046880236871175439163024872986780317627988529025313269979037994926701672831986840563427463897297157698390945272255027004640663634349746051392446298920679388622716356511759839783138247804033903620392567977454509412099707825306240677924790872926632040974937066905199093477113708850713267464313657688606334473270575173246076528760836312141365415505736063886675844683506025806880621175493575263502361997754526631984788543029229249562067970350137628344908112137636594491363054405444468711668075957515192166744515484720187499357/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^18 - 356711853120421112011864439902795108477876285473254654575486330132946814131090360346689131182583017906926557887944788787208920945417015454640491981917704248399098606236643359113924883014884096285157304131415894127570577120731894603698448438186929076770144371295778501331657096143681776879010441715219157721679150783612027666203451332698824723966418090349308838007401037073338441748608510602226476582342302251223312500632123078889256938233806909997451493555923269971209693960309857573887812363250607889983374026092266859294399196206157264823281413529452474552676621229594717/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^17 + 443200146428657107812572101513661838937087014983915362386214725308718631812867914786694493567474831658622663780741939347590405936541700132394784977284641079190593775233294412359835368860060813221340273296073036200535591204869767734594902693676259565621347784971113076044872057366121481954568666442131067936112345982277842504101973241452428211452921030843618342698058422482290895450652306334494385278695659653735505172295383769769746081376632900481170955604488612882333721427370621194961976439105020719999356511776703121816064868756106458438598242411615045286482518235335329/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^16 + 65747789924917358393388386194527795319421181676057416390676901502840874524188589819626888763422427950534358895362414007671327015347642423503479184921729615460079393561672173717085240960267187664459797718496661635459243969893022788639457111895601036455739727430444213035785537430120340173970717024863481764497803496677433055893893884388639169975176827761219325382027496326652874959033331017091341352894439152280102190402287906967976514257094943345470464517888297755919470898333991695379219730884285679815361347237235002838732004412563129334129084038106321885719656716679037/11434801575641865093893759677847995399652757667549696213606354363437874871906877803452755835736529285551874278710548482401115982303784749929861982111000574990090768291415134323059122114494808432694917528257709055394989022891152757084718107162126714739040011241086062404608577197781023596447072752953644521744624985820819665211998526585856250496088120120351899239813797344910170078398377958798144456108425955159612926628359917388362663315943299742910738287950583907557691123526155796182941939554865143172515354293797428721687794456409740310294233643804803403858903040*y^15 - 17820452920282927244073881113749196108612112955625994555845306602551606137849559305449650590695249319972941445514568352287752355801023959520305799298656105227758762437201760139252582518190810295456467321030386299964194829882798639690737458675260661168183967089419420232633827606321073261969865460325678066135227561397327602655764916464752380312922642678939364688128856220274755369774935967932754872389120563435931482465025472734722287807792448728237816533187187758472472760241058214570508978187643259361447642695504338815307997469886024197378091135947457050083452102830881/3811600525213955031297919892615998466550919222516565404535451454479291623968959267817585278578843095183958092903516160800371994101261583309953994037000191663363589430471711441019707371498269477564972509419236351798329674297050919028239369054042238246346670413695354134869525732593674532149024250984548173914874995273606555070666175528618750165362706706783966413271265781636723359466125986266048152036141985053204308876119972462787554438647766580970246095983527969185897041175385265394313979851621714390838451431265809573895931485469913436764744547934934467952967680*y^14 - 43143899735059422077847988970306423746693669691833566045037403081202300322957024083396854829993345857790574800441503470447286366547297462605850661689883165454141865468795076500913510907654065944936529702984451233558514538781459560734039296459301798686036882735826230740449983751140054836131074282350929095701776390513709039761752262195849336364779611961363575993059601908268680382894882816625542147153876177785240283016684258031616801921376383848950986132361794653998447517410409420753831405198958410423324483892771012077595837464445465454041075185023064251135297239240417/17152202363462797640840639516771993099479136501324544320409531545156812307860316705179133753604793928327811418065822723601673973455677124894792973166500862485136152437122701484588683171742212649042376292386563583092483534336729135627077160743190072108560016861629093606912865796671535394670609129430466782616937478731229497817997789878784375744132180180527848859720696017365255117597566938197216684162638932739419389942539876082543994973914949614366107431925875861336536685289233694274412909332297714758773031440696143082531691684614610465441350465707205105788354560*y^13 + 2069591305472425805956499494031590606471482414866348700700311709989014777552872489978248909999143078410883365129165583721911222689987968534982985669647437711470984267006440103043991160451710895397037053834888320357220786065190147797006278626082254763532121637379458565300774143163937525297566695818097963263747611576399086554348260777983800927656509512656305908682241723784666929241430624459208480821183525451791984753530630282844110828616309182051382917975410070596323660457438798723852349934824252396558716408545545091931450984172032030647172712188935105310638455342367/6860880945385119056336255806708797239791654600529817728163812618062724923144126682071653501441917571331124567226329089440669589382270849957917189266600344994054460974849080593835473268696885059616950516954625433236993413734691654250830864297276028843424006744651637442765146318668614157868243651772186713046774991492491799127199115951513750297652872072211139543888278406946102047039026775278886673665055573095767755977015950433017597989565979845746442972770350344534614674115693477709765163732919085903509212576278457233012676673845844186176540186282882042315341824*y^12 + 6362582195972578748442775727500335991294660933354050348709494523755945901777309457982030991659659518665299604906459420234510925494894467707122336994970320232061119013775124582502039538028958734299540905144648673490690113652273250810127746121941822410527601350047235584654067476704755005509967007078321739710575123681113492162637008850493603177300812657895823583872385635696518115708428749258622571036429052957337631508378172796669092991941495257901555725941828580300235094879280964992457519779190326527425674997000610986336173840339672836900572297213459134319683067965007/8576101181731398820420319758385996549739568250662272160204765772578406153930158352589566876802396964163905709032911361800836986727838562447396486583250431242568076218561350742294341585871106324521188146193281791546241767168364567813538580371595036054280008430814546803456432898335767697335304564715233391308468739365614748908998894939392187872066090090263924429860348008682627558798783469098608342081319466369709694971269938041271997486957474807183053715962937930668268342644616847137206454666148857379386515720348071541265845842307305232720675232853602552894177280*y^11 + 105641885907562410564745629378245071319420720028680182241607689642357717243658939973309083234963228343162396369825771671872331455559566639720436847194381263034519272167920030392439414718082078111427693641181832354251820687887394989512390758681582984457908335519925716605063263738552022194474335242272334906178207069395865911058349605470454841818004063163674399471623273805149391978918423817918127321532674670169894129272080774032062922492047743791711827898415200034192399016689740271722856897314268529592533320000542239705275695560658798948545417116634592563681024737611/483160629956698525094102521599211073224764408488015332969282578736811614305924414230398133904360392347262293466642893622582365449455693659008252765253545422116511336256977506608131920330766553494151444855959537551900944629203637623297948189949016115734084982017720946673601853427367194216073496603675120637096830386795197121633740559965757063214990991000784474921709746968035355425283575723865258708806730499701954646268728903733633661237040834207495983997911996093986948881386864627448250967106977880528817787061863185423427934777876351139192970864991693120798720*y^10 - 75846674593745813393770567657200837445460747332288511491101414044563055714160864873467123836587218409856060789494699664412034618619953497062591820841817144964656355365697598152492571219180625390829180398133722057927234798687397716660305043287913420071455989540251108554102753564093779110071533739136281296962154535475452331634057089434922181545364106382218167218542654731765215919329015432389857164800833196564836307849847508706489626167445168963132214947184538127451348976421258521008112671979476232635564410450288647891622685224882806809003012782381947451608846455669/745747928846208593080027805077043178238223326144545405235197023702470100341752900225179728417599736014252670350687944504420607541551179343251868398543515760223310975527073977590812311814878810827929404016807112308368849318988223288133789597530003135154783341809960591604907208550936321507417788236107251418127716466575195557304251733860190249744877399153384733031334609450663265982502910356400725398375605771279103910545212003588869346691954331059395975301125037449414638490836247577148387362273813685164044845247658394892682247157156976758319585465530656773406720*y^9 - 2048539468494094611919486426765595793387074266591111611143994316127933149528967392100662969153269827057553757990013099584693206966445325959941996437033904826040038855308030849800800989697338098989093410924155817467366179580941417744985048557925104730163773873795334971326987346234964480064270758355336567994476203337213328937009351932131140995216539329475496333756809055198673573369591450546431552183024303105141439783053487567106196015507320758428576313996417680908475572841390590649141444515711530075430552654501125926216615273986274179194494845095648224993400329864779/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^8 - 9332178924348594758324344001124179294896543009435177224009624992839188283527564084745721676610076108823859955619539667876888948179996089864708645676766987330303532470734239704368127577832979446839255588084314345881112769069074507942422013604605710915194598954965097285380019927442396674142550176148689472980527075529252857104521796337656099771157520896320814647925163438559835693333432852877242824830209284249147752936796619263377922522881970026445462676753133655009732101755252021206925403072645440564859690879793784316185852646208147056691844149746694373903621828279/5717400787820932546946879838923997699826378833774848106803177181718937435953438901726377917868264642775937139355274241200557991151892374964930991055500287495045384145707567161529561057247404216347458764128854527697494511445576378542359053581063357369520005620543031202304288598890511798223536376476822260872312492910409832605999263292928125248044060060175949619906898672455085039199188979399072228054212977579806463314179958694181331657971649871455369143975291953778845561763077898091470969777432571586257677146898714360843897228204870155147116821902401701929451520*y^7 + 17501366389657117052183440151047516652587956698856969353619025427696234524702571037828570562310588432207852947794131954423058681016562696067645499971489086550541826410318228132313714319470480801891387156568580933701139300845664358311229705732788238868465289116850401895831368945948037346383282717375657268393680990498746432036625135667175409551402020337784000746000889835735103682013986828107062330400045212470194543962821887971429768426208840179731385359083903890546038161055633452589330375211321705548130763235957759446647855130115245479442621181528959579914986701557/2858700393910466273473439919461998849913189416887424053401588590859468717976719450863188958934132321387968569677637120600278995575946187482465495527750143747522692072853783580764780528623702108173729382064427263848747255722788189271179526790531678684760002810271515601152144299445255899111768188238411130436156246455204916302999631646464062624022030030087974809953449336227542519599594489699536114027106488789903231657089979347090665828985824935727684571987645976889422780881538949045735484888716285793128838573449357180421948614102435077573558410951200850964725760*y^6 + 60150304695816581633283689188889425867895227778897066136016144170239676917508388296787762581164255544418072697291819597152127224230787067047690570787459334502160306881402300265560657056543964771401288648407827297434990454546493261888643543656062505234897508538086240470988271321782172052263297260106221518171378855135153773532351036821209130095370513692133560459361616631471412090621833241779149512642843926040163984333134645215201451403532496095046472223440342114230273406314091442583425178058627465958864528760933625779768863527128883377189876468654589552794798063961/34304404726925595281681279033543986198958273002649088640819063090313624615720633410358267507209587856655622836131645447203347946911354249789585946333001724970272304874245402969177366343484425298084752584773127166184967068673458271254154321486380144217120033723258187213825731593343070789341218258860933565233874957462458995635995579757568751488264360361055697719441392034730510235195133876394433368325277865478838779885079752165087989947829899228732214863851751722673073370578467388548825818664595429517546062881392286165063383369229220930882700931414410211576709120*y^5 - 1788026484273551264046887671315717112208814470381832774664727349494384607324974476060922088082835577339974943723688135206467589682951629671620492531866082412292498649131651163446618203091267794476646929482617872984867782025961058176001861960230720235167776043904696006060634868964455958696403551163370846952258253615097302779107774451844698120476082754453322211974218718095868693194563711965602323022247789969631566727572431569343175172144434418292798394547689890079938550436947454192353817348451573107990832758572475807507568654553197573804742953629930749005482710551/8576101181731398820420319758385996549739568250662272160204765772578406153930158352589566876802396964163905709032911361800836986727838562447396486583250431242568076218561350742294341585871106324521188146193281791546241767168364567813538580371595036054280008430814546803456432898335767697335304564715233391308468739365614748908998894939392187872066090090263924429860348008682627558798783469098608342081319466369709694971269938041271997486957474807183053715962937930668268342644616847137206454666148857379386515720348071541265845842307305232720675232853602552894177280*y^4 - 518733105562283391591874923654618586937260541699050882512424662395143341339680942640845139931395554507143639680557644389496712457865114424319723510868521637220415914152767815946401877771974322549501688995619413715790344039111201026543809951505156917301781945846107559665314281560023915784291469267550705714994419061814996795362258384943288253331853725661208312069385326525893248432406269706471798230081297488214074127580004603358026696025360511417043459909526363519693607124154159301078911989414558984667164726198679860698071385629189011608283025787399887825188752219/3811600525213955031297919892615998466550919222516565404535451454479291623968959267817585278578843095183958092903516160800371994101261583309953994037000191663363589430471711441019707371498269477564972509419236351798329674297050919028239369054042238246346670413695354134869525732593674532149024250984548173914874995273606555070666175528618750165362706706783966413271265781636723359466125986266048152036141985053204308876119972462787554438647766580970246095983527969185897041175385265394313979851621714390838451431265809573895931485469913436764744547934934467952967680*y^3 - 15125392645774296851778744058691940125713700748357261920143343194649823168339237301202058068489708738964455260377672940974065084687441764575895866375184161652728909191325814243155318626485856341179790270956279451513701244850496903685782586095550205867044176242416645107073988973370313497190576664600028487802729461238941712068309822526771123364089439462061699655613688921430724514446680156923165785003203579880413010499904487810132399657374339183609630552746651585124340285161510749516170000520567140321194035734503143702483603464877101327047389773936446661231994921/3430440472692559528168127903354398619895827300264908864081906309031362461572063341035826750720958785665562283613164544720334794691135424978958594633300172497027230487424540296917736634348442529808475258477312716618496706867345827125415432148638014421712003372325818721382573159334307078934121825886093356523387495746245899563599557975756875148826436036105569771944139203473051023519513387639443336832527786547883877988507975216508798994782989922873221486385175172267307337057846738854882581866459542951754606288139228616506338336922922093088270093141441021157670912*y^2 + 9110642082455389317034258016503010889772404306478580149652395433723250326624526404321788180245675151548176501757416544083241476470955425001692821742217606047192835352644415601704114713223789435513367990922055438532345752748964505281764590947387281265731432304367376091093262583240240999649797202245877301129202164562884826859896765176888970076830011569155728381632727441428473812258326665201643789308014839009954440604223194378006110463735210061185520787367391862416875864025001509549773835940758282612592272380863897413318991136873448491141966872115272266390959077/3811600525213955031297919892615998466550919222516565404535451454479291623968959267817585278578843095183958092903516160800371994101261583309953994037000191663363589430471711441019707371498269477564972509419236351798329674297050919028239369054042238246346670413695354134869525732593674532149024250984548173914874995273606555070666175528618750165362706706783966413271265781636723359466125986266048152036141985053204308876119972462787554438647766580970246095983527969185897041175385265394313979851621714390838451431265809573895931485469913436764744547934934467952967680*y + 1234790268473626550825030970526374345569604255162377239634910547812794259683315020149070245604155785213284362906183468844824411928165252763256681386802930290454661548365456016695904218626540113140726148321851008691259296980647038257494857288798768018373067547451310344742908683570957764679195552532860319477669447251499699235471803457507589549902070672816282299789442053056089050638453334468724103305977054695929237442564327317894004778059464733084339039079426286966008299907590179330849989836535197801130658899555905737820089029848223357464814884174790320260473003/6860880945385119056336255806708797239791654600529817728163812618062724923144126682071653501441917571331124567226329089440669589382270849957917189266600344994054460974849080593835473268696885059616950516954625433236993413734691654250830864297276028843424006744651637442765146318668614157868243651772186713046774991492491799127199115951513750297652872072211139543888278406946102047039026775278886673665055573095767755977015950433017597989565979845746442972770350344534614674115693477709765163732919085903509212576278457233012676673845844186176540186282882042315341824