# Manifold: Census Knot K8_75

# Number of Tetrahedra: 8

# Number Field
x^23 + 34*x^22 + 250*x^21 + 730*x^20 + 379*x^19 - 2178*x^18 - 3875*x^17 - 2406*x^16 + 822*x^15 + 17739*x^14 + 8186*x^13 - 24105*x^12 - 11592*x^11 + 20423*x^10 - 11669*x^9 + 11072*x^8 + 6090*x^7 - 14990*x^6 - 336*x^5 + 10932*x^4 - 7432*x^3 + 2192*x^2 - 304*x + 16 

# Approximate Field Generator
-0.823314425650152 + 0.389715339799502*I

# Shape Parameters
-3088901438302456293206593260203885583144485648/162981387146089310989562845334097238138934691*y^22 - 847342224998346432694610050014182401762060091195/1303851097168714487916502762672777905111477528*y^21 - 267602624036496111438171291091686557115949795726/54327129048696436996520948444699079379644897*y^20 - 9934560749186902337940684143997660699865428097277/651925548584357243958251381336388952555738764*y^19 - 7433836210535504779867660377459274739882219681431/651925548584357243958251381336388952555738764*y^18 + 50427150381201931254674128618819496997331772431459/1303851097168714487916502762672777905111477528*y^17 + 1550163641492292844514943182215113757735181297180/18109043016232145665506982814899693126548299*y^16 + 30308686446995364509257276849652352205629166997239/434617032389571495972167587557592635037159176*y^15 + 35946430976504008890944373346008827832169354737/36218086032464291331013965629799386253096598*y^14 - 24719037353323051588447067026648856763030611745935/72436172064928582662027931259598772506193196*y^13 - 336581335200079427983552990958252139493386350827289/1303851097168714487916502762672777905111477528*y^12 + 127547715673537432182770669268677654165446802554861/325962774292178621979125690668194476277869382*y^11 + 456044333902988099305423696941174198882254803290631/1303851097168714487916502762672777905111477528*y^10 - 187097060979878550275055294466828686590846168790713/651925548584357243958251381336388952555738764*y^9 + 161545483156425304846486269663059512044172799598739/1303851097168714487916502762672777905111477528*y^8 - 227748500098490679426462547504853622073714989330379/1303851097168714487916502762672777905111477528*y^7 - 111300068908057893159517947270341820488307493803191/651925548584357243958251381336388952555738764*y^6 + 154729633353028554561160635178882324783710731179439/651925548584357243958251381336388952555738764*y^5 + 54478384831802332078302638311404211893990558396401/651925548584357243958251381336388952555738764*y^4 - 60299430740252350364609641152882655383743728095617/325962774292178621979125690668194476277869382*y^3 + 26869645716563777573034341332704613838273735201561/325962774292178621979125690668194476277869382*y^2 - 801029183959487854137808312767916748658189823922/54327129048696436996520948444699079379644897*y + 150335790877190384916673047203066484511937719256/162981387146089310989562845334097238138934691

-14012109977092839705940949486199114880039423697/72436172064928582662027931259598772506193196*y^22 - 965322854232480413208427610385999852291633913645/144872344129857165324055862519197545012386392*y^21 - 3718279700368932734778759512181830518378373189943/72436172064928582662027931259598772506193196*y^20 - 11886402722528855559875426068346151924083450770381/72436172064928582662027931259598772506193196*y^19 - 2651259733809080328811075068050825030529717324154/18109043016232145665506982814899693126548299*y^18 + 51628061220450077327675825499466772799345672774725/144872344129857165324055862519197545012386392*y^17 + 16461608209988096056805834100894979978118930102282/18109043016232145665506982814899693126548299*y^16 + 126120973198243639867551430351337789919389339150203/144872344129857165324055862519197545012386392*y^15 + 16477540932144110012457769242310087895650487020225/72436172064928582662027931259598772506193196*y^14 - 120705229595510268327890302886730507579775990908893/36218086032464291331013965629799386253096598*y^13 - 445077909094275137675044249206521509599606308994751/144872344129857165324055862519197545012386392*y^12 + 119411522370815276629341747092738053086682265877143/36218086032464291331013965629799386253096598*y^11 + 539112135510599286773371857123935521921232337570853/144872344129857165324055862519197545012386392*y^10 - 165955432235899646169901668873794441878705604151435/72436172064928582662027931259598772506193196*y^9 + 177996966264862286122250139914305264586051043676771/144872344129857165324055862519197545012386392*y^8 - 230970247653474592819291409704207017969352374306139/144872344129857165324055862519197545012386392*y^7 - 68510496100652857998051502826453440592948932889487/36218086032464291331013965629799386253096598*y^6 + 149011576764017786356805522394563417768878801985411/72436172064928582662027931259598772506193196*y^5 + 71469784557497084017970253088967276234346966618121/72436172064928582662027931259598772506193196*y^4 - 60682247938861925297936188593963763752328161575499/36218086032464291331013965629799386253096598*y^3 + 24918687769293710832810580889654078845721610369775/36218086032464291331013965629799386253096598*y^2 - 2096609851907927461220938803826809268271041656138/18109043016232145665506982814899693126548299*y + 125009236956088944616794770353989377841873513969/18109043016232145665506982814899693126548299

