# Manifold: Census Knot K7_6

# Number of Tetrahedra: 7

# Number Field
x^29 - 12*x^28 - 45*x^27 + 335*x^26 + 552*x^25 - 3462*x^24 - 3340*x^23 + 18193*x^22 + 12147*x^21 - 54775*x^20 - 28557*x^19 + 99656*x^18 + 44461*x^17 - 112149*x^16 - 46512*x^15 + 77043*x^14 + 33833*x^13 - 29105*x^12 - 18770*x^11 + 2531*x^10 + 9126*x^9 + 3056*x^8 - 3923*x^7 - 1707*x^6 + 1234*x^5 + 462*x^4 - 225*x^3 - 71*x^2 + 17*x + 5 

# Approximate Field Generator
-0.660016093252821 - 0.121113035509663*I

# Shape Parameters
7364324959576440999191806053044959054224/852205449335098872376135288911987967369*y^28 - 74927924894927901766726397647612207832048/852205449335098872376135288911987967369*y^27 - 490581639767717457948076361312853857389845/852205449335098872376135288911987967369*y^26 + 1843158480736334542217163361791418264194306/852205449335098872376135288911987967369*y^25 + 8391583842531806234988270360796012154774397/852205449335098872376135288911987967369*y^24 - 17663241811502836233352104494805303719142155/852205449335098872376135288911987967369*y^23 - 67748415089279674281067328462992698838014409/852205449335098872376135288911987967369*y^22 + 85382515243714813842519237371975723735026260/852205449335098872376135288911987967369*y^21 + 304815424074472069312165965991300575776816951/852205449335098872376135288911987967369*y^20 - 223305324009320408892286980605035879682275277/852205449335098872376135288911987967369*y^19 - 810395537828737732201579841272186973620371420/852205449335098872376135288911987967369*y^18 + 311787325423233513090542060351721885475091699/852205449335098872376135288911987967369*y^17 + 1297983225754578149114958619243642325747386351/852205449335098872376135288911987967369*y^16 - 194444501237387259803678548020049672202778394/852205449335098872376135288911987967369*y^15 - 1254018189260144773125193528684968782841903118/852205449335098872376135288911987967369*y^14 - 34920596759523707316297457308981370810977156/852205449335098872376135288911987967369*y^13 + 708786220622093916649607915391724719856158618/852205449335098872376135288911987967369*y^12 + 156370593281836637275684172483820569915170877/852205449335098872376135288911987967369*y^11 - 208320392615443397662510028632602435057322159/852205449335098872376135288911987967369*y^10 - 139758683691252747945078765151402188828419171/852205449335098872376135288911987967369*y^9 + 13568681059421543333091680664072945671073026/852205449335098872376135288911987967369*y^8 + 78535270369034819126437187226217128754470198/852205449335098872376135288911987967369*y^7 + 11546149900022275810911463602265332639485271/852205449335098872376135288911987967369*y^6 - 29649064900029819206809153936923471342820408/852205449335098872376135288911987967369*y^5 - 5272311572211535931997355140814022964979016/852205449335098872376135288911987967369*y^4 + 6439901451940535518225260251111189425554107/852205449335098872376135288911987967369*y^3 + 1274483692995065368231467716930898941601930/852205449335098872376135288911987967369*y^2 - 571307062289232583031707220383783317313788/852205449335098872376135288911987967369*y - 136315220234611618646428789140356498097792/852205449335098872376135288911987967369

