# Manifold: Census Knot K7_16

# Number of Tetrahedra: 7

# Number Field
x^32 + 8*x^31 - 27*x^30 - 40*x^29 + 334*x^28 - 337*x^27 + 33*x^26 - 1321*x^25 + 158*x^24 + 10214*x^23 - 24522*x^22 - 18257*x^21 + 43139*x^20 + 76381*x^19 + 67449*x^18 - 212881*x^17 - 173280*x^16 + 350340*x^15 + 135866*x^14 - 364570*x^13 - 101774*x^12 + 233436*x^11 + 85273*x^10 - 88154*x^9 - 39268*x^8 + 17627*x^7 + 8498*x^6 - 1413*x^5 - 886*x^4 - 4*x^3 + 47*x^2 + 3*x - 1 

# Approximate Field Generator
-0.185623542825725 - 0.196127069212990*I

# Shape Parameters
39908168646998353624254982695442118442874050835568339400457942740729796849878456101/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^31 + 337198848856244617959293024982845401835804408415419417312273436182882316497759309721/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^30 - 464891687158298329952174428267885610700054636042209783617698893863789442672193659423/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^29 - 1021788653686620418022044462608587502329188478627210377756990208283688053383287398685/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^28 + 3129867702098667916125163890348022524924850185527020180863055564901307139327663932302/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 - 7702140293517954796383477316839238182626875934652353686357470880037654685295768807149/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^26 - 854090063649500370798322167685840581589793050908832563997897037782683879974191712480/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^25 - 52664435978566406915682608179255040772640766031965004434059652869753455121303364682757/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^24 - 18094947032108998506435651775147898317053752755500048369259028722649915756346603078747/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^23 + 405029115706891884683617271287573633858502469873654099776863905766374279030864429045647/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^22 - 61443318833855987894305682900801564792964214134327618286827485204742330748469689936175/9061405433856836414737689829563326402020672008900896776435331965627235193444486532*y^21 - 281147269520940794299482373099312861239134759515453165446683289889961997023911481482245/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^20 + 1316988097422295143038414019859698316767066564284710768473349373767147976865570162354835/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^19 + 919809926475585708987619948850188500897163768381562193379543483250151004275233892604839/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^18 + 4192846657474671516388399617321479883279884020043953816278035144274018567494899168421981/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^17 - 1716045752465544603054014281550414246327062196958091400114219593427446950487997153401752/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^16 - 2555831980546909281029428018549059252108869980033550483410461924786853252367599846618257/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^15 + 2550853486993179050728878352973125903637152643154460381653684665926449493642858260178522/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^14 + 5221784562153399312588865064063349950812336873487497222664056861172876121917392230724313/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 - 2781325027559995761184738256845989389621877227608131708430868962916702773622359322215998/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^12 - 4619795219476005316720722483093846379812387894804766222746390372251052507848623978162485/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 + 3176901131613218506258834060941296574036565182985038811860391633157664786417295110220695/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 + 6380402276171025870158577678394596895411400330818137426594543192858454234140783480603859/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^9 - 1358983567030408917918267462810780053631050237641841019386549937999211262206372192790187/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^8 - 2346748602817820468859192892115836186100242377419357148430513619288508533996175370806871/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^7 - 25393532653294593011032596087280529956548244565895346571015840034151878571898532184759/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 + 185267384717956579991144133863725505781353713286128252208782271362838472329151095845253/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^5 + 70195830026277445377720702752678444683058549528372590694306498286728194923575554091261/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^4 - 17036595594269812787371685872487970372071438007068822107451811911340528346949832817401/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^3 - 6477909813441052879209505263375506646026468060967004209214431669096022230311460791165/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^2 - 31076726285153340089713730510708091460487394435218816970267269857844955635693404953/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 215859763848480279603542261674401226177536490734698488509594229195625448758905919913/117798270640138873391589967784323243226268736115711658093659315553154057514778324916

-109245015584339340855982122533974331601288984958312336116421365918466818860471296366/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^31 - 1650060705280409801186400554599250217222809410385195410759227731420504931134085944835/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^30 + 3319972610909491921993633264144013767076785202931866176422710330518362537336848866140/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^29 + 2889486402448563681447947974924032504877211833324957228875845448037039750939393572453/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^28 - 37804357475741741002026872795558164901292741680873271177070253401952898302680835771401/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 + 53716317468203389755088259699127285281835313434985450388502511312109603118008040108283/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^26 - 54779744223840374173493762742247107893072506873475283092242440914622909551140992871397/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^25 + 312573889105858581799403029056934563997646849750727575470513647571300921878574398049045/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^24 - 87167684111911246764344031025526996263467538102063093529280557654545352714775280133941/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^23 - 2155850842779392408320907525757748045785682921327602738101082237000568560144779206522373/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^22 + 3161827880570494819975034979487121808677615655039655077474613605356815784394157121083965/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^21 + 1173176240187174260335496194527800708676166672620072171963892925762036738561472504445579/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^20 - 9992208736104818826843213266587806481890577865763025574837791659634451008921731586018953/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^19 - 6119609956910486536521746788213722131435338671135695519818318646926894897379687783076949/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^18 - 4595542125336382987226019975807388693398208193303892605436793473478483169585741848052728/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^17 + 50744283876680513352889252263324602783212900135609175913948150180045122030557841664708627/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^16 + 15255136244813291000198379198048981764261578856644838009875107429163310838686464094671665/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^15 - 83700351322515882627721316927437942016320186093156462394358614645839853783258500896642811/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^14 + 7565801478102087420338339009099015657923169948209535595268396719762892605867621940859835/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 + 76798670766904971335148223301057659365016791686205707820965352575537548368507825537139921/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^12 - 12028866307169481153231558214132853874435206197423689445745304509364072690643807824877531/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 - 46132554532653317850539168793098119607975853909300274448997427334548891814122159804307379/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 + 1943060222594939124964815802364234996645675363137951463946952990807609414750603804661439/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^9 + 9342366269100517160545960929452282255669635391220277378130136281983763094075487069124733/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^8 + 287411332150285649153469075473711099554189328002479782068681253382844611515428999615727/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^7 - 2042998522068843238752776646434202759179667434854691522813969889615149998465392933970796/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 - 28628038711119191367734509412426131778732973339133624078986280425627359702154698121126/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^5 + 177186465583835189761650159544118229332219570197240653518542388873705077191833558012318/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^4 + 40290164019059676937953835445473538077831789845964703344513556017162037542787871694735/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^3 - 9095128281594835386334171424033662518579299916211242248632462099549881360711592212787/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^2 - 2671064550189018634612912369991987627962749861154401959748107956703719240774128735199/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 565450177920689375394292518113624264750233040733483751811639057378718547319169748803/58899135320069436695794983892161621613134368057855829046829657776577028757389162458