99893823336547418170591860691195445191358012623/289744688259714330648111725038395090024772784*y^22 + 1721817103818552954923263900467840373855105128229/144872344129857165324055862519197545012386392*y^21 + 13301224428948084160173067008423181938763799926563/144872344129857165324055862519197545012386392*y^20 + 5344757484188288295618395887281207148029023689232/18109043016232145665506982814899693126548299*y^19 + 78404285144309558980058326754897383304761203379901/289744688259714330648111725038395090024772784*y^18 - 90062694132011202883873483003276705139200652555241/144872344129857165324055862519197545012386392*y^17 - 471766110113373105013785933652567576533573142967213/289744688259714330648111725038395090024772784*y^16 - 28984282459906033881317178511971973533496599405624/18109043016232145665506982814899693126548299*y^15 - 69519017073432218849324435488856287023064377789371/144872344129857165324055862519197545012386392*y^14 + 1703443945990298574064682766096310707767838998790499/289744688259714330648111725038395090024772784*y^13 + 810509540428120178037700976864233876449428641800531/144872344129857165324055862519197545012386392*y^12 - 1636940852537671720324835455539830450294833418959503/289744688259714330648111725038395090024772784*y^11 - 961823726322523610485363163296706493551489194232721/144872344129857165324055862519197545012386392*y^10 + 1130322990487365403571091456007651519663315722503681/289744688259714330648111725038395090024772784*y^9 - 637777897142683618673878258424898392462968186058565/289744688259714330648111725038395090024772784*y^8 + 200963304806225150485726312565220209894289842457373/72436172064928582662027931259598772506193196*y^7 + 123246589441640828633735619846581546654322815843057/36218086032464291331013965629799386253096598*y^6 - 257501704987803518850000225109664426470862703015055/72436172064928582662027931259598772506193196*y^5 - 64569455615538805558335754049356622404244636745889/36218086032464291331013965629799386253096598*y^4 + 105865302831294795299831518054823390035629066631325/36218086032464291331013965629799386253096598*y^3 - 21512411406107699849332426485758078173332209012505/18109043016232145665506982814899693126548299*y^2 + 3597620609553597795723525708508997024078975321575/18109043016232145665506982814899693126548299*y - 213546111768271892128798568205516259482765441006/18109043016232145665506982814899693126548299

-3695224594292447393178840119242322204848080457/144872344129857165324055862519197545012386392*y^22 - 127179117377064784051994060587095765981759308497/144872344129857165324055862519197545012386392*y^21 - 976825089907070794698163331623825027768372598971/144872344129857165324055862519197545012386392*y^20 - 1551895752823587482121673926544836185671213434589/72436172064928582662027931259598772506193196*y^19 - 2685300755774837535951417062463390287856789001409/144872344129857165324055862519197545012386392*y^18 + 6963889673367574427112312724417572857105054003223/144872344129857165324055862519197545012386392*y^17 + 4318517372073637409829617021088661465596307563267/36218086032464291331013965629799386253096598*y^16 + 16066668368206319915705455954148159007533789766929/144872344129857165324055862519197545012386392*y^15 + 3482911934748866241060738872071239038899310505959/144872344129857165324055862519197545012386392*y^14 - 64373238240714305470707033032751811174334682808823/144872344129857165324055862519197545012386392*y^13 - 57328071295265453074981809688008655478483773656515/144872344129857165324055862519197545012386392*y^12 + 32800783208780767095247641108676630710306031087149/72436172064928582662027931259598772506193196*y^11 + 71043791122138345680285530756854929472050030426961/144872344129857165324055862519197545012386392*y^10 - 22927782531212375936697337709139128925542876358665/72436172064928582662027931259598772506193196*y^9 + 2913987159559341897721947729808592998033678269666/18109043016232145665506982814899693126548299*y^8 - 3904278023526416967651122937158527799490834018548/18109043016232145665506982814899693126548299*y^7 - 35782433580698355045117318419987209035929801531059/144872344129857165324055862519197545012386392*y^6 + 20291330470654756198727780860256171888176961604747/72436172064928582662027931259598772506193196*y^5 + 9293139590335044816630031169746525868875589836385/72436172064928582662027931259598772506193196*y^4 - 16365838794850842246378085125782252971953117897095/72436172064928582662027931259598772506193196*y^3 + 1696702370676199129556775297556439165864072867229/18109043016232145665506982814899693126548299*y^2 - 287054279922526696016690726821553255308556376078/18109043016232145665506982814899693126548299*y + 17153183474262928636828001589971933305252625090/18109043016232145665506982814899693126548299

