# Manifold: Census Knot K8_66 # Number of Tetrahedra: 8 # Number Field x^27 + 28*x^26 - 313*x^25 - 4142*x^24 + 113887*x^23 - 711322*x^22 + 760843*x^21 + 8519037*x^20 - 18867952*x^19 - 210789380*x^18 + 816149283*x^17 + 1004570223*x^16 - 4509738342*x^15 - 814483751*x^14 + 7260338041*x^13 + 87210866*x^12 - 6637324750*x^11 - 2873327908*x^10 + 3290568006*x^9 + 1707961379*x^8 - 2551647390*x^7 - 692335733*x^6 + 650966392*x^5 + 241793854*x^4 + 54371452*x^3 - 82652920*x^2 + 8501418*x + 204057 # Approximate Field Generator -0.234025860579378 - 0.420579008026098*I # Shape Parameters 1197126143877139720985615231317254779552824142139530546934733394050300016564765498182259414638243589367435328787009306762062469235573405922104438856713544110932085611/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^26 + 4818701749683477948286400513089712994024028469013701986481844209148449479912465309618215389384988106964762155834849716823429522030667636097742254047520083033109251255/706802568288674359104540173248469973714509927700520451049794360144470511617203142281214132087303122026163311847656273918934608027448981364680397929790822846359799658409984*y^25 - 92172419793782540802116604858707679156616018843676248191156441400050223626441434064344540176097421462504994370181473379532321663972595083563314937444155129438936951003/1236904494505180128432945303184822454000392373475910789337140130252823395330105498992124731152780463545785795733398479358135564048035717388190696377133939981129649402217472*y^24 - 2511038170898231888776746975298882481578730834588851853720423271950169150452200148746559319620533760952280632350684599501734924168368428258785025182767240956066884357143/2473808989010360256865890606369644908000784746951821578674280260505646790660210997984249462305560927091571591466796958716271128096071434776381392754267879962259298804434944*y^23 + 135432812790568154071888972225747032001919573246747306510013841541300535074645976389917377388086180703711345320375400448307480938867978158102728187361404426220983031750579/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^22 - 827849832415417389292838095281436436744288033934039965966271819889098037972479544575978785403630062865274431907778769092725808353655488448677539478898372669495984524809497/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^21 + 385470287450147595522683717809669244689432073657972646790261900425209045030687446694048902366896712063965619578245658720655803890946142214303553707118030442953937533777541/2473808989010360256865890606369644908000784746951821578674280260505646790660210997984249462305560927091571591466796958716271128096071434776381392754267879962259298804434944*y^20 + 3431223329951569635748888971280243477976248835541939052945845065120763622931947139525332203718265308576524531379154516384852397992391679719541395073913894684111323125987735/1649205992673573504577260404246429938667189831301214385782853507003764527106807331989499641537040618061047727644531305810847418730714289850920928502845253308172865869623296*y^19 - 20712916404186404052682273200733268604323016522382579818862612648196871634551866934579459254477494480385507081672609660644743087172712324194156726555623310148489541477053645/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^18 - 255575149198561338036342586532490768909695346372968044193661718727324518450528562923224481292856952829037681895558861902603574567921773420452569974222166044154563753493383079/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^17 + 19391727129337985523518889799042939982541083457273330557529059561250249124637817273150260333585203199761241680379000060501931326748259572442174152950332070102887942136371553/103075374542098344036078775265401871166699364456325899111428344187735282944175458249343727596065038628815482977783206613177963670669643115682558031427828331760804116851456*y^16 + 451987919235037501347298095175509268990217303063858012608028594249381664998916329458999140037604505310791017211321098660965222539926240434154779425111468782507089411007182375/1649205992673573504577260404246429938667189831301214385782853507003764527106807331989499641537040618061047727644531305810847418730714289850920928502845253308172865869623296*y^15 - 1704143857949798411468348976029549283817115125411821317286272333698293718878590195440726893649688860182710766328896349894276877491093301496349455027301151529095922234575909509/1649205992673573504577260404246429938667189831301214385782853507003764527106807331989499641537040618061047727644531305810847418730714289850920928502845253308172865869623296*y^14 - 921184746642921449606840506194059234025641052161034666546814675119511336647607320915316152148679610502850802038131376608064148020106808248932800084772459267275888248778287947/2473808989010360256865890606369644908000784746951821578674280260505646790660210997984249462305560927091571591466796958716271128096071434776381392754267879962259298804434944*y^13 + 8142618071948613617194482023320189937528444390969809812790467631992098820868121741582666605941678942653644712899794496203513153351533925259849934625608861673653102226894819065/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^12 + 1574434384327991772000533524851010997472433181665820193545889303277527636367318645712687858345515252693676838660070215606480320292861583071595063577987315380174948911283595989/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^11 - 1061786764641179770988972123259392042372770789928744123695571654303860653912517422423086266734426324018445988547034955985562456774402890166389140289899825375324113835926122977/706802568288674359104540173248469973714509927700520451049794360144470511617203142281214132087303122026163311847656273918934608027448981364680397929790822846359799658409984*y^10 - 4760710209169691330332784861230364426417105574422493604602045850720650124722340801586557127862236579360370925993334922600597952048365969680864693522407452944497903598133536189/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^9 + 961962735045398001588004786307566096537176930662842864313798208146477316799795157387245881702713798052593448379040367125162613737945963125814694045800792955190026192804410109/1649205992673573504577260404246429938667189831301214385782853507003764527106807331989499641537040618061047727644531305810847418730714289850920928502845253308172865869623296*y^8 + 1216028283659030981404642184161532018937437706449217858544511370774798946090007840643462692237504203122633795989358703933623354144895134633123633403716489992612643414940933121/2473808989010360256865890606369644908000784746951821578674280260505646790660210997984249462305560927091571591466796958716271128096071434776381392754267879962259298804434944*y^7 - 212893079023440030590502013215139030652339203593985330157281501382383552322372744845850019751632844746982232733668905844510546011121090546132706564777143209010424156873479045/412301498168393376144315101061607484666797457825303596445713376750941131776701832997374910384260154515261931911132826452711854682678572462730232125711313327043216467405824*y^6 - 1281371764837982834791461248169041040023045360895244505713668721242443562200018707026485502102079954759391248754397918907089506735137358751999152325239548339892612831723312395/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^5 + 490048816445584504307110516854144902044706646091991178671340735086208444383971846202872694521336603469614285956954895460465922728025375106320195623399314945232390481658016123/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^4 + 346484089745753150962384276853022080010846625269313854502162768042641595364845925898130420582998554143106425208946393566925958448351991506719070454822216382545720844563298919/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^3 + 122031012312652744426935917573164146189068140911273334932205148539303605896825297284693598356915040582605113767217131306793590184267084247395589925829461227801721526501408005/4947617978020720513731781212739289816001569493903643157348560521011293581320421995968498924611121854183143182933593917432542256192142869552762785508535759924518597608869888*y^2 - 10420870554441301224376759941088278881222273793459881078488090730592803248456107773256836755765828037660936173645466384277817596017585131104022956688628506247578260589863539/706802568288674359104540173248469973714509927700520451049794360144470511617203142281214132087303122026163311847656273918934608027448981364680397929790822846359799658409984*y - 41788495907823078414919792184284237407474056892334890039585127843569927910263834702724095204932187102451347092502052612152422642761160705030863452856458123891080544171655/1649205992673573504577260404246429938667189831301214385782853507003764527106807331989499641537040618061047727644531305810847418730714289850920928502845253308172865869623296 -3304777406857280869825774648805319147114546175487018132838854055899202322883300368362676610728586232422307448079869227453809067799949079463464888864107994717875503/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^26 - 92075925602335003774126622893851871838840454435999806050070399020260773355344479964246142686612265657979814671778691909069539054205555729907444898561476444883156485/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^25 + 261597551813484791381838505310881498532657384642289407343101299495945658548405304005711846899537801202139372479725425626591771350351039645611345547413130836425166899/25242948867452655682305006187445356204089640275018587537492655719445375414900112224329076145975111500934403994559152639961950286694606477310014211778243673084278559228928*y^24 + 6761288905092653155498602747798309127398325771485552468316623681194748069704076284507551458780421455169980578998820733864802326436938598552546868823621513929402357107/50485897734905311364610012374890712408179280550037175074985311438890750829800224448658152291950223001868807989118305279923900573389212954620028423556487346168557118457856*y^23 - 377993618566559787811272382785205791611021771987175554203399999662196395310978329496969397971866869904496105257426766426484460869081122015908319870225827647414534924599/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^22 + 2406119929696315536941888726621525472964571259308486080010560844692455582829568303017714163396693025051464423693164570315430260649632439937734050669467065035130691633133/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^21 - 1468121419209258407726198179615955133783370464083000279009720942203797717567872925147504332246684670297083018417769754548583770553608316932899100485480692422220599356129/50485897734905311364610012374890712408179280550037175074985311438890750829800224448658152291950223001868807989118305279923900573389212954620028423556487346168557118457856*y^20 - 9049873430101898942927147046369411735657161612208759035102515244620704326954859730830292372578664440681758985597944601899020724814363774120167002284673653762378777291355/33657265156603540909740008249927141605452853700024783383323540959260500553200149632438768194633482001245871992745536853282600382259475303080018949037658230779038078971904*y^19 + 65142945480292936935145299807174169196937600193966962354843886675262100225654408437728374777638978021723978851461400370690079069598157392955941982337962748746918989374769/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^18 + 681861049802842094031316913988574916097052109024531445038079439544208134871198858424804196783469683419739147034228072634307223122469156258637574645848982528923143538873979/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^17 - 115582458822898198927647674327369429758314192248317038239873803876213242419011053193341318940009640368029391367456745194638289307240301560908310495413567050678757801737297/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^16 - 929216610516245241617444767547272987869779811782012126136497174502769647856979919101075261832755759492440786189181656777984981951301528878419473471914167593132708430542787/33657265156603540909740008249927141605452853700024783383323540959260500553200149632438768194633482001245871992745536853282600382259475303080018949037658230779038078971904*y^15 + 4860477304656694559627591007279348961687830858567713797879605859554127140414063829826046854190515678121524866891415401271696980226705010264886839696745669019028701232929073/33657265156603540909740008249927141605452853700024783383323540959260500553200149632438768194633482001245871992745536853282600382259475303080018949037658230779038078971904*y^14 + 193232200311452731719096566870661846856392532039683678138763013724584991687410582148785553658031816291897998161070186681127905393305273063662932314161157802630555240699315/50485897734905311364610012374890712408179280550037175074985311438890750829800224448658152291950223001868807989118305279923900573389212954620028423556487346168557118457856*y^13 - 20621011279222636995504318211959311744987330667273618983789347308805432437859909428468900785906630925908093956333023895560973169565546384981784770899961488915891075855112445/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^12 + 952928493847339709093524342728715188366177944833389130429947864564493866495727029490178595541133535202388011032724599432392177873985423058044417515751756235777423003942111/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^11 + 18175641103058295998467124174852389875223068879883031395526426972051514685506773876960719202143619248056346535321545039357698291712505409232044748915518161517392851482195715/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^10 + 8906792101060172881348926551359908596617630664913617109270267525495045658704335011394206071460780475328135289142737141530532902796102547133281586652556513055259546033059433/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^9 - 3087498931484432308494439367122416120260073449663991037349510463675958464580430744298112590701449273140620288386716024629021219911662357457825029275202051595876168689751537/33657265156603540909740008249927141605452853700024783383323540959260500553200149632438768194633482001245871992745536853282600382259475303080018949037658230779038078971904*y^8 - 1823113727705712508551981346955852628906634472330462817807810646430038475520701601075983222357586387824832988032663675365990539703658219589623322721939167822421263787369269/50485897734905311364610012374890712408179280550037175074985311438890750829800224448658152291950223001868807989118305279923900573389212954620028423556487346168557118457856*y^7 + 568365771747683879870410861330898368564916049168468587523912107521436710476697085483416665416239848990368692196243169124609347972790727898243809921014604186808185914939393/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^6 + 1733432699941858493131125191007197887719481984089479269196237654191481382875856263720023994214764053631741803804053323877256483197167182400492960136957664609853532709801391/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^5 - 1205544178656390260464789631772386719664117214295267582203335816566530262574149283323016502155744204020587962336671902998015091595658494537538244679313898506576315719805095/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^4 - 823989787263442555156192337958491395342164077759381343131691793462329836949504960165063731824288575836696639536632899490720397563641830731969627177530398695903531024176971/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^3 - 78311668281399574812096017971262271204605124328621915963244965057175964308365003562101235190240187259794050236563759198011170177136989709973396302354668481588557250183625/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y^2 + 144233182362831802366873876962334625334886847569830094038852198582637859316650082470999542457121117215930945020629490042773838416091633672440585974900841760034592971798497/100971795469810622729220024749781424816358561100074350149970622877781501659600448897316304583900446003737615978236610559847801146778425909240056847112974692337114236915712*y + 6042561742553195563086554255445066025941029325019325201511930389824658736670639810517157330684177194156232922557136864240365705783907928252993418852024846736296915991539/33657265156603540909740008249927141605452853700024783383323540959260500553200149632438768194633482001245871992745536853282600382259475303080018949037658230779038078971904 -305368336358328894605755860035862570416956050571507090896633589939715274718659147076208039833814475202317825458359971758546647204414866012381045477082883470076119219315/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^26 - 1173804843705576414587247973411905925160059508518635606630517680408983801382224070262425847143565262230878545749718815629617967659075095601925320250463974781569827608129/1102788707172404168792858805310925276488064114694737033750441650415410115750741202744264349589214696141321307310305701382017722174827273174242590869956131346032877417034177536*y^25 + 3270899023441802866772277209883889290503084819814016405274835126440313807700023925975772074312493159946363682796074481696802665375936217168856768209173515375945041407747/241235029693963411923437863661764904231764025089473726132909111028370962820474638100307826472640714780914035974129372177316376725743466006865566752802903731944691934976226336*y^24 + 576748645226486324906646937393408608203674720276574649067169644100617339196724304307615329056324619360884108860549859220805934713645903822516002759598137417725933638428129/3859760475103414590775005818588238467708224401431579618126545776453935405127594209604925223562251436494624575586069954837062027611895456109849068044846459711115070959619621376*y^23 - 36073649241422757275549687331686119595754436237464428954227679814045292255890115763061936091649102172445269348315219940169508656154518585813441765353811745611479317178399123/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^22 + 256193796227137173499383144557158886995952414814652492186635876651315486150498542138068604806174714565786600453188755280874732281402843906576476565741479837151322987582975947/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^21 - 249784921495823296586865645903483450073412598747780991909488847148152347669126247185949540049155944623612811973819269888838966098302974824896768356280142479730903107350232501/3859760475103414590775005818588238467708224401431579618126545776453935405127594209604925223562251436494624575586069954837062027611895456109849068044846459711115070959619621376*y^20 - 713159867684314341981054209455165627077117586168103883371317727028785680430358401848710529280585957359476930024607018513104606914880515603841254203566469017726487892419627579/2573173650068943060516670545725492311805482934287719745417697184302623603418396139736616815708167624329749717057379969891374685074596970739899378696564306474076713973079747584*y^19 + 8223585839590453468563534695727101361294412452226187807350538976913987698774589210048185443818087386302421892917391546098527928166637277441060743000467637698789788328161807463/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^18 + 56238946658538064207497620205855487117680324077530909209396571626773718174443568847021796849215496651290105891723628561471124899416261487796792080144636016622701479190807884447/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^17 - 52180313047461457461885955628311858305232025292919402665312907847908531207801196993071280620745486466255422700989032264347656013354425502431038248579338885587612249764264955455/1286586825034471530258335272862746155902741467143859872708848592151311801709198069868308407854083812164874858528689984945687342537298485369949689348282153237038356986539873792*y^16 + 4483341924847352857419293628722548039732840430982553489947047068281140323944626640005546737669361095038846905548816016725203660355040509326009149601377785728449529146520599343/2573173650068943060516670545725492311805482934287719745417697184302623603418396139736616815708167624329749717057379969891374685074596970739899378696564306474076713973079747584*y^15 + 486968451061599335413478511645348350957758439284416672349118028433150423110398487996990625494804161043268376736641731515848963333514172200650096396251666654193898137817047589577/2573173650068943060516670545725492311805482934287719745417697184302623603418396139736616815708167624329749717057379969891374685074596970739899378696564306474076713973079747584*y^14 - 160812231107546511452482557842788969678075308616479452339700975892727978870633974176199805779944995451909365263101909149390451547100865874691749927953459022715573678655130051049/964940118775853647693751454647059616927056100357894904531636444113483851281898552401231305890562859123656143896517488709265506902973864027462267011211614927778767739904905344*y^13 - 1301417093498747628963589306812007247617496943570634420820986681280262665423073518352179224194121396001655187415607216411004144511631333013197244916912232620959402960094300681431/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^12 + 1532614022456440106042137738806532587406569015067287984321942888563917564884480325617848956164563700881389326844300480696196518200082879933727256130214153425502478515014073187055/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^11 + 133129586207187670096170774163156215988936427119750411697392523601140257872104790934739987909311404738758511451508939469151356550532981777670244187700307749233390909636495369431/1102788707172404168792858805310925276488064114694737033750441650415410115750741202744264349589214696141321307310305701382017722174827273174242590869956131346032877417034177536*y^10 - 315861117029065232469188451706633025948565427870648004627348574480510998706228972624350558789981409128840641556777560680047409278341733296649643885502873055288642066832553297127/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^9 - 379106095338049298165358272882220938110443344510876338215369856784631976314472839604629165094210205847221184850450906444221239684544465113697023940409752555725838429744331403307/2573173650068943060516670545725492311805482934287719745417697184302623603418396139736616815708167624329749717057379969891374685074596970739899378696564306474076713973079747584*y^8 + 265209352857029201122055124070542943048036850691463647668915636021039811904829579130210545489835647475175626850443441530097746421126363818874712216115013207709583145697739622509/3859760475103414590775005818588238467708224401431579618126545776453935405127594209604925223562251436494624575586069954837062027611895456109849068044846459711115070959619621376*y^7 + 42393526976726581492083559617367028532372234935564266812484920042006131388052103723092944687781437606556558630833343021044769092547307207494761691439147524309579060407200912829/643293412517235765129167636431373077951370733571929936354424296075655900854599034934154203927041906082437429264344992472843671268649242684974844674141076618519178493269936896*y^6 - 331469109285937846532132999071466015698748397327451908600940064145849657798825022905316839046931663010908396389624950153224439453193232595574051742808581096998313772808850859925/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^5 - 29267491732312858861177774030901027202397998006157254563081611598569066032879031902486955257452154074321824593409390297413651483204180734258374120782924213813856632812263170349/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^4 - 44910204401578258342704029790191892865648472080989685108854011121046952541482344395207426860106414846656990898247478375003244047976945578438876416355107350892356058455782732323/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^3 + 60412141899241435358323140264454963810327651850852262525026854009122853064251750955530619320016693841087150342674898772925246201356207610551915487947028480682622315433952722225/7719520950206829181550011637176476935416448802863159236253091552907870810255188419209850447124502872989249151172139909674124055223790912219698136089692919422230141919239242752*y^2 - 682515585042085619185758389926217942483164321152055153243594820520651754553006917739603895219211888776516137337741978562508658944559831644709605223485221497391243665982547765/1102788707172404168792858805310925276488064114694737033750441650415410115750741202744264349589214696141321307310305701382017722174827273174242590869956131346032877417034177536*y + 8933720910698925763261479345189076523841643593094251287809338469154728504845706687520226817787023068423827802821176028509494999450541158832422989742380029118266860861941355/32571818355303076715400892983866991288676999168198984119211356763324349410359444806792617920356552206705692620979493289764236519931607224555688337931193752836414100925060096 3021997794604388238367528905322886954562569204599219861494880535100285831210057629654523229864009419763630341183916098860511035696046123249177017510265924219064811/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^26 + 87117993926293803433227752209881794422602969138123506637757273327128376855674926250937195125676843027771849553419849083082173479841136522961109248537922228934877895/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^25 - 54782214707720497416698753574948070991854075636513983911300341845860342556847691637879873666607437207478937963087755736710358120951263998473500190155871946169973677/525894768071930326714687628905111587585200839062887240364430327488445321143752338006855753041148156269466749886649013332540630972804301610625296078713409855922469983936*y^24 - 6659243219492617604217870445170466828833631596824990316599440268773808687298851342271377964861898064541949298826282410771314110899651526197716159311176121136247900385/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^23 + 334045936803716318264557072138021767124808790853627190704781916787011848744069158307042831262837239883962702728567806205847170923705413505510264075810646479830730255915/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^22 - 1862157060977018379803003165128307641595869076621384280215327097175296203273560660965131423888729293541924788648849079225599921647077150598023061911109274045018481803259/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^21 + 218599666278196768741873163822169535634771526328403358069400781856224037033474767105047877104834794451426223463588164625563945194202816318146105531333713867521752844317/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^20 + 28257451196015970299299651882219739344777942209533257831751975445374954524899648978698232242599704977091826720352552042965345769444601799112111517954714443948396602657737/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^19 - 37052797650944548228806625551877906937617760565818259540529946217420528546424872833295538315980272643866197391328535640838364227387776586704942744774821584323364053738071/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^18 - 688632404746672346724892646586350468047054590093184422106296677664851987281222105341990009740487396122999161023355174464923384385974996753660596331536390488738124711106231/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^17 + 979772078291362125877496411748984491760653371702774127027959302669046552148449545617735475604215317486931076922535782251095451370504515982526324287596918351643389098738401/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^16 + 5197528643624026608800173142879613571197644828032138455597298423375087591938109416730257506331017240149334816370690899657747950361070500617318543021187679285727155346557811/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^15 - 11872421552345691669558363428327465762816270168345471360474075269855238734845754541482091222095163223693113817385503847071020170167755090531461857734434900916364658417886787/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^14 - 840220114090590303255207947845630443095121403708073353315698785619129355776692890813667128169198617840360505777944299220611424448069334802039379373402812906107071146402177/525894768071930326714687628905111587585200839062887240364430327488445321143752338006855753041148156269466749886649013332540630972804301610625296078713409855922469983936*y^13 + 23244191947266079878249549221704845239499916724129446013529929218101663778582096499961646820466343997329546574253517658026717626629802461748340126141549130342880018312638839/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^12 + 14213292568803254148351936205723280149933078607061329720637679353293073105757540560610462369680991677724013320690513478467024207854843698639379153532330263543548936321609961/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^11 - 21921075572612932141546178396713892849574016306318843740134885186565905163071349495393766263807106038271065777407784772362406687530783995889123285995390050180362003012170273/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^10 - 20415114590933590663287986334531976450550511154524703823973366842566525358933064828381473323008069503872556273672037248718393504563426911998579379104334121966002799047674033/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^9 + 3811394777245819663520022199205692739275493126736436144131764082739932771391015363917515421204144355713398154711478949654056034644799371644129145056823574257505777258735489/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^8 + 5770959610515590187838277376821436470024114778951444953380613272569901918984052364049698338810748466766508414117432065152737418579401951744794842448930621898445904815231619/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^7 - 1495812892293591826536944025092138170695327546905062518844968896634868062116071736358854477582087457444437913343886745544592050807231906528388034028291178315298811692674127/2103579072287721306858750515620446350340803356251548961457721309953781284575009352027423012164592625077866999546596053330162523891217206442501184314853639423689879935744*y^6 - 6237443614878250842772039380034605102785008931650249982860436122090036166497741393281940969473733611585868676848619477072107874094722402899336966340704468987268209327015363/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^5 + 1225191331371067036997114623167913356531352677078500588677519012950144637556357748397087988317925282834417173707505540499181990747587564960701444772986430065120749061486957/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^4 + 1139829880892942613330454236150389131334204507628829192098318302000920851078460427826452365060230746014812351595430542528282850629675795886274990466797151753941032631230859/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^3 + 901611890905913751105803081869145038958035756246917606753847505167710465102362200151171952742289283153441804763699106676707617208795396172916091297333433100495454520366655/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y^2 - 155746946375843265995511981835113638406984491608067733548745912719974007778650512052009801568382705015661430786614626205084994653422976244642120742565069150471710332184917/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976*y + 5831401237547876149697459653909556715170589782098056138250624381374147157994016137050443392590113531698960125827049431937648261351989921184274378858902035124318579451201/8414316289150885227435002062481785401363213425006195845830885239815125138300037408109692048658370500311467998186384213320650095564868825770004737259414557694759519742976 5407840250544617413737788245349900222364786585144099760989005784332519499538186762192019580645604493162016236793978288745177159949052924312021015837767980142824197840958349/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^26 + 21664698081389917496108452219627619614570788839317752853206360973069405823227966199898056961626126623322330495702542730526986832922877738411633517483560848720814746039051961/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y^25 - 421535014586863581324489643898629214431340305811786350445892383876288840379292618652185440409291829344280842226122606614704609608446675946826736703591654117258322773639965545/894557072426951599351300896465063601179552059012440928276323446627477549970313272094439143224375257883851814384383800780554958102904508187658075325562009684149682069820268342272*y^24 - 11236410563777951880930828218172716454711097331478347779093874152867339917264188752083097356492524736129139680588925499256053177318979231907054404464627041068987440029078696697/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^23 + 614924013786867855733817872689690167710642374613819608451115550834023482730062902766132041562761771857142568841811064156018045346540017486392981857570411302809474672807858235493/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^22 - 3820075245010106280921052657300301723802262272220944817241255086365588544116276680329477419293010477409488494338589866157439424091904705131739104338033207534219378716756799299719/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^21 + 1973002671734238078089115263941074797724465556934037037994446720410871775110769256086584534375481657795161635828796371298802885722803869128894979925765073810090615821654666838627/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^20 + 5140919311147305988978139870900372962450781487577530620931879368611326357236882494904968447087807042618899117283145669224747320787525766522369282732330605825881050752486298303195/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^19 - 100109032708704867528500722497761463292277420983840011874264137624546041298494387251994064912697473897422273314999151844543540408318699120742983561409496173789116757882913720619155/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^18 - 14486177233221208334743283604431302005787192865756142362353107465014511547966816182870129735847276855704604005557409655066026118607477609640048930696879428134758693555782596570879/45294028983643118954496247922281701325546939696832452064623971981138103795965228966807045226550645968802623513133357001547086486223013072792813940534785300463275041509887004672*y^17 + 60628102189676069202323874096709045695310956409243699833702041022187173065148699208318929117882553462293037482729094339026699282935940212814184787239690510871563615362490515626969/49697615134830644408405605359170200065530669945135607126462413701526530553906292894135507956909736549102878576910211154475275450161361565981004184753444982452760114990014907904*y^16 + 1875274660952221382446780051979074465151852500891726376847547729896127216119572760323650549609543476470202890217992694326434778695043048173601963633941712657949250450654074255942985/1192742763235935465801734528620084801572736078683254571035097928836636733293751029459252190965833677178469085845845067707406610803872677583544100434082679578866242759760357789696*y^15 - 2686785733246970380026233998175262566870406837845106233489918677290080308095851807943296205506608517298251804469588218332424722282168259770020615850271825889274114753646519209050225/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^14 - 2710500098853175647144944257127717558976849934987773261100176413571778477106496084239537415069676013523307174456594383079046412539270122294743271342901631873163521757194423566151737/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^13 + 75195471123334985081429112331863441426709729370557397753099772087708464907041790585207884863784521237593494460680154213143148507769622684603116462961002002017330849076141397609471/6868000556061048747418816863455382734583892967465957222850851797523819961384362933546557721492324436728228901223676013670287586202721751920599426683777425598078173280769814528*y^12 + 1913612352600628211757879272538441733523394622433489438054621957490358775676305129251118246379190760196495676405767002188819805410424515247205717572538921921573965089274163939213091/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^11 - 5121963325877264803886170132886560854039401835282763244643279284925940498596565858479447369963439342593136952745947917591063690010684515691133208115647084019288127331164355178729519/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y^10 - 16819389414576947375660722236047091035646515124563154343056220284296590744265278750884760078097523770082304831259073379398526518183708374338673654817072826525785688760102410164442427/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^9 + 1895749983703445821842420539162412434984940474251288685725555770473576640390185788548534920598504139090912229148625776285137159496686261942396656156723162705209850049375348298906225/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^8 + 4927564896513726285985013431447381253418865419603967444993932994172526636241068534767165470809366412351771731764660175050314275380662388080738700983525806291280277482068919861721471/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^7 - 374559987280154031803201133120318272815503943360192296740228093221758386817328906259863009834893363765550263885142101766499156147463342765172375690690575143271213882971161371380177/99395230269661288816811210718340400131061339890271214252924827403053061107812585788271015913819473098205757153820422308950550900322723131962008369506889964905520229980029815808*y^6 - 4188670831814831317869846308663687767899237324439078023521827424368693447451987533062974486543014577702351333384308592980227905074103455713346983976689569783423999053189598429043661/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^5 + 3358775407946596224784712124504764739646288609437777325846211885166215214766742579885834845492825949919625073681316988713100711449862561299506805761279611152746416373282792239298741/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^4 + 1380603043879413520290035681255214164815007510896416645159447815236472390619891617425338485036220514413110316382549052583848237687786338157153732256342541033366209527695837210163297/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^3 + 369732373337071004147697481675734390671693120007748559245778419708122598760763810189353668277911286180144045989865470450113797650256741709509609524373348139600808226850025408614491/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^2 - 62016272701688071572664416679480501326218222148555984191746790786589674658270231348606750164604311920868729938506869976649150533497555874625725723350228028660858966022180949432261/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y + 12879355875775744074520045476326907727949160593471070000163598081704585530854525723729133044942862445976971610162896122028984379698974901387928336981574067753471283442539070634855/1192742763235935465801734528620084801572736078683254571035097928836636733293751029459252190965833677178469085845845067707406610803872677583544100434082679578866242759760357789696 5407840250544617413737788245349900222364786585144099760989005784332519499538186762192019580645604493162016236793978288745177159949052924312021015837767980142824197840958349/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^26 + 21664698081389917496108452219627619614570788839317752853206360973069405823227966199898056961626126623322330495702542730526986832922877738411633517483560848720814746039051961/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y^25 - 421535014586863581324489643898629214431340305811786350445892383876288840379292618652185440409291829344280842226122606614704609608446675946826736703591654117258322773639965545/894557072426951599351300896465063601179552059012440928276323446627477549970313272094439143224375257883851814384383800780554958102904508187658075325562009684149682069820268342272*y^24 - 11236410563777951880930828218172716454711097331478347779093874152867339917264188752083097356492524736129139680588925499256053177318979231907054404464627041068987440029078696697/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^23 + 614924013786867855733817872689690167710642374613819608451115550834023482730062902766132041562761771857142568841811064156018045346540017486392981857570411302809474672807858235493/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^22 - 3820075245010106280921052657300301723802262272220944817241255086365588544116276680329477419293010477409488494338589866157439424091904705131739104338033207534219378716756799299719/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^21 + 1973002671734238078089115263941074797724465556934037037994446720410871775110769256086584534375481657795161635828796371298802885722803869128894979925765073810090615821654666838627/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^20 + 5140919311147305988978139870900372962450781487577530620931879368611326357236882494904968447087807042618899117283145669224747320787525766522369282732330605825881050752486298303195/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^19 - 100109032708704867528500722497761463292277420983840011874264137624546041298494387251994064912697473897422273314999151844543540408318699120742983561409496173789116757882913720619155/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^18 - 14486177233221208334743283604431302005787192865756142362353107465014511547966816182870129735847276855704604005557409655066026118607477609640048930696879428134758693555782596570879/45294028983643118954496247922281701325546939696832452064623971981138103795965228966807045226550645968802623513133357001547086486223013072792813940534785300463275041509887004672*y^17 + 60628102189676069202323874096709045695310956409243699833702041022187173065148699208318929117882553462293037482729094339026699282935940212814184787239690510871563615362490515626969/49697615134830644408405605359170200065530669945135607126462413701526530553906292894135507956909736549102878576910211154475275450161361565981004184753444982452760114990014907904*y^16 + 1875274660952221382446780051979074465151852500891726376847547729896127216119572760323650549609543476470202890217992694326434778695043048173601963633941712657949250450654074255942985/1192742763235935465801734528620084801572736078683254571035097928836636733293751029459252190965833677178469085845845067707406610803872677583544100434082679578866242759760357789696*y^15 - 2686785733246970380026233998175262566870406837845106233489918677290080308095851807943296205506608517298251804469588218332424722282168259770020615850271825889274114753646519209050225/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^14 - 2710500098853175647144944257127717558976849934987773261100176413571778477106496084239537415069676013523307174456594383079046412539270122294743271342901631873163521757194423566151737/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^13 + 75195471123334985081429112331863441426709729370557397753099772087708464907041790585207884863784521237593494460680154213143148507769622684603116462961002002017330849076141397609471/6868000556061048747418816863455382734583892967465957222850851797523819961384362933546557721492324436728228901223676013670287586202721751920599426683777425598078173280769814528*y^12 + 1913612352600628211757879272538441733523394622433489438054621957490358775676305129251118246379190760196495676405767002188819805410424515247205717572538921921573965089274163939213091/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^11 - 5121963325877264803886170132886560854039401835282763244643279284925940498596565858479447369963439342593136952745947917591063690010684515691133208115647084019288127331164355178729519/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y^10 - 16819389414576947375660722236047091035646515124563154343056220284296590744265278750884760078097523770082304831259073379398526518183708374338673654817072826525785688760102410164442427/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^9 + 1895749983703445821842420539162412434984940474251288685725555770473576640390185788548534920598504139090912229148625776285137159496686261942396656156723162705209850049375348298906225/397580921078645155267244842873361600524245359561084857011699309612212244431250343153084063655277892392823028615281689235802203601290892527848033478027559859622080919920119263232*y^8 + 4927564896513726285985013431447381253418865419603967444993932994172526636241068534767165470809366412351771731764660175050314275380662388080738700983525806291280277482068919861721471/1789114144853903198702601792930127202359104118024881856552646893254955099940626544188878286448750515767703628768767601561109916205809016375316150651124019368299364139640536684544*y^7 - 374559987280154031803201133120318272815503943360192296740228093221758386817328906259863009834893363765550263885142101766499156147463342765172375690690575143271213882971161371380177/99395230269661288816811210718340400131061339890271214252924827403053061107812585788271015913819473098205757153820422308950550900322723131962008369506889964905520229980029815808*y^6 - 4188670831814831317869846308663687767899237324439078023521827424368693447451987533062974486543014577702351333384308592980227905074103455713346983976689569783423999053189598429043661/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^5 + 3358775407946596224784712124504764739646288609437777325846211885166215214766742579885834845492825949919625073681316988713100711449862561299506805761279611152746416373282792239298741/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^4 + 1380603043879413520290035681255214164815007510896416645159447815236472390619891617425338485036220514413110316382549052583848237687786338157153732256342541033366209527695837210163297/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^3 + 369732373337071004147697481675734390671693120007748559245778419708122598760763810189353668277911286180144045989865470450113797650256741709509609524373348139600808226850025408614491/3578228289707806397405203585860254404718208236049763713105293786509910199881253088377756572897501031535407257537535203122219832411618032750632301302248038736598728279281073369088*y^2 - 62016272701688071572664416679480501326218222148555984191746790786589674658270231348606750164604311920868729938506869976649150533497555874625725723350228028660858966022180949432261/511175469958258056772171940837179200674029748007109101872184826644272885697321869768250938985357290219343893933933600446031404630231147535804614471749719819514104039897296195584*y + 12879355875775744074520045476326907727949160593471070000163598081704585530854525723729133044942862445976971610162896122028984379698974901387928336981574067753471283442539070634855/1192742763235935465801734528620084801572736078683254571035097928836636733293751029459252190965833677178469085845845067707406610803872677583544100434082679578866242759760357789696 -30601670709144242519165686943312527525818858986311211194381955164103277190144904257203553827612086128121135428640946810486229319098102913072802753252782849608635648307/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^26 - 1154031947387847203400215337687036618884745577663902797639472755784319883669572531716754762163351397444143180335472660690136878983993843894006014682535361026127656126161/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^25 + 355969202565353234202544084466595031332934312657616514547145864955599845509498669854444295921534425007136324619662613936993960876060749466894839668276290312374979546807/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^24 + 112138871383546276854797058415992599290867981710042327051141053163456697154212084231718707153725982992672262037164775344890406110477163473802188176308065195830575486482951/1437905682020416474745912632453387343668156815772458795702348316861527104633816792597049054811131618057226143274074825445939253530889303898184569540786834935342064809837682688*y^23 - 2310780176660835089017508928647466101726956664292985665835921029764393429414815145064266372262980060659153596285717950878585428635320142917859949264416513004705866771888411/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^22 - 12714087323951832640871704924359728750051587255248751801694193585921713395634585724517881562054806148772958403870697360476618754622810193881030848105351312708329117428339495/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^21 + 103862866579260331756625550371399837203352478309513357228965934944305992543643052857310823727125113497440628127273412580774509671989696037909772398475798538355632102799424867/1437905682020416474745912632453387343668156815772458795702348316861527104633816792597049054811131618057226143274074825445939253530889303898184569540786834935342064809837682688*y^20 - 624392609027078754441585065130580324501133145905650616009252678564659934765422578748264236982404829449372282127709807324608531170590860352872865807867404306919704724392031437/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^19 - 1696199778704499555580984449481286505979814801720819584336148473684576658308493787443887827626302738804424495883192582450663205464195684801079113916697233409095190471094777331/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^18 + 13244109247820324052469645932999640828955470308376762692790190771067952528325434400298027767022997073315309505729907338483617904739292376121014994082922357885426969676862463439/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^17 + 4167430389058302474969876214627166904457686566868581458852261964757675492679702811710414735614515596658079407681350099889170532549290624801532846011257472550266195487567427277/359476420505104118686478158113346835917039203943114698925587079215381776158454198149262263702782904514306535818518706361484813382722325974546142385196708733835516202459420672*y^16 - 304382038815027610935993796600086751357503169255177302223341300937671748661091288216819683337399028326444867422392833179119260495782813605660545878885470653539238564788741823109/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^15 + 6282643085034562650013464683763478133468530819116284222026402103792065326219653321739374391084515626609957954703763907944183373255831706947503130307816508087036871361648762951/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^14 + 687233645166388003911246845134862846393342291265680082740718759439686514989506664201258695952891982985935519261716364492064344606805509461536262257608509951255481242134440383639/1437905682020416474745912632453387343668156815772458795702348316861527104633816792597049054811131618057226143274074825445939253530889303898184569540786834935342064809837682688*y^13 - 1461460946179580647638313791030370003494552699652881910687286051348433684322284031514928252041448875286149197555552674661012715623240597108546991010122701514273907860840024929/5519791485682980709197361352988051223294268006804064474865060717318722090724824539719957983919891048204323006810268043938346462690553949705123107642175949847762244951392256*y^12 - 1540858998653160300101777919584744012139581234016739569733933187459171957088496578454142958663238508677449496946920559085611557303797265971942216080309534633083355969409144562205/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^11 + 885992987190015079935705928222681445492453402364827793696600402612509501857205155544467708088996586620538719481650106386078763181956534558551646874290872942189739982174348585111/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^10 + 1322119684734517553657360763268476635034456639240442247773766679997219508183092055826812349268835184110485077846409078727851025608941930623628902102208744591366070041240155957445/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^9 + 249739255461411400004042341096787893431913708789731289146018993432899574735716595990171172227563189297755544232874438522548278528098449952077630695905051461400528028968776483417/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^8 - 468558429632730091149974048931395507558353515499733263956837680374115207600035767681708752097509718454268686366007156188568626703371255476416956744459875691065888254354200430401/1437905682020416474745912632453387343668156815772458795702348316861527104633816792597049054811131618057226143274074825445939253530889303898184569540786834935342064809837682688*y^7 + 30789703273351349280437658088508184871373755427820024133224111314946361271284243975821403681507430888433771422998514929367902614599163399176786212679273100304596551295751112407/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^6 + 523024460461952426722895541051639770435543629448890531688674454200505703025842034731773552459929126555066324643517752791098760843296836831458267391104176677952051072009518785971/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^5 - 80955575514334845084576818780318582697690560461917766767866297795648686914500223657932404573498733759933804889257646524897214225139850798933324083094939710202482278850760179243/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^4 - 47436104034397050544127145232401064433231468837275554394713666591038865388966481847152161733289274746617056160749985935598512997653477569468365678020342899323845026037089720991/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^3 - 69112550070687337143866687589880449695338885336854338956098691042680127240937579540897977509028551137988460866207352138754197509009284893346760496414074623867581041190089843525/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y^2 + 11092658291817439030369140121417489589562057034517010047929888419061019734992997688450637151284664718244556782765667978768610733658969975763500827711606076434497658813718894109/2875811364040832949491825264906774687336313631544917591404696633723054209267633585194098109622263236114452286548149650891878507061778607796369139081573669870684129619675365376*y + 39790145529418093055781152405269243257669842044166997082331952250922433614625317790177505645728934179895849412471476524237680086949970473242356062793617179256166501661303949/70141740586361779255898177192848163105763747110851648570846259359098883152869111834002392917616176490596397232881698802240939196628746531618759489794479752943515356577447936 836862346242031345947940663306480316854782571244135097395103429147034005938288826727243316988639701134555703680116080179665976773906591569900206661041282326952089/2103579072287721306858750515620446350340803356251548961457721309953781284575009352027423012164592625077866999546596053330162523891217206442501184314853639423689879935744*y^26 + 408134128195546300302174722083884072138608250547373604325642328687588463330240069129688268975819323933510894278700757648670817435820729224158702156307022851320687439/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^25 - 2542695697300007011369759533063611772705250535045435587213303187223261559637124851334302026371819226514861538438766158235409416845294154862958176792581774835857276039/18932211650589491761728754640584017153067230206263940653119491789584031561175084168246807109481333625700802995919364479971462715020954857982510658833682754813208919421696*y^24 - 9634907683960725244465086956670795523678235370229123343586912778048867126350844639587429892803276884015699348892904314541319898146279471790777752810151299608998777371/6310737216863163920576251546861339051022410068754646884373163929861343853725028056082269036493777875233600998639788159990487571673651619327503552944560918271069639807232*y^23 + 294694977098670299238505110186060773284693682425912262300973379082406529705525605371923146931533948449528605119513190227927599776896959341632568186106585777832832481609/6310737216863163920576251546861339051022410068754646884373163929861343853725028056082269036493777875233600998639788159990487571673651619327503552944560918271069639807232*y^22 - 12313332594351670065421087962329748894742902468693495372479631848264342690793023652366115543247336930227125353370838454788126224547907420862094330855720166267864488631449/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^21 + 5629843447648036689140582115372596103574398760756717753125892485574559680210160783104679947985632916789832098492151034325717137246686965650986012632547810587201054498665/9466105825294745880864377320292008576533615103131970326559745894792015780587542084123403554740666812850401497959682239985731357510477428991255329416841377406604459710848*y^20 + 27138805374649987003265033323688633702917217832947453239477286783453166421683241610680809028296032930760696551134060600455994062251886225212960478252547494986984905844657/9466105825294745880864377320292008576533615103131970326559745894792015780587542084123403554740666812850401497959682239985731357510477428991255329416841377406604459710848*y^19 - 383466288275608148556284502195797030531966166439710831643492821814832498049791294098162555529966264152938024603864098524613639326130029055182329713101440730287381733901437/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^18 - 472388394681672789854114762989023923326899771911938843399596213495487608819534508354678269413328470524419232784363071836085144573098808296163637617529829557032898845179827/6310737216863163920576251546861339051022410068754646884373163929861343853725028056082269036493777875233600998639788159990487571673651619327503552944560918271069639807232*y^17 + 4959807156459109655732358942994988901280232088204406315920780565521045362030147185725831150981666565221649714176253940265340019744764322759752214416553955442292680825052953/12621474433726327841152503093722678102044820137509293768746327859722687707450056112164538072987555750467201997279576319980975143347303238655007105889121836542139279614464*y^16 + 1818601032851650703702124253252655477485408895251711881890384030388964448942525864682851504262908326816332128382809782106511696839156163609326466682658815116446381847701275/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^15 - 2929849132878031852888407963512058821186069168437826001597265900326845058920309376917356149743897466206303381133416586813978307861070738499553304755638641924893263931034249/1577684304215790980144062886715334762755602517188661721093290982465335963431257014020567259123444468808400249659947039997621892918412904831875888236140229567767409951808*y^14 + 5661707244161585030902632066192038337400248773924526546919354108843633850632168777735628500384431496596386458105930063189448200486185521380713711633517888333082907665263245/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^13 + 22307360761985330955729919852362705443007056126036128650030641645374006819073048983378321646272024298738541502659510519322329985391455758901032292399087352530575865892179985/12621474433726327841152503093722678102044820137509293768746327859722687707450056112164538072987555750467201997279576319980975143347303238655007105889121836542139279614464*y^12 - 5026051104742033210812424474167686163763930316964030961985569279315988473186645934256081076536405830338523015631154197790028877208210677091212684848335871256309511181694263/3155368608431581960288125773430669525511205034377323442186581964930671926862514028041134518246888937616800499319894079995243785836825809663751776472280459135534819903616*y^11 - 49933114958253807513118878119125528756923536297127931616358042431377828803806206280676751981275170278009286800726818996626009183039283815691703905544192703591783351371495345/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^10 + 284201248174306983198536819529412336028940376742787948816612793366056824749302697550753611087800274214779588082968782779037779883570579330978861791265288391484225808776659/3155368608431581960288125773430669525511205034377323442186581964930671926862514028041134518246888937616800499319894079995243785836825809663751776472280459135534819903616*y^9 + 50316144196929390060901741608733026104408403167147092507171470606751129677298840331318950884664701460468632475140460571770284727464063971137447408908177498164287772359939225/37864423301178983523457509281168034306134460412527881306238983579168063122350168336493614218962667251401605991838728959942925430041909715965021317667365509626417838843392*y^8 - 9308584697712997197032644164344785273242126014361009695935766531773815373846539464767185120849321441642077863848713164405320530120631072486293803356754888464424010429022415/18932211650589491761728754640584017153067230206263940653119491789584031561175084168246807109481333625700802995919364479971462715020954857982510658833682754813208919421696*y^7 - 334091105345559387530189670842966605510713267465144980355365041808126250563995187188467502143589430133697178354001762924756147921579073934195540454642272040677329140937651/525894768071930326714687628905111587585200839062887240364430327488445321143752338006855753041148156269466749886649013332540630972804301610625296078713409855922469983936*y^6 + 5618753100544167347410345637691417494540038646501054182731129803760937910167255565769853920949148540406424302532135127297303685667123581237372207137199423432376653938253421/18932211650589491761728754640584017153067230206263940653119491789584031561175084168246807109481333625700802995919364479971462715020954857982510658833682754813208919421696*y^5 + 136937507704593363800405999028183304445449108447289833416964638675492453401809162998582653211455135615695036038071110187983411521180629321962974652833973738924660510823893/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488*y^4 + 13263235439378028239842851456906404853327868561357911664746868929306302320575177057686123663984116683923688447632611007048453171109833322958337673760161657041018960910271/197210538026973872518007860839416845344450314648582715136661372808166995428907126752570907390430558601050031207493379999702736614801613103984486029517528695970926243976*y^3 - 570866252103053946668794643290523554570661190120189936744542905392511310092031364724257020182942219754180799993323150440809124377214403493144942536411644522573041060575929/12621474433726327841152503093722678102044820137509293768746327859722687707450056112164538072987555750467201997279576319980975143347303238655007105889121836542139279614464*y^2 + 6031203996840718073921324066582954504817831209420393165812900945923046900111750984682183740791274089237048472655524683179807014905703752824347878510837216826871548960733/2103579072287721306858750515620446350340803356251548961457721309953781284575009352027423012164592625077866999546596053330162523891217206442501184314853639423689879935744*y + 4769405308061328156975983400519110628963007127868970669377001137441910398105848867984436830608508677032649369335811669887740602580715473202492493936832915949804824898331/4207158144575442613717501031240892700681606712503097922915442619907562569150018704054846024329185250155733999093192106660325047782434412885002368629707278847379759871488 # A Gluing Matrix {{1,1,1,0,0,0,0,0},{2,1,2,0,0,0,0,0},{0,1,0,1,0,0,0,0},{0,0,1,0,2,2,-2,-1},{0,0,0,1,0,0,0,1},{0,0,0,1,-1,1,0,1},{0,0,0,-1,1,1,-1,-1},{0,0,0,-1,2,2,-2,-1}} # B Gluing Matrix {{1,2,0,0,0,0,0,0},{0,4,0,0,0,0,0,0},{0,0,2,0,0,0,0,0},{0,0,0,2,0,0,0,2},{0,0,0,0,1,1,0,0},{0,0,0,0,0,2,0,0},{0,0,0,0,0,0,1,2},{0,0,0,0,0,0,0,4}} # nu Gluing Vector {3, 4, 2, 2, 2, 2, 1, 2} # f Combinatorial flattening {1, 2, 0, 0, 0, 2, 1, 0} # f' Combinatorial flattening {0, 0, 0, 0, 2, 0, 0, 0} # 1 Loop Invariant 11484502397347847213793561858655314222135987548353127975414143495634966713786206644484230408753470111743392848360480215833629650252439106436509147675935184289898221404849/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^26 + 326804535806090328642064612733799114126217870263304718145777286264645810534649524330245260985777295932959633539324194743931174559897149438804783134165001979981352021299343/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^25 - 862205963147541713063428886401114318817933646523785634187060868353901860644945553218139235528024696696880030908705858929875607924296959629368029047783709348401795380538219/539214630757656178029717237170020253875558805914672048388380618823072664237681297223893395554174356771459803727778059542227220074083488961819213577795063100753274303689131008*y^24 - 24615134125340548709817059224842248745367101706010176185439529354088758358717170984024383589382029981903739605470646987823206547354997189871504750909803041178716320698897337/1078429261515312356059434474340040507751117611829344096776761237646145328475362594447786791108348713542919607455556119084454440148166977923638427155590126201506548607378262016*y^23 + 1286559869560743257407565220181968282628104153484381035373269322145981469106028908814085658848170786998017355293714767464233503152391028670817099519754483910560348817123842809/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^22 - 7569729533876006154600538486626686610207309604287935434508253188794318519779426153806358524435830120617595583383876676750096366842994717910062074676301341144185688469853887407/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^21 + 2453353781650133762649826040224842905983967555859804980525753612150228853070768339345535541358943037553200879525440459644608554082331137759512734624777569961374452456505034831/1078429261515312356059434474340040507751117611829344096776761237646145328475362594447786791108348713542919607455556119084454440148166977923638427155590126201506548607378262016*y^20 + 34221574389623683667167195627417581864860300716930157324404998088790113074830817539310997483199233806423269287244263513256139019662071198506912180111818313290590986222093401645/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^19 - 174310943105993791864448597414074763307145031760989760162723642593742341033447053567627574706138143175966552245119164239898624931135605916695334765097236390293206762531485378139/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^18 - 2524276991623747930539098351107710439200835895558359884758201910396575934798200293422299252216334890418346485921848032496537427890140150807818459916054176948309613678796728366213/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^17 + 691689712582919898555064583887413382745449139099884839720256742366610768195207079914783320643371620172806122285738935703863405676880247050168367391156498851780901849839816292555/179738210252552059343239079056673417958519601971557349462793539607690888079227099074631131851391452257153267909259353180742406691361162987273071192598354366917758101229710336*y^16 + 5314620764292535838079164482889462056939027234575844825061955420033725197938575201151195664525224031398647904742891809204120507872533869623311766243935658843692468493563883664585/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^15 - 15873069789284702085584760574741815347165944149201241961902587224860431442945956555936883523575207126388348660562638043062300803783040553643923723132970283099365156723783564523703/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^14 - 15961773007021788933168281360634067898241821772826314016580234205675168621606283230529726099314223180989960786079063641048658129725043001729135796006722558200376977163793737317331/1078429261515312356059434474340040507751117611829344096776761237646145328475362594447786791108348713542919607455556119084454440148166977923638427155590126201506548607378262016*y^13 + 160630823532908689094516636727098087340682187767881628123356784767942293953768096198517137529699491786214125958707330453399562667993917969154769576057353330889854684710348093359/4139843614262235531898021014741038417470701005103048356148795537989041568043618404789968487939918286153242255107701032953759847017915462278842330731631962385821683713544192*y^12 + 30341884025550316461031702008808455142365115954476153238227862513636841972469587860156269825762605287655956002014824528476009390861337355274197786535388745194154555586162897496855/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^11 - 77405318089638929329089071516853912833217723119032375518289443379077026695953360518733570093680195979274653366768178228492492162407600848254415829566549733632654330874640187709353/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^10 - 57297209798528430136075082066697309529287658995264219035992206902472768498838854794285730313251675532905162310633263551216480175641661545511143789132413556579395855717085216473295/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^9 + 7518801820406933340409355663263180299442031357439610584185230519216013020405575559915001449453106565930939850847518089443382238272175717512799118495537129630743950327472275250899/718952841010208237372956316226693671834078407886229397851174158430763552316908396298524527405565809028613071637037412722969626765444651949092284770393417467671032404918841344*y^8 + 15426083300006356219241048766222204830854837060420482439580685575412878522699603092727285816055917953846791895911892412329341208242078754433445562608227719505138402895641641831943/1078429261515312356059434474340040507751117611829344096776761237646145328475362594447786791108348713542919607455556119084454440148166977923638427155590126201506548607378262016*y^7 - 2046253816123599281091189187825326877882610469118585105091149103816359979210102730220155197325590143608649995895632121557052736322052745988820403146454923794695394831236778922735/179738210252552059343239079056673417958519601971557349462793539607690888079227099074631131851391452257153267909259353180742406691361162987273071192598354366917758101229710336*y^6 - 16088080065562690282075012012790012130869997414064056457939687101347169981155944018131845691557232583399797620379805207626480411183673546454074014498851382554702887958971874982145/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^5 + 5267531035322627066012619613837780153338925782776188498353382596583162424405491727938538128728856444347490016926775032554617630477582274212601009883665230254101174929565842046485/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^4 + 3077024870223700693213392429950072541917215713179996486429693009689850767490788084903404838002270740453914333556972919912771475654278435264458301334290691574301629104772300239181/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^3 + 2069572594244573048912281534645453723720241406608906981430207928954105351051187408982765134951015794516636030890898526395023470454046604083311448115789736531451494377567401863011/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y^2 - 465537407575339392330380889591664673469436546939095177761653224952997997193726676198023048195577639446414109843614788639803209171742872964072399572152218889887531364887541193247/2156858523030624712118868948680081015502235223658688193553522475292290656950725188895573582216697427085839214911112238168908880296333955847276854311180252403013097214756524032*y + 289560562966286510373149245792791158639420875556755461774386530451241246783726011314702833199832236819863372388470448680596501609224676052780796724129381561610986484444666711/17535435146590444813974544298212040776440936777712912142711564839774720788217277958500598229404044122649099308220424700560234799157186632904689872448619938235878839144361984 # 2 Loop Invariant -19699019667667275793098126597286118374609157831173567863425329489000065691206747301241075203820790925832787477294698108962238982887943967604533708989134227725893997165752553972358195609318931572725303614388698678370147849623891724468015224298590054491663558225/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^26 - 571165504537533104058125659279263165912489090526841195718244770472911960372807311639031145612989648563283113506852649012083091656737212395473024432225413919192187702106610765739325407221406911435228783731031226285295310302627901316374155201155736327935695193411/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^25 + 1406334966573759064991878012715892106282207939529701477541205906667114499699772318268307124685523342581442081246302342770794858253970216099170271193317489295841753592412074679484451602945287704016396462457829471758788737717354739503963338759853939560752161536553/514474918452164588192154536094954140864660905451417821817154648136992123153097146312063515943604866890840420844041723635936903094525932366261982765977740226676279266345950305454670161941346174397899826666216391367392537077362771867602053590035228201086528313535246336*y^24 + 43972829283695289177329780700804054432251479414377348215345547901364626272052353424095341494484100323149219246446639065868814067579275265737487804617000171954813011931801726213034467324898803788172610968914585168389419853074253603919271574172342820517650135558117/1028949836904329176384309072189908281729321810902835643634309296273984246306194292624127031887209733781680841688083447271873806189051864732523965531955480453352558532691900610909340323882692348795799653332432782734785074154725543735204107180070456402173056627070492672*y^23 - 2165088730236675769092831494125375017613174887918627382902886584210666930555404459981221464969296924411010325379864076921409141317504410638315398995618070829917973222154026230729247780147195433599021604589166608922309681889655214722931600471764278548836915870212137/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^22 + 11750049800902381097801269999818110569255096191749674208883767214030628492365832278530833791935576122973044513493116852415193400022942658591787910116852121216371362894398346715914766589420561273154314448274601211758009236010837580450584053759417514781241724661865195/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^21 - 45103901083940540854287245951029489652484201932268478813704502369197889998730826732963481565547443511504876605239322787528326249899767979770009195593936558911438780279589476322007427270905913607004488539774319498380261536089471014974865384444652891693346004378623/1028949836904329176384309072189908281729321810902835643634309296273984246306194292624127031887209733781680841688083447271873806189051864732523965531955480453352558532691900610909340323882692348795799653332432782734785074154725543735204107180070456402173056627070492672*y^20 - 63170528731368525764484236373615544531649548495853607795972304194355460511296241675677270422469663393661576470282109895242339422902538073247776196366352069250137029376728638244754710997788962581311707904682809269430528829010581750699753058293948693143397294449983157/685966557936219450922872714793272187819547873935223762422872864182656164204129528416084687924806489187787227792055631514582537459367909821682643687970320302235039021794600407272893549255128232530533102221621855156523382769817029156802738120046970934782037751380328448*y^19 + 217820128250151141659912205323647532500274571693722470945043767620722183134254352895164845370011813991945328841145394134347368985403579337920014346169367035635665310852493779729543852586846873111081589468677950838171734877958634460678130110902978833071231427896081479/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^18 + 4579229230629122560391873058153052576220956504617002380322026095323102994338172981582286817426303377613802645450405674539058209644849002816614934430238951181148775605216638677870082865843705981529343492918754275123688813256762827491708024404480639812632645490776259461/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^17 - 31673999800782261629269462209253246717673711066231639973997623634634796225592474390581952670537470926282802366200737431073439857110566204845929896853622665157678266827490669547722284851753154999947369235732658481282358826937223978806661565687670836722178061211000317/5359113733876714460334943084322438967340217765118935643928694251427001282844761940750661624412550696779587717125434621207676073901311795481895653812268127361211242357770315681819480853555689316644789861106420743410338927889195540287521391562866960427984669932658816*y^16 - 12428759612832054372045632895526505018038354241176564668502029466646193842025433240158853810085278354250099722566448516653878792388097431039183056732913144746468614681152630928660109592238946165126383738493898885916059366237626479552368793449628915255457217119919458101/685966557936219450922872714793272187819547873935223762422872864182656164204129528416084687924806489187787227792055631514582537459367909821682643687970320302235039021794600407272893549255128232530533102221621855156523382769817029156802738120046970934782037751380328448*y^15 + 25803668522580774599054032723867486180126846549924453095870312123172680307336399241515764663479784841268259062989174917533441093488652287590041620237146510415654380982330312328260063859924909688448944259858017821466956671444596229531444647333868157716958316127881440351/685966557936219450922872714793272187819547873935223762422872864182656164204129528416084687924806489187787227792055631514582537459367909821682643687970320302235039021794600407272893549255128232530533102221621855156523382769817029156802738120046970934782037751380328448*y^14 + 52168215975139498209720692649214289530656358959680216101320321989750173944872696798543876018758562737592204743999735925738213331504212863473459034737948322283636107635018099556369874089045932909064719046358076563610814740150060278876245207281012636910229111488194341833/1028949836904329176384309072189908281729321810902835643634309296273984246306194292624127031887209733781680841688083447271873806189051864732523965531955480453352558532691900610909340323882692348795799653332432782734785074154725543735204107180070456402173056627070492672*y^13 - 317376460223547785635438591518007072955645416551732738651511706475182933332229694428316785164588102285881905261176140111339943977850309088994099554469507719802694187634154199398541206037989896540752765307748540389141698130280507908953932299908225874529846938748211795/3949903404623144631033816016084100889555937853753687691494469467462511502135102850764403193424989381119696129320857763039822672510755718742894301466239848189453199741619580080266181665576554122056812488800125845431036752993188267697520564990673537052487741370712064*y^12 - 111255707231980589998555330709770496392674066249040114363908471940253712015999669381356360885493204969564863562760581457892099383267216458396387189532964329337894190062640370776983023014015460808326324959086886408394539061437425117914223479474404577308605111855820120719/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^11 + 162164599360689153421543969643727098532967822275911614204842560463172386726780988039631240767409042930813847400426116127023364822251811963704168834498717624391574911301678591741407692452248586030862285074718213484266031909740389964202682202589279617658716263091111964789/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^10 + 148254949997332231083962052734922925841750216646730427408284619667050153036240664882469502572187660980309599592901393999386737933702248017733726698320188430558605523703639547828954838331704175738085752910361254868865399187876275938699640980201170331393343926685537239175/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^9 - 10584551591786710312583828737389090602200611018875731588103334688066008421208883758679276141816497655592081037893200533586980801326406825260401285167755312987392799947414343433584114449342046584830432750533044047985797557644515007001215972135830070413618091405812212663/685966557936219450922872714793272187819547873935223762422872864182656164204129528416084687924806489187787227792055631514582537459367909821682643687970320302235039021794600407272893549255128232530533102221621855156523382769817029156802738120046970934782037751380328448*y^8 - 45687992471859633714629272117643537754299868487963952570973360817879471887343665706966885591700051341598643321522243618097541202081804363603155130211075281586222502062662246235423419330718248321130915203593501013277968258391415544007435411033264310118373393350632057731/1028949836904329176384309072189908281729321810902835643634309296273984246306194292624127031887209733781680841688083447271873806189051864732523965531955480453352558532691900610909340323882692348795799653332432782734785074154725543735204107180070456402173056627070492672*y^7 + 1226416682901271400905317492185786212586138607966692491327814562876856907604621158683042090855721315494175025226953742752286092783429229622632529631708658463215007544065414945579666360430089034986144744062514201383910572106130464695982926245862847643666938173148456133/57163879828018287576906059566106015651628989494601980201906072015221347017010794034673723993733874098982268982671302626215211454947325818473553640664193358519586585149550033939407795771260686044211091851801821263043615230818085763066894843337247577898503145948360704*y^6 + 49237522013071525507720154833928977548233262274590939389220507412400661872325380135872926073590584854390780733486766114509799484923927668006080276494630102101263378510863934566347389553023913292645141593954856898974096408149466082313919255232621733359646224254974846129/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^5 - 11971455406061102275099735429075991888585403538397305308231599256860226020347278878015098166916843462618700714953783676351023690990693833108090876937350364706976442021385229736922488709585501289516407653622422232709171510755847227468906926087033997340106006786181957105/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^4 - 9246004196037777026204100129763996169930695917597672555422553780999442190696934816409819944380789278270954247603632780713707750917497044888825465349848791470522772035924452637660742667181803388540263619004992164918136079673936215378913068220901457040532367440219428965/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^3 - 5427100136695560743248007558684397685961614864752044846692839722446245903420729513351519564970444124925249045575648332699620021454086063239217839555031287042222925023504439623832290655158821645131385356710617307435937630627696044239417384696740939001736397498496737775/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y^2 + 1512967402177970656992926416100655277311411892120552622949216550835067060674510433465493264896288135915904415696619114119544600932891545352407150885002551877547361754172701800225806513114394046965946470721323919936487839214861606150465780554114892535441998774482497311/2057899673808658352768618144379816563458643621805671287268618592547968492612388585248254063774419467563361683376166894543747612378103729465047931063910960906705117065383801221818680647765384697591599306664865565469570148309451087470408214360140912804346113254140985344*y + 3779946120858867927111568954975997005868705361174882289224232577833202745491842325201934249092498143620749325307732348719955012687685470336456397211433147814725523737775828072776773511979065830243109093394579689655488954750538603391211847101785415395609726836323309/16730891656980962217631041824226150922427996925249360059094460102016004004978768985758163120117231443604566531513551988160549694130924629797137650926105373225244854190112205055436428030612883720256904932234679394061545921215049491629335076098706608165415554911715328 # 3 Loop Invariant 4245069308823010472703825388867608472383674259853448921703381459831607725760858535528063226861695763166869904545558996015651670359399463237955809255037255247975414205308501877800221137154009352400549026943772034408149256667882311305044456231077171570944845038251527594446289437555859087301229122380737791/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^26 + 119275175814816241188527185248185831139663108007683756956393148620365334725936516582408469040849399317113896480650407356965780664721309006957042292594955221594896297708091233018124079052655655154615787025593583401526327123071240117045752185112548843243975908023604368681411751482751000459926246426051802869/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^25 - 329093260055251606372732881687012652574794955941185767944402893166944972247823229184158886725234100706374547853723984058510291153512538375423944436092163992426459291383227200496796949607349019044765381421161306656198275191455209130003758362010463678621260385708941074605921822024747918609078771920166153139/254860393067595303600449483726695671347305763794149164690364813912892083393543637890740526181538044927787010665491030595335061136153811891591996739482010490596039485268316909843236984859145847475519531674231113773439500003077369320018189176937128745656010237126543965125387778554515244396480533416386172467259392*y^24 - 8845774107744271965537533130459782248016892847821484342439642125984370047022638713898590456846006492242255619615957605901778688156852362185988949753573908067212483109362975697377972243390744587904817747484406646451937601966427478167135293341175473106233675333650226680259391911918691985693418641761720399715/509720786135190607200898967453391342694611527588298329380729627825784166787087275781481052363076089855574021330982061190670122272307623783183993478964020981192078970536633819686473969718291694951039063348462227546879000006154738640036378353874257491312020474253087930250775557109030488792961066832772344934518784*y^23 + 481494346153845516518197411783916186975723596547944282098329557499241832865548338840487339046448522884359638744147379132353727945214854327510395513772059385677784735037599350264290721302807420551656141948911547605389552540416274025167966863785447829147151736950114344059475602368060462996154843159551364301127/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^22 - 2975542932124516478278137418570530565850913062066737811738308343314566785854593306736441551241361781772096314757864089855011157398159519153182654635840235498547559600928676844207264727145465738727529535286986277877179690977075457864432275097571005075647105059524236353374853982441551352626831161821629114718749/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^21 + 1512345096020886593668215784708815040115319205362909670295189819150973617639753499380244301508072473487253181336962111999773376455303685333067016088993662557149801740452516355140553828844031513374607400884354525839230457783468454289723379824086159764153806942684610539691629311714700885773218544767180222338449/509720786135190607200898967453391342694611527588298329380729627825784166787087275781481052363076089855574021330982061190670122272307623783183993478964020981192078970536633819686473969718291694951039063348462227546879000006154738640036378353874257491312020474253087930250775557109030488792961066832772344934518784*y^20 + 35877507417316926143296944727052439258054984543894216076263913381076726811024908313788544133172316801967281080318082688391111338331557435709002513654473366960754542175819069241537272165530289941695343645711684018538757215515606501446696250031135437319523219497314863103725920540255242442707883177362322667442497/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^19 - 75591110662913738011522394518549196525606738332206824250999116926015067050527007168988290881042890679283538402378974904577848986829781176283571163125617875125460412440179843490742088984077796051345632076293476256084309191304913061198845013898447738148417777861401004199551827106420668077305287793446753461668577/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^18 - 896849587580753237515587920685505697689699734964939040041626366204756643890926180961740218748499677976507040178853800115111795718573331906865536713813044077931583184680210499067324123629933554636161364252581848637833016227487994035548749792008486308847439332420728598152076745278334803047632424368010690328470347/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^17 + 419944034759057410079517612293125480685188145599849902871849884789768858057699050794480870040994679968389682065214749252247408454295482439221277446310084977720013148210824054787351926391340134244632727335680607399241802725305354869104630743824287712708008610374674332925164615171371109127858326490605623003256715/127430196533797651800224741863347835673652881897074582345182406956446041696771818945370263090769022463893505332745515297667530568076905945795998369741005245298019742634158454921618492429572923737759765837115556886719750001538684660009094588468564372828005118563271982562693889277257622198240266708193086233629696*y^16 + 4453420214320713577079086021339387298655995948837878353710416255326423037662573199610030375752546310453137180975737228213886115367708660345828668943687508047788515502694004043897443926475364399509356044498523434574116364398710484365268796611852949899921787701813192520318865465466262487653099811619551925657320313/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^15 - 18013274617148146061914352353237487924277002277714207526890349671524912883333314395869605716959184948289547604605116634765488028912151718502807646054826688207429549635990108790731657688855161200350192261207880298628406860501129821158231261222598719598249317592633378561156291513595113885261775955200998320134641891/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^14 - 2520831241578334082802659603401176907686599606128276176550260156963530622421288823702786211894809024225049301798686151477050552884387530047063027633975981929374933529922138580271827780411892028678801537101623987707817157560347091924895274431712121069792408555522192008174441852694421848566538452353701026791633507/509720786135190607200898967453391342694611527588298329380729627825784166787087275781481052363076089855574021330982061190670122272307623783183993478964020981192078970536633819686473969718291694951039063348462227546879000006154738640036378353874257491312020474253087930250775557109030488792961066832772344934518784*y^13 + 51790646336271375712913506624677985553206297193409116964590442597650523146104256848992524393348932823070627123891836568436283862786658476532423706002489934549933276857326682715925654387795661943223532413207357829346192709795205062940422246888939161591521805959480088660655009515877303479798876052456715220620485/1956701674223380449907481640895936056409257303601912972670747131768845170008012574976894634791079039752683383228338046797198166112505273639861779189881078622618345376340244989199516198534709001731435943756093004018729366626313775969429475446734193824614282050875577467373418645332170782314629815097014759825408*y^12 + 5038585878925778601751834248424778508262079411735786169822418121298700146755987253181278228111752703499578053886670760619087556343265958282273302016315373865876888508865883498722212046082284409296855736310002729915347688551527358414918859302579030707141552381822222779551535877262273499000622073456219031741734033/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^11 - 24270017951245692923694026424706649987951622409559511315597916367119799095612798782733200252172628275011641236005254671368226193260190442557796258513339487474464867086023099572173206948935917430876959107839085420669480578629793443755971592298423455217839077454391326801467748710357001779778977996212126733619637971/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^10 - 16989237024872499483031076492524434613636392898450526311028250919456663082127288859322285829924505991335679242129598808237828838292509191385840708798488512924932659746504965650324476925348520922949966996596694220044035760964993544290393272597490443511194846287813814494150703875647901677887151795874908937037795097/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^9 + 9678705059302402095413296745754056328732085138629437211735789716246610998039210006178161411803197035966419895980426352667192270959568266232298638280530262168117757519302998753878262031928355409376959015511078317615430958324724438896015094329536073640440099719753179154025823461518290763743284058183189036012471011/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^8 + 3967327771606557857022349177052784862852450366411833223275310125170646944868208138611881775862322208517105293866647450131217809054516681513668065965053711236601514414681593107923737900322825516083426156200844262723530825599627994900266387993661813645656407395358017719816059202533378385419931960418298395008357189/509720786135190607200898967453391342694611527588298329380729627825784166787087275781481052363076089855574021330982061190670122272307623783183993478964020981192078970536633819686473969718291694951039063348462227546879000006154738640036378353874257491312020474253087930250775557109030488792961066832772344934518784*y^7 - 1920944961477834759007563706724876812608308426109029672375411934827043171787230834880656050379673132991961052008009177460517940192530788954181978291319814051158821843588009400968923184362497773662711343774494892580767076384598891221490430834605984303042397558207997827815109385454345911500504670644727195786965507/254860393067595303600449483726695671347305763794149164690364813912892083393543637890740526181538044927787010665491030595335061136153811891591996739482010490596039485268316909843236984859145847475519531674231113773439500003077369320018189176937128745656010237126543965125387778554515244396480533416386172467259392*y^6 - 4250240616344889497781222358381372567927013518433758158249555554319548134264065644013735537681528544396765784170933278438672529644358231143126267543655375814564977042208343870858975816626624686151988488161798661441338429763471431560159764964796080939639094838628612599163135530419775822506310541547967355246535231/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^5 + 1189862511498567970607387370005403491071175982158326692706545433946111119225139827152668523637869654555302886855890072964021117528493460006541703420636029993355847265801394329005883818257287269148372068384148544141553271253323060137706584080064228072060983095161769075973798468264078338772182798531624088497591863/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^4 + 1508407977387274640728544163715901758527175518662896967071010942451450997758444111763294665524578992540345914725501494803935820280392338746552549548432254812072132077817017065694478384834991255332234936519018186672516049735467802984866709334148620335013764471336358208006138183303851031853664217816820279313450843/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^3 + 452638747642008958025982053111753671449009597252392160221521076724012140805371688480901128829815458114476200084938939480947061122182058869028260487517794389866632579415987362170916358807882415824324028938175808121379774553718101695535825799787825716812388501754806315495109037413301971408617805800304706936264057/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y^2 - 138111659008771081929027780721587644662531213419014843079061451288096896742740194517248627696782111051688883102523497769208616574523354330454444757337286683978296601428837697125975627980120711292633315986326073492369426023840681565599905350180014893224306773698412622040047714655656770783538203539925813133288017/1019441572270381214401797934906782685389223055176596658761459255651568333574174551562962104726152179711148042661964122381340244544615247566367986957928041962384157941073267639372947939436583389902078126696924455093758000012309477280072756707748514982624040948506175860501551114218060977585922133665544689869037568*y - 680154286306660707394106582941552405805517342025479622445054616672080807238486301609578390284457306386307584998316969941627311026904497044434995545916253380647838818766842001271559139627549064920476716385337073204804348330833925294613024480319728025954888740482010589033455851407465122816588516594046840174881/24864428591960517424434095973336163058273733053087723384425835503696788623760354916169807432345175114906049821023515180032688891332079208935804559949464438106930681489591893643242632669184960729318978699924986709603853658836816519026164797749963780064000998744053069768330514980928316526485905699159626582171648 # 4 Loop Invariant 791120587553932631486471116805835013922928354262545811335425736144915387022739467033151685439399298754787345432649029483341384780690648125631129164454457852677897350338824168691521759146052806650292881678695558357749739083737613408971876590592736198722828761957611927008890602243846127574932228659927601862011671188207156445683148171894558380923833380105356383533351544844404543657646696819633150643/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^26 + 4453616449043664202881108669756420162573156212476928235410432491175659644608348420183904011111570475102128283771651339974197447818102246875629726544021685618616069462568848801691984819283646708412064629199496438318843535027275576939850785346340349938751287009763614009277042554113694813458115059784920781645525325882868321275593154168497474633218896091047315015390139221714380590763280707842917498973/17508034124416922221185088536112166024586818670224349789341278435314160996601083074645358095451387710418943742620933675747751923030638761804377051651195359314289742195049170145818233808867163559197766828188406489935906562837327726246652249194796167315222110912632830639392898198114553966519746436836692327911389732022492688502388743446003059111833148820060356969975484609483356616209236579743266861305233408*y^25 - 61074880177370539389984064874411935771078095414547806013728690180682790093200169174348161114896604936023163571909992055660742637909703256900696033164350211514220318023831193045595587773149043585714927081590117741145354686787533354123341382125023530331372950988718091237046508985701180169989436769860879881246872621536683687779163805686697254395888441251531726141266988361662674691007728417317619041879/21885042655521152776481360670140207530733523337780437236676598044142701245751353843306697619314234638023679678276167094684689903788298452255471314563994199142862177743811462682272792261083954448997208535235508112419883203546659657808315311493495209144027638640791038299241122747643192458149683046045865409889237165028115860627985929307503823889791436025075446212469355761854195770261545724679083576631541760*y^24 - 1655938389623768260190893660730156940817367488500412379938018141624870389281252399176000189849819184726057323586549593675078679346811585965093153036484586145836780069761205199508264671936378454404387108122857534500686394786623640755139476001056481881885046340047136428588976813920845241081014022458670782116134426011991847355347279633110274535279699215875853921026860183947611506723863144687118305545991/43770085311042305552962721340280415061467046675560874473353196088285402491502707686613395238628469276047359356552334189369379807576596904510942629127988398285724355487622925364545584522167908897994417070471016224839766407093319315616630622986990418288055277281582076598482245495286384916299366092091730819778474330056231721255971858615007647779582872050150892424938711523708391540523091449358167153263083520*y^23 + 89597594080189998875943514523643670167104373642436014941588256384409837645706684944273663768328115430184437727810039271682485680913621453011832484907942224850015629243469696874016308601977409298415320529947938931380744385515266157286052281555278731701193468539376619450053638893516532756717655847555150150382966294355688597367661558420827772536273019030715891362510341620731569766405253292558621433378331/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^22 - 109932735016930493824982065395083467485176698579803287708141191526320554617164213200775263032374704085304671389974169873943016827718893432562581791753923584890129631540632082445537478770201510221540143441467630859946418034372819361286467608273683091237873442221683409271532330113077428342288615200821160769696734839070590168144053149966908072441245794222854620236471519102011806845840683515224377302181509/17508034124416922221185088536112166024586818670224349789341278435314160996601083074645358095451387710418943742620933675747751923030638761804377051651195359314289742195049170145818233808867163559197766828188406489935906562837327726246652249194796167315222110912632830639392898198114553966519746436836692327911389732022492688502388743446003059111833148820060356969975484609483356616209236579743266861305233408*y^21 + 262539929275706940277473446461252366380862181063526166706450713015775627369298645208270061671843701181360471644090794354602057750802260315699790308824292146588646670735828247464923635071702319699779868403070070425734132870929527045322470372218738110710472377806289139363288301846521433671789143165740646408039688325065650134153310077254858401505186534849743147769748550627987889296919725154349962871932893/43770085311042305552962721340280415061467046675560874473353196088285402491502707686613395238628469276047359356552334189369379807576596904510942629127988398285724355487622925364545584522167908897994417070471016224839766407093319315616630622986990418288055277281582076598482245495286384916299366092091730819778474330056231721255971858615007647779582872050150892424938711523708391540523091449358167153263083520*y^20 + 251392710366982378480646441755946224307305870099494618693226092403114242066382824709478913635868295616229593683989372831428130395816477688282863544657211536460803542172108500432420956174135056740216724738002929907986629059896288955351384814716623886225141770212295006598645401100105658763240363154146512139958215063710628280570852572658363886607004773406230287155764643499956699030025849389775788834384439/3242228541558689300219460840020771486034596050041546257285421932465585369740941310119510758416923650077582174559432162175509615376044215148958713268739881354498100406490587064040413668308733992444030894108964164802945659784690319675305972073110401354670761280117190859146832999650843327133286377191980060724331431856017164537479396934445010946635768300011177216662126779533954928927636403656160529871339520*y^19 - 2774490588346538620734196471840250813821402795076707870610877679552802539345093905127954988597477273453778042662123434335441138797680919273147363101204008845299011452491911818152620090841971588630921951346327696738601647957915563284977746665224683659051738437059081320543801335232048063469011937599162778941559594983301780210182560226060804822341959399273947376992981032233111808716073239606524482354821929/17508034124416922221185088536112166024586818670224349789341278435314160996601083074645358095451387710418943742620933675747751923030638761804377051651195359314289742195049170145818233808867163559197766828188406489935906562837327726246652249194796167315222110912632830639392898198114553966519746436836692327911389732022492688502388743446003059111833148820060356969975484609483356616209236579743266861305233408*y^18 - 33708833500525860828584233966866236927472487515082248811159369416792653489380456274304235906199533596068985520482990820244697998186438232078673219947497942089594600999110959041270783171384696100007626270851963780571617776262984384056079809055964847282681523739506912914403959554430612330460118076626415099786361777663244450021142774986447863306143510500735334067399329850142405665882943521335989634867814339/17508034124416922221185088536112166024586818670224349789341278435314160996601083074645358095451387710418943742620933675747751923030638761804377051651195359314289742195049170145818233808867163559197766828188406489935906562837327726246652249194796167315222110912632830639392898198114553966519746436836692327911389732022492688502388743446003059111833148820060356969975484609483356616209236579743266861305233408*y^17 + 25829195770211757062834989052800071663121924427734399613377352630307843723788531382229616010877858957763137094504196017556028536116780689664679813773921880658228172176370169139184865749241206675945113432015753357372775451081092914856619348548788682165241733413903536246536231274125516556703666563824696615035539813471603681980368634217445588900743746719348186129386489366969938194029482737930091636027415497/3647507109253525462746893445023367921788920556296739539446099674023783540958558973884449603219039106337279946379361182447448317298049742042578552427332366523810362957301910447045465376847325741499534755872584685403313867257776609634719218582249201524004606440131839716540187124607198743024947174340977568314872860838019310104664321551250637314965239337512574368744892626975699295043590954113180596105256960*y^16 + 293112202933317662074277020215554884333089302693760646629195254562476195369979491757144495689348258529242321875879739825902367969155590222656900585787673078259247987790789227647420459107876232797344103277606776980485277878427642797972253042660957744392896417087714512188059697770962392549901868047940481455880412677638154602464647905271457213465101252173093173973623936546002858176530462164689793470879468951/29180056874028203701975147560186943374311364450373916315568797392190268327668471791075596825752312850698239571034889459579586538384397936340628419418658932190482903658415283576363723014778605931996278046980677483226510938062212877077753748657993612192036851521054717732321496996857589944199577394727820546518982886704154480837314572410005098519721914700100594949959141015805594360348727632905444768842055680*y^15 - 226838735542248778819595323085217360898091323619880048450310426839940403289972224948695652986766233835404125919881046275269408413939017555337531136678992961578568930938622579520821242673110530793530100892360113769457333052395700430127708130752124145400130621840489036408643811379048723325377915823851377660412403834800343803478270401508823914645830954831807180340765254957199636009360138945181780348461729993/5836011374805640740395029512037388674862272890074783263113759478438053665533694358215119365150462570139647914206977891915917307676879587268125683883731786438096580731683056715272744602955721186399255609396135496645302187612442575415550749731598722438407370304210943546464299399371517988839915478945564109303796577340830896167462914482001019703944382940020118989991828203161118872069745526581088953768411136*y^14 - 114068012745397474802401137479396534603447931667201417899972916363033418903374552411560647420898274622861490191645321743925295072643752019835462226034757601772915707773476956060196737743144644112190214879477285705777834195381453021237769681463358108924653885605848960611500516115832704657041412906985352491897567221376843044732464153316992083999600552883610389324320958138733059688261420461172273882712969931/8754017062208461110592544268056083012293409335112174894670639217657080498300541537322679047725693855209471871310466837873875961515319380902188525825597679657144871097524585072909116904433581779598883414094203244967953281418663863123326124597398083657611055456316415319696449099057276983259873218418346163955694866011246344251194371723001529555916574410030178484987742304741678308104618289871633430652616704*y^13 + 10380756111027240398354475205057731304069666532869192021499370849757228874108183168611020703963665888471541771260422887838977426004691867851514998776546967953302597727867871727222103193543944657007204447395402693063097487588903350813272266170475962588065752255930083518605882255705313137269606355930103012109329670183423796963791227120034134908546809348938588394779780727306026116562093125278716168825496609/168023360119164320740739813206450729602560639829408347306538180761172370408839568854561977883410630618224028240124123567636774693192310573938359420836807670962473533541738677023207618127324026479825017544994304126064362407268020405438121393424147479032841755399547318996093072918565777029939984998432747868631379386012405839754210589692927630631796053935320124471933633488323959848457164872776073525002240*y^12 + 196480778628402881029025119258904488984450785722788777421418091061833510700587375248744991364712657024211387495983593992486733111967266075048637402486343579352378452520458868530272328144515046901548215788814426168105844783194403219227805261375987147656032936526997867951098820765481125132144360189347220122702155098739999859194484342660981378140997553939593312893531449846820308246667252435772432023273630137/17508034124416922221185088536112166024586818670224349789341278435314160996601083074645358095451387710418943742620933675747751923030638761804377051651195359314289742195049170145818233808867163559197766828188406489935906562837327726246652249194796167315222110912632830639392898198114553966519746436836692327911389732022492688502388743446003059111833148820060356969975484609483356616209236579743266861305233408*y^11 - 4948130652664193446118461040738341531097500952003151067405906426665287652436335787369872842758079727004132875406768292263441283751649012271669178791481921426790036539504287448857355887604111323634448875432870570663278916294030103598257474122942782529707238977232738958911487596948241697555144174742022406092158013701632945185988144822207295903178598572736813361918168557225033796873074037188788048136183650519/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^10 - 3136579119596564386063977788933962002488532906856050362339319030610450199992383526444350210143453653709259452138250803705218398658168386524736692020928965429964722789595949427861110503512049509677215065518403161741019332917291218629492787622378407427016557968569979889261738414947192643514350806298970895191171731256081132961246186486634438426141225936467408961510891006564376456806852726330421203936214438469/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^9 + 674181716011579679291300341364565296461726245700893305490187057528630379265261701253114082794661595032499306823548937583090871243259713267580095545661225322077810218260180559272968178185276178365529929277978063582942664570831442810561266898534795519508660490043574417783382215257415489231802889913530628709193103785279689919735427221923641396879784662486529285278598260591576011273934847822111676643403729549/29180056874028203701975147560186943374311364450373916315568797392190268327668471791075596825752312850698239571034889459579586538384397936340628419418658932190482903658415283576363723014778605931996278046980677483226510938062212877077753748657993612192036851521054717732321496996857589944199577394727820546518982886704154480837314572410005098519721914700100594949959141015805594360348727632905444768842055680*y^8 + 164815908316954587684722050171754314632182462242815550709040532113766362844583297821911913504836104722860935579163518711122024937675363254726028691850515690768003170690174568597159391407501684748116860463642011392733009772911909556585668166333076246411528378328176183843020477738189321288513414223208573445894796486227485614430734953396400558993926755682729106562673738983714699038158474736724150484818703245/8754017062208461110592544268056083012293409335112174894670639217657080498300541537322679047725693855209471871310466837873875961515319380902188525825597679657144871097524585072909116904433581779598883414094203244967953281418663863123326124597398083657611055456316415319696449099057276983259873218418346163955694866011246344251194371723001529555916574410030178484987742304741678308104618289871633430652616704*y^7 - 138465909172605337649619907908545523408440471996603929193342737394742540508061114761321925786828413723147038045989922515853256967946656319218909787688774038927804072079880275791387887497502096615551153771641595846500773947623110442368105777719487076367935657996857391173702964296496617472080933910779008533299651705691550587567343814101891008795125142254014949009008368771408203118179860430300902343212516717/7295014218507050925493786890046735843577841112593479078892199348047567081917117947768899206438078212674559892758722364894896634596099484085157104854664733047620725914603820894090930753694651482999069511745169370806627734515553219269438437164498403048009212880263679433080374249214397486049894348681955136629745721676038620209328643102501274629930478675025148737489785253951398590087181908226361192210513920*y^6 - 834281827154374720288715678246971852872837308020298181015850434242077532436803950368184788923691220962732007504410940731314335669729271611031360302836828863502338848477070483821601488030973107258720437003183814230173232488773859881380773852534562496381971872973642632891981611199868602346697120010702991269875477127888756353941643826969048244513790174432125737376883949920262918734248976017935911086578579507/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^5 + 337547318082899012048763894499293993677543412422583299045814960608002892603264757181213721635545330097842044338327079025279417462528743225110843107871710682129171178847982028979970336011798724800526431892428922421578687798364424373975894154024378842721940182579327919199434623052106960700943808714358202239704648458952706205460112779502545757153453545044468031826942968037795154447604803874561500108806889259/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^4 + 265090205899308875401613910674640735440962406583359749731137283276786495051519616077555877845854754381439207141550228352599436414688120923359644725577976724427960511111680585532537086823617050077166825320665184790180763931602438675035200507452668005721581007968776245539219157354306001964010022691918062170898603333326687975888124576312403814438225437903886962718637295444940862168313610598861216953878072863/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^3 + 83792450071383328087053685187807648547379264390786487508046197997402862362371156945640492835822311556471983515251986139291113075292633563393788842305982477675687774493516236120092888163417119180658941443964394059375336535645709634539667314575752765710723102339056637221034294202112744241732905128590595318909475187524493839466742251462159866827632234090293214381712662755519545939250817617953280098935449029/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y^2 - 46848146659686562091314930525725475255577706796540102055813109834259406442899636263271416955762746208051490347003039382769313091087496118430721769681680759244824475491283962659832322633047652873989633762058524685141702825798872617709678415369938202110740605003207189255136185163067815997572711666584929716324441946701900539633278355833207758910981072507955983838978272659391144896125919441775375980493392349/87540170622084611105925442680560830122934093351121748946706392176570804983005415373226790477256938552094718713104668378738759615153193809021885258255976796571448710975245850729091169044335817795988834140942032449679532814186638631233261245973980836576110554563164153196964490990572769832598732184183461639556948660112463442511943717230015295559165744100301784849877423047416783081046182898716334306526167040*y - 10025031859601017949384529603358511804329143962819595228081784188740191035572884647882443568838854158680175952675538713564395699829911535165694238248374633455922612591766412959807996679037369526506349066667442846889912195126733277650774350269395940711352844417266981345264257092637306088897075587737558407691316659843619253652858130739708581179149895088648409130148423500778612156656063419339886472110117/237236234748196778064838598050300352636677759759137531020884531643823319737142047081915421347579779273969427406787719183573874295808113303582344873322430343012056127304189297368810756217712243349563236154314451083142365350099291683558973566325151318634445947325648111644890219486647072717069734916486345906658397452879304722254590019593537386339202558537403210975277569234191824067875834413865404624732160