201484543817683750020981527271480180981721703086209591726071592794256955491066560819/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^31 + 1954251658858286957641522630058354432680445459408696309855137785806202241615945251635/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^30 - 1550460256426331277284832999858704524419246125774986590464263958235077923254887920839/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y^29 - 10306634430471218241600475394400707891777166329697333976457000682101608618750554446409/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y^28 + 15845514833758338141068855190555927866554767409320858680117171932423695624144891694936/1443028815341701199046977105357959729521792017417467811647326615526137204556034480221*y^27 + 64390005095794373872894211160022751491019249145166377900311528534282387988109166382361/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^26 - 8386695148088801794549084912357837780709461584633491493074973317056234111872480320476/206146973620243028435282443622565675645970288202495401663903802218019600650862068603*y^25 - 151260045823196246288842697213843610154798231166621139007447372802433671302155257136875/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^24 - 435607425585723732273031363288720949816564716188383949782675706975659992302001038584105/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^23 + 380825849135960362969076144156108649162709945403930920290798485507127678407214625121415/824587894480972113741129774490262702583881152809981606655615208872078402603448274412*y^22 - 1361556278269259345291307161708610744427415980140129530518511485909379026662590209835477/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^21 - 3999929853602319299996950884000244847048350400233644816306883384091270401186204109488187/1443028815341701199046977105357959729521792017417467811647326615526137204556034480221*y^20 + 11147943670237826339732108002402861387324361899249077759274973895557743530771545780589285/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^19 + 106986526187945760183733837583034518035628710670512443246416759863579410234834221377139/15857459509249463725790957201735821203536176015576569358761830939847661588527851431*y^18 + 27155750272560171194324123391651792972585048256982216801950570452006487415571539968627275/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^17 - 1860635276821310432588865375197977827692482220983043361575970387020590879398143767347857/206146973620243028435282443622565675645970288202495401663903802218019600650862068603*y^16 - 36753791910819164721483821468299239855421052043071273095275391302860032245818320949922047/1443028815341701199046977105357959729521792017417467811647326615526137204556034480221*y^15 + 19523015279595009794354812669935872123056690517900532229339128001132040599814419487913466/1443028815341701199046977105357959729521792017417467811647326615526137204556034480221*y^14 + 113579156014693407018973193155682156690341655983412461562306746570661339099737749540078837/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y^13 - 31786400506053510280036307232300045556932252752856402607669839736310869280086035032746709/1443028815341701199046977105357959729521792017417467811647326615526137204556034480221*y^12 - 105407752823700250651101162247225638613681757701907497476393536080292155729036192203570909/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y^11 + 56547451993926637936710036764556195040240353141575134167770838110486058968657749011166733/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y^10 + 21840683702869537656583894485053218135684662212107772728768179299046934385353849085281199/824587894480972113741129774490262702583881152809981606655615208872078402603448274412*y^9 - 39986235708584915099253675424640689713940963958193805182944969908961705850104065983217165/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^8 - 75458780368219995574624186091752848617994694949186334617158616151611586324584803670349081/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^7 + 7287729851202414870691910865681861081343498957405290181149820322524126799570572120914/206146973620243028435282443622565675645970288202495401663903802218019600650862068603*y^6 + 1289061445020954009954138818355585977885619976057068950087834171600851936642856272898395/412293947240486056870564887245131351291940576404990803327807604436039201301724137206*y^5 + 2434964138659159224746790452873868756687494746690612319905895538986583361843728083534219/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^4 - 1323446852339133531533614652877749482408125702894010638429752195396181608404569438940083/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884*y^3 - 44010797841456040151865707854890795288677922104768152177038105149310904550034197053965/824587894480972113741129774490262702583881152809981606655615208872078402603448274412*y^2 - 2334025212320292530052925005655838956946220677875664049912388593855845987107521922831/2886057630683402398093954210715919459043584034834935623294653231052274409112068960442*y + 19268652072966590302485184813951093154667788454022399685090637713273519605017300279935/5772115261366804796187908421431838918087168069669871246589306462104548818224137920884

