# Manifold: Census Knot K8_74 # Number of Tetrahedra: 8 # Number Field x^27 - 6*x^26 - 35*x^25 + 365*x^24 - 2225*x^23 + 10568*x^22 - 37345*x^21 + 98207*x^20 - 183980*x^19 + 201618*x^18 + 51822*x^17 - 766970*x^16 + 1840666*x^15 - 2722594*x^14 + 2752843*x^13 - 1811707*x^12 + 535397*x^11 + 282839*x^10 - 422154*x^9 + 223748*x^8 - 49438*x^7 - 8050*x^6 + 8391*x^5 - 2090*x^4 + 73*x^3 + 71*x^2 - 15*x + 1 # Approximate Field Generator 0.652700326219865 - 1.11786956337303*I # Shape Parameters 11918914056119490923066019805286411/4170888172581837259188063439*y^26 - 65655858015504249443498858132443287/4170888172581837259188063439*y^25 - 449438480787206114447183070756118576/4170888172581837259188063439*y^24 + 4129572491456223993532632796123303109/4170888172581837259188063439*y^23 - 2226336386963496349691678848723221392/379171652052894296289823949*y^22 + 113920335080326582946153058463511600704/4170888172581837259188063439*y^21 - 389106789280639207951414694754995064852/4170888172581837259188063439*y^20 + 979208753217399738477593319095368614409/4170888172581837259188063439*y^19 - 9892073810056414999569499737139324592/24109180188334319417272043*y^18 + 141941913234475336529899218247307334347/379171652052894296289823949*y^17 + 1386083577163883989498904262679279614494/4170888172581837259188063439*y^16 - 8461032913329454523786434321001718967408/4170888172581837259188063439*y^15 + 17779072502078222564524620147018799481669/4170888172581837259188063439*y^14 - 23706596636411140863805981683214832539325/4170888172581837259188063439*y^13 + 21148588187114541204714154844681950087642/4170888172581837259188063439*y^12 - 11186009782534333964595963030050509323513/4170888172581837259188063439*y^11 + 79365440658917537141224754058531340667/379171652052894296289823949*y^10 + 3804449296182031388339257747164438877838/4170888172581837259188063439*y^9 - 3160771789224913898299732641151528476643/4170888172581837259188063439*y^8 + 100990853900041306440432229932247833495/379171652052894296289823949*y^7 - 41858847076244739694495210659263099675/4170888172581837259188063439*y^6 - 116794075977932632444872084609523316909/4170888172581837259188063439*y^5 + 42528267778490231722057772536260062676/4170888172581837259188063439*y^4 - 3952526807950442257107910178708054091/4170888172581837259188063439*y^3 - 1081883399998062370460002352860268170/4170888172581837259188063439*y^2 + 313645958954336887218247081062442208/4170888172581837259188063439*y - 24160642210697022244387596789706163/4170888172581837259188063439 599545779621432694777767243181813944334/343551887887393353202061597406991*y^26 - 3329047130408920077114010093758095020282/343551887887393353202061597406991*y^25 - 22473033225370313930910062613565388715113/343551887887393353202061597406991*y^24 + 208777939777147326723477371784066808788499/343551887887393353202061597406991*y^23 - 2301674794439461731717624837327530532927/637387547100915312063194058269*y^22 + 5781115149603614298424916512080445697578521/343551887887393353202061597406991*y^21 - 19804478066823244611561174920527134661274696/343551887887393353202061597406991*y^20 + 7146160487898675251986068229202875394690892/49078841126770479028865942486713*y^19 - 508307596264381151094839508135150821322088/1985849062932909556081280909867*y^18 + 25836920589058627098683868770669080269962/108822264139180663035179473363*y^17 + 67513555015599540385478288616303220981444720/343551887887393353202061597406991*y^16 - 429595384969034331261245723374784350935288286/343551887887393353202061597406991*y^15 + 911435911060864548294345585316292549903405874/343551887887393353202061597406991*y^14 - 1224833324992157037772995246838674515305280736/343551887887393353202061597406991*y^13 + 1102998243126181355095660812749927440437527790/343551887887393353202061597406991*y^12 - 593351963017463994666094626467263214978991267/343551887887393353202061597406991*y^11 + 5091948834122020412525517600982061265009654/31231989807944850291096508855181*y^10 + 194455309547883248542044534586556489187786568/343551887887393353202061597406991*y^9 - 166159517551356559859547319935316131606698104/343551887887393353202061597406991*y^8 + 5447488824154247703426076272023723078980571/31231989807944850291096508855181*y^7 - 2892802001461551592004106089172961486331910/343551887887393353202061597406991*y^6 - 6109664136447230902115078966898563523144585/343551887887393353202061597406991*y^5 + 2301268912434191506200311574460691289502269/343551887887393353202061597406991*y^4 - 225906355443256653094615951916351755967081/343551887887393353202061597406991*y^3 - 8132229996026348546918945632089546852329/49078841126770479028865942486713*y^2 + 17141301374708496086541928314711796460095/343551887887393353202061597406991*y - 1344091936273930515236926528838126755668/343551887887393353202061597406991 70046960035061453628642186268337717/4170888172581837259188063439*y^26 - 387340605026628958936012257107087538/4170888172581837259188063439*y^25 - 2633817135259726384084960197238716995/4170888172581837259188063439*y^24 + 24328619112992402434746207570251366207/4170888172581837259188063439*y^23 - 13128426259741003225860213419305253683/379171652052894296289823949*y^22 + 672337092663392610507402097518272975660/4170888172581837259188063439*y^21 - 2299688041555862849429845286978850188800/4170888172581837259188063439*y^20 + 5797466549072496810826262223952522491464/4170888172581837259188063439*y^19 - 58730280899753966795775103533657856842/24109180188334319417272043*y^18 + 849397105418988077426208517183756016321/379171652052894296289823949*y^17 + 8025898622217036533197278625853573886117/4170888172581837259188063439*y^16 - 49950971967290853367888428922567397995367/4170888172581837259188063439*y^15 + 105439747755249880077027387360207081776197/4170888172581837259188063439*y^14 - 141112589452336272759967499042714949814939/4170888172581837259188063439*y^13 + 126445540433654814463397147737617477447927/4170888172581837259188063439*y^12 - 67415069533071548010990813596551776819003/4170888172581837259188063439*y^11 + 525424754857755209361455901120432909590/379171652052894296289823949*y^10 + 22537597319069155809976758185296640068285/4170888172581837259188063439*y^9 - 18969578106682182321171621641113680364057/4170888172581837259188063439*y^8 + 613392473464753652912727453625345276023/379171652052894296289823949*y^7 - 287339345243246901891806126109480585526/4170888172581837259188063439*y^6 - 699478994663891842027137981322132040619/4170888172581837259188063439*y^5 + 258661059758798730830173676701614782602/4170888172581837259188063439*y^4 - 24654980295968300742369401704237272143/4170888172581837259188063439*y^3 - 6497487729537403289766701282173043171/4170888172581837259188063439*y^2 + 1916072788731922365006322601406027382/4170888172581837259188063439*y - 148783829424814471046888372594997347/4170888172581837259188063439 -5614748894590653198929583842982209827065/646262438788865355962153677619294*y^26 + 30990281428552049712535736265241715041037/646262438788865355962153677619294*y^25 + 211409182092362246933138074294423877600145/646262438788865355962153677619294*y^24 - 1947790775710881185161054768517063424946205/646262438788865355962153677619294*y^23 + 1050616031167718807071228495861260128549715/58751130798987759632923061601754*y^22 - 53782851140459053353042361989651874229349421/646262438788865355962153677619294*y^21 + 91918176915397639022687194723653455170790501/323131219394432677981076838809647*y^20 - 231530283293782308394063189411163086301101740/323131219394432677981076838809647*y^19 + 4684762426305089285890061466875142558958967/3735621033461649456428633974678*y^18 - 67503170638002671656805875822019949068336783/58751130798987759632923061601754*y^17 - 323919605732058929516120445160785996958757823/323131219394432677981076838809647*y^16 + 3995050187375430117161111222781130008813558811/646262438788865355962153677619294*y^15 - 8414972949194757517636702898287236873812113649/646262438788865355962153677619294*y^14 + 5621286346680667752818394994944403713825338797/323131219394432677981076838809647*y^13 - 5026690655530856742651134951555209575132709219/323131219394432677981076838809647*y^12 + 5340517869588337558316176872734650234901308055/646262438788865355962153677619294*y^11 - 39933785076615573974171344120574217202480909/58751130798987759632923061601754*y^10 - 1799335766163759794047698877760874451331900933/646262438788865355962153677619294*y^9 + 752782872974950675215022704935317414268129620/323131219394432677981076838809647*y^8 - 24212737597495924541398161012696042269173584/29375565399493879816461530800877*y^7 + 21542057673622871762578938859778923661644253/646262438788865355962153677619294*y^6 + 27781203340898029259671308577694331687666402/323131219394432677981076838809647*y^5 - 20409311996050377048646707674264233112131463/646262438788865355962153677619294*y^4 + 962350252493907968874146094307804103495049/323131219394432677981076838809647*y^3 + 257723688754324208044946874698477701657170/323131219394432677981076838809647*y^2 - 75455937434665971793566173950440315951843/323131219394432677981076838809647*y + 5839958551687842259179099694679497365001/323131219394432677981076838809647 -5614748894590653198929583842982209827065/646262438788865355962153677619294*y^26 + 30990281428552049712535736265241715041037/646262438788865355962153677619294*y^25 + 211409182092362246933138074294423877600145/646262438788865355962153677619294*y^24 - 1947790775710881185161054768517063424946205/646262438788865355962153677619294*y^23 + 1050616031167718807071228495861260128549715/58751130798987759632923061601754*y^22 - 53782851140459053353042361989651874229349421/646262438788865355962153677619294*y^21 + 91918176915397639022687194723653455170790501/323131219394432677981076838809647*y^20 - 231530283293782308394063189411163086301101740/323131219394432677981076838809647*y^19 + 4684762426305089285890061466875142558958967/3735621033461649456428633974678*y^18 - 67503170638002671656805875822019949068336783/58751130798987759632923061601754*y^17 - 323919605732058929516120445160785996958757823/323131219394432677981076838809647*y^16 + 3995050187375430117161111222781130008813558811/646262438788865355962153677619294*y^15 - 8414972949194757517636702898287236873812113649/646262438788865355962153677619294*y^14 + 5621286346680667752818394994944403713825338797/323131219394432677981076838809647*y^13 - 5026690655530856742651134951555209575132709219/323131219394432677981076838809647*y^12 + 5340517869588337558316176872734650234901308055/646262438788865355962153677619294*y^11 - 39933785076615573974171344120574217202480909/58751130798987759632923061601754*y^10 - 1799335766163759794047698877760874451331900933/646262438788865355962153677619294*y^9 + 752782872974950675215022704935317414268129620/323131219394432677981076838809647*y^8 - 24212737597495924541398161012696042269173584/29375565399493879816461530800877*y^7 + 21542057673622871762578938859778923661644253/646262438788865355962153677619294*y^6 + 27781203340898029259671308577694331687666402/323131219394432677981076838809647*y^5 - 20409311996050377048646707674264233112131463/646262438788865355962153677619294*y^4 + 962350252493907968874146094307804103495049/323131219394432677981076838809647*y^3 + 257723688754324208044946874698477701657170/323131219394432677981076838809647*y^2 - 75455937434665971793566173950440315951843/323131219394432677981076838809647*y + 5839958551687842259179099694679497365001/323131219394432677981076838809647 -164076828542937070593771276084238407887238/41037664863092950103596758528825169*y^26 + 2716901271801737534457941623697447278292002/123112994589278850310790275586475507*y^25 + 18533469040384018510115466359583891108968132/123112994589278850310790275586475507*y^24 - 56920250513130498367459303352542188106265629/41037664863092950103596758528825169*y^23 + 30702105916754786202774130343348589361107181/3730696805735722736690614411711379*y^22 - 4715094974636529431603261918604604940727853750/123112994589278850310790275586475507*y^21 + 5372280575425029944232038154704660089989552611/41037664863092950103596758528825169*y^20 - 40596395153264909872666040216862705430882048394/123112994589278850310790275586475507*y^19 + 410712611450824475099604354105322029645833974/711635806874444221449654772176159*y^18 - 1972659750085552528638714627292750349440647759/3730696805735722736690614411711379*y^17 - 56797424352747752569616306683914299519943800540/123112994589278850310790275586475507*y^16 + 116749742467941784612814862221404304263328969768/41037664863092950103596758528825169*y^15 - 737743273844824849152156174729934511428137843574/123112994589278850310790275586475507*y^14 + 985630184908767229960140494930449441448649750880/123112994589278850310790275586475507*y^13 - 293785423062298478206268320971986122734239898449/41037664863092950103596758528825169*y^12 + 156054930282153121047993869928134815972116145709/41037664863092950103596758528825169*y^11 - 3497758712014091000497204501099029665071762879/11192090417207168210071843235134137*y^10 - 157763003651255027499274150439595954222452655722/123112994589278850310790275586475507*y^9 + 131988539251282551311702432282120752609836479009/123112994589278850310790275586475507*y^8 - 4244629126522214105494153752422037464562294922/11192090417207168210071843235134137*y^7 + 1884361297356104353328319816457106120371125542/123112994589278850310790275586475507*y^6 + 4871411181570657159293149313195356845619316405/123112994589278850310790275586475507*y^5 - 1788838990495031887753514186984326726158009578/123112994589278850310790275586475507*y^4 + 168596459646565104566981474680312298292193898/123112994589278850310790275586475507*y^3 + 45191753502938535589035932885208105732439099/123112994589278850310790275586475507*y^2 - 13225235783613876988791693500777534011730261/123112994589278850310790275586475507*y + 341105239942658809513720631569843451221320/41037664863092950103596758528825169 16777216*y^26 - 92274688*y^25 - 633339904*y^24 + 5807013888*y^23 - 34425798656*y^22 + 160088719360*y^21 - 546500771840*y^20 + 1374389665792*y^19 - 2399477366784*y^18 + 2182850052096*y^17 + 1960853913600*y^16 - 11887194398720*y^15 + 24937653866496*y^14 - 33208720685056*y^13 + 29580681282560*y^12 - 15605059026432*y^11 + 1179941601536*y^10 + 5335221796992*y^9 - 4414957944768*y^8 + 1546389553184*y^7 - 56237228016*y^6 - 163175202808*y^5 + 59190018052*y^4 - 5469372414*y^3 - 1509949439*y^2 + 436207616*y - 33554431 -33554432*y^26 + 184549376*y^25 + 1266679808*y^24 - 11614027776*y^23 + 68851597312*y^22 - 320177438720*y^21 + 1093001543680*y^20 - 2748779331584*y^19 + 4798954733568*y^18 - 4365700104192*y^17 - 3921707827200*y^16 + 23774388797440*y^15 - 49875307732992*y^14 + 66417441370112*y^13 - 59161362565120*y^12 + 31210118052864*y^11 - 2359883203072*y^10 - 10670443593984*y^9 + 8829915889536*y^8 - 3092779106368*y^7 + 112474456032*y^6 + 326350405616*y^5 - 118380036104*y^4 + 10938744828*y^3 + 3019898878*y^2 - 872415233*y + 67108864 # A Gluing Matrix {{1,2,1,0,0,0,-2,1},{0,1,2,0,0,0,-2,1},{-1,2,2,0,0,-2,-2,1},{0,0,0,0,0,2,0,0},{0,0,0,-1,1,2,0,0},{0,0,0,1,1,0,-2,1},{0,0,0,0,0,0,0,0},{0,0,1,0,0,2,-2,1}} # B Gluing Matrix {{2,0,2,0,0,0,0,2},{0,1,2,0,0,0,0,2},{0,0,4,0,0,0,0,0},{0,0,0,1,1,0,0,0},{0,0,0,0,2,0,0,0},{0,0,0,0,0,1,0,2},{0,0,0,0,0,0,1,2},{0,0,0,0,0,0,0,4}} # nu Gluing Vector {2, 3, 0, 2, 2, 2, 2, 4} # f Combinatorial flattening {4, 1, -2, -6, -4, 0, -6, -6} # f' Combinatorial flattening {-4, 0, 0, 2, 0, 6, 2, 0} # 1 Loop Invariant -56156220648086475488274167108762867301433/646262438788865355962153677619294*y^26 + 154432770225888071556489614430301170878681/323131219394432677981076838809647*y^25 + 1059932028651853915127878355266542005577898/323131219394432677981076838809647*y^24 - 9718659557952396891823874604211626308983114/323131219394432677981076838809647*y^23 + 10475562455648493873105808714537413689385609/58751130798987759632923061601754*y^22 - 535856864466316596047219803812895206772808091/646262438788865355962153677619294*y^21 + 1829289105518056211281760196073818600030910351/646262438788865355962153677619294*y^20 - 4600509652970307572123880739439865465390158669/646262438788865355962153677619294*y^19 + 46427350124397259389188690994051219907270813/3735621033461649456428633974678*y^18 - 332143453212211966932513434503196551614749469/29375565399493879816461530800877*y^17 - 6562701574437956059830040862881288915916617561/646262438788865355962153677619294*y^16 + 39789398485458151316976065153317958242288370843/646262438788865355962153677619294*y^15 - 41737441011844573716819193097687445321613879953/323131219394432677981076838809647*y^14 + 111163593965391951239061650424569472662238039821/646262438788865355962153677619294*y^13 - 49510962239861919350390853300611299380802037165/323131219394432677981076838809647*y^12 + 26120563901619545369354081721929984840694303239/323131219394432677981076838809647*y^11 - 179680565472107905246475023588287807354299589/29375565399493879816461530800877*y^10 - 8929270755655154647221336003675213682300336207/323131219394432677981076838809647*y^9 + 7389761667228698430469665609426626125620243310/323131219394432677981076838809647*y^8 - 470651670521322795646536610113647594043034073/58751130798987759632923061601754*y^7 + 94239297077923752198039883213265315459883314/323131219394432677981076838809647*y^6 + 273117455262170395010792928671443147333710963/323131219394432677981076838809647*y^5 - 99082689757222359988314528125566408630398312/323131219394432677981076838809647*y^4 + 18315165593813740491254284480694526212955859/646262438788865355962153677619294*y^3 + 5054706203585778238535419038144571777362999/646262438788865355962153677619294*y^2 - 1460460983817942383707817802490186519013865/646262438788865355962153677619294*y + 112351282762957532000982102510584447980763/646262438788865355962153677619294 # 2 Loop Invariant -170590741519585857086818187426363108305194610328375206652864026206649520456565319781139649669095293709165153750991144397461434802624709/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^26 + 156924163030646536214529268937486371295997761685698271707573348428803218690850461048033996061189718406712255331832557211886113528850707/21630575557136796969068766201624128989173457963125136752058917903386179967004842065942540888540897414144098668150410620076503224*y^25 + 3211645999429605367385705350254879892867452597128905318983446933426275595940603329462961126380587696785353909450524237170887955908573119/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^24 - 9863042087167519269182052606914150688639481376872803671533450901131208256835718584336224649233945859573361270779306130847301009237098725/21630575557136796969068766201624128989173457963125136752058917903386179967004842065942540888540897414144098668150410620076503224*y^23 + 31919749643251150537586720961479096411971258776378082153956006901226062306986031730449650333113735758989899058115463541384013787851193441/11798495758438252892219327019067706721367340707159165501123046129119734527457186581423204121022307680442235637172951247314456304*y^22 - 544672218607718261883791935436369171721963847592587736537160871041310160789434785648690543695682973949975697323744521152462015203740794523/43261151114273593938137532403248257978346915926250273504117835806772359934009684131885081777081794828288197336300821240153006448*y^21 + 1396301612334650110423754594400145650127855542316124274258921010385718179874114031646263691984115356872069453795419611514872512835678146199/32445863335705195453603149302436193483760186944687705128088376855079269950507263098913811332811346121216148002225615930114754836*y^20 - 3517051739340029897097675088435716578438806336048558024643925326220709260211169745899173797941827924816729345003635118407004167458466709205/32445863335705195453603149302436193483760186944687705128088376855079269950507263098913811332811346121216148002225615930114754836*y^19 + 23720597635210230316318078861606335195248962535846374346809183505238257001341682170710844972070509493325263737312683492682145015670122083/125032228653969924676698070529619242711985306145232004347161375164081965127195618878280583170756632451699992301447460231656088*y^18 - 256323325720731099208573966898154237356624357789243111388465253432359187786709095600487196069297897539974880899593316834674978978513118147/1474811969804781611527415877383463340170917588394895687640380766139966815932148322677900515127788460055279454646618905914307038*y^17 - 19686745030053512794538605932957916429804384662766817587526586935138775643965139819126793048550124658077842199183702380744454543486968949939/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^16 + 40459285827182919057667866289033586530846735891428156861880984870472350666713983405251422372209429825542817453423610274089062967524521428005/43261151114273593938137532403248257978346915926250273504117835806772359934009684131885081777081794828288197336300821240153006448*y^15 - 255651494225808525231023736399206115642586973781316706048615994956060426232086426206886219538663108973904234382591637293515269900038050074219/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^14 + 170770230547944791618221736031304964867409506798007646071292913924802666234244161700912141936008496327077618958797245913523969841055222083425/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^13 - 305395645443631505004250448435315358516202037421765875150143275033780640691963891878060851371316080085986403817764676116774863457656102983541/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^12 + 162211687281097431787645249079549065117431690895522934339860578052885485699257352280885731283128377773095656546433238447395841314743684808379/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^11 - 302767565265602201281590953978715547018990422318867778435816274021373562052790391652845500029508314032573937471860007303015721535143404099/2949623939609563223054831754766926680341835176789791375280761532279933631864296645355801030255576920110558909293237811828614076*y^10 - 54669048336902100219990355433943328443070953123609016192185876464059679347976254961091857045809322695126842760374328245795801054121462162823/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344*y^9 + 22866615049050391225656039195670574299625713521937285079466989898824613081772210471348588375783343437567160707585701048984441143665072066327/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^8 - 735314969902767696432671139400243421004679146852916669997230768282845694224245774238979410316245005399646400722651843420633533606454546527/5899247879219126446109663509533853360683670353579582750561523064559867263728593290711602060511153840221117818586475623657228152*y^7 + 326228064411393474686790625308672580444820648444027219720477148188459800848183012593668375576623113960500792716572338268331527069977378709/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^6 + 843954555066328934432689809605716273476065409445693194800112340397955543527482895352691001132249323809331643967167645577063310085052382429/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^5 - 309888523279216714724745718403356438472440207844157220663685886314199885998936509741819924373685820601953282209884656443673732128528666241/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y^4 + 1216843223723668242860289862928508499292189441574148452914278407438221772792002599594125245633282937988587720945838105699829859970213855/2703821944642099621133595775203016123646682245390642094007364737923272495875605258242817611067612176768012333518801327509562903*y^3 + 978635994664673218053371473599465662211115657035503972291411140553564807103682920248859085059384213695152597181393827728529612711870918/8111465833926298863400787325609048370940046736171926282022094213769817487626815774728452833202836530304037000556403982528688709*y^2 - 2291058914113209096850847155102610900794519487102258128224489196628734792164368197282140944370921823832962691439111441254817581408866717/64891726671410390907206298604872386967520373889375410256176753710158539901014526197827622665622692242432296004451231860229509672*y + 354543156588303677053702520550796661313676793187436935308107613015217591328672496854025061317238284523534928909640605653987559657450555/129783453342820781814412597209744773935040747778750820512353507420317079802029052395655245331245384484864592008902463720459019344 # 3 Loop Invariant 12360182734909587101673621154058694838589304467518566130195302991450081411432571009600152736578395500777979302777073365829892255255274653875659306850258941006134678878960834784822693/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^26 - 17067237309553355090008648729075922067145213158662372860132279229246385633203307726928652336383700549450869959044989233370613598086066157365313270614520276636203066680490568107053779/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y^25 - 465151073566444694763647873340064534732959827668718887049120527890574424327917114608620598735214507491775020215075951253213844606800965068772762644692639769046386671499415337005371669/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^24 + 1072432610650792566282787036354578593608901676836439881320003398203120545565278964493135978883607048132734212230300745166897823109428624342789670716934071396491590324842596532602977871/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y^23 - 2314222845608577697313821017054357972496215391444917644651839071653885883978134623447180580912386319446590283172003439111617127637307024915869880254417904773081597140182589939489180501/1439013810153011218517321722775567647054329326568660121363359424929221243303536351680499566597324961578378244215369445132389408089466976052650556830031588498017072683560197696*y^22 + 118487022781552373999324960814957126956003468176764053460303960697540513074073689891593630661873297685687943328514388985707947466855723148343326922375486382804089556784732688167453975337/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^21 - 405106643390726536516946078123962226262211339020014059932108399390263455162298055827951866416747514085517045401648270153078047610184253161424680414684878566400180251871045713965542918799/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^20 + 1020735273310024484172021050990147647033285296463607760061173344877681351672109704674826194362837239659596192824851078933115657625262566272645369257362117637590616748849249952687419851015/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^19 - 10331910287970195415750274530059084191378671444922145964654742841882606921300482965705275690281054443378791906129391523589741879543037756767593770962184652427890681510797120668389789783/91497987928804181524222768500180601835824408047718273612699154186251061712941617736910377066881933973191680268029271077781985485457437783694544075897962274440391904735041472*y^18 + 37270974185814723349474915479062915953440917194288114818090266224422865659320506694390887462062313656549583317752882762417205358112054823766148667109698199214793486092235270414724823029/359753452538252804629330430693891911763582331642165030340839856232305310825884087920124891649331240394594561053842361283097352022366744013162639207507897124504268170890049424*y^17 + 1422355704038778846446284450553348704380289270251600954153652140164046918046492999310174892807866424770209321835410338922234480224843857465046679014351524056263577719460003595502565938507/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^16 - 2200474150926607054140062655424689786436669819656115055161840360654122605922118141901943130535201982802062209646996856107300361510720205726218391891833496782466817609480292097173721806159/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y^15 + 18554978226268283941858712247525151375418755453485857053192739209883034048331501272633490960591723650832617046045982258094940252276591737263044607838983190647540455752247008220448205775417/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^14 - 24806139356884316926694529258511210725894332356818511727585613005027163089572061456173574378141123905455349061514835115144284675487937081593924821729016261037667813366880569950659970664265/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^13 + 22199724952300316304562806051778391936318949269505279873685726449192500178089289528305757564772376641184257696971616157292792808626522681918343208229665659086531127934949453845906870824891/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^12 - 11809446917110374926620890103993702394910949472401866403873691577563077893353755292359957897129237813745539445642525917873684502901373090191603859463372254318212730603718660896806922240079/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^11 + 89754826777720039872771725078778309147433736892818971509327201196568733192958234735869417815642158662837203267114579862207113758543327446383101870405736751419802327050428621808349596301/1439013810153011218517321722775567647054329326568660121363359424929221243303536351680499566597324961578378244215369445132389408089466976052650556830031588498017072683560197696*y^10 + 991715966856743720789033732498289650632576029975972433337013917586005015395116691840683768795814542281653452201340605512115665264225532881234027640742382922425012260516395970741856053799/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y^9 - 3326809649871120272720732638505621677127142840347394551128202971440598036953188835271584169147644599706102106421102669014996232281196979357120083340371500533389931176708986177596660648027/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^8 + 107227354929964939361336199878129016464716531710405411772475914737459107933564620414514006640976304865621802288188128660828475316795313113905348969847381787763923998113048183578670690601/1439013810153011218517321722775567647054329326568660121363359424929221243303536351680499566597324961578378244215369445132389408089466976052650556830031588498017072683560197696*y^7 - 12174801715314124286187628088758247302556101267452152553265941811404650439025520334000584403360617567662687818366319867809831377961324870399456621238124534761536873501638664112286182375/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y^6 - 122732058520506203788582902566920002523512481019504655009446117240306833239812104677766709767741527283941989599295927679053642592520218724789353237117197284481382200637790389550038490555/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^5 + 45202108404184164178320928021970287803388223298879274065008726319706209359145929867338902160337108421290893917272586531803740660018739626236399730361263840265415184928718813992110136063/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^4 - 4281126769646294425955336710095229088081417347837461734556051458047207533531440266623773564028672417221154803789786453146107687695688378496466212078419271323683635098158943954837668627/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^3 - 1139139552454563189199083106232199712932287406154325719410190847766261469562031740692664651979889116841727376336173927622055367357450234051996442617168415504025987717198521715775604085/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656*y^2 + 83620996538021691320848415825220146828317317393455868370281952761129303187403584781587162886940066946408039801076565060754595927317198767000756424107684242876493719096503661743470099/3957287977920780850922634737632811029399405648063815333749238418555358419084724967121373808142643644340540171592265974114070872246034184144789031282586868369546949879790543664*y - 25922395988183488805198996785010474440719342384560989787181761889060726581754088175063321762448229818874638646315566731915873782535541720915546481222422131888325367713833364300431589/15829151911683123403690538950531244117597622592255261334996953674221433676338899868485495232570574577362160686369063896456283488984136736579156125130347473478187799519162174656 # 4 Loop Invariant -3428918174570301622839766916702299851133822549416500896926064442908178308997107942448771681704874476933824389287963132560784751103821342500965149446976690695522632999652859354365608978041379947148457705544383351212864548961376232638375544999634412217506082712819121026498973691/23841266433915920393253994481754959452517844947501534970122216855173707974786682031114547085834859079882829834005824817363850214904161316980903693502771151877770114330255798228929586176620904499078893559180920281175243785304807787982650163969757946774971361427403612593920*y^26 + 76120233033344656940384219749305863648870313125677788849222949060573096218219534326176259584455363744232627078920700255656348397481711882621644519491117176570234848415687179889754477189776880384517335232477424040823710833115960267431899412459751866907813089964146047039030787333/95365065735663681573015977927019837810071379790006139880488867420694831899146728124458188343339436319531319336023299269455400859616645267923614774011084607511080457321023192915718344706483617996315574236723681124700975141219231151930600655879031787099885445709614450375680*y^25 + 171440527035987390254930552381044796095084851586937542909966650297708041438891194257057206534384130088904349104770527811982540844917414901227460440749058600720025637297002396624666190672053821053935006597606713068228940455616439194120751845332969891674074623274332882506395366251/31788355245221227191005325975673279270023793263335379960162955806898277299715576041486062781113145439843773112007766423151800286538881755974538258003694869170360152440341064305239448235494539332105191412241227041566991713739743717310200218626343929033295148569871483458560*y^24 - 4774756651551259354475720884844006195786657740403577948308561090885758853909339998839906068031807212741129021851859517210287229905865285797885766539932389354207468607730166418378891930355924967411271485681083654561462106303395152356510148622851471993893600633788084494366409516473/95365065735663681573015977927019837810071379790006139880488867420694831899146728124458188343339436319531319336023299269455400859616645267923614774011084607511080457321023192915718344706483617996315574236723681124700975141219231151930600655879031787099885445709614450375680*y^23 + 57308591184588713283021450605774201775073677974766121925044358945297207043454752874196875634142187518790389710001561794440403734387399606328243517684692717575211211006837306032603504556124967303214898652675991816397257189632984090266468367848171536202313675466891541200884592897/192656698455886225400032278640444116788022989474759878546442156405444104846761066918097350188564517817234988557622826806980607797205343975603262169719362843456728196608127662455996655972694177770334493407522588130709040689331780104910304355311175327474516051938615051264*y^22 - 33043774759702876336001445196729623137727502436499153034805826169354856289394839337138011374481570592166851058524325372338135412148777592181063542681489857073532245230420292323882999523706892230978327962972944553077424869033939019192500272391168500115015950051313934344788142673199/23841266433915920393253994481754959452517844947501534970122216855173707974786682031114547085834859079882829834005824817363850214904161316980903693502771151877770114330255798228929586176620904499078893559180920281175243785304807787982650163969757946774971361427403612593920*y^21 + 113174651526585923400217712989114524175115519384462139085977085198523659700312872226149338098445365877291854759364140594180479096093484606968724520628285851157584146947953912971338492832477477204652288533624629929628740567833861605789792400914323568831566825640724058216684851735443/23841266433915920393253994481754959452517844947501534970122216855173707974786682031114547085834859079882829834005824817363850214904161316980903693502771151877770114330255798228929586176620904499078893559180920281175243785304807787982650163969757946774971361427403612593920*y^20 - 1190753134068220167861053886388312570652924426877357592496105860025350258202367040339562819925245212441607554405761843045086826637306526581297342706794220406247465085048834765226966409347323532009628473579843519329885348318339866317082066226380515101913741693012919023026754660319/99338610141316334971891643673978997718824353947923062375509236896557116561611175129643946190978579499511790975024270072349375895434005487420432056261546466157375476376065825953873275735920435412828723163253834504896849105436699116594375683207324778229047339280848385808*y^19 + 2322074714112679845373179407408963453451037981411329878508988025969455258486574064376341826088494792234070656210560798084527214806871925539241235835052420481303775776916880081578336239857143518864613926620389593197105920611767802981620357277112357815359314688712999260139141656025/110248630908281712801174540956092298046325294554920392925420655977681886588608934247928541437386631583273201544535606091855954751001902043842329218509924401746913823492512361752275543013275858955278120504882868352255462591004891505122081683097146574681948492149843295232*y^18 - 1879362006112591140080745849201997149497529224371829263727293879448996562645957793832363712148328422505244640883327697094731227600244833305873191717869549118033071774563490562722231401225867178867063776272292298533699602873390237591243429837200662711568737682954044442172130431483/96328349227943112700016139320222058394011494737379939273221078202722052423380533459048675094282258908617494278811413403490303898602671987801631084859681421728364098304063831227998327986347088885167246703761294065354520344665890052455152177655587663737258025969307525632*y^17 - 258215701762091177590845386193089908025560863488652923430741878829080734178805303794669785259095560216451419301278953776631704587981028190470785483832494752874307348827626272510019489890303461271873596543814927593798485082323438124407349108719675836315715491420225800827774318390071/15894177622610613595502662987836639635011896631667689980081477903449138649857788020743031390556572719921886556003883211575900143269440877987269129001847434585180076220170532152619724117747269666052595706120613520783495856869871858655100109313171964516647574284935741729280*y^16 + 3274285801849362743907480298458279858654931358526016731770423170202348986676283892901621858067280635086784762469204972983661832878947312717404076288532648386829559106474528784558449612778073648793624988125431133829355003387365575953601058266616972849125934247893828402247237811197233/31788355245221227191005325975673279270023793263335379960162955806898277299715576041486062781113145439843773112007766423151800286538881755974538258003694869170360152440341064305239448235494539332105191412241227041566991713739743717310200218626343929033295148569871483458560*y^15 - 10411510870935583404695077632898810767711767241486099759468911858210695897680267934065048130663873689732173230471024341602519965082251257792300618978406210532501981625746989850830462608881868647217414944909155336258286770759099049521942794856162739408277383842546527552156621671495123/47682532867831840786507988963509918905035689895003069940244433710347415949573364062229094171669718159765659668011649634727700429808322633961807387005542303755540228660511596457859172353241808998157787118361840562350487570609615575965300327939515893549942722854807225187840*y^14 + 13981653682488110645798065741232977523332076412163358366980254619329155532960336670434031613126765233584351312317859274650826655853014120091877784071021221106701147614247893589487464967122282573165702623851792564795546129910069812814441983400534021969722060718386097863048999813382267/47682532867831840786507988963509918905035689895003069940244433710347415949573364062229094171669718159765659668011649634727700429808322633961807387005542303755540228660511596457859172353241808998157787118361840562350487570609615575965300327939515893549942722854807225187840*y^13 - 12579517165769284191431374432425265252255569382292655026328668758881752617445422528675194247415797464455445724923928286559363007262551200187806623392401783697525595182083313671901676614125573063110214898071545014186435148358613523520399227677239681503180023602963412257765688148946199/47682532867831840786507988963509918905035689895003069940244433710347415949573364062229094171669718159765659668011649634727700429808322633961807387005542303755540228660511596457859172353241808998157787118361840562350487570609615575965300327939515893549942722854807225187840*y^12 + 84442533673542088296611366488856805990312303417640370967321943537134639596861842774885913635039176535652735885532798318988213539295499177925925910607876727892727469815689408950367939431160141557106577040870057560404939546760277607317821641708449549274801571656747195909937467870149/596031660847898009831349862043873986312946123687538374253055421379342699369667050777863677145871476997070745850145620434096255372604032924522592337569278796944252858256394955723239654415522612476972338979523007029381094632620194699566254099243948669374284035685090314848*y^11 - 22755372328057263360378365829755028088878907537054362016232342158136698847055483670654230380745672692781234235012157114501257020840086231288844875158914643872204023849707836289073733273177090737287370701329108878331854727882199386225359811888361965051880759703554678472625902980309/1733910286102976028600290507763997051092206905272838906917979407648996943620849602262876151697080660355114897018605441262825470174848095780429359527474265591110553769473148962103969903754247599933010440667703293176381366203986020944192739197800577947270644467447535461376*y^10 - 494064251092506993937995624308630423569236489765140111372928441242658381471348701967627628167078865881960560041716919153548123970611903190472437908752874108594325175042011891665895103461264052527670740832664741734726364505551206939079522521947837890860279496555145280880166518623299/10596118415073742397001775325224426423341264421111793320054318602299425766571858680495354260371048479947924370669255474383933428846293918658179419334564956390120050813447021435079816078498179777368397137413742347188997237913247905770066739542114643011098382856623827819520*y^9 + 473432463291013478868557383169608627143793241274020429446650204501174827657483546554856109988809553707230184849442644986866822645262705242243066575570786440998885600931169001214053783934955052485724942801716112160076083250202548655638083888942852063236344118473419143205158255576081/11920633216957960196626997240877479726258922473750767485061108427586853987393341015557273542917429539941414917002912408681925107452080658490451846751385575938885057165127899114464793088310452249539446779590460140587621892652403893991325081984878973387485680713701806296960*y^8 - 24756460237698693219667522778710417154060002503536074264640283224440301540969999679841903484663835950903811538343126000606613354796596986385275263187569220348317247391601508178835421592061147885317566277317507343530743915459651943256476355706177951653417542573384300850139635666389/1733910286102976028600290507763997051092206905272838906917979407648996943620849602262876151697080660355114897018605441262825470174848095780429359527474265591110553769473148962103969903754247599933010440667703293176381366203986020944192739197800577947270644467447535461376*y^7 + 332597075522419003454654388684734321893205984788013083847757115787710456273035824289676665968958799548180046997607721771768721810315933040340403158296653908806428742481198738786134429136265282103112450156618625777877947168984102553704983151483203027493055827639973612293805796261/496693050706581674859458218369894988594121769739615311877546184482785582808055875648219730954892897497558954875121350361746879477170027437102160281307732330786877381880329129769366378679602177064143615816269172524484245527183495582971878416036623891145236696404241929040*y^6 + 11616627650013574617687703933958465053085867974170637901570413313710263835351805946307714051883158593964609641672631604791672439490764474279076168184481489075125917500368155853853490241165248823421658320063314787718803994657351878346613635885931351338366103186884102654136700663999/7947088811305306797751331493918319817505948315833844990040738951724569324928894010371515695278286359960943278001941605787950071634720438993634564500923717292590038110085266076309862058873634833026297853060306760391747928434935929327550054656585982258323787142467870864640*y^5 - 17419906688721296237535373199749949456315487531735477524605688850737782853922350496634310329019828000973012425099075700670137694893565355735451151285724442263142426790168668715116880751587784702251983666806628403605472987710854863150521912591664216787671288385249114519391205737283/31788355245221227191005325975673279270023793263335379960162955806898277299715576041486062781113145439843773112007766423151800286538881755974538258003694869170360152440341064305239448235494539332105191412241227041566991713739743717310200218626343929033295148569871483458560*y^4 + 5089696228393492216033859102472203474878243250360505070430525738434560706479861638422581096219086187865064579718812614578939944831944676142507598437809704008280323368245340801345968008470372124248092182631487367215214251357100693277979668380240932579042550164756576900014700843281/95365065735663681573015977927019837810071379790006139880488867420694831899146728124458188343339436319531319336023299269455400859616645267923614774011084607511080457321023192915718344706483617996315574236723681124700975141219231151930600655879031787099885445709614450375680*y^3 + 1298197434849870457009281895248005676435182448200395580415178748279344950348921908131236332844262514484950913224428992184185469328682814724992914869022853941554280963931341059469437998336725304889300704051705860374102973938208936127278678892315933690919876481240412749780099358061/95365065735663681573015977927019837810071379790006139880488867420694831899146728124458188343339436319531319336023299269455400859616645267923614774011084607511080457321023192915718344706483617996315574236723681124700975141219231151930600655879031787099885445709614450375680*y^2 - 388598610994970785165562146726411048501574090394359041986626625573097238862359210649747768521101931214843095847716291888870919980406720005224471362286762160395087405840489870391028969905891938527791447906177264274187430138304408296242898128066309560523611077865793807052828880679/95365065735663681573015977927019837810071379790006139880488867420694831899146728124458188343339436319531319336023299269455400859616645267923614774011084607511080457321023192915718344706483617996315574236723681124700975141219231151930600655879031787099885445709614450375680*y + 15190657032073270085750053541521853320511517760412894835215025973686578810324809784379865233896925442721762067174212800439957646593011731505859723807340827996939749274470311805980878583136321970194870047517004588334261283603979472509600308296193007837872286291064768924872430941/47682532867831840786507988963509918905035689895003069940244433710347415949573364062229094171669718159765659668011649634727700429808322633961807387005542303755540228660511596457859172353241808998157787118361840562350487570609615575965300327939515893549942722854807225187840