# Manifold: Census Knot K8_239

# Number of Tetrahedra: 8

# Number Field
x^24 + 30*x^23 + 486*x^22 + 4674*x^21 + 30515*x^20 + 138234*x^19 + 460573*x^18 + 1168521*x^17 + 2150886*x^16 + 2665352*x^15 + 1423919*x^14 - 2965204*x^13 - 5449494*x^12 - 2794498*x^11 - 722143*x^10 + 345975*x^9 + 1447694*x^8 + 1463388*x^7 + 541181*x^6 + 245041*x^5 + 205325*x^4 - 114688*x^3 - 95848*x^2 + 11647*x + 5921 

# Approximate Field Generator
0.0302694175379867 + 0.762512987203685*I

# Shape Parameters
3574929842492698483600165204907058013499236864752603262479716/61852160284564364353940716135663609765150671846914358690524328311*y^23 + 105194026214290133651824563066828211423226556359488053849662573/61852160284564364353940716135663609765150671846914358690524328311*y^22 + 1677122276888442109563754504838058702717105917666558815152009104/61852160284564364353940716135663609765150671846914358690524328311*y^21 + 15749998335767150311678179405088070706739642168417860950320185552/61852160284564364353940716135663609765150671846914358690524328311*y^20 + 100110909380451306617108547013409135858820819557785958297476132351/61852160284564364353940716135663609765150671846914358690524328311*y^19 + 437350664180545494973083407381239349321290976451253624035549759753/61852160284564364353940716135663609765150671846914358690524328311*y^18 + 48270466915898075494879431470584354616555315968980821549352903295/2132833113260840150135886763298745164315540408514288230707735459*y^17 + 3394601004974547313810155501050002310482223851398902856154072759604/61852160284564364353940716135663609765150671846914358690524328311*y^16 + 5813615384871726672258003355046894696915096754265702408471197471115/61852160284564364353940716135663609765150671846914358690524328311*y^15 + 6389184126768884190104037848793440627190309940737510956715393928839/61852160284564364353940716135663609765150671846914358690524328311*y^14 + 1827678458165599315952860399483116915468843894483762084804767449931/61852160284564364353940716135663609765150671846914358690524328311*y^13 - 649259334018306913228691301661110731853772772210945549690112705469/3638362369680256726702395066803741750891215990994962275913195783*y^12 - 12528719457570030798097895304634714514807611547038649123168604918930/61852160284564364353940716135663609765150671846914358690524328311*y^11 - 2693967211703714742910050738453392954025995102172770317194834465234/61852160284564364353940716135663609765150671846914358690524328311*y^10 - 1445782607705538280564956400730328568527736760791153219403363765181/61852160284564364353940716135663609765150671846914358690524328311*y^9 + 1597884616354112775684833444481910447361468640457676992731021561364/61852160284564364353940716135663609765150671846914358690524328311*y^8 + 3787207951312175758298646026939086636533277325333045269749564085983/61852160284564364353940716135663609765150671846914358690524328311*y^7 + 2705526550457710362058386381825614027022822696234856142729914960098/61852160284564364353940716135663609765150671846914358690524328311*y^6 + 223765843865037708246450483280668726308827742956107258979099562424/61852160284564364353940716135663609765150671846914358690524328311*y^5 + 716300347664537644670343841783441958506366756141781922818922801032/61852160284564364353940716135663609765150671846914358690524328311*y^4 + 306228265512456517516570042370139010705248690378799102908457295657/61852160284564364353940716135663609765150671846914358690524328311*y^3 - 577315551630624864193279248208788586821825242830255790074159888408/61852160284564364353940716135663609765150671846914358690524328311*y^2 + 36896762691911272910404982096708789440695964195048612660596321204/61852160284564364353940716135663609765150671846914358690524328311*y + 72381385853996174200727599589041324274923157188866913844666893689/61852160284564364353940716135663609765150671846914358690524328311

-10529225569431809846786883453377714509772485341952555154142565378/366226641044905601339682980239264233419457128005579917806594547929431*y^23 - 294709607485555027682209925423076744795245578782376490707134562904/366226641044905601339682980239264233419457128005579917806594547929431*y^22 - 4494349797529047704185972120422879411912503435984413038069434678975/366226641044905601339682980239264233419457128005579917806594547929431*y^21 - 39283359310067813493154902837941292039888612349782548045947304671988/366226641044905601339682980239264233419457128005579917806594547929431*y^20 - 228043578105134380479255248322294491611101968930480065841814563856278/366226641044905601339682980239264233419457128005579917806594547929431*y^19 - 862740272923184615880838340427819494123811666157818850098387202812181/366226641044905601339682980239264233419457128005579917806594547929431*y^18 - 77928404330238175200984428195455721295795828270042809554979780563589/12628504863617434528954585525491870117912314758813100614020501652739*y^17 - 4015147587956085228827003541441811389819757594546013813855986966184783/366226641044905601339682980239264233419457128005579917806594547929431*y^16 - 2547731317678613109046121881784715170701254483078059733984821066009624/366226641044905601339682980239264233419457128005579917806594547929431*y^15 + 6358324263889280387686524479005465376383174530863297175353765311088859/366226641044905601339682980239264233419457128005579917806594547929431*y^14 + 22837594870998790044379075802655820086553097603479061992180319902179337/366226641044905601339682980239264233419457128005579917806594547929431*y^13 + 2473116819187058460864043552284055754807437489713967038671363500008739/21542743590876800078804881190544954907026889882681171635682032231143*y^12 - 7973545219015487795654339693421287981487105696378748597988689422374401/366226641044905601339682980239264233419457128005579917806594547929431*y^11 - 44758648112946098602311385862045028200045677226900109985140219061294286/366226641044905601339682980239264233419457128005579917806594547929431*y^10 - 8347373320111499534582190044709996791557285117671329011432640278885460/366226641044905601339682980239264233419457128005579917806594547929431*y^9 - 12203327636608662570967198851506630231771264976826453481541790910290251/366226641044905601339682980239264233419457128005579917806594547929431*y^8 - 5782021868080312779504391629376805270683312574482756907360888377502088/366226641044905601339682980239264233419457128005579917806594547929431*y^7 + 7015715932119715316816519322434825093886597263707695260276788489724679/366226641044905601339682980239264233419457128005579917806594547929431*y^6 + 10321205882369426769053733392607055737888949794563357470229798804908840/366226641044905601339682980239264233419457128005579917806594547929431*y^5 - 1255174401234251846139271396794289012714590514634284987110999853677994/366226641044905601339682980239264233419457128005579917806594547929431*y^4 + 10886393290461471399484759382905657615691947697796242816683349050642/1917416968821495294972162200205571902719670827254345119406254177641*y^3 + 3020753382206250447923905310374576404082564294630724133839278185657161/366226641044905601339682980239264233419457128005579917806594547929431*y^2 - 2409080168826029710693577223404890042239354087742476026614844092913224/366226641044905601339682980239264233419457128005579917806594547929431*y + 95831841691634357616981067413122501383040667221161425683092358891318/366226641044905601339682980239264233419457128005579917806594547929431

