# Manifold: Census Knot K8_61

# Number of Tetrahedra: 8

# Number Field
x^24 + 8*x^23 + 33*x^22 + 183*x^21 + 562*x^20 + 880*x^19 + 3917*x^18 + 3389*x^17 + 13201*x^16 + 11389*x^15 + 28578*x^14 + 29419*x^13 + 39458*x^12 + 61331*x^11 + 26150*x^10 + 104787*x^9 - 19196*x^8 + 125782*x^7 - 32928*x^6 + 62832*x^5 + 1344*x^4 + 6048*x^3 - 2496*x^2 - 384*x - 256 

# Approximate Field Generator
-0.0823793320787180 + 0.331776654882903*I

# Shape Parameters
-59339767934482300495790297713229747903330040003649/1117353147874259472105023455486223264472411506557595776*y^23 - 300532423686035513657277746371271641301277961172489/558676573937129736052511727743111632236205753278797888*y^22 - 3069939552582116307552089186621625832651177302431005/1117353147874259472105023455486223264472411506557595776*y^21 - 15815187087453881963517832480690364070347101076385297/1117353147874259472105023455486223264472411506557595776*y^20 - 14865245121523877436231772988096938443842956769244731/279338286968564868026255863871555816118102876639398944*y^19 - 8717278421116118507569563256250917755829739542977787/69834571742141217006563965967888954029525719159849736*y^18 - 389740134420968303678290005280787590709359140001323669/1117353147874259472105023455486223264472411506557595776*y^17 - 737908360210754203571107143521968253358700339668843751/1117353147874259472105023455486223264472411506557595776*y^16 - 1471466218292349190820064062104553990381101515546228999/1117353147874259472105023455486223264472411506557595776*y^15 - 2403321096722902555517252641132614003411452366661678555/1117353147874259472105023455486223264472411506557595776*y^14 - 58240340547042212251988058542795646447126839725682159/17458642935535304251640991491972238507381429789962434*y^13 - 5375400277919564639879305676398136602492563954110083971/1117353147874259472105023455486223264472411506557595776*y^12 - 834429170963034784321396813705539645914063916952801955/139669143484282434013127931935777908059051438319699472*y^11 - 8640121315071771407749469838968545246642191577661978691/1117353147874259472105023455486223264472411506557595776*y^10 - 2162074343274874748142871934031897068206220322639880893/279338286968564868026255863871555816118102876639398944*y^9 - 10096036815563932201185842975163597386666642513688120547/1117353147874259472105023455486223264472411506557595776*y^8 - 4184272655552285634510344338260736800603651046383834885/558676573937129736052511727743111632236205753278797888*y^7 - 3812455446552950119152234671620671424563035673082843349/558676573937129736052511727743111632236205753278797888*y^6 - 1630307366575510451615333232058575693552862091753979701/279338286968564868026255863871555816118102876639398944*y^5 - 352676679597233407751121434683170256643423887377842575/139669143484282434013127931935777908059051438319699472*y^4 - 149808368066596091662920941927429226493148726467132515/69834571742141217006563965967888954029525719159849736*y^3 + 3418625955656925406092053297253538817515590025595918/8729321467767652125820495745986119253690714894981217*y^2 + 1446430072467600251955869497991608931989498480605597/17458642935535304251640991491972238507381429789962434*y + 7543601136544540540204599248335205964171753491796596/8729321467767652125820495745986119253690714894981217

-111045878085489166077722289088531150436849603478070975/302802703073924316940461356436766504672023518277108455296*y^23 - 477270374332578511145639696395935144845366697481543507/151401351536962158470230678218383252336011759138554227648*y^22 - 4218462112208329807945911438898933171486255108268241215/302802703073924316940461356436766504672023518277108455296*y^21 - 22689150353978317769709034967700180839841843015988304383/302802703073924316940461356436766504672023518277108455296*y^20 - 4695968491013992739953104277102463424751305596608936363/18925168942120269808778834777297906542001469892319278456*y^19 - 34552094389305339901732535635471813497285554089467026477/75700675768481079235115339109191626168005879569277113824*y^18 - 501454545629486367909286040800788191922268625647972043611/302802703073924316940461356436766504672023518277108455296*y^17 - 632961669497115844831492544189401392223253755118391521945/302802703073924316940461356436766504672023518277108455296*y^16 - 1720918267781750466672350803805121441701105621419614645573/302802703073924316940461356436766504672023518277108455296*y^15 - 2094896634123883392686919856888074574185682482479016571881/302802703073924316940461356436766504672023518277108455296*y^14 - 975408303255524429887857009416313883601036534247316397915/75700675768481079235115339109191626168005879569277113824*y^13 - 4959115675416064646945251196197021092094089299699130199017/302802703073924316940461356436766504672023518277108455296*y^12 - 377236846692474172830820861221755089699032746666570973119/18925168942120269808778834777297906542001469892319278456*y^11 - 8932321264326867410619237878137911748858220666688462130841/302802703073924316940461356436766504672023518277108455296*y^10 - 1503181668873872104343266532026711920087728498952791605003/75700675768481079235115339109191626168005879569277113824*y^9 - 12604501244234156359665197706665351744940511175814172530673/302802703073924316940461356436766504672023518277108455296*y^8 - 1555817497830587552417372067650412244678114967341366329039/151401351536962158470230678218383252336011759138554227648*y^7 - 6059092665102976381949722993919132290096482156083472479849/151401351536962158470230678218383252336011759138554227648*y^6 - 669021185294343727769955413030106690702372329387822494375/75700675768481079235115339109191626168005879569277113824*y^5 - 31864947425757917547550252277191866723000263591723522622/2365646117765033726097354347162238317750183736539909807*y^4 - 233682325729436459621862591743378388700951484176268863047/18925168942120269808778834777297906542001469892319278456*y^3 + 1888940619338718130100003329685745617824812208003176202/2365646117765033726097354347162238317750183736539909807*y^2 + 589997738923379576065546504970829124317387808502112844/2365646117765033726097354347162238317750183736539909807*y - 240385906762349713043269182593938949712387460803230438/2365646117765033726097354347162238317750183736539909807