23074914275595687729434395189252761603415/852205449335098872376135288911987967369*y^28 - 306031654702746046528279320038514860315503/852205449335098872376135288911987967369*y^27 - 672200469443872427301400355163850970517124/852205449335098872376135288911987967369*y^26 + 8817234731720933635271433742719359683692264/852205449335098872376135288911987967369*y^25 + 2542376979948679649392759410708892295362236/852205449335098872376135288911987967369*y^24 - 89455803861434799492379389396905378954371515/852205449335098872376135288911987967369*y^23 + 24331703046221544930395589769484327491908668/852205449335098872376135288911987967369*y^22 + 450771356251383585332627266781109971860611239/852205449335098872376135288911987967369*y^21 - 219662258645122491798789725560213724284295858/852205449335098872376135288911987967369*y^20 - 1282250127493888759010296176767176016853393587/852205449335098872376135288911987967369*y^19 + 717781647513601360844668921478537196164392553/852205449335098872376135288911987967369*y^18 + 2171332773343286713790929097106041578441491182/852205449335098872376135288911987967369*y^17 - 1196697895936964886687079714626225579769938053/852205449335098872376135288911987967369*y^16 - 2242227620986091743253649606773729273150588643/852205449335098872376135288911987967369*y^15 + 1077526676965419652983308906027624719897635586/852205449335098872376135288911987967369*y^14 + 1415539238486096798007199766153556807849073366/852205449335098872376135288911987967369*y^13 - 456229723797707576658678827579738836682551760/852205449335098872376135288911987967369*y^12 - 549537824409781941843266692391242864263107141/852205449335098872376135288911987967369*y^11 - 31122790324414599740274632172119486490051699/852205449335098872376135288911987967369*y^10 + 155599189908630446304870136997861415912249906/852205449335098872376135288911987967369*y^9 + 138430584872180169447379664074228379961628511/852205449335098872376135288911987967369*y^8 - 55375781049733897285699498970054698859489719/852205449335098872376135288911987967369*y^7 - 73453208288213698326921967928765036809136767/852205449335098872376135288911987967369*y^6 + 21559179373467485897336395858153787266879460/852205449335098872376135288911987967369*y^5 + 19579650518583305169956858919833332920111014/852205449335098872376135288911987967369*y^4 - 4792406370572859075516675436899962325374525/852205449335098872376135288911987967369*y^3 - 2742196640330678368532807774555498929204846/852205449335098872376135288911987967369*y^2 + 396230729591123868728136693557487206886146/852205449335098872376135288911987967369*y + 164611365329487386862594716933153616554020/852205449335098872376135288911987967369

y^2

63468161496185046280025039270599789928462/21305136233377471809403382222799699184225*y^28 - 746045489485155589030632078696347490798549/21305136233377471809403382222799699184225*y^27 - 599913258958591115232109182427649556441101/4261027246675494361880676444559939836845*y^26 + 4004998269588014324933462677325661550175274/4261027246675494361880676444559939836845*y^25 + 38512859389850814710414229026423956920593249/21305136233377471809403382222799699184225*y^24 - 196224928914220407486902576543808922208462004/21305136233377471809403382222799699184225*y^23 - 49620983495403733392016400660295298366475474/4261027246675494361880676444559939836845*y^22 + 953108649485076952423804556180185133664306891/21305136233377471809403382222799699184225*y^21 + 970813961486226019279286242825047143815503499/21305136233377471809403382222799699184225*y^20 - 507788002962572466766563428459806680419296312/4261027246675494361880676444559939836845*y^19 - 2439913869633727525294189116243910689670206184/21305136233377471809403382222799699184225*y^18 + 3780249491574611192926427105166666915567882707/21305136233377471809403382222799699184225*y^17 + 3962326074661602220129504965144497269898955027/21305136233377471809403382222799699184225*y^16 - 2968640357098786578044002103462231047736347443/21305136233377471809403382222799699184225*y^15 - 4115604710785669243774102756576643405506193324/21305136233377471809403382222799699184225*y^14 + 790196324935305480755524246889754755635019001/21305136233377471809403382222799699184225*y^13 + 2678844135324874176658884463212340785494998806/21305136233377471809403382222799699184225*y^12 + 22334310700235428619663770904637167380476087/852205449335098872376135288911987967369*y^11 - 209322943901963546501705293187004530345292883/4261027246675494361880676444559939836845*y^10 - 618538721929360021732430765984605404115049053/21305136233377471809403382222799699184225*y^9 + 206423242678279523227864359102951685998645182/21305136233377471809403382222799699184225*y^8 + 306162187836885569212329665655197884199108742/21305136233377471809403382222799699184225*y^7 + 16381596264440452231688061644045546375089369/21305136233377471809403382222799699184225*y^6 - 108097493762691355876756355659909158791597694/21305136233377471809403382222799699184225*y^5 - 29308279157694208901407291603912259043830857/21305136233377471809403382222799699184225*y^4 + 26069639726733269875975966527726403547659174/21305136233377471809403382222799699184225*y^3 + 2054969461817233827745462927350509591352918/4261027246675494361880676444559939836845*y^2 - 2891011690521583152809121929770137321948577/21305136233377471809403382222799699184225*y - 1298696494018927295329250216436343601473266/21305136233377471809403382222799699184225