29276508690277897215974140792929196453415854939625870562560286194359664359383496549595192475167/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^23 + 887568986388672435474104313002375350410909973175903937802941877015652609941079778199149465601865/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^22 + 14511145919385621500831894356876602789300947001993880432208078588398911152505707819197982444519235/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^21 + 141482597020188127876418862129600882406038054345421910738194361267812177968183125442132741841445773/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^20 + 469474928086437931881276975518102360420731783533838728099911011143222093110487795523317842446878179/41801087432287275626808522609026097028333830300387524405026166568755957643119482174662999817512856*y^19 + 271975340411338402044209909511528947556830468631484423082757462770745002328368334114797815043937378/5225135929035909453351065326128262128541728787548440550628270821094494705389935271832874977189107*y^18 + 14908219404354814144804548405430268419866037310402240348709305991103401782755717621800300974292797771/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^17 + 19567185102708355673375466736547323394838689209465393959369695081412255991046003889850449322579506149/41801087432287275626808522609026097028333830300387524405026166568755957643119482174662999817512856*y^16 + 4751238377278810180496548738646532988327220098141596485228011276897576075865952185004564247565416857/5225135929035909453351065326128262128541728787548440550628270821094494705389935271832874977189107*y^15 + 12965103661393013485495907202711810222378750250099391067862139220096325738271251304893238546873901613/10450271858071818906702130652256524257083457575096881101256541642188989410779870543665749954378214*y^14 + 77376229646262343625879954809266434276404007876058902761858409767346509992448495486551669490368379653/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^13 - 3469506176593863883783914960253106947901152422574507267842879201654710689101153388646149590557804199/4917774992033797132565708542238364356274568270633826400591313713971289134484644961725058802060336*y^12 - 176749996163672269265793112843700103868070229953877993851423446499636701167221677089033146911378627985/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^11 - 142188106248610095489160034784488914452683269936008663268195840479908601308563256040291435310279419503/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^10 - 4495514470594950886206709725327772002405730332133127034434514426048128093081931427621872658471392688/5225135929035909453351065326128262128541728787548440550628270821094494705389935271832874977189107*y^9 - 14879510160159811207886782360981762626102998962411920373274056561825380454279965026907367743606926895/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^8 + 35946722690672531675937335868727132511635210757990221001386076657576596249818100452614607019681926307/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^7 + 54442206676761381088444137759043245545987893722547039926454155107743753325998544149464640613676727539/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^6 + 17340783737916698461021497813835056574663189286713657326428248572046337835741711007794361336667734079/41801087432287275626808522609026097028333830300387524405026166568755957643119482174662999817512856*y^5 + 19571476058310122757339904027782543354169296149459573494752939069270909079759318556346955338614479973/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712*y^4 + 16550930250459997487134543435556960815595156743018333088028525396357002928847802341319916329885973/109426930451013810541383567039335332534905314922480430379649650703549627338009115640479057113908*y^3 + 305933792897390373337753215179134425406541533787420137007755071626816398294881878451390823786428955/20900543716143637813404261304513048514166915150193762202513083284377978821559741087331499908756428*y^2 - 132419750541492554066689952617817928045281605988472458479657925159299220720115430134634214626497950/5225135929035909453351065326128262128541728787548440550628270821094494705389935271832874977189107*y - 505851749100413407041735516973659728354723317134599903057174892603728398191050874423631880544473307/83602174864574551253617045218052194056667660600775048810052333137511915286238964349325999635025712

-17696625808256101402495168755388266373194447613343917962521867714967823202643813199663794993889/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^23 - 534427424632462857990906851163833934615212160145416950048555812160507198330351724370894378962899/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^22 - 8710862991038315382963190833905304194416494965230007057455373761384865067560151042814933712675477/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^21 - 84561587990326554076876422720541997074448173076063610354939106449828764343320207205227864527577731/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^20 - 279323062649727653663363130747171570276838651071046599895897433499653247351964632586772658667902707/71307737384490058422202773862456283165981239924190482808574048852583692450027351945013352629874872*y^19 - 160901982975307972089971308618058322731549229477562532694665477475057729695176613940849779485542183/8913467173061257302775346732807035395747654990523810351071756106572961556253418993126669078734359*y^18 - 302462199631248587753496882979886921162873808435618585670170167635686839089992570095011377728539445/4917774992033797132565708542238364356274568270633826400591313713971289134484644961725058802060336*y^17 - 11451640884219755742388343099887752412480880920338534763269244030813172564658353511273907876904689277/71307737384490058422202773862456283165981239924190482808574048852583692450027351945013352629874872*y^16 - 11043796766090550173177331771756281331232826771514520101650617672111825514811917744271932184404139753/35653868692245029211101386931228141582990619962095241404287024426291846225013675972506676314937436*y^15 - 14948445145851400378559710292264374333912019210185661352679195726006844476780379790629365856585064669/35653868692245029211101386931228141582990619962095241404287024426291846225013675972506676314937436*y^14 - 43874400106583590482714762195137682701767103152853478010125653163737974198476933784847055043791227595/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^13 + 35819408023160114469785180287656620026123973822945224952349547055099152754953345905360909385569210873/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^12 + 100178343877446995489757912273551108785741697835041214751301475739810365497996910866303904026818112679/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^11 + 80236915101140908548211518409789452880030882990924158731651004710159482314733209097018291067701691313/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^10 + 2731738794870247405681279004748190051320871071817060647932895348998159327829151647133524298352982096/8913467173061257302775346732807035395747654990523810351071756106572961556253418993126669078734359*y^9 + 8544561785609353469456454203982157267597972338161316624800509068376220956801582373716671887651317789/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^8 - 20701136037422198689041983324744101582902552087779934778917460275975431739494619368108277322737492929/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^7 - 31061778763716140701280225148306718665891165409082644123869455035429975716265882737727028128103109869/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^6 - 9940981078019544293716700209556471438845326139263917962779340876494538112004987347570584318805329639/71307737384490058422202773862456283165981239924190482808574048852583692450027351945013352629874872*y^5 - 11939949019641932921090678474711735552786983912230752103185579321557158643507332922533318227875512023/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744*y^4 - 4745516244284783029763180283631612548000791964589894206313875630071451168945913392195137785646331/93334734796452956050003630710021313044478062727998014147348231482439388023596010399232136950098*y^3 - 163843577705774643744488388177751069346456213907101429413924147095867109064561775416385795935608551/35653868692245029211101386931228141582990619962095241404287024426291846225013675972506676314937436*y^2 + 65482180246501702607128153131886320843393570006303197430378327190371552745617723108406155808074708/8913467173061257302775346732807035395747654990523810351071756106572961556253418993126669078734359*y + 482515438430147644375850522436690310800390592233664977785625729607578889378095916337197409722343529/142615474768980116844405547724912566331962479848380965617148097705167384900054703890026705259749744