-66274736530964060752822850618685041880549154968401312383/41029766266516744945432513797181861383059186726548195692608*y^23 - 555239021289795185273086955327102257794828848938279968871/41029766266516744945432513797181861383059186726548195692608*y^22 - 2375567477091922923357195683706193442874012777252549623751/41029766266516744945432513797181861383059186726548195692608*y^21 - 3214868015877649317303390489823041873396283739685332814423/10257441566629186236358128449295465345764796681637048923152*y^20 - 41436948601733305144996439233283034090099521578532809880327/41029766266516744945432513797181861383059186726548195692608*y^19 - 35118979503065945092683360568932714163452114716350415587301/20514883133258372472716256898590930691529593363274097846304*y^18 - 275011899749502856113565529932583063336052935278854195060239/41029766266516744945432513797181861383059186726548195692608*y^17 - 156309759579997323914925021711705577400522660014092103388727/20514883133258372472716256898590930691529593363274097846304*y^16 - 457622960124462101071905679484707363090222817086339122556749/20514883133258372472716256898590930691529593363274097846304*y^15 - 524049317559903223374797451431548072537887599096767928878595/20514883133258372472716256898590930691529593363274097846304*y^14 - 2035581085947927512989368303010097450332221063857209960540173/41029766266516744945432513797181861383059186726548195692608*y^13 - 2546532158204009590772798664810433498850538517328255975551823/41029766266516744945432513797181861383059186726548195692608*y^12 - 3056927182512897764210364091226834255820506353234022296216295/41029766266516744945432513797181861383059186726548195692608*y^11 - 4756975162881162821718036422868205843308305996521107707112003/41029766266516744945432513797181861383059186726548195692608*y^10 - 2896121902644731740250500735311989365634468996991537696119739/41029766266516744945432513797181861383059186726548195692608*y^9 - 6993009911770888901761243687834994295556237656705150957809743/41029766266516744945432513797181861383059186726548195692608*y^8 - 1177632259286452603574319992003132005566703798169130473049157/41029766266516744945432513797181861383059186726548195692608*y^7 - 3410590858224379148816773198560403011290987177363033659134999/20514883133258372472716256898590930691529593363274097846304*y^6 - 654242496508792448637969252455702464690573474854166230372735/20514883133258372472716256898590930691529593363274097846304*y^5 - 133095781359415304276046407444974372320322962883471513305145/2564360391657296559089532112323866336441199170409262230788*y^4 - 259817152803646005291396507374217953193681641754821808221579/5128720783314593118179064224647732672882398340818524461576*y^3 + 955233213110742374909681904572497910619057197152034614606/641090097914324139772383028080966584110299792602315557697*y^2 + 908282689178074105966546376709081157765202914142476727537/1282180195828648279544766056161933168220599585204631115394*y + 933243359329684871140151860800205724656356114473348050353/641090097914324139772383028080966584110299792602315557697

-25985241613996756198552118821441481220350341715436443225/87490986184850265184767546611482254054718765786472864452352*y^23 - 224176781018899164515749237104838230834478083733634408547/87490986184850265184767546611482254054718765786472864452352*y^22 - 987676620737277857086771141776747146997435232210907403383/87490986184850265184767546611482254054718765786472864452352*y^21 - 661574136935705863445218454405608286510234007120688393411/10936373273106283148095943326435281756839845723309108056544*y^20 - 17590047809277065520717562750722804914277901209917892493969/87490986184850265184767546611482254054718765786472864452352*y^19 - 16020287080607651940217861550236269930636658991527299303421/43745493092425132592383773305741127027359382893236432226176*y^18 - 116278160888176664214494305474876861346623266279529281331063/87490986184850265184767546611482254054718765786472864452352*y^17 - 19084529151985235782704126874332919960317468438680079779243/10936373273106283148095943326435281756839845723309108056544*y^16 - 28533429675441884318766626523027404778915576169810313919451/6249356156060733227483396186534446718194197556176633175168*y^15 - 154935913281343126366349157979765329584525203461268838631/26257798975045097594468051203926246715101670404103500736*y^14 - 936297649589194735001624532163630931581316739407747770636881/87490986184850265184767546611482254054718765786472864452352*y^13 - 1248524604509027079223930774178680673239857074690619890035357/87490986184850265184767546611482254054718765786472864452352*y^12 - 90199973740704110115881173640106852248363552467910510527869/5146528599108839128515738035969544356159927399204286144256*y^11 - 325899132023953948939740989944118269440937949633998569552913/12498712312121466454966792373068893436388395112353266350336*y^10 - 102856133405676325963646895816318569005656282718730335891297/5146528599108839128515738035969544356159927399204286144256*y^9 - 3225364464667775598201897540308363436929170959703541593874503/87490986184850265184767546611482254054718765786472864452352*y^8 - 1326725378966905347791232112925523082355896810919601675161927/87490986184850265184767546611482254054718765786472864452352*y^7 - 763603631881516123481750515145226830651502139409682834591003/21872746546212566296191886652870563513679691446618216113088*y^6 - 167819233900290855213149474759432114261967291938972484832797/10936373273106283148095943326435281756839845723309108056544*y^5 - 74793909407970214602501517828947913516069365547091044833677/5468186636553141574047971663217640878419922861654554028272*y^4 - 72402134879303503944910940358104722318767765965763598380837/5468186636553141574047971663217640878419922861654554028272*y^3 - 9266308345275216719348750183508099744655885642140428404995/2734093318276570787023985831608820439209961430827277014136*y^2 - 1003709318361781304945521635777253873866690179870392223367/1367046659138285393511992915804410219604980715413638507068*y + 138958220846244943475169075846818935470354540395726588975/683523329569142696755996457902205109802490357706819253534

