# Manifold: Census Knot K8_267

# Number of Tetrahedra: 8

# Number Field
x^23 - 3*x^22 - 8*x^21 + 67*x^20 - 80*x^19 - 155*x^18 + 706*x^17 - 961*x^16 + 130*x^15 + 1100*x^14 - 1518*x^13 + 536*x^12 - 236*x^11 + 1213*x^10 - 2522*x^9 + 2910*x^8 - 1864*x^7 + 776*x^6 - 326*x^5 + 162*x^4 - 36*x^3 + 2*x^2 - 6*x - 1 

# Approximate Field Generator
0.547224835195605 + 0.436368565102190*I

# Shape Parameters
1372847470367978080606290475041417711/4702799128018807901654947400179302569*y^22 - 4589974273055300363380680452318837461/4702799128018807901654947400179302569*y^21 - 9260933679913228455630463794758761813/4702799128018807901654947400179302569*y^20 + 95057645300131401514513873765704040295/4702799128018807901654947400179302569*y^19 - 144403049315116437278703556487883989155/4702799128018807901654947400179302569*y^18 - 156598130573875234738901136515831508109/4702799128018807901654947400179302569*y^17 + 1031388377756974877407900740224164653946/4702799128018807901654947400179302569*y^16 - 1709265798613764353656543478412499629636/4702799128018807901654947400179302569*y^15 + 810419801927960574405039624613237098018/4702799128018807901654947400179302569*y^14 + 1285563233610903935957904729455153895085/4702799128018807901654947400179302569*y^13 - 2701996593944994526483941121732818627264/4702799128018807901654947400179302569*y^12 + 1759677820628991278873398183397578010339/4702799128018807901654947400179302569*y^11 - 850150052739840616860035504811631251877/4702799128018807901654947400179302569*y^10 + 1714948345518472709921301287185847730431/4702799128018807901654947400179302569*y^9 - 4079928048679777297111438085689472070790/4702799128018807901654947400179302569*y^8 + 5460732491953311024621813605725209739121/4702799128018807901654947400179302569*y^7 - 4493623911956231742593305621143023266229/4702799128018807901654947400179302569*y^6 + 2399970157110093747886392423990174891354/4702799128018807901654947400179302569*y^5 - 966369373428647549095746635793120500609/4702799128018807901654947400179302569*y^4 + 364569191235238638446030896979147176317/4702799128018807901654947400179302569*y^3 - 110213123758708381367021786091262822163/4702799128018807901654947400179302569*y^2 + 23327314843723829138170525789497304608/4702799128018807901654947400179302569*y - 2843818942214080919426943705567822089/4702799128018807901654947400179302569

-2456935864008972085915976822295564835/4702799128018807901654947400179302569*y^22 + 5474099075375809555994524087222136456/4702799128018807901654947400179302569*y^21 + 23585290224324308761332313244678420278/4702799128018807901654947400179302569*y^20 - 145592130267146290061502840153964921944/4702799128018807901654947400179302569*y^19 + 86761152231763213576353831269063384279/4702799128018807901654947400179302569*y^18 + 428470794775826158616543949196802479935/4702799128018807901654947400179302569*y^17 - 1385055980099239857079789369074242639651/4702799128018807901654947400179302569*y^16 + 1344885476581388590515011839277062991765/4702799128018807901654947400179302569*y^15 + 517768482159785832285861480853398986668/4702799128018807901654947400179302569*y^14 - 2071166399785127814589190876190536523883/4702799128018807901654947400179302569*y^13 + 2179191527100948734303241274349678080084/4702799128018807901654947400179302569*y^12 - 3306944136857764323263750050710757797/4702799128018807901654947400179302569*y^11 + 963532448975069574426335982186340288974/4702799128018807901654947400179302569*y^10 - 2252743732769387761635392079126441437037/4702799128018807901654947400179302569*y^9 + 4434572960402237732149759558111905260906/4702799128018807901654947400179302569*y^8 - 4036143177454336028851849964656451257077/4702799128018807901654947400179302569*y^7 + 2135638777584012358074915969461897140729/4702799128018807901654947400179302569*y^6 - 906753059506421176267495985660646951431/4702799128018807901654947400179302569*y^5 + 371942849717166977036109117746408633666/4702799128018807901654947400179302569*y^4 - 99214455205633184539827561657069664035/4702799128018807901654947400179302569*y^3 - 15058693918038368224072549518809765711/4702799128018807901654947400179302569*y^2 - 21617301648397252431067145165187477886/4702799128018807901654947400179302569*y - 3901336054588459484754764934057769556/4702799128018807901654947400179302569