17270481516425471756750529794176334928344/852205449335098872376135288911987967369*y^28 - 198203748219636227399396901640560155500321/852205449335098872376135288911987967369*y^27 - 878087746633290807378864356980524217376279/852205449335098872376135288911987967369*y^26 + 5290279462896313917036105953854598136591460/852205449335098872376135288911987967369*y^25 + 12193141994825412040482989200351220989338913/852205449335098872376135288911987967369*y^24 - 52418898265649979638214688024798228987637756/852205449335098872376135288911987967369*y^23 - 84082783725891474716116010624067096092524248/852205449335098872376135288911987967369*y^22 + 260379010589976942181280959336446021433853803/852205449335098872376135288911987967369*y^21 + 341801068286162558540672635279323667121752943/852205449335098872376135288911987967369*y^20 - 718851503133502145314536291031686112075137340/852205449335098872376135288911987967369*y^19 - 859984527350079456058195631094335459407609282/852205449335098872376135288911987967369*y^18 + 1138864182623669143542350607311770366541272638/852205449335098872376135288911987967369*y^17 + 1349501644995462092982013262736948110060903908/852205449335098872376135288911987967369*y^16 - 1019831117321536329613320013208869609306405612/852205449335098872376135288911987967369*y^15 - 1314940837562408840352137908730695923109873031/852205449335098872376135288911987967369*y^14 + 444251859930331170351269804590547169557842137/852205449335098872376135288911987967369*y^13 + 784604720477745416024781861262396772022238394/852205449335098872376135288911987967369*y^12 + 14060946256520992468067308002803391995515844/852205449335098872376135288911987967369*y^11 - 283013015940261679305669246687977803687411345/852205449335098872376135288911987967369*y^10 - 131508228367553414815375843536396238356337270/852205449335098872376135288911987967369*y^9 + 64598379640622633158594980773233131460067388/852205449335098872376135288911987967369*y^8 + 85712988829989783416293434825640125800670863/852205449335098872376135288911987967369*y^7 - 10513154078699321761634638312495536650277160/852205449335098872376135288911987967369*y^6 - 31963474089496029807236259466190515636207142/852205449335098872376135288911987967369*y^5 + 119185319243010358077454182361893285469556/852205449335098872376135288911987967369*y^4 + 6808080248287461221002136889277605715391642/852205449335098872376135288911987967369*y^3 + 650780543649251985245024113972401916864517/852205449335098872376135288911987967369*y^2 - 604264315018484407052910586349041597945184/852205449335098872376135288911987967369*y - 113790504018878490390379077538073584340990/852205449335098872376135288911987967369

26434363419627313631062647054975895003942/852205449335098872376135288911987967369*y^28 - 307900048187250825041662657785564039882642/852205449335098872376135288911987967369*y^27 - 1288537855014148041461781204576368446520070/852205449335098872376135288911987967369*y^26 + 8286487805223969757046401892399977204565417/852205449335098872376135288911987967369*y^25 + 17106739578368630756113987518927874146009162/852205449335098872376135288911987967369*y^24 - 82320795390201317419905188103242595658464760/852205449335098872376135288911987967369*y^23 - 112751081292011809428191668757225075468892932/852205449335098872376135288911987967369*y^22 + 409520408329709010315849928858874125299990232/852205449335098872376135288911987967369*y^21 + 440879638661236038371168758644242393568225803/852205449335098872376135288911987967369*y^20 - 1134541363241531841201759753033191267980579338/852205449335098872376135288911987967369*y^19 - 1076052546774624454538222773982085480096121645/852205449335098872376135288911987967369*y^18 + 1813942611269017881302202296990170691903387162/852205449335098872376135288911987967369*y^17 + 1650748569156155887737867989520362100174937521/852205449335098872376135288911987967369*y^16 - 1663524810942298235881361998099997917671655597/852205449335098872376135288911987967369*y^15 - 1586523212054247229129822572799077397693306633/852205449335098872376135288911987967369*y^14 + 786322648868137698291206349503474615016881765/852205449335098872376135288911987967369*y^13 + 952073392255381646896420191901124967691868655/852205449335098872376135288911987967369*y^12 - 60027937157093869370150814002408524727596520/852205449335098872376135288911987967369*y^11 - 366128085053146109903345619029073132980404364/852205449335098872376135288911987967369*y^10 - 150498866526601120519867837923110232188630136/852205449335098872376135288911987967369*y^9 + 103240384709281182038051781332325655467568177/852205449335098872376135288911987967369*y^8 + 103907561480955296591009946311220314443856271/852205449335098872376135288911987967369*y^7 - 24941132640769433650021346959341772505833335/852205449335098872376135288911987967369*y^6 - 38003214086059999615743013876887483077842116/852205449335098872376135288911987967369*y^5 + 3294623425218258396544712805053107558993625/852205449335098872376135288911987967369*y^4 + 7933273241397751693618928496357217245135359/852205449335098872376135288911987967369*y^3 + 371481613294930927768616360068426083928712/852205449335098872376135288911987967369*y^2 - 699975826634997545074974888694297138280279/852205449335098872376135288911987967369*y - 113602555648894883746061830605530529691282/852205449335098872376135288911987967369