-2516239892598402014004438638657256127027866858448957/56775506826360809426336504331893719626004409676957835368*y^23 - 20468592918018966469693056176127141096739107110235405/37850337884240539617557669554595813084002939784638556912*y^22 - 107254632151481209115473591190885198163746066238412541/37850337884240539617557669554595813084002939784638556912*y^21 - 251638005828010147515978785963766758775724390199943193/18925168942120269808778834777297906542001469892319278456*y^20 - 6251256306011833691651162626584106853088452675374537003/113551013652721618852673008663787439252008819353915670736*y^19 - 13869318411070826662635900912772352977261674552519346075/113551013652721618852673008663787439252008819353915670736*y^18 - 30798166856698686471246762833300648087482891687211533133/113551013652721618852673008663787439252008819353915670736*y^17 - 3697939615861976088814192302579703012679883298570736915/4731292235530067452194708694324476635500367473079819614*y^16 - 29571578917485750025678973855235946387514497109285677619/37850337884240539617557669554595813084002939784638556912*y^15 - 146714858381991140386595002543775328954563575936731161513/56775506826360809426336504331893719626004409676957835368*y^14 - 229051439756156569882420619028905351077411420811656991785/113551013652721618852673008663787439252008819353915670736*y^13 - 612638173870928421261310110604274113296528105589842389099/113551013652721618852673008663787439252008819353915670736*y^12 - 250181955769604408593294248119454228029772693072616823995/56775506826360809426336504331893719626004409676957835368*y^11 - 33103137321958816831989668364175782756157376754937594863/4731292235530067452194708694324476635500367473079819614*y^10 - 337952679925961827422836720696236689413510266400351309153/37850337884240539617557669554595813084002939784638556912*y^9 - 125462720143823059848481546663935174050820492699043520859/37850337884240539617557669554595813084002939784638556912*y^8 - 234181925913826287004393563539427790262007098253678207955/14193876706590202356584126082973429906501102419239458842*y^7 + 466441326955492923155963826898492427889697450234568736343/56775506826360809426336504331893719626004409676957835368*y^6 - 226293000810516059298495721701760591462052729797230881455/9462584471060134904389417388648953271000734946159639228*y^5 + 207777198913386967835527667484050701957588289153582671175/14193876706590202356584126082973429906501102419239458842*y^4 - 95108518329977531249836046501862982658997022282200901667/7096938353295101178292063041486714953250551209619729421*y^3 + 25218082275580553399754422153498365981779014346486645655/7096938353295101178292063041486714953250551209619729421*y^2 + 3371927456769471378071315963712813781788069358105948786/7096938353295101178292063041486714953250551209619729421*y + 4073427867267124531878735833735139080350920724769546359/7096938353295101178292063041486714953250551209619729421

-194340323813367550461215735594241077454165514960617/34917285871070608503281982983944477014762859579924868*y^23 - 6352262986853897893835564160930984059597913913974855/139669143484282434013127931935777908059051438319699472*y^22 - 26584321527306788764988202395318601057184615340315087/139669143484282434013127931935777908059051438319699472*y^21 - 36396015435277209117521944076128611772405835533747789/34917285871070608503281982983944477014762859579924868*y^20 - 456926179784298354700557783813283230048383735920497755/139669143484282434013127931935777908059051438319699472*y^19 - 734876328284247764789208924699967611425384690979202589/139669143484282434013127931935777908059051438319699472*y^18 - 3089466804397164424288947854191429015126721417747089103/139669143484282434013127931935777908059051438319699472*y^17 - 762773823217047359066897566968373775424379927333873395/34917285871070608503281982983944477014762859579924868*y^16 - 10219079993690542306075167362745891661468868528625832489/139669143484282434013127931935777908059051438319699472*y^15 - 2562516572039034409810799513275260214277302391789269957/34917285871070608503281982983944477014762859579924868*y^14 - 22146918392937937348689876630903947722411915046599537833/139669143484282434013127931935777908059051438319699472*y^13 - 25529736114842407306760125034174800509281799495882537527/139669143484282434013127931935777908059051438319699472*y^12 - 15699053727873789502782698936105715330148704759773706829/69834571742141217006563965967888954029525719159849736*y^11 - 24997752329112197902636391641100465037421952747009205935/69834571742141217006563965967888954029525719159849736*y^10 - 24680568934135431455588313315246865036064294311677023475/139669143484282434013127931935777908059051438319699472*y^9 - 78572437126686234462800782894703995219956888635331753857/139669143484282434013127931935777908059051438319699472*y^8 + 129561615504496327115793300188694135618623145339795615/8729321467767652125820495745986119253690714894981217*y^7 - 41821857709799067366876657342429576097589058211670656293/69834571742141217006563965967888954029525719159849736*y^6 + 859809182704404131771992871668904999170504822403281023/34917285871070608503281982983944477014762859579924868*y^5 - 3752110436035767654264621589192597045473197232070259779/17458642935535304251640991491972238507381429789962434*y^4 - 999110010984180426265287651176964283193720640044841163/8729321467767652125820495745986119253690714894981217*y^3 + 112548808886711131292659442422468919610771768739291247/8729321467767652125820495745986119253690714894981217*y^2 + 24358071856951761104183586266421483442744214296890218/8729321467767652125820495745986119253690714894981217*y + 62279902601809824042996770232002673520543929554796454/8729321467767652125820495745986119253690714894981217

