# Manifold: Census Knot K8_253

# Number of Tetrahedra: 8

# Number Field
x^28 - 12*x^27 - 3*x^26 + 202*x^25 - 587*x^24 + 3158*x^23 + 6273*x^22 - 4292*x^21 + 28368*x^20 + 6475*x^19 - 269531*x^18 - 273440*x^17 + 506126*x^16 + 640265*x^15 - 466258*x^14 - 628558*x^13 + 305695*x^12 + 243352*x^11 - 172645*x^10 + 78574*x^9 - 4671*x^8 - 42518*x^7 + 19394*x^6 - 3859*x^5 + 1497*x^4 - 76*x^3 + 70*x^2 - 7*x - 1 

# Approximate Field Generator
0.782978299240372 - 0.225133094364740*I

# Shape Parameters
-3301942998570769898932049855289837444283522670643699474546137790464592789/37857571356319283129118200861447528220346064141778483067604370828183412736*y^27 + 39478583745844331836699091222127756027831327427415435842351912270067272449/37857571356319283129118200861447528220346064141778483067604370828183412736*y^26 + 5855583229297413073405025996856016019739364194849676667251099439370928359/18928785678159641564559100430723764110173032070889241533802185414091706368*y^25 - 5214075970862949867285540256023677902923231695641795055486706104668467595/295762276221244399446235944230058814221453626107644398965659147095182912*y^24 + 1909035808509147630575376732032233595448962307890588011421049377930227153447/37857571356319283129118200861447528220346064141778483067604370828183412736*y^23 - 10328514818910180064196727912140565254245232843224434201039055203103005138181/37857571356319283129118200861447528220346064141778483067604370828183412736*y^22 - 662953652909837285127234110158700345589406182139167389823101579695359527119/1183049104884977597784943776920235256885814504430577595862636588380731648*y^21 + 3372526515694667860575013632477166599689123288862086101101613842722309689405/9464392839079820782279550215361882055086516035444620766901092707045853184*y^20 - 23169278388078931938985906508658227039073231835471071334564753405029887787441/9464392839079820782279550215361882055086516035444620766901092707045853184*y^19 - 25949979734429648873367649213025539709018936351755820914883814700624607424547/37857571356319283129118200861447528220346064141778483067604370828183412736*y^18 + 445489642012468895451527579044833815952769469018632623087532286532448944268501/18928785678159641564559100430723764110173032070889241533802185414091706368*y^17 + 470890125046963953719984800319028032297619536475191667826440133870207271603499/18928785678159641564559100430723764110173032070889241533802185414091706368*y^16 - 412648069742114789932309190893428749220002122020356770023511487519501737450519/9464392839079820782279550215361882055086516035444620766901092707045853184*y^15 - 2200690685616713973029647140637498616435185082696745650881139245302479467573345/37857571356319283129118200861447528220346064141778483067604370828183412736*y^14 + 1490791137612869158153065081076576834919823876900093774512945827211160315631499/37857571356319283129118200861447528220346064141778483067604370828183412736*y^13 + 2180831277474295789852288354986118822357822278588598252069761693888062111874891/37857571356319283129118200861447528220346064141778483067604370828183412736*y^12 - 484686699574812044434324483063682172456686839843517480168279528319937004044691/18928785678159641564559100430723764110173032070889241533802185414091706368*y^11 - 445639316005614729285633172993771801971543096211758458915962578918912024897433/18928785678159641564559100430723764110173032070889241533802185414091706368*y^10 + 572813973351032873013220470103670469386513610868474002384593140921295231882715/37857571356319283129118200861447528220346064141778483067604370828183412736*y^9 - 214319656196030258027467066967917866553855178860076835024138882119888550001137/37857571356319283129118200861447528220346064141778483067604370828183412736*y^8 - 3693168728132854085176375127955551037915967711568311917599537482492496881469/9464392839079820782279550215361882055086516035444620766901092707045853184*y^7 + 72859978073675578668387742482764186499566217199455073411579951781195317704897/18928785678159641564559100430723764110173032070889241533802185414091706368*y^6 - 14612130814225681800414385094955209830515408426734620574800655504453131483251/9464392839079820782279550215361882055086516035444620766901092707045853184*y^5 + 6753032261814697662800102969269477529053246746670122483061389886250782826139/37857571356319283129118200861447528220346064141778483067604370828183412736*y^4 - 287365194158591099512319409617783815456007029328485937608693165354197169727/4732196419539910391139775107680941027543258017722310383450546353522926592*y^3 - 25944660934506893657888509870433248148628826727883734844286116152006467203/9464392839079820782279550215361882055086516035444620766901092707045853184*y^2 - 98409124157731892186848873212560583712092853887521737269916426737124735961/18928785678159641564559100430723764110173032070889241533802185414091706368*y + 45680760908628107692116640598817340206342934841326646375331560868621138789/37857571356319283129118200861447528220346064141778483067604370828183412736

641898015358088396375871381802632937950119408849858014151332717016617569661/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^27 - 1230939822373137846210671364300955116095385576928136684297251058606912009997/7760802128045453041469231176596743285170943149064589028858896019777599610880*y^26 - 10111662018364100933965385631405365788432045213205091800311022609005356430839/19402005320113632603673077941491858212927357872661472572147240049443999027200*y^25 + 950253170030856375766751958301796562570206777859841565232853750183557553497/303156333126775509432391842835810284576989966760335508939800625772562484800*y^24 - 2581311410980830893071714161237728215091256035331707249271942386865666619127/1552160425609090608293846235319348657034188629812917805771779203955519922176*y^23 + 1175324994085863460749137654735683754796363278957056482972926859132312409627413/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^22 + 68317389347042038797232577005100432600808247631887182817292773939378816346993/303156333126775509432391842835810284576989966760335508939800625772562484800*y^21 + 1962943250060399518319852776417122076760594205038127590097015053143956530856499/9701002660056816301836538970745929106463678936330736286073620024721999513600*y^20 + 661206296939308293403926339541939516270209812979393466855117972179510322796997/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^19 + 9309475123835841703356945352942554858334948675211102635666908578712569114851231/7760802128045453041469231176596743285170943149064589028858896019777599610880*y^18 - 77582668721772559480418639755685820561227448834311420132388807780557260216275953/19402005320113632603673077941491858212927357872661472572147240049443999027200*y^17 - 295951193678772484920683378335577864767700676027991055538814802265717998940799351/19402005320113632603673077941491858212927357872661472572147240049443999027200*y^16 - 43727846318715495772291063848553329973952584471127612380300583058907001032552067/9701002660056816301836538970745929106463678936330736286073620024721999513600*y^15 + 1127094169328118373051904828165645758317228232869106344218676838432015341748618129/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^14 + 170417464326380054737776354799133817565479292235246931660404848161971022837171769/7760802128045453041469231176596743285170943149064589028858896019777599610880*y^13 - 951754971104555894380809244554129618405659080189955497112364704493389994090557723/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^12 - 471479826687554863760468874081262795048772969875824153060258935399576192507670613/19402005320113632603673077941491858212927357872661472572147240049443999027200*y^11 + 44397609301133760611959788088703895507434405079667854377732273512869266414043397/3880401064022726520734615588298371642585471574532294514429448009888799805440*y^10 + 76175933769132823550189132098377543214765748153628107256203340265638139658172489/7760802128045453041469231176596743285170943149064589028858896019777599610880*y^9 - 135681683498821501750884751159715632774507379275034584408142484294636164970157471/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^8 + 14736352800703131815395425780856848280882716531041107104730266319059299653814213/9701002660056816301836538970745929106463678936330736286073620024721999513600*y^7 - 7889413144104759586292496097332928410183895085231268080711473575763258772701497/19402005320113632603673077941491858212927357872661472572147240049443999027200*y^6 - 13602949444180976218621254470575167394881974423427513367414847353080374486802001/9701002660056816301836538970745929106463678936330736286073620024721999513600*y^5 + 14374750868902179952976226911817688965116163586926448026641065456729658900097693/38804010640227265207346155882983716425854715745322945144294480098887998054400*y^4 + 89563327920817306022542041559371397633655419961581272176460629276788125467983/2425250665014204075459134742686482276615919734082684071518405006180499878400*y^3 + 85604123117947144074753911415955970478298057142536375762969262115915038057641/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^2 + 25391208949111219905982145688468361607994904679981042516004193355850043436201/3880401064022726520734615588298371642585471574532294514429448009888799805440*y + 71664230981535489735929757411339093047211339478555291407310942081221648536043/38804010640227265207346155882983716425854715745322945144294480098887998054400