-16632577846552077283012488732490936851525391799721318640981326209749754314829371224630223941/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^23 - 562423300819350367385974484263725621169607070797945749830937664897930189848597076405391131699/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^22 - 9975916870920149240738808202705525921424096190228113856602625112117021647625913031241239598017/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^21 - 108268979986349244616770383726353627418022172080959630230472022185790239268517455857188034896579/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^20 - 399698652840859622713773755482453003616163985007492358166681278468222742896550404277167318093457/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^19 - 1048488399092113660525397648541084691924626583770571496519736645713662963419346716018399312673009/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^18 - 558252382393029400695950270931274724026358965746825812962927747653877301900033338384558601939177/56478415716652289311681841052560171630918872218054415679819174556670775400262769362827900445888*y^17 - 23865840186019768506049154382323759760582018946442213034743174456953445957941488003005146916428053/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^16 - 6715752676840406964795642513721850786218246560224627678434381513453453567233834975900990486909981/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^15 - 5510504597926296297276148110012600326640814918433600825164714755740433637374039999260201427639627/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^14 - 189686979311246920635926042551674436724782981539039052238906123517689622036029583044629581645190931/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^13 - 2803896694136722417054180396925081990404456411714212775214781044117114051943647273465161760375999/96345532693112728825810199442602645723332193783739885571456238949614852153389430089529947819456*y^12 + 252963515993108197784848512078148104371962511405306749154423142474345126769573532148914813267374647/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^11 + 342855240092442587107364262780126691780221741941171379145147254187856323578258453381905738013101249/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^10 + 46960447820975773932790353047307890768714919173686114602206198415773020926203218881371577989841045/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^9 + 84282132504923068953266447404847589111171755233902213553368770961989358248307984391266324692383929/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^8 - 28214596049536890153890307084107146362484557297131843959900817833098593732859863077467342232842349/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^7 - 96918474597834786714640691526257817621452750779741430155086642096624144578801938413797455151273937/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^6 - 45446342110870798708747797196535577813730075056195959616184355701171349314026632879258127195389073/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^5 - 42102271309527246247589947636705712283030930353414616071871888977998356902513878435436628434946743/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^4 - 1046162655587360493485448694719975846356397516204792992574826140061607919319952801110200374890745/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^3 - 1435899694940916982656840877066031106440623598909301108817495722715624447701070273558447664852629/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^2 + 693639946855788162644055148813296213224941400862514148878253281505283648933868261990945880385505/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y + 2703678458902983987211996898696677452466592182217691462170829013055756522339439655941437421380949/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752

86384885240219465803528675889563312508861951583061259609342263145321117376204550820527291287/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^23 + 2628604265351362505088039296708649197548308071188194517987287766183527778260266412040869598357/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^22 + 43107288862008185451744269344118734492747961493722618956640205947340095242113637000629343528563/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^21 + 422152555559201950351696259157816726625581302574372425467835989479579939485510117453374547188989/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^20 + 1407727418856103368536588944225531810668199204962737466792915816211933012586626943569043706081923/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^19 + 3283203233768065539447711469833221552678252852528085283241181290431793550420911209910959935420179/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^18 + 1562502776286046064063528444437789888267894912927702274281002200093994395344531986780300083829771/28239207858326144655840920526280085815459436109027207839909587278335387700131384681413950222944*y^17 + 59942436606930678826019390185993609769541084430701800336775366857087416127617778619635940299611237/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^16 + 58887405174852660593927883177710797779712758426852153253199757646266122118748059974699868032746025/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^15 + 81733729956000128219816620221058422797858802074398643393627830109946688466401448914639393740907875/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^14 + 254977713991986507276131710265761936977068653099245595639144380811544434729875146890318331620756757/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^13 - 9268916735543002231584531512961167464391505181908885287435793351964900577156991797380932802406899/48172766346556364412905099721301322861666096891869942785728119474807426076694715044764973909728*y^12 - 545307090321540176540023414998146521334047802307683363326975081815131758935051801426415348458531457/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^11 - 466416186318719965195753356586884532137633789623739993832563218590938173033163393817790515039353123/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^10 - 15107575117215691246591249823632213245373610343919920914288832192035663656965431426498966483294923/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^9 - 60761882539625995882529294517653199304269720114779418698306357634949762973174174306944759251614335/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^8 + 102481721561851605800307982741682508919979501889445414531234146904493870461259674860341795242890751/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^7 + 171919787594954232008220975148739886809713422415409112372091537648826814052114924442047352236835295/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^6 + 58837997651793984210753698244307058586609972934377738765836571037052397934535296549623324826087151/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^5 + 64749370280620131437789105026523628573385684627844518517694879575820673605031394428744771807052917/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^4 + 10669931992330252888446738057424481675983564618917805038764107828534242102939067754381229701840571/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^3 + 1570696583616146818907677963150314047497243310530099456083229490468577275032338432495994020008593/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^2 - 1693297427367218578591252285901624264229987488564363198290572944300668607999796948932195475204149/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y - 2004317889540830941514410922921105530932697790846439827620030316027913787963385281452504564525875/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376