-3220935194214226215409702294312171153982269823/36218086032464291331013965629799386253096598*y^22 - 222281722660481006647116023640930809665665723271/72436172064928582662027931259598772506193196*y^21 - 1722937686644838756089977598354545306326367129489/72436172064928582662027931259598772506193196*y^20 - 1393897622633218825802869019737275008084288924912/18109043016232145665506982814899693126548299*y^19 - 1318669198888926722436816386538507145149653390103/18109043016232145665506982814899693126548299*y^18 + 11314994336686989797732920894438996335319039721301/72436172064928582662027931259598772506193196*y^17 + 30618902035598625611427762926621987480714049345387/72436172064928582662027931259598772506193196*y^16 + 31025930025749987471912919797105947750009987918363/72436172064928582662027931259598772506193196*y^15 + 10638818066195604103339416109079534659950443797129/72436172064928582662027931259598772506193196*y^14 - 54262698642860258810442545412465704083986211132373/36218086032464291331013965629799386253096598*y^13 - 107326165126051783939778005700630135775501820566545/72436172064928582662027931259598772506193196*y^12 + 100405923981486485924111358621849841595094053252703/72436172064928582662027931259598772506193196*y^11 + 124338377453010943598134953041087008530883575671293/72436172064928582662027931259598772506193196*y^10 - 68634273674711842248539447794316583161901180064581/72436172064928582662027931259598772506193196*y^9 + 41363369817652290333403169097567313049624795002257/72436172064928582662027931259598772506193196*y^8 - 12586957528331976061742120551986636508845904030979/18109043016232145665506982814899693126548299*y^7 - 64366851687761482774460200012037221950912494746969/72436172064928582662027931259598772506193196*y^6 + 15962140624468183926984961121250646050423032532175/18109043016232145665506982814899693126548299*y^5 + 16952114725878154711686467219213497372990953140143/36218086032464291331013965629799386253096598*y^4 - 26576530305515496636506847521838977432241631684187/36218086032464291331013965629799386253096598*y^3 + 5326502609603671620222873815477063766675598255928/18109043016232145665506982814899693126548299*y^2 - 883515989885260622013838141485928304074768999229/18109043016232145665506982814899693126548299*y + 52213110490110705585360406402900619013349326099/18109043016232145665506982814899693126548299

22652655643742676934762547283354118305666069035/72436172064928582662027931259598772506193196*y^22 + 390344402334601418014341708999253966846682390355/36218086032464291331013965629799386253096598*y^21 + 6025005870077168857857252510002234177856600849451/72436172064928582662027931259598772506193196*y^20 + 9664854805720354161015085776681262412089740553999/36218086032464291331013965629799386253096598*y^19 + 17551587744501645425317601563716349588947119558721/72436172064928582662027931259598772506193196*y^18 - 10293802894660070557335150914167289506367950872972/18109043016232145665506982814899693126548299*y^17 - 53411715533782882347039532811496415362970337347925/36218086032464291331013965629799386253096598*y^16 - 52017360989076177958877853824839654552139378918595/36218086032464291331013965629799386253096598*y^15 - 29737198161527844749586874667670370347640155914547/72436172064928582662027931259598772506193196*y^14 + 387840170382583712255119013123681629084998735160085/72436172064928582662027931259598772506193196*y^13 + 182505383629521389119631044094928970961236211805391/36218086032464291331013965629799386253096598*y^12 - 94131019608464516189995878306169347961413268532028/18109043016232145665506982814899693126548299*y^11 - 109109387998199054647764263546878322128599856370019/18109043016232145665506982814899693126548299*y^10 + 130166015387725434134816360274421347945233410770537/36218086032464291331013965629799386253096598*y^9 - 144217831565129223099293155291862352298490511821497/72436172064928582662027931259598772506193196*y^8 + 183944129514019107282679083599008114515062484439957/72436172064928582662027931259598772506193196*y^7 + 223014588727649516689997755366263058131355054841179/72436172064928582662027931259598772506193196*y^6 - 118054279807744521218262409346827402756055703188187/36218086032464291331013965629799386253096598*y^5 - 29178005962517146927894626943721528356739111379312/18109043016232145665506982814899693126548299*y^4 + 96736171810995005447966938044844565181974018350121/36218086032464291331013965629799386253096598*y^3 - 19718461326837955169522782316673392207914105666727/18109043016232145665506982814899693126548299*y^2 + 3303404533734533367615031204688194011775654535551/18109043016232145665506982814899693126548299*y - 196257778786280373258317676169708071061395746254/18109043016232145665506982814899693126548299