-3147609940382442384727917917547879612910408607979989603795159941145842846753/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^27 + 7283623925746906623981763847550839730572585562720116734859744201748851621905/10865122979263634258056923647235440599239320408690424640402454427688639455232*y^26 + 12299751463091119907519064473661356007258060658512373706012092266118059054787/27162807448159085645142309118088601498098301021726061601006136069221598638080*y^25 - 345709840674851473715859145785430450341158819401825100699099130577496844529/30315633312677550943239184283581028457698996676033550893980062577256248480*y^24 + 317180776295091155465500904490107582106336258811735040199996209300422072078063/10865122979263634258056923647235440599239320408690424640402454427688639455232*y^23 - 9356866145200138205273502777413125921014467236731824742452901530805203736519929/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^22 - 22975696875985828350464837551583173455122218763226003221756431973146976764933/53052358297185714150668572496266799800973244183058714064465109510198434840*y^21 + 486467817164786501751735449936492054562704024360294669367564371447073996121233/13581403724079542822571154559044300749049150510863030800503068034610799319040*y^20 - 4618839322303608766462974412316293588570538842714830965880240521169163980096521/2716280744815908564514230911808860149809830102172606160100613606922159863808*y^19 - 12012538285216526739054780665528490901726194399707927705595198288129889157387051/10865122979263634258056923647235440599239320408690424640402454427688639455232*y^18 + 404164661980596374061224314789248865675595303301386189195438109797781714600020629/27162807448159085645142309118088601498098301021726061601006136069221598638080*y^17 + 85508706520106177978626993349516324688712856635451513889458456492010420139243669/3880401064022726520734615588298371642585471574532294514429448009888799805440*y^16 - 237425208143378000269093096478521166174837907367942562249406432338627841988415689/13581403724079542822571154559044300749049150510863030800503068034610799319040*y^15 - 2217896851239155102627398904225092891611130059214042435680782205815551893589577637/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^14 + 74403335043058525729606635144999522605184586492098029149252630137503152489263603/10865122979263634258056923647235440599239320408690424640402454427688639455232*y^13 + 1746754715272960159113764131834863232059972121886444067718567481815620421750807799/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^12 - 91006348834962578569456053858268880333047990056066345028903912662512753483549671/27162807448159085645142309118088601498098301021726061601006136069221598638080*y^11 - 51974912281341057235169907686683555694596557713770854834644679921478779239232425/5432561489631817129028461823617720299619660204345212320201227213844319727616*y^10 + 65483392462093905185635514312758102482109245086322881569470005012276496748642211/10865122979263634258056923647235440599239320408690424640402454427688639455232*y^9 - 223484562813416651154962633569072865602732773133901169580747532326684788694738357/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^8 - 11464205803840524040651112958006553421641635770174938483429395335284215712091209/13581403724079542822571154559044300749049150510863030800503068034610799319040*y^7 + 47539689021636372920872740098247662254863028555147136965669755805898394261308621/27162807448159085645142309118088601498098301021726061601006136069221598638080*y^6 - 8150728294159446345115961946837145111180868511930933974407726967835173604597227/13581403724079542822571154559044300749049150510863030800503068034610799319040*y^5 + 13541142791314713425881834902828152569054988077736504558033354127695159610837631/54325614896318171290284618236177202996196602043452123202012272138443197276160*y^4 - 55491800728862236102803698297347124346378601651125102573308251957847332091189/3395350931019885705642788639761075187262287627715757700125767008652699829760*y^3 + 14566345665771697838239216622290642904337895310297753816346703441174203981739/2716280744815908564514230911808860149809830102172606160100613606922159863808*y^2 - 5341976843010168154541114339903261626375144882193122853146139059658067091213/5432561489631817129028461823617720299619660204345212320201227213844319727616*y + 84264064261639895207739478889922376239693035685333262472792316666004328605561/54325614896318171290284618236177202996196602043452123202012272138443197276160

-225749145355309559099335519425301341274939767577990542440854492021622447/18928785678159641564559100430723764110173032070889241533802185414091706368*y^27 + 2743426124249630317065696415782085101572890316137014523770867736767004375/18928785678159641564559100430723764110173032070889241533802185414091706368*y^26 + 115681322017764894512622231299480220443151831751923470050489313556033625/9464392839079820782279550215361882055086516035444620766901092707045853184*y^25 - 354254156662420818651979627398540383366681908229331629898370351991597513/147881138110622199723117972115029407110726813053822199482829573547591456*y^24 + 139943614218265698785582882075230708397203388773322904893027737766005438149/18928785678159641564559100430723764110173032070889241533802185414091706368*y^23 - 739566210618048990807273768687002271702905238986829259049896821725548391691/18928785678159641564559100430723764110173032070889241533802185414091706368*y^22 - 80911939886072663926502203779831895011898756798628025692989739272800606613/1183049104884977597784943776920235256885814504430577595862636588380731648*y^21 + 274840521506055216326784908389114207256031698484768389923583286376223743955/4732196419539910391139775107680941027543258017722310383450546353522926592*y^20 - 1713395862107546867385768266047568728402447091075327707586934621697718567315/4732196419539910391139775107680941027543258017722310383450546353522926592*y^19 - 560299247316837596327963685717901001566234196833709235900475385272336254057/18928785678159641564559100430723764110173032070889241533802185414091706368*y^18 + 30122854266240908162925022128837490757949170554273721995730655876122060628549/9464392839079820782279550215361882055086516035444620766901092707045853184*y^17 + 25678013327490740478149806324854178899402358584728636964827849125312151983271/9464392839079820782279550215361882055086516035444620766901092707045853184*y^16 - 14404708036263849921489261223497785253374592356373918212722029365934293462243/2366098209769955195569887553840470513771629008861155191725273176761463296*y^15 - 109686948321671421426671540094661119801433588348836543097614705273353406742207/18928785678159641564559100430723764110173032070889241533802185414091706368*y^14 + 120844870926016130119717894490716357843642789631435512966720140733648363665809/18928785678159641564559100430723764110173032070889241533802185414091706368*y^13 + 90381811489029561461603964474093398673217472982171079966332518676720600318261/18928785678159641564559100430723764110173032070889241533802185414091706368*y^12 - 49052436316637895761258649615923608418294199632427149319460942593760107568169/9464392839079820782279550215361882055086516035444620766901092707045853184*y^11 - 6071651874305398164955980918757252084798145367587491633197168028792677148319/9464392839079820782279550215361882055086516035444620766901092707045853184*y^10 + 59505983764935062922356655583152793323782401194860443682481826268949829278481/18928785678159641564559100430723764110173032070889241533802185414091706368*y^9 - 38715398870713226386556562018656475909457232203836438606025822921490295705871/18928785678159641564559100430723764110173032070889241533802185414091706368*y^8 - 26688133277484498464143842735132513924732688751419045179974962191081652791/4732196419539910391139775107680941027543258017722310383450546353522926592*y^7 + 5771363801716169339964240267795717616940896445441589005552059113597284705307/9464392839079820782279550215361882055086516035444620766901092707045853184*y^6 - 1744546874233062721786543019196476203459890312989898204353301799591823115751/4732196419539910391139775107680941027543258017722310383450546353522926592*y^5 + 2546048762720644883129968062483777461629046492231244011030321368772795380105/18928785678159641564559100430723764110173032070889241533802185414091706368*y^4 + 34249566363621363309116132572464562580436218352885265056928248882432678821/4732196419539910391139775107680941027543258017722310383450546353522926592*y^3 - 7587711584588127656295960895549100547192794761157384423211526254699190171/591524552442488798892471888460117628442907252215288797931318294190365824*y^2 - 3383525985141875409956672726794189673921233453764467684933512863455620629/9464392839079820782279550215361882055086516035444620766901092707045853184*y - 27439911850873556315762910589455789142125992758147927204607335468761370405/18928785678159641564559100430723764110173032070889241533802185414091706368