-3561719256330308408522776870460932998320077112350422579114416775512652843445076610522337207947/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^23 - 108155897114665409960460802052727753530871288926105919414022708970101625907868551002415084615385/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^22 - 1770602273032554644659754499048854447348539871862855851550342542211498693486241453434067535954867/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^21 - 17295864579909937845193362918787608050879484038744156296396003043563394959396866743172700799289941/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^20 - 57509734235024920253936555128298744746129239938731714091330671993610535225987614626345916618056307/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^19 - 66808670524379625584567983335921842466832966073481598116676450100296995015162469432057352369325035/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^18 - 63315332941889632213309310753608426702160300834828156775836773032090624886087336452568714754903207/14119603929163072327920460263140042907729718054513603919954793639167693850065692340706975111472*y^17 - 2417148878512822715204993806496992720507646711881869585934247191748610475018868035935883144571793417/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^16 - 2357759768574355867674664142918300341964230189266036903486437865599941796879499426264558428477187175/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^15 - 1618320376726326612919822886261486103719770696240687014299267880546495893038259647817601244898429003/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^14 - 9812107913219832382372475445802877333526724048788855293291798148897541262729274486867459647547674025/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^13 + 409917785284035059121392964864609023488442250813539479539078454019446936599190420005793623601242843/24086383173278182206452549860650661430833048445934971392864059737403713038347357522382486954864*y^12 + 21961607421814861498644427987911108333929030751571621206142347757543162449822152431402611205473583189/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^11 + 17994291422995242567880457617814534107319322294307486100657789545128014799518624229811982392862377059/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^10 + 1145097699894910891905313638292053815876159171621232463479078791289561644858838532871875841342138999/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^9 + 2120724003183978386307522350149040202267419587377219689252883417669429452407094294280212359575737975/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^8 - 4380618806278809334553043153367423821210221256876795829311674912132775064088029973295295865418812687/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^7 - 6814608530227467942448701839765657948454853245532908144493770102803929477421218639255323210893169223/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^6 - 2211707435341075928794797907113544815608509356980460108925775625698006586456803564819409041177456437/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^5 - 2492050874852837561419058219625167570737420070524216789142171941481715515511066865414402720043521345/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^4 - 102723550142048028159122896819889177201947159601006060934700519422338263212167173928958323721818436/25591782121608068594355834226941327770260113973805907104918063470991445103244067367531392389543*y^3 - 24164606551518633987648678944964363122471024781371562887453758602562146044054842465170786663573469/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^2 + 67701603683548587415716639639330879280776863480272189869133357730498958820810794838962185396683447/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y + 58194706973985418009499848860918077992777736919451074613172113468967268672025644959505525792412207/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688

-16632577846552077283012488732490936851525391799721318640981326209749754314829371224630223941/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^23 - 562423300819350367385974484263725621169607070797945749830937664897930189848597076405391131699/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^22 - 9975916870920149240738808202705525921424096190228113856602625112117021647625913031241239598017/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^21 - 108268979986349244616770383726353627418022172080959630230472022185790239268517455857188034896579/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^20 - 399698652840859622713773755482453003616163985007492358166681278468222742896550404277167318093457/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^19 - 1048488399092113660525397648541084691924626583770571496519736645713662963419346716018399312673009/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^18 - 558252382393029400695950270931274724026358965746825812962927747653877301900033338384558601939177/56478415716652289311681841052560171630918872218054415679819174556670775400262769362827900445888*y^17 - 23865840186019768506049154382323759760582018946442213034743174456953445957941488003005146916428053/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^16 - 6715752676840406964795642513721850786218246560224627678434381513453453567233834975900990486909981/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^15 - 5510504597926296297276148110012600326640814918433600825164714755740433637374039999260201427639627/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^14 - 189686979311246920635926042551674436724782981539039052238906123517689622036029583044629581645190931/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^13 - 2803896694136722417054180396925081990404456411714212775214781044117114051943647273465161760375999/96345532693112728825810199442602645723332193783739885571456238949614852153389430089529947819456*y^12 + 252963515993108197784848512078148104371962511405306749154423142474345126769573532148914813267374647/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^11 + 342855240092442587107364262780126691780221741941171379145147254187856323578258453381905738013101249/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^10 + 46960447820975773932790353047307890768714919173686114602206198415773020926203218881371577989841045/409468513945729097509693347631061244324161823580894513678689015535863121651905077880502278232688*y^9 + 84282132504923068953266447404847589111171755233902213553368770961989358248307984391266324692383929/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^8 - 28214596049536890153890307084107146362484557297131843959900817833098593732859863077467342232842349/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^7 - 96918474597834786714640691526257817621452750779741430155086642096624144578801938413797455151273937/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^6 - 45446342110870798708747797196535577813730075056195959616184355701171349314026632879258127195389073/818937027891458195019386695262122488648323647161789027357378031071726243303810155761004556465376*y^5 - 42102271309527246247589947636705712283030930353414616071871888977998356902513878435436628434946743/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752*y^4 - 1046162655587360493485448694719975846356397516204792992574826140061607919319952801110200374890745/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^3 - 1435899694940916982656840877066031106440623598909301108817495722715624447701070273558447664852629/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^2 + 693639946855788162644055148813296213224941400862514148878253281505283648933868261990945880385505/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y + 4341552514685900377250770289220922429763239476541269516885585075199209008947059967463446534311701/1637874055782916390038773390524244977296647294323578054714756062143452486607620311522009112930752


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

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

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

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

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

# 1 Loop Invariant
2251493759713028915568250068114767932318482639902877901186121764473461070644660347315164494381/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^23 + 67262159715297069118863786549912300227621365371971782319651904526221835260381088103636353200671/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^22 + 1086516108696963495212754915012884753972080927419216706215221466925290982271413185532206234616657/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^21 + 10408923459118720761574819585014844790467222756883309008870718455171728391058012116091456348257323/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^20 + 33874557809874357879277215287357267087679624512119513931913654693235219293171216526335318255039617/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^19 + 38259524930419764958710016016474109199050956076484305654186606872438490332167188155327345019125195/25591782121608068594355834226941327770260113973805907104918063470991445103244067367531392389543*y^18 + 35179149602303846788134296186793404141663752469952436121846132816983322409565331049820468376441121/7059801964581536163960230131570021453864859027256801959977396819583846925032846170353487555736*y^17 + 1299827667545342260798870472727148519117420931179932287041046501514128834568503274844946665432537363/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^16 + 1208773837304473831191660850818545330127011273798259010512007794447772869584831587332611290270655715/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^15 + 1548521670834908299891205806680817643011488988844812099409663156559727940647870284205507143714760549/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^14 + 3880665616196896621196852407706026458936120462522792032113373016690736439885246839673509868346424839/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^13 - 316568358532252836497205855705526536521691728867136576112330061482992973283278052120207291679834829/12043191586639091103226274930325330715416524222967485696432029868701856519173678761191243477432*y^12 - 10640340435561791844030272670526183348009625636510432426721756398999225128232736150757858423013420515/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^11 - 6907191880305968859615257898169573021477519125200585524962743730450370092507354781992700904421119765/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^10 - 493586184894420034908825994417605567697746607770036787894889849233721101851719901865481049675781184/25591782121608068594355834226941327770260113973805907104918063470991445103244067367531392389543*y^9 - 291126103262950656381127036024744200313430484493502047131719948190194774958460823114853635189509913/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^8 + 2484328479085271111466324713720730355966714244969621499295215969172556716179706757544073016472880825/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^7 + 3030863732918413928132738841897408306624396763196986926437424054818729141959914669980427850002496809/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^6 + 817905468478440098310971739096731310292531539651823866938930565051902049161984210279633617736132729/102367128486432274377423336907765311081040455895223628419672253883965780412976269470125569558172*y^5 + 1152008683438301412708335039032831767007674814246003653743170028304014710195385718003370790918181703/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344*y^4 + 153305696901625928035062732012168463764673704746434217385236389481909600969707427049539187682836471/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^3 - 24062675538059485767247863859484034810041845510935579944147751104893441913167996464817781095749463/51183564243216137188711668453882655540520227947611814209836126941982890206488134735062784779086*y^2 - 7752668472963790731044265773446553868947508239150638093856386250624270017900403526865977006631177/25591782121608068594355834226941327770260113973805907104918063470991445103244067367531392389543*y - 37667770369825421921926836536040652237314064414506079167893446551413474243647037747590500505104433/204734256972864548754846673815530622162080911790447256839344507767931560825952538940251139116344

# 2 Loop Invariant
-609929274226149569870884514260937890547706248806101980670564482145809181964141928591159265261430285691025153045890458736704142600691226805474285772991599307143473909/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^23 - 18563914736478809712846753743944101189551363711620817602478309035148272603478152835944902599762747650657624553596524786167405864624162457964525268602969230940190349793/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^22 - 304470045347059648934568607103673158301872149044607589657620062985299160218850635204040112735657808845295756910252109883222763668034474652757630065552770145140841652409/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^21 - 994018172126068473354479795711630592792574712150858998966516136879408069472714708734304113545749244279880494959169291660678011646718463064788595815686308818623219020527/7709087822651902622264737065209286982716579098358848577168987112721155163032426393622589905992035370951297074642947644169204753100929131499517583240837411682219863404032*y^20 - 3314627953537135511194151576459603789237251893252968683386570662110474791049679077022585142254130299078070496393058754589914970888080470571223498970937313958976008270805/3854543911325951311132368532604643491358289549179424288584493556360577581516213196811294952996017685475648537321473822084602376550464565749758791620418705841109931702016*y^19 - 5797003468008926969000445076263323357735730753756582738345770476678175765463062658634670575184878923147650723975197658255457826095818937260384198192180925464139310819781/1445453966747231741674638199726741309259358580942284108219185083635216593068579948804235607373506632053368201495552683281725891206424212156159546857657014690416224388256*y^18 - 11029818271219920379412329839110903802161097714143109183253387042619161068773740401815630926831760891843723189691396891149283523106994175806188217194793137793912600677569/797491843722610616096352110194064170625853010175053301086446942695291913417147557960957576481934693546685904273408376983021181355268530844777681024914215001608951386624*y^17 - 70463710440355581133320171044098807250655562574101629996866521484403542661670585898462361219272259565257695234821148633204333704380711716917375364361146429850693810002573/1927271955662975655566184266302321745679144774589712144292246778180288790758106598405647476498008842737824268660736911042301188275232282874879395810209352920554965851008*y^16 - 276503348704256945708933626587358031935439174724509067761061850775095003070046583090025237354302550201845556820018968170184530981292523168565846003424037463313734488529273/3854543911325951311132368532604643491358289549179424288584493556360577581516213196811294952996017685475648537321473822084602376550464565749758791620418705841109931702016*y^15 - 1147801120698348029618506569485570764953402389467179445902115674703926723812090584895677486401007040008492365600056654669621793186583837837183066999310383121260599710297467/11563631733977853933397105597813930474074868647538272865753480669081732744548639590433884858988053056426945611964421466253807129651393697249276374861256117523329795106048*y^14 - 1774358200749024798305833842690677628678907041276391812857683141570353071298880475358187581595730009212762640280164154423973798356090727444361018889944633057726965875307349/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^13 + 382624026986796529458128913794573344819601280037417123291699541418099991521143258976781254065846337329208905880700900193455029270667983067910342534725906741815475776417171/7709087822651902622264737065209286982716579098358848577168987112721155163032426393622589905992035370951297074642947644169204753100929131499517583240837411682219863404032*y^12 + 3876943918814717112135277579844053237109603021827022154891736175564031919517726234344772941380997323899672124929842226279397176921271845237664922346171172561189429159174457/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^11 + 3249344753415571012214292404325103641003992195964990710186454042514943559985478817546540378872775812418257882918773072453057133173940218620699157664136088298899984187228689/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^10 + 825602267866436504134738916648465265889585148881732977145445127835699498523295848874199557112553767260841505608472442609573077851299873905797616411618136236007545882375459/11563631733977853933397105597813930474074868647538272865753480669081732744548639590433884858988053056426945611964421466253807129651393697249276374861256117523329795106048*y^9 + 407302662403116273080035228493750405801363662769953992878515840195749020807108074642070910258208853925894132068128531556973704300836299524442813136509973633996667159610991/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^8 - 257405937784610348958113192915325165763663758105920413800970213251215669621265742002782907462046357729823445938541363960267671273177385249026702806065321569673393946423503/7709087822651902622264737065209286982716579098358848577168987112721155163032426393622589905992035370951297074642947644169204753100929131499517583240837411682219863404032*y^7 - 1212622192762012071667921472989769368815975575836469221008314832793008642838996750807178408928711162346936755643777529067965991618827731137682172670944183910789739090106791/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096*y^6 - 400833947641871491193106827543586546983151624241743113921265483525954324220923358532182043093678429190729782263013880776328763372865592647681113004869669011783172046897939/11563631733977853933397105597813930474074868647538272865753480669081732744548639590433884858988053056426945611964421466253807129651393697249276374861256117523329795106048*y^5 - 148172295053253000821337265231766364997108680252486560119258291170906413565276790497610617310273157972861377994013493612824972637837104359157051368375274481909711891803509/7709087822651902622264737065209286982716579098358848577168987112721155163032426393622589905992035370951297074642947644169204753100929131499517583240837411682219863404032*y^4 - 49240341564155798019588836666244025861994271970697082471224777803764174979993624469254983318105473973587474880343882105877334910895764576113757933226768266885764114827933/3854543911325951311132368532604643491358289549179424288584493556360577581516213196811294952996017685475648537321473822084602376550464565749758791620418705841109931702016*y^3 - 17885954928588089638880875610384557930897200426885833372441673741589291742239370124541561902028668685870744295676236973027060703868575833287490402099008770669985561759501/11563631733977853933397105597813930474074868647538272865753480669081732744548639590433884858988053056426945611964421466253807129651393697249276374861256117523329795106048*y^2 + 26872990021782802039239938468842088069549070751837120037951677634872213776040426341429905389119650327691834362866928747786091501194384039451618683793908475384332296434127/11563631733977853933397105597813930474074868647538272865753480669081732744548639590433884858988053056426945611964421466253807129651393697249276374861256117523329795106048*y + 33651726320138300871860447732096905150087359970890963687573079362056052057410049295142976650687691329954461737623392354943130934299175847824295614443071863966199629913167/23127263467955707866794211195627860948149737295076545731506961338163465489097279180867769717976106112853891223928842932507614259302787394498552749722512235046659590212096

# 3 Loop Invariant
-4379607698091224802341999361197596563661630387495024615869176782255038288807316003043649944317674790374923785646789826908762064649772411108404125645384693509945799983282460665916266107621267136932641503/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^23 - 132718317232539893669339503357459637434141182861117735649346094107926915584468213991568360516541194472566675543507211676872485187762925611242517776825280389825718725958116146619929781571706808425900255907/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^22 - 2169230841538389292247076297892603170670145038387466171466381578859552251645009647782432772538575730209106412578193747207099105460289484100389518266177958316681910994783938950513413151772775936106467367963/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^21 - 21141883829630106537913693261293108722256702416926009867600066351775127761854481922896022821153313499481819060161579158754108972018156747245028297855100853352962576059870043774777828808741454594675536285797/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^20 - 35067176482102653101729910580238008792937024140838929908053016954492455646682384348886809305972370770485670113798948563908750505756967534073439295383021839356505596366676984318274436342483197490114688273731/414469547138935439990981922263534738113645883250830630639834527788939607662733184694578278062738537863172107656746639761817006295795428635574278972921850184028451994072960906145821897313339313429426864992768*y^19 - 20310286003123739927510598660251958354755267548222255921386460434176418135056355786099337660777884225194788576668473616742020597088264487039441793924920293270371110862719013326245072276340809633862637987551/51808693392366929998872740282941842264205735406353828829979315973617450957841648086822284757842317232896513457093329970227125786974428579446784871615231273003556499259120113268227737164167414178678358124096*y^18 - 76783557743396436196147177619858713265387606074329670931224113212326463059709688346289741153913982148754911372546852957160380526774252562261254246206808467044886206370049119435496574344322419384539595187969/57168213398473853791859575484625481119123570103562845605494417626060635539687335819941831456929453498368566573344364105078207764937300501458521237644393128831510619872132538778734054801839905300610602067968*y^17 - 365460214092139455064868691580708320533661261988077450268669062239534329482269096778134529811613169817182298594286671485549694637268426738764530476323013940528103433987373030439832880574407740046105403500531/103617386784733859997745480565883684528411470812707657659958631947234901915683296173644569515684634465793026914186659940454251573948857158893569743230462546007112998518240226536455474328334828357356716248192*y^16 - 5683720815788000287285143104284051587145779731051768819284003339700481103983459994283955298800961320453626947367328493771213970704673006951636354145914295865424440590996737759415937360625589453119230482346293/828939094277870879981963844527069476227291766501661261279669055577879215325466369389156556125477075726344215313493279523634012591590857271148557945843700368056903988145921812291643794626678626858853729985536*y^15 - 7771598913973934917814678927272634072313941541476164817723728633004975921323142736195677428231089233394246212788848911837289857519985710957324170405226142844043579005070279689612437997114121454009546807620527/828939094277870879981963844527069476227291766501661261279669055577879215325466369389156556125477075726344215313493279523634012591590857271148557945843700368056903988145921812291643794626678626858853729985536*y^14 - 11677269695597671865252229187716525240664772125160867936255053551311291481559286681007755697933309963392580284984539882621154948585979565132891086166612251780540817582043979635286912172630466110033434855062541/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^13 + 507926527153477838993486727848050051185250536131629891116067276776273483216714425309538905754179735741186673157865441769724433263098948913435604360986203786115087036166780384451975695425311489307806613146583/97522246385631868233172217003184644262034325470783677797608124185632848861819572869312536014762008908981672389822738767486354422540100855429242111275729455065518116252461389681369858191373956101041615292416*y^12 + 26228341737449679457650873875921145673288449526380469994934985441793214478789595852070371561781611698742513510366355600135189564560447271325498107068280192614042752300678002151781989551621388776586626384048693/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^11 + 21521441452876115113173697310635053769879984561812750057977583469625153973728055528663772800725971063612171623698525994409501918875350038683828623944685137006406742326030263742605197071881963287865355525851235/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^10 + 2815466104216281044985551556899093434634716618990683038233249896656561303968873834156792757786736517991897356124474018735166472038026420671976275669201943226070778373970080046967963500756956869176371813600009/414469547138935439990981922263534738113645883250830630639834527788939607662733184694578278062738537863172107656746639761817006295795428635574278972921850184028451994072960906145821897313339313429426864992768*y^9 + 2387186161532445486255028383520242124918295502457573978525424100143608240383535391989887878877642188573463175068464179189007612381291828457233790193722643985201431627078437243125952665318068961927189303026729/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^8 - 5340410126566783651861955170474917293465593893495426461304081034414388552052540979642652266841703382466879443344954199518758046805893266683527435541563259785320790827265315300201224413588275961653554257682945/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^7 - 8079485879264974351820742685777418876839835607609345663834179271821096226809251423780156427728768641262566290360259048264136980024903354969378857321135080482466283570316901487543989774164097933627418751415395/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^6 - 1329571985692891365775585711652182316739955564523398528549473057825584812262916279126987305065363680528996878558423679635154077807650280178582757539195172733247291943337684573612172277308757550151364073004607/414469547138935439990981922263534738113645883250830630639834527788939607662733184694578278062738537863172107656746639761817006295795428635574278972921850184028451994072960906145821897313339313429426864992768*y^5 - 3129769856630169633262809536406128387018355640582830828695881861396821973194429230190334795168076506008724038151770172578430448191124952856882508957253966011999622567779210544917756033805908437518850666279335/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072*y^4 - 955787835678313253984623315644108246509645478332477362146647847661790600760584033828061242963304102016547207424040473664864168801261184803114053287873278122317633259772214776913037647580378216107782402483139/828939094277870879981963844527069476227291766501661261279669055577879215325466369389156556125477075726344215313493279523634012591590857271148557945843700368056903988145921812291643794626678626858853729985536*y^3 - 50677259429021340349142891176610293876872292861246125770145507788953884139098001397217746639248273675097307365476512004388286270797657464871641593426311643625144237995523108006303152779150033071059690348873/414469547138935439990981922263534738113645883250830630639834527788939607662733184694578278062738537863172107656746639761817006295795428635574278972921850184028451994072960906145821897313339313429426864992768*y^2 + 74634522426054491117692951500546505800568275435587903641609481456417368382147518066277098958447723869535381092451090626463289699008481200335005097996505971463164814208230799759116962442285768895038099072707/414469547138935439990981922263534738113645883250830630639834527788939607662733184694578278062738537863172107656746639761817006295795428635574278972921850184028451994072960906145821897313339313429426864992768*y + 124319791182099678716264919765655229831683010297813552929365084811652142999798858068881026950251226577399869811129918782615466655902592566654440050869370903312383092283214767263657935488882083066863443837097/1657878188555741759963927689054138952454583533003322522559338111155758430650932738778313112250954151452688430626986559047268025183181714542297115891687400736113807976291843624583287589253357253717707459971072

# 4 Loop Invariant
2232708101605065007595682010337975186503946682909483212238757243120742064543285984897602275209182465031637418391834240250359995767330015694778871861985361645573009000280325293818174413955866105323901230017411615340452867434204263030829881646489788017024349987387184761208600059/497456713777226935108499225078756925682215801592359803929984383095742078457535611765933890236247458525386145895117402202354772639542266047474207396923628550791213729802206749151765346477426550145052010967957651756499920405664916001242457471219915522626814308423462334767706345533440*y^23 + 20419378910555578931510697552391415916813518249287297417161627399308337476840870220753965527578551727835376245916570209068952583773049463231750811520174978073420318694144503642211826039067028089044723970835205921117528313554851660064442375034414880078207570202495262717686750725/149237014133168080532549767523627077704664740477707941178995314928722623537260683529780167070874237557615843768535220660706431791862679814242262219077088565237364118940662024745529603943227965043515603290387295526949976121699474800372737241365974656788044292527038700430311903660032*y^22 + 5365384136274091087367187016944767343838910646152317564623670536702987051734782383115109732514518729130706767620625948597104214472913529268014732906048963860343384616553586684727909442017872605259783489019018331092064174034962952140857367344865406142690282325476247989091278272671/2387792226130689288520796280378033243274635847643327058863925038859561976596170936476482673133987800921853500296563530571302908669802877027876195505233417043797825903050592395928473663091647440696249652646196728431199617947191596805963795861855594508608708680432619206884990458560512*y^21 + 52647041927804711911006454394880157442751433199382475233134861513249944807798805959391940909758255290035435536371450481363186392855432283010019451243108354196778392858603073514072746049768341417180775333985253042011978594669341996473999627675030327511641600584803546371365966781587/2387792226130689288520796280378033243274635847643327058863925038859561976596170936476482673133987800921853500296563530571302908669802877027876195505233417043797825903050592395928473663091647440696249652646196728431199617947191596805963795861855594508608708680432619206884990458560512*y^20 + 1759048873444400645031004240131898941064847598086294022773723496289110612706402104416270286156777400424187066434211771880331197079249912273773467526322547846542600599299818348915597566892671754429703992556852992404652337381010957615515230278963950046299707813895493579396092045116533/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y^19 + 4112224470271726140270507450862463355038004826075216172791486998657715566720587803985437164345055963322939474911160521770164417678574776666529098595437800984301074773345932054975668525289007683353412624464837461689779415494033772464987056568846883135016922639167159963005337077900663/5969480565326723221301990700945083108186589619108317647159812597148904941490427341191206682834969502304633750741408826428257271674507192569690488763083542609494564757626480989821184157729118601740624131615491821077999044867978992014909489654638986271521771701081548017212476146401280*y^18 + 163425750456322737359254096202057709719864104010421541948192739136627356537712458441457436002258082695704169686016772915237591743557118816220104512151154170940850069879344548406065137797988551727485389558101977215723155305403931653140598562999730336498843634222288403925544533714733/68614719141686473808068858631552679404443558840325490197239225254585114270004911967715019342930683934536020123464469269290313467523071178961959640954983248384994997214097482641622806410679524157938208409373469207793092469746884965688614823616540072086457145989443080657614668349440*y^17 + 75367413560253652506515558948603650729333241860524659938326795478225023793457675277406017775652938670053631324541017059453005483554893036595301387931978461661238869561980609948012018756160609083201302000771248285392723751284097787723495937300994117893194855409958311415097705194391419/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y^16 + 24731839650023044342422948281999879978059462697087179722301962448750232375610392704833705064701758576871028636173674211632912686888813754656124439450615314463380615192046750237044965750783584400139914391542542136002113560140055817479531553831075539568008658156731436637869643857262689/1989826855108907740433996900315027702728863206369439215719937532382968313830142447063735560944989834101544583580469608809419090558169064189896829587694514203164854919208826996607061385909706200580208043871830607025999681622659664004969829884879662090507257233693849339070825382133760*y^15 + 206225297846053403107724582522692189410520329321906445590696035064297088976816795561635403640328766021852428496318351071174028274233641785434341676658568138146934635997100980219273999073324883556947201339146645771385693609496902998821680324152144481618102788854058555448454077017591579/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y^14 + 8933597302179382239713452366700847011643417978473312289657557923410478012776442566980468209109591596930847668598664905609083609854281138192827817035334447803686003764468025412345936719314084624388593400004919734142243418085267776973554550824619835050730982271757967351749377495735749/663275618369635913477998966771675900909621068789813071906645844127656104610047482354578520314996611367181527860156536269806363519389688063298943195898171401054951639736275665535687128636568733526736014623943535675333227207553221334989943294959887363502419077897949779690275127377920*y^13 - 2938186793257536232411294913880163152032555653913965292464086568658074890722927378886407753429726565663161978499600160830036587252404465867966692101383580730082100358306058895070091037863180963389286978845371804568209198855684424740199092752633002084391240001479658657958668275997257/351145915607454307135411217702651947540387624653430449832930152773464996558260431834776863696174676606154926514200519201662192451441599562922969927240208388793797926919204764107128479866418741278860243036205401239882296756939940706759381744390528604207163041240091059836028008611840*y^12 - 11685568510797555881168123838769008895138868680868100044178112034925023732115881101066980769181564911136488089245457981891512291172288799120763961690489476636704618083433606662417116467423967024585396956244353174473016702397137126154383450281579364608567892092399156195553842693383177/397965371021781548086799380063005540545772641273887843143987506476593662766028489412747112188997966820308916716093921761883818111633812837979365917538902840632970983841765399321412277181941240116041608774366121405199936324531932800993965976975932418101451446738769867814165076426752*y^11 - 29871622699030306706943975045702186579275984776662689597707680754794614964198231990132878160578480788578671133367598947961434257602212817067053391824505689720451351408557251823177989747240601834817651343111714010675880059759841663790178434831486949552314205604131171585294439291315613/1193896113065344644260398140189016621637317923821663529431962519429780988298085468238241336566993900460926750148281765285651454334901438513938097752616708521898912951525296197964236831545823720348124826323098364215599808973595798402981897930927797254304354340216309603442495229280256*y^10 - 8334516350228617264673932035215847648861864421964408441749576219046311844149913645416396755937096319628324271617371481142696948469251077072980811752437104456934810652489457914646606162653856242846927175916035801382782169437487900864513398817678011903513765928447562599691439640857369/663275618369635913477998966771675900909621068789813071906645844127656104610047482354578520314996611367181527860156536269806363519389688063298943195898171401054951639736275665535687128636568733526736014623943535675333227207553221334989943294959887363502419077897949779690275127377920*y^9 - 578329747461018226202369465225896288155276992521864333830556402018415869392587732268291130958842453063512553431524010065447746154716936700597460480839813332789266182631040060790473020462611549119519231505597471580924747309018014328719138767241214780236929369068652688854527061491523/186546267666460100665687209404533847130830925597134926473744143660903279421575854412225208838592796947019804710669025825883039739828349767802827773846360706546705148675827530931912004929034956304394504112984119408687470152124343500465921551707468320985055365658798375537889879575040*y^8 + 68688684593664457416501986230292872108783007120907786880718858201601835925618680528833897377035372959073041472274687295942778902749057506111001625030029366731309938061216001343304164817142178203888477588896616467342017126448577440232291790152018899477132747283264758104230866860938141/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y^7 + 3086661749955591518659122338586013015262280747835478407341623533960241014876155095741371145259913026816943871116160834122009946031418907706209100547454735994329959958924229334532469569593532428673391922337164688344523704871247915519439133617334582610873764899795267376517591518918993/331637809184817956738999483385837950454810534394906535953322922063828052305023741177289260157498305683590763930078268134903181759694844031649471597949085700527475819868137832767843564318284366763368007311971767837666613603776610667494971647479943681751209538948974889845137563688960*y^6 + 4623219954872964058318917315629156516585120873118424583475742647651447915472548295965987273417356899486188911475342892387403629743710477989535618874305702602273240545093625461277767398573396959494356825522461319414084081472820016037899606761600961276811526804866639542114370364177823/746185070665840402662748837618135388523323702388539705894976574643613117686303417648900835354371187788079218842676103303532158959313399071211311095385442826186820594703310123727648019716139825217578016451936477634749880608497374001863686206829873283940221462635193502151559518300160*y^5 + 4457803855811672638002786067937921730590243952757733583089692963395678079784437522611469047633225431306488149896535300851346049517960163226849386946806646175787831244266084198802158821270498635009777647081860093898871584873742409862301727312664218307035998624696666782626162517292251/1326551236739271826955997933543351801819242137579626143813291688255312209220094964709157040629993222734363055720313072539612727038779376126597886391796342802109903279472551331071374257273137467053472029247887071350666454415106442669979886589919774727004838155795899559380550254755840*y^4 + 13561676144591539963528387193593718526336247492010106920844699362192992491852584757117045550099209880401312169983670671859308214374150619989283580871985694029738130523162016933152099236734744748718927980780442395608291342911087276810323909934490476896154516582823969227721243284693539/5969480565326723221301990700945083108186589619108317647159812597148904941490427341191206682834969502304633750741408826428257271674507192569690488763083542609494564757626480989821184157729118601740624131615491821077999044867978992014909489654638986271521771701081548017212476146401280*y^3 + 3957212743417990107136117377026535531711895851786047374572943327633608037832537861144856434424310528801027895289511180375547667731556130897809604331335229754496989324244320009087886196183037433615573579344490713412093398432203935642580339744015328933834978458043861403885143012693017/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y^2 - 4668613898638751620704779820986013165255717170437523235113219055354806750574071959840341439481568440633373909432159658905943344732021008950837331101160465550929021526967006127696436788764834527032447406552609488976114934973344891672856278755434327392687575158818771846820495173091201/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560*y - 981667412405024583877137273496095881223604514900307014382130077376572014210725792593697955139098423989222200249261524588513739594478872348701643538727818683064144386259762029325792764597534466285794624828629776465234904962470756488012995770494956875112176837710625590231397639153719/11938961130653446442603981401890166216373179238216635294319625194297809882980854682382413365669939004609267501482817652856514543349014385139380977526167085218989129515252961979642368315458237203481248263230983642155998089735957984029818979309277972543043543402163096034424952292802560