-17027518546259146319089383575112079325660679261/36218086032464291331013965629799386253096598*y^22 - 1173570562741158555240405522644030019050872803019/72436172064928582662027931259598772506193196*y^21 - 2263699717720996390784063673442248025301678221181/18109043016232145665506982814899693126548299*y^20 - 7258833187682086665079069617197178704507444553368/18109043016232145665506982814899693126548299*y^19 - 6574892311379160712297466310785601433951949021020/18109043016232145665506982814899693126548299*y^18 + 62020983168088213073178912651520079452915315931291/72436172064928582662027931259598772506193196*y^17 + 80258968179171359666584221746833769452442777772139/36218086032464291331013965629799386253096598*y^16 + 155958990952679096218857278945201730421587327516627/72436172064928582662027931259598772506193196*y^15 + 11010194398603051862998584604279536912065378994759/18109043016232145665506982814899693126548299*y^14 - 291797479146007407324773670927451509520029639964409/36218086032464291331013965629799386253096598*y^13 - 547648451654847677979453008244513510987876594187965/72436172064928582662027931259598772506193196*y^12 + 284044667441478739399904646320621993792251936066335/36218086032464291331013965629799386253096598*y^11 + 656024286082420255811180084762968945014199567845977/72436172064928582662027931259598772506193196*y^10 - 98260076734501414846209672549381998221811330791842/18109043016232145665506982814899693126548299*y^9 + 216718577864489161480498451792491406604901281896391/72436172064928582662027931259598772506193196*y^8 - 277127995227059969239461701831190448271608762728011/72436172064928582662027931259598772506193196*y^7 - 83742305049252991559302191494822510252568609346931/18109043016232145665506982814899693126548299*y^6 + 88991981373641952807865578233515149020644557524875/18109043016232145665506982814899693126548299*y^5 + 87614315068010663479439854119484281656047819335521/36218086032464291331013965629799386253096598*y^4 - 72858346825320081435738968242505198983306227389931/18109043016232145665506982814899693126548299*y^3 + 29731584981923299117181302815772294910667150313703/18109043016232145665506982814899693126548299*y^2 - 4983732724187998765387928249842536345427943264566/18109043016232145665506982814899693126548299*y + 296292102258394408368181908670127752120090247872/18109043016232145665506982814899693126548299

22652655643742676934762547283354118305666069035/72436172064928582662027931259598772506193196*y^22 + 390344402334601418014341708999253966846682390355/36218086032464291331013965629799386253096598*y^21 + 6025005870077168857857252510002234177856600849451/72436172064928582662027931259598772506193196*y^20 + 9664854805720354161015085776681262412089740553999/36218086032464291331013965629799386253096598*y^19 + 17551587744501645425317601563716349588947119558721/72436172064928582662027931259598772506193196*y^18 - 10293802894660070557335150914167289506367950872972/18109043016232145665506982814899693126548299*y^17 - 53411715533782882347039532811496415362970337347925/36218086032464291331013965629799386253096598*y^16 - 52017360989076177958877853824839654552139378918595/36218086032464291331013965629799386253096598*y^15 - 29737198161527844749586874667670370347640155914547/72436172064928582662027931259598772506193196*y^14 + 387840170382583712255119013123681629084998735160085/72436172064928582662027931259598772506193196*y^13 + 182505383629521389119631044094928970961236211805391/36218086032464291331013965629799386253096598*y^12 - 94131019608464516189995878306169347961413268532028/18109043016232145665506982814899693126548299*y^11 - 109109387998199054647764263546878322128599856370019/18109043016232145665506982814899693126548299*y^10 + 130166015387725434134816360274421347945233410770537/36218086032464291331013965629799386253096598*y^9 - 144217831565129223099293155291862352298490511821497/72436172064928582662027931259598772506193196*y^8 + 183944129514019107282679083599008114515062484439957/72436172064928582662027931259598772506193196*y^7 + 223014588727649516689997755366263058131355054841179/72436172064928582662027931259598772506193196*y^6 - 118054279807744521218262409346827402756055703188187/36218086032464291331013965629799386253096598*y^5 - 29178005962517146927894626943721528356739111379312/18109043016232145665506982814899693126548299*y^4 + 96736171810995005447966938044844565181974018350121/36218086032464291331013965629799386253096598*y^3 - 19718461326837955169522782316673392207914105666727/18109043016232145665506982814899693126548299*y^2 + 3303404533734533367615031204688194011775654535551/18109043016232145665506982814899693126548299*y - 196257778786280373258317676169708071061395746254/18109043016232145665506982814899693126548299


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

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

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

# f Combinatorial flattening
{-9, 2, 4, -5, 0, 2, 2, -4}

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

