# Manifold: Rolfsen Knot 9_30 # Number of Tetrahedra: 13 # Number Field x^28 - 3*x^27 - 2*x^26 + 18*x^25 - x^24 - 95*x^23 + 88*x^22 + 388*x^21 - 684*x^20 - 1346*x^19 + 4479*x^18 - 635*x^17 - 10000*x^16 + 5973*x^15 + 20274*x^14 - 27473*x^13 - 11880*x^12 + 39698*x^11 - 734*x^10 - 42514*x^9 + 18244*x^8 + 21001*x^7 - 14468*x^6 - 4662*x^5 + 4653*x^4 + 78*x^3 - 219*x^2 - 232*x + 76 # Approximate Field Generator 1.42078828454667 + 1.02844262733048*I # Shape Parameters 721293041576964094897641947350523521356291602829889149707/406154713500850237635798078026867828946575915433284808728*y^27 - 1783145911938941454720507962234118954204283858478413788199/406154713500850237635798078026867828946575915433284808728*y^26 - 298191873735923236861282023768101215998263001046708012317/50769339187606279704474759753358478618321989429160601091*y^25 + 5863479422514543974028602987508707592927903583675592432967/203077356750425118817899039013433914473287957716642404364*y^24 + 5476578654940466616295764240106126736219145571053529992465/406154713500850237635798078026867828946575915433284808728*y^23 - 65653287090066532005650641875254940682130424902257760892399/406154713500850237635798078026867828946575915433284808728*y^22 + 14394452320862303785221879700882048039640966789655112943767/203077356750425118817899039013433914473287957716642404364*y^21 + 36898552294330140169009085528477723092939217189456104588061/50769339187606279704474759753358478618321989429160601091*y^20 - 84378432662428099917797622640609651159307682599037752962223/101538678375212559408949519506716957236643978858321202182*y^19 - 574840186527723722013242062290032921327813972620867577483859/203077356750425118817899039013433914473287957716642404364*y^18 + 2624076232919370220188167812556514052158890394605342349305641/406154713500850237635798078026867828946575915433284808728*y^17 + 930002025606536530150857473956319835929676873203188674759365/406154713500850237635798078026867828946575915433284808728*y^16 - 3362938608540700529416260139706789689128360260573295474990149/203077356750425118817899039013433914473287957716642404364*y^15 + 11237033513018955806413365517696160573256864240461663604721/6062010649266421457250717582490564611142924110944549384*y^14 + 1879031280457329542272953164284553009271882697537644484400497/50769339187606279704474759753358478618321989429160601091*y^13 - 11873628916039930132046379064927789391181383309751109136846635/406154713500850237635798078026867828946575915433284808728*y^12 - 7432774149794332249134188994693789334958969551805556944511745/203077356750425118817899039013433914473287957716642404364*y^11 + 10395680940103439771638031402180442407880496636555372409420269/203077356750425118817899039013433914473287957716642404364*y^10 + 5241435037614550905365669539633689298894778579804903029546285/203077356750425118817899039013433914473287957716642404364*y^9 - 12573873514349855999486645883450789444045571053875165460753277/203077356750425118817899039013433914473287957716642404364*y^8 - 19392216544632402018768850250891931647986741914052882389754/50769339187606279704474759753358478618321989429160601091*y^7 + 15092869601518743255974424809332067972685530865138995837143459/406154713500850237635798078026867828946575915433284808728*y^6 - 1222608973907511623233903891050825292544323740259342724315737/203077356750425118817899039013433914473287957716642404364*y^5 - 2334916838247313159565657830106253893060039294096857263962239/203077356750425118817899039013433914473287957716642404364*y^4 + 880923137272523537179326466679872240634862982428783757350907/406154713500850237635798078026867828946575915433284808728*y^3 + 131752703696610568160701075890177325118128504067613546969987/101538678375212559408949519506716957236643978858321202182*y^2 + 121840138736494482076432292961735308416823421641668119227071/406154713500850237635798078026867828946575915433284808728*y - 51600074392541493884838171317177846695497471381060231138423/203077356750425118817899039013433914473287957716642404364 -43748298303718285041499527537145706049406584066708582591/101538678375212559408949519506716957236643978858321202182*y^27 + 101670102481315353568627074980804719252009225001182521017/101538678375212559408949519506716957236643978858321202182*y^26 + 78647271535543626627193725487481287852715765337002032687/50769339187606279704474759753358478618321989429160601091*y^25 - 341479937976870014369553192565512701837606281725781051735/50769339187606279704474759753358478618321989429160601091*y^24 - 423012100203405964742741421611048627971136115581916130785/101538678375212559408949519506716957236643978858321202182*y^23 + 3884005328480726589826568298852938340428674169613601674865/101538678375212559408949519506716957236643978858321202182*y^22 - 602571545762769224041738772905346234303111014328787126068/50769339187606279704474759753358478618321989429160601091*y^21 - 8937031503136674979893084268713762621862795152577252580857/50769339187606279704474759753358478618321989429160601091*y^20 + 8908982560729449289031678194702852002391223773511051793785/50769339187606279704474759753358478618321989429160601091*y^19 + 35681487432651687990298232001785955010486806395820914385253/50769339187606279704474759753358478618321989429160601091*y^18 - 147884862723964399552243392166937443381892216443516297392455/101538678375212559408949519506716957236643978858321202182*y^17 - 74085752770988103023643663448727866665095816998685619802961/101538678375212559408949519506716957236643978858321202182*y^16 + 194960317596507777818457861575679654778558952505071293290086/50769339187606279704474759753358478618321989429160601091*y^15 + 86358982259684091751943953931815558695454546013640602535/1515502662316605364312679395622641152785731027736137346*y^14 - 445449023132249283416114733258959611394783840441580659180194/50769339187606279704474759753358478618321989429160601091*y^13 + 594747919803910297231024786411390406668552299206720878122153/101538678375212559408949519506716957236643978858321202182*y^12 + 470804044514801683797758046762870265051002623078462082078594/50769339187606279704474759753358478618321989429160601091*y^11 - 551579089249472017082405763423045161757497408759678442626358/50769339187606279704474759753358478618321989429160601091*y^10 - 370336499390627149935485950458898329655854830069983878981330/50769339187606279704474759753358478618321989429160601091*y^9 + 686258067477846616209647193484508967641694555900005544070187/50769339187606279704474759753358478618321989429160601091*y^8 + 78605893039171225286221537983997361827125004963751816881243/50769339187606279704474759753358478618321989429160601091*y^7 - 833264851140871938794890202166451048116524118464639313627033/101538678375212559408949519506716957236643978858321202182*y^6 + 26492301588182111508844134544050141241168357672082503002748/50769339187606279704474759753358478618321989429160601091*y^5 + 127222306543199783457797527096435757273160934259282940612591/50769339187606279704474759753358478618321989429160601091*y^4 - 25690443137411661297455025293010785854528183443270677321481/101538678375212559408949519506716957236643978858321202182*y^3 - 12758734787709293676292069430117014456883417577610834085756/50769339187606279704474759753358478618321989429160601091*y^2 - 8609099662666088159813011667465053311540302990219769337651/101538678375212559408949519506716957236643978858321202182*y + 2427679218846488900278216413323788794362375981925700027136/50769339187606279704474759753358478618321989429160601091 12661745736754155480258840762916089220686510054340587843/101538678375212559408949519506716957236643978858321202182*y^27 - 32996644438278040777129726985914145374796169780708979365/101538678375212559408949519506716957236643978858321202182*y^26 - 19368178481648215038323959438394530549277612178037761565/50769339187606279704474759753358478618321989429160601091*y^25 + 106780078594471927981490043630037813576698449910980537786/50769339187606279704474759753358478618321989429160601091*y^24 + 73210524640935173937627663873807743634329507946533577581/101538678375212559408949519506716957236643978858321202182*y^23 - 1180289510658940261169994353925434671050883078439463568283/101538678375212559408949519506716957236643978858321202182*y^22 + 321850421686729383952359234682236272726157896992771634711/50769339187606279704474759753358478618321989429160601091*y^21 + 2601507313264233327976688947787351718418373832842686975077/50769339187606279704474759753358478618321989429160601091*y^20 - 3306855976949465660150805915843144348171323274261857389905/50769339187606279704474759753358478618321989429160601091*y^19 - 9911545003977418082993078739919853790158065765495219525258/50769339187606279704474759753358478618321989429160601091*y^18 + 49035327156491450136683753078583968343221265338449732763625/101538678375212559408949519506716957236643978858321202182*y^17 + 12008231247105473225076158670480855965883655834179912123299/101538678375212559408949519506716957236643978858321202182*y^16 - 61574988038926253342240190025157558392309159365048197486545/50769339187606279704474759753358478618321989429160601091*y^15 + 388815724633870286456216084078635891731683766061685628865/1515502662316605364312679395622641152785731027736137346*y^14 + 135257669776025337414880719672127059733577935364693245701897/50769339187606279704474759753358478618321989429160601091*y^13 - 240205393522076201841858988042950453135169039236385840638829/101538678375212559408949519506716957236643978858321202182*y^12 - 126747730708440819489927955241362408809272930883386074272084/50769339187606279704474759753358478618321989429160601091*y^11 + 203014996759962346962887252601234632456434277897144716539036/50769339187606279704474759753358478618321989429160601091*y^10 + 80456816093083356264852575444591246971778690355837794072209/50769339187606279704474759753358478618321989429160601091*y^9 - 241137590834380475977059224697902301185175706709523927276159/50769339187606279704474759753358478618321989429160601091*y^8 + 15611562444099059006498634392511498062885550842341867868649/50769339187606279704474759753358478618321989429160601091*y^7 + 288008835231208835120640789050471295177676714725930893459463/101538678375212559408949519506716957236643978858321202182*y^6 - 32085251195584215102992200268612432026294216299059747824576/50769339187606279704474759753358478618321989429160601091*y^5 - 45087205397668239538273818600215436703627825669530247795920/50769339187606279704474759753358478618321989429160601091*y^4 + 21070441845180411327450859284792606912036357519714307974103/101538678375212559408949519506716957236643978858321202182*y^3 + 5413552988966777007636449905878447697345680698285563618436/50769339187606279704474759753358478618321989429160601091*y^2 + 2048790458978799703216229535589271080223711994779892429109/101538678375212559408949519506716957236643978858321202182*y - 1041338462559616787221433210092974319917987841185585422848/50769339187606279704474759753358478618321989429160601091 -9375061764709042267017652623610213636926581668794899816457/7716939556516154515080163482510488749984942393232411365832*y^27 + 23889565246940485708243905362647643449443049636228821888877/7716939556516154515080163482510488749984942393232411365832*y^26 + 3705121215983364627087442193202783301231538866974531839582/964617444564519314385020435313811093748117799154051420729*y^25 - 77738595874191148046468561342146227220911729591269716643273/3858469778258077257540081741255244374992471196616205682916*y^24 - 61423869272558290267674938235847255721919800198361650674755/7716939556516154515080163482510488749984942393232411365832*y^23 + 45469469460180486135354308424914719918443977857780890571439/406154713500850237635798078026867828946575915433284808728*y^22 - 216128201674355050336519277282629748827004246061473622988981/3858469778258077257540081741255244374992471196616205682916*y^21 - 479971922383237041620981880147759803470042531580534140449527/964617444564519314385020435313811093748117799154051420729*y^20 + 61467286608333898701744358371513594801640946965942289997673/101538678375212559408949519506716957236643978858321202182*y^19 + 7384191781843134588347791886331866122909448893332103966519421/3858469778258077257540081741255244374992471196616205682916*y^18 - 35314220965688444326247807622410948114654435740436940754025931/7716939556516154515080163482510488749984942393232411365832*y^17 - 10185997175290039594413120176134154453973323338304426675750623/7716939556516154515080163482510488749984942393232411365832*y^16 + 44644991959702664660515794376289275800401690352048800659286663/3858469778258077257540081741255244374992471196616205682916*y^15 - 226941531419570226245056573520921081506644325181594285207083/115178202336062007687763634067320727611715558107946438296*y^14 - 24687537553026312178631939449234779067143409530323575709494309/964617444564519314385020435313811093748117799154051420729*y^13 + 167476834460279475996767225928947855789690016907310478168140401/7716939556516154515080163482510488749984942393232411365832*y^12 + 94331541552189387974745466040424297170402165190083898433449247/3858469778258077257540081741255244374992471196616205682916*y^11 - 143102074581983596310495712024248784280918016775518147067132011/3858469778258077257540081741255244374992471196616205682916*y^10 - 62572813019699180893734569591703010988940388024178496418826779/3858469778258077257540081741255244374992471196616205682916*y^9 + 170943386905163019046621783755852921808496193016160612174469495/3858469778258077257540081741255244374992471196616205682916*y^8 - 1651115615308492340054137741004163383107898660359371868028048/964617444564519314385020435313811093748117799154051420729*y^7 - 203432775271321169889323745950775439308884628796910005709658873/7716939556516154515080163482510488749984942393232411365832*y^6 + 20480096599833990422489890953240735835051823341108197937668831/3858469778258077257540081741255244374992471196616205682916*y^5 + 31396439812925306667220148862602438551630529067496663532435349/3858469778258077257540081741255244374992471196616205682916*y^4 - 13794312629327714475589621074007573418372422798949716508135529/7716939556516154515080163482510488749984942393232411365832*y^3 - 1794956675299445121813555224628504709503700994305026687519647/1929234889129038628770040870627622187496235598308102841458*y^2 - 1593136342136380999029503376880244948711234889989335410215989/7716939556516154515080163482510488749984942393232411365832*y + 742451283281383797718450379299515936300597049048532373691849/3858469778258077257540081741255244374992471196616205682916 35695187165165561901822798795006221224269275396489395803/101538678375212559408949519506716957236643978858321202182*y^27 - 86107282510399545616735193269060809414875453147569204777/101538678375212559408949519506716957236643978858321202182*y^26 - 60785348895273652623969001519567875223462339389607534179/50769339187606279704474759753358478618321989429160601091*y^25 + 285176916306680610138062729819925969053201288036904369420/50769339187606279704474759753358478618321989429160601091*y^24 + 297490423490432906450585729478981671527143828127305858385/101538678375212559408949519506716957236643978858321202182*y^23 - 3210845900390360581286658144937457318631361465991449312893/101538678375212559408949519506716957236643978858321202182*y^22 + 630853225930031451998259689169107159855537455026457369240/50769339187606279704474759753358478618321989429160601091*y^21 + 7279193971711384085932839379320780522106073513084796553290/50769339187606279704474759753358478618321989429160601091*y^20 - 7934522997288997530685458437510610084904728177050369805872/50769339187606279704474759753358478618321989429160601091*y^19 - 28602244327118035170394113294446225260473417380576857148039/50769339187606279704474759753358478618321989429160601091*y^18 + 126194153032417425232603953926454230638325680876471648831573/101538678375212559408949519506716957236643978858321202182*y^17 + 50763178418961649005314505386578976578619840038687467440305/101538678375212559408949519506716957236643978858321202182*y^16 - 163078419176192781278742844170372957101559036861104478830033/50769339187606279704474759753358478618321989429160601091*y^15 + 341212023423629970647612630301146149271141313600857541173/1515502662316605364312679395622641152785731027736137346*y^14 + 367092183625281677824586281967911226833610731697421332929857/50769339187606279704474759753358478618321989429160601091*y^13 - 551022927039138536799437779634420480095515671151295964656831/101538678375212559408949519506716957236643978858321202182*y^12 - 370307817960356232772342359100275444789855019835224032372520/50769339187606279704474759753358478618321989429160601091*y^11 + 490326552637833709116410896379182255216265958112566663850053/50769339187606279704474759753358478618321989429160601091*y^10 + 270288346701125318964366774228025863325646780781983819038992/50769339187606279704474759753358478618321989429160601091*y^9 - 597596544823667066105808142285043837098135006488994218739959/50769339187606279704474759753358478618321989429160601091*y^8 - 20995286689774800752240510566100495069159298848365972062027/50769339187606279704474759753358478618321989429160601091*y^7 + 718405175760079247454493863322656647168348705153279387139547/101538678375212559408949519506716957236643978858321202182*y^6 - 49756201099771777225070173386965441957543634015458193235604/50769339187606279704474759753358478618321989429160601091*y^5 - 110561701177850665089678926942969812030959223048950530935004/50769339187606279704474759753358478618321989429160601091*y^4 + 37888520602463287163064899834661910421267175394855318025381/101538678375212559408949519506716957236643978858321202182*y^3 + 12145229173340292150357966439169250182169356589555814649083/50769339187606279704474759753358478618321989429160601091*y^2 + 6073477504347288462305661949933134734066709605672351627573/101538678375212559408949519506716957236643978858321202182*y - 2352992286564364390157757590165320146707081150508134735684/50769339187606279704474759753358478618321989429160601091 73286365990328201893451929086770425017879907111891433947/101538678375212559408949519506716957236643978858321202182*y^27 - 173294895775519302595345019212341445351830222141117938253/101538678375212559408949519506716957236643978858321202182*y^26 - 128544787608376293309687931220985430305221878565452077516/50769339187606279704474759753358478618321989429160601091*y^25 + 578257172772017565177404488769886851065171491238362886273/50769339187606279704474759753358478618321989429160601091*y^24 + 663508548795217144953847459120775930015552467824471567187/101538678375212559408949519506716957236643978858321202182*y^23 - 6546052616513512645409019726021766245353981920330429962625/101538678375212559408949519506716957236643978858321202182*y^22 + 1141297515217511765235662806450879428899161052042349740328/50769339187606279704474759753358478618321989429160601091*y^21 + 14959345866807419461656603651910809283523182621537732274389/50769339187606279704474759753358478618321989429160601091*y^20 - 15554734401588250125794352087712609627297520002040848070992/50769339187606279704474759753358478618321989429160601091*y^19 - 59289452269815191432008858389723601171264328762380357293761/50769339187606279704474759753358478618321989429160601091*y^18 + 252978464740258993199125302073922324809927620800169330305713/101538678375212559408949519506716957236643978858321202182*y^17 + 114940632159450307293965391345772996589028473572890676612363/101538678375212559408949519506716957236643978858321202182*y^16 - 330410084872857023748458940095498098548416609567567886782321/50769339187606279704474759753358478618321989429160601091*y^15 + 245900892915935631616832049521349414900128203423338797221/1515502662316605364312679395622641152785731027736137346*y^14 + 749704600481281365833340115663615674731206471014966075774740/50769339187606279704474759753358478618321989429160601091*y^13 - 1058768076614400090063053133565348629650036095245494170831015/101538678375212559408949519506716957236643978858321202182*y^12 - 775647805608238814710686652030846944189174265911619573013922/50769339187606279704474759753358478618321989429160601091*y^11 + 962417945736217910550905478524174544236075081517201823957778/50769339187606279704474759753358478618321989429160601091*y^10 + 590134576263153909054159415049930658172440526193012927275728/50769339187606279704474759753358478618321989429160601091*y^9 - 1185674744351837429912031572295978428437274013612166486751414/50769339187606279704474759753358478618321989429160601091*y^8 - 90516414705703158127240837455236992621925378508047240041239/50769339187606279704474759753358478618321989429160601091*y^7 + 1433046147184936730833414509945673105964448151734649774810635/101538678375212559408949519506716957236643978858321202182*y^6 - 71447157315619146173024225023515365406838821265179408611537/50769339187606279704474759753358478618321989429160601091*y^5 - 219618468187241900325899729960876787724169781297156567275705/50769339187606279704474759753358478618321989429160601091*y^4 + 59695860555619771450600342493400146662415318132858638896129/101538678375212559408949519506716957236643978858321202182*y^3 + 23105754861457932273423799042753948439655482762556990753360/50769339187606279704474759753358478618321989429160601091*y^2 + 13406287572344926731834411515856589366592035583216153722243/101538678375212559408949519506716957236643978858321202182*y - 4405461436018532880768873855868710474210033224772815963686/50769339187606279704474759753358478618321989429160601091 13790002415332039803455793979482374931323821174504208085165/7716939556516154515080163482510488749984942393232411365832*y^27 - 34538566463800752384565514223307133186727574310915597446649/7716939556516154515080163482510488749984942393232411365832*y^26 - 5591928107421381210165744981921387100520594839931462324444/964617444564519314385020435313811093748117799154051420729*y^25 + 113067156258083778160571231157740713342531211898663680936749/3858469778258077257540081741255244374992471196616205682916*y^24 + 98455754052236512280213351338012107234166672518386952034887/7716939556516154515080163482510488749984942393232411365832*y^23 - 66413123788043167642491050321274834417374684627329010535379/406154713500850237635798078026867828946575915433284808728*y^22 + 293772098914434381571741542383355506332132144881839123277621/3858469778258077257540081741255244374992471196616205682916*y^21 + 705643445708417779158355989690306820732595312135748913895080/964617444564519314385020435313811093748117799154051420729*y^20 - 87296066194933369294738585367010403652248921225819315451397/101538678375212559408949519506716957236643978858321202182*y^19 - 10933184752810067222799309579380291926008735250992925177083081/3858469778258077257540081741255244374992471196616205682916*y^18 + 50938911375359147288229491548068454320756344319099080216994879/7716939556516154515080163482510488749984942393232411365832*y^17 + 16559677666115296909809314933306819655297889895928939259725355/7716939556516154515080163482510488749984942393232411365832*y^16 - 64898126718433067298068348297919973184661426700461046007993635/3858469778258077257540081741255244374992471196616205682916*y^15 + 267280540048852509396636634404943297473327500423858227776071/115178202336062007687763634067320727611715558107946438296*y^14 + 36095492716353412593219218426956982596842498629970755545460212/964617444564519314385020435313811093748117799154051420729*y^13 - 235542691074969569158975002189769453791547276116268232610600469/7716939556516154515080163482510488749984942393232411365832*y^12 - 140667146182963389166625618478006612423537857602975121830433879/3858469778258077257540081741255244374992471196616205682916*y^11 + 204034210111898062671696954545417322549115623775368987934281799/3858469778258077257540081741255244374992471196616205682916*y^10 + 96595999586709112123017040309148173034706579711741621440295275/3858469778258077257540081741255244374992471196616205682916*y^9 - 245447109620259946006853866417361434440312134655388949176416751/3858469778258077257540081741255244374992471196616205682916*y^8 + 885276988753028182162878269634401649978757137446824312351912/964617444564519314385020435313811093748117799154051420729*y^7 + 293767356514246558599117796011055197166304824893625646971672309/7716939556516154515080163482510488749984942393232411365832*y^6 - 26526680488494680916229936268684724129828133866268364659194547/3858469778258077257540081741255244374992471196616205682916*y^5 - 45499604224779165235661022791380976980985308824009515239333253/3858469778258077257540081741255244374992471196616205682916*y^4 + 18591869884243981569105436941105959267753205607358496743750421/7716939556516154515080163482510488749984942393232411365832*y^3 + 2605833495110776301591660763509048968024518520241235745107065/1929234889129038628770040870627622187496235598308102841458*y^2 + 2280878467383801288123133355746651759205562992040859747759113/7716939556516154515080163482510488749984942393232411365832*y - 1032532230670855535926759900148936951853922110058703054727929/3858469778258077257540081741255244374992471196616205682916 -29456300415339436517438911445894017554147156235759475443545/249429763428709652188084494668250205451815934065466033160083*y^27 + 70574967390893670354068020047572892095977564639432939692086/249429763428709652188084494668250205451815934065466033160083*y^26 + 101430597235986955231339530413064752190992944473589199559854/249429763428709652188084494668250205451815934065466033160083*y^25 - 468672355114668719286862784670603929879045622827871344550011/249429763428709652188084494668250205451815934065466033160083*y^24 - 253178393001945530750416491848679161816196585819133530692315/249429763428709652188084494668250205451815934065466033160083*y^23 + 2643469158878241100008965900134729830922430207129368342382595/249429763428709652188084494668250205451815934065466033160083*y^22 - 996761298163867950475534322962984982432570650462391142294862/249429763428709652188084494668250205451815934065466033160083*y^21 - 12019915042737184305998147221869180370000496745589460135390348/249429763428709652188084494668250205451815934065466033160083*y^20 + 12885228874848462737521783602719920790374723155693315708894418/249429763428709652188084494668250205451815934065466033160083*y^19 + 2786974847033594315459856510218234876532321137853581998380610/14672339025218214834593205568720600320695054945027413715299*y^18 - 103268848323263607122599605557458763741659073521958916765851101/249429763428709652188084494668250205451815934065466033160083*y^17 - 43458618864202588531638405353185541897049469109545543227038358/249429763428709652188084494668250205451815934065466033160083*y^16 + 267906123312033581045360109050253082759788097732200187749166056/249429763428709652188084494668250205451815934065466033160083*y^15 - 215513499383121021048707662378724331111799234362083347986454/3722832289980741077434096935347017991818148269633821390449*y^14 - 604710788333368646285233540644980684849708889641964189817648188/249429763428709652188084494668250205451815934065466033160083*y^13 + 444256228702160345407092506333546202191072143725247546385013300/249429763428709652188084494668250205451815934065466033160083*y^12 + 615357629849795438413265843301812589233776760428558006095771048/249429763428709652188084494668250205451815934065466033160083*y^11 - 796483889840604934351221328901492592405837257872997086475879260/249429763428709652188084494668250205451815934065466033160083*y^10 - 455537550288816464367072008086135324498434251054588644401490948/249429763428709652188084494668250205451815934065466033160083*y^9 + 57304969954611885012524362870737668171954941485443592036581661/14672339025218214834593205568720600320695054945027413715299*y^8 + 46883503093874709581147320885992581904585374945167080474649717/249429763428709652188084494668250205451815934065466033160083*y^7 - 585877238322963856370158843136514650037078079399946129055330975/249429763428709652188084494668250205451815934065466033160083*y^6 + 75031937264698031390873737908758721668148393854308416918436765/249429763428709652188084494668250205451815934065466033160083*y^5 + 179224611009466781010466804755145736059051843702158112139765008/249429763428709652188084494668250205451815934065466033160083*y^4 - 30378322831774550441923978897619527304729312648796333435231360/249429763428709652188084494668250205451815934065466033160083*y^3 - 19243183042680350762771396289351164619091058390886359976727276/249429763428709652188084494668250205451815934065466033160083*y^2 - 4735079363034314736148919559961901626244948104854120942089733/249429763428709652188084494668250205451815934065466033160083*y + 3953556330096048788407878985997583749436647519123457668570677/249429763428709652188084494668250205451815934065466033160083 -373648946646992048577926106626015037798568897976330185031/406154713500850237635798078026867828946575915433284808728*y^27 + 928924831059256786288450591917027569886216673830904702547/406154713500850237635798078026867828946575915433284808728*y^26 + 153252641231788505811051656599122314320489993434109015204/50769339187606279704474759753358478618321989429160601091*y^25 - 3048964385773685850017648591911158526048505193126270585359/203077356750425118817899039013433914473287957716642404364*y^24 - 2766051905241234194644194301878795077684299126038809936485/406154713500850237635798078026867828946575915433284808728*y^23 + 34091967216983300508395253338405250702353635176679317108619/406154713500850237635798078026867828946575915433284808728*y^22 - 7669433113476005081168424493048773196774463995340027426475/203077356750425118817899039013433914473287957716642404364*y^21 - 19120098088633864253703978860601584506443867984337956587141/50769339187606279704474759753358478618321989429160601091*y^20 + 44236674138190925014305311773564421509542875533731922337297/101538678375212559408949519506716957236643978858321202182*y^19 + 297190073512636814743909166254473142712534126685826047857507/203077356750425118817899039013433914473287957716642404364*y^18 - 1368350688879025154851604057406811205694348651365907126107725/406154713500850237635798078026867828946575915433284808728*y^17 - 468170382418767180036102554588850091170438666672833530071065/406154713500850237635798078026867828946575915433284808728*y^16 + 1749505176694825432433163334690128393613455068601780198040593/203077356750425118817899039013433914473287957716642404364*y^15 - 6416316401032635003854524695740162427339602781519932186525/6062010649266421457250717582490564611142924110944549384*y^14 - 975656194032763535215471886974340704448826516334412923387766/50769339187606279704474759753358478618321989429160601091*y^13 + 6248884496493954525787274675107137776857078918260212105398631/406154713500850237635798078026867828946575915433284808728*y^12 + 3836401528180542913115898711588417354668204461690853263006813/203077356750425118817899039013433914473287957716642404364*y^11 - 5447480730532641709814654404635214315208290993556779176701429/203077356750425118817899039013433914473287957716642404364*y^10 - 2676309418171658350041299748060330484201480479790280259157093/203077356750425118817899039013433914473287957716642404364*y^9 + 6574429791825856109168853677027775215447199382102961180620089/203077356750425118817899039013433914473287957716642404364*y^8 - 3903756635328280059222568920470779986207048289347566054434/50769339187606279704474759753358478618321989429160601091*y^7 - 7884463021456075500100134374849199664273475682417744421717055/406154713500850237635798078026867828946575915433284808728*y^6 + 669318719395387268472609117953191870720743819375990034800809/203077356750425118817899039013433914473287957716642404364*y^5 + 1220923997538873736566268964055249002093631704570232749009039/203077356750425118817899039013433914473287957716642404364*y^4 - 477196357606040462080381428383075441305185129194838817690639/406154713500850237635798078026867828946575915433284808728*y^3 - 69374614725873219553776411822790501475720760672791711987383/101538678375212559408949519506716957236643978858321202182*y^2 - 62319838245149801384411512666785886640169904321393083090867/406154713500850237635798078026867828946575915433284808728*y + 27415237430583847698611358273528484757355123570801427602107/203077356750425118817899039013433914473287957716642404364 -184188580226041597631722967257644029994513843183036851337/203077356750425118817899039013433914473287957716642404364*y^27 + 439144324175786048584893092215159621604938745130893819761/203077356750425118817899039013433914473287957716642404364*y^26 + 159201790951185672482505555134415637823082674951263152498/50769339187606279704474759753358478618321989429160601091*y^25 - 1459707944359979032755340958739237083340933756872375116821/101538678375212559408949519506716957236643978858321202182*y^24 - 1605097983930031419718643152387899246954060244845694900523/203077356750425118817899039013433914473287957716642404364*y^23 + 16482212054377973059870645129509666899836054561442229826513/203077356750425118817899039013433914473287957716642404364*y^22 - 3044115203505345896525032871395230196263918917542917304773/101538678375212559408949519506716957236643978858321202182*y^21 - 18762983742952110033832514117020611748148687577379085663116/50769339187606279704474759753358478618321989429160601091*y^20 + 19943841335066308834904501002210030066152195957969362615159/50769339187606279704474759753358478618321989429160601091*y^19 + 148124484725132374295745005744309277481637572747886084952485/101538678375212559408949519506716957236643978858321202182*y^18 - 642057796928787090167548985751618852768338661181655265335615/203077356750425118817899039013433914473287957716642404364*y^17 - 275050829869342199996772995724519400207329295137917071964607/203077356750425118817899039013433914473287957716642404364*y^16 + 833585657940089008592986912848523850929214568649403003186951/101538678375212559408949519506716957236643978858321202182*y^15 - 1174267857323111445507057421425136995721000820891795034811/3031005324633210728625358791245282305571462055472274692*y^14 - 941890873848144240994883272245381987887082263852298080606366/50769339187606279704474759753358478618321989429160601091*y^13 + 2746003924381847982300976634725205604502623839633860962349089/203077356750425118817899039013433914473287957716642404364*y^12 + 1921195434612421906116407997837106655461591835324733591646351/101538678375212559408949519506716957236643978858321202182*y^11 - 2466425946739023659157338522362177384311501783463980831285777/101538678375212559408949519506716957236643978858321202182*y^10 - 1429040756114897740434322636698736688972994690718972534846283/101538678375212559408949519506716957236643978858321202182*y^9 + 3019890869217335700582854586984739683032912887761921401409435/101538678375212559408949519506716957236643978858321202182*y^8 + 79183550762620186241434949516075945538872554570861047978121/50769339187606279704474759753358478618321989429160601091*y^7 - 3630519021624991242883706619946192093856776544988009971347989/203077356750425118817899039013433914473287957716642404364*y^6 + 224840339637920588632916617819425812541840285038686982605655/101538678375212559408949519506716957236643978858321202182*y^5 + 555117106744793858368857859640720285458854649088790728847691/101538678375212559408949519506716957236643978858321202182*y^4 - 180209708157394709275674983907081506829620199655071804401741/203077356750425118817899039013433914473287957716642404364*y^3 - 29612762435431693790339644318013054154843639602621914924817/50769339187606279704474759753358478618321989429160601091*y^2 - 31216843252603537514982513911718199362096266244159174137801/203077356750425118817899039013433914473287957716642404364*y + 11718692699560520334863315053372917607342328408232431478755/101538678375212559408949519506716957236643978858321202182 25651555942263570789023556044402558539935716867044854465/50769339187606279704474759753358478618321989429160601091*y^27 - 61586752542995216888367778922141844613324964220430606438/50769339187606279704474759753358478618321989429160601091*y^26 - 88254524822265874007023047739374157014777432719710734571/50769339187606279704474759753358478618321989429160601091*y^25 + 408949695329087170203934825602192734546006936020571800504/50769339187606279704474759753358478618321989429160601091*y^24 + 219595088576574166112531122684970138291772234827143030356/50769339187606279704474759753358478618321989429160601091*y^23 - 2306082687346393058662272450111421615364712992952969474108/50769339187606279704474759753358478618321989429160601091*y^22 + 874920231095774520767134727184549424234929165564145689886/50769339187606279704474759753358478618321989429160601091*y^21 + 10481402445395544215426853326993423448101156383893362151678/50769339187606279704474759753358478618321989429160601091*y^20 - 11265887670115784317164690908281881664824416861798240300616/50769339187606279704474759753358478618321989429160601091*y^19 - 41298468467162972138391837374145121117930953694443742603202/50769339187606279704474759753358478618321989429160601091*y^18 + 90164326932395612280625395897624104932202916318296532004859/50769339187606279704474759753358478618321989429160601091*y^17 + 37822113554385217384068283617131933727549961642443196944456/50769339187606279704474759753358478618321989429160601091*y^16 - 234001841971688589285719373191018482433308946460797748081043/50769339187606279704474759753358478618321989429160601091*y^15 + 192156345762341157394440726670229440817413334932090550315/757751331158302682156339697811320576392865513868068673*y^14 + 528220663014690303999791461941629116533934230581589237241786/50769339187606279704474759753358478618321989429160601091*y^13 - 388145287280004927501559574749298557647380349764311594626009/50769339187606279704474759753358478618321989429160601091*y^12 - 538334741402888978284739786642002905221765325990892036910668/50769339187606279704474759753358478618321989429160601091*y^11 + 696255910673709792835332240153252377100467033183870229235593/50769339187606279704474759753358478618321989429160601091*y^10 + 399636111985659611090990766218314614807782629774230289051512/50769339187606279704474759753358478618321989429160601091*y^9 - 852376393457651308835548901908597199412451757889358930926386/50769339187606279704474759753358478618321989429160601091*y^8 - 43681897977544447791189794621772323521085198323419497558437/50769339187606279704474759753358478618321989429160601091*y^7 + 514129708752046538317178791184239198041859899045896068925209/50769339187606279704474759753358478618321989429160601091*y^6 - 62876314628007886345524790359804101470241473134875656701027/50769339187606279704474759753358478618321989429160601091*y^5 - 158346244428565144093034783774463209916417553398867486353149/50769339187606279704474759753358478618321989429160601091*y^4 + 24752079061492665393227207057552699049589188803256980706760/50769339187606279704474759753358478618321989429160601091*y^3 + 17064769447478279570608460408927161979745732680135987570816/50769339187606279704474759753358478618321989429160601091*y^2 + 4494062472049190158595217726125672801896191489586947560621/50769339187606279704474759753358478618321989429160601091*y - 3204701345861046352542174249969897958879287663738845175967/50769339187606279704474759753358478618321989429160601091 -2821206132261973477534474763598822239759185111383131363/50769339187606279704474759753358478618321989429160601091*y^27 + 10985889818626270967092301197838991332199473783668160481/50769339187606279704474759753358478618321989429160601091*y^26 + 2291526739959675552668804592493564865413582887677587712/50769339187606279704474759753358478618321989429160601091*y^25 - 64189870954363897334146566153775887281093847470161230517/50769339187606279704474759753358478618321989429160601091*y^24 + 30672910491551055311074933241206961094230171436180645107/50769339187606279704474759753358478618321989429160601091*y^23 + 324620298546252034457824505835843839406354123132353484560/50769339187606279704474759753358478618321989429160601091*y^22 - 429180679344884457055845719771246429779094750092670129577/50769339187606279704474759753358478618321989429160601091*y^21 - 1221506929305777301141270593546936391528479436531840270221/50769339187606279704474759753358478618321989429160601091*y^20 + 2914315369411360882632827933764909351732370873130623866474/50769339187606279704474759753358478618321989429160601091*y^19 + 3762487025098833012674563776809058282942170871303986334480/50769339187606279704474759753358478618321989429160601091*y^18 - 17186168163641943537047816102670396261161891543658768687311/50769339187606279704474759753358478618321989429160601091*y^17 + 5995345217689642494306929673680114397067675125296667419232/50769339187606279704474759753358478618321989429160601091*y^16 + 38394795792863734537418442100082446981886800454088199665390/50769339187606279704474759753358478618321989429160601091*y^15 - 473282357065986717739108607943459524793233586186098192843/757751331158302682156339697811320576392865513868068673*y^14 - 75226279239557930846140624150342136572540712447364932918381/50769339187606279704474759753358478618321989429160601091*y^13 + 118320075418107052752722102939273212262165337277899571710107/50769339187606279704474759753358478618321989429160601091*y^12 + 43593521203993419078958297736276479549563520632589638294877/50769339187606279704474759753358478618321989429160601091*y^11 - 174546761103647775540183130708556035641340359016522433719273/50769339187606279704474759753358478618321989429160601091*y^10 + 8014021965976476748876975774830085415092984108002136225184/50769339187606279704474759753358478618321989429160601091*y^9 + 191816265363887037561650530863796727395322766726376633899148/50769339187606279704474759753358478618321989429160601091*y^8 - 72574531493853522319985759419528551888032511039621182308385/50769339187606279704474759753358478618321989429160601091*y^7 - 112222747518237425806806454235723746601480336996410887518709/50769339187606279704474759753358478618321989429160601091*y^6 + 55710141146338194871890790824100511095481658976260922950558/50769339187606279704474759753358478618321989429160601091*y^5 + 37388394488832145377089625954147843469309695510038413750615/50769339187606279704474759753358478618321989429160601091*y^4 - 15776938583044353452637267979787438714424913612702487043513/50769339187606279704474759753358478618321989429160601091*y^3 - 5758760877865741231686327026451107523664111121970987853172/50769339187606279704474759753358478618321989429160601091*y^2 - 285582120513903684912416964751523386363528140151182725530/50769339187606279704474759753358478618321989429160601091*y + 1248145083520299989618338383948063001641902659765307743251/50769339187606279704474759753358478618321989429160601091 -1529408982662281279288292362531680003046431676047355892505/3452315064757227019904283663228376546045895281182920874188*y^27 + 3787582561851408420715199627747457532204927277051959480573/3452315064757227019904283663228376546045895281182920874188*y^26 + 1255866065845082631009144523026580163238306975408123713517/863078766189306754976070915807094136511473820295730218547*y^25 - 12433457694715086430165452888964163482728642754986374718781/1726157532378613509952141831614188273022947640591460437094*y^24 - 11411121301208302379979571439676132694333591220356652818743/3452315064757227019904283663228376546045895281182920874188*y^23 + 139085634290780547966842661700147220307473426364563810809113/3452315064757227019904283663228376546045895281182920874188*y^22 - 31026375181306449004724247910886248744199186322876014941479/1726157532378613509952141831614188273022947640591460437094*y^21 - 156122388868627528944556803250707424217246782596195929668025/863078766189306754976070915807094136511473820295730218547*y^20 + 179836914272038369849623757108889061125841807701488523294690/863078766189306754976070915807094136511473820295730218547*y^19 + 71417644494941818306661697239940339762081944770175806025433/101538678375212559408949519506716957236643978858321202182*y^18 - 5575224109407784401649903289674532444814367072032638383397071/3452315064757227019904283663228376546045895281182920874188*y^17 - 1917727968241714859583201530441076710973459855924176653301007/3452315064757227019904283663228376546045895281182920874188*y^16 + 7122578071079753286189038738845015656710735082935308779707379/1726157532378613509952141831614188273022947640591460437094*y^15 - 25729838860360700754969512461454251835990777405306240161491/51527090518764582386631099451169799194714854943028669764*y^14 - 7945809705132958045035266688487090294858066896052946515537952/863078766189306754976070915807094136511473820295730218547*y^13 + 25433790553822208020070643149975127613501240758758573187323625/3452315064757227019904283663228376546045895281182920874188*y^12 + 15587456595800256212349497730389083716474608992250733744410165/1726157532378613509952141831614188273022947640591460437094*y^11 - 22145103515792597145120580378299085614369885913738400226859957/1726157532378613509952141831614188273022947640591460437094*y^10 - 10849172128955127647338035699269769407785588246308550509101369/1726157532378613509952141831614188273022947640591460437094*y^9 + 1570989354701688410768979635884832576516521981394440453521591/101538678375212559408949519506716957236643978858321202182*y^8 - 70248574110402900464686346058883755604759596705944670181271/863078766189306754976070915807094136511473820295730218547*y^7 - 31925618000120964782400483910008390175957778319909159420266133/3452315064757227019904283663228376546045895281182920874188*y^6 + 2780831242990248295192087013763993678265644568154541764230943/1726157532378613509952141831614188273022947640591460437094*y^5 + 4924323989955711960167561677460088989540407630318704995081933/1726157532378613509952141831614188273022947640591460437094*y^4 - 1994202817783590214028333441771682730264231658023532047249237/3452315064757227019904283663228376546045895281182920874188*y^3 - 279068973647004987031729268374364073918965651051217455719124/863078766189306754976070915807094136511473820295730218547*y^2 - 248729489124414280664356626097117373385722341559257826837077/3452315064757227019904283663228376546045895281182920874188*y + 113894504569461781588610523437305502823023346135473121554167/1726157532378613509952141831614188273022947640591460437094 # A Gluing Matrix {{0,-1,0,0,0,0,0,0,0,0,0,0,0},{-1,0,0,0,0,-1,1,0,1,0,0,0,0},{0,0,1,0,0,0,1,0,0,0,0,0,0},{0,0,0,1,0,0,-1,1,0,0,1,1,0},{0,0,0,0,0,-1,0,0,1,0,0,0,0},{0,-1,0,0,-1,0,0,0,1,0,0,0,0},{0,1,1,-1,0,0,1,0,0,0,0,0,0},{0,0,0,1,0,0,0,2,1,0,1,1,0},{0,1,0,0,1,1,0,1,0,0,1,1,0},{0,0,0,0,0,0,0,0,0,0,0,-1,-1},{0,0,0,1,0,0,0,1,1,0,1,0,0},{0,0,0,1,0,0,0,1,1,-1,0,1,0},{0,0,0,0,0,0,0,0,0,-1,0,0,0}} # B Gluing Matrix {{1,0,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0,0},{0,0,1,0,0,0,0,0,0,0,0,0,0},{0,0,0,1,0,0,0,0,0,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0,0,0},{0,0,0,0,0,1,0,0,0,0,0,0,0},{0,0,0,0,0,0,1,0,0,0,0,0,0},{0,0,0,0,0,0,0,1,0,0,0,0,0},{0,0,0,0,0,0,0,0,1,0,0,0,0},{0,0,0,0,0,0,0,0,0,1,0,0,0},{0,0,0,0,0,0,0,0,0,0,1,0,0},{0,0,0,0,0,0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,0,0,0,0,0,1}} # nu Gluing Vector {0, 0, 1, 1, 0, 0, 1, 2, 2, 0, 1, 1, 0} # f Combinatorial flattening {1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, -1} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 882580758521672092040459058208184797181494491058085171133/203077356750425118817899039013433914473287957716642404364*y^27 - 2185459384520872717267089337704605514838943555926456098413/203077356750425118817899039013433914473287957716642404364*y^26 - 726293572951346009784142508406569368119928115434296518682/50769339187606279704474759753358478618321989429160601091*y^25 + 3589267304196083328679520535292739402936011828678611072700/50769339187606279704474759753358478618321989429160601091*y^24 + 6617393047896738304510563116587760789330759108927685983435/203077356750425118817899039013433914473287957716642404364*y^23 - 80323093987034648451294929048591985547911333369728318096161/203077356750425118817899039013433914473287957716642404364*y^22 + 17835527002691861444674516849299773986447701038176545112211/101538678375212559408949519506716957236643978858321202182*y^21 + 90195944583137622285921263591167214901368612080586995777525/50769339187606279704474759753358478618321989429160601091*y^20 - 103696883818341008375167616411506910095988950643619890429783/50769339187606279704474759753358478618321989429160601091*y^19 - 350871770651172335104388112595823080781218206713184926983109/50769339187606279704474759753358478618321989429160601091*y^18 + 3217207892544778031214822980017013258573468082988586053930453/203077356750425118817899039013433914473287957716642404364*y^17 + 1117210529233996659071399600191799547917315515454482458980097/203077356750425118817899039013433914473287957716642404364*y^16 - 4115115172393167217351498937042633538825862361593674062436125/101538678375212559408949519506716957236643978858321202182*y^15 + 14520754629646140684902898811496688933942094240524988642345/3031005324633210728625358791245282305571462055472274692*y^14 + 4593493029849818317543509623964674549412874178165727597846808/50769339187606279704474759753358478618321989429160601091*y^13 - 14640000707359132020907997768140020432972451483791798112924675/203077356750425118817899039013433914473287957716642404364*y^12 - 4519852622983478550022201037805824588730531611075870397313667/50769339187606279704474759753358478618321989429160601091*y^11 + 6387004347020279402101120744999977625877859488388663908640334/50769339187606279704474759753358478618321989429160601091*y^10 + 6323013180768695984797592069128877965513304939717385813754525/101538678375212559408949519506716957236643978858321202182*y^9 - 15424864847010819689572433269497915187467640476798228177028851/101538678375212559408949519506716957236643978858321202182*y^8 + 16416536617771858107204283921318368027339708272230079453241/101538678375212559408949519506716957236643978858321202182*y^7 + 18476558148089479516592550960519416064602263716974677134158025/203077356750425118817899039013433914473287957716642404364*y^6 - 783140334659544593061453750866312244399343726037367064428509/50769339187606279704474759753358478618321989429160601091*y^5 - 1427661274608465847493971199475426776556142042245141377461367/50769339187606279704474759753358478618321989429160601091*y^4 + 1128494828556969015613661062399414321740603504500846575990813/203077356750425118817899039013433914473287957716642404364*y^3 + 161086804560184969851697746975676038490062305533490599323182/50769339187606279704474759753358478618321989429160601091*y^2 + 144167236851850003205216835365568661168647179946872995641891/203077356750425118817899039013433914473287957716642404364*y - 63732166025374153828031638275410961960738226298797387583277/101538678375212559408949519506716957236643978858321202182 # 2 Loop Invariant 11276033251494595281976449027494301083075377782180625241681736166058695867270270154439087177205613542246991061201893835390964192176497/39570628592145246783900659403423237544271565676054514771940214610637663581491454705416392444446498453900780971306055701665865751823664*y^27 - 83135517113647748275619755008412880070330421762470683000733631853186842733740722034211485398314251934105485609172030405291441626796645/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y^26 - 56424046064311475302141041110719607332745710319712387719759226335335972728831213178158161441322813925309788396908441013976099970129347/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^25 + 273943635235238472130832758074662279915970237894491842428024934164237954689555434876330760724267785183607431063491623370084209620785691/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^24 + 263702288932108820182098941170815171350815358765642711184689284670939175862208573906346458566370942084319540805480272009959527969087541/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y^23 - 3071895427274596035997536218813158120488343154092618589628851266067123238478391007920229858160788923244751660029375557139323017129054861/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y^22 + 5548775760196907315081583777099824361861642522847912238264600544754545150112138982888230889263975862929769944476134398152067828378747/503016465154388730303821941568939460308536851814252306422968829796241486205399847950208378531099556617382808957280369088972869726572*y^21 + 576788901025721401002512707760658259293979674635380706252079584853798777267977083797312294747185084733847143400996329270868424162806027/4946328574018155847987582425427904693033945709506814346492526826329707947686431838177049055555812306737597621413256962708233218977958*y^20 - 3907704716064648169614954339932174741428286318431605953132413902877110568016771705855352199628366310431004696876309675607229978982367751/29677971444108935087925494552567428158203674257040886078955160957978247686118591029062294333334873840425585728479541776249399313867748*y^19 - 27022882610718295675499978011337532476140676365099144740697603382498459051071296261036211403445764349092732421503971808732819359264684223/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^18 + 40742663857128457403284718229130064890280916602059980992272962742501997074427827117457126238508582018949106441788161979305148410757404155/39570628592145246783900659403423237544271565676054514771940214610637663581491454705416392444446498453900780971306055701665865751823664*y^17 + 44959787315947530970688054180091352859371963138837327973025926851067289106895697746237371977348937108560209412210388724969089501153619291/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y^16 - 26179591389446029114550503747572028636416727701237533443577546820447730192718321755821543564748157068563011407258166402489156905700882887/9892657148036311695975164850855809386067891419013628692985053652659415895372863676354098111111624613475195242826513925416466437955916*y^15 + 156746034302942235765662845060023824019666193791851037885115672800521421064283419217879981862249514346688696527006283071057048524275903/590606396897690250505979991095869217078680084717231563760301710606532292261066488140543170812634305282101208526956055248744264952592*y^14 + 351774700690702710878151475690563107917682845737981171114648837018018618429135821240247885041416369279775362130280108029869760119197205241/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^13 - 182550079144427936950229603583453199615333697322077205276750883801227818040195492689655258295112062682236192389506260122168887139559591877/39570628592145246783900659403423237544271565676054514771940214610637663581491454705416392444446498453900780971306055701665865751823664*y^12 - 43775121018133263161356020870533635817570610662170829807590442480197951906744848900010796666867385415647197492983684732720843095664859110/7419492861027233771981373638141857039550918564260221519738790239494561921529647757265573583333718460106396432119885444062349828466937*y^11 + 481977447248478090387645123370261150696399881648998611744029906795366631871116395157779986036598136222324809941502019581103898925545082523/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^10 + 83218235843806210579209968696660184839628696984785169542179028047585411113514717861450310966543870178881553393415200874814364253863984325/19785314296072623391950329701711618772135782838027257385970107305318831790745727352708196222223249226950390485653027850832932875911832*y^9 - 584403191593380271876815374470967522041251243704398315694551934405582554480661277801550840033021295837409202593206608757883664937954045365/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^8 - 1111296853864642631254427946529114809861830439345299976079225287538010253271146324660117102146613724475094461337817076512624737334243345/7419492861027233771981373638141857039550918564260221519738790239494561921529647757265573583333718460106396432119885444062349828466937*y^7 + 702542852268987454588167862203913214764498331134651258211020726311572070087137646985947391145642109070820288082124765088476355152400752159/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y^6 - 13563500214087395348123275729549817190012334497877692640801979673740669655017909771101233998431170680505518432170328421261801496853238365/14838985722054467543962747276283714079101837128520443039477580478989123843059295514531147166667436920212792864239770888124699656933874*y^5 - 108615671967136075128517424763750410249462556100351174886012719035668629692404722963599764132179458681386567315646067819733688398352293857/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^4 + 675633322567146192442067104879935537530737031244655166940575519491264253627267240274877333328954303413839498610121768226745786232111449/2012065860617554921215287766275757841234147407257009225691875319184965944821599391800833514124398226469531235829121476355891478906288*y^3 + 12176180243201264946249003724974767623598166922724607534269684374054456387337711558593913850048379006890835867045612087915968871776915361/59355942888217870175850989105134856316407348514081772157910321915956495372237182058124588666669747680851171456959083552498798627735496*y^2 + 5644627786164575150035682287223248471201650258384324736030190795833533544802896643827552201514991545284382402986654681757699140692183571/118711885776435740351701978210269712632814697028163544315820643831912990744474364116249177333339495361702342913918167104997597255470992*y - 398556367227435073846629447436917379322767596896237530019044601772798333865454174151260003689824971631739361708943047391214000992125423/9892657148036311695975164850855809386067891419013628692985053652659415895372863676354098111111624613475195242826513925416466437955916 # 3 Loop Invariant 3160092481956620366716313989105976246513302065699391674134421159047465240364461408667871056019286164677331674067288006541829447320334732296143548019283646425085727487318145/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^27 - 8030355930684861091700173755755989892301560479447333931343715622396468622659980786461398617702984514020574036900744970248184714277007156423980858337679276723278013916229589/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^26 - 1258739699303491567952560604792779300208960358504681628947712587236314929436367436361141604995794512864586308835793525845413612572611228583910814489219510893428392325133151/4366854094629827193483159182604601698295874557794567540847878283015238027225963797497724535451615188678344099085381065185507768493468356935579624245448931915108949861453016*y^25 + 26190531328301937257127556355318629910681682651390944310469842195317732547737998822209481462704161547700291566355983511728372200811261407528694091878027433716485539340930889/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^24 + 358626594288960535377842235784680888189544646913028681865275013701796455568876914534663017702256863471551103872693571301686264996704243753063118883846836315337991740901345/592115809441332500811275821370115484514694855294178649606491970578337359623859497965793157349371551007233098181068619008204443185555031448892152440060872124082569472739392*y^23 - 291367053095068360271730931017791992849311217250235310547574273760059573622835527205963576007520641522374230277741727273002278249702662696588128976509507169933107746836848037/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^22 + 71691528976046829687532599068195942684656108495543251967879658939961694556673439836028284752603873061045961842469053460383720532239416439857985976499154231388419631134536657/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^21 + 81068959081233058892210577442643988628307459219551242022895120435801587381120187331072762956300397266038964407585339351173106960797573591718589003098025095876225094760966599/2183427047314913596741579591302300849147937278897283770423939141507619013612981898748862267725807594339172049542690532592753884246734178467789812122724465957554474930726508*y^20 - 391437771132548537190049735195004403830877726089334449910770066253438934168918207623490546420094656714242319200438197833764906148173895448217690558106329479183249671476951051/8733708189259654386966318365209203396591749115589135081695756566030476054451927594995449070903230377356688198170762130371015536986936713871159248490897863830217899722906032*y^19 - 2498834419999786634023196289200799135447074622286940489410892870533508932997117555919326682930005712889968067878075439379575182675511726818851769161914348275978474642616637253/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^18 + 11875144860458133039122566464043500684592209317177517014012652967988436139653016701666477379460748056557299049726380908549571206019442866885430377642306637158590208817021752755/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^17 + 3552326708460866875806357712840360349263068626686193480124217772626928446197216520877849519117324071450086356994325288964253155149782416148327171911429398906590129119522251407/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^16 - 15068238546914904444427406544051816641071291401699027687012963139480660491642024235660339711083755668429075929745278326594020518530043037140656506220738430811569218125204532743/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^15 + 72676817136474452739164369124877568524567687585423507352644452643414249765492771465749234632090735435078443650571659120617467300932571561661689308668439486253845858216948843/521415414284158470863660797922937516214432783020246870549000392001819465937428513134056660949446589692936608846015649574388987282802191872905029760650618736132411923755584*y^14 + 1043427293447119754955479583863606964845799754673361832722322486529780770553241701789770220241986394913841483063151873092886698121583426662619247017730155471000666498577142395/545856761828728399185394897825575212286984319724320942605984785376904753403245474687215566931451898584793012385672633148188471061683544616947453030681116489388618732681627*y^13 - 55958124365954132148402696216552208682928328191324224710981918277315251037792157028394084816228148434838643682566466651585134477291499072704103737648535623266369695193861328033/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^12 - 32194046667272170384197836385457454552213140972558607370807829312394634000505986503859796204656379730817046252093841387748631270065080780046808708940889197142939411804531233195/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^11 + 48126505706077345223415784540833457645884955971969696286255058538115437974422461290242315722676000212319477285598886624527393635429779307425736390021333390216093940155878803399/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^10 + 21645848919972835407537745126526613108992017074004314906121546256088331818106386239501805340240146241706717377159133420582001187326590784696119464917637784292794537208317319635/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^9 - 57701077201333365029322084463484098189719978843539167525897690967731653772590656185023077818403887547527635564406380909925947342394057110170537227226675257257633747705881267535/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^8 + 51767724792584241915101545654376786574112244004459284803846399315874131556210247714464769006270761676389627373129932286787778568392098381778029106314295524709855136668612427/545856761828728399185394897825575212286984319724320942605984785376904753403245474687215566931451898584793012385672633148188471061683544616947453030681116489388618732681627*y^7 + 69174082582738659824468309697559729075215857324341963824925262867901874720876592455764855018462509551331826419354921224806856170169017342563177014879995194823336003438056140553/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^6 - 6638604826459475611270376780199068469050083331789663621669631818746995863077629067735577267566727696139843428570371911906269640346046806356126357119466816121007072327613908355/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^5 - 10804186256398786786440432568634920548954089110519447228914595453062934021688491766163112520635115497542743095571311437705233703515288508345295170042550016198374072497074415805/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064*y^4 + 4577403807495793507128823151899628366322052508537018914986155042784830350855891976967026161354601220558722076090597178525375477366497176315660331964302901967439059345059287617/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y^3 + 637699734442681558837964189857080136380541826969046913330785427276020601731698318839705239416031388854671297608884718572979805284313889482287497230295062435303997316438225031/8733708189259654386966318365209203396591749115589135081695756566030476054451927594995449070903230377356688198170762130371015536986936713871159248490897863830217899722906032*y^2 + 510345369918326597975953934210674423697267119293119926709178859771218338681212525456622983518335206583284309136125461023969039048512656905295517522010642586112170765539446973/34934832757038617547865273460836813586366996462356540326783026264121904217807710379981796283612921509426752792683048521484062147947746855484636993963591455320871598891624128*y - 252325637173153124350614747413322856917171033544979994227408591481764617027017746687344200201137177205636550617312128429697456111512767148206854914968094438180292654368749145/17467416378519308773932636730418406793183498231178270163391513132060952108903855189990898141806460754713376396341524260742031073973873427742318496981795727660435799445812064 # 4 Loop Invariant -12995341080259158371189979849299820346815145224082466944880758643635602571492049993284142256818955204952978964882170369197259530182630686194439710991689798369349085568165517923366286267553993830457831821507587577229494571918079842189375804653793679941/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^27 + 7692496521668681471520354574385389843003049388602615037853316768106294090738461805714412170127911475761702253118212908619156354598612838870557401061787884603035667217891915728218856417642081058142706770515132023597638988789094594972431112231493053583/38290641515573957546887134016075942954799514508157907187861909996570891850008525696737377813163749413225183908792960886224386539002040477631377689843879530715453940673763012748425700838597101658345010203918044474008814379073426845737216689435006474720*y^26 + 45931413994301855274254088178651813672086583434714424026524071730588460566419952903586513594426977958740024674743559217738600852910788288177077244184597884550226247979173668678099025799936865761283120445055663199869679891991060368470216324191431659863/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^25 - 17148091608649267913068475067046085134337555836350828069602596155987287946430884653948412052446935583225339927229311575225318017650263171350148229221573025571516946753196328823499763660176398868282393869550485448365565647883457492927019187381060455879/12763547171857985848962378005358647651599838169385969062620636665523630616669508565579125937721249804408394636264320295408128846334013492543792563281293176905151313557921004249475233612865700552781670067972681491336271459691142281912405563145002158240*y^24 - 119258890720551681987760259728524794447657704297475502818923343059608368465693274850573641275681631113203149927084128740190531529793462866350372036848209808639047433848570897975004920541626137636558390308702538016664193946915056136268390485419768876149/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^23 + 116567886341530306423764868848344749762179252687476833152334387894499054008542361242647750577271679934015254792829423339107143306570061236228259571335492495239154246033385419488062115223256518241907841764431121182732143195801030752799559692156604991247/15316256606229583018754853606430377181919805803263162875144763998628356740003410278694951125265499765290073563517184354489754615600816191052551075937551812286181576269505205099370280335438840663338004081567217789603525751629370738294886675774002589888*y^22 - 2253519862389954840674631551938897466507000896618542205779454581571838566477016453211504966102575981384564344078809746384105284876840921848153234930376412624168063212408747221034453997772846421826859645321126326367320556395421821669312718467198470471/865325231990371921963551051210755772989819536907523326279365197662619024858949733259601758489576257925992856695886121722585006531119558816528309375002927247806868715791254525388151431380725461205536953760859762124492980318043544536434275467457773440*y^21 - 148154848660893619421492040826532478626515762891035716101406506478332489491614571615192986280441292346339507181513799403128243295958573073429981100362033575087047776049222907655538940212300979026993587673292470242670852965822019110960143066226180023861/4254515723952661949654126001786215883866612723128656354206878888507876872223169521859708645907083268136131545421440098469376282111337830847930854427097725635050437852640334749825077870955233517593890022657560497112090486563714093970801854381667386080*y^20 + 275585273637111667826457495420726366755030962765730448671399227648053956508205765656171302565534091234727892971765023104895581736051991340578680800230197517193932162304189011298032508021746015555221519651873084120488241160569168824803442699436320721729/7658128303114791509377426803215188590959902901631581437572381999314178370001705139347475562632749882645036781758592177244877307800408095526275537968775906143090788134752602549685140167719420331669002040783608894801762875814685369147443337887001294944*y^19 + 3528498548518474136778939324545948734448335831599358369952702112458888678611642877757209524778084601350930393038247163368339014996593264016578812533906695024412497442734235001071493723860993596399223693873939169113337809914895742432673513256813650094933/25527094343715971697924756010717295303199676338771938125241273331047261233339017131158251875442499608816789272528640590816257692668026985087585126562586353810302627115842008498950467225731401105563340135945362982672542919382284563824811126290004316480*y^18 - 44926089858706289084084028019710038343215078177043433436847762931232345759493142343289589672012485684723944654432143443684807446198973973951060936560412318929130138636841532827473136649229403951647685897157106914114475037736320487230990131841639679872933/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^17 - 10493548754945121756122697493448422745171569980938722543480609449247292760698227454567319722931866174024892004173437907300903880076798509846983826589693509637543372013503882155587749403060355005607492238487836645581523539869531046105404628190412287919011/76581283031147915093774268032151885909599029016315814375723819993141783700017051393474755626327498826450367817585921772448773078004080955262755379687759061430907881347526025496851401677194203316690020407836088948017628758146853691474433378870012949440*y^16 + 23584697953847309691416785226128764131702818609547272850563506830317595950323271136643790272195861018835722322266043305759706438044315169317889126679511709328708240275052825916266341337338084942914265006887922907992344536945121299569929987363416291492897/30632513212459166037509707212860754363839611606526325750289527997256713480006820557389902250530999530580147127034368708979509231201632382105102151875103624572363152539010410198740560670877681326676008163134435579207051503258741476589773351548005179776*y^15 - 25173326233670593203263438012059765263590173232231539467626534958935642063343335469202268219534859578097022965254505507895143296242830574774216260714058685830490954910010709427851701036816391134112968070764866826718642134544949390166430711352173477243/2286008448690982540112664717377668236107433701979576548529069253526620408955732877417156884367985039595533367689131993207426062029972565828738966557843554072564414368582866432741832885886394128856418519636898177552765037556622498252968160563283968640*y^14 - 268139070145443260154975910641605488799290638107213711133270717948277843371902158397928930300976001338757237736578603005169497259279830522356151247293848205225060935262687096647763147424093895810200543869626212648764908325136069479509520065444130935238957/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^13 + 185736071985259841618030669986862291354619099170367696614047229353761199281193607422943637364430249026770329319732550970511229527925717250440436436998567028640658637287019779731742688320947937087233034892371205170687558381531346020535327013506579331380539/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^12 + 280710517380813480695063962215769693617174071639579519456667090762492106110665588630515055131993820140758752699006373443021286555129575783291592252292413570572199540257569602153903000274036102420584158949019060954802843311060008588777154752839640624320503/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^11 - 34078140680574429910259586518664811214068338586659240113411765881664034126931677909121342696446486491587662377868223133842877914254677013140464354310711530104342674515341878640591501932136091018096370850029464249407084021166862415133013511023021803759763/15316256606229583018754853606430377181919805803263162875144763998628356740003410278694951125265499765290073563517184354489754615600816191052551075937551812286181576269505205099370280335438840663338004081567217789603525751629370738294886675774002589888*y^10 - 10855578417605984063608308709958463335570587121591306027980129597333256092169523263230719371639477310279376429964792410890600280867032213802623680422295140960073179505887073526872618152798553297159213549849939037921276473111857143704159734286920135843177/7658128303114791509377426803215188590959902901631581437572381999314178370001705139347475562632749882645036781758592177244877307800408095526275537968775906143090788134752602549685140167719420331669002040783608894801762875814685369147443337887001294944*y^9 + 105454698798886878060262673428991165862824955894961837037345792821948812057253624125297782953717123256460397617350971395204320993733539505791119637652096044225156167955443826648250114309445081986759701329891986579098877423285323684067596376389180612026363/38290641515573957546887134016075942954799514508157907187861909996570891850008525696737377813163749413225183908792960886224386539002040477631377689843879530715453940673763012748425700838597101658345010203918044474008814379073426845737216689435006474720*y^8 + 6777770548277905787214106779918178894963666884852851425728123700974040014719433486609112416247667794795165024142356470536440577294147799114800585010254697667536092834566551538470198972625496099037589446844223406327382124447993834460166127434541924069903/25527094343715971697924756010717295303199676338771938125241273331047261233339017131158251875442499608816789272528640590816257692668026985087585126562586353810302627115842008498950467225731401105563340135945362982672542919382284563824811126290004316480*y^7 - 256713618385528582788234716803191636461400809935995562159382218212561505813490365217015831865799171302650858527544076488320012154931168899158494916139538261239036782322889275382836492271618484697374245805910257893870428819814332407763679069639360670202137/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^6 + 19657017765250820340887129804368739606143348258927222081867302886633251950420987382741500348677215945940769831697673983678410657883010347944376880661041358181478190965649909248980663330427010847710123726221538666012572931765947143972354894503593691748769/153162566062295830187548536064303771819198058032631628751447639986283567400034102786949511252654997652900735635171843544897546156008161910525510759375518122861815762695052050993702803354388406633380040815672177896035257516293707382948866757740025898880*y^5 + 13136388536417037338953184772083436130358559896288189838022648576758570474269516302383106298435129986988811082038745814074812737525321573378171887048376932479614031624425625425944390698781025994731540408661492307830337690361189510716376567231090933879849/25527094343715971697924756010717295303199676338771938125241273331047261233339017131158251875442499608816789272528640590816257692668026985087585126562586353810302627115842008498950467225731401105563340135945362982672542919382284563824811126290004316480*y^4 - 141877614990954150342783973294923882742793150098359871361291284856605181426541822158693723018268013640632739976763709846943647837118677393594405017991215249252344623972505408234971108071507481320588955530761947193511370723260447464310945982983986400369/2595975695971115765890653153632267318969458610722569978838095592987857074576849199778805275468728773777978570087658365167755019593358676449584928125008781743420606147373763576164454294142176383616610861282579286373478940954130633609302826402373320320*y^3 - 870299194950849494750124107302988128140595549178383833402900758988203962855491609735698991390946995441129726671348167267133774767752168724933098748887123075134663712680032300974982389192892359388857902738027821527745999396148257754058416436475035505893/17018062895810647798616504007144863535466450892514625416827515554031507488892678087438834583628333072544526181685760393877505128445351323391723417708390902540201751410561338999300311483820934070375560090630241988448361946254856375883207417526669544320*y^2 - 875432334051175372965568017350829615875682140632812131603539838293981689648901955143593323419371743456293085718801955709516895505877557129465960265513017482440780934490777840422273547972387147887554003975671377539672707521216625320000384816308978227253/51054188687431943395849512021434590606399352677543876250482546662094522466678034262316503750884999217633578545057281181632515385336053970175170253125172707620605254231684016997900934451462802211126680271890725965345085838764569127649622252580008632960*y + 271194369546353404276706359056460505060750970577004503449428417512965229295578029975120416501870837730943993878200012914443255185163847167503343341444459249270545664507913093251691932207249045751913507765126496418491962693523376307270622074691750947729/30632513212459166037509707212860754363839611606526325750289527997256713480006820557389902250530999530580147127034368708979509231201632382105102151875103624572363152539010410198740560670877681326676008163134435579207051503258741476589773351548005179776