1348155780591063824369342590144673437/4702799128018807901654947400179302569*y^22 - 3277329202732266633301103183735576296/4702799128018807901654947400179302569*y^21 - 12260345743504804205489786632523916471/4702799128018807901654947400179302569*y^20 + 82307651547494118313776450172116514415/4702799128018807901654947400179302569*y^19 - 64335327828574275915260735045157179395/4702799128018807901654947400179302569*y^18 - 220886373882505243218631867786621675167/4702799128018807901654947400179302569*y^17 + 801675580420610880883743872132916567064/4702799128018807901654947400179302569*y^16 - 899042798230286441455388758833586826332/4702799128018807901654947400179302569*y^15 - 87378157423445175608328476319323194170/4702799128018807901654947400179302569*y^14 + 1114376909981157198782418120041025849366/4702799128018807901654947400179302569*y^13 - 1377810727771671749010743289537295399988/4702799128018807901654947400179302569*y^12 + 287748693843383484475516124747789975094/4702799128018807901654947400179302569*y^11 - 667057821350856054716641203463115946876/4702799128018807901654947400179302569*y^10 + 1453538836811402991366891053393366784569/4702799128018807901654947400179302569*y^9 - 2749832687740980290790814519266765780248/4702799128018807901654947400179302569*y^8 + 2757145995571584855363855657028672468263/4702799128018807901654947400179302569*y^7 - 1804633131938498110081594792509018715329/4702799128018807901654947400179302569*y^6 + 1018558050790378202858454938869275625808/4702799128018807901654947400179302569*y^5 - 554245501875311331612679489016604976781/4702799128018807901654947400179302569*y^4 + 227159552363718933097989815922253605854/4702799128018807901654947400179302569*y^3 - 31123721218058571459954520970451188826/4702799128018807901654947400179302569*y^2 + 20034398580765963754913869229690137491/4702799128018807901654947400179302569*y - 1530808289971643703592641177723596404/4702799128018807901654947400179302569

-3177608893252538270751226827161746267/4702799128018807901654947400179302569*y^22 + 10629579266971607441304753884329300552/4702799128018807901654947400179302569*y^21 + 22730940749007617480854769643594798571/4702799128018807901654947400179302569*y^20 - 223544940068253055682660872282287280066/4702799128018807901654947400179302569*y^19 + 323284723563686672408691968197874804020/4702799128018807901654947400179302569*y^18 + 445141843124523905666132854332563522696/4702799128018807901654947400179302569*y^17 - 2467921969456058836310253080871684850278/4702799128018807901654947400179302569*y^16 + 3751855257101334924454879662309597628677/4702799128018807901654947400179302569*y^15 - 1039318034806389344391240374946202105453/4702799128018807901654947400179302569*y^14 - 4014693536758129067491366258412917993810/4702799128018807901654947400179302569*y^13 + 6285356414131645503092167269390020537172/4702799128018807901654947400179302569*y^12 - 2817009731553741213627114891085009465394/4702799128018807901654947400179302569*y^11 + 283971367594292540932321322717807513256/4702799128018807901654947400179302569*y^10 - 3490978493215845858912608278154759667411/4702799128018807901654947400179302569*y^9 + 9000915694080265225626233801223248701741/4702799128018807901654947400179302569*y^8 - 11308964088641797712656930711321964302756/4702799128018807901654947400179302569*y^7 + 7497607356359017741968610466954053750394/4702799128018807901654947400179302569*y^6 - 2404489171833116951362639056537256449370/4702799128018807901654947400179302569*y^5 + 231810832429357941745378262966147312291/4702799128018807901654947400179302569*y^4 + 2248398470316844043719054156639004475/4702799128018807901654947400179302569*y^3 - 28363818858630272881219996994126995749/4702799128018807901654947400179302569*y^2 + 57781637259558951675974243822372453411/4702799128018807901654947400179302569*y + 5639609706293545797732849957195448871/4702799128018807901654947400179302569