26434363419627313631062647054975895003942/852205449335098872376135288911987967369*y^28 - 307900048187250825041662657785564039882642/852205449335098872376135288911987967369*y^27 - 1288537855014148041461781204576368446520070/852205449335098872376135288911987967369*y^26 + 8286487805223969757046401892399977204565417/852205449335098872376135288911987967369*y^25 + 17106739578368630756113987518927874146009162/852205449335098872376135288911987967369*y^24 - 82320795390201317419905188103242595658464760/852205449335098872376135288911987967369*y^23 - 112751081292011809428191668757225075468892932/852205449335098872376135288911987967369*y^22 + 409520408329709010315849928858874125299990232/852205449335098872376135288911987967369*y^21 + 440879638661236038371168758644242393568225803/852205449335098872376135288911987967369*y^20 - 1134541363241531841201759753033191267980579338/852205449335098872376135288911987967369*y^19 - 1076052546774624454538222773982085480096121645/852205449335098872376135288911987967369*y^18 + 1813942611269017881302202296990170691903387162/852205449335098872376135288911987967369*y^17 + 1650748569156155887737867989520362100174937521/852205449335098872376135288911987967369*y^16 - 1663524810942298235881361998099997917671655597/852205449335098872376135288911987967369*y^15 - 1586523212054247229129822572799077397693306633/852205449335098872376135288911987967369*y^14 + 786322648868137698291206349503474615016881765/852205449335098872376135288911987967369*y^13 + 952073392255381646896420191901124967691868655/852205449335098872376135288911987967369*y^12 - 60027937157093869370150814002408524727596520/852205449335098872376135288911987967369*y^11 - 366128085053146109903345619029073132980404364/852205449335098872376135288911987967369*y^10 - 150498866526601120519867837923110232188630136/852205449335098872376135288911987967369*y^9 + 103240384709281182038051781332325655467568177/852205449335098872376135288911987967369*y^8 + 103907561480955296591009946311220314443856271/852205449335098872376135288911987967369*y^7 - 24941132640769433650021346959341772505833335/852205449335098872376135288911987967369*y^6 - 38003214086059999615743013876887483077842116/852205449335098872376135288911987967369*y^5 + 3294623425218258396544712805053107558993625/852205449335098872376135288911987967369*y^4 + 7933273241397751693618928496357217245135359/852205449335098872376135288911987967369*y^3 + 371481613294930927768616360068426083928712/852205449335098872376135288911987967369*y^2 - 699975826634997545074974888694297138280279/852205449335098872376135288911987967369*y - 113602555648894883746061830605530529691282/852205449335098872376135288911987967369


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

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

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

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

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