-91422426278667280562934528942452192052985462053619196477310118745567354392465914933/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^31 - 377418494516960846363844011039998566248106921705553965444559496882736863005558384811/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^30 + 1135258017664424059207204757918887083650887126526887316877501341633452184322961787012/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^29 + 2103058399392625442374497058117411368498985299490638962861751403391173080701245865691/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^28 - 14670269835539139625269158924559308627841934902293186221759522177879996446539078818550/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 + 23433349108017097972211353543826965206013600013592143694934095926090073826488411649035/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^26 + 1599902292270825178403239452390525632489864107786248212558716159797153249475923631495/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^25 + 61373208270292889032405405480198539416219025403694430918868729330806094318805605284785/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^24 + 16503615352396463996338035762754408528020208072660724296033861906411721479162975020413/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^23 - 461863441893762616176782538847872966447046020704549398784699637445065325635410081476573/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^22 + 2003807398530978475379413469078218789242500711488241104602065548430684949518185044055883/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^21 + 2141373725816695085018616515057493591409992640249858868724742076180356429900563267889881/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^20 - 1643825526445694387555814349643595947054080320631540907229515051105667775171443258907939/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^19 - 298732798540116214066574042471568825692547649103840008632555596631815774661035434627774/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^18 - 8325640759380396555544922058006793222327864057651162855314900226280033152936297810140633/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^17 + 17038883307708525184169293327813569436956009209326490265355525560178918013540187170962905/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^16 + 19914540866182992687092777636909357774739378029141851206931180841931061396165525606182353/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^15 - 26070187375776581337538153848924697025939806073509331100590018378531949801254205395781371/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^14 - 18524340385530225607964064588820183855716076027595252825596001484101146428206343547284155/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 + 27225036013579696248774925896694504639421849744697935343303127658263471748873232876883839/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^12 + 16012213211745176615649189576089619911437064966534977795928966011768788865563657559329233/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 - 15962747329501417613963248720204179800778062675235355581604678384975940859988157630336539/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 - 5855550440749856201702124765561596644844885534489979581328304995307078664556565922118663/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^9 + 4355980790532080363199700748799680855076312352668227788176287540918152975656418523783777/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^8 + 2256635232128285298092837931398912995525066805489569531317697260184094226917647332626029/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^7 - 119188355026003007914703164515461091646041288745737019269508916625777798815863393092253/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 - 385899616850625023695207695765647291025717149896751097119308283997234441964864841123924/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^5 - 95081239724721629071098886383465945767147036164583918979572686226704299251423670031937/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^4 + 26092138057975239439187116502982052307219591243830037168956515628271881898962316547840/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^3 + 12549241166982466239853033804129144250656434087076560747878483457340068117262108915153/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^2 - 1289732788493291798124866020413569789580476357289978611064262691184651839440588175939/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y - 238077337157088281116319896905827036379049834904602311300873283014647553283856297496/29449567660034718347897491946080810806567184028927914523414828888288514378694581229

5770684166687236019286383531822097575770508746804588954410612508463040877580835279/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^31 + 35386686746871326707025030883931192279433176534680413766359812337531058363655291971/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^30 - 120119585320695661922435376213960794016576703271330465678103826666263075447367089485/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^29 + 37314953974751297503303431885372000895758498266198816345099847144194440431121964227/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^28 + 577791842138371227691193194531457822307780457668501539172543233867240908470289380981/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 - 5609976311569425549374450741129408534956392175458416243438088047678002692474702203683/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^26 + 84617956695822471508340730137601649541736353779089475897800983886931667986980288126/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^25 - 8617348483698145495764877771710845880047001847805854379539863560836304133559554136579/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^24 + 15492652347620319844650809379890574284385991633804540389476686462866206598099517474891/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^23 + 54634683993588360667730619909403704380976117743315165282192611176537040853953059360065/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^22 - 251361693730543183661125587796785074710664068946616856588377549891130232692468516198317/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^21 + 3386756030895896832879962098523034829166701725138350806620120383642824229049962581319/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^20 + 401631518739020503667347622075956036003026138471082948177850328598761119686043351723873/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^19 - 12149284705227799024688142278619930095822436115756452828894201167504648767759576891267/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^18 - 377084314312299570263575720849195392643789338310383812665989795284138280436506927111925/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^17 - 459610572525784960388468804975259800810083065692399341969879877174493497644186449505367/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^16 + 362305404247503207103966405494563397572852810626562196329337804652865530817279812249643/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^15 + 895928593546901537270813776136695560269616193463865301687725417627735410490020641953889/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^14 - 1608920912898045621076794806840894117038773173051488864905676685212440551191558216153401/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 - 774766099152722804433285520002773901894517295300144990748892890649489987393077875595666/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^12 + 1702225672186636973595126783849363083525484683022832455818389411176525984447511113188125/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 + 78226325230405203545679917918932581640060035828939389957289420739873935381750480127457/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^10 - 2061077820940467362784114801246490519577593327989195083443640426508573713943279091987503/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^9 - 1254309574349053388389591087368715331693063546693917586321341944173452646410377526716269/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^8 + 752261103602707818126328495001774159722656763934212933739248926724666036604332143484555/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^7 + 123025358250290267247133033180373969708299295596167996358857746646537974848760396837821/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 - 62205200121361283757755457764731037076117405104767146866453493342903869529613632327807/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^5 - 95153322629169218522445529859677582191944748338063083545260862158853412346829668849513/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^4 - 9732749675956745366545575752898033292993189049406938381876136762998014085296566019/9061405433856836414737689829563326402020672008900896776435331965627235193444486532*y^3 + 7789758659842512354515102379922117047655775433331515413817051466992783764848310111453/117798270640138873391589967784323243226268736115711658093659315553154057514778324916*y^2 + 533247192842290067392953728207949303810040725587038413423802523410771961020645613897/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 3364203352918619393691421361128841244418766186627398282001452003271337741760461303/9061405433856836414737689829563326402020672008900896776435331965627235193444486532

