# Manifold: Census Knot K8_111 # Number of Tetrahedra: 8 # Number Field x^31 + 32*x^30 + 437*x^29 + 4539*x^28 + 35155*x^27 + 161718*x^26 + 940881*x^25 + 906500*x^24 - 16119514*x^23 - 12950061*x^22 + 164041324*x^21 - 130052232*x^20 - 486005421*x^19 + 799837829*x^18 + 258893131*x^17 - 1259806023*x^16 + 585232619*x^15 + 564801750*x^14 - 699511088*x^13 + 81797330*x^12 + 325491493*x^11 - 140655196*x^10 - 97768389*x^9 + 50295898*x^8 + 20699564*x^7 - 8770428*x^6 - 2421074*x^5 + 826306*x^4 + 128063*x^3 - 38176*x^2 - 2294*x + 639 # Approximate Field Generator -0.390948522692915 - 0.250296549317260*I # Shape Parameters -90708972232186602570692553446884374416982081889218540750993551402380674929574392651931113525350981532486166272622791838344660573207366318842917725620690150/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^30 - 2929014193202762041623087957209223262829452359698786306540908918727224474535600381870029925245709637912783545125961410836825012991936020813801785484320302208/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^29 - 40487893851712018832461163875001630518533346605066859398199118004006300785937399239527060173743861554416918624463482275238169388353708725679746324621325487756/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^28 - 141137937760438618746335758863780752187889396438752511444610016251459191729379934749975688123930644187325698746841678069709039606062339223936493436182713757532/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^27 - 3310869154066037086281905707556184258166866009106865838991489458924366283715382128135756717434526076506666546320406173233447949834968676508369484215437376715904/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^26 - 5206963494322181528956799805232923061613888746660724611214377845938501022559698145394090823737234862071101592097981026364889730733792052849197384814575847943290/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^25 - 29935895179812798334312070528487244593979826961587177868284337104702042729417445916026878549658551346087709099847478450569403210276370508601125967672280753355503/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^24 - 107957001487390635008473258466406668916354290073956280939315792577751342756519252264187027599019659891652705807711932373622449421671948325072081769347281068929139/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^23 + 1432801597992824260155265561272092541515274683331088983697192964855074498457584349630411596579441070896548833289124084520099563314525297402775363015957302123015088/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^22 + 530861300513956853253584580571169350957677055973258942560576956996875695167129860952614342464643646099593460294238615021040047956564123498617543928953719139469656/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^21 - 14450236667529220328193173258182782970162627172751134730395494857250551001153602963933570699116473448144767547571217727274200515880979172498518618638684977748966854/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^20 + 2524662098246219305965673696502256960405584258577679018019532573636889255497079254721609695105992181455743731352524547377288261690980633502354975312739448132606597/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^19 + 15537329121344640108677857530744698494931499815160614159706870441176819432704810792895204496166758371257163588763884190761570143213376032727809121362206367081409756/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 - 59263333988290213808895181650114515058994924704637647064041813626225114285975279931076577773024781008933378360099722076474554674497221451901604546460294634277655346/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^17 - 41668501962071315189633094545996476297923352548760408664813706648566486067767811643504165277471922580986680609502177888732066388124267678666317008620446075734068767/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^16 + 34571123888240247949514610942751357205830721802867978655460886968727229796445041742921870380585933959007401400114357133828987047645619442981341482978353377088249070/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 - 22406121375210802413767921121227711186732492488168052439321558628101966573700397604884398824391105358961688790995821617658998326635245419139954350401147126216554384/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^14 - 20051543247759764011089632047399632588700414348617030500109373930638224614028234976593317023237998266066612104644852217546818090685272791197249094828621154101624769/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^13 + 47044578385479986458872213278779003890295988603301239325486507150484343140108123294710160618708422656778974484686910602320968609395965545197606367983698783424011757/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^12 + 7313750589274584925770057885008206619239588272758384874491824130705002307406523281294700424679077530323351522811488626803198839876948504778327464011661892319151721/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^11 - 28692419154538579424242362572016003445392278472525969699349907339828081162584388241332570627344717229830065092602117297092720736846763366804019845985063320262282088/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^10 + 4569558713959623697472855152305895999099785582960783789792476094437260112797579095378047588598476139831750408704067932488464601550359109266449796015517135836107436/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^9 + 3597984802236280143000291293221584425525333324775865496770273673172341416663920358155300510608617456517405814342393922151856485224156041416879196848342980920600759/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^8 - 1668799280451122494630857190655389649208762088524199105290486910944572402756375137438895856089103304215304351468153512644411881592076189075361073158696773523730659/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^7 - 2541257195485833147500434038319727463711165973518538266233933524010383030173791438931266293039496816993470949381498435725213539906724750710138668689165691423361575/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^6 + 45739412735235961786267485459693298898912507996350248117405322689110142437586188512525188603798824735174706717349968312923365967181802738152806190102045685170180/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^5 + 295857448499792160125037465252294909232254660149300941104561196785968627566548870418437474698500614789994034439060095253259240744083384067907783320853584992772997/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^4 - 1189856522847344125803431012870525034302531958282998098667411965524280784787204610524674440210429411827587416566752402634865127651015023922382411283072776328336/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^3 - 15617229461023498794462740961488089846248698211511489445350778584617811861325743709112796810321453464019401533400643873254275241476596198973230857279938387233616/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^2 - 117459844090805088134435216348395121513217533870383103437512707395758120097632560995373951346920230474196192906058663595297698360516054353566673720175553599497/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y + 301474157438806879122713020460983945173160866827953979839291653593434168543538899786424889825861889498961556761683969431912037914372712638471342108006705810590/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173 -444747132471955924834462199738741343911494148259192273535644223807353480278311999798380363729509128367020781778675373030728279424600539518706488708499128762/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^30 - 14339382919645474200085636166859532398834289544233064629077085901383393840437580512197398876662014578086333219185992826317545037957528492824683085908463291993/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^29 - 39564061451641499771095237168973995995825485161675255559292725451914272652206171711915823717552684712791961802564671342576229585972787646332827809934869369634/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^28 - 2066532285536553385389541583288733875451911332921834041789606738622782267183376155903255479541181399093591962019898776414081071359396062615234538818032805187928/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^27 - 16134764215143565733321914214620191689907150389199862741421113176829257631569375919851976110293047207089434834282736392859751890851509632987555111288635952990686/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^26 - 75825730126220850574654754812068727744713787956168699353297163130359425199981433700780483331144897264205247275704922725675856862524922234247684605129744764519743/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^25 - 436802024454219281408904451229118862186423410952414912584536395677387388881925499954223212117111077590225113502142395315836605997616740918166034480935391367084003/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^24 - 508834988147786099086321404000150830310518251648032451107485320864408724109883787125635303747719930044672397618097118593110970459350701655802645830293032242598241/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^23 + 7045477835823150110562350497632005309227638140637948299598250053574559826233152609955833453303024538805725820715369577939783670201936543128844846490705162789815671/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^22 + 7461150266985718975825776344977483650704601923695016117550881185068967661652977737367307941827297441987377690211314975806205204519089945376165324859621441688364284/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^21 - 14228772471002275464858676212857959157934978088457065514252127553571031452557467539422715714468194981655549052832404676693327703545277597789671113025949560350311845/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^20 + 40661705135647861969476946967156603878890618338256428960316786180373441345220757352821990017365217197024607733997525152448143743276924476623937897182051374095758619/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^19 + 45175141597156848919418044025183004788310763743708472467623413573596750504054313748944776977229631901387513830778226950918635229625471557644508611262846115156752260/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 - 301108593867059101366436705254513265037828922676823384678341141628709826080959634421580584576165608436796400761181991484873887322727194504612826947026854596278626483/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^17 - 187572708007545787891764844727975857960318399053125788601714438909598974837220055085677485861884080336375330551400347352387794908614751996386953977171049882926653743/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^16 + 102924474426968421699620172929262896665328734330409611843644141696694448260366962855829386735599221951623454987400189588853385454466511807460897544569357306405395607/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 - 136271165531117561829969585534713078302439394674017492171082461772578386691468379192064706282883135214694419616914917234523572268988819660963416184944125728948303143/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^14 - 283499549335614475403555089868793876936642306808848800957977089987928523588302930043117359323805075175942283836677134428760752502557617179834877221564954118312692336/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^13 + 242564804588633769882344461854121944757679954912784453987449474038430332389828175992287088473754726894935005903965706416444510994277872614994604825805618409166697404/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^12 + 21860052937506414839388191896677488063327827877236600024163689079048598109276503386609452192840808034186713018760412968380925502778522208854805717762093106010990373/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^11 - 27851592101609348841704213493481718522193120063391889691977337519687083433922869410158350951735273256720723028155973347548534891710369533349125423476501443146293180/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^10 + 28985630610886658589890710441469836652409477022848299678384324035850897644006014295329002922944736973061850465401735860463175922534886754553791149081996145297033707/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^9 + 50331073524016035939486658789698244564026692426567059658323416559264694473973327241623753876591920503648514324944937457923905241977030594937263877878931061985225222/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^8 - 10216883782324621289769510107050991734244058390222442547787051173736923745696147875923338518599723919633664249094146190673027590540661442774664078139492744305641062/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^7 - 11611854591544100743831838017031341110196136420361788253397971063212972878907836975853103862671454050556509173299947208339607674095004231621494346651908779170207127/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^6 + 1102942317962907487215154876846003374255747972063483357594496467113776786806107223012764231406356393724301447434984744861393582524695391396908907448401914722625412/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^5 + 1329792361201908444201476626772072690894995381597604400784762563974995596334590872879334024161154423313653153523723579754308497474005299690123022928055104602708942/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^4 - 49645293113325802474947859884208427611796166673943829876878261981520080005181704712403369572908470832360005750176403726286248365253528294474165610271163031453313/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^3 - 67992773833954995505438451895752935343865703146544692605889849951704480557015703028847643357181557135813351899202839717019808612700961021959326978256399772478532/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^2 + 930714363904655168788027533408637761580326264688138957429749878183842117063243114567143676062947304809839812045440263976359533625807821158084834141254962916438/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y + 1226029022407736205909971552320736598406709970234051136348519531551755470395671674159581553098263018437975859213476372978569821702770500300597256831644400918394/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955 -122258785561132630863955342145327313201590410310772183706721333931804674827651646011801927259125847043857093372354987001503670604897414158105916567269518162/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^30 - 3936396071707144326217180994770317985468132031575524659629787007845800432880560037994139501472647500776236447841352440200155715616261684399161032943662577357/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^29 - 54205505477633761065670492632627603052221670196056386623695061727571399314567365964251630078792931335640615792878770830310620039520966739483435818800524402350/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^28 - 188562758183071881006747067556497510170899590796017172070397682252502022694502217195678996282989203228502538978622863418706015198293120304614893270680456794696/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^27 - 4410468252973608244923816203424899081024300862596763899580561521180801219755347040631735093500326837062371327331051394211207223675909337064189623648471668918177/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^26 - 6883535103413195568695042606181664577610934536526257895577844889487253413146729155343674032193768931688679906391352487803760699588768878531320080656364602111516/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^25 - 39725409701577312915705015849187702359450763606807487359259002908382914517934549872902336743100716231852318751543856365226811593696254963484820517849473152522636/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^24 - 134674023256105594898125435706321700547244533008911266068970898764267840366146258222459301393321206512369290131663155618309508246239313104762261381512099519110889/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^23 + 1942227158322335441128927699696603440433545402114214282535926512577286838957369077514082413358607620177157069632633065532505121347706370027275945924407016895421696/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^22 + 654670257684030567146508577865626915603497929590625734044746449312103332015018775811666894913828831586652104839249341008281000644778283176590851760937041125334353/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^21 - 19637189952545773412950191524366341526737195050910431312338627061247510528397479779076505590941493231106226891709948430230240719117733018340690468173232288003160866/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^20 + 4019580180832776591590435528794677026788679449298782017762726953598468609552927792167996526332005083135019180439059721504280669233550671172873411824905874804973000/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^19 + 20495052908009911476168512731010408350132457405082912524772469815334519601812802355777149672279145003645608065858600140444417005912793279100470604788984649965042902/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 - 85464130967202431835685484268259406132522246698455328478175211495166184446444670603689225145095746268875041664277350912229919662198501047698755596866409240841680249/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^17 - 47556538791208817309020520144429757318996806263403923054559777281157516907060741453274708628044304171557310290067211233544883071194942126261116316473268653916902553/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^16 + 47760415764578834308720299211013741712114528748582188089893373744525987378706310461571944037396143993338527570365513342543502719147525892709839077212651718249001643/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 - 43930465547143014835350738820958422482993604299509283452125046234967859159995775150301546730049890345775986717310698622997193513114303203639909363639458351222500799/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^14 - 25171036020882665412771752263111367106411804170729550295542451487097987653263433794896950810356798098170988284251563232394876445981421285733335029056180178413983681/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^13 + 69776532730782648534361425961220164954988318402180591173566088234125513411015087452261597602403438560430705033343194931462154360967786483168520671065228246265956690/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^12 + 2725564346797018231839176544339029774479395647370098341657540679885000753461702421493115634562780844134833251787563300249604420653746646118964709053600879863995601/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^11 - 38117305509175439970648845408689053260136251713381742438672184693317008361854320766733355998288166419201369814867412868679910025823279413691574503317306729665665638/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^10 + 9608839755921310352038887619729100361583986436294910970696720742229006102811974351279633745598807409352731936908799892935760628285300826987770823179679689774086734/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^9 + 4432335608283691132955021026298653387053914152535707992268044506770158257063066065559340129566936733293708660130965179778664856909545542764977803692635052913370708/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^8 - 3336088475689754583298464613769851453815567486862259720017750176952971002652113099287673737278312368111153116278305472156848460504665609090844054368698551891252017/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^7 - 3019760213582155454183959220539068934587744244076505815429421479180148432063449783664753426411415695486362551234862827788289419403569646732260899158024010547473578/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^6 + 137408478362132702551011159614076390607091500476554286405469776557559195187664633036935547899007823368483302979952479872467274637716044088662030882269891926054783/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^5 + 342891070407680467489257770962662892651909042237238589967426092824679961137585738906869109979131558522990799853939459497054489378975721640626866057157719286639302/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^4 - 23615220245068130394710758277694617055004469416318801856042902402305814820760954549928184871601835434866904913406010760301040755145036285864308412578143351114594/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^3 - 16822006124777411289463558345907578216155038230692069036527253770775743088178875347433558574200626908111430269988529206604165634556603572330254592156056571244080/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y^2 + 572773811638359172708150840910353921372618734159110948518082047288231623847549934332841389759060193798980690978026574923972269153247535277381436824162856860351/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173*y + 269170042769553961141470523570022720069066601697051431315555644275866148595732377733537720676755057164517294268884937719530015724451938053142256779834352767014/3458946770605482034457686658442757782733649720393487633292625322223964706073632003835748654399948414612434497012713957787384718691056805284032064089944272173 85973758803240827307508459695172078867840163366397617669666377282017466054389790548070073210977602039277202010643895916071844812468571172089371833460015332385/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^30 + 2764905991724273877280966927304790359148656837593110599192571669035601004210364314153953975313365939715216861973742596698003477890016892179031874145952141323822/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^29 + 38012593387587833142716253838792265804763727050229902447061604290081126910286363525096426610498795482966672571433071413423987464804792469843729012192834241129780/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^28 + 132104120879594101182960779400751529273776265501827450503454961207310427989492202783124532039554758222454140085452114609721640047062985147940389752913114169780452/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^27 + 3085768108584737016832681861324823690050480619482983735265721887295956366062731133865635050123974532665469934801463513379411522873748484388230043184616233870059216/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^26 + 4798941824721364719809605123965266783042803206491702459871854304212422796949574797145180605614811027781273774427765950218017417635720783936463171126188653726916591/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^25 + 27730820601911176160623597658597603566223664996111829896440035124928173700848736958800166226293074984271338869406275110835306138937023125630558018949959894778790185/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^24 + 91232959733095198635865404427603882724408234843109517337888480150829111128294916594701331096771495420881199035327988334747006472028218527677008798495015891396355715/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^23 - 1371283846336312833314980708123432835902880242206516140319577850512952139204754716828653586125878097684490372126159887899196912987142545372257035744839237271367569548/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^22 - 444233209306696603328524540024916776802772184411830367111287247371050835297260508730020262053568409360528737031029927103534830274570176999177933221449086853115367870/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^21 + 13890071129963075873826978550511382901443133581694619628415359710903788276541169262434910383229435987464105042510642200706790941671175507401092240640484994348209921731/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^20 - 995423807247020211509111338015744574781487749862491409907738490227772098584266049979680376944324146038576138086862197051277234595354834049386001221239150825860710192/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^19 - 14404877964826969140000902668667277478789484992105819937094262382676119401569134143681557657156355221209698598717552926924963605108791828430667700083206711654715773392/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^18 + 61840680853954774487181333903256816631866834925316867682755174482093528169917529460586323380147336285366334195771528199231328159261300289889210084315412915306659972287/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^17 + 32155582478741331956561714555891437189886134620922805920218939940469004760927974220342501323365201946627373139290362390447183747642056429327925900211252413485663973734/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^16 - 11458144541516127506492146348140242689288115263782524003915333617828100457401297614770450510750860569422176032712049446729141963842424274505634306570492031928602094882/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^15 + 33758573026562026747711282726916133072632338659059723037565908535374079239241981423767304538154971188730010379272057061087610527043977604871141128840832327991983701950/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^14 + 5991775907230422165698887249143701037550009511781793491885168390349406194437434770671654020214822402845886044247538623874400678290519778598132415391202156468666794893/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^13 - 51408618556087094034734585502385322488434445251499567653593044785785075141629138978005823188753212222669128760923097271611020885020856974331247476874672464939715309269/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^12 - 1229532191213110870116830534694630292505276304834039874712290656482916512616215044674490279438318810897081559252459288633220702170934816312799853225902800691925507819/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^11 + 27736944072990133499191625458112917039372226041136166823988748766218530853003794760822116874763311591351889262016236214827447000395789082273660479968069082841929033466/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^10 - 7603450588806191970426969192542811069338890205949029273228920469733472261808169596544236739222038223898875400631348894895002782023752941565105182245474863499397670240/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^9 - 3208245053262517408114195137825865135976355563417644857605947807883728940330597663159733312694200171884087016122281561432360547794669148151697474770912478046844813248/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^8 + 2758954684600797932391362627630757573289752647093035289722546290996750607549363816769764992001981569421259187904390197587887056592203209466380617135061685145589261969/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^7 + 2229444275776589586073010993500721861122271559133321632037146166776041436976521416188525117626205632660287726424529146893908235627990993485261640932734533583365762170/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^6 - 43216495645683940015471146004688061141764060794934898515275412936937083095319403399738679376859987518464861496351375286472911972828042362668564849240278365590066844/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^5 - 272964604917462646398606762895510394337022960902111431437585088834703731992122784060353387751067972704808187995527669274414664838996053788716872231914964782814280183/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^4 + 25508140078412059579648732391678845498853893429528509799131806902478918324635536693057906606153627234213179942545350159266000264686587300684109571419039592735158361/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^3 + 15360990267273639465219617992578900109725215691702806481469385137463931559741240367563447416620620828908432260228320311662879461286321097351178257345537852103565887/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^2 - 638745267400159501686585268197297527059816436049510125342732281238401339917503753632536602521715423402973654141502209245990482249507150889763028452902651362553861/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y - 306473938072575217608596688743702136798986813977988951347405194720724557541184526609903534519708094347300287263519509030866620704174782359054699945036882767122944/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849 85973758803240827307508459695172078867840163366397617669666377282017466054389790548070073210977602039277202010643895916071844812468571172089371833460015332385/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^30 + 2764905991724273877280966927304790359148656837593110599192571669035601004210364314153953975313365939715216861973742596698003477890016892179031874145952141323822/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^29 + 38012593387587833142716253838792265804763727050229902447061604290081126910286363525096426610498795482966672571433071413423987464804792469843729012192834241129780/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^28 + 132104120879594101182960779400751529273776265501827450503454961207310427989492202783124532039554758222454140085452114609721640047062985147940389752913114169780452/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^27 + 3085768108584737016832681861324823690050480619482983735265721887295956366062731133865635050123974532665469934801463513379411522873748484388230043184616233870059216/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^26 + 4798941824721364719809605123965266783042803206491702459871854304212422796949574797145180605614811027781273774427765950218017417635720783936463171126188653726916591/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^25 + 27730820601911176160623597658597603566223664996111829896440035124928173700848736958800166226293074984271338869406275110835306138937023125630558018949959894778790185/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^24 + 91232959733095198635865404427603882724408234843109517337888480150829111128294916594701331096771495420881199035327988334747006472028218527677008798495015891396355715/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^23 - 1371283846336312833314980708123432835902880242206516140319577850512952139204754716828653586125878097684490372126159887899196912987142545372257035744839237271367569548/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^22 - 444233209306696603328524540024916776802772184411830367111287247371050835297260508730020262053568409360528737031029927103534830274570176999177933221449086853115367870/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^21 + 13890071129963075873826978550511382901443133581694619628415359710903788276541169262434910383229435987464105042510642200706790941671175507401092240640484994348209921731/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^20 - 995423807247020211509111338015744574781487749862491409907738490227772098584266049979680376944324146038576138086862197051277234595354834049386001221239150825860710192/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^19 - 14404877964826969140000902668667277478789484992105819937094262382676119401569134143681557657156355221209698598717552926924963605108791828430667700083206711654715773392/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^18 + 61840680853954774487181333903256816631866834925316867682755174482093528169917529460586323380147336285366334195771528199231328159261300289889210084315412915306659972287/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^17 + 32155582478741331956561714555891437189886134620922805920218939940469004760927974220342501323365201946627373139290362390447183747642056429327925900211252413485663973734/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^16 - 11458144541516127506492146348140242689288115263782524003915333617828100457401297614770450510750860569422176032712049446729141963842424274505634306570492031928602094882/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^15 + 33758573026562026747711282726916133072632338659059723037565908535374079239241981423767304538154971188730010379272057061087610527043977604871141128840832327991983701950/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^14 + 5991775907230422165698887249143701037550009511781793491885168390349406194437434770671654020214822402845886044247538623874400678290519778598132415391202156468666794893/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^13 - 51408618556087094034734585502385322488434445251499567653593044785785075141629138978005823188753212222669128760923097271611020885020856974331247476874672464939715309269/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^12 - 1229532191213110870116830534694630292505276304834039874712290656482916512616215044674490279438318810897081559252459288633220702170934816312799853225902800691925507819/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^11 + 27736944072990133499191625458112917039372226041136166823988748766218530853003794760822116874763311591351889262016236214827447000395789082273660479968069082841929033466/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^10 - 7603450588806191970426969192542811069338890205949029273228920469733472261808169596544236739222038223898875400631348894895002782023752941565105182245474863499397670240/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^9 - 3208245053262517408114195137825865135976355563417644857605947807883728940330597663159733312694200171884087016122281561432360547794669148151697474770912478046844813248/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^8 + 2758954684600797932391362627630757573289752647093035289722546290996750607549363816769764992001981569421259187904390197587887056592203209466380617135061685145589261969/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^7 + 2229444275776589586073010993500721861122271559133321632037146166776041436976521416188525117626205632660287726424529146893908235627990993485261640932734533583365762170/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^6 - 43216495645683940015471146004688061141764060794934898515275412936937083095319403399738679376859987518464861496351375286472911972828042362668564849240278365590066844/81861740237663074815498584249811934191363043382645873987925465959300498043742624090779384820798779145827616429300897000968105009021677725055425516795347774761*y^5 - 272964604917462646398606762895510394337022960902111431437585088834703731992122784060353387751067972704808187995527669274414664838996053788716872231914964782814280183/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^4 + 25508140078412059579648732391678845498853893429528509799131806902478918324635536693057906606153627234213179942545350159266000264686587300684109571419039592735158361/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^3 + 15360990267273639465219617992578900109725215691702806481469385137463931559741240367563447416620620828908432260228320311662879461286321097351178257345537852103565887/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y^2 - 638745267400159501686585268197297527059816436049510125342732281238401339917503753632536602521715423402973654141502209245990482249507150889763028452902651362553861/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849*y - 306473938072575217608596688743702136798986813977988951347405194720724557541184526609903534519708094347300287263519509030866620704174782359054699945036882767122944/736755662138967673339487258248307407722267390443812865891329193633704482393683616817014463387189012312448547863708073008712945081195099525498829651158129972849 3650921954413089193998449481792950727920081967849451769041586318797001345687360451262617234515117021958978766351849219190756013947106718441168396179656478968030/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^30 + 117807827923693727283399365721852843714476039711437942116216040178384348585412943972127568681249239627654729385797277134875558859552017158051212830158296535159589/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^29 + 1627019225738507985719498972024278435846459046600977258979688956903465279432330387970767056371147333602872233635075186938981927405427168984264387145609522252056566/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^28 + 5669149826668792820756192142748482853008805767788483773765371908018176615620970672894376061645175866562546560769380090634159842468653862932732736151771880015206010/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^27 + 132904594869557733611080321631900595414487236819542801202523147748842777797502913346461211623748831301068541661871015702496866234556787956339300628259119992118551889/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^26 + 208674463141345075726012318185316481101473613428853786570935133475804878483884777213211524841022149806125729351687010378923735547359918755171040722684383108987443902/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^25 + 1200918400328138819137333167424307348120291572590951678005256833902097557789194661703729210377628468877480257889415700874463603068737295056300685538202434789472631368/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^24 + 4274596526290475137846679242513494278646022860720568153123493671136951485268146863987369699315379704399563138563951594493985333234820603234563035598760998487725225220/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^23 - 57707844098506175511121559782190642985843794302808180121250807894254664775728169770022662776974987086093888065891579225244570571913431788175340733485730823020711042157/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^22 - 20915344462043597740759626928048762494834970486768933172606262659724857073076994391759227554974792108377267712234528984335521672259286983824953747079748517151191861019/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^21 + 582123489229093944856674324171657249415370479179676431256188676236890508770332766071569447352682365647121961083044479843206644825443615810461910819136044576727335048021/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^20 - 11806802833876073238904967688892832073574919166808168147044821853873385196999581804705558940161925091361862972236662116109094849860432618741347336776199831251549868348/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^19 - 620048753817195033018124059205751912895779727836447678103095976864866173325808852230255859393361879105330926427408274469152566565894340622086484623850349533755225601775/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^18 + 2421897871703349667676410769048358054763754802533389020767919162978821978352262704149474379451887306422482592028801188117122407958809283492940431953039074213932169753911/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^17 + 1595290115704156116582019150627181098896349712798965144188058898601759507901107627289287207563422998704421169803146490197248733020645293029107754856774577197953946396770/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^16 - 154572973159345110859157305183464646290010996105906347029044264293769525388881027589108536106520170189152151409174483048047426930484080956805141174720836976004042603347/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^15 + 1017449324937413653354450171846152860710763823930359781612707078576408258486885483059074835092199279423485279574527542057911003615256899617211200000365895320366816556562/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^14 + 86561098885562523172113557993259895035145886211400284617811428540738276285090935843931831454534404309723857176749020826651883748882100219249561489647483314678241376065/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^13 - 1928349308069930850873318261692511702038352573551354705766503401450659975094762672518601661532202765559196604028590362290266424004285686093530960460858321905222541036017/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^12 - 219309573426921501602070158318529631140817938325906535420050835034788413138837048503491544979149750828529804964723606086060139615503026423974208056658544783025813599784/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^11 + 1130727455719524645436797612524434514056944096014855280684246169998905615552669816500125079589279791300366384651173934248577361347454670797993372905656768817630252680938/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^10 - 210511837656938594387824697278988332443164453300993871266295267546188068648208539347758144211072918589744053233644772824785061486004413413353873056524484265700026472956/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^9 - 137985143092659219795173033552990533396790222691293212484905593968671525229133502528592344331902821635242949692337559474707300640635408247951142638281714879119456466156/2210266986416903020018461774744922223166802171331438597673987580901113447181050850451043390161567036937345643591124219026138835243585298576496488953474389918547*y^8 + 72842364058423464685369479844361645740299527589080996578027835412561809714983936844542736157160988639858707400062010631120066699341296643926072588788305017522625000714/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^7 + 95297461962798761917971988081592481179350695683453767963230569178630310981674353964770798769093326513158722965456610241545329583435738562599466175197659321550739127895/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^6 - 241597844544579673245704081068989619970194885585135075622173308753994857579143494680328484368364011462917820823023959032063994118277256550038136186386366599384502986/245585220712989224446495752749435802574089130147937621963776397877901494131227872272338154462396337437482849287902691002904315027065033175166276550386043324283*y^5 - 10631102661320624213254796856348739298846599857490517407872527508428670272329414004719063564342011769264967181520001051837732542548532858304911880415200363125716666805/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^4 + 170533984981211944516438099847116856010696645329803315123871347599001978946341722160684116323273597887383590143871267010958645011251298640954824432040659820276275965/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^3 + 517267061595606170603222336943341220592576192263660197665218046525641310200249832372379188487828862427994240622716260536485692361780624746220566605080913762139909126/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y^2 - 752953629111839274356771288752484886813757450758567767734842750921301648643820400048355032791301635202363195885002465924582177850622449756778225178683035444923929/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641*y - 8708339388837780590062802783422389854939633225314034592402334151321227481164101935899164085854663050406033711836658416916312602844196596967385448894624509493896812/6630800959250709060055385324234766669500406513994315793021962742703340341543152551353130170484701110812036930773372657078416505730755895729489466860423169755641 18278979603452417954391970646693371266508436691079886629065140839095873248199806561565299969739941201239244328753444869114629819407527005102806881419507635/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^30 + 588622898653035038190374373860092233579415751552979663317864589174876323794741624365652939673925313638042933177014093593259137834862521495569034534607004499/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^29 + 8106949485023055896074785895938443491055021544034892796482577179318029329683764926939698063452054989558452853208612041078017499158432179173929377033083433210/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^28 + 84608183407624091478824973328295873597997562697485219333154449269516785755005316606161825937187998701954079149506587125388980164494498820895016004310643822964/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^27 + 659713037842413462927585658363208453432860847386262577668744859892142092077916965995199182515621639627386539867173321058598250496353588191679840008393356763783/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^26 + 3089506081010086045622610009647847819962316052582469857085976558321893594661860409456794122979286984141659415544669795030401236375381207018734117813951662256318/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^25 + 17823503583038236138846024514477474160857122571890475997854414387085671749233691923654141826113283395787081821497967657824580113645459990349971075998065966937700/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^24 + 20173982593111174356753032878531836585974524083484306244679849475755362494761091004120521734324611694430967862673269501394634565239404280271456944302692503480205/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^23 - 290562750150871875292948203127293064037792754409033182206323537362321060991141390466975383547676801093218461571486884320679546524704837144073074235439873689808530/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^22 - 295555041843738107953876605066907393054693713373905957752162212885908525072782678280157826773683010175983078468208870108418364932712803136952416468486614266662297/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^21 + 2938027004197399520472046494421312981508806223407506409696005814582352898959127906604922111135823445678017070556647362394643582057702926162274236383154724436576158/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^20 - 1782177021197742162049908802834944711670105633377351715777685211152481954239534787627960982176143760326441036806303253326077333010648769606153485744515133989454176/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^19 - 9236058354583671295956673278369443876251035320365084979077568530501372425653456034571885338724954899616962891958026767678384661289802672453246428773384804358411495/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 + 12734833017057569103538375744072469932521134050754840304925751087565993580753998771301040560851882162499311559997177136210838733512614125077527173617930747836281286/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^17 + 7291007430814124984486767920977739529397713015610766485460362131989698700660866990397673792708001590036960207292374400657436742213387407531684800800976205488512353/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^16 - 21480724734737863058056793610823770312660567599729827677793841693572291469819536225445747361992311575332093533109802124426989542802653710605754549346646586098502574/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 + 6330070599599855813129759188061502327150997513109755157703630868555791891961522410815008617977724521665007619493016082377264332510099743100220747007959311357648567/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^14 + 11509062514301202449665399773684006287473030756133442215719296982877732639671098250325954246606631734086845104438232290706013629764161621753349861084510412060334762/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^13 - 10372980246763578245674121672737138775582883475496411033469026487057133183837474799454928867224230735689484950336966441068850719281592251601024936791049402814064077/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^12 - 580705060299608671866958637883096883229995519601084206902552554451311090263018153101729607195427522504890253981661610834615290289498483649579191748984540066865329/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^11 + 5765748969243073815871853948417079989133367594558946782532647465937953170598587288681266082437044412684720972228000793053296585450912703237203889896495192951511649/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^10 - 1376669283305391426844348920247039590972378368087183623382501701944293667549147006764041841918419220565163851934422060983586679650558160637629003738408243007302412/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^9 - 2043931735022828110207477427499317574196301888080985378463064503885084565369650855425562913774325164215479403825113552708254788398391066085790196146087427482480507/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^8 + 484700503884235518352523231303297551163377227027577586938784193153099042751863716508440851353912536196465850939525383942030802929461073811927557535900185581761897/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^7 + 471576883289219118158724554051017207474744099186586880875773341062728675687380574853665147468686716348676517169542128263098887815133819059368354798222660768601303/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^6 - 58330202982151893874572152179666644166851455960243818019433717920425444841962774897259759914346503965766380655376881502342542019062332699188591566367904085960250/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^5 - 54968617289630301908306011384000264416554919448415139167421632066473485635321415688426630006409039016209221743410596857220075118891983702404792388823849958393655/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^4 + 2957813975718776040399127197006113149337599533430861152663739008282040177119545222409256966616202400243071750523486183003981385898328553939401129085464898942456/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^3 + 2829657145748386698594242433423805658425562805789149003756870955229958951051286235161534882313796223505052509335762821734177137621884897400245478567072073745904/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^2 - 54097199122573416449543351842867422423903421689388002884944599688719151617946360581875023378165590486468300488112677759869002279216852506764667744014258492154/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y - 48769739016591123313469686836119244965182786192890235850672921153690671053847256444808765191043493887187590698106466069097554469252105151854677257928679032109/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391 181508543851456339488217564863792723267565197300710003691293668019185674262516407896949535098218427345518128701731031106530268306377430724254545343871324992/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^30 + 5852560703252735326317049039591263408516244771409708107851417908571901922232482497154997683966242206794499672382728058850539253459121521858973817158272760633/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^29 + 16149666967943818321570630158225078291270263380531898234430798126380415952155391092226995830242035940372320264934256515283103429858638141226217729194949013924/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^28 + 843604967369723377370598229313455594384835971826228592168135773273024293955312664281444035600863378021592686557099111169864058718262801446088783463242541007198/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^27 + 6587256466670601412500193728356946487641413614747519345666975489328056825644122790971798991053344432215632312367632199864502865675940004480504056741287236748516/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^26 + 30965549344458109613785252713134635355858524000265840191386106569782523621883574174584207769899812636110898969440995079513622701299448280979773131232596595419223/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^25 + 178373064521017066744110324074993818339131031601285123048503276516698336932286496699554336995254015947951277681665462945647801786004612685922302995428423866017718/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^24 + 208245370593015549554426298548378399843845871387582500574546327834406161416042692935109125925077893010646682313837521491375950506150385277761265166683938973153916/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^23 - 2873944976604547015359632344459964108243020119015465601505322305839928167798803371328502253348613475756534929626751572674557683948718467515856867552143456172574026/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^22 - 3050568949921544665165984724949642524080942321114052314159599098240924244169753416457212889302525411871892901577556455428279121202804861409210506192957890981000409/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^21 + 5802633821506969750143848959954459644610928812626308094947721421073751122883343942494735168572937286928725897574317641715365637402758192240084099733988218118611090/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^20 - 16543547083630930816633698571370382789203658299671594300058525404325323239295098885885127798302138433638409225839486711349956857734340448202467794104823789757631819/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^19 - 18414993861510883350704542763465713224642090987135218172769519071820522621885176862749716859797712824906387691195554195229225167382794669022335708692986615216408238/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 + 122595509345327474698239816032573008714664510820235072663002923322830526533064740041125425443995294927433701159768088983211743667279865737735369598419628754680323633/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^17 + 76369376078180677109655091821440889251606472712366390565563896063164888609819296677563313137510967743529787484923770384987809126263466288145688681843303217145055468/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^16 - 41849954858586945683602560693129976257130924161872441888831091515747562356543452759609121962496746796496601615682215819623452337650328707859094830676490914904347978/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 + 55521612153769130373879177964448161052986279661340379301162368139216087748316800636060145878370919313676611622425088925666617215189275620116603083903118118712673618/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^14 + 114808773126497072461123364258040316311637409752520012728073042733474324263320641020467326804786183872904624491816951276622798668169610916804778553437407030996990296/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^13 - 98464472080009860515656889308260312797506010495402721586389122255746360205003422695957324788910867960523797108595198385371295731197426743256704970897004905715686564/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^12 - 8596929822420371428386835485023440332351832588502918905540030602351016014084573902465727101689416976377897994128712257120856519555626755335353535910764369286651558/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^11 + 11267299057645243813873559056160330558984396341870983194076260531444960403481009543232582933335654644628071427310795737614940559430699950669346121547865380008526660/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^10 - 11738910345431995969951673114981731963901966226062265817114245004359970582998532913959103119864443554911759449439907603720906366023601262844800830825462920616474787/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^9 - 20298641986406630761246442626881877258397544364207571609055085202840808877039154393396475286493538778414123711059463764727480852885698106375199182363465961604242527/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^8 + 4068096499148673348468366435254846899362860465814513612657159908571088959207153953360283183584205041859913203828851185072325855716490920380562170253346243683393757/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^7 + 4654414582097538435078846662788802879268177590998415726993065346698839291165208508918130819862526300926996086225487677615178417930863678049693172535799615137697867/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^6 - 420867938010581550627732701779160407779794724307426629593555387972672723330737517041811263363063235976045793879425397831239032223141475643966313630037941676973192/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^5 - 523281723415420737284950006527837340414820191112503143298362959076227449313666796680603201516952414629414492659240765557224202377753666591313377815069294257711377/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^4 + 17202308805843680763529112547049146497870242037397018233612905042193474994921762147399440463742950171388981825345008529217457403627540125968673091342872327414818/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^3 + 25697682845619812430630059625758949894569592442216216718607789103569851972404236985040252370023598702814692484098517409531700550028519715697332790268553073761367/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y^2 - 262468137473512666716682190066721045301647377723498830704648698226493774216102734447546049750595059513706507865821332547836013685220013341886418259891383794748/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955*y - 425346394054275389308276424679602793709451243861090675184547171338835174374659667381230903593042480398267362679795068962766484104812867393423434172961596605039/5764911284342470057429477764071262971222749533989146055487708870373274510122720006392914423999914024354057495021189929645641197818428008806720106816573786955 # A Gluing Matrix {{-2,4,2,-2,-2,4,-1,2},{4,-4,-2,2,2,-4,1,-2},{2,-2,-2,2,2,-4,1,-2},{-4,4,4,-2,-2,4,-1,2},{-4,4,4,-3,-1,4,-1,2},{4,-4,-4,2,2,-4,2,-2},{-2,2,2,-1,-1,4,0,2},{2,-2,-2,1,1,-2,1,0}} # B Gluing Matrix {{1,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,1,1,0,0,0},{0,0,0,0,2,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,2,0},{0,0,0,0,0,0,0,1}} # nu Gluing Vector {2, 0, 0, 2, 2, 0, 2, 0} # f Combinatorial flattening {0, 0, 2, 0, -2, -2, 4, 2} # f' Combinatorial flattening {2, 0, 0, -2, 0, 0, 0, -2} # 1 Loop Invariant 1423282872136517254688054100756166343699402717201697042984787904095510271411204001730489663602533466482772911239622129094879341096089569594993699485240518882/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^30 + 45871135423905500815428644864734775497229278585926560253769243558018493187617447336583551176342775616101883157901054151421934069858681280762461129657871873053/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^29 + 632474651445123653687053727324257823604011518679101786959662867988170246801269730335171204492433703226096356887081622156138054757296831483156099476851574459745/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^28 + 6604871999288953132776085892051806525087214605733762036303225334783680976361386924478953729795526347856721540423803866303011820460476628434891123453939389075534/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^27 + 51544177167959007550291560157061039270127676626220360803419439370328734083291851995043432571518483876745296449091835033116388208097779010059298763520562173669185/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^26 + 241930398000784962765389825750845257562310537476580356879647822936812582813428479805200781329338394135447217807542224988964731906277292085601946054099041287935612/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^25 + 1394166517008047069632413760709532431579311908641247912657709758299827501553963653877726010833958891709603596867070519163092538190016863544881321857546453142696601/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^24 + 1607518656804918087706541872526909968106643494163779224126012577512275067120843669726634671373440401893987910588564678354807635834042734966454271747169248798897207/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^23 - 22586164161352623071586936383837913715402460844514074611097714588457611284524294139506244760195002554606103576416264854594375768937099188011565698438714985837203959/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^22 - 23631854065357540095226271088891094859212063107784710069652287696226520230093423420546382378293928710744137251373398785704064397516616475866765677543698395892699025/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^21 + 228178787175132304184841303065375815548082159339016855614772651374389907852244258748112353200352491791145930500414291422951732244942440125618021186896276807329444182/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^20 - 132519572861263708547526226622702819452474388156493883235387189328606092811923961932434976804591131003895585516353814181624981185417979636001175988042688061261964989/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^19 - 723191097431575172034022620017657880623789273005476935822417384794357445679517103873737423459244158217368326970592896522565691025439651457437634475340709089826830692/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^18 + 972151007127470100866831658054232375233683612210497812772293102308471303023810928150047571841738314902009282170939648707078420269613666702610018649780738061384797837/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^17 + 595210756071213760798998958092810699331905099401620560026619121241553929715996499497137752296312212840691451575328997189908017737443017197661186837962980989982133171/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^16 - 1657827036093736432218428846570591299839141024241451747582053003612255566118469142555012853563863473388421313470383609772555528610837634388527589859300753355036705910/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^15 + 447791485439129732241369868625372368676232840719494157914521289675665959047393747795421844109238983897699089170642430272597826259305812271348796684581943707844572512/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^14 + 910093241470697447189021483635068428164284935347529749982114882345779303277939279249265001886851378004573988988092624072377168442283736129797795091965891957904224169/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^13 - 785105258343100392657974820514899928625517728048003928285685542863209327789175953599136555658187173797727760111261377417934588318302742208551353524391621780943931859/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^12 - 66478048727762584270150449362261478335333164171779548669881796311992587344762185453213883070378810618779672722556480779332260334562230012463599420016768391312909114/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^11 + 448774265536725189889452486493069191119228816155512880060923005497556098284164415683862373292662715226197954267067217385136817843569476318921676558696767061053084064/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^10 - 95899940126848948334952640762531276902319609425760153350963072155669676403079659159390587968927660024797563646425888660289095006292784614233569706119480361067888530/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^9 - 161928513272288312898600572820879125767131316702371362402522655540593470386442297302683122754307699572523477121479686149058918597518290426540240735171011142542019136/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^8 + 33867447523512164445731189017340644470125857281707445173294894861443320865409019129416986654163769048691028668548602512675700459311223212228056898387517257370596443/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^7 + 37459929972751505248077455134937510174132043798657486093416149375511562207189041632906615916250626251044380569999573371802664766421772599520910342165353832148032059/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^6 - 3728344579815655017585659456356041805653145269119978411929856981145117137462612422534841076363369985387308507530352846781117750211468366128803330567303704314398422/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^5 - 4320207411141860279389473179649629661755422240575804000631102325842619764933656490369337524219794708879755424482608480051362604457877130664560675674504243277374430/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^4 + 163734705735986005063756579023132112871893308796700262810267174218078448078084098676021001589609184165006406965497315735191372380078105933718957437303244342869731/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^3 + 219902912151622823593204487418269080139546009862865513928554465523648783700485807420762915212402119336019783672145973955808388252340354903189325406345503996227691/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y^2 - 2580957687154767377701830219064644808163095749673202893801241988938307438357541722025499134561898963419370824976598711819497973523990686259363266875851044435980/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391*y - 3809643486035820756054964691198306875984746633146971465110542620790040143029312850897323210209855687084042771677822353798123343636919277389207099012882000253550/1152982256868494011485895552814252594244549906797829211097541774074654902024544001278582884799982804870811499004237985929128239563685601761344021363314757391 # 2 Loop Invariant -35633955372706618745930433302554433069494396801532577107460955457663179473671718634904635788939608673920070966508978382254578821624768464248481023095300761107373955056477240056435374424497992261253444788662585618863880728948142577339773148851914453042020409441/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^30 - 383052195421630134553039191918910992014413470593919768469019134906227851958906343990367166263254876055242366104276005886184521209662584785902541482191867857437887297071030098875013771268348924387438972945861915715842458961863805002807027816069726454648693407665/3913048103228743484498788253840268733470472781275305924408841181244714746109903684834796595100728372734309791099132913180295812043371561376634897044760094756205441575568978681207022572433269795047482042398536823086882428271982698457084255322748916401786646926712*y^29 - 15858101006238792412948596718181789873095721520191209076936098780692719460083731717345225177709890194936651979421802423092879031198988773847597556505623463746567030638408915590628675336886796797732715274047879195502160915757965706772778410623211723889983364821147/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^28 - 165690386409054035466062193817943418085381211295676631538097026855891270677126684322872957362666874664188909152895822316903535668188352756328320023771719542215984179571015454779664893625525248031290246662231360822441929087528227427880930477399379526525396549442393/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^27 - 2587923629707733203710974648975470584474854648582706135142609230353981813161018946641881200919112755271953352000930934942820833925662343426717430019840873898939327796113969126101820644159678765814949415098102225595497253931151597963051565126656173455677311890494087/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^26 - 6084812531917119250938361154450655928140520801328551338444619965708760298201494739666179447677654129258873052994616191785289962602386239163869123533628766902633415379440280633446458280050788080479256385838220141014449127143000010013098764094920171621008383532584811/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^25 - 70084943761272066847201848826337528961657540948495903761143230075431905427157416960533305612422337602415290168731321303381739120851378167566543009115846213948007423097851594427823392803824811528932294955940253479477917548341703035993878988454157747397655773077259119/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^24 - 41027466592012258821799361213018338487709638703811712208933346021221123125784461093500115306909809069762428517474718936976616093064184587944285604729285043783603530645331042120093432912137775535147632184059576842742680299727947483399539703607457108312876996202600523/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^23 + 1128350761679927913628902587895389619439273496278117391768166023864046325880939166561519571360608612015697164381426818018785281562392878165935113761271078531946221747638386361398293277464098089110775668274352746243209202218057505780001509940064672425582789757431932975/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^22 + 601878681821131649475104054889831491073617824377741484408437571986884602993544330745111883925423954097581028591140822785206225279105754413666383205696614364749628243495746717064309020543610053144108222265377629947744924980712293446870174808184097439808585250762438637/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^21 - 11390774286243254280741601904323891929993162963654077500900235978856707717945092026128047377101116013718456894200250025823803863686702180074919302204123070271635894725660834614577754689867372281498599946185969767954686984924523491926278658267035909273322858419790821069/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^20 + 3216912884578367516103396637501735768692397242049710836335891072409236385233538186450734143936157963134070186441427329826679399150907532214413630328161364932975752580354333568827820737582064917506803598038300872055355508150459823094659036449842341954088146662725884275/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^19 + 6038886232214239894881653121288849518815032767768425266631479731793301957550421037507441944771834325833176700267510735874646187689172417149340534973469188553277132962934831706081272648639096434280652395902633822831287343916636517082668553486298404454682819798709495803/3913048103228743484498788253840268733470472781275305924408841181244714746109903684834796595100728372734309791099132913180295812043371561376634897044760094756205441575568978681207022572433269795047482042398536823086882428271982698457084255322748916401786646926712*y^18 - 47983089720385184721594884133503245915246488486608158321725958446729359489439738639270130988649675299903998459042001520287668714601402816413407856565550191842947686052343360323503956444551407369049327738104773290917226646841084384312692264820358671752961004531116629103/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^17 - 10125144609168233860707251872208583610147638079022617304443319599425362741808977125493390917671265918560974874902665744466185218996972358843399369681332562723730953994943746895184905937684267107356202302182390633240922638349531058435916241999114911075822567653431129277/7826096206457486968997576507680537466940945562550611848817682362489429492219807369669593190201456745468619582198265826360591624086743122753269794089520189512410883151137957362414045144866539590094964084797073646173764856543965396914168510645497832803573293853424*y^16 + 27402324101847526242845828158191643593771335742302179477707105251834142933326518602831397535050610692636848169365355573295689648218056365864264549068569450359959549714417348299888802612770518867218891157559375296516762623469869250437352576305582420851216287523475434385/7826096206457486968997576507680537466940945562550611848817682362489429492219807369669593190201456745468619582198265826360591624086743122753269794089520189512410883151137957362414045144866539590094964084797073646173764856543965396914168510645497832803573293853424*y^15 - 3546051485340005601444374868801179766553947612189265628993533626172704211137325911333449709710409059983389692544654401452695822895981618978709114382182385267225603947706330584901393297620931907486533934926688926422402527860179788782905209411864175724806318050695973155/3913048103228743484498788253840268733470472781275305924408841181244714746109903684834796595100728372734309791099132913180295812043371561376634897044760094756205441575568978681207022572433269795047482042398536823086882428271982698457084255322748916401786646926712*y^14 - 22753050604281711844494804193901495008702173828634738043867236036160153366542032620424337480113393519916218727966061534438730281460268812495600188254124969172739557898897064729373001408509568931484532837611187953227709490540155967303812344353473724355805265620720531677/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^13 + 6422935263147823116794405160147745331927933192178688558294549344941903518718604568814918180283908205060240185507404247052055270339719206015823446582230919429324238926032639025621668162496939109966185560895899491930795278310092373071436435599843967386505466562998511235/3913048103228743484498788253840268733470472781275305924408841181244714746109903684834796595100728372734309791099132913180295812043371561376634897044760094756205441575568978681207022572433269795047482042398536823086882428271982698457084255322748916401786646926712*y^12 + 3721047178744720313136517842086752838139571883915705593508114016276463022704473973011843412227054065386836053137203035315074667999911328035949258323119263123342857330770496901030674533560938202527954345084390286591675677495073188690375492327392255172075151213942381341/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^11 - 7418312734432227118819993668414250420240453093436156145782678371178988031094830995339060240141895785164724083984490050983673295785137756924818171140375000188024164880367278134766558660649870718364803739706139701942377896208121075570457477600372441585659250982388793237/7826096206457486968997576507680537466940945562550611848817682362489429492219807369669593190201456745468619582198265826360591624086743122753269794089520189512410883151137957362414045144866539590094964084797073646173764856543965396914168510645497832803573293853424*y^10 + 281209234538162198882617747061768005912982780096809711147333979064578270011884722397465463321320459628851244254261922226332625244774114686525382198329269773837349371378580078378471026295123574684775532842269232036967459966545443483495545027684446760112297017212079070/1467393038710778806687045595190100775051427292978239721653315442966768029791213881813048723162773139775366171662174842442610929516264335516238086391785035533577040590838367005452633464662476173142805765899451308657580910601993511921406595746030843650669992597517*y^9 + 2690061636510206289357384038600941603273242419065738011384883398442058018277373070125384193068217578918005070243417394149695260599860068161980130612878141147004077561354116587533361834214535109061084791303500674671997749861152918246737990587013587918368075769007711039/7826096206457486968997576507680537466940945562550611848817682362489429492219807369669593190201456745468619582198265826360591624086743122753269794089520189512410883151137957362414045144866539590094964084797073646173764856543965396914168510645497832803573293853424*y^8 - 98521167786571770408678770654835480010055297206501535198361675802016898032037358979407388688519537361909829300493216557779634222046460626729533903509060651447364767044275763768431024176277469829500448087531164361493396490895254573870681752406880564659316417588418704/1467393038710778806687045595190100775051427292978239721653315442966768029791213881813048723162773139775366171662174842442610929516264335516238086391785035533577040590838367005452633464662476173142805765899451308657580910601993511921406595746030843650669992597517*y^7 - 929987064236759723189170650914131451530485101446438344993862068679860061691549126063055237137531160983217628159153570098836262106807312586854887684988316468440387340495833324128590789987981620653820671616129732834772420838805021666899854276280745912393421819703643255/11739144309686230453496364761520806200411418343825917773226523543734144238329711054504389785302185118202929373297398739540887436130114684129904691134280284268616324726706936043621067717299809385142446127195610469260647284815948095371252765968246749205359940780136*y^6 + 162009539109835360084904446793037412663277730022975513875732728212920797915469643511498670430673737947832207406598257619027599321539352421722419494216320440218148353012824918900216422571073145747410545870764612442357266735356757148221238099662144198603403029943765503/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^5 + 210965957837582177159733894202364377207553262479818169839718270692413597802164143375235878656288139260168608399140898219626763090098402473195984844072084386011995804021388702966879559475467892593405396353031251183979420796016066315578834899365262347791580600828852683/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^4 - 6489923058534308100419153902486900796441338443832838796306376089078307855625701055345837634975909528974043559389463122648592225944093371933936020804838098999129858707273104374560980451079816497186186007228080232573573091068242386943630517955254536411543761875598465/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272*y^3 - 3511159563382822389541624734582951429269262977955736860959912183246658723960391943347790165431998646828410775679155332533920936983253663098420319035972677617496282330469263128600075871889773266214816077687224113696339412534417807572014278232480233447707576082932909/7826096206457486968997576507680537466940945562550611848817682362489429492219807369669593190201456745468619582198265826360591624086743122753269794089520189512410883151137957362414045144866539590094964084797073646173764856543965396914168510645497832803573293853424*y^2 + 9167404751837155743655385855850206983938071667541659755058471151538695715275485877289927062921519556019418235571410141583244821189907880609409000289442502983937818524635963458899266860101906092287493648913943739395879230393555613031576719941193131415666522300845/1956524051614371742249394126920134366735236390637652962204420590622357373054951842417398297550364186367154895549566456590147906021685780688317448522380047378102720787784489340603511286216634897523741021199268411543441214135991349228542127661374458200893323463356*y + 190380833399365446724774213735183041386094786515819721711044806667737033121124215209055802233690483178545472563721659733048973254943315545936159675092584861457520349517145666604585218883213729192229334390812932407405779995062972572606087009220527951308026964280971/23478288619372460906992729523041612400822836687651835546453047087468288476659422109008779570604370236405858746594797479081774872260229368259809382268560568537232649453413872087242135434599618770284892254391220938521294569631896190742505531936493498410719881560272 # 3 Loop Invariant -835626198843424759638170888909701332273794788774681384484079412460055393965200820588698051453564273576901000643725336206344531301476095564779645558213976809859447083310092244260572066171238578388244893106059394350982557526073289110036178039085237625238776008325504543237479534016078532158802795568716318103974495/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^30 - 26941134894646038859010847198846906471827973759823685691576140886996922886070130437904604757737524034178661034644628295366826091270497485187437700998332138967158228223191812914356932772594757065771337956480913354802511513020969232589963004526183793189874825946535308372354015169789891087321182978114539081031311805/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^29 - 371655535604912522257708637210470785659373331574789319331282010753900108356038082142623971961964463312597482301469373935717100941529687910928003042577348885704955661827224213959175760885636702449947918274160778818748692685489969937430141813190178074157798627085938500053290187290160392842626221327955270549505727343/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^28 - 3882456252287796168684188025108299594416321076092726237032472720665393781020803503691248326592811485430856318421051582333219971129042667776931027928496074016022782666840101772273934868242195000336857699232371208422019192127474140438974700687853076494514664971872806145652682068999652831150695261966506831114241260001/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^27 - 7578061472471842732051637167202585871344411419888687915226625878132579725764446837523396033096409154238808379587173681110821891052150682404845562917466575502936340574349937815545213667586508498021078613236630222141938203999316777746480058322131690526544728530756910319231770773779487971114489740825081302128338073555/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^26 - 17805736489411304854937783251484447800797754268970676134105575321254716571011793520130435207115253921707080098721639780432699031097352030042948905764445965210940218585102304152449848890019349295121074162324168631925342949798375995395769734598922583592097699357763162497201587134413897523860845397035796916553228904551/80596554213463362795961098451921700358364374010076508505133598573513457442527451686871764451924363091482648348561797431018771728068185213247604449698635400285040612627752873440055029041441099559139578887746193667721920334947579724208937584519889028703871310369021840376378209412268726087894700466705359479662266376*y^25 - 102577932980328960568934164751196907729950401577113953667734609969731119468164471567479462861874236165898325934095104222455792955650218546685471717106976933830144671483697936744977326787724569239604074943248415468143374451530873673959311915385864904604838775615706445772594724511914197547557264699538573094059610914043/80596554213463362795961098451921700358364374010076508505133598573513457442527451686871764451924363091482648348561797431018771728068185213247604449698635400285040612627752873440055029041441099559139578887746193667721920334947579724208937584519889028703871310369021840376378209412268726087894700466705359479662266376*y^24 - 477761402802867081124694477762899414488088869048517135825452016524293218978300599642922370216875800717960627664601336915477646259373207214027733377518391249272690484790366143309585922425391416594080467025883956589926998215238283581417592328026508341741284387751255184684623006754709526058929743834106360886077539321295/322386216853853451183844393807686801433457496040306034020534394294053829770109806747487057807697452365930593394247189724075086912272740852990417798794541601140162450511011493760220116165764398236558315550984774670887681339790318896835750338079556114815485241476087361505512837649074904351578801866821437918649065504*y^23 + 13236777980262319660363003861762665680574053048306876440320263811116595083759820710066843043319054536870847374607117474477099253949639231628745382500296379849196831403485903888787731995281360222596371043558025447074013664650002186414529256848384622016496492662133747692041704288257094378731652967659951786951919698969919/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^22 + 14004050982937566830065887406608791705097270874739318701804929266146211816658278092086311666985209854206533435053712349373005747489891333201168767393740401823939179405262781557920953170942184545075285885104592362656557841256546158399693471319241144431131623269086908424439099283273241259058940304220066955597109916044911/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^21 - 33412980963431469303161564702312085684764073758077969893060603825788641207413752204877115713008697870841222717137511856155904519947473773223403019339006430136707358032634143158285751215892998291709652286666796224063563963392635422954949891496097789869920282822716385854698291243635737188727445696239284243773793600258285/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^20 + 9568986814764947524685224730160829448446043901795850957022067763440864593710133329111342223193287208492618536351242357231522277265185088078760691812366116848986742981906670509516222888457428250167730688577669446017192715402598107297706291344073686469526580647054301447491987984791675817841925411563578127032606488582733/80596554213463362795961098451921700358364374010076508505133598573513457442527451686871764451924363091482648348561797431018771728068185213247604449698635400285040612627752873440055029041441099559139578887746193667721920334947579724208937584519889028703871310369021840376378209412268726087894700466705359479662266376*y^19 + 423980365379583305136247102954623902545764072919073416022014788228876904267010777036772266515120682060782740508456188036049519966121022434685209294825439155817040856940682206274832738179830302133717547282109285961037843342625866420031392531675327652226941823385380432522652932890043016778395919807771068201021817446928063/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^18 - 565856985992355382246925967139000963074587665342824653347560998618132142613326353881395373554937693241969893320196114547686830247401616598890784321065993538206341766052087669181146845522757945941450894895835659729478367141273669774162842939743606707365370662583887005231199357226000150182354079808151461205102396398835561/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^17 - 350896675333741279498348263172918571890113549303133365489124449859932337994836291716702623992491439447424354723153795058762243667603903627162510552645188900978701087532231269147007646448982851937995540235538208543420991262174870518167135725862455147191923114988549985512711569252728859450432464266773511862028881380455957/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^16 + 965495147388032934534714533140058713727739151207914190080437050719121432344485179882431356004058706668963067762640704719431512194521409885808339757379170141240195828456183235680923534252853858690915582989954612421288617276349316738988959997876734076444450055746540773845206400700372440442538473872945613508676826761605159/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^15 - 64347599003230896713282069775921206822520654279178083408502108307448783309153590577575150721430608957402784407839851878494572357565163607476599434081588742149346581506026706477371440019958269758502353738298229622020059480858706227457712136261215106482428449539382785326377791160258888454693673749051532549280254325051929/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^14 - 529719636587679800013259823685658982050142662196730521007663274507049388683637624116962275598283329689296339472248151892340282851571346830359029003616239660902688440434382722876999767974420584508015579370748491442680161867550194367658726089448131362411017065258812008608633064890501828951836372380439758038783988595327137/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^13 + 227453411527693976402075801669338449032151429214959817080790848920258921302280230232455816776821114258897745715869664443555041631910314531178960119205900847359011327330378666393653776029102479594889228612127741377292122312880654245065818621088481258077916168986025806371822130877310511109299496151408143515406817576183339/322386216853853451183844393807686801433457496040306034020534394294053829770109806747487057807697452365930593394247189724075086912272740852990417798794541601140162450511011493760220116165764398236558315550984774670887681339790318896835750338079556114815485241476087361505512837649074904351578801866821437918649065504*y^12 + 9877060291821175616605464509078970824886729667994290043647744398750864270477105062092733098398941031402458546802667811744512321933337150833767070411142324294691198842795222099579665678730202768820447631436968909223131887067608315186258646220120661331552444210999763286499696686100142401291563564587715475944663633155977/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^11 - 130111782479817312138314790211757110103805804945034902915219155838746985734592332720515840079105232023111975008817279875181502784663921423208369261270445499010674423537250984908863962855224262644880918432797924616024629676679775696512612690095578606068186680527957432634668719982634651122277963471539717786239443479899271/322386216853853451183844393807686801433457496040306034020534394294053829770109806747487057807697452365930593394247189724075086912272740852990417798794541601140162450511011493760220116165764398236558315550984774670887681339790318896835750338079556114815485241476087361505512837649074904351578801866821437918649065504*y^10 + 13621403549605993752182884537206707160695827229034569900606685966329627917688273685587280021618580944170353591688308865775341110163508139212200014114096087263436614170598904574406921956269315029335370250044892764406160059305008090676965513113319735787211275411872219489848466951310177183116704305511603638481742800546517/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^9 + 93863201448430426040453558543013699014034563738327349011022393528289651574935480341875882965768659577387938712862422851150862874930155619234784069094500114206461464716095046653195662783456896165446918493399782583651302782067673905383856427411952566846098539707129507494052725408192160961670054568845634131606497196305379/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^8 - 18985366687052860484886885796554231774637716652902978868274719639321077732473510406707525093693148239613605509240696249707506316747648858315823376134186040506322545245302975555398816475263163625065944724380410518500182956800498542742919402523021271455735996995121186204353062956051032047643346260364243708839083668503739/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^7 - 21593250747623376866192376951619160029138784305677074119346062974408862908169646079024473889346073322895981256430982787719434020616515270184173071528550845868064831809913085246802969389701565920398281264982900953136549939328488594594719700830428682146147835591361813816242932514180193584309766213357885277363129371666599/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^6 + 499360969000524873443721986825348239534446838717284939409363573522864905357960990504388509886913214518196733889228840499576108796409808505259000397809608213005542360797596198378123024859715562278426950795262527311653671174187444871940047716568587417038738367752827944853476375027933340433643343176263143356794399865497/161193108426926725591922196903843400716728748020153017010267197147026914885054903373743528903848726182965296697123594862037543456136370426495208899397270800570081225255505746880110058082882199118279157775492387335443840669895159448417875169039778057407742620738043680752756418824537452175789400933410718959324532752*y^5 + 2448962860393146542155703029316827129233609804652590013652953789687033514786915806081093902622654049804178934091632575972793277041514866567014677860402958261169778114631513988043894457125767861582880370072395284051334966038527339940802644041653266559701002844160797955438780417771316726077094575711864805177770424048511/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^4 - 83695904574420470727798527525658390147532753547641840655457338922812958461433639962382204227240675375637753468023734242078281014955425473321557524962490263114896403973196091976001116202936968847930188678524094035068876165727645655792451004889717097182229496358890803341493740022425120299112839987488842619405226335029/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^3 - 122338361047581616108212718433187546048409708329452477994795486116712151929856325430833827072652216659478220158061133726383641706292056049889691970384980341055008127528673496205269691603053265907706323603835065653835293820664512324916524398359406123691477222290166619787558271682097678696920403872228516995100864170519/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y^2 + 1403485685281893510272438567841722109984176016273979350050905194271123171558287662360120808624815757780314889642830032006936244412440017959138934306165460080305264012262418458746577199908715727541938423894578013927034527876173409432202086605874407420584162238497946056934954463499754415933552312346414133700002955909/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008*y + 2141362004476686335894121169217754206220144019275736749162891907304850237824389628287570239207878508492337454134333729690502877898158090074137996246977306437372224850667838816604357087279352272513798377833097789894918990972987940830608770507765988759801889635740609122938716420991348117122850184892703047570785321987/644772433707706902367688787615373602866914992080612068041068788588107659540219613494974115615394904731861186788494379448150173824545481705980835597589083202280324901022022987520440232331528796473116631101969549341775362679580637793671500676159112229630970482952174723011025675298149808703157603733642875837298131008 # 4 Loop Invariant 17158106805359006047559511878198278812274314947086246200755014138153417127325549235595799556407631173033996871707166986670921105464844149970346129177427479309074572965878508123601198142047873936904059505828982428281085904445867928417309101266178331732225793267878091383189540954941461778221677457395103043825969288629427503906639456011875004540615098029109014362276249146742030195145516730019159159417471168380408213949/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^30 + 557339573978911221732699517873347280301410832639767431241017233204257426885271210625179274390847411867876814015885659282349788258976416849905535902337723498127927047805953276326601156087891307442121207059451687874856853562496292596337907014728964433365201430688438327130071216582704821025513950406056083867976456023303819667401272949138604482783643546018296455792867085763837938541464083292480481346257718788252788762197/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^29 + 1294141479128663280200856469734107357484745297092679819975487713682535105524142544315042207014729824067577298647976516072695235278290551271461981246102008069141268971274055830640023033084074901746483911936398581045982942823321023177431134919186780139849830461809948044054134314691709657218945273603285883725137669805630262079144549434057883185606742931024232478985480225001971117524097414389920237016031731634501941752921/32823907744946667548474959068281428263802504060650786643682639821923864213854666571825182739391091396168590479767596064197384749330826768547193971134481863323994955014092536123216356417977170581614472771967069258685522062214302152448163662964086514440505533365535922288421583153404990917957684995161709792084866167441672135143139356416502576157984320144936691447203880737691621237708573353340294523006213164830544123747840*y^28 + 81556682553176999132106291823124633869563647715898208920239990194825912554416244770351579546334258429255292656693837810964266815358898127612912088746111223418225209334275623377602142494296192563071333162502051626765494166840575471310849475448787233033731772273096631656331978750827448649589797943150916696762095985372690920796480354839507110751673743943498577664632420806365001564285227528490913652362653953117023921442779/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^27 + 641568582316800181103774397010766854895365672860888376067098482939910925336002591921636254707623662755227597703323164510010407634053803477114239445363586823891553824054134960205380228978351668904960249178389458287496618054325893816770925855917451509249861009873435212450094955157667141553712634604294820758764914987062489449679715428519112797663350846660265399040206305607752176445074056630499954151543709519334150595384589/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^26 + 768527575119377253626729903235190396073406466507403421749336979111378573595763763487751939829154098311831511736488915487426735622092938217789872536826278464806613606393936587105446619718827058078881539514159251741850995034241819868447356630833443120302538162460914728130938483267116341927979001930746542748823561677893027435258930673546733666364756563109904621871364631830099113243229786711502316805648123882024368251821009/49235861617420001322712438602422142395703756090976179965523959732885796320781999857737774109086637094252885719651394096296077123996240152820790956701722794985992432521138804184824534626965755872421709157950603888028283093321453228672245494446129771660758300048303883432632374730107486376936527492742564688127299251162508202714709034624753864236976480217405037170805821106537431856562860030010441784509319747245816185621760*y^25 + 17546925624932425650249647508974845564673510073691213747172972681832000372758007156347781623456358666773096068683922647989792658176646364559637355151062629874231187810717518114316087408513594443041175059246111952344049136093251449046043078233861706763478527358050111717274452875712486985788680211120652741575306893828710929301214908462014702291687435579949379072093530706007406438158337702635014879797768569820375339671475103/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^24 + 23642757332551066963388153955388465133352189581190535941637109704030682548971987753862041899356849922455191038226871799014352772742667249232155154636671012392014505764277749490295017864746927149185587154799791818572965438548084836982112981564821290015635729953797002635170826964003714011839419835095338364947080592997113790068317754460777624102073934548263389966518270244390800064594872089738709090578432901040356332428890287/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^23 - 267354822817445280449727258817626538615145759038888899182442223359351282019358526412956421789574487786637569426770072328592537241549384917810178740445251640560434217185062493188289414957227210833416102906845554988856841968350939024752312166422409183337401677396556881865022085646850533805312038407066520734001599677186996968581506754653665437040131563202688680600228180368214387065154504164392882581020988605430652988328502783/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^22 - 39315511374608765668902384330210161191466641090378055863418032637432458818791924282872562424872564919482652335604525572594965744035461280495483793138082823269409327183313522535810244579734110055123177694231833755622086059011707979954074731829826388591039204420010814375176804998076616782181019924264527892402514684380115732871728767661173114423260753392335817592758492769038067200661207065051291234534438892705908302997032069/21882605163297778365649972712187618842535002707100524429121759881282576142569777714550121826260727597445726986511730709464923166220551179031462647422987908882663303342728357415477570945318113721076315181311379505790348041476201434965442441976057676293670355577023948192281055435603327278638456663441139861389910778294448090095426237611001717438656213429957794298135920491794414158472382235560196348670808776553696082498560*y^21 + 892811837333917141240084608209146498768211450516155511571784312838077004905584810804568619665021292566592312878407716875284404545121841495896031972185842144021981154011499138365488760832838302465801013045753733504455696278444510050711110021846911000264509438151494694749561996396169319701512887097471085937353309269099992786861951213607814691153068980180383905979805364587350996317046869061801410508046288858047643577533842301/65647815489893335096949918136562856527605008121301573287365279643847728427709333143650365478782182792337180959535192128394769498661653537094387942268963726647989910028185072246432712835954341163228945543934138517371044124428604304896327325928173028881011066731071844576843166306809981835915369990323419584169732334883344270286278712833005152315968640289873382894407761475383242475417146706680589046012426329661088247495680*y^20 - 90176539604610877491580383161161149756924569175136061602597402121037218616362923774479531601562802515886675663915376086289512335403782999622618404627436794672123103151266558699699773291358200603385758035329387343144616572776947897522993332194453245575798113653715469720370841183028775855590760675105919449359543248839952489162462155187582981704528822376365330299527488635898079606781266393222653696388887250702746627353295453/19694344646968000529084975440968856958281502436390471986209583893154318528312799943095109643634654837701154287860557638518430849598496061128316382680689117994396973008455521673929813850786302348968683663180241555211313237328581291468898197778451908664303320019321553373052949892042994550774610997097025875250919700465003281085883613849901545694790592086962014868322328442614972742625144012004176713803727898898326474248704*y^19 - 1520301756368417256059352913717993591738826625977242131514185328829255089484090759510210208789181364789116389753700046814328123342240322532426430968361403452211287106301979860374710266011890825538054783077074215498310346495746585644625756798947464189854218047356344159222852521274545769383505627306820502555175177731762265890259176237869598032586882731608966416406840650815209007324355322632592493842669025440053949340769228423/32823907744946667548474959068281428263802504060650786643682639821923864213854666571825182739391091396168590479767596064197384749330826768547193971134481863323994955014092536123216356417977170581614472771967069258685522062214302152448163662964086514440505533365535922288421583153404990917957684995161709792084866167441672135143139356416502576157984320144936691447203880737691621237708573353340294523006213164830544123747840*y^18 + 59522442307261950768822104025531522933030728015762633443257135133429671207944704363775496606608139984784476704790217891117572377105244452574585264442091251445751765501426417377354860014712353753026420162785522187489046584649341090448318687833008410456454863731103360716678836840994877265052385166714513763555853965387087973484952854204009688630966003647110373448594552600268397234955659088815666416930197779550200260921058721/1230896540435500033067810965060553559892593902274404499138098993322144908019549996443444352727165927356322142991284852407401928099906003820519773917543069874649810813028470104620613365674143896810542728948765097200707077333036330716806137361153244291518957501207597085815809368252687159423413187318564117203182481279062705067867725865618846605924412005435125929270145527663435796414071500750261044612732993681145404640544*y^17 + 10119912307012689457680144179311283064644756007930538236507444320071827125600163136266636349590927498144382508734953821407475960216237295885150990533227075705424999808888144371522059684736783627336479455306099715600502569243745255116601641914923365696316989124358369514627864790381561950202067447908572059211588250338071618862993826847367213728246656179147927230322596619241531818381088979185875080641982142033743021999431398799/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^16 - 6065900127976165484497265555533260838256019056506461698212469033230164159662419819898785802352609857834915344036034651010983187631135796836615317846811360404800069043948342076166136558911286334942729466357689560271808540992192376305956737573865021680545450277008904802927043055193542416048003802870193266501372073068838705855895083713369330119369831562701084325983576444425955687715522351038919242670575416202089503608758026129/65647815489893335096949918136562856527605008121301573287365279643847728427709333143650365478782182792337180959535192128394769498661653537094387942268963726647989910028185072246432712835954341163228945543934138517371044124428604304896327325928173028881011066731071844576843166306809981835915369990323419584169732334883344270286278712833005152315968640289873382894407761475383242475417146706680589046012426329661088247495680*y^15 + 73590749455098246772258424261445064528068767651821745867852213567196226223631998216547239849347511146522376642394601644064644235491198786494583591946091840371867219865726365101150158620822272901225108083160008211747569955914304928946724766150107793348586611321084695854610760822961010142220623864569144259626747342591286102866701814648865803904894686574090594345713729007906951799387997894633965738381831130850082602887795913/32823907744946667548474959068281428263802504060650786643682639821923864213854666571825182739391091396168590479767596064197384749330826768547193971134481863323994955014092536123216356417977170581614472771967069258685522062214302152448163662964086514440505533365535922288421583153404990917957684995161709792084866167441672135143139356416502576157984320144936691447203880737691621237708573353340294523006213164830544123747840*y^14 + 1026466749455755065613554996049095993177990273361000189179627198133132216555083496373442310517635521045114509310705746761072026266271693943935588465259565608131189514735823260922960031723865777585014715136190955793106819426378672145892402936507115068293572499785369123646255276515398849592869062368611883083215822619273672332154423306812589243480008934104753380536195566123254735330691137753657158181746506800670809661515612541/16411953872473333774237479534140714131901252030325393321841319910961932106927333285912591369695545698084295239883798032098692374665413384273596985567240931661997477507046268061608178208988585290807236385983534629342761031107151076224081831482043257220252766682767961144210791576702495458978842497580854896042433083720836067571569678208251288078992160072468345723601940368845810618854286676670147261503106582415272061873920*y^13 - 6835965131848033540574055625799399959937111440558732328732571460966241100480457456324589243138829848165434449794781285012908613705417380612134715746528406558648747427739383938020038930553311552266880626314364124157774782869001723436676640043869862096554969888990702498837020614870181372192390448507388871344170681275412634127855202489617895796000950108245981350841548772334253066802499278844493297263238674588487929637800057113/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^12 - 1543543843145926490428707984344247183139035410707130575719372967032257138893617101401601159939447945249851243348773709839191438832526526879418008639855217048416701472625725641747971790938191686409086776896644282934709842236116606711268260799373859288926092259102029116993647563805980798141664903669770984709864205206488094933161855839996419353185179318431808694343378188241051566029942797979845942579126528482973405640261188909/98471723234840002645424877204844284791407512181952359931047919465771592641563999715475548218173274188505771439302788192592154247992480305641581913403445589971984865042277608369649069253931511744843418315901207776056566186642906457344490988892259543321516600096607766865264749460214972753873054985485129376254598502325016405429418069249507728473952960434810074341611642213074863713125720060020883569018639494491632371243520*y^11 + 292343651914876964569736034170993556706247766033047563845975093463001693687224391946163599614233347329478328229766418354156373539530438311084846084279273197533996999074172291768321602169623985105701746667300129654721282487935827304105540013451327662011666464756074051005894737940635429905710825351669894539356091469098465791714803082470409388926905871639456212660378691384353801817517101502875012184141367105527900500845746669/10941302581648889182824986356093809421267501353550262214560879940641288071284888857275060913130363798722863493255865354732461583110275589515731323711493954441331651671364178707738785472659056860538157590655689752895174020738100717482721220988028838146835177788511974096140527717801663639319228331720569930694955389147224045047713118805500858719328106714978897149067960245897207079236191117780098174335404388276848041249280*y^10 + 121110355025317001101447821031075267876646169439072484712283398765305264846780366811825039077386086845538514650418473970950169639087692345940133923560088260023136129550094660582805904444219169376523748968152957956567869973622973034072436592304655292071244825606636218711680507188477829949773511448458672831113757204428532348614457609119233984384778124546855638155828721888150917412692637386411071368840466034213742096785129741/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^9 - 2218805498682251134914279759995891875385163828935102079665210870742956428170905869924573570660915129884165451657471327819901739731952832744003703425403777131508436119149623330017998300350062814142835508978460080394124815211450105586364042938605805409025829598220762568062560275696036257671809862112671991106209637134220521947323653744757345567684547765118526811940007851947551967953085677655691275073989235807015185413209235997/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^8 - 48664547191607094946735698128500478012972887506145703607906893559965751734883467248370320023888200366305459406701596430208434220238719850449964840543943666348889838411121783438534235180115471497293635762347910033141159577593959895811822189142430465580881456976377907362840677541237335018697678738828455634778272184079439167086357669143909798370288558890571746821444183164852476472383826460760799528722097041592184534500499023/196943446469680005290849754409688569582815024363904719862095838931543185283127999430951096436346548377011542878605576385184308495984960611283163826806891179943969730084555216739298138507863023489686836631802415552113132373285812914688981977784519086643033200193215533730529498920429945507746109970970258752509197004650032810858836138499015456947905920869620148683223284426149727426251440120041767138037278988983264742487040*y^7 + 263749001362343703400903246710803596381917683803494193119735324556888512593032282210966877552022045611133050504781389532851554781880832454019560840124914731452426769418971225405506341214218877561285203266316408247681163559104318299377515863065871655220931285540817933493095542520927841228882800765720860909408616845472547435489702612251067762226339165379374294325627835832082919060906330386091382954920894734620385313405663213/98471723234840002645424877204844284791407512181952359931047919465771592641563999715475548218173274188505771439302788192592154247992480305641581913403445589971984865042277608369649069253931511744843418315901207776056566186642906457344490988892259543321516600096607766865264749460214972753873054985485129376254598502325016405429418069249507728473952960434810074341611642213074863713125720060020883569018639494491632371243520*y^6 + 11130496655053774956207283491030659219663523956899485101726525914645121125329258924504719918782986021026670983138842513485637961709152953396861410738908893601930926800072061164135914179559798170300389526792479550357707121771108338546226274897415658199881039366539782472875883791548868710554791454397422995775764301598764828696013761233207486215118036444256311502795840939581284952856580810746555854426847785000558190921732965/39388689293936001058169950881937713916563004872780943972419167786308637056625599886190219287269309675402308575721115277036861699196992122256632765361378235988793946016911043347859627701572604697937367326360483110422626474657162582937796395556903817328606640038643106746105899784085989101549221994194051750501839400930006562171767227699803091389581184173924029736644656885229945485250288024008353427607455797796652948497408*y^5 - 6878095276640831966527917745797565028416846957114574714204945875275714939755478369436372649193375117682862908643344677608883018252646176147316669582093170881484005231722402042159522854777911663770041849272799468805590476514814931237926719973866819973986573423374974082180710841490817745153194234852742991191907367565153032753679414951006366374008983547438417940645273347966626520586948809582122509552225083381632861042770837/24617930808710000661356219301211071197851878045488089982761979866442898160390999928868887054543318547126442859825697048148038561998120076410395478350861397492996216260569402092412267313482877936210854578975301944014141546660726614336122747223064885830379150024151941716316187365053743188468263746371282344063649625581254101357354517312376932118488240108702518585402910553268715928281430015005220892254659873622908092810880*y^4 - 1191845450131070258013225617532924375745745747018459578490620054166824707053119516409599113638181252766870315569750900381164580062620498838318197537644640632782686439095302027122166433624509317089244015899438529043776344489332580285601125068865328698696297523650458794479952525877337834357570298990043441983333769990488447222092099139733523145791745673540897239312650140797526104691275666141850235981552313689409141848882547/32823907744946667548474959068281428263802504060650786643682639821923864213854666571825182739391091396168590479767596064197384749330826768547193971134481863323994955014092536123216356417977170581614472771967069258685522062214302152448163662964086514440505533365535922288421583153404990917957684995161709792084866167441672135143139356416502576157984320144936691447203880737691621237708573353340294523006213164830544123747840*y^3 + 605848932890390427081521903366837018581778226401795072041935726939439798978936836413027450642037565028428269548196891177852487530397641016493621058776720315204126723798407215678429124400539947367664226129348225102752144712321063873040109439285457638211090934453005093540417655262592509405419815633631160287912864115782057022167567849759672400506003380620403545025719179429756467298512286019028734084866420722020618002163949/49235861617420001322712438602422142395703756090976179965523959732885796320781999857737774109086637094252885719651394096296077123996240152820790956701722794985992432521138804184824534626965755872421709157950603888028283093321453228672245494446129771660758300048303883432632374730107486376936527492742564688127299251162508202714709034624753864236976480217405037170805821106537431856562860030010441784509319747245816185621760*y^2 + 46051655178058225675300836481525145272115312991439465350757621541096454861852384504298417725883711796835742213953253082672152829251487405913592916607414431663095668812661224901008946768110115355763477471536808832125033609916963481028143354172107475893369996261796635535790484722464164592424772581885111430750109332401537464076250969304662260481802037398077651358816103505483257272983282778566072888623261053924966389480291/39388689293936001058169950881937713916563004872780943972419167786308637056625599886190219287269309675402308575721115277036861699196992122256632765361378235988793946016911043347859627701572604697937367326360483110422626474657162582937796395556903817328606640038643106746105899784085989101549221994194051750501839400930006562171767227699803091389581184173924029736644656885229945485250288024008353427607455797796652948497408*y - 3128950337889722043297049631062074470406565011413437671667276939823742418605544505999648097929685478529802945940762683150771464025812356915838693027822877781470108868234547582022651982089760708604081852825423118145339401882441378474290176078125144583151179918653838866808034201605955561907394977525130579140077940093043493746177165557379510981656699141341143673050825062801737992802818492464167618042837912031281574512171/16411953872473333774237479534140714131901252030325393321841319910961932106927333285912591369695545698084295239883798032098692374665413384273596985567240931661997477507046268061608178208988585290807236385983534629342761031107151076224081831482043257220252766682767961144210791576702495458978842497580854896042433083720836067571569678208251288078992160072468345723601940368845810618854286676670147261503106582415272061873920