# 1 Loop Invariant
443334903494954389322376519477020273573113/852205449335098872376135288911987967369*y^28 - 6005674688583508429243513168262043257956165/852205449335098872376135288911987967369*y^27 - 11412764509730693800125869145608261613445615/852205449335098872376135288911987967369*y^26 + 175269794264497425083932304010020192763974866/852205449335098872376135288911987967369*y^25 + 5972669874359397158417632756772049370649365/852205449335098872376135288911987967369*y^24 - 1794864021601626817518902579402421518675315891/852205449335098872376135288911987967369*y^23 + 927116153809785146245745158379666246453451675/852205449335098872376135288911987967369*y^22 + 9147573788363703681704325956912996380739878613/852205449335098872376135288911987967369*y^21 - 6742148297361426991158891411469550638625115980/852205449335098872376135288911987967369*y^20 - 26475611774991526722242074842079490597091881518/852205449335098872376135288911987967369*y^19 + 21696723986358935435668694620652947852490474311/852205449335098872376135288911987967369*y^18 + 46103302582972081153962159735254235621461401401/852205449335098872376135288911987967369*y^17 - 37708257162903251727290086397897292236021998125/852205449335098872376135288911987967369*y^16 - 49783788182782991530919844554620767861248865898/852205449335098872376135288911987967369*y^15 + 36919779365662399285584892555816813784392595511/852205449335098872376135288911987967369*y^14 + 33797254985393408830011511661333632605612735562/852205449335098872376135288911987967369*y^13 - 18820026481323608280460358731199033333590613087/852205449335098872376135288911987967369*y^12 - 14897593574411870387049909405096697336031300064/852205449335098872376135288911987967369*y^11 + 2199309359160056907235689940622049116957880310/852205449335098872376135288911987967369*y^10 + 5199227394450359202489985745614430406940097443/852205449335098872376135288911987967369*y^9 + 2965980444102329429407844175836028980582217255/852205449335098872376135288911987967369*y^8 - 2138189328268760538874521801761904751206503448/852205449335098872376135288911987967369*y^7 - 1909113875030510265842422516156819947374750318/852205449335098872376135288911987967369*y^6 + 857420364910935850653289714234085039080925001/852205449335098872376135288911987967369*y^5 + 555933539728240860027783463282352319605831521/852205449335098872376135288911987967369*y^4 - 200507678507276276879221824695359708826340075/852205449335098872376135288911987967369*y^3 - 87959327099258998770953665143124717605144928/852205449335098872376135288911987967369*y^2 + 18128518036654163191375491275841299357777430/852205449335098872376135288911987967369*y + 6392867158957042347814030343091754908809968/852205449335098872376135288911987967369