-43951943566607649921577709970339471757358866609609673044322636081783328798637786815/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^31 - 172954468894154431882801582748634431528414495707568459814014727580857234688942258098/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^30 + 613741121177412953188925826275053852551743615702883643026873502211368883624610892519/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^29 + 782539398597203054098535037164126158693159559443739351040945666211718889083566932302/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^28 - 7388432081077272839259354910869676029664187525030940267945376789445689752854663278497/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 + 16904900446831633846663816107755483720122067800170225699624660932474188383796038727993/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^26 - 4985206425548066493918562863372176292631262643757062485836433976668666608555073061005/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^25 + 29972884451900299200688756086303193068527424367519332402872928047988292782223292740184/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^24 - 14904066333706069821591342583584875022752247716157650352801613528410475485576588967129/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^23 - 16976244402937096392163908539224632596320799280357118606691704686827840789885481696067/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^22 + 1135219846825522261548111593446548286077416836380281820872650633697798949276964286619531/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^21 + 613697583703880749752945496363843884883768115325370445271251081991205336721560737808333/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^20 - 939954764823477745764572719515981786511546737587594332903597628779097224493935192282109/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^19 - 1515514658040844696528970001880523447489012589896005168810022841765076309091980652623294/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^18 - 209489301658120784237312366235894996902255461683793783902413231931810446895236301804251/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^17 + 722182739655870018353551923506800334908893114383291071624766349653249277441231772993703/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^16 + 6050170522962515681271769605738204739531508079930465724991600940422013239034305675465973/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^15 - 15403527997645766712073843873219688551184418664707794602831086268953627343243314871637339/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^14 - 3208756476797818295942256544676377979355476167843515861340622112433109634644094868033975/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 + 1170404080077016993212590344125248664083874166567237607018865413083263090217163487086995/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^12 + 1900157704143615020757690951304216716509598969584905402531228462555321821077886033157143/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 - 9271245540281311374032075587073079559788717142065297737070147732707690061729396832136441/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 - 1029694716172624694600946900158791455137388319462526201593409755539913056437766598540581/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^9 + 3435434532760956090427129707159012997604774884607836278750875208175660379479878644681405/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^8 + 457932167843866101871669317267836459362285043232186952022112608483989541435380423242081/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^7 - 342231077905960357787889091383830113878306458071016901328726524545804803045437332169985/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 - 77541156437697793831584500506124216242920738891277749256519547797539890867391679094789/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^5 + 56284667528082731361415538077151395869439558722708121105506665790869630320517156060847/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^4 + 6644141677356085560707821667367774909794927068347992702122147919398533512661040272231/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^3 - 1096122229562702783666225140521013472678580163674414787181832454028436972871412597733/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^2 - 902515024257856344275332486085008027038594579790121446748180199421673802691955448741/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 33062785569789854013099189527309604465447371380563063924525601881424783665547460050/29449567660034718347897491946080810806567184028927914523414828888288514378694581229

-43951943566607649921577709970339471757358866609609673044322636081783328798637786815/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^31 - 172954468894154431882801582748634431528414495707568459814014727580857234688942258098/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^30 + 613741121177412953188925826275053852551743615702883643026873502211368883624610892519/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^29 + 782539398597203054098535037164126158693159559443739351040945666211718889083566932302/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^28 - 7388432081077272839259354910869676029664187525030940267945376789445689752854663278497/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 + 16904900446831633846663816107755483720122067800170225699624660932474188383796038727993/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^26 - 4985206425548066493918562863372176292631262643757062485836433976668666608555073061005/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^25 + 29972884451900299200688756086303193068527424367519332402872928047988292782223292740184/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^24 - 14904066333706069821591342583584875022752247716157650352801613528410475485576588967129/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^23 - 16976244402937096392163908539224632596320799280357118606691704686827840789885481696067/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^22 + 1135219846825522261548111593446548286077416836380281820872650633697798949276964286619531/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^21 + 613697583703880749752945496363843884883768115325370445271251081991205336721560737808333/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^20 - 939954764823477745764572719515981786511546737587594332903597628779097224493935192282109/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^19 - 1515514658040844696528970001880523447489012589896005168810022841765076309091980652623294/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^18 - 209489301658120784237312366235894996902255461683793783902413231931810446895236301804251/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^17 + 722182739655870018353551923506800334908893114383291071624766349653249277441231772993703/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^16 + 6050170522962515681271769605738204739531508079930465724991600940422013239034305675465973/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^15 - 15403527997645766712073843873219688551184418664707794602831086268953627343243314871637339/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^14 - 3208756476797818295942256544676377979355476167843515861340622112433109634644094868033975/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 + 1170404080077016993212590344125248664083874166567237607018865413083263090217163487086995/4530702716928418207368844914781663201010336004450448388217665982813617596722243266*y^12 + 1900157704143615020757690951304216716509598969584905402531228462555321821077886033157143/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 - 9271245540281311374032075587073079559788717142065297737070147732707690061729396832136441/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 - 1029694716172624694600946900158791455137388319462526201593409755539913056437766598540581/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^9 + 3435434532760956090427129707159012997604774884607836278750875208175660379479878644681405/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^8 + 457932167843866101871669317267836459362285043232186952022112608483989541435380423242081/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^7 - 342231077905960357787889091383830113878306458071016901328726524545804803045437332169985/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^6 - 77541156437697793831584500506124216242920738891277749256519547797539890867391679094789/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^5 + 56284667528082731361415538077151395869439558722708121105506665790869630320517156060847/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^4 + 6644141677356085560707821667367774909794927068347992702122147919398533512661040272231/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^3 - 1096122229562702783666225140521013472678580163674414787181832454028436972871412597733/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^2 - 902515024257856344275332486085008027038594579790121446748180199421673802691955448741/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 62512353229824572360996681473390415272014555409490978447940430769713298044242041279/29449567660034718347897491946080810806567184028927914523414828888288514378694581229


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

# B Gluing Matrix
{{2,0,0,0,0,0,0},{0,1,0,0,0,0,0},{0,0,2,0,0,0,0},{0,0,0,1,0,0,0},{0,0,0,0,1,0,0},{0,0,0,0,0,1,0},{0,0,0,0,0,0,2}}

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

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

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