-194340323813367550461215735594241077454165514960617/34917285871070608503281982983944477014762859579924868*y^23 - 6352262986853897893835564160930984059597913913974855/139669143484282434013127931935777908059051438319699472*y^22 - 26584321527306788764988202395318601057184615340315087/139669143484282434013127931935777908059051438319699472*y^21 - 36396015435277209117521944076128611772405835533747789/34917285871070608503281982983944477014762859579924868*y^20 - 456926179784298354700557783813283230048383735920497755/139669143484282434013127931935777908059051438319699472*y^19 - 734876328284247764789208924699967611425384690979202589/139669143484282434013127931935777908059051438319699472*y^18 - 3089466804397164424288947854191429015126721417747089103/139669143484282434013127931935777908059051438319699472*y^17 - 762773823217047359066897566968373775424379927333873395/34917285871070608503281982983944477014762859579924868*y^16 - 10219079993690542306075167362745891661468868528625832489/139669143484282434013127931935777908059051438319699472*y^15 - 2562516572039034409810799513275260214277302391789269957/34917285871070608503281982983944477014762859579924868*y^14 - 22146918392937937348689876630903947722411915046599537833/139669143484282434013127931935777908059051438319699472*y^13 - 25529736114842407306760125034174800509281799495882537527/139669143484282434013127931935777908059051438319699472*y^12 - 15699053727873789502782698936105715330148704759773706829/69834571742141217006563965967888954029525719159849736*y^11 - 24997752329112197902636391641100465037421952747009205935/69834571742141217006563965967888954029525719159849736*y^10 - 24680568934135431455588313315246865036064294311677023475/139669143484282434013127931935777908059051438319699472*y^9 - 78572437126686234462800782894703995219956888635331753857/139669143484282434013127931935777908059051438319699472*y^8 + 129561615504496327115793300188694135618623145339795615/8729321467767652125820495745986119253690714894981217*y^7 - 41821857709799067366876657342429576097589058211670656293/69834571742141217006563965967888954029525719159849736*y^6 + 859809182704404131771992871668904999170504822403281023/34917285871070608503281982983944477014762859579924868*y^5 - 3752110436035767654264621589192597045473197232070259779/17458642935535304251640991491972238507381429789962434*y^4 - 999110010984180426265287651176964283193720640044841163/8729321467767652125820495745986119253690714894981217*y^3 + 112548808886711131292659442422468919610771768739291247/8729321467767652125820495745986119253690714894981217*y^2 + 24358071856951761104183586266421483442744214296890218/8729321467767652125820495745986119253690714894981217*y + 53550581134042171917176274486016554266853214659815237/8729321467767652125820495745986119253690714894981217

-515095797540770699614746968741040021183129252827173/279338286968564868026255863871555816118102876639398944*y^23 - 7946083244934113945779889548308487399221826724257339/558676573937129736052511727743111632236205753278797888*y^22 - 15830066372501547717679189711105749854008990335104727/279338286968564868026255863871555816118102876639398944*y^21 - 178947725197770552167094925964035884849006642304222121/558676573937129736052511727743111632236205753278797888*y^20 - 525406697037236981447878369091456986850983902353523069/558676573937129736052511727743111632236205753278797888*y^19 - 371900019212326380419317959350398525144329167092161653/279338286968564868026255863871555816118102876639398944*y^18 - 1890643363276115159649616323776358480000986453162131821/279338286968564868026255863871555816118102876639398944*y^17 - 2327495314608321107209101355274579109074153784414951473/558676573937129736052511727743111632236205753278797888*y^16 - 12651142213771099165460700142732223842975727903138530061/558676573937129736052511727743111632236205753278797888*y^15 - 7723927138742087825983115735947986591102274279384295929/558676573937129736052511727743111632236205753278797888*y^14 - 26204383820983497377795154910991717191764223198913309711/558676573937129736052511727743111632236205753278797888*y^13 - 2690021307298879038888674062683590593769336301763225217/69834571742141217006563965967888954029525719159849736*y^12 - 32009296939266121734535890443596590636065153811859243909/558676573937129736052511727743111632236205753278797888*y^11 - 6370094459587601269991739304133287340752703801757959609/69834571742141217006563965967888954029525719159849736*y^10 - 8283308296209831001953455044040354893034226986830739573/558676573937129736052511727743111632236205753278797888*y^9 - 25012611118256711670681693866160557733500287716987556335/139669143484282434013127931935777908059051438319699472*y^8 + 52821965718800760125588678423542657794508670625353591255/558676573937129736052511727743111632236205753278797888*y^7 - 34205886244062694935414004338210760922809211221302719607/139669143484282434013127931935777908059051438319699472*y^6 + 37728248494879340939239764887716830109311090724999150471/279338286968564868026255863871555816118102876639398944*y^5 - 4888858838224449171528706419317643901302442520423934627/34917285871070608503281982983944477014762859579924868*y^4 + 674825767630663016375308050638787942885366593088578481/17458642935535304251640991491972238507381429789962434*y^3 - 528175337947880797556507119370248399135397822893285007/34917285871070608503281982983944477014762859579924868*y^2 + 73667447907746753808432653944568332230848919136489104/8729321467767652125820495745986119253690714894981217*y + 4026808643222862595744039912033123987293061710450754/8729321467767652125820495745986119253690714894981217


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

# B Gluing Matrix
{{1,0,0,0,0,0,0,2},{0,1,0,0,0,0,0,2},{0,0,1,0,0,0,0,2},{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,2},{0,0,0,0,0,0,0,4}}

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

# f Combinatorial flattening
{-5, 0, 5, -5, 16, 15, 0, 8}

# f' Combinatorial flattening
{0, -4, 0, -8, 0, 0, 0, 0}