-1352381912745556789623355016308121343/4702799128018807901654947400179302569*y^22 + 3064727608255144260939238306667564052/4702799128018807901654947400179302569*y^21 + 13189402570781675837620340941747142638/4702799128018807901654947400179302569*y^20 - 81369129529760488298854471181204583279/4702799128018807901654947400179302569*y^19 + 47698870820258720750330793919594356772/4702799128018807901654947400179302569*y^18 + 253414980996682718058445832977371436014/4702799128018807901654947400179302569*y^17 - 783198506448699030372825334344204613184/4702799128018807901654947400179302569*y^16 + 710204436965685183379389236384021997185/4702799128018807901654947400179302569*y^15 + 443602611410787182526058842815792272677/4702799128018807901654947400179302569*y^14 - 1326558622179951168673850252113447242940/4702799128018807901654947400179302569*y^13 + 1150202345146816320721086233578048013179/4702799128018807901654947400179302569*y^12 + 262046812404696296187260225733180370113/4702799128018807901654947400179302569*y^11 + 241815529990476155729528466052138856200/4702799128018807901654947400179302569*y^10 - 1298347185864847510839646147641644188666/4702799128018807901654947400179302569*y^9 + 2420900736531369523250442071145415105844/4702799128018807901654947400179302569*y^8 - 2015214090548906419914511566045180992246/4702799128018807901654947400179302569*y^7 + 677247851708608374135319223676955329944/4702799128018807901654947400179302569*y^6 - 35641933136880198793310658445543522758/4702799128018807901654947400179302569*y^5 + 29863496605819048695889322138561477243/4702799128018807901654947400179302569*y^4 - 39947571694224696552337408713555038917/4702799128018807901654947400179302569*y^3 - 17012568595272154599443605148569216282/4702799128018807901654947400179302569*y^2 - 4306964112262032979405484585454821858/4702799128018807901654947400179302569*y + 4144780946885090581895842180030625761/4702799128018807901654947400179302569

2978925440232183557279468581363002783/23513995640094039508274737000896512845*y^22 - 10438545291565882898314478102269646677/23513995640094039508274737000896512845*y^21 - 20406029117683673969898793476070357832/23513995640094039508274737000896512845*y^20 + 214201926998891363848628989224450154068/23513995640094039508274737000896512845*y^19 - 328814636204437282902644302170909604728/23513995640094039508274737000896512845*y^18 - 407831825503660113572540588216421478362/23513995640094039508274737000896512845*y^17 + 476732544775524771982735644309995456123/4702799128018807901654947400179302569*y^16 - 3730805391963164707070856535534945055968/23513995640094039508274737000896512845*y^15 + 1183137212856367516707763301188993674628/23513995640094039508274737000896512845*y^14 + 3746938694924768026120285637584921606947/23513995640094039508274737000896512845*y^13 - 5953030208999645912700787175549460751626/23513995640094039508274737000896512845*y^12 + 2844875349976661412348170944336152582199/23513995640094039508274737000896512845*y^11 - 457179982605734926413234084607452444642/23513995640094039508274737000896512845*y^10 + 3954574665944190561138944469218749523096/23513995640094039508274737000896512845*y^9 - 9036921689270588632756672849595085349227/23513995640094039508274737000896512845*y^8 + 11339284342696728551874829068104379326892/23513995640094039508274737000896512845*y^7 - 7847574718279293829481967339070269929989/23513995640094039508274737000896512845*y^6 + 3158003560002404559532646144334606282037/23513995640094039508274737000896512845*y^5 - 234154103745936231440823395022047930016/4702799128018807901654947400179302569*y^4 + 639762293789885208243237960151184856996/23513995640094039508274737000896512845*y^3 - 188258092895621888884033147308925819579/23513995640094039508274737000896512845*y^2 + 1656731802706865814299638455790485865/4702799128018807901654947400179302569*y - 14581624484749316612606774481024978838/23513995640094039508274737000896512845