# 1 Loop Invariant
-486191993151890441619419794512730062910803811613232926751873386782326421931770549808/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^31 - 7286516387979684831409214967558422976838208687688301558576018203871065343419944021775/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^30 + 15057158196063173922338697708077248081538565777332967821820886060132719788038220717125/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^29 + 25001699715623045497112068137845821757425470544125827517073400694849499338755258771583/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^28 - 170963899805636712758213205569025712511224746687202117989550744374461147322153028355003/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^27 + 246985385731493972168207462489810315712542423217645590161060310494718522404884218594462/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^26 - 113194518671272783788465242142478320426600838573202538323514218131353098894591837624666/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^25 + 1344657275730530636518604578588907319073417681538613676833241647902073491053749338467629/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^24 - 414729600244982478131422350792271346996774619030320909724606040809076724093050963387945/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^23 - 9736228510537857388855520691298641770840527005638019049991781035383587323699045920788369/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^22 + 14395030714435419828640081518236588407436151102720681545128488987528537906786654927939666/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^21 + 2444312422219674619000390536210326230991641161136836050934889336654868572130304432048295/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^20 - 48486518603838549833847141839867720264213084282908833171161361234126480810575621108867617/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^19 - 2035306156912174495305942048049425637044880796001480438822224831336106488498292235883664/2265351358464209103684422457390831600505168002225224194108832991406808798361121633*y^18 - 31810288282065938013308921157459028013752995897710068627545440262864621744777839079112211/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^17 + 118069196642686072853125799717742531763238064195941400682286758456623427219793032894081166/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^16 + 30655564230988246588526166391793844475923199886982300822415905103669340729293981020312969/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^15 - 203199523564151579098943363942472754380599895013837604153263315598541109919679689088035508/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^14 + 43352322034558062253766031816663293750576127931569355876872263575023295512487863836281811/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^13 + 388628581553036313328973893259730583301841178851821096632052319068918256475780628447747385/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^12 - 74193500044012417694591785579789736783297764826172638044879016987353124579816615637614921/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^11 - 247020067699678672823252887085931015040336447295127821683316949427444115377666207824299237/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^10 + 24122797250542175817688571130777993930455218678302795678658792880779571007255769555115043/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^9 + 108847548032815227078769483814461453868798126762006663414446023556697814466127809258519391/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^8 - 1136940952303454387954143970930536420911854743498901531355234736470065281745457705424782/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^7 - 28072970690196122647014812018281077256542383693561338836142336373837120462260523002336729/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^6 - 151774235149022848835063067336690635768982834889176107860289910146855699001753107301961/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^5 + 1706141847017641100615063979961790043077006254554247262967684444678619071067132877431387/29449567660034718347897491946080810806567184028927914523414828888288514378694581229*y^4 + 186058998341316715087503888847400374001280439319697179614448750181684251507289190144047/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^3 - 167447220842705953354934403051495666674853856598589227959536824554105015251657239613435/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y^2 - 28612589434569548226084053915046861891240152376662856814708494314856699913457086640917/58899135320069436695794983892161621613134368057855829046829657776577028757389162458*y + 6863820420922030018976169980571619951862270481820554943530446473589073672756331894733/58899135320069436695794983892161621613134368057855829046829657776577028757389162458