# 1 Loop Invariant
-60985412689113818095508274906980573522085725063049847/1117353147874259472105023455486223264472411506557595776*y^23 - 31035629071959598235492542030027110547583277932419495/69834571742141217006563965967888954029525719159849736*y^22 - 2069595793121782793396134976302413241526109517290739331/1117353147874259472105023455486223264472411506557595776*y^21 - 11340313599105181942230873273771943128249559228269704413/1117353147874259472105023455486223264472411506557595776*y^20 - 17698031039977144372608595154379875666104438669825012879/558676573937129736052511727743111632236205753278797888*y^19 - 14014754400398652676008537004154145927550421034127141721/279338286968564868026255863871555816118102876639398944*y^18 - 238381250806600387273840145345582551334624874333317720247/1117353147874259472105023455486223264472411506557595776*y^17 - 226497273403196935323504547874058998849120648848932570967/1117353147874259472105023455486223264472411506557595776*y^16 - 783337615897185908801081774176645373752807617438253988735/1117353147874259472105023455486223264472411506557595776*y^15 - 750564024348814027624770230421432294590422246352995943831/1117353147874259472105023455486223264472411506557595776*y^14 - 838488022400644548439063009477257513001785432287027188835/558676573937129736052511727743111632236205753278797888*y^13 - 1869505910842730869572703186548633501378079819607385790393/1117353147874259472105023455486223264472411506557595776*y^12 - 1159951794845235731518122895226737276635645201888996635565/558676573937129736052511727743111632236205753278797888*y^11 - 3700463193684797216148001180937371308073246114846547133205/1117353147874259472105023455486223264472411506557595776*y^10 - 833610029427853317495641430177067111807591742178170964585/558676573937129736052511727743111632236205753278797888*y^9 - 5937304235233140984343955242789580876122066926705723297057/1117353147874259472105023455486223264472411506557595776*y^8 + 36220494588115879453927937082378546080709062102089155465/69834571742141217006563965967888954029525719159849736*y^7 - 3247314163308541357098929013297531845880256760548194320945/558676573937129736052511727743111632236205753278797888*y^6 + 12578735694850714071205143712839471282197541686670591867/17458642935535304251640991491972238507381429789962434*y^5 - 156025170070414053358340271707269003565400960753162621915/69834571742141217006563965967888954029525719159849736*y^4 - 52840391460925793457708347834690337676784307256145557607/69834571742141217006563965967888954029525719159849736*y^3 + 1623574601345868051782396009058173701394558390443927883/34917285871070608503281982983944477014762859579924868*y^2 + 1417116319906582638657710109119549100392897453200956089/17458642935535304251640991491972238507381429789962434*y + 363046130330577340586816218805565184659534331827666671/8729321467767652125820495745986119253690714894981217

# 2 Loop Invariant
-1723122427826264270219962962114387041832305586065927751206268880722440754234370411073912243065214189365879270012225305723526942433/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^23 - 2475619924646304976213896867506670250594555310023938018457567196381645840465125991840181748221180980985741197137023234820355977935/3344822100068050389740173474002454140011845755283183266759989269601128604647315204911049673493732135174859712469265423036183893459968*y^22 - 64731756328179260194124554635986778467365692318015484356206654886280596206121083909488925833950679437264132413248551869551131847025/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^21 - 345164668440634297570054760911886341775241755460182591886669079487267971069027583567054096151497551989745322727005369442690901184353/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^20 - 2973629740381321617825240814617902552661229637663059842345959734800502434102771048687510146339657105254569321024497512030842211613/52262845313563287339690210531288345937685089926299738543124832337517634447614300076735151148339564612107183007332272234940373335312*y^19 - 498760333698844841309416997984186207603483477724723710241866476788140249148087169922904564069099683552644869382921909236360002607859/5017233150102075584610260211003681210017768632924774900139983904401692906970972807366574510240598202762289568703898134554275840189952*y^18 - 7319425631166042252873383745916753441128667637192074233040514422931845594616535784944068366124845414667006133506371894904074894365477/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^17 - 9485969656331511049151396780929585605780730907865622255946514623113103469481919983024356748863437609844313712909111547740275830563111/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^16 - 7959938290451972308305019567649113237645343435074113040564467727537257377125414074465109463645926748037840681696207258349806559557929/6689644200136100779480346948004908280023691510566366533519978539202257209294630409822099346987464270349719424938530846072367786919936*y^15 - 31756393545499373709270410515580760782096075114326887981222267197924844058436866495864215915962613847251190300839687103625262526903943/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^14 - 13375250241322125181173229626969669132616586583125966414564734623688235351865638800195659008649389484840477190721033119855863265250269/5017233150102075584610260211003681210017768632924774900139983904401692906970972807366574510240598202762289568703898134554275840189952*y^13 - 74832742618086162436969618949525348124134896212758797506490278430820001492164160708934933424120516882759707926722769287780570851915415/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^12 - 5209031939587502106557555718626431985522691116890546701598297659674188070031740606267691864177106893895069639914041711638661661738701/1254308287525518896152565052750920302504442158231193725034995976100423226742743201841643627560149550690572392175974533638568960047488*y^11 - 131652312994565786401172127229643095909819983512975728538510841109908488957498532773952377617759838274689898649519996321238280091225015/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^10 - 22687026294113312517686411654911445049101803974818499181902037136977368140599161071801919789782083759840625644649477600282044551628385/5017233150102075584610260211003681210017768632924774900139983904401692906970972807366574510240598202762289568703898134554275840189952*y^9 - 174824723936113303078368404345935069721606352616122304653829234763105251982864347933590430158776797217502931415571688536853782126028639/20068932600408302338441040844014724840071074531699099600559935617606771627883891229466298040962392811049158274815592538217103360759808*y^8 - 11734409813512027002365573741400159212547303037866805115096190960653614136403329179178530233713312276498872474424804116851784063769051/3344822100068050389740173474002454140011845755283183266759989269601128604647315204911049673493732135174859712469265423036183893459968*y^7 - 23088611117999998167799767108477571087239103041748693394394951913421588014161636061403357449892247817240675603586869772129461503157397/3344822100068050389740173474002454140011845755283183266759989269601128604647315204911049673493732135174859712469265423036183893459968*y^6 - 8118724664878930818077031613704087579848106120940027623087891203707556840611553727983824948430015582518230224215958087824434832605727/1672411050034025194870086737001227070005922877641591633379994634800564302323657602455524836746866067587429856234632711518091946729984*y^5 - 11185120820494613853025950242724451472300777446222896627934489873283829662861745700533455876777931925908425193009566773155339952405/39197133985172465504767657898466259453263817444724803907343624253138225835710725057551363361254673459080387255499204176205280001484*y^4 - 1881376344692785672042439125448536255076435890606068786086713996653144338501868355048893534963796990444507806972253627590765710403117/418102762508506298717521684250306767501480719410397908344998658700141075580914400613881209186716516896857464058658177879522986682496*y^3 + 230504208577649179575008806260658003093616964096482123170864850768291390373151879947057678445221160547377883880095832000916527660517/313577071881379724038141263187730075626110539557798431258748994025105806685685800460410906890037387672643098043993633409642240011872*y^2 + 629290831235248748944762045395082717554241311228471077003304958766903165185337113779557783650421086241149459957927855736317983218/9799283496293116376191914474616564863315954361181200976835906063284556458927681264387840840313668364770096813874801044051320000371*y - 39249849579603633367241813520449889529866515634965259377461341056531054041461770857649992917971052583568234733270200767475826159157/9799283496293116376191914474616564863315954361181200976835906063284556458927681264387840840313668364770096813874801044051320000371