# 2 Loop Invariant
-6126401399043814302760472455520957545471626932618385796734986650058678495250380884911487254153903240671432839722172773933214320643539119/8009928530244970768274089574930167822302739157308592962031689467489481783729351682573902690031958633455340034317347603735998904370956168*y^28 + 205773236441606540522552173276156192785843208904355600267619240194835632551272381262924912136227587384275549672445400635876998494679128155/24029785590734912304822268724790503466908217471925778886095068402468445351188055047721708070095875900366020102952042811207996713112868504*y^27 + 666159387672891548957801025472499945909913031729489268736240074468241659781673521594987017612176233429899980031510784637820361335559212647/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y^26 - 1812751958965348129432092517964957330301897534473840456376461810211362558249740920885017907293020962505060990336140828050301827096435055275/8009928530244970768274089574930167822302739157308592962031689467489481783729351682573902690031958633455340034317347603735998904370956168*y^25 - 29537237613621034248002736611132931770756254092694914713526020988200156644801645357493046540538813875205419208108732303495896504195298565959/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^24 + 9018997668808806772539128981858743440053306462613660791011584033386009738631622560350902773333018739481874825220930543931033333563527318295/4004964265122485384137044787465083911151369578654296481015844733744740891864675841286951345015979316727670017158673801867999452185478084*y^23 + 107111190960380701682310455494596457078193707704142163388933596096831516571841320201446270285301354834216435651451413114919229821449936589849/24029785590734912304822268724790503466908217471925778886095068402468445351188055047721708070095875900366020102952042811207996713112868504*y^22 - 543482968842200807537054106306320103191544257805635133011128563784900204612663147264827681561362673211772164926494497952826684068987926618313/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^21 - 898187940377954717014841667364916558920406944097586309316798067720667259189496046805006536214121352110062225124552042295077375038766016693385/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^20 + 1522837183269160460536786804663291909368731588553055941468274564170505358710410400467571661323994707674027529436845221224324599919061438701261/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^19 + 2286748499616918314741178778121218190762519025840073461014003002217080748157312495364545504457855859118626826923302967370962514954224826588661/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^18 - 2459897793375144733226727904310174496869039613105303183347164555817731396644543693262684999381224637423963734488772825724377158980069058509801/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^17 - 595605662641072336127878486208977221956964892658048873360302428424752616583246630165870069640356215483007733911100567564898732000905471910009/8009928530244970768274089574930167822302739157308592962031689467489481783729351682573902690031958633455340034317347603735998904370956168*y^16 + 565328598881325167654320826078597719826300197808588662151479460981887307147072566228422042287896822285073591376129652490957469422004886432583/12014892795367456152411134362395251733454108735962889443047534201234222675594027523860854035047937950183010051476021405603998356556434252*y^15 + 570595510059115067049277441314208141514025587478829754017502068870934330816722414162342521086433438168836994698382478599633724452874611762531/8009928530244970768274089574930167822302739157308592962031689467489481783729351682573902690031958633455340034317347603735998904370956168*y^14 - 1023828856507981774903516166420637522923648011660499468292738735538869993602392390429387240698658735733947802163276806410738621093084539309593/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^13 - 1981479682010027140870063384938627096474344427817015091185527628471477243143139460124188060334425945152832731541585178717039906905291415567415/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^12 - 1084741465767873304420581458747697737088210778568334009425585636810853530915180932307053512684697080295732939976195560238460050922905656949/2002482132561242692068522393732541955575684789327148240507922366872370445932337920643475672507989658363835008579336900933999726092739042*y^11 + 226437228148363532231335962419784460446526287101019069317179679839832413160403960500010380915142173405314893095607200234900188071387568609603/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y^10 + 324457221275536285057672695653396561525885961289055706080795217818079432464898953105615164220232840577959022097767413496761233235651425222963/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^9 - 48384708613000559450898466468219335827762688184181976495424110520401353124288347768024249688168215288249190300783944458191258421113124438659/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y^8 - 219333964575668963106019245555311947721265468059521213175751620497295219298088968964471020611730325585478058804081063238865056618938960418987/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^7 + 8301090293886112178245786486442348232169087392279578231112940254487651683162567421681077479487750179603916293484682128411509602122313071289/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y^6 + 81869629166066154238208980846534950441545642292017624514474433023139140505778085307991041153336209678159425112087989790212394707588521057445/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^5 - 442052633320220709841695603442131338415156482788265405063508626901774848177926405388498643451022264005567792787891548470903296788957934365/12014892795367456152411134362395251733454108735962889443047534201234222675594027523860854035047937950183010051476021405603998356556434252*y^4 - 5692876996925125183428631629649036121928969454159222298195279289768643264371322130312830142373397098375944577966043202954382663486256006193/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y^3 - 1150670746076926818038894218145544525041238209289455226735311560531712207158295079205349176086360785773892971190357954254219530292903314149/48059571181469824609644537449581006933816434943851557772190136804936890702376110095443416140191751800732040205904085622415993426225737008*y^2 + 492666971874689135886276071908675420014315847869919737512454831048842777203711145584959246480230236224031687334810400054261938952178875993/16019857060489941536548179149860335644605478314617185924063378934978963567458703365147805380063917266910680068634695207471997808741912336*y + 19434543400545228568657548664541053710091306563507415510442108676650451922540264741171045972259307247544512503087022961232358498312893829/4004964265122485384137044787465083911151369578654296481015844733744740891864675841286951345015979316727670017158673801867999452185478084