# 1 Loop Invariant
-7254708443270847304397723520061666257302547995861/144872344129857165324055862519197545012386392*y^22 - 124988216933231364536393249872813554363848433430499/72436172064928582662027931259598772506193196*y^21 - 240993966452047408846746931882380322392290692849929/18109043016232145665506982814899693126548299*y^20 - 3088680713735469121475155956017467981046392237784259/72436172064928582662027931259598772506193196*y^19 - 5574206412087381849953562982310045903906431659375459/144872344129857165324055862519197545012386392*y^18 + 6624851250122050105486374405003249663198124275677729/72436172064928582662027931259598772506193196*y^17 + 34164841514782089662104869660791493926208070685501125/144872344129857165324055862519197545012386392*y^16 + 16537627721970190249459737957951816417933811314384123/72436172064928582662027931259598772506193196*y^15 + 2292807077255007135387769486722536149168972250406267/36218086032464291331013965629799386253096598*y^14 - 124476671251175798562741517860183237279094039934638979/144872344129857165324055862519197545012386392*y^13 - 58135793600040278852972031824142915897933781868314097/72436172064928582662027931259598772506193196*y^12 + 121686168864467934656492744719841872291896476522388483/144872344129857165324055862519197545012386392*y^11 + 17456853364288854927168778297417027392965658874075509/18109043016232145665506982814899693126548299*y^10 - 84317694537158476967560088256738079662842749017217557/144872344129857165324055862519197545012386392*y^9 + 46167600722138356598546804831485022407765754453609701/144872344129857165324055862519197545012386392*y^8 - 29608732667098557965659524337530557804992280516294483/72436172064928582662027931259598772506193196*y^7 - 17807887134133118357148185977002985544441744091440457/36218086032464291331013965629799386253096598*y^6 + 38087654145712190750660923107330693603721746838061699/72436172064928582662027931259598772506193196*y^5 + 9306384806278222927707551715330899703595441443860555/36218086032464291331013965629799386253096598*y^4 - 7785382790514324750158933228210617609179837191168461/18109043016232145665506982814899693126548299*y^3 + 3183121921859090384393026312565935657691880627512273/18109043016232145665506982814899693126548299*y^2 - 534214073537926243301087311709370873096585585651606/18109043016232145665506982814899693126548299*y + 31786944292127313684036924517897637013899120216736/18109043016232145665506982814899693126548299

# 2 Loop Invariant
1670033295753058994652487945971773615571463369816219560103252699998734392580172192476226852998837771039849326414752577/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^22 + 57546191374550092562282418306447408252131623252460089453877652816475114068674393686357332096133926696263607654989108423/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^21 + 221935533814373009710519415694587400709970378909840106198454858297424846781798610472971551102543061941251576647401883139/86069043637548711535600050775039697189412680822158662309675827828520804582294263759539757977674199381492884504610368*y^20 + 474158259738390755873415567155789288303596998484123958250161086188118665866320618318538833066967215098832468197547005503/57379362425032474357066700516693131459608453881439108206450551885680536388196175839693171985116132920995256336406912*y^19 + 1284663222653386569963544245107381911139798626800377686325608488574913977904062332914272460854999094688202186351714061963/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^18 - 3048563673699056682319817110947885570991050997695608981100987545323921798416773937822291243751090733418403297522026295229/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^17 - 7867614645764736342066579860570943125130174103030925153679042897078430106836308272855344843508108970851493075462714221861/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^16 - 3811282643881330537803305739117560211556862502886166760893351843068200085871606905963753498255690751628669458865671935981/86069043637548711535600050775039697189412680822158662309675827828520804582294263759539757977674199381492884504610368*y^15 - 265060222715757333401112008239991233669701835680231158797938564737820076408929078868066745836738781634245946067965926003/21517260909387177883900012693759924297353170205539665577418956957130201145573565939884939494418549845373221126152592*y^14 + 14325711134903927897488260702437746919167057508994198679311697279000078140600339201495633473560315798432909677667956526399/86069043637548711535600050775039697189412680822158662309675827828520804582294263759539757977674199381492884504610368*y^13 + 26794910258199303333498366430752691925602372392220697314984185756387678612011572512678834015654699950916168119415804407015/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^12 - 9325971309677225604428438323765201914570557162460624120821251912757213968598857101523247632533203462231238520675813654985/57379362425032474357066700516693131459608453881439108206450551885680536388196175839693171985116132920995256336406912*y^11 - 5361706929763733264928603505878963878630604692089296765355318265120705632760245919229358374616983913500664925295364068131/28689681212516237178533350258346565729804226940719554103225275942840268194098087919846585992558066460497628168203456*y^10 + 19368994985675275542401537534771329473779062116767045752478840752305131247028595070749954621799608297208329528257131765095/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^9 - 10619302012258722813723797096246209616019461030677521052791036745991062911117261454362276777381189319875251225021789101439/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^8 + 4541943451939159118665673083648798694217546589805837123678359913668550391784652111366842892019432091728926741494496216335/57379362425032474357066700516693131459608453881439108206450551885680536388196175839693171985116132920995256336406912*y^7 + 16410962592132366527541464033543188457996888033473632086899376201812775983369531130105806761987057309025700445443861455435/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^6 - 17514791670472039497593820697197892078977864669238096170626666204785718097323190102325901052968796776250095369501320131709/172138087275097423071200101550079394378825361644317324619351655657041609164588527519079515955348398762985769009220736*y^5 - 4290981376761070324174925220234105513450935776677062187705640675136134542077180821877010958639708295858197056163705285501/86069043637548711535600050775039697189412680822158662309675827828520804582294263759539757977674199381492884504610368*y^4 + 7162241639134964029846520929797139116569678610419263371536652483697088110961204729637684312442274505228022767907861815373/86069043637548711535600050775039697189412680822158662309675827828520804582294263759539757977674199381492884504610368*y^3 - 975193239054123793778033575832020770307594102766399001449838457913305170007208521928123345811153022170592544150318476775/28689681212516237178533350258346565729804226940719554103225275942840268194098087919846585992558066460497628168203456*y^2 + 15333667802401263681279395268841113273100954501468445835896862077856724055372871089739722115038244042631726984033509647/2689657613673397235487501586719990537169146275692458197177369619641275143196695742485617436802318730671652640769074*y - 14518069272492536251675004716599427519547568197963426494204228002654480114219335365525097539719702605050093986493362707/43034521818774355767800025387519848594706340411079331154837913914260402291147131879769878988837099690746442252305184