7823189552308824562998439737369811985996870699548163307727190040437726053/37857571356319283129118200861447528220346064141778483067604370828183412736*y^27 - 97180217626276664654913326703727581276245971065221659167272418275717305425/37857571356319283129118200861447528220346064141778483067604370828183412736*y^26 + 8004507544458929073851886005009160034920357664385472959585171074377047145/18928785678159641564559100430723764110173032070889241533802185414091706368*y^25 + 12437464500195135842753866241737609790709739138268971417932770211305957183/295762276221244399446235944230058814221453626107644398965659147095182912*y^24 - 5259613991475737601492633278607110407354336757676921628738158935134509045271/37857571356319283129118200861447528220346064141778483067604370828183412736*y^23 + 26614668414700415600524449422646099847227079977063687737223515525632566028821/37857571356319283129118200861447528220346064141778483067604370828183412736*y^22 + 1210823538835096138109140142511883291684785532970037319635425247517589074759/1183049104884977597784943776920235256885814504430577595862636588380731648*y^21 - 13697911612906067037115198719467411025689891717728518347776087550952556271821/9464392839079820782279550215361882055086516035444620766901092707045853184*y^20 + 58854586820668851661359948249903873204378930290057660279502845609506662857281/9464392839079820782279550215361882055086516035444620766901092707045853184*y^19 - 42021961201116088710528728735163375546963189562309927920725458108285274956589/37857571356319283129118200861447528220346064141778483067604370828183412736*y^18 - 1067271041478889721081450055033024167053370746435835912704950536744922674107845/18928785678159641564559100430723764110173032070889241533802185414091706368*y^17 - 624096833579193598801619101848366878772722693023592264344929135796196961697659/18928785678159641564559100430723764110173032070889241533802185414091706368*y^16 + 1225324971361446012053029477788522381454972813157474259484903013536749769876919/9464392839079820782279550215361882055086516035444620766901092707045853184*y^15 + 3358322179740550399098959254873367674334277930364777700127903381162853721521969/37857571356319283129118200861447528220346064141778483067604370828183412736*y^14 - 5848315399897121896124173655704072413402114021326673178415403419176892741593019/37857571356319283129118200861447528220346064141778483067604370828183412736*y^13 - 3426537241007260991516108203365117447374397176266500657865441290226295896790075/37857571356319283129118200861447528220346064141778483067604370828183412736*y^12 + 2286170603833670957319048195250691748708567833543487017212712526649836388823363/18928785678159641564559100430723764110173032070889241533802185414091706368*y^11 + 467207712391916493093073670420527070751468399394704838462734047040363751180137/18928785678159641564559100430723764110173032070889241533802185414091706368*y^10 - 2241913192269586475250131974445754794265515934347009572094485882369195264215051/37857571356319283129118200861447528220346064141778483067604370828183412736*y^9 + 1187513269234146454226259874027766076374231729214771386125949371158649118771137/37857571356319283129118200861447528220346064141778483067604370828183412736*y^8 - 62715443648716194390308194745293064585111640474416576458633146699693292098675/9464392839079820782279550215361882055086516035444620766901092707045853184*y^7 - 173699524148799009555136580632655935086139409624831027594171408034650611923665/18928785678159641564559100430723764110173032070889241533802185414091706368*y^6 + 74360723581207125227891806308019626663888936186486806503305256801659973620419/9464392839079820782279550215361882055086516035444620766901092707045853184*y^5 - 88638211739262481190268519326330943776023557736494844503721848383861710771531/37857571356319283129118200861447528220346064141778483067604370828183412736*y^4 + 2308043377702626004201095907014010759011320272986715369341124172098257340935/4732196419539910391139775107680941027543258017722310383450546353522926592*y^3 - 723370989811049865721609174245594058645954601948386978064202941476711134461/9464392839079820782279550215361882055086516035444620766901092707045853184*y^2 + 221922312461795072389168371067076923212632821028418246081879419111307477449/18928785678159641564559100430723764110173032070889241533802185414091706368*y - 251580575181625556314686824586709851326163802671880617693923183757313554293/37857571356319283129118200861447528220346064141778483067604370828183412736

245871729134760038974966876708800819741518544324694734594256852489917839/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^27 + 4374738104505590739213779547750091783341416124947967351368205494478844847/388040106402272652073461558829837164258547157453229451442944800988879980544*y^26 - 148893002573505837553977789972947880686966860444433622716313269128631971231/970100266005681630183653897074592910646367893633073628607362002472199951360*y^25 - 547170414542965992084984278965741800237966112331617491132138454154036209/30315633312677550943239184283581028457698996676033550893980062577256248480*y^24 + 973930871945618043647361021478645560948664990642945436908620727047212120799/388040106402272652073461558829837164258547157453229451442944800988879980544*y^23 - 13632333132083198401184791103490197515255412314679949316151341050742574411723/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^22 + 9926703517251211694080507221462703655528675545184878946106757448729505918807/242525066501420407545913474268648227661591973408268407151840500618049987840*y^21 + 39379594549043341952171099567440671867431170298405389329562100087618658317651/485050133002840815091826948537296455323183946816536814303681001236099975680*y^20 - 4747997093089409596820173668757569452069589660660122459005956956466510949809/97010026600568163018365389707459291064636789363307362860736200247219995136*y^19 + 140661873668005711634255532552549331248022192113686755964110565883310555892893/388040106402272652073461558829837164258547157453229451442944800988879980544*y^18 + 30980867470748714185795479029459385690150628268758166404474549481610537157119/485050133002840815091826948537296455323183946816536814303681001236099975680*y^17 - 844494925410264080687774304620578349221811256816323830695596000476701945805641/242525066501420407545913474268648227661591973408268407151840500618049987840*y^16 - 3436742954122055863518968221171668281885786258123502214794428733931191824580621/970100266005681630183653897074592910646367893633073628607362002472199951360*y^15 + 12536252497305279137436362469047985405126973279872437636725482064761426384244281/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^14 + 3213934299987271808963700975117886698388193539782734960050080075959022068201203/388040106402272652073461558829837164258547157453229451442944800988879980544*y^13 - 11522196788776577561280609415627086325390003720317156289752130416254643259507427/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^12 - 7905218480204828615151606703538707200966906071304182053076182782820325426503367/970100266005681630183653897074592910646367893633073628607362002472199951360*y^11 + 772901604618745261658342108604102227839910919756509770381026878771369009436761/194020053201136326036730779414918582129273578726614725721472400494439990272*y^10 + 1270718393703061220869787630645835868543639340176671378986714958757404280882971/388040106402272652073461558829837164258547157453229451442944800988879980544*y^9 - 4544083614100804164790582727128297793957161309352245998259616422064395839185479/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^8 + 419711626384140908205013828048240011917092959590037108372768443591480782527407/485050133002840815091826948537296455323183946816536814303681001236099975680*y^7 + 47671860736365116638404318822618099836603022926829671341016737591845763121977/970100266005681630183653897074592910646367893633073628607362002472199951360*y^6 - 16676375811577994206321688779967698640141141060675699873108002063363337522559/30315633312677550943239184283581028457698996676033550893980062577256248480*y^5 + 480611161216711038456846472274449730238223106129956181350189543837215424261067/1940200532011363260367307794149185821292735787266147257214724004944399902720*y^4 - 30878436883655300730937065923857628106743716653332920171478092114835032104179/970100266005681630183653897074592910646367893633073628607362002472199951360*y^3 + 1379622408989720991082692515370928371217309404774661151796283200696824740709/194020053201136326036730779414918582129273578726614725721472400494439990272*y^2 + 96105011972363706901370776168372927660418810901463133143701390949362723/1515781665633877547161959214179051422884949833801677544699003128862812424*y + 247996331260152227353308188866139639687900053307303456043964526739436465427/1940200532011363260367307794149185821292735787266147257214724004944399902720