# 3 Loop Invariant
3507457795372544819355854508048181505824863627727434902004070360211949553327407818277472005872876695906873583875766933500406960680102149484806130186724322492581683411691988965474870179/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^28 - 9638980027620979366007464788420104028305866823621920145845241528639797736890327766890604691737371834299525492975442574725099343209968363641216398252249956419267580356036369008745635695/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y^27 - 197718940940992068797647589592363457849595152214351063882201086697384797834815901257256453818394618518579674880024590243136846400648125178536199571486700082945365583535781578030959018541/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^26 + 246736891174902317784319004398587547286418888709181248889880115818341771400633886343587913007510137080894181236198751608108115123181343490662510492856267728854029663136696622709391049225/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y^25 + 1496654159364960621280808430940294312284018250910205143768493425674971014017309686052744511509764352300794540653906006999115832226385712045807057302936427680053261965895967251197707836417/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^24 - 9415240476316442982244674693713027124402929149152247810541890568072514264398196535084134847931930542583976408587339564417529613716643278346064387947767573177655207270156035670600954907649/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^23 - 11108335289829739158396234514180586138147739334779342969774384674041210662106066151664615311119744203835784820788264006088593203025398996526749012204787939109210067387055973194296809050115/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^22 + 22150186956337549661566978057432950234796101991395421706526487241129348443414517973607188615785450115046491373974396416987739694912780803828447429555430984768829137085166468982808123547419/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^21 + 95173222635190746250897060432398937352596480115504836344652831367380791612885092035152036060064942371541099448766600963781219120189103634598474424563944218100807466869676394948996102083167/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^20 - 27723344491892523062973909928126959638861099557538113590416637256280941294549043862524683183297064250819914663265937430400594750502061766040723213234032032881835950368047205810997248483509/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y^19 - 247111963562545323313481718234458016183056190504213398835830231909237907669744436356733793870908302913621262036491199553317820783906808597415700091170101594520222293435185966597197583208535/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^18 + 71474070519573145609171473556868751098483177717843362498726475013920420886688756920739384282624481537987663037390456084958187081824399977334414782588524687058766489586180554489529805114133/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^17 + 98426595339718801508533757602546762870987116450172509513298901148006800066791867028166326697583685470556078534439544078135464511616132964976982923179171765616788809094997446054561907185587/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y^16 - 69268405281434565155327622811807696608577234989555732894692389257111289967132882933865265120147733687384403354471699966445986469567636409025058366724018734276639658630947942089788033652751/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^15 - 384740787118051389643529319596937992577354315377470236495921466884927372467611962227633012613011082830302164413791352112419744882083631952544924894734175280632804489266865290118548149369277/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^14 - 42579058971263954527159140264431594638399671868881444784473749716741605592466917021547973594985261882395210289621419935110032099417373461739006790249360183103297850985158644576814661072367/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^13 + 224976900055498670896699202450793406194383750961692437537908556824349402085071752583569148870499157748865108344906061246406232114356849625257511975879699205294967421372434543051895371562425/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^12 + 2530223449742449266758938389946280710130194398789142101802321501933054133792871473396590976748075179463294436630111250795127409660211411579857917757682562916670503160547029673139362053881/2170530152245024408512456286830403157812529247687244987896011218923017862429524163043035513807103269225962610074609516668778082564214833870018793520542188203428831151287692836915553274*y^11 - 70970514651591148111250483519446349471185893944988779487285357940552155421056946093472064169637507923829603962009858645861231151824758158728606602219356946572056561444811909396674134344425/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^10 - 3440053861815765070038806972778825439488648621041668575822496073046715238343632482420911234868554891710823021504387840578697162927867482428787495169666507769125636005058498141498005705135/4341060304490048817024912573660806315625058495374489975792022437846035724859048326086071027614206538451925220149219033337556165128429667740037587041084376406857662302575385673831106548*y^9 + 4808386988208277644028380681317085108017386377562067401796801295777290788655670405673858205433771747601636685549855133206347143855810580335617872464352672051768334543544432473500230397373/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^8 + 12539885589309756349329306803798661756739417314141886604008885688426672812598075360881647417427490107135165120538374009219568413614893578360353105549629089127487757353686476352215303236911/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^7 + 1534631933719221655321648451161707445049542306544208881475050404755705294572641605709529411998599183448125652110590842571792872879377456964533288085560819345602547079337058974945030236089/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y^6 - 8946160661629401663848767239393170055328360206843645375343169540049911257223868191704409498610273980736607035534839425506804647333628458829455539039018166548500309303038039378776119581715/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^5 - 3299575787529453192178643849377095726461919583921015339672239370297464229937607053509864657026481801325712779822934231806558161430507327296652005473627528561898252487591012735918823781865/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^4 + 2108192357150906353798026245314405765930859724140207909365970219800194246069252038806568005517784824118686275716828076602164717366771036433272823295845817756496126251544094935179082272291/69456964871840781072398601178572901050000935925991839612672359005536571597744773217377136441827304615230803522387504533400898642054874683840601392657350022509722596841206170781297704768*y^3 + 404561454008101418513598127416057933015883441463428093331732267480619920771237475228617513507731820801287988596131634461337248149903575440966943953469996915521986467054078774242863535011/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384*y^2 - 54550961120012733315208596054932127548912032061555407498284441803999158862910764179472163304683224063608922022480615989585979745870478245242696211195802694002385452512484787059580620079/17364241217960195268099650294643225262500233981497959903168089751384142899436193304344284110456826153807700880596876133350224660513718670960150348164337505627430649210301542695324426192*y - 38497196182188593490451771328723315340198841568802185701498748871415847422070614449519614421837869228288660737795188672558398440651814228547295069205676622265519197987299288666106536369/34728482435920390536199300589286450525000467962995919806336179502768285798872386608688568220913652307615401761193752266700449321027437341920300696328675011254861298420603085390648852384