# 3 Loop Invariant
194737723333064531591524615976361003454853668406126101570221044232881476077222755790907436259849958627827737262564818317938528764623742652971854185565443/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^22 + 3354482163873340064151393159145728027176371373980660894424116808987690439302716837294304021926011829361759501092257203404845891509017913432996038005331923/18055554813442284471173983397561955203235552547850912557339009451186496467193012284370734357730704905269674729782684578321255233519568213910238704824064*y^21 + 103423679678630741756464652678548429962139582820782996272720129559664992680377743945133653664661874252070146004455733076993574029970679993793642855801677127/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^20 + 165487127875947645084154201187234209778367667303959555586462266412213535092727196634614340186243027426010837042279577353591602432805018287377926086154850159/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^19 + 74210327926635555391668901063247597743790887011467115345195295502294662321721718105422429465234659261065325620976909567763907814431706428801776512271594037/18055554813442284471173983397561955203235552547850912557339009451186496467193012284370734357730704905269674729782684578321255233519568213910238704824064*y^18 - 357399041446621282401584328691241482346651404730672859279073419407655498589755254463602706090934682248061695637775996605136221029830607467749299616344692647/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^17 - 1832467267976778676933927195724741453559211877108689165753011478448475427074275391839197197458680848186746755431620353083257220947456638944347298991855247729/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^16 - 881824688194047205775814639033579565329521776541030239158281238255476961898595955326216802154313599905194906393061957741343358587673981085028072108936244907/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^15 - 473327056018153215405772554331853559941468015514709932208029944662802892515777958616422688696300108018564358373332410719599239721104770287963252282655234505/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^14 + 1674755659117066361699107204558643311020302355039070550899293908886361976868434848346478392174237896559795678610200153449579260826682847491058735038996014721/18055554813442284471173983397561955203235552547850912557339009451186496467193012284370734357730704905269674729782684578321255233519568213910238704824064*y^13 + 3107230031631311807802473247534429088686304464120518016628136775805651772350000410562863034900119989049777768611512520450558798508434565704974258637569795645/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^12 - 6589676600042799780123312495767574371496668363115111184345022358079040894601474955925006633006967164045146409270504675302518640028195665668903173718729634069/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^11 - 3749959179359884811783597193623139926982447643897031705415362173268204101145022488622765794042988776320353684717322033474865864875173167022653157969884413627/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^10 + 4569810390183777365153196373124882633503383038741905809926739969262134327504776259860281058396139419225487745629776302138097889655403383919079594559740196555/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^9 - 1236746833500980866018146061051541317904906420388171042606673056311360118116196052863589876017993557202785718072811685475004686124796580015023430569907273817/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^8 + 3196772462063950759872148696740280804907230308799637565065753556659068204984550260506486952081676213101152469856806872589442497032305960032712866135472494521/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^7 + 3817906515518948448594786528787704960525947291973281487519351998088490860818382771713338293907247781071472319037017149730708557659391721226156168762076375169/72222219253769137884695933590247820812942210191403650229356037804745985868772049137482937430922819621078698919130738313285020934078272855640954819296256*y^6 - 1029199345510049717435620709372258296070025032718289797850775783762089240253299874278313792970935574935976178503790231245573176580050514673645048351103323007/18055554813442284471173983397561955203235552547850912557339009451186496467193012284370734357730704905269674729782684578321255233519568213910238704824064*y^5 - 997127243425130713377880829560730468445448604198319273200601049997718224364952739504396187893495262387557165965862092205507560644146097571523332901987341307/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^4 + 1679433457781412010732065405346335082296996975572602179841665210699302984333310141515936735945060960087096878189487219747385709154578046196642759454897586075/36111109626884568942347966795123910406471105095701825114678018902372992934386024568741468715461409810539349459565369156642510467039136427820477409648128*y^3 - 21494538313173172714697506779747910977710965104521061738054292376887700522685240657511665682250123209085834312191747373347736759062574699118727539620846271/1128472175840142779448373962347622200202222034240682034833688090699156029199563267773170897358169056579354670611417786145078452094973013369389919051504*y^2 + 57772836015923615758264123326597236293861640769052679097172032619917879517089230694438918304195522481223537153191041135297322737457664810064166169975600417/18055554813442284471173983397561955203235552547850912557339009451186496467193012284370734357730704905269674729782684578321255233519568213910238704824064*y - 859772150816911423137740857482434206504088815393124278021524854796855700801126279594739710653536800488955067420309038200461294481097031819508316783962735/4513888703360571117793495849390488800808888136962728139334752362796624116798253071092683589432676226317418682445671144580313808379892053477559676206016