-225749145355309559099335519425301341274939767577990542440854492021622447/18928785678159641564559100430723764110173032070889241533802185414091706368*y^27 + 2743426124249630317065696415782085101572890316137014523770867736767004375/18928785678159641564559100430723764110173032070889241533802185414091706368*y^26 + 115681322017764894512622231299480220443151831751923470050489313556033625/9464392839079820782279550215361882055086516035444620766901092707045853184*y^25 - 354254156662420818651979627398540383366681908229331629898370351991597513/147881138110622199723117972115029407110726813053822199482829573547591456*y^24 + 139943614218265698785582882075230708397203388773322904893027737766005438149/18928785678159641564559100430723764110173032070889241533802185414091706368*y^23 - 739566210618048990807273768687002271702905238986829259049896821725548391691/18928785678159641564559100430723764110173032070889241533802185414091706368*y^22 - 80911939886072663926502203779831895011898756798628025692989739272800606613/1183049104884977597784943776920235256885814504430577595862636588380731648*y^21 + 274840521506055216326784908389114207256031698484768389923583286376223743955/4732196419539910391139775107680941027543258017722310383450546353522926592*y^20 - 1713395862107546867385768266047568728402447091075327707586934621697718567315/4732196419539910391139775107680941027543258017722310383450546353522926592*y^19 - 560299247316837596327963685717901001566234196833709235900475385272336254057/18928785678159641564559100430723764110173032070889241533802185414091706368*y^18 + 30122854266240908162925022128837490757949170554273721995730655876122060628549/9464392839079820782279550215361882055086516035444620766901092707045853184*y^17 + 25678013327490740478149806324854178899402358584728636964827849125312151983271/9464392839079820782279550215361882055086516035444620766901092707045853184*y^16 - 14404708036263849921489261223497785253374592356373918212722029365934293462243/2366098209769955195569887553840470513771629008861155191725273176761463296*y^15 - 109686948321671421426671540094661119801433588348836543097614705273353406742207/18928785678159641564559100430723764110173032070889241533802185414091706368*y^14 + 120844870926016130119717894490716357843642789631435512966720140733648363665809/18928785678159641564559100430723764110173032070889241533802185414091706368*y^13 + 90381811489029561461603964474093398673217472982171079966332518676720600318261/18928785678159641564559100430723764110173032070889241533802185414091706368*y^12 - 49052436316637895761258649615923608418294199632427149319460942593760107568169/9464392839079820782279550215361882055086516035444620766901092707045853184*y^11 - 6071651874305398164955980918757252084798145367587491633197168028792677148319/9464392839079820782279550215361882055086516035444620766901092707045853184*y^10 + 59505983764935062922356655583152793323782401194860443682481826268949829278481/18928785678159641564559100430723764110173032070889241533802185414091706368*y^9 - 38715398870713226386556562018656475909457232203836438606025822921490295705871/18928785678159641564559100430723764110173032070889241533802185414091706368*y^8 - 26688133277484498464143842735132513924732688751419045179974962191081652791/4732196419539910391139775107680941027543258017722310383450546353522926592*y^7 + 5771363801716169339964240267795717616940896445441589005552059113597284705307/9464392839079820782279550215361882055086516035444620766901092707045853184*y^6 - 1744546874233062721786543019196476203459890312989898204353301799591823115751/4732196419539910391139775107680941027543258017722310383450546353522926592*y^5 + 2546048762720644883129968062483777461629046492231244011030321368772795380105/18928785678159641564559100430723764110173032070889241533802185414091706368*y^4 + 34249566363621363309116132572464562580436218352885265056928248882432678821/4732196419539910391139775107680941027543258017722310383450546353522926592*y^3 - 7587711584588127656295960895549100547192794761157384423211526254699190171/591524552442488798892471888460117628442907252215288797931318294190365824*y^2 - 3383525985141875409956672726794189673921233453764467684933512863455620629/9464392839079820782279550215361882055086516035444620766901092707045853184*y - 8511126172713914751203810158732025031952960687258685670805150054669664037/18928785678159641564559100430723764110173032070889241533802185414091706368

-5571398581324057769254846591753447610576111201902329285000396229770728203/970100266005681630183653897074592910646367893633073628607362002472199951360*y^27 + 2975161869272801264155649267518064259013371409311409600369477504466599379/48505013300284081509182694853729645532318394681653681430368100123609997568*y^26 + 25460456813794584155794984705905918529028688593649959281576283272423645941/242525066501420407545913474268648227661591973408268407151840500618049987840*y^25 - 66766420635179357775456530225825906080189668809545278803937704810755643733/60631266625355101886478368567162056915397993352067101787960125154512496960*y^24 + 364010990458135334820505727501267311344070304886792269214189990549798685493/194020053201136326036730779414918582129273578726614725721472400494439990272*y^23 - 6940907492237867083447780833749078388632095308410997963734643891899174797717/485050133002840815091826948537296455323183946816536814303681001236099975680*y^22 - 14196360308946569475741959489781043092444622432399331882960542019385040839823/242525066501420407545913474268648227661591973408268407151840500618049987840*y^21 - 3879112047818617403210037471677297039375050020807977680777492532071826394091/121262533250710203772956737134324113830795986704134203575920250309024993920*y^20 - 7624873238835883910718086077432231621052629233721415818384517196999802978791/48505013300284081509182694853729645532318394681653681430368100123609997568*y^19 - 50053497702262407969690982559164398538403194276181456843502063209957911248693/194020053201136326036730779414918582129273578726614725721472400494439990272*y^18 + 1361763588339801161167029416290193016341545507315996526002335713964732176813853/970100266005681630183653897074592910646367893633073628607362002472199951360*y^17 + 3417492754020125520820755417025577996320930910100011350517679814299854232332001/970100266005681630183653897074592910646367893633073628607362002472199951360*y^16 - 33185937112437024302780865491739471484450083962007968068754453525754945229481/970100266005681630183653897074592910646367893633073628607362002472199951360*y^15 - 2934530644989484257104078867624751953405002317110874173416143697144570398433171/485050133002840815091826948537296455323183946816536814303681001236099975680*y^14 - 531110519879492322858263010682860979182493215239980119138503304864593248743191/194020053201136326036730779414918582129273578726614725721472400494439990272*y^13 + 2266321660408056657057603909802391921219900914309528291219620132292056455735597/485050133002840815091826948537296455323183946816536814303681001236099975680*y^12 + 1319052601880724982440278973662063938684883613278682737465916332004862836733539/485050133002840815091826948537296455323183946816536814303681001236099975680*y^11 - 45938892195627722308802001754167920312385674215615309947283946573775468749359/24252506650142040754591347426864822766159197340826840715184050061804998784*y^10 - 104797725860284862489791611975754997499098030533485901198738553085461235627827/194020053201136326036730779414918582129273578726614725721472400494439990272*y^9 + 135343657015361934845002492949788064423740145838194204984860588790205097659089/485050133002840815091826948537296455323183946816536814303681001236099975680*y^8 - 98667491551249160015978454670481081573284871509840269346013304504978609650319/242525066501420407545913474268648227661591973408268407151840500618049987840*y^7 + 79645763615351695073787125616250687876799458206059007068603963599564580782721/485050133002840815091826948537296455323183946816536814303681001236099975680*y^6 + 61756145453224774128089314040370543558554504881656863314804468830096352683051/485050133002840815091826948537296455323183946816536814303681001236099975680*y^5 - 47738129810104774743730435887598437179807932844308171865840830619904819433289/970100266005681630183653897074592910646367893633073628607362002472199951360*y^4 + 13429836774758664668214150909310679719766714533306355321718659065377733465411/970100266005681630183653897074592910646367893633073628607362002472199951360*y^3 - 1434612313192235989860305136307607684616524773412987006756880402633418587939/194020053201136326036730779414918582129273578726614725721472400494439990272*y^2 + 12186593668115251845052824172444976221710950241603565646525217721907090573/194020053201136326036730779414918582129273578726614725721472400494439990272*y - 47785744413313705735138899732847645552169912782456108942264671907298510157/485050133002840815091826948537296455323183946816536814303681001236099975680


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

# B Gluing Matrix
{{2,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,1,0,0,1,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}}

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

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

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