-1128616838538707723144463075215316923/4702799128018807901654947400179302569*y^22 + 3148296478857856909575627916479278084/4702799128018807901654947400179302569*y^21 + 9610760071877936143491994472748017829/4702799128018807901654947400179302569*y^20 - 73507284091869854327208061774132176803/4702799128018807901654947400179302569*y^19 + 75840404895994331121641708524043050920/4702799128018807901654947400179302569*y^18 + 186944706662406418068540244863466432932/4702799128018807901654947400179302569*y^17 - 760555137596821274979187764547522781258/4702799128018807901654947400179302569*y^16 + 943922206772258897096249344821485413827/4702799128018807901654947400179302569*y^15 + 23030614974643136578068229894876507636/4702799128018807901654947400179302569*y^14 - 1252233343985003933442552509448934348224/4702799128018807901654947400179302569*y^13 + 1533946279256588668216926842942152089912/4702799128018807901654947400179302569*y^12 - 336454864186257025732635239285256470205/4702799128018807901654947400179302569*y^11 + 168887015419765689133938056344167993880/4702799128018807901654947400179302569*y^10 - 1228750156550940748676831301725630105597/4702799128018807901654947400179302569*y^9 + 2605297052262453183097705609117624331741/4702799128018807901654947400179302569*y^8 - 2793126499812027272978334161768003944401/4702799128018807901654947400179302569*y^7 + 1560698060596250268137228792790841171238/4702799128018807901654947400179302569*y^6 - 493353043758241464450703057453714564956/4702799128018807901654947400179302569*y^5 + 130742688296636232080360886034980348290/4702799128018807901654947400179302569*y^4 - 77266647563047823183700967280461352435/4702799128018807901654947400179302569*y^3 + 11278540009235459199039110362102063782/4702799128018807901654947400179302569*y^2 + 3377417905815834543303520031537234798/4702799128018807901654947400179302569*y + 972509050556591944119867879488825844/4702799128018807901654947400179302569

-17926106469199017166842040689540914329/23513995640094039508274737000896512845*y^22 + 54330153353756965089085256887177142461/23513995640094039508274737000896512845*y^21 + 141521157091259363758037365575811860666/23513995640094039508274737000896512845*y^20 - 1205054968461750018739720747510429228994/23513995640094039508274737000896512845*y^19 + 1473518376559392186682805734487954117144/23513995640094039508274737000896512845*y^18 + 2721828001454327147762790708144709083036/23513995640094039508274737000896512845*y^17 - 2547956507899714828442514051356709629651/4702799128018807901654947400179302569*y^16 + 17659070353624050303399409756547131860539/23513995640094039508274737000896512845*y^15 - 2964651326900372150360097246877439019254/23513995640094039508274737000896512845*y^14 - 19585817318471019747908688228851109316956/23513995640094039508274737000896512845*y^13 + 27898316821328707580318700596159097623158/23513995640094039508274737000896512845*y^12 - 10534303609950305662039430096161741202137/23513995640094039508274737000896512845*y^11 + 4556016924136818454687228365221625006731/23513995640094039508274737000896512845*y^10 - 21809593291692268744630148466155758627388/23513995640094039508274737000896512845*y^9 + 46117714993706330994263577529587143167591/23513995640094039508274737000896512845*y^8 - 53864379286675650278412008743355546045541/23513995640094039508274737000896512845*y^7 + 35354947518922348366319802549613897812982/23513995640094039508274737000896512845*y^6 - 15145177405775322027471126911319691377326/23513995640094039508274737000896512845*y^5 + 1291498721303186181480226829594811839219/4702799128018807901654947400179302569*y^4 - 3353038487443854062562684508062151576948/23513995640094039508274737000896512845*y^3 + 983339050697459117629333829117508719172/23513995640094039508274737000896512845*y^2 - 33866311504022474687942465800484633821/4702799128018807901654947400179302569*y + 141035347602320116330277432715516398999/23513995640094039508274737000896512845


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

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

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

# f Combinatorial flattening
{4, -6, 1, 14, 8, -6, 8, -6}

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

# 1 Loop Invariant
-25726076524664059466568334869152689827/4702799128018807901654947400179302569*y^22 + 83157592939423519375926453187424538609/4702799128018807901654947400179302569*y^21 + 186798074141016567282225278161172838846/4702799128018807901654947400179302569*y^20 - 1768922042043345428513291708476637028229/4702799128018807901654947400179302569*y^19 + 2469550265516738335511326761647216060222/4702799128018807901654947400179302569*y^18 + 3441886373908542754301503495373474928855/4702799128018807901654947400179302569*y^17 - 19050493214285000207301613790388132259696/4702799128018807901654947400179302569*y^16 + 29181477357049302506022955662118816694645/4702799128018807901654947400179302569*y^15 - 9758318705770256591962846957533451046126/4702799128018807901654947400179302569*y^14 - 27014233383718089696330739435337126707282/4702799128018807901654947400179302569*y^13 + 46309006954370826784134627832419758353402/4702799128018807901654947400179302569*y^12 - 24286911975211143728761069658564801785053/4702799128018807901654947400179302569*y^11 + 10044652740715878765145870202907937256620/4702799128018807901654947400179302569*y^10 - 31849894606472918886328106773532462992375/4702799128018807901654947400179302569*y^9 + 71805730601019600959739869545370469798673/4702799128018807901654947400179302569*y^8 - 91251166684899606088673977322169874842236/4702799128018807901654947400179302569*y^7 + 67182977013105127027640866696424437295621/4702799128018807901654947400179302569*y^6 - 32225145918625756316905548699534987857267/4702799128018807901654947400179302569*y^5 + 12607014069238073442599234994385630412645/4702799128018807901654947400179302569*y^4 - 5319822270212868064603860428447024980144/4702799128018807901654947400179302569*y^3 + 1748332210538941444788928205553304185929/4702799128018807901654947400179302569*y^2 - 177389712216828612985470181230922063706/4702799128018807901654947400179302569*y + 105006412045207253416427529521935473375/4702799128018807901654947400179302569