# 2 Loop Invariant
28894023072270328035866210876772521186660644987053646887123719510220540630233954805163417515526956672144258858054258737533439679160364901486347182931132254679198399208149858161481091107560361784762671/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^31 + 207374844940925771785581381840897190182476621510082107370529480586050921326497721794199178114767709754433477852882875696474930155347932098029747873528972847935443449174275022069398155319223801622989879/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^30 - 160321542048478410637994251450139315475055531186318393962778846344038935684194554075226751402141473059090216185693365658108592600400873790259052901970463090998524603815315842515466721732738152354712819/1350042302894199270886488924971952894261487273902663764711108840796656164972736024576787230880343743181087716898887054278589772949554543877079914163791143167441755144028441821393248121633527755343854752*y^29 - 73792333892085045825210909366081594820335780369338714695244453790903037141963731520584897598939596400127027071086042975818914899753153770367023417147015502857197721699777127950330387277598993711851671/1350042302894199270886488924971952894261487273902663764711108840796656164972736024576787230880343743181087716898887054278589772949554543877079914163791143167441755144028441821393248121633527755343854752*y^28 + 867318462663348792913762687333457112819987568705949584417715703734445827470429516529454754014805347678361420317357442210193877216732112511631471453028449781440138253491262111020547055456562500816984075/675021151447099635443244462485976447130743636951331882355554420398328082486368012288393615440171871590543858449443527139294886474777271938539957081895571583720877572014220910696624060816763877671927376*y^27 - 18072594608976602160893140421638346699876192264713375711791870641441708076501929665495725357771456080915402736196167238001097729062779986189894395436644944853502257611020249237363273527530833799735050463/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^26 + 2878722119206211079413789043390399400851722120220952339491253338377049984850920511917517330885580652585765245216386635067415619506479241908440703823989704809468034172920880126402503608177432473306036919/2025063454341298906329733387457929341392230910853995647066663261194984247459104036865180846320515614771631575348330581417884659424331815815619871245686714751162632716042662732089872182450291633015782128*y^25 - 40803162421265043779755253897636976122865235546680675604098018795074184699049205379955273401542788359055020690674679941866268897941181865595974716087515963341925866558025043870928854854440787427110384991/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^24 + 36594380564448756359172716197820873717007962796450810784377983487172830234255262546674161496215374920653987741759041592142903624556055520064275417367796980679821153713648516879641345337814119724645772647/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^23 + 278969079764066777064658273201376897603904246936469226144978115554173516705786683932936494956280720044137685977904037150502071966274078406890845891227574547954758762625162715541060857153519293633344525813/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^22 - 954375826597474325054079269702716368246274647541764768149024417788265978551286591786745048613579557542468121389565339516303777745141141980509600067339415577697792702213972076201530862269927426123220131437/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^21 + 16877393051299633456203626058338639988239779057243431661534573882571715034466726614051794788751431229142022002522205704879496691458279657659020893925739721518515895060229096781143035931372979659732052949/1012531727170649453164866693728964670696115455426997823533331630597492123729552018432590423160257807385815787674165290708942329712165907907809935622843357375581316358021331366044936091225145816507891064*y^20 + 503472317432358230410992109477325179522896920196979769824403331889520612522752438701524220002627532018618135828691012787326658154940765545015504040448514877419502211378923375157594320698850045735368149807/2700084605788398541772977849943905788522974547805327529422217681593312329945472049153574461760687486362175433797774108557179545899109087754159828327582286334883510288056883642786496243267055510687709504*y^19 + 20554609274518641160644731593392087785577206535631614406866364703653972240904675308187435354010568369208843254243237180613930310678711946714993379870942232487359720735733664381176621600117528245226828399/168755287861774908860811115621494111782685909237832970588888605099582020621592003072098403860042967897635964612360881784823721618694317984634989270473892895930219393003555227674156015204190969417981844*y^18 + 16910760099331126265751765967268426570664784381781666592812223286931262531414173940803012387849540528424240976226295857951323633962591973416807323402683420351013616996450614737810338043272244950974593801/426329148282378717122049134201669335029943349653472767803508054988417736307179797234774915014845392583501384283859069772186244089333013855919972893828782052876343729693192154124183617357956133266480448*y^17 - 293887779947048511005895629418791769142337960881653941836530865799261048306991464912559506280055914301532682671436793840182058181550467079646125423326960247080642156774082284673039689173263313854262151943/337510575723549817721622231242988223565371818475665941177777210199164041243184006144196807720085935795271929224721763569647443237388635969269978540947785791860438786007110455348312030408381938835963688*y^16 + 261011059971246537965008738622231606425194683519276549033738416915211007935450380947429921156171288813496988195734254234066268696858433348030966513944021451726264594904763960475621030557019933674168870843/2025063454341298906329733387457929341392230910853995647066663261194984247459104036865180846320515614771631575348330581417884659424331815815619871245686714751162632716042662732089872182450291633015782128*y^15 + 3271670543155586866700498625655326104760837375415756130919464170664793614817734620358396156756877990937119405432062731891240685514721689094433503165267221070523947876972438872496520531641164744313343424799/2025063454341298906329733387457929341392230910853995647066663261194984247459104036865180846320515614771631575348330581417884659424331815815619871245686714751162632716042662732089872182450291633015782128*y^14 - 3080024637737255954963743223698262964232098375763247205085693535120603050220707355578921848361357458730020538800793988715273979219274173434248423165303258013422441892848424243303986570616703247693346906821/4050126908682597812659466774915858682784461821707991294133326522389968494918208073730361692641031229543263150696661162835769318848663631631239742491373429502325265432085325464179744364900583266031564256*y^13 - 1533246339218369345378040896343322025009786670743446575926289903695466739968037033880920186503693316892179447944718132671959699147079167723501354430607827394831241297843430987773420890615020936801251302921/1012531727170649453164866693728964670696115455426997823533331630597492123729552018432590423160257807385815787674165290708942329712165907907809935622843357375581316358021331366044936091225145816507891064*y^12 + 1202056126943805291622188725567708971345777545661336091370512332905115648301021940716547737290358437554536037278711454264109284864975312067988119727747273218946594391779485561754694608719092504534420531173/1350042302894199270886488924971952894261487273902663764711108840796656164972736024576787230880343743181087716898887054278589772949554543877079914163791143167441755144028441821393248121633527755343854752*y^11 + 1295065583372206067993078724075835275588672058134724332279241474938716428650311827598050429278794476881672961263829460340013832464601727427124949069665174181931247299149932816326428698381816966962756430549/1350042302894199270886488924971952894261487273902663764711108840796656164972736024576787230880343743181087716898887054278589772949554543877079914163791143167441755144028441821393248121633527755343854752*y^10 - 1498540467927409101565306998907268895008801982751929271155588140056986795565305362454115367796219087486008756732649172852995541569642493061439404640853169823984251108737688525784175116459913006495664799393/2700084605788398541772977849943905788522974547805327529422217681593312329945472049153574461760687486362175433797774108557179545899109087754159828327582286334883510288056883642786496243267055510687709504*y^9 - 317946972573865766220073768737201149695854065396892674234236069548141775499806771049110225836044065818648109125987268821634553801095321082479170567540504828323860207748476787906199213465970589439673817713/623096447489630432716841042294747489659147972570460199097434849598456691525878165189286414252466343006655869337947871205502972130563635635575344998672835308050040835705434686796883748446243579389471424*y^8 + 611001712145787347005903286181673313959957813228898697651258170012235885511382281137663830434479881612612890100110340351034253876249930648431768917157636076823239074205589885440373089322602267627965154597/2700084605788398541772977849943905788522974547805327529422217681593312329945472049153574461760687486362175433797774108557179545899109087754159828327582286334883510288056883642786496243267055510687709504*y^7 + 66154568359755700528278246729527762300878392892682460345951764641329660312367984994869241820423204261762683425487036642145527065468057755915816543539630509403149137309921142670572464800226503458116814509/337510575723549817721622231242988223565371818475665941177777210199164041243184006144196807720085935795271929224721763569647443237388635969269978540947785791860438786007110455348312030408381938835963688*y^6 - 172147577682298645668908470702061188565231345873809541494108172297337656273063863248367771010213806144740929720385137437857538331456969873640319278863948006383420009878786760792814350965839120969133869105/4050126908682597812659466774915858682784461821707991294133326522389968494918208073730361692641031229543263150696661162835769318848663631631239742491373429502325265432085325464179744364900583266031564256*y^5 - 25912200045460144727603717470415734418119252526907920493717545460952440690203075095662341961091685809808989803872947938273914680844643127652243949090598718161140775216713025079214334582613885888317088513/623096447489630432716841042294747489659147972570460199097434849598456691525878165189286414252466343006655869337947871205502972130563635635575344998672835308050040835705434686796883748446243579389471424*y^4 - 165363565017422839786509880674118216120117491072672087175860266557756663485415633164625186830999511030694681731674446301972255807038322457966807468090713830191550610023767254789581299140854880751911463/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^3 + 30491413368427041651344753425191758716335483840978331255461699755079449831071575723831649617337576246880236924006476342761065687668528327448262012666615979102148589959240510927624195198441769931546440965/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512*y^2 + 496071890386477702809802954010418471504752273767958639963585950231869084435090482608514770908196881197856291214800410012680253601268356697341517655458082174198451463635746644720150652072834807486525125/1350042302894199270886488924971952894261487273902663764711108840796656164972736024576787230880343743181087716898887054278589772949554543877079914163791143167441755144028441821393248121633527755343854752*y + 1876372366220231408635860379546581329233765517551405068432183165097257540265905089600991405350570509678300371840157949940976954514326160780948904424066438501552951979452670276360272477619580947920945367/8100253817365195625318933549831717365568923643415982588266653044779936989836416147460723385282062459086526301393322325671538637697327263262479484982746859004650530864170650928359488729801166532063128512