# 1 Loop Invariant
49898792297043123416289347188551886941684436073560517930573488022703048503/75715142712638566258236401722895056440692128283556966135208741656366825472*y^27 - 611217402204594347694050248698591542368150815407507344719321222588436790547/75715142712638566258236401722895056440692128283556966135208741656366825472*y^26 + 2378608380325063483216174459450472267524497403283495220582239632197112107/37857571356319283129118200861447528220346064141778483067604370828183412736*y^25 + 157133178467609464467756305900254149344158029899977621760950089351483131083/1183049104884977597784943776920235256885814504430577595862636588380731648*y^24 - 31849816709205724510901458289984329098045754380514996886157372452679107335645/75715142712638566258236401722895056440692128283556966135208741656366825472*y^23 + 165901436261696296712907108699997783405111185514356960856271126331354673100911/75715142712638566258236401722895056440692128283556966135208741656366825472*y^22 + 4237762746554754962765711472151086376785987744420595592951545669278806979453/1183049104884977597784943776920235256885814504430577595862636588380731648*y^21 - 69165524245279844548394581896837087963469236303247289531111543104442938350679/18928785678159641564559100430723764110173032070889241533802185414091706368*y^20 + 377481441945771184502836554707642015773306269282828628954318417476928810987979/18928785678159641564559100430723764110173032070889241533802185414091706368*y^19 - 25754209093263794773451519562375618243819989877052587716478973812300734621103/75715142712638566258236401722895056440692128283556966135208741656366825472*y^18 - 6684052214065981144503943485709990165360062995161184464069908503249162130174571/37857571356319283129118200861447528220346064141778483067604370828183412736*y^17 - 5084869980956226002300097273517482134743464879171123695867489991556855463488413/37857571356319283129118200861447528220346064141778483067604370828183412736*y^16 + 6834766659203347475907839064340434499781765473575881498770006746828911915442747/18928785678159641564559100430723764110173032070889241533802185414091706368*y^15 + 23514914195807668103028109200305540732256290493905216300240793904240134840591331/75715142712638566258236401722895056440692128283556966135208741656366825472*y^14 - 30071649525674483017011767868044969020297399399506946580557978469738367211995625/75715142712638566258236401722895056440692128283556966135208741656366825472*y^13 - 22077804030860814889107927958664843132273482414294651533341130321947332213424673/75715142712638566258236401722895056440692128283556966135208741656366825472*y^12 + 11448655600875774510861343885415995838060883996299450264194570847314171455848993/37857571356319283129118200861447528220346064141778483067604370828183412736*y^11 + 2954374228966107878234297289447888597577198733140718686780013827596999281597499/37857571356319283129118200861447528220346064141778483067604370828183412736*y^10 - 11464255661270954123916525362380463245960167421869370592799910857515685697368185/75715142712638566258236401722895056440692128283556966135208741656366825472*y^9 + 6652027594956149009544803703545650084890464667090244815858518737307277813425875/75715142712638566258236401722895056440692128283556966135208741656366825472*y^8 - 445202983706566396587845644321167569521791626769386613137903976180363872913105/18928785678159641564559100430723764110173032070889241533802185414091706368*y^7 - 840556039971011120252265285546658825611348721459831703564092222530831086384075/37857571356319283129118200861447528220346064141778483067604370828183412736*y^6 + 393912477683691776480979387966758064597260644469199971074282335652083255534565/18928785678159641564559100430723764110173032070889241533802185414091706368*y^5 - 555797545143647805893838443301937522725581978781704915239335387437767982524425/75715142712638566258236401722895056440692128283556966135208741656366825472*y^4 + 5837674370853280193918369991887477792866067878221016233743376529307619436995/2366098209769955195569887553840470513771629008861155191725273176761463296*y^3 - 13510869082965205308030830925596429878655814537470545120324363755465057236493/18928785678159641564559100430723764110173032070889241533802185414091706368*y^2 + 3463305577138680654781186126385315110889195185438288322177539832198447389711/37857571356319283129118200861447528220346064141778483067604370828183412736*y - 1316744960162947365375054364128162543253199765924243939110633014722614854703/75715142712638566258236401722895056440692128283556966135208741656366825472

# 2 Loop Invariant
-3031947048226606594580365180492607032990801165158495041918267026839688567319240767669956927540589639690731617810354666336851911592630110050145547494275210844985615501/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^27 + 37627110176300224490104541334346889733416524881209908256649665259649795834708567981709411060445085816856008267388812548066611140378634161569475862218799192111851754603/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^26 - 965108863728556974043361468350161763710005128901460738765992787161944273235652691983371494988064294427751983481372733471956497681022270739259354870151942616089784015/32388958781469588278886160937689061600884401129146171044132642148006047120761336665339152742768189157502236688845747671262191628917445455529415765412269160538290855936*y^25 - 154173531511020130411280774624287476969444105606812162221210844211959208531395240899609365550812403453844511438263626334505844680680800985320227204883144196441311085239/48583438172204382418329241406533592401326601693719256566198963222009070681142004998008729114152283736253355033268621506893287443376168183294123648118403740807436283904*y^24 + 2031447204318780017132728260334289590280815852574497634282844518615953903931350422319906948592624873783538466625163762148816241660206244494164499672121561648841864185339/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^23 - 3432332930815379144689965816971999698353235580523741596756944637746505276452239160282352768730293210320092496104552124689027579852969097091781553203128389319183935345813/64777917562939176557772321875378123201768802258292342088265284296012094241522673330678305485536378315004473377691495342524383257834890911058831530824538321076581711872*y^22 - 1890491504903874850183074679388368562328169417319631351106239121225852035403942558427585159786819370366634979274900628678177085625750465755619465388373607587801703466621/24291719086102191209164620703266796200663300846859628283099481611004535340571002499004364557076141868126677516634310753446643721688084091647061824059201870403718141952*y^21 + 1746989650219419635546300379678643345357005885512040102180723101487287149779995111079040909485911297696834795605999542873273647619670632605016800761584055715369023198329/16194479390734794139443080468844530800442200564573085522066321074003023560380668332669576371384094578751118344422873835631095814458722727764707882706134580269145427968*y^20 - 22814150460857099525036523611807586734002352436789567128163126361195570661577942910170413386551314633384984139112599254808658321694668135164376875022942896752573749358389/48583438172204382418329241406533592401326601693719256566198963222009070681142004998008729114152283736253355033268621506893287443376168183294123648118403740807436283904*y^19 + 5056253541117978837123987131227494125202069849867667827918752271522533444038818202160329013354604722935529948164047815064605652923031926163233447329266744893089661733711/64777917562939176557772321875378123201768802258292342088265284296012094241522673330678305485536378315004473377691495342524383257834890911058831530824538321076581711872*y^18 + 17219224630315412370642061048478863367495871392976191443001389103575871718105618473965183588700628585326410250594858334406186205193537120152982373054247687561624387639013/4048619847683698534860770117211132700110550141143271380516580268500755890095167083167394092846023644687779586105718458907773953614680681941176970676533645067286356992*y^17 + 61590648757620071076366010941281764647604620457763744703988263703727427467250426063971629775760223416339948715292345163974666941054257007736096450842312269253527788142043/24291719086102191209164620703266796200663300846859628283099481611004535340571002499004364557076141868126677516634310753446643721688084091647061824059201870403718141952*y^16 - 942724994375842639197961834493765466337809760736230575382908210055242072829407791866298227135624799677250949061606469069244501624110151886307491019465051015452870800408151/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^15 - 436444975625608471197166610307959057562744017078063259111757027646233907974334299833844451839770154270443942682985999312206371707576584646468096617597071272585334775020497/64777917562939176557772321875378123201768802258292342088265284296012094241522673330678305485536378315004473377691495342524383257834890911058831530824538321076581711872*y^14 + 747968791164264503980577042730231072548572537994341583215250911961697244573060648096117586336415298477725496711036278599344967158863770662099700438232787182957272360299081/64777917562939176557772321875378123201768802258292342088265284296012094241522673330678305485536378315004473377691495342524383257834890911058831530824538321076581711872*y^13 + 1327596070546092194217085899170432138436560484092603882211381869294213995778562662976571927654520068748971254218276762205960864753630251649962197377536779695099220918639453/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^12 - 879689875974122883301318983968691075083056265365323457052165582046262144219441339489034872819170153075873644655783532219590947732005100048065964246922961808206293510570629/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^11 - 181265145721085089166928850524399075646985293506842928721933418467247257702623602635738138135071592416692165963221618590674960719493709681065538480096502631830514652892721/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^10 + 869207782351206196934108344873570591940714584873631001196732078051879020992106945550157725367799175658425460682387203703415126276119954756695782430907586802174103284584799/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^9 - 456274324917736398414591084779239137284977555198296915760303421547646978426043797188602972912979593891686301743437620451092300727745446178714154620559429269131663315320659/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616*y^8 + 23150808857262348738817939875003565144973767557418031869524480528272057878506853620519081891203251018949651860275222274305979210839176648987327853041669748085566945650449/48583438172204382418329241406533592401326601693719256566198963222009070681142004998008729114152283736253355033268621506893287443376168183294123648118403740807436283904*y^7 + 67182776138731382147256851055145662359103533346880769884572881876824530706375050262485726513463366732258293415884452460974784624678306963811414314737877633779763834615457/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^6 - 3581221667069084807568349198224721983632967952618904788546416091318046254371912683099669958026642001360422645994108220753735942009358396699531269655672437711334880131021/6072929771525547802291155175816699050165825211714907070774870402751133835142750624751091139269035467031669379158577688361660930422021022911765456014800467600929535488*y^5 + 11206985465264813206212043794230300391646804244572428896309677456861434897140539723082465850448451149945605600352350936270585024774232923664074843518921613290266056864765/64777917562939176557772321875378123201768802258292342088265284296012094241522673330678305485536378315004473377691495342524383257834890911058831530824538321076581711872*y^4 - 3394912213761922624795723156453159705586840324280296719942703365494133846832925695312732613739783209939365770753001005078908900761272714798206809281317405855126017191481/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^3 + 582046039505234650931173625026182829514974353239926511427755307675705550901685671335079145052225183369389114544639850607852109353986013092280690602576021892816319279693/97166876344408764836658482813067184802653203387438513132397926444018141362284009996017458228304567472506710066537243013786574886752336366588247296236807481614872567808*y^2 - 41326787533205718070212254851129240913598524788091262931494986476482592007674782094796037072222330555523853544119129411684006057149815988255935593287585550536753711367/48583438172204382418329241406533592401326601693719256566198963222009070681142004998008729114152283736253355033268621506893287443376168183294123648118403740807436283904*y + 42361474607831234398284736447176807539513350538043755853067940278343233246222868301030112104049297975847822223327976454077589340834735553938038355368275637329781088023/194333752688817529673316965626134369605306406774877026264795852888036282724568019992034916456609134945013420133074486027573149773504672733176494592473614963229745135616