# 3 Loop Invariant
-77149843089832576584434335867297948860121504083678300818662453164390447239487605734262286316072904550052464789326446707555753340163588764456842511230280432952739064647/2046064471169649755875842063659807924698169040321504625912291450880849711917251900948324281608297506264102311388277996952668318801625063256074492857529843166180847664258048*y^23 - 2428563007767374807957594584285771383546791252255637154810559206800082162631338174750717875974977819260805264665565965056086264123129867075474099393200795689677578102183/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^22 - 1235521019697483069550190586261886623753955580691811649166320808149987310102695076559278112581125220595757712852177015683139901759414687874978459624953603053875689810843/1023032235584824877937921031829903962349084520160752312956145725440424855958625950474162140804148753132051155694138998476334159400812531628037246428764921583090423832129024*y^21 - 55325031887392623204593242153257020378193992368272716490884086851121914359625307379226585027007539263094845132197130859790256472200373236867883353155365861633081764877779/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^20 - 166798206873933059432431989852877140707062814087670422657841885872152069188642937864010154495953954459734859066932031450876539859534728215913123059697258282719182586414701/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^19 - 126475443814964852718110352036652822307477962889389008218578014841131278245617366060996997511583163949886568721668475382147190199570848244959572038531989260985030634721961/4092128942339299511751684127319615849396338080643009251824582901761699423834503801896648563216595012528204622776555993905336637603250126512148985715059686332361695328516096*y^18 - 296415960891146044217980355140988692882193027297924370076222443898551814644750965602517682750734831362124776890194474244855225476411241427090757841472907779039668375329211/2046064471169649755875842063659807924698169040321504625912291450880849711917251900948324281608297506264102311388277996952668318801625063256074492857529843166180847664258048*y^17 - 906185209581379479145249959782298997725459047843178409046427621418688548838594111230452133430377433392124182386501196603809316081987258575845345128076839652840130277135479/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^16 - 4019479731486402017120322876132913799628672395267507761143803391812513803921414476822988555649936164092003124937365269868058107763743480027327624592908722317936301259520139/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^15 - 3059378527214619825119583071689567445595423842057062209635970931451322361020328153578086399364322147722723146127398369117390435225496913736649383526099314538234302323026207/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^14 - 8626140115937699828850249954182113732439366045130142522176828673149146910919608219257752968705410001428539594339862093637963191067030800190986074574644085168191637559737727/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^13 - 4102305933829049509549709864765935765742645064240732678843350668142234520931181469490761067146040353228081412053616549624171656596380937608181538028704296274470358141189743/4092128942339299511751684127319615849396338080643009251824582901761699423834503801896648563216595012528204622776555993905336637603250126512148985715059686332361695328516096*y^12 - 11592612445698291293301104430475272768620380105126727389874435088818277283896138895433982619693787987237020953583021253389017684669267952795960091093070685414645843173643733/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^11 - 9044604471144814250061831947768667945440877005451994110771114069802490046373610526459453018006127315368891064301871572977115042074448144841789573728111695832846407082430719/4092128942339299511751684127319615849396338080643009251824582901761699423834503801896648563216595012528204622776555993905336637603250126512148985715059686332361695328516096*y^10 - 6554064033792237535877664664248865073681593557876511210538542127576149792514876616848095857784522609525093061115766175866109435016929319546533946743792168952625296466817021/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^9 - 16443737581714356769573128270594708160138102874811065531271206708687237753985276662338377042827360960247408513305353727592887460345553668784702485120691315935618732036348437/4092128942339299511751684127319615849396338080643009251824582901761699423834503801896648563216595012528204622776555993905336637603250126512148985715059686332361695328516096*y^8 + 9141608000494968564403455510445014304170801729854354799922970679331290187189358709556699217917004343921673433668268482585677222078904783074524656726896835504334491400164171/8184257884678599023503368254639231698792676161286018503649165803523398847669007603793297126433190025056409245553111987810673275206500253024297971430119372664723390657032192*y^7 - 2642075930498988224852100794907357434853409560202639212023799227368164106652362570960974210409711935792516364296011904783760096592685018077648651061843423788917723123516735/511516117792412438968960515914951981174542260080376156478072862720212427979312975237081070402074376566025577847069499238167079700406265814018623214382460791545211916064512*y^6 + 7353003011672853703514817913761620589315606163581610690612067080884581455287940099695330679598249280824035249748654735107113607688422878856387361700669967214278804458050199/4092128942339299511751684127319615849396338080643009251824582901761699423834503801896648563216595012528204622776555993905336637603250126512148985715059686332361695328516096*y^5 - 2961515183192832806929239882989398594452580678022897269330247999744530950647189697082826229760171782750901059224032587405170149630277226584895773267197406297428828918297585/1023032235584824877937921031829903962349084520160752312956145725440424855958625950474162140804148753132051155694138998476334159400812531628037246428764921583090423832129024*y^4 + 87025483957044619693996672718862533412198554937819179814412001268947277154162709943563207738859721068162120445728094701284593331746328059721542866744726936810985652435197/511516117792412438968960515914951981174542260080376156478072862720212427979312975237081070402074376566025577847069499238167079700406265814018623214382460791545211916064512*y^3 - 94346047779441680875169061557919707304294619505749107547132134532916355313257471556341135221087170884330265284219085761762059959973955701727993752412632841605728354231507/255758058896206219484480257957475990587271130040188078239036431360106213989656487618540535201037188283012788923534749619083539850203132907009311607191230395772605958032256*y^2 - 221130156787591408654001663098015460100172979056183977206616207427392911641317307065063870196144317740456632536886873059528832206868708059981353796372067604585067559753/63939514724051554871120064489368997646817782510047019559759107840026553497414121904635133800259297070753197230883687404770884962550783226752327901797807598943151489508064*y - 1051737802546980552095871181230278964735448329648991492506549842209193155093902894849442850421961636548516412859512068186490632094634561600171110554980630277037944237707/127879029448103109742240128978737995293635565020094039119518215680053106994828243809270267600518594141506394461767374809541769925101566453504655803595615197886302979016128