# 2 Loop Invariant
689234697555906377229730585769808008010103311259624043267597547022899141221219261646086385918284587768105/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^22 - 270487026329759883007323602876856356789913686798159007376925083391105825935833291802167978986321189321975/1246337750007803580829644793687653177285598766904223909905433677296500798018843256530136216762542742457654*y^21 - 2637612376141137323617754869504291145315944444192993408872835664780521603352138042762314827462061890814747/4985351000031214323318579174750612709142395067616895639621734709186003192075373026120544867050170969830616*y^20 + 15690440642781406217286067635567318953603457950795633072747248243720837717772451815141133144863508313259045/3323567333354142882212386116500408472761596711744597093081156472790668794716915350747029911366780646553744*y^19 - 10185918271234524959468974398782434234144337988082468037632760430270653548344221951712781680359239430320667/1661783666677071441106193058250204236380798355872298546540578236395334397358457675373514955683390323276872*y^18 - 17039233568730275033401304951371693143397785977822352831281379780830173920205220929791673914316454478904609/1661783666677071441106193058250204236380798355872298546540578236395334397358457675373514955683390323276872*y^17 + 83968238933820260781699327829667310033943868187120477600770206113112188699928514044117021313896824470504387/1661783666677071441106193058250204236380798355872298546540578236395334397358457675373514955683390323276872*y^16 - 30047149755808126815048337152151729703530545341553929256996343254047905641112500314221347487762502908691625/415445916669267860276548264562551059095199588968074636635144559098833599339614418843378738920847580819218*y^15 + 151715961095774858642258131267973277551634684711371917094410759931575339266821112820319880159742894453013779/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^14 + 776600741291541135790357604533774797810392048630565702921251393682200838095057275869779740304358370499084399/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^13 - 570295568337071464997503218474383446757816619540357861297746569774140193536645018515779645740433864110073283/4985351000031214323318579174750612709142395067616895639621734709186003192075373026120544867050170969830616*y^12 + 116702843033632909078123656410206047867901632854314077244722027465960846775898567323564762693010279403555481/2492675500015607161659289587375306354571197533808447819810867354593001596037686513060272433525085484915308*y^11 - 168041467335800436826026284730207251204992592163078336480611757084815641964487281775597007950178876190000243/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^10 + 286673713112735828828200516745455384343126497835938642993673089051344233715949095201274351986656634081434297/3323567333354142882212386116500408472761596711744597093081156472790668794716915350747029911366780646553744*y^9 - 1841426934860699391858914728425694289605563632907700228457587485383313218030107756403516696344441273348174465/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^8 + 136867049285940610655314196098905822392682028728272272531269415691402410502700600284024562010845486412538641/623168875003901790414822396843826588642799383452111954952716838648250399009421628265068108381271371228827*y^7 - 1468833869846826573143181206451109227323129720112451811282652162629461349756538253227915818123503629570134225/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^6 + 156101060337535852967463220654177917786255578435183139743923794270299784282256317033121663666394105720929721/2492675500015607161659289587375306354571197533808447819810867354593001596037686513060272433525085484915308*y^5 - 257496195523739243749625239976142190792478125670053852450552038329421440389686511538814776309597646440117329/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^4 + 63089999113028375514412703020452446061215557686239684331536969046708355084388331781857110541539594867787619/4985351000031214323318579174750612709142395067616895639621734709186003192075373026120544867050170969830616*y^3 - 27645250156838366749858745400785645670307555458852155563303828031259573676656591542694666339301415134619297/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y^2 + 448083712285649205526335792912139426320978776644011012280060301891637823645878312170339483792054782555627/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232*y + 112180389569493216073290676496791447316184673753292728356390343383057987815687260609929628492481665077131015/9970702000062428646637158349501225418284790135233791279243469418372006384150746052241089734100341939661232