# 3 Loop Invariant
-193360104413841106557742985046194930048353289651957514037634145731976202136320705389448098772447169121643522480721387408448972574092456254303001419395873628302467204301237281898926137074577189849491113940324452865/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^27 + 2355531075058312662536980559331842868736844357338640870575782791621554890262947176714319069987815271326917538196528309370238536180053521764746326627537306964132266697292444556290645295188134935873592971142183812557/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^26 + 78576849804038304128773634674866755308325213391816333156305337881508877613888176310877636945110228630999277036110284346250166235000897326157998408746587228657369892822566856651219217995308611674065425783681916289/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^25 - 9789846845287682780776711153610787239031532269044228451212973576798213703153997897718767782947667395461687327309726319770154568965170691009193022885380862941082223621896352285260135498742169122206318726762124670473/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^24 + 120614780527708656980139074474712324890893827537895063114777712099501603630370905540184326327664153928864275284280092405326259338491828845753288629225406408506112110109617961114625818981654212033087215386462654320927/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^23 - 631379174746018033453198533176558543556220877495886846465962158296913732224707941666048649648316923701774764068975870855803892353145291523694874076363109881365915419197221973977205672698737710959144947733626874843557/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^22 - 68843483032947937465590204093771237761022049973067144052213612500268167012769821608597032412483772023857920262046208015993641194133830554069419590961643032374284536308785504680904600247863752392260976602138714238515/473684430068748260958319784020328472228555751559928187618850991724953351898199278475833674833647267963383779785668943652148821869481557775608580287100583528411242146076022042123553819894393900482225867044160991232*y^21 + 262346025911711686293255518766325906676575936293573378288449848477921077896305843699770852211479114473407744063352610087444549361891204325967907449933078547818065218625608725133271016369026896484678892745893412420905/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^20 - 1409642346760245548103952033739220353952994988152030055882161656325612186228974336328193116406535538602854541914821400326241706495260208128264627941862834557075141927529461814413781048506768448600170173587361724570697/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^19 - 251672029329446144333335018356164938182761221941459944983173807348272492981433637570257728933421399050269233495303818976894366687622081672554389753675946238972596975101602752529506290506756875416807958923521454594919/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^18 + 26165061081030247560823906746851979535150121585678522007838825634433384476170413112139853125048429094625181418904042142525853886423219182820323603529964406932871642594399973498950335592840518341437382314667539381064793/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^17 + 21690352494958953198712937151498901556090336701048907850785615521971297202614934816263062221795173127913748724387946484149556541309393026098077032746258557523546757676458660680614025849257718554327486072617876202022249/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^16 - 26847491544357756076774711715593616253251639362234243912781349970593331633825283531295282113617641871928994022394273863747402974156903034901776410916497576100229447965899258740842412908515291346638734370353805842800731/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^15 - 105900251950076840033700060082988980392910061959811413316200129190451977381072021967632897435936069711392374692330911130633507715281722117019483434253862611713981596334297585356764228176286542918043771047853384748706249/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^14 + 112536562499870957460891957020585733496983790517558554680061388356212124133031012404963981584435597461399099431977846337339944943958310235355086164269321649011043178575545797695151184006970367168011073395523221777171207/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^13 + 105040692298756261693068017765715625126011524758052147022933248683108634949213187016519553742273251206055632919496117612301880622964877468262833992121229707105218094969997668590062606309350759022264406372195914943740359/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^12 - 40506490226157761190123616919502802636634824281480096591750396941336196797903896261256851168830788514636041820105968628682250505451653451224292705826045189794763198710455879222177212554459186191096689228924222174700205/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^11 - 18144326981459970348118843642515851998148903229242405188220784754907651283442134971502010050979039018359051030878464165207819231211919672640164145555462564690970788148658633758359241550448877844170081181713715075236055/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^10 + 41697802406156316656926984325118506728202914127982954729213145972583236154868897875961103785428695799181362228208654749502927160419813805803650431759089566826903735669850960231744478555725027886886684063771575052536939/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^9 - 21201968909216142614675329218374799476453182077333814553846866561122534920487887693307743677167840938407737548403419607945247518213913231493797846527126138073450007459861601561737883781559313347363361361257632711221721/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^8 + 956671433551418158545764524744423601627775838881946475520750477625735558734645738992586230313156647739962761498782489368727353098995046591803100151094202868023592039096295277155628233620418276846659405825179990468217/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^7 + 3984526462958681903180905735201906846572640855174048185666282375529286655331233041971034684879667910384420732938294920422123184619763263893619275747842205197630447047444522720101826192381305389490883749213604519556969/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y^6 - 1310201188881702356681940219706658824648725740660211580876961055531810698331099785328781920032998884616289288509914306914162846262248898397109482112592559999274234330381696925388408354742364385247531991496885461080801/1894737720274993043833279136081313888914223006239712750475403966899813407592797113903334699334589071853535119142675774608595287477926231102434321148402334113644968584304088168494215279577575601928903468176643964928*y^5 + 1440716416924944236102528290984732077059927682736300201180107265052209390037281389795091479015449225716636901117730315405530110423598584896781645487763686660280897566538444383358715145590170535485507445702108751453967/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712*y^4 - 27724310090704360417807491550376982347855779175394826416053393898830130510134846048842807430227506257990042289412168932064320848215264897339110583059193639339905494409085594754436626754195418737350155938559241148975/473684430068748260958319784020328472228555751559928187618850991724953351898199278475833674833647267963383779785668943652148821869481557775608580287100583528411242146076022042123553819894393900482225867044160991232*y^3 + 4644256026983841121873100996573002255903874398029999106278981406367696187752470869187672252989276535485471529767017240643537611829384754428997780130352787256968652052956196726582603900596953817826255657096958378851/473684430068748260958319784020328472228555751559928187618850991724953351898199278475833674833647267963383779785668943652148821869481557775608580287100583528411242146076022042123553819894393900482225867044160991232*y^2 - 8125808844120666414428088769866927351842110266739016167139229178130602882229247620287959229737641105105319936578767609023155431427602443778421111875810631839325214607885343697097049806844750791775393572058493135053/3789475440549986087666558272162627777828446012479425500950807933799626815185594227806669398669178143707070238285351549217190574955852462204868642296804668227289937168608176336988430559155151203857806936353287929856*y + 4078168379572240304692128333432560205086628273750328763682760662258761882096166550399798079552992520678647573814239879478289481206574882270432642534932240742889873480951821568751725452633394376202940528051148509285/7578950881099972175333116544325255555656892024958851001901615867599253630371188455613338797338356287414140476570703098434381149911704924409737284593609336454579874337216352673976861118310302407715613872706575859712