# 3 Loop Invariant
-914716770584745051992131599013142137596795798177319080427909942300564707374748759305930404109337600702856953645377474185097031361497380589296933142134044106983713159976812628585773849381588420200090452855874094339871397445141877231300019183246045718498450623/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^31 - 6643082335231896137087842977327120405720331891957302444534122203584720456647053259048945923005028335515059207108477356988708829814756762349063425233048440349568918907414967568023602746654369129241718028510353443798249402979399624972030483131947726856565593029/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^30 + 15545668961293426791587362737565581486980964035358560928867931725308053455267973318300312224382636621189485122711812983633666977540027035676135405017647863889144751228573288063079064536571290777899163144671170557063733601124707542108768993476146255992762640249/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^29 + 13452256928495192923964065065560786632209743942019797716265402691016692474750355677647827266166250714791623640898165739492720469365269283092786350567619808643520692481357205777825371099092695312625482501912956251681425776371145759633336096177145275828319328501/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^28 - 88644299720714688334772678448037638020921077523117152743320099547081065972835428256394159227577498371531145591065431361950084279898664183237327981709020011656505036847184976120004783490056220211002155754039793987013251234120744653202034783946474042549581333815/102196638367147416238417593459318940727715770318817457728978349824263863742707608289197002277011531406141044161487401774554178188893034700510963001126400631734862501302410660142510175714943746787161916936665901812854562906336002268319086360127609895281414769088*y^27 + 481882063459142330386823632497496414749265522144156622650028627550982768293420948668191448452852725084176648042197474215788649289996642129580048055696427403399304844410675812068427205938097048211583342216143768196737731532676880017163494842957731497281456615975/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^26 + 22187638441576879698567156646984255205819772060210459012455490638489206669208425694797028484953385360725489465578032050113948514426566433290118331683516675765578760681408457469929083989052970691473280679581239205549922523310405630152211607132480205179851842193/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^25 + 1061896106233148598034842558473586736145918470109243174408166301889058303326690367928218549974493935810637958498687251216814696768023790411495172438169568519186942031336382721625365533067070391066728549961285209477086640446301199121484829526199652055719351822605/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^24 - 1073835102735005117029779558128592193227101219178534750378839738583311489572606965610569628468776735473738658357904726108663851841493011399034792547727480655886886960216191503181908331502863419741414918454414332502417479968844222581928617202315769869943303889487/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^23 - 10609226460544026425250588012244803434538336430626839049553024581702559328765673836745836525544589239666896544825458069022512464456101082784272516415617083935332043950149747971684102635956810836013258126692555367378081254463797779531800838142424742940320805647091/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^22 + 28731872189563986748326574894037947985966865361564411922513032960853123481969971405864502050213636429478651056302890369780152982016804224746063811736099738908096976651051140477303575205645073457114789340636987799328571198912404473751147607184052379988772060473221/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^21 + 4952500403421798661503748679681177125555120776363974611933671743691369549629467237762141253857765840201076193311068718884035275078956129625215582976995247571638936601966106681331156718582441468883108711830060856706484849912770228863554046916079617160675122051719/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^20 - 70698475787465444373654723162915164719150001712167076190457939236183802301946719476571985091874241305637461951535908775218340172062255550877659851887337161528182935936456363040475492006290706766823032143240641116182426267706239012392857762422151602363773532413687/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^19 - 4305714217480908466613254620084415207925323903791074389177296932779519669146699573379326716338652449786695516741930813047493203059927442983282716119113348114515178879562573810925631098056922966089736610640109010501636453650312622972156764131660909652501161558917/25549159591786854059604398364829735181928942579704364432244587456065965935676902072299250569252882851535261040371850443638544547223258675127740750281600157933715625325602665035627543928735936696790479234166475453213640726584000567079771590031902473820353692272*y^18 + 15126512751044834322701567991394152161865657863689071914974483007243957551114865570317173087530691034044937314527895029484593048161990628143340422053933154473016776076235879281152967423997672289369640093313586843493924179465834155713863257207902777262279680836349/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^17 + 165153385645618061407630571288553364124838307310359351336048389414857921919912877827432956293573184148947691861964770893042198171257048326322034193577838066941319585135773067088093331868476245255843081013650740226698717489775739034440446640611956510682370356232489/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^16 + 67732058376695054066883278127542623747027005985864380612846906313688263178609477412847366357645147969596463367546000222211119763859502825042877851398075377969423831588977304666275301271401893799411475022892828471558379365325002744293204396841235737546938132232351/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^15 - 15217773886257141492325664316231638100694608375893101858922634104489904635958363720068920837258169224555299218402563975239678864564350405051208735021661911334276554195100485730662859901719448063170769564711919751113198603225238532625333315876002565573602591266595/10757540880752359604043957206244099023970081086191311339892457876238301446600800872547052871264371726962215174893410713110966125146635231632732947486989540182617105400253753699211597443678289135490728098596410717142585569088000238770430143171327357398043659904*y^14 - 34263254859564234111307880103296266905759379914625237678587615205059307670072692699628735905180703192418354082601315897355478093729279762165146238915907387606375612422858082770593095784507135909977885170326623730659885243602963873464167864118387044700007302543847/102196638367147416238417593459318940727715770318817457728978349824263863742707608289197002277011531406141044161487401774554178188893034700510963001126400631734862501302410660142510175714943746787161916936665901812854562906336002268319086360127609895281414769088*y^13 + 309477940986397831031160409893672525767498427105114537618915292137631951850670042844112888322375585901403749604218432881803848215185596044202520546247706333302574421685213529215348136941840295389083935658115333612360814929595429109399133025327824589092812522957341/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^12 + 10869230270712802055383818575356797205884229344168784358882939713056877651143449665515065336615653196016423961707424023085709374131938200629191188989956462175193926002702322981657278933608799273492849480326474173577233373322701153033669600517294526135469485997725/51098319183573708119208796729659470363857885159408728864489174912131931871353804144598501138505765703070522080743700887277089094446517350255481500563200315867431250651205330071255087857471873393580958468332950906427281453168001134159543180063804947640707384544*y^11 - 60737311638540934056895457812066154507621643128572217173520809626641004536558264949193290720609458023762043697805897160962440489116275147830219820086557014369517089570809955218513067699345347930917268263741957016702480031071870951437662220940345216465496825224203/51098319183573708119208796729659470363857885159408728864489174912131931871353804144598501138505765703070522080743700887277089094446517350255481500563200315867431250651205330071255087857471873393580958468332950906427281453168001134159543180063804947640707384544*y^10 - 137982330851346916935710034371711286899952133084192705557847457146161589204783274718991592346658178666813599422856608919268142305370922973669861808778202057633902407836394049609958760193932669588734247185091828355231533031263784959153631454978646163272853036661251/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^9 + 225801981685707167268941494020445803930117702685533359337123864518044619237716037711785765941375692550415442462709125915664695406763295935972265148729672275404551287663817482027334945984415814181249761761362049442981255197905975491910841506538044902050486035393437/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^8 + 8721415425359524631567195944001708772143000386721586021721035030388316504864428974397161155300135401555082682064501909475400966170336784928509163261215316434644379262084848508251108618050673787972812771411603921519032812308204509175781123028101352714364414008067/31445119497583820381051567218251981762374083175020756224301030715158111920833110242829846854465086586504936665073046699862824058120933754003373231115815578995342308093049433890003130989213460549895974442051046711647557817334154544098180418500803044701973775104*y^7 - 516843984797011701174840760012925324575082108380858923022598610570735439179282331707301677821700160668512320069932548667432094662272215822398787481573939473891455071949182518405660712805644710345773234842191074662607468334099555098718626225266196123711911739395/5378770440376179802021978603122049511985040543095655669946228938119150723300400436273526435632185863481107587446705356555483062573317615816366473743494770091308552700126876849605798721839144567745364049298205358571292784544000119385215071585663678699021829952*y^6 - 16452834009738032570865061493296545965306109835962376648263103516296776343592818356261060460576475768766289833302095439965147476185753353564827759230960305856816012344658668415973663190959883102135964704839101755537391118736955937039662409599034242082053139568493/204393276734294832476835186918637881455431540637634915457956699648527727485415216578394004554023062812282088322974803549108356377786069401021926002252801263469725002604821320285020351429887493574323833873331803625709125812672004536638172720255219790562829538176*y^5 - 2103184780443294056712064809820453925166932619876693112871062462997607620582940715269428729456353492092538701504801472685913721024880456980386181143070405371609506456945436805086503928727648898924551601903361030531512587264778198197340990003759698573228611801135/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^4 + 2469382642414045172368036446755147314181018317473010704774824514307874521922530824385988509117772595519302544302374210616360963832380135566776403235202263548795033936814360403456367729518175222452120536634827873670767616638347159263552471600762516896533805277573/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^3 + 683369296801147625807914141278054255150125451397823416704346425847656030776256057609627394627064744240420476268773871251617498760736213037114569780351231813312652970222366546536664859126273735142198385440900252541342520948443150167051401161415467191855864729251/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352*y^2 + 1924571957365619667094448425420446038534364602664231246376177650320743521513331743898592292772853025780436629847591461767853764100035414615311324481069494006679169535555938367256166190273902334841584097699428405251708151617219110371462087932706309910674737653/102196638367147416238417593459318940727715770318817457728978349824263863742707608289197002277011531406141044161487401774554178188893034700510963001126400631734862501302410660142510175714943746787161916936665901812854562906336002268319086360127609895281414769088*y - 9229341283797269241411018305550827241651518984345872820471119656808946587602041726753477347037312673369211128816779729774238343919351618658176565064548360328411111854523543364555454685052775018650823018820300945875569482390532885449449925773210994024998184921/408786553468589664953670373837275762910863081275269830915913399297055454970830433156788009108046125624564176645949607098216712755572138802043852004505602526939450005209642640570040702859774987148647667746663607251418251625344009073276345440510439581125659076352