# 3 Loop Invariant
-144819826678407840324090090917101665408984597874001253308521146375926338576828708021118801181317409261328488280924131593547875606896367557/2761077073138894219826094796877035631711767145832288646217665961370016622642101146755589559605812905595485500613664075784092510547802419442*y^22 + 14468928937509202724177745527505269914993937293556034965263651267026298330094943737045347659657068416106222259965441099345652822498451822335/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^21 + 35326358712872007998435496079985585940925995312061713569214091758342960498523543754430844570369247548053776751547026254782679656637433962339/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^20 - 314788072200718774986400238847300763840145838632193683261538217086982969854077690275190158796788702786072402033423234295746314774480837578729/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^19 + 204417991096819455729241485130575412307328723188124276823970480377848306241020090664357098051671577549238692210891589030564797351654974270759/44177233170222307517217516750032570107388274333316618339482655381920265962273618348089432953693006489527768009818625212545480168764838711072*y^18 + 668950256424720033306758193978768018206718069773014611156807766186319855757566974907747638354804927105605671884155587083039633739230275992205/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^17 - 3350040662280479241663981842300262123226688213829841347341021531631054413737341963205094910568321661789571043241353420018485184612971310222239/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^16 + 1213952562214587453137155376290440527316986791716955160174454674781438676367114049705321619352483385946021840850538545260078383022094310468639/22088616585111153758608758375016285053694137166658309169741327690960132981136809174044716476846503244763884004909312606272740084382419355536*y^15 - 1195649139118051406815469483505113289261187113905720516859115113752844445278216490644083963664093189747181866559698540943951872339959295790063/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^14 - 615175874812477373354709527343997556201687640742481558242785265668999308092707872334852274733173370325148109278448976678023775900502285820733/11044308292555576879304379187508142526847068583329154584870663845480066490568404587022358238423251622381942002454656303136370042191209677768*y^13 + 7585009093998768429455345582015976242360001750980326268517944486903951059452111587959941280965448437373530614649925587109788422328143601356575/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^12 - 849914939333398221046903366302759261493371353917026559091078602961159203614029858772322538533394361910427890445013582957830815108519684261885/22088616585111153758608758375016285053694137166658309169741327690960132981136809174044716476846503244763884004909312606272740084382419355536*y^11 + 1553684817949019370600533085851891549655595539991504906449179746754742510986156987793739040428256951451853932108550867879140150289847817542153/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^10 - 5886358781205233669100665937776924278730064987299043363301706884227775467086677140492538530519382876714831106286271068335969787064704103670655/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^9 + 3103633976337855980648125782933476224492770999378771063248236722739956174246088514887462496584909868039301880391154399877595680980728461368001/22088616585111153758608758375016285053694137166658309169741327690960132981136809174044716476846503244763884004909312606272740084382419355536*y^8 - 7503114991923394776861882888661566947958801692630086837248927111712430599330851880382000665502722826239544413878774448172749656285822483656549/44177233170222307517217516750032570107388274333316618339482655381920265962273618348089432953693006489527768009818625212545480168764838711072*y^7 + 1312774759416392525880466939074388758637656163075465161055625044354978500430107038618577130703783500094077533635887891857215595523586861731073/11044308292555576879304379187508142526847068583329154584870663845480066490568404587022358238423251622381942002454656303136370042191209677768*y^6 - 4978876433288237880569513062308692010876472159976707835468702565906288029713370842319439983101955383440229083582786496886108628881322241895125/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^5 + 1122849605177428509487319584342693359864771122954543558519813583126710591434271227693900290037387101832526918461819426519602844101978947529501/44177233170222307517217516750032570107388274333316618339482655381920265962273618348089432953693006489527768009818625212545480168764838711072*y^4 - 1100975866307732545045797372821429113030136892191374277343128077198051419937776650920735266867535270496806766395484770316556440606978505432791/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^3 + 328861484095746363900637468335256882108855962984480206589277356841194190485888210924892901485535904815554552593904096465822556899870899791885/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y^2 - 57782310545870695313789138719986562282002067755891545057041747804914815314568724092283115993721648820117918641861487578181148024408410279257/88354466340444615034435033500065140214776548666633236678965310763840531924547236696178865907386012979055536019637250425090960337529677422144*y + 9698533059032858597482340045507210472276059008569359572497074562581004677785075336873293669086010596376470240669211658704216797246676325039/22088616585111153758608758375016285053694137166658309169741327690960132981136809174044716476846503244763884004909312606272740084382419355536

# 4 Loop Invariant
53671033719318217225684620071047008477346933220576330020592515193220316328623612914532392581825905799878267887560167173668215363438768410567051940298894537120554754708382398494551665817229272859079125228802807/561977684102945028082491819328725409934530347067621453478889054962183946590404088186859846285271984500225542752965133240008043597080499381470400102974954735877985223635732085583063841168581130784767386482410496*y^22 - 207048716688230405141994309264777272398770252544558477269558245060087102525004818439228504045012208447410851143040559563672226951588372028729423022856768690964812147702185273789828406159459511204751381840501339/702472105128681285103114774160906762418162933834526816848611318702729933238005110233574807856589980625281928441206416550010054496350624226838000128718693419847481529544665106978829801460726413480959233103013120*y^21 - 1041049279708076223989807378996556907062993354011744035717040898625661838261497840767560062136602838690416929439835429759442632938755722547661021932090573217040415602112423053682879902716752376272664180549100491/1404944210257362570206229548321813524836325867669053633697222637405459866476010220467149615713179961250563856882412833100020108992701248453676000257437386839694963059089330213957659602921452826961918466206026240*y^20 + 18174098296083078370959521000267816203481000049072617054199640014549393758067384505071709877955015273165180190648366732389267777638531542005591666174839033141059819392123617908930403626937820344585092942591536059/2809888420514725140412459096643627049672651735338107267394445274810919732952020440934299231426359922501127713764825666200040217985402496907352000514874773679389926118178660427915319205842905653923836932412052480*y^19 - 22968744275639825326227193850608564922444890310330303233544016027317642710082857815443625603841953741605614336884540911602575673757067545517716449519919935387045754005826391211036354193154921529116802507467739037/2809888420514725140412459096643627049672651735338107267394445274810919732952020440934299231426359922501127713764825666200040217985402496907352000514874773679389926118178660427915319205842905653923836932412052480*y^18 - 6669218428809330800772377426947948154319805801557803409991440428717849634701815101541475325931425398324104472378087089911532407496269005399012304855634409565149114896542082154719979425997199395525194355766744937/468314736752454190068743182773937841612108622556351211232407545801819955492003406822383205237726653750187952294137611033340036330900416151225333419145795613231654353029776737985886534307150942320639488735342080*y^17 + 64374141036963820664312846360577235185412240535737899453057213451857026143635328190915543836561023038728371176496161684083500495264364166202900619526203218631512754050388711201122516425521990127003468225765101321/936629473504908380137486365547875683224217245112702422464815091603639910984006813644766410475453307500375904588275222066680072661800832302450666838291591226463308706059553475971773068614301884641278977470684160*y^16 - 15179277875515838254343290859947740359449533186688723639185844186171853378711065568314923651824290476992611224167222828263677768242415989879965175633039399676077372408413414706729019906219072239590676199902345861/156104912250818063356247727591312613870702874185450403744135848600606651830667802274127735079242217916729317431379203677780012110300138717075111139715265204410551451009925579328628844769050314106879829578447360*y^15 + 5457040665607884547512402524039590905721471393175605459518285167600051937614359158645405976742553658745013516354853961698448776611268671373050487065856905885079442846894274312304231390236343514773922043489444155/280988842051472514041245909664362704967265173533810726739444527481091973295202044093429923142635992250112771376482566620004021798540249690735200051487477367938992611817866042791531920584290565392383693241205248*y^14 + 146863316934809100163723648447992277525418159540821646276128467070202293983708434872895052001625034106357297266214477186147001045292680081213369434124644262164793211069428139620860781162629586477281466341237894141/1404944210257362570206229548321813524836325867669053633697222637405459866476010220467149615713179961250563856882412833100020108992701248453676000257437386839694963059089330213957659602921452826961918466206026240*y^13 - 214916700376415197768916809582324623767209925817351481728209736006044225598269011713654842366189241617069252254581516440471190883231966191021759157729107370782037447538599822612519133820594392037482220073928266511/1404944210257362570206229548321813524836325867669053633697222637405459866476010220467149615713179961250563856882412833100020108992701248453676000257437386839694963059089330213957659602921452826961918466206026240*y^12 + 28948618726517168780482731753489516842554465044736994881616170135021926347578066561277874124753759927989687395109457421972393139370928948502053957255793512702740627233518150945182642369457943869645474428866603703/468314736752454190068743182773937841612108622556351211232407545801819955492003406822383205237726653750187952294137611033340036330900416151225333419145795613231654353029776737985886534307150942320639488735342080*y^11 - 908896353834521075608307050292256987829672649020635368946421913236960963114630435883375382478315929523653710730028686281820890409357475043557940892155336798475752002167527042188928407591301720728006946634417199/35123605256434064255155738708045338120908146691726340842430565935136496661900255511678740392829499031264096422060320827500502724817531211341900006435934670992374076477233255348941490073036320674047961655150656*y^10 + 111323116548070623139083669865986037049002763157359802259859089799835356939431476575818167598019160912242212754293225825076084361309039912409884540139275582198231599371487009328571542022273577804230369537336673057/936629473504908380137486365547875683224217245112702422464815091603639910984006813644766410475453307500375904588275222066680072661800832302450666838291591226463308706059553475971773068614301884641278977470684160*y^9 - 705544517824332173825328528157840554009861841250455014591459278382627929325807493314166465258074226622625168066727140700512723572460208682904156458299035169744629488664306220395954308460514559202229599870935738987/2809888420514725140412459096643627049672651735338107267394445274810919732952020440934299231426359922501127713764825666200040217985402496907352000514874773679389926118178660427915319205842905653923836932412052480*y^8 + 167197027558764812102150728355173098413196771600562578784168284217978130183322683350686932160811140113857935848012403675930340321318151525623257369040514218332455470551769996159221127891883146616179041381748736003/561977684102945028082491819328725409934530347067621453478889054962183946590404088186859846285271984500225542752965133240008043597080499381470400102974954735877985223635732085583063841168581130784767386482410496*y^7 - 93509838319098721207227340511750680406990980057145726412135379586285784158816276406347955657644785142613460154728955764385746607360722056350158085629800946371437652935820431240250712841748694448290987342662951473/468314736752454190068743182773937841612108622556351211232407545801819955492003406822383205237726653750187952294137611033340036330900416151225333419145795613231654353029776737985886534307150942320639488735342080*y^6 + 61980654970756713057021967459869956012058073622978478614627986667900649741081885818029107186855996044047004951708734899796753171272812651542559625660114140062528482630265660744332706237509581896633183733993167093/702472105128681285103114774160906762418162933834526816848611318702729933238005110233574807856589980625281928441206416550010054496350624226838000128718693419847481529544665106978829801460726413480959233103013120*y^5 - 17957706791068758429687892628858650784773979741487956079902206471392599021939007636248191356825137241711485299356490398161433602459359477676245127674502196437212616211909109793167930582611247387456057529206062167/468314736752454190068743182773937841612108622556351211232407545801819955492003406822383205237726653750187952294137611033340036330900416151225333419145795613231654353029776737985886534307150942320639488735342080*y^4 + 11028419409619461181246062855873580186885870828662235989591371040664928500074360379443852499396321972502419561984862702780426773731492705182662077906539352370654147132085757812197689282029760027866947182512955421/561977684102945028082491819328725409934530347067621453478889054962183946590404088186859846285271984500225542752965133240008043597080499381470400102974954735877985223635732085583063841168581130784767386482410496*y^3 - 16113872684437842665076884520094869048540881073467640552167587558578028378146064649360282980127795082571958779943511752192099955786951804051851296623521005428661884027378910935255108052962221394653220895924920263/2809888420514725140412459096643627049672651735338107267394445274810919732952020440934299231426359922501127713764825666200040217985402496907352000514874773679389926118178660427915319205842905653923836932412052480*y^2 + 1282453594826214786140942027528410886440834466317971925624974752857482203278528894495129646698421462491478406642075658796476104414112385018153713565870807866058740217595047180367337330606609785843491702572289957/1404944210257362570206229548321813524836325867669053633697222637405459866476010220467149615713179961250563856882412833100020108992701248453676000257437386839694963059089330213957659602921452826961918466206026240*y - 449044631664130754219272557591279613203464911959389615761823847751253392267435590091180611508631178681689838328610636772501341529970028197468151331086976242773501181296476776375331446772233703826190886959116193/561977684102945028082491819328725409934530347067621453478889054962183946590404088186859846285271984500225542752965133240008043597080499381470400102974954735877985223635732085583063841168581130784767386482410496