# Manifold: Census Knot K8_272 # Number of Tetrahedra: 8 # Number Field x^17 + x^16 - 193*x^15 - 2779*x^14 - 23873*x^13 - 152918*x^12 - 651210*x^11 - 2317513*x^10 - 6251205*x^9 - 11853058*x^8 - 15218531*x^7 - 12427311*x^6 - 4753435*x^5 + 2033925*x^4 + 4037659*x^3 + 2498758*x^2 + 702039*x + 52155 # Approximate Field Generator -0.360639252460801 + 0.856597668631761*I # Shape Parameters -29026148851809797059206475330027797100441/251467896081881890358234525699103205475132355264*y^16 - 14405991141221707668560733509230097050649/125733948040940945179117262849551602737566177632*y^15 + 5560227285269748219704170311310713034738471/251467896081881890358234525699103205475132355264*y^14 + 40300000584896532592167674742634663304004581/125733948040940945179117262849551602737566177632*y^13 + 700405548308880762509541363443553782824638947/251467896081881890358234525699103205475132355264*y^12 + 4546515700569070821845724665986823032834641353/251467896081881890358234525699103205475132355264*y^11 + 6610680866974323244365114731132373537342787905/83822632027293963452744841899701068491710785088*y^10 + 18318672472487251361029726977895478948980055017/62866974020470472589558631424775801368783088816*y^9 + 68959442982816108538008843568264400807552607883/83822632027293963452744841899701068491710785088*y^8 + 437093979907998950221054989659611334400523084243/251467896081881890358234525699103205475132355264*y^7 + 347966375776275625579999924044878409949221544831/125733948040940945179117262849551602737566177632*y^6 + 291491257898747564151337351598046958395026789767/83822632027293963452744841899701068491710785088*y^5 + 113736980178532653562277517163090086252158345159/31433487010235236294779315712387900684391544408*y^4 + 286465723201595771678827321334453438017720620329/83822632027293963452744841899701068491710785088*y^3 + 98316388275000080790723794210014811546634743539/31433487010235236294779315712387900684391544408*y^2 + 389008676425215115569141891130766356926667077313/125733948040940945179117262849551602737566177632*y + 219599179673592100276224486312165545272152820417/83822632027293963452744841899701068491710785088 505833375094976615685692874383596772743292213/68308896459117447873092300457482956674768374941635*y^16 + 497890517538771180246431117460016522263116153/68308896459117447873092300457482956674768374941635*y^15 - 97622308038536317771923913425706579621225462649/68308896459117447873092300457482956674768374941635*y^14 - 1404183271369058820364625195409984815641428723482/68308896459117447873092300457482956674768374941635*y^13 - 12055893535189299972591005888078555270266508503354/68308896459117447873092300457482956674768374941635*y^12 - 77190078136248461311599542963850747794228881274404/68308896459117447873092300457482956674768374941635*y^11 - 7298251978265641226346469578004063098679370052423/1517975476869276619402051121277399037217074998703*y^10 - 1168519765510072092393210579140323443347807354133944/68308896459117447873092300457482956674768374941635*y^9 - 69979367576428884684293545933361671655268234851214/1517975476869276619402051121277399037217074998703*y^8 - 5964750672889724222791920987415406906166302920467794/68308896459117447873092300457482956674768374941635*y^7 - 7648358759918865142162279423205310252060807542638423/68308896459117447873092300457482956674768374941635*y^6 - 109415127644349856135074195942236666051509867128709/1198401692265218383738461411534788713592427630555*y^5 - 475317764461750376773774840899045146586898705155829/13661779291823489574618460091496591334953674988327*y^4 + 22811284177215939332668259549625462036278164619840/1517975476869276619402051121277399037217074998703*y^3 + 2030340408385486902629280426038951331678287570510282/68308896459117447873092300457482956674768374941635*y^2 + 1246565963701994702402781933477151370203788787319549/68308896459117447873092300457482956674768374941635*y + 42440483093728974857320870680854305985955961100308/7589877384346383097010255606386995186085374993515 5306388196576954611547947515739108842788942481259930151243/269498927235705683347898162414640884639295949080653075915181568*y^16 + 1813475280431621735388777707983514080915889494714354255009/134749463617852841673949081207320442319647974540326537957590784*y^15 - 1031689910783172304581452998002065358161283727838555055558209/269498927235705683347898162414640884639295949080653075915181568*y^14 - 7207138342256965491725840582996731608465395280721745665387511/134749463617852841673949081207320442319647974540326537957590784*y^13 - 120882358192604551632973437284380534598537633208288886879432625/269498927235705683347898162414640884639295949080653075915181568*y^12 - 757704527872374184832649036121827598085677863652411650857529383/269498927235705683347898162414640884639295949080653075915181568*y^11 - 3093570796368417702803850164416132016398907071125790414004068721/269498927235705683347898162414640884639295949080653075915181568*y^10 - 1323693462354513089604169942873806631077565282624426876427663283/33687365904463210418487270301830110579911993635081634489397696*y^9 - 27185169312034221109720981190786936990412156338775308268898577839/269498927235705683347898162414640884639295949080653075915181568*y^8 - 45397218924521284508106145696655915146084710290877271685895980929/269498927235705683347898162414640884639295949080653075915181568*y^7 - 23348072383437570369912579917881252291139600756534327880171824643/134749463617852841673949081207320442319647974540326537957590784*y^6 - 24537600683966257406807445757966739231540224388121201762954194147/269498927235705683347898162414640884639295949080653075915181568*y^5 + 318972272035977743811504723858153654370872108665165532900575045/33687365904463210418487270301830110579911993635081634489397696*y^4 + 14253557605919725438082180963363714940808840152543906096679907135/269498927235705683347898162414640884639295949080653075915181568*y^3 + 2463296443079471926487379324041260324985635765887947220009404265/67374731808926420836974540603660221159823987270163268978795392*y^2 + 1255987199697072443391029961232403022255041947803489258444909211/134749463617852841673949081207320442319647974540326537957590784*y + 272759793400153522001777332139028832507235463171292892462583435/269498927235705683347898162414640884639295949080653075915181568 5306388196576954611547947515739108842788942481259930151243/269498927235705683347898162414640884639295949080653075915181568*y^16 + 1813475280431621735388777707983514080915889494714354255009/134749463617852841673949081207320442319647974540326537957590784*y^15 - 1031689910783172304581452998002065358161283727838555055558209/269498927235705683347898162414640884639295949080653075915181568*y^14 - 7207138342256965491725840582996731608465395280721745665387511/134749463617852841673949081207320442319647974540326537957590784*y^13 - 120882358192604551632973437284380534598537633208288886879432625/269498927235705683347898162414640884639295949080653075915181568*y^12 - 757704527872374184832649036121827598085677863652411650857529383/269498927235705683347898162414640884639295949080653075915181568*y^11 - 3093570796368417702803850164416132016398907071125790414004068721/269498927235705683347898162414640884639295949080653075915181568*y^10 - 1323693462354513089604169942873806631077565282624426876427663283/33687365904463210418487270301830110579911993635081634489397696*y^9 - 27185169312034221109720981190786936990412156338775308268898577839/269498927235705683347898162414640884639295949080653075915181568*y^8 - 45397218924521284508106145696655915146084710290877271685895980929/269498927235705683347898162414640884639295949080653075915181568*y^7 - 23348072383437570369912579917881252291139600756534327880171824643/134749463617852841673949081207320442319647974540326537957590784*y^6 - 24537600683966257406807445757966739231540224388121201762954194147/269498927235705683347898162414640884639295949080653075915181568*y^5 + 318972272035977743811504723858153654370872108665165532900575045/33687365904463210418487270301830110579911993635081634489397696*y^4 + 14253557605919725438082180963363714940808840152543906096679907135/269498927235705683347898162414640884639295949080653075915181568*y^3 + 2463296443079471926487379324041260324985635765887947220009404265/67374731808926420836974540603660221159823987270163268978795392*y^2 + 1255987199697072443391029961232403022255041947803489258444909211/134749463617852841673949081207320442319647974540326537957590784*y + 272759793400153522001777332139028832507235463171292892462583435/269498927235705683347898162414640884639295949080653075915181568 -533111643395679391459780878523746070640295536778688019623/33687365904463210418487270301830110579911993635081634489397696*y^16 - 254696552668798084726222793360467444860249417419601201875/16843682952231605209243635150915055289955996817540817244698848*y^15 + 103395181305706816555535328335997497629010737339287103227713/33687365904463210418487270301830110579911993635081634489397696*y^14 + 738260032793375489208019726679791135047845194177749708567275/16843682952231605209243635150915055289955996817540817244698848*y^13 + 12568488874409989331073572706234375696274210332802076264151533/33687365904463210418487270301830110579911993635081634489397696*y^12 + 79793551756697359320697098727111522634344849821950654193145903/33687365904463210418487270301830110579911993635081634489397696*y^11 + 334340438728570999226496889756826545661594995857315585595377373/33687365904463210418487270301830110579911993635081634489397696*y^10 + 291255474692909627201790799858528643870575195979240942178649449/8421841476115802604621817575457527644977998408770408622349424*y^9 + 3077589406729921286868023355994517046379239313311382385470269399/33687365904463210418487270301830110579911993635081634489397696*y^8 + 5490792679667458711122040884379487378425736487228028014680465741/33687365904463210418487270301830110579911993635081634489397696*y^7 + 3156404398369028474247034972083788815059664480859077592532560389/16843682952231605209243635150915055289955996817540817244698848*y^6 + 4131356629112546711181016629543916761174408496372063666330392275/33687365904463210418487270301830110579911993635081634489397696*y^5 + 59907629646554018182934406539234591234455389649212275780137547/4210920738057901302310908787728763822488999204385204311174712*y^4 - 1819378651462613383758260276457194310239160853510758903929478763/33687365904463210418487270301830110579911993635081634489397696*y^3 - 27895362650988048276159703410228823509602632997998699447522823/526365092257237662788863598466095477811124900548150538896839*y^2 - 360791237096424716730961553526527021052127351480123345653782077/16843682952231605209243635150915055289955996817540817244698848*y - 65862780011407102603468177029940009289280892450833202886431259/33687365904463210418487270301830110579911993635081634489397696 1643771419083451131584889036539342680014197836347972220697/33687365904463210418487270301830110579911993635081634489397696*y^16 - 218190138746278846244996054526620601182131326705258683681/16843682952231605209243635150915055289955996817540817244698848*y^15 - 317203779951893623489336775056013679527957055444893298967379/33687365904463210418487270301830110579911993635081634489397696*y^14 - 2083016419140727707463807203559563070909906546938847465837981/16843682952231605209243635150915055289955996817540817244698848*y^13 - 33872118150347224041371964257975720475971893877109706587493419/33687365904463210418487270301830110579911993635081634489397696*y^12 - 207298564181238941140235202869803676951543439261793381963528725/33687365904463210418487270301830110579911993635081634489397696*y^11 - 798744439888890511308096013389462377647552576653023718721964267/33687365904463210418487270301830110579911993635081634489397696*y^10 - 171457107845112387996686050001531260268338283404831297198925981/2105460369028950651155454393864381911244499602192602155587356*y^9 - 6609072094223201922241333985655521980422036959469834387204203981/33687365904463210418487270301830110579911993635081634489397696*y^8 - 10459782902173328086158592453827147759587590654933926508746853147/33687365904463210418487270301830110579911993635081634489397696*y^7 - 5186190024003043326151460184554727095370599116329931664278148453/16843682952231605209243635150915055289955996817540817244698848*y^6 - 5471934791220160799440176896536495051155799108576244356215453113/33687365904463210418487270301830110579911993635081634489397696*y^5 + 49935893053270908059066146331324335351525183517636277010054319/4210920738057901302310908787728763822488999204385204311174712*y^4 + 3062617390095689021815424614925661769833313449733504412539879093/33687365904463210418487270301830110579911993635081634489397696*y^3 + 578794922400848457196982362961261120199925010323422282833679477/8421841476115802604621817575457527644977998408770408622349424*y^2 + 395306397212333532913635801819778052760260338185732463882701149/16843682952231605209243635150915055289955996817540817244698848*y + 108460507666174275573875213346646325773504344890606450758895185/33687365904463210418487270301830110579911993635081634489397696 -4550080083144221343962424290980914143689871190092904890352613/154119699012919187664579261630872755903097370880498477788994459200*y^16 + 435860714385266873142823895439495700464445067862376964843411/77059849506459593832289630815436377951548685440249238894497229600*y^15 + 293026531896540068632219273293942874956987792340815892814628073/51373233004306395888193087210290918634365790293499492596331486400*y^14 + 5798125974638527575358330457378647290928754089689607081137586561/77059849506459593832289630815436377951548685440249238894497229600*y^13 + 31476416200126724408655012908312880685228314861100613593969855853/51373233004306395888193087210290918634365790293499492596331486400*y^12 + 578397902148429640507833162698207022725047878562714234540851909829/154119699012919187664579261630872755903097370880498477788994459200*y^11 + 89386606532139127767139135558121299636650068369668168676717094863/6164787960516767506583170465234910236123894835219939111559778368*y^10 + 1911126738439387405785709425664640216091307618684700375247209514661/38529924753229796916144815407718188975774342720124619447248614800*y^9 + 3687839027391292116006702554339656667783682552602498709777488462297/30823939802583837532915852326174551180619474176099695557798891840*y^8 + 28912876856697695288455414351381800507054713882214634159387773723079/154119699012919187664579261630872755903097370880498477788994459200*y^7 + 4610181686838944389751240476623911444883826792787482907117808955633/25686616502153197944096543605145459317182895146749746298165743200*y^6 + 12925418115563656339541022038899437743819421014884181898803631764033/154119699012919187664579261630872755903097370880498477788994459200*y^5 - 82509757066545893890581158472661589016983601404238940781931942107/3852992475322979691614481540771818897577434272012461944724861480*y^4 - 369741059259765574745067216371070151531235411236279511156312307353/6164787960516767506583170465234910236123894835219939111559778368*y^3 - 723616138014905427854245765221961682746857986339741616141624085949/19264962376614898458072407703859094487887171360062309723624307400*y^2 - 565248234081553674789069352517407037560146334935862813169023569307/77059849506459593832289630815436377951548685440249238894497229600*y + 276853339173429002591299673523665076832652350820508036386322584423/154119699012919187664579261630872755903097370880498477788994459200 1643771419083451131584889036539342680014197836347972220697/33687365904463210418487270301830110579911993635081634489397696*y^16 - 218190138746278846244996054526620601182131326705258683681/16843682952231605209243635150915055289955996817540817244698848*y^15 - 317203779951893623489336775056013679527957055444893298967379/33687365904463210418487270301830110579911993635081634489397696*y^14 - 2083016419140727707463807203559563070909906546938847465837981/16843682952231605209243635150915055289955996817540817244698848*y^13 - 33872118150347224041371964257975720475971893877109706587493419/33687365904463210418487270301830110579911993635081634489397696*y^12 - 207298564181238941140235202869803676951543439261793381963528725/33687365904463210418487270301830110579911993635081634489397696*y^11 - 798744439888890511308096013389462377647552576653023718721964267/33687365904463210418487270301830110579911993635081634489397696*y^10 - 171457107845112387996686050001531260268338283404831297198925981/2105460369028950651155454393864381911244499602192602155587356*y^9 - 6609072094223201922241333985655521980422036959469834387204203981/33687365904463210418487270301830110579911993635081634489397696*y^8 - 10459782902173328086158592453827147759587590654933926508746853147/33687365904463210418487270301830110579911993635081634489397696*y^7 - 5186190024003043326151460184554727095370599116329931664278148453/16843682952231605209243635150915055289955996817540817244698848*y^6 - 5471934791220160799440176896536495051155799108576244356215453113/33687365904463210418487270301830110579911993635081634489397696*y^5 + 49935893053270908059066146331324335351525183517636277010054319/4210920738057901302310908787728763822488999204385204311174712*y^4 + 3062617390095689021815424614925661769833313449733504412539879093/33687365904463210418487270301830110579911993635081634489397696*y^3 + 578794922400848457196982362961261120199925010323422282833679477/8421841476115802604621817575457527644977998408770408622349424*y^2 + 395306397212333532913635801819778052760260338185732463882701149/16843682952231605209243635150915055289955996817540817244698848*y + 108460507666174275573875213346646325773504344890606450758895185/33687365904463210418487270301830110579911993635081634489397696 # A Gluing Matrix {{1,0,-2,-2,0,-1,-4,-1},{0,0,-2,-2,0,-1,-4,-1},{-1,-2,-2,-1,-1,-1,-2,0},{-1,-2,-1,-2,-1,0,-2,-1},{0,0,-1,-1,1,-1,-2,-1},{-1,-2,-1,-1,-2,1,0,1},{-2,-4,-2,-2,-2,0,0,0},{-1,-2,0,-2,-2,2,0,0}} # 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,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,1},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {-2, -2, -2, -2, -1, 0, -2, 0} # f Combinatorial flattening {0, -2, -4, 2, 6, 6, 0, 0} # f' Combinatorial flattening {0, 0, 0, 0, -3, 0, -2, 0} # 1 Loop Invariant 551311236907535030376381744082369944785279865474381044446265/269498927235705683347898162414640884639295949080653075915181568*y^16 + 160790600984526024877750800949897348288058394884880684628587/134749463617852841673949081207320442319647974540326537957590784*y^15 - 106766330600890493722509738981134455602349993598635028210345163/269498927235705683347898162414640884639295949080653075915181568*y^14 - 743767606899045812704410722769273850070743592953406832045488413/134749463617852841673949081207320442319647974540326537957590784*y^13 - 12497225767578559726144987463983867898582231515614015767327799707/269498927235705683347898162414640884639295949080653075915181568*y^12 - 78518633120755983824782351838753176821485078991498004777929248941/269498927235705683347898162414640884639295949080653075915181568*y^11 - 321624669264353035618834700849359564171181173201221313930752577499/269498927235705683347898162414640884639295949080653075915181568*y^10 - 139404343499146878334117412500094348744275408374347342871676914129/33687365904463210418487270301830110579911993635081634489397696*y^9 - 2873798081684237573492908548549627456926593471962245909031625541509/269498927235705683347898162414640884639295949080653075915181568*y^8 - 4973288203072828839471363254385041439851643581590726750740802516363/269498927235705683347898162414640884639295949080653075915181568*y^7 - 2730211215458199020666741714907702276943208825544365491969463079585/134749463617852841673949081207320442319647974540326537957590784*y^6 - 3319249483180921798111753925110880436000790091212323462336601616577/269498927235705683347898162414640884639295949080653075915181568*y^5 - 24026294334164021593611305982315847436091350795702779223299703369/33687365904463210418487270301830110579911993635081634489397696*y^4 + 1505424146588005829774773567404199573139369076805658246890814408885/269498927235705683347898162414640884639295949080653075915181568*y^3 + 324148912290770798704788042671212309055451665927822333304576981699/67374731808926420836974540603660221159823987270163268978795392*y^2 + 232566800275070686504882508518130542804822870818712906314734235177/134749463617852841673949081207320442319647974540326537957590784*y + 42423013082813933025461702186301235114119729772154668300522381561/269498927235705683347898162414640884639295949080653075915181568 # 2 Loop Invariant -10101041135252814591157732929303908446081148543474380244608451979249584200408705373774543391189601980213239/1183769394537833566152757831811974789073764481742617394038021548548081979470820246607772619650551355529182258048*y^16 - 889452404823805005160119906455653249692150487321727324586420786321925215318666056746315072107311194599947/295942348634458391538189457952993697268441120435654348509505387137020494867705061651943154912637838882295564512*y^15 + 1953914260030194245468008702845226559564090852427154039370094414212375055562704720114410624031433465131713045/1183769394537833566152757831811974789073764481742617394038021548548081979470820246607772619650551355529182258048*y^14 + 3350310485618888350086687062848908108205859455153619864931968592843773857469999034425173714151507628368683177/147971174317229195769094728976496848634220560217827174254752693568510247433852530825971577456318919441147782256*y^13 + 223375426520270717280905986477663424904441298183403386474864620823316349962424128894388191750493214253175070825/1183769394537833566152757831811974789073764481742617394038021548548081979470820246607772619650551355529182258048*y^12 + 1394983064790580195213600663173397099771570608073719885539670354070071113757269405917883768893336086499845934711/1183769394537833566152757831811974789073764481742617394038021548548081979470820246607772619650551355529182258048*y^11 + 1878555963703765487498608556748584529639222325513006877732786737972235897696212792248683894618999449337246643101/394589798179277855384252610603991596357921493914205798012673849516027326490273415535924206550183785176394086016*y^10 + 9765354163651433591262946280265703175890891477990596612288619823550254336850533376777896916167972629236977478277/591884697268916783076378915905987394536882240871308697019010774274040989735410123303886309825275677764591129024*y^9 + 16564127812459329645933812068538470156272929757206096989339001080530947695496043733337356997325492053077665956311/394589798179277855384252610603991596357921493914205798012673849516027326490273415535924206550183785176394086016*y^8 + 84814584008770568374937893160354871677928847019073943621989964395579191130812002960179258968742554415601482111707/1183769394537833566152757831811974789073764481742617394038021548548081979470820246607772619650551355529182258048*y^7 + 23246571687983900970193710117764783062728841913599549833824160848076159084340942689608901070921265363375913607441/295942348634458391538189457952993697268441120435654348509505387137020494867705061651943154912637838882295564512*y^6 + 19215387146436614402096354589417562833617374376119425958110038786988915099337067221471093661453383440234260549957/394589798179277855384252610603991596357921493914205798012673849516027326490273415535924206550183785176394086016*y^5 + 598935566907041360847592552278725101726728577029029920631801019985249287223850496664363752683586237449094243169/147971174317229195769094728976496848634220560217827174254752693568510247433852530825971577456318919441147782256*y^4 - 8457845879875395280751685303080788510939977653965490277905059970223692392574351820104883534690399095388084320443/394589798179277855384252610603991596357921493914205798012673849516027326490273415535924206550183785176394086016*y^3 - 11500065062067199626297734155445338050963722223402147057234610771320183213624506861728373974938979334632162105867/591884697268916783076378915905987394536882240871308697019010774274040989735410123303886309825275677764591129024*y^2 - 4230955261424767084049123101516930562035418535994223887566160961420451559136508480736487284862202059436881302993/591884697268916783076378915905987394536882240871308697019010774274040989735410123303886309825275677764591129024*y + 768732463418132912690427695620884017572709410347690026875426225111148512046668112631466229081006777984296444201/394589798179277855384252610603991596357921493914205798012673849516027326490273415535924206550183785176394086016 # 3 Loop Invariant -388155160391026873202913687560513637259814955088403044522929862880627772786953663831625074619986239455617073389949260433946543854827/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^16 - 92541564922621102970061713264960873579903514180196157926359701286349918455425738387226592321964169024089554849214050858488668182775/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^15 + 75008474318010339737923445801364951637024510536670943989032067076348077951447652647392963916431205975259783286050901030018485965014065/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^14 + 1021552344120858099512009478608199389883926889773745991606284036814779508870820503375269340392219099415153778386692594646701220909743485/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^13 + 4241887561233101611593403392943591153490513142573402106866469105297581039703489002843947393990317114810105353515167906864577688475511999/67261950588423833900990406954600503102165521389231088723653850788287069808478446284050375604669986794226775591061755227465251959617252608*y^12 + 52833658536816436619388147051413651008000840685482207299182899171078893331397056314563073674294922327403231694416030968104261881140821809/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^11 + 35339562923416252728485109871878065634056213619597395412081696107399729329575057397066127776091386972228043944248231767917363298260232885/22420650196141277966996802318200167700721840463077029574551283596095689936159482094683458534889995598075591863687251742488417319872417536*y^10 + 367522683704595184598078034328094863131322014662073757949243056298982921794860711012084999047154308577643732655817177023011643861134857765/67261950588423833900990406954600503102165521389231088723653850788287069808478446284050375604669986794226775591061755227465251959617252608*y^9 + 309175524675330918151139914495744243739188698053376973924346941719855455564871657221496432454693060822200239598038273305681206764299226393/22420650196141277966996802318200167700721840463077029574551283596095689936159482094683458534889995598075591863687251742488417319872417536*y^8 + 393597000151411412443385193900657790829198998063695464340499373913022836543472591204843573677855979232951455780126779636677707186397901163/16815487647105958475247601738650125775541380347307772180913462697071767452119611571012593901167496698556693897765438806866312989904313152*y^7 + 3415659775661586656484470370444753543161456107551061050620067628141596130877910220344861936910947888614329676248582501230213416578092253327/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^6 + 86756826122412993767897675168144852274458623879734382793209899296414404938418946023840092777662217879331077778340574577134257109225346605/5605162549035319491749200579550041925180460115769257393637820899023922484039870523670864633722498899518897965921812935622104329968104384*y^5 + 138533846764931860158419502958879196013409139493289481987729428329873060848685888560308031839967708829809464687213474006698956297505511025/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^4 - 154628790266003597531065378379275117364272419964653913118804159636780101646272764848260506338765842048786127642448227755027312015798070675/22420650196141277966996802318200167700721840463077029574551283596095689936159482094683458534889995598075591863687251742488417319872417536*y^3 - 815369080979352872888083420203276343146445870771831698118197834557441430178961833960559595014254495523775343908429658069215870237458675741/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y^2 - 289329787592304634346216445042621031916434098198861302687650691632749333537129633083878094123397167101107546388455047992504401115909038221/134523901176847667801980813909201006204331042778462177447307701576574139616956892568100751209339973588453551182123510454930503919234505216*y - 6904275502603883235113266028266142194083143553304765527140695327166898744370186780539342254212838032333439725674045438996579884097942559/44841300392282555933993604636400335401443680926154059149102567192191379872318964189366917069779991196151183727374503484976834639744835072 # 4 Loop Invariant -1653783745137756545146434364918345873141447717869162946097381899705746158944128266314967689838666014468193197670552624386432052838767759070975507687400726939211196121900152197062989211/378172107605210056305241758238752565758586318066212649165636268420508155279788760468367322563525999576149009528324568424132340667937631761628540049745284503857472527754888084941404497264640*y^16 - 818106754514260512667939091580879800080692410861585960816274672187548118621774061952175004318415096777951933631609769292340641713424896747098070828410975057432678147917196977179094127/378172107605210056305241758238752565758586318066212649165636268420508155279788760468367322563525999576149009528324568424132340667937631761628540049745284503857472527754888084941404497264640*y^15 + 80167183811764665690914174633940874947126625646913675390312293558939058125773934282378029921067805476084501892612097796708776860962797981045308639302257005573158191394463814037234662333/94543026901302514076310439559688141439646579516553162291409067105127038819947190117091830640881499894037252382081142106033085166984407940407135012436321125964368131938722021235351124316160*y^14 + 2216439177868361035819794965896093786924339798872169725342927537547437251050123140508612078219683897521361399630607732531697149845682183696648450015095037359640407473666207135023662034061/189086053802605028152620879119376282879293159033106324582818134210254077639894380234183661281762999788074504764162284212066170333968815880814270024872642251928736263877444042470702248632320*y^13 + 18516836184461495651650850959787408626522915905101958820927161187177554647118998786597859780889295170453283565601567385159745675209868490675611863745076183247084472468602047311281971745173/189086053802605028152620879119376282879293159033106324582818134210254077639894380234183661281762999788074504764162284212066170333968815880814270024872642251928736263877444042470702248632320*y^12 + 28947919651863896239932211120921184211833820244286331191609866482620070867425180021146392738246273548932352922521469267486371408271776208342411590720492609867764794730526759166067216644397/47271513450651257038155219779844070719823289758276581145704533552563519409973595058545915320440749947018626191040571053016542583492203970203567506218160562982184065969361010617675562158080*y^11 + 313144756745006710559905757976578154782261450441309313271686443184857545017170167500714162761500145074832668635046385022004380261521212746117508096587624653419252518221775493368475000730759/126057369201736685435080586079584188586195439355404216388545422806836051759929586822789107521175333192049669842774856141377446889312543920542846683248428167952490842584962694980468165754880*y^10 + 161778505864385856711420499032538169815497422827540289004672431400152613434384359911213816456129154357117292405037816948837247218688292546865169869691244640007278506324253488729231714095235/18908605380260502815262087911937628287929315903310632458281813421025407763989438023418366128176299978807450476416228421206617033396881588081427002487264225192873626387744404247070224863232*y^9 + 137672365179733569864390668277705859277361545616305784833091621917821759037865192725578111046132033091261019603212007692907426936204137808543839446239824502813991447680715553360619546904959/6302868460086834271754029303979209429309771967770210819427271140341802587996479341139455376058766659602483492138742807068872344465627196027142334162421408397624542129248134749023408287744*y^8 + 13930579745368638346851096587633575342789124695750263810287514297559640575326902486282736235760537533484647923447791717571437886371774610919973218784251048703646191232754334817572882682002749/378172107605210056305241758238752565758586318066212649165636268420508155279788760468367322563525999576149009528324568424132340667937631761628540049745284503857472527754888084941404497264640*y^7 + 2960883850659326542394899359788597936586259412890351810526270619651150694100465112882012497553258225662131604810497464231274658942331349001207258544979446044477894748074708090318005055850229/75634421521042011261048351647750513151717263613242529833127253684101631055957752093673464512705199915229801905664913684826468133587526352325708009949056900771494505550977616988280899452928*y^6 + 2845352612354276737706415157750380576593364213486628944258757748446345694968371942901934734897840911396879187520394438953279458943895484737064675063483166381420528555375961299848369406869181/126057369201736685435080586079584188586195439355404216388545422806836051759929586822789107521175333192049669842774856141377446889312543920542846683248428167952490842584962694980468165754880*y^5 + 20624970637205032119608878482755871104598997427409870983838262660280779306700026668070950572404248207913088791364503168659889818680464991726618033953956151753374410403457033432809293021821/378172107605210056305241758238752565758586318066212649165636268420508155279788760468367322563525999576149009528324568424132340667937631761628540049745284503857472527754888084941404497264640*y^4 - 476986465057544069146457478330631015518222595296389969332872778885449154009871355958927273445530803816016813238760881429743174183768932982363901182217524768165312002111482755782507840930533/42019123067245561811693528693194729528731813118468072129515140935612017253309862274263035840391777730683223280924952047125815629770847973514282227749476055984163614194987564993489388584960*y^3 - 3468853675520174653338532826100198076931677264321591156527599522303493329123173274360091012351446855588746004058679863365531121154805230926630148377327971921126379071026769601596849133380731/378172107605210056305241758238752565758586318066212649165636268420508155279788760468367322563525999576149009528324568424132340667937631761628540049745284503857472527754888084941404497264640*y^2 - 557013738786729841685395265233244917139066656363621931940531152039607842897331191139823775936994986346841860008342336178480084295785494405682307806192180248773525885033430871519175353179657/189086053802605028152620879119376282879293159033106324582818134210254077639894380234183661281762999788074504764162284212066170333968815880814270024872642251928736263877444042470702248632320*y - 24899797674081232734250644341195310348220067431022289991847980814366639833286444102079132598255563161206523113405598472169059893013579512599586130222547663547643556830245038122941110891673/126057369201736685435080586079584188586195439355404216388545422806836051759929586822789107521175333192049669842774856141377446889312543920542846683248428167952490842584962694980468165754880