# 4 Loop Invariant
-65171377502574278454525029826483992422843066556514399130645304354844893008205839391554966493694861936296314436663913577882667048498948099112183182744920540741834230566555529087809500765616428376733997109856226521239428040026884698732680018169835653/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^23 - 288345220645148413604290395366932021937687070409621544649143761877687240220943712204406120058803547241055346270020843733360895762093516286185209787829091275169276836799130977149401670919407813079947642304414890862723178515204727019825067102866578389/2204978616444440891033641839111241969752642120744288887364316263738082188902670785278150475266145015478316222720196637353040347399897923201661535122884141973853194851164297870624071482257311761825555911678058303642896933592850174337696576786927158231040*y^22 - 2592631163934286281154446739346430036893047762811196501520332709701303350509564793669437664840316478883610647722528666252062072790016070668848587693613817375393936203414410605269298773100894760064712823950645427816630064418097868076464830937298297857/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^21 - 4584989844576551640505921897967231732730872961540663074789757148625313910956785119010715277706507126877065167008013158055222119462754287888974264048090773449988733292169102331039991239348214750428444688326007606571498838682448701455792298374001026251/1469985744296293927355761226074161313168428080496192591576210842492054792601780523518766983510763343652210815146797758235360231599931948801107690081922761315902129900776198580416047654838207841217037274452038869095264622395233449558464384524618105487360*y^20 - 11700592917109693061135106085706343975436407430647856822138648350059038709170249668956698888464402621415349608676169143957596524176876535002594123418293785576278516342226810258123965407888249839714286863501741633403044982890718081540861587322958992549/1102489308222220445516820919555620984876321060372144443682158131869041094451335392639075237633072507739158111360098318676520173699948961600830767561442070986926597425582148935312035741128655880912777955839029151821448466796425087168848288393463579115520*y^19 - 2463080223097068693608754941590775493707481754219382256348262112317382444802578757351788962433428262549858394338539938116624451148070713089448262792549845056556633504522942131177503070531130690553306935750913570693048598809696665144262901429614352067/122498812024691160612980102172846776097369006708016049298017570207671232716815043626563915292563611971017567928899813186280019299994329066758974173493563442991844158398016548368003971236517320101419772871003239091272051866269454129872032043718175457280*y^18 - 33931310436955650045453727207118130795339026172738847435623222427529455409599079290409525728865344035629765515765464935540130498284328925906165223712130636686557443493467441274894137836087956646537087705094411446281164825636809816094221940228586743781/489995248098764642451920408691387104389476026832064197192070280830684930867260174506255661170254447884070271715599252745120077199977316267035896693974253771967376633592066193472015884946069280405679091484012956365088207465077816519488128174872701829120*y^17 - 443218671651290282909412704266787012921756754376267526935681121901270644588326547532706246852413240946158675888717985684962469093979970347893875603710403240808280721361237594445586640437398112769823622159971216872222231826934488789151312824429213714411/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^16 - 1058033782561397092473033628872717412826613482085628389215980836175934604803309721950577164218641024990978868530810981046826633558826126325419957413357781334169194862273147212209050057308864300370497281276258906719555891341188302400718573481469304273843/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^15 - 1509258310770343266393013723998408361970912891471735620997898494434888900487068754178046852763789286444634738391103755519775868225242252419713790292819454343552916461136453654650624634869581581284060661154438557194472178592629833105162362008831000882507/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^14 - 14153425173481303079566671407786643804515211736966977429188690044278742853051415858038102736020485262875059269928657549898737765390090229928245065207637693591269380522761104347086223537006734873270281848033910308897603990150652104934402707159602675595/24499762404938232122596020434569355219473801341603209859603514041534246543363008725312783058512722394203513585779962637256003859998865813351794834698712688598368831679603309673600794247303464020283954574200647818254410373253890825974406408743635091456*y^13 - 1208624483673595077504564478310747922295306495894674936078251250584699702230948417839033179783716583972807450007609507484341967163710863132333900019870547225019205099459087904127459039201211595013118790415684958235306475796346773860198023085733437036937/1469985744296293927355761226074161313168428080496192591576210842492054792601780523518766983510763343652210815146797758235360231599931948801107690081922761315902129900776198580416047654838207841217037274452038869095264622395233449558464384524618105487360*y^12 - 1096629159386356471970627897327475092405171976104384545869322605449745623396039245945666763521107957711816291517946965944498154977080496758670742973371584664250625204274199574210007844370826836377319194139404770261770753549256045897850436745949220910739/1102489308222220445516820919555620984876321060372144443682158131869041094451335392639075237633072507739158111360098318676520173699948961600830767561442070986926597425582148935312035741128655880912777955839029151821448466796425087168848288393463579115520*y^11 - 6484135034671072645456102373298842972597772472999891844155375445224749196575268131083426510710262215891757267846936001765610997186083138551527339794361653121924731642409324409421322131736984083616391303501760385257845248900635550815508552503297630056167/4409957232888881782067283678222483939505284241488577774728632527476164377805341570556300950532290030956632445440393274706080694799795846403323070245768283947706389702328595741248142964514623523651111823356116607285793867185700348675393153573854316462080*y^10 - 230241958607402251505157326136437164355107405007378334349013555924201144671588687068000807808717705210775846305076527159020691236431231721793875704309460208350332523240551229863695559058519505635786608183812690475325521575306130199028118302816407760327/183748218037036740919470153259270164146053510062024073947026355311506849075222565439845872938845417956526351893349719779420028949991493600138461260240345164487766237597024822552005956854775980152129659306504858636908077799404181194808048065577263185920*y^9 - 587125233846392339754744606733011582325273578126369373381071976914127768368963802630793200809848804492873986111983756860255778504325715741903290330407614692162208242443399614574067919339269756765944134129711207540446971066344263913974699146705891665993/293997148859258785471152245214832262633685616099238518315242168498410958520356104703753396702152668730442163029359551647072046319986389760221538016384552263180425980155239716083209530967641568243407454890407773819052924479046689911692876904923621097472*y^8 - 2616551172515706323118732732957174576127115604392541321240922518441647181294222743564814180393165051440627222607296357174284936371725055815599242893682254388651160785267629928667212681947468433981330662991997694134178643790230563572297951222933267175759/2204978616444440891033641839111241969752642120744288887364316263738082188902670785278150475266145015478316222720196637353040347399897923201661535122884141973853194851164297870624071482257311761825555911678058303642896933592850174337696576786927158231040*y^7 - 780719044561658621172363102707210032194613907278427241197976863709730991740781977654431928057916441036090344724715218582992462608593109877856138313702440472817924891290659846664515177896001831523689467677889927353964706304764066982233575724659930584389/440995723288888178206728367822248393950528424148857777472863252747616437780534157055630095053229003095663244544039327470608069479979584640332307024576828394770638970232859574124814296451462352365111182335611660728579386718570034867539315357385431646208*y^6 - 704829427738817902758944537744444125467145671916833128487335036707833184397785472926853504444642207987021987698733009317119198909422797740444827428900817341311250148439278581230241805219698355197847350493675334479673822400658421614203883395003715740711/551244654111110222758410459777810492438160530186072221841079065934520547225667696319537618816536253869579055680049159338260086849974480800415383780721035493463298712791074467656017870564327940456388977919514575910724233398212543584424144196731789557760*y^5 - 70857178253634461730501266084541030152787964615032991764894796683204698122215744498635065678059901342202523479164538300249119062351357632214473816335824492348527563248417649733586675301252051860933446511721249275811230405272612112495279181943720475115/110248930822222044551682091955562098487632106037214444368215813186904109445133539263907523763307250773915811136009831867652017369994896160083076756144207098692659742558214893531203574112865588091277795583902915182144846679642508716884828839346357911552*y^4 - 43942506845846892614600475315870794889990956809340647071822540571040684410952269508301649742440703466818511902154686305815710378467496022678990198766791751292252690482615887699520214957658603933497231106183694328051982068182064899796232353697934758277/45937054509259185229867538314817541036513377515506018486756588827876712268805641359961468234711354489131587973337429944855007237497873400034615315060086291121941559399256205638001489213693995038032414826626214659227019449851045298702012016394315796480*y^3 - 13275915993543763533897284792774987077709076851315561816147921824688288656346893677923125768457705422961237907960865162774832728346867525812703633493311427395652080540785233970403704919640832379611151960569087281461904312679488766987092748087312493851/68905581763888777844801307472226311554770066273259027730134883241815068403208462039942202352067031733697381960006144917282510856246810100051922972590129436682912339098884308457002233820540992557048622239939321988840529174776567948053018024591473694720*y^2 - 3129516840613746469399644200111945874504654137475053316675558641347664210453691802327324817383903049779798873535662406985503659213541050400773052535597940053928086019887950160071642723750392066832122125447370359468358730759232785948432843440152575327/34452790881944388922400653736113155777385033136629513865067441620907534201604231019971101176033515866848690980003072458641255428123405050025961486295064718341456169549442154228501116910270496278524311119969660994420264587388283974026509012295736847360*y - 3196919546342224849508968321673686859304125945685312084012401050509513460417157358910696424634085221968720553103172339659338046484277440213666561050828042805119149894910399074735261452355092150789283005234243688013900594396687335471956277780797771/2153299430121524307650040858507072236086564571039344616566715101306720887600264438748193823502094741678043186250192028665078464257712815626622592893441544896341010596840134639281319806891906017407769444998103812151266536711767748376656813268483552960