# 4 Loop Invariant
-93702967873599505543680054645833553547424712381902402533357793139387117448471611252375467271229706791546961591284935575912360455227154026411859559960098318184081837267599745704494929078363336313716953454967541124290593635815620055808198654720222722996944067172715941541823725381745425368223943073728083214909/1244957593126766886299359086378746900667555528095453614711165441660150653661402437408265933120995416467420965158394661426327701888070883792300970282122234993243847183710336454742740273854881857705978655307806234030507531198261821414581279966426339386869486205360551301125029271977028104148162709742593196949504*y^27 + 17001483920903014336417373872449249168634928749870193447916684484025407602228504447319497070186140842701704943083604560388945758821027822466817740471164957285371042222043274765806082327255296859864430236329207165270424516684114570960421192189528615585227218596117101293091002214635511192121619969733691268103691/18674363896901503294490386295681203510013332921431804220667481624902259804921036561123988996814931247011314477375919921394915528321063256884514554231833524898657707755655046821141104107823227865589679829617093510457612967973927321218719199496395090803042293080408269516875439079655421562222440646138897954242560*y^26 + 1297639647722651816815518542227994333181978304837861892139786580454929315691451772866643215026888900790159346415987928227841349299940485370488225063384445716849137309011469476538588929083983083665913783025092878490766098467173599544276430909526854699184762017740624569003838180102929299432869255138656566563977/9337181948450751647245193147840601755006666460715902110333740812451129902460518280561994498407465623505657238687959960697457764160531628442257277115916762449328853877827523410570552053911613932794839914808546755228806483986963660609359599748197545401521146540204134758437719539827710781111220323069448977121280*y^25 - 11845697889708322890681275013717069322501637067263118363552144807444950737885227656972671088854482022904782362318275815819534021611013504787159730374898468627207070186176140147803867168951994788514534637240828615102140617038857226237885279119022210354025227995785003482369253415742282898671191995502617914676021/778098495704229303937099428986716812917222205059658509194478401037594158538376523380166208200622135292138103223996663391454813680044302370188106426326396870777404489818960284214212671159301161066236659567378896269067206998913638384113299979016462116793428878350344563203143294985642565092601693589120748093440*y^24 + 852267202729938127867139235054461564682227499997740916146931455317980632515573239155793094579793067391715982031923871067450457603227532465225262143961830639989936650163938598611435193252964259789611706792624443040165799025039969137890041395618929694692136307101870739570151935996845760666628366866873430309067209/18674363896901503294490386295681203510013332921431804220667481624902259804921036561123988996814931247011314477375919921394915528321063256884514554231833524898657707755655046821141104107823227865589679829617093510457612967973927321218719199496395090803042293080408269516875439079655421562222440646138897954242560*y^23 - 502039703551717070130182014046921398668370940927266096864335667505885754794124904469106776002338563232287497350436790830882031872476130707611402516327931310940139542818730959393563977646814090857157541324297394491527899061343442003029720305747070299243392267566139388407509672020973859994808472045119811967043151/2074929321877944810498931810631244834445925880159089357851942402766917756102337395680443221868325694112368275263991102377212836480118139653834950470203724988739745306183894091237900456424803096176631092179677056717512551997103035690968799944043898978115810342267585501875048786628380173580271182904321994915840*y^22 - 524297157805224910108793012294225239539117079614290562901976118014640403146552030199947439100886838853897432859117095889052433100149856337359185077857418872719884495158655560357806766761388488131177398767486942951108931991445115002458709385011272207788788921164199364428024637483156435369537871083372617744624671/1167147743556343955905649143480075219375833307589487763791717601556391237807564785070249312300933202938207154835994995087182220520066453555282159639489595306166106734728440426321319006738951741599354989351068344403600810498370457576169949968524693175190143317525516844804714942478463847638902540383681122140160*y^21 + 1717662793999549054560759885102409129852085932997593761341187977785921425700963504004028346287586933788159457716619144000351109295395770455178180551173517313216004803778337718270478511389916221977576547619402053461491336562802548265402097097968417830149993086803468014962284273043642130548280135691567670110983271/4668590974225375823622596573920300877503333230357951055166870406225564951230259140280997249203732811752828619343979980348728882080265814221128638557958381224664426938913761705285276026955806966397419957404273377614403241993481830304679799874098772700760573270102067379218859769913855390555610161534724488560640*y^20 - 3370863030455770583156690549996148739910008076750656040265130238642547193863361309931004571820252308171911812563487039728707429779852166957593756828723698218492277029095720107071815194199944591099318173408050939593987024250182706228014934306125730588431639777965549489793249626528429711128425821403382113448259541/1556196991408458607874198857973433625834444410119317018388956802075188317076753046760332416401244270584276206447993326782909627360088604740376212852652793741554808979637920568428425342318602322132473319134757792538134413997827276768226599958032924233586857756700689126406286589971285130185203387178241496186880*y^19 - 5229641644921304876091523477094189475952664166866762304574044537021516434540942156817310028526250049114491384951168013874766721538391803249387048456627536924648107341181128217941550562901003962383996327330407992854732178745274842297642806678053173817777446956883584435959227130541755675958157076696885392438013829/18674363896901503294490386295681203510013332921431804220667481624902259804921036561123988996814931247011314477375919921394915528321063256884514554231833524898657707755655046821141104107823227865589679829617093510457612967973927321218719199496395090803042293080408269516875439079655421562222440646138897954242560*y^18 + 37965342527958041452778561745108954186606839524566884560193372511346410566096172652080362685540326196010406283677328236184201130906472926830059741770538561550078534707066241791645892277830295906018636622551099425012466099872451881313399258475839670304829187142255768998220017789459347844902719250384084997325840325/1867436389690150329449038629568120351001333292143180422066748162490225980492103656112398899681493124701131447737591992139491552832106325688451455423183352489865770775565504682114110410782322786558967982961709351045761296797392732121871919949639509080304229308040826951687543907965542156222244064613889795424256*y^17 + 174040049715687539937812479338602384974101171832356330843394715258422872476666580749058548754565548077449250317978175497583610104314665448027691404013158059132048494692135637635138442598659773038393683827403355704046014677865858614814684646707270081749598784854091941630346682315619869193716514483882789426042299199/9337181948450751647245193147840601755006666460715902110333740812451129902460518280561994498407465623505657238687959960697457764160531628442257277115916762449328853877827523410570552053911613932794839914808546755228806483986963660609359599748197545401521146540204134758437719539827710781111220323069448977121280*y^16 - 93458293122997081517917231129417936707237491223111855999065732004871004111197372079045458122558327513914628508390885928749806200053567858678896683114277208584230223827682392446124845385768662021567679330855520874394011365877042226420034142117854332127658917626813960019841537934590988591791603781841563722254864997/2334295487112687911811298286960150438751666615178975527583435203112782475615129570140498624601866405876414309671989990174364441040132907110564319278979190612332213469456880852642638013477903483198709978702136688807201620996740915152339899937049386350380286635051033689609429884956927695277805080767362244280320*y^15 - 55484449195448132591752770254240827542532521772572176414986866981180824852411676894352275195082136523600080699097252468864515384465046508599949275397981335289462706971463517009304148149363480481580661603784666313210682000167712324020784354567082472265398354402222527816483158462641535161491490575744017056328649429/1244957593126766886299359086378746900667555528095453614711165441660150653661402437408265933120995416467420965158394661426327701888070883792300970282122234993243847183710336454742740273854881857705978655307806234030507531198261821414581279966426339386869486205360551301125029271977028104148162709742593196949504*y^14 + 738989212458172869333161874445439811153489942412861925218329922582036130267042532913025179327360396794021287078699523022213269716242860176946905361533878751554551524924520138826733738642437673574549702208687133845622061856685307288154052659587297214855025367915210112252442913028865474122334278497521762655915841693/18674363896901503294490386295681203510013332921431804220667481624902259804921036561123988996814931247011314477375919921394915528321063256884514554231833524898657707755655046821141104107823227865589679829617093510457612967973927321218719199496395090803042293080408269516875439079655421562222440646138897954242560*y^13 + 820683755330118496505588179061010309141734341921887583044495844658519019402381548785919671077259487447884379363713733460814727556351459023784218380545244636930401750881353381835327140369461977789025965927638168553307598783433024483931658962198657421416744161469632576321941990600929383300262057808052442778369922177/18674363896901503294490386295681203510013332921431804220667481624902259804921036561123988996814931247011314477375919921394915528321063256884514554231833524898657707755655046821141104107823227865589679829617093510457612967973927321218719199496395090803042293080408269516875439079655421562222440646138897954242560*y^12 - 85042447199819110822228104990518599926509174905373886646291485227145933778521086672892133640474596825542607787930791251444232554230182694559079205440404351376366975416990154101100429240782646613505018159688195680155798998730586068071958503402131727312231705908120305699094561179700977982135212524501520604297749987/3112393982816917215748397715946867251668888820238634036777913604150376634153506093520664832802488541168552412895986653565819254720177209480752425705305587483109617959275841136856850684637204644264946638269515585076268827995654553536453199916065848467173715513401378252812573179942570260370406774356482992373760*y^11 - 150036112032926684714072307678239818967798183925611702745369299901047059760226168027133995638242252292278365041310891289020355956869243718664226751690342016314217215440153737727172091118993937672905787816479670508495533405787459149052501508096618877223655556688880528192076300047101523469820012888730132192220194831/9337181948450751647245193147840601755006666460715902110333740812451129902460518280561994498407465623505657238687959960697457764160531628442257277115916762449328853877827523410570552053911613932794839914808546755228806483986963660609359599748197545401521146540204134758437719539827710781111220323069448977121280*y^10 + 18148032535383260830245772215416901926169722820126365061319599756308063608067531912382918619396847399318433363846977537390295661470452622763003523117925915462041748022462096893529247045658845830554903565520533076322486422796594159263348040957639399861610642648537853410996278544902347499374177308302170182624725467/1244957593126766886299359086378746900667555528095453614711165441660150653661402437408265933120995416467420965158394661426327701888070883792300970282122234993243847183710336454742740273854881857705978655307806234030507531198261821414581279966426339386869486205360551301125029271977028104148162709742593196949504*y^9 - 14890692572748813815124835693712932753630399157772010104688899352117894193601513186270544091114544184048114272333736607699720540446482051924388958387319513456753228975394322007300325053660604205227387993611186180386465504995714387004693218842706121814694664892520876090356557512892545689538731092419141078552587251/2074929321877944810498931810631244834445925880159089357851942402766917756102337395680443221868325694112368275263991102377212836480118139653834950470203724988739745306183894091237900456424803096176631092179677056717512551997103035690968799944043898978115810342267585501875048786628380173580271182904321994915840*y^8 + 4592650336166185412069360088287689106596422708100574507420334942191533929492987339154440442086836807664356700555848462312926770348444168107615278168692418045754297571220086404618925271485160335422027755325718140807732628943173354941717211032720847360072945591297050336803099970642311488065764700188481173555700209/4668590974225375823622596573920300877503333230357951055166870406225564951230259140280997249203732811752828619343979980348728882080265814221128638557958381224664426938913761705285276026955806966397419957404273377614403241993481830304679799874098772700760573270102067379218859769913855390555610161534724488560640*y^7 + 29273349381504638076705183949956340648906336268391004137729185794440039171483593752534604971342128571361719217591670560531868084138528033708928545981399129415194151863884555981158852568848009101760526939993726158825720954740922146999958096185310547607989106530134658018569888653241697784863347988835464448703658711/9337181948450751647245193147840601755006666460715902110333740812451129902460518280561994498407465623505657238687959960697457764160531628442257277115916762449328853877827523410570552053911613932794839914808546755228806483986963660609359599748197545401521146540204134758437719539827710781111220323069448977121280*y^6 - 8176794962743063055810161277496589741249581685458416084980461694659424043233025262248345459056204313143872934998652416976446643180663135393302380849844545509189792896331858191905408074007379250982223119988429939816235582897303141076234342779398905834213408762808260823760647913790285108228171812828331872195166527/4668590974225375823622596573920300877503333230357951055166870406225564951230259140280997249203732811752828619343979980348728882080265814221128638557958381224664426938913761705285276026955806966397419957404273377614403241993481830304679799874098772700760573270102067379218859769913855390555610161534724488560640*y^5 + 2731951993463780146692167470756060074011585240301013842523879187093978045127603965379595010585224948484704266405244004400639175556614965699493241011784833614388214655859652252327308292116369209012270796576656543841501471741530775188400930377799602426244317436017230193485675569387714696415091508527930189487149047/6224787965633834431496795431893734503337777640477268073555827208300753268307012187041329665604977082337104825791973307131638509440354418961504851410611174966219235918551682273713701369274409288529893276539031170152537655991309107072906399832131696934347431026802756505625146359885140520740813548712965984747520*y^4 - 699836587533635766429885002310105213136805110616384589955766585097611259296286882481873527940671883717065135470750874601316258922076835204588804033254700969262492481663914574944661695985172858908180645991147195324466252487934052494191019846736224623436823693782180283388621047532072508410672411451774154051854471/4668590974225375823622596573920300877503333230357951055166870406225564951230259140280997249203732811752828619343979980348728882080265814221128638557958381224664426938913761705285276026955806966397419957404273377614403241993481830304679799874098772700760573270102067379218859769913855390555610161534724488560640*y^3 + 43699008323622787051199211556491448910925636893177999650234327033028906730990690745876966676087427659948099392308804751192096232748582410104065008280918485449465147073091262450275705860679870879159000949038958956730311645517982791135706223125791619417005994828833148949109384038976591682676049639275970773561031/2334295487112687911811298286960150438751666615178975527583435203112782475615129570140498624601866405876414309671989990174364441040132907110564319278979190612332213469456880852642638013477903483198709978702136688807201620996740915152339899937049386350380286635051033689609429884956927695277805080767362244280320*y^2 - 62313985535901249544030756671023201088141994776714199475098818954312252734512613319670899333233222447823960476692019175766589646036602925192606442162258931462773746119459802552701261758023128834701548922244734237540850463138994448345649264839981674896918307635235779911190250666066042697643146552154954989155849/9337181948450751647245193147840601755006666460715902110333740812451129902460518280561994498407465623505657238687959960697457764160531628442257277115916762449328853877827523410570552053911613932794839914808546755228806483986963660609359599748197545401521146540204134758437719539827710781111220323069448977121280*y + 7273278189256506705476310843123881901138090488387772991189730510306958773624419467758735339192413874748024865000733527726723782745963028912317412452559936258756764631169795784673384237706427116627607702557855810396589423464342775570547366575765327793592884893857538049476157166909000707195141917866212291960029/6224787965633834431496795431893734503337777640477268073555827208300753268307012187041329665604977082337104825791973307131638509440354418961504851410611174966219235918551682273713701369274409288529893276539031170152537655991309107072906399832131696934347431026802756505625146359885140520740813548712965984747520