# 4 Loop Invariant
-433991021559719079348631705403725357232875810750267760824124717834378781283973852724817452173668083671302825345490339463397505243713040227471729940412483825743867118820422413357894706583701593233150718163460904014389715484531/143024706288579868429333642750937294413522325981202066652992539803144641122206652590588837554697428757129794699179043921035744055842037124925410698847023219296281744127838829696626469188440743728306023686365924029999595438080*y^22 - 269181846967335309243984022135164576200356798658059760557567657496393443950231762932193546868220218282343362361497908477636797383759329189759086948025444855731144049241849822495626444943203307105124027241832747802744757746625031/2574444713194437631728005569516871299443401867661637199753865716456603540199719746630599075984553717628336304585222790578643393005156668248657392579246417947333071394301098934539276445391933387109508426354586632539992717885440*y^21 - 1038149624668914656962675630755484865027631217362148154679681607761065526374262273676223767268196356129983455219210970970317162431955429650997608124642952872660470076823715657416442457913815242625413746290751022047509205724711521/1287222356597218815864002784758435649721700933830818599876932858228301770099859873315299537992276858814168152292611395289321696502578334124328696289623208973666535697150549467269638222695966693554754213177293316269996358942720*y^20 - 3327030449901152207831461925357334532625104467902324864806049447384086891201349910324562537054272590367212811559436341219160012697260455906047866764206615941916386249864784203504336721953764755777546328649946651356185278148439131/1287222356597218815864002784758435649721700933830818599876932858228301770099859873315299537992276858814168152292611395289321696502578334124328696289623208973666535697150549467269638222695966693554754213177293316269996358942720*y^19 - 375631821521049523142822220201016285858797018099041644219288033810719303356700653501520954742198067844143552211423246684400232464168833700512691956485270471678113799737503933896936912899059966170527571261673613618178053876719703/160902794574652351983000348094804456215212616728852324984616607278537721262482484164412442249034607351771019036576424411165212062822291765541087036202901121708316962143818683408704777836995836694344276647161664533749544867840*y^18 + 14258379053917162031598646589544199216063064665971061084653640663319955315859948417964613734185296114466362469115416578748194267949846807331113130177726239138260883582722698700396081079332521529247461113815203833395497974328756619/2574444713194437631728005569516871299443401867661637199753865716456603540199719746630599075984553717628336304585222790578643393005156668248657392579246417947333071394301098934539276445391933387109508426354586632539992717885440*y^17 + 4600169480452347672830705839591269954936504418040960109196150502062786599749668223425534160846214855946177255607908938669991788215501345667118348115847846529964994261019253035013416358674044920354411760656281085839954725695625041/321805589149304703966000696189608912430425233457704649969233214557075442524964968328824884498069214703542038073152848822330424125644583531082174072405802243416633924287637366817409555673991673388688553294323329067499089735680*y^16 + 11886533632435319847121335071114659147498166912649232437676483238325090607641493652783533642879251482921025345645372884590268961338519098694329113787420364636853114426685440173967029561237385419945421959612591333235283307591038499/858148237731479210576001856505623766481133955887212399917955238818867846733239915543533025328184572542778768195074263526214464335052222749552464193082139315777690464767032978179758815130644462369836142118195544179997572628480*y^15 + 1654675907170130801656634756592332648220883809663050347938135090663567239315961922039409060784400523370187042034687262168943466197382320989474758026223720107252333443317393152152493866333067137998183236736308871246774159572712677/429074118865739605288000928252811883240566977943606199958977619409433923366619957771766512664092286271389384097537131763107232167526111374776232096541069657888845232383516489089879407565322231184918071059097772089998786314240*y^14 - 8375663242145366194733235954280226072869635481995816937590686531362012179473218534397621846577540837613155998977150655617745407813430550370864403830445381551611006360040089216342802416855213386714391207673077224124750145012593829/160902794574652351983000348094804456215212616728852324984616607278537721262482484164412442249034607351771019036576424411165212062822291765541087036202901121708316962143818683408704777836995836694344276647161664533749544867840*y^13 - 125339853084607746615405479713405308714086819975689462969873487770758206407557008307490917624344112119568120187207648065486132271411250453532206394432163787965645363024107076410759399340162074258136885926065839700956313381020827293/2574444713194437631728005569516871299443401867661637199753865716456603540199719746630599075984553717628336304585222790578643393005156668248657392579246417947333071394301098934539276445391933387109508426354586632539992717885440*y^12 + 16355844937951081918639000201700201322868457300410171179972090095154276160055239741736295609816399743745737622676519574920178884936939995294190482321051920232708159468456499115443801905741224800968329170579843918982639226154396501/321805589149304703966000696189608912430425233457704649969233214557075442524964968328824884498069214703542038073152848822330424125644583531082174072405802243416633924287637366817409555673991673388688553294323329067499089735680*y^11 + 150462485348065599893500593458573729053262443461990082474781344704225500786611045003133229210867587543880633383888600962735549707648546848590679833394539458532685544659893182928411436693159794128079852936264003142014986878671109159/2574444713194437631728005569516871299443401867661637199753865716456603540199719746630599075984553717628336304585222790578643393005156668248657392579246417947333071394301098934539276445391933387109508426354586632539992717885440*y^10 - 45295805592783926170919035773097758143976425464621175531001523198721289370527262909868445037077835255160084965173898532781475069394038868999465878294708894118266151087522248990464538459914266506730157822066172232827962493695878893/1287222356597218815864002784758435649721700933830818599876932858228301770099859873315299537992276858814168152292611395289321696502578334124328696289623208973666535697150549467269638222695966693554754213177293316269996358942720*y^9 + 49688108642535977967037729678408644708443509482147672208077409958734494588287530532482712542293940083846458673023675663416425559839162102534201511458950917877097454544512591921374397630425479341856901179967256009413161682208985741/2574444713194437631728005569516871299443401867661637199753865716456603540199719746630599075984553717628336304585222790578643393005156668248657392579246417947333071394301098934539276445391933387109508426354586632539992717885440*y^8 - 21242837847548372368913811278218547933835661280179604846472296834538717712267286786571645839356797942946894678168977009612135077447121109270147667028587797323447268870142470710432747673928491283773197550366098179846425330857939443/858148237731479210576001856505623766481133955887212399917955238818867846733239915543533025328184572542778768195074263526214464335052222749552464193082139315777690464767032978179758815130644462369836142118195544179997572628480*y^7 - 9595169097189495256037771581663832531672664873209068511983785167719612721745118504628118898894349996097049194836231548350915556670860582743767423041268000307805942258066405569857881049737591113738722248151028171705373654857319621/321805589149304703966000696189608912430425233457704649969233214557075442524964968328824884498069214703542038073152848822330424125644583531082174072405802243416633924287637366817409555673991673388688553294323329067499089735680*y^6 + 40959438288918904745967190553783868230203052331297025819977874137190457519810519691083270510369178000347103390778875874481799087168185133203017882023661983631452607475061831452152291286956793868846034854447657260170007876123535929/1287222356597218815864002784758435649721700933830818599876932858228301770099859873315299537992276858814168152292611395289321696502578334124328696289623208973666535697150549467269638222695966693554754213177293316269996358942720*y^5 + 4013605136432129919215838933490543258280064068438623899883138012781766115180880871473702105982185129786458146969518669783399779075835825839486722921463997018105702426180494300448606877164571063193518186567464776111017687369576113/257444471319443763172800556951687129944340186766163719975386571645660354019971974663059907598455371762833630458522279057864339300515666824865739257924641794733307139430109893453927644539193338710950842635458663253999271788544*y^4 - 8375050847417780248490464242773100803300391474318056203836201122554931585569322509235149800914745255840239937816275231401223493401188989125488111934473433774675531128457867018243663986357948738998442032854645106209362287722501431/321805589149304703966000696189608912430425233457704649969233214557075442524964968328824884498069214703542038073152848822330424125644583531082174072405802243416633924287637366817409555673991673388688553294323329067499089735680*y^3 + 6843007364254554890288152815089072272535549431912780689869586114398402213179750260551901370420037861135213010349927184040417258479848897556203508390726481327221732197186766146571051651222838493799435930862983521838621607819392867/643611178298609407932001392379217824860850466915409299938466429114150885049929936657649768996138429407084076146305697644660848251289167062164348144811604486833267848575274733634819111347983346777377106588646658134998179471360*y^2 - 95663369845791778454086071449896489436418583305440330337111920654076563628714425269271880701803901716560036410192663025768022867050587544206429775670744829856948304457550425420762390644716421609497490716271812702909310670891543/53634264858217450661000116031601485405070872242950774994872202426179240420827494721470814083011535783923673012192141470388404020940763921847029012067633707236105654047939561136234925945665278898114758882387221511249848289280*y + 3414143891669870233062743583763839274667627932557592038147333974413537121065737528005856043583467124102628523063259340794437771745893546259263014956000606225953782909787444995735647166197786211339799473573767104338988986262943/32180558914930470396600069618960891243042523345770464996923321455707544252496496832882488449806921470354203807315284882233042412564458353108217407240580224341663392428763736681740955567399167338868855329432332906749908973568