# Manifold: Census Knot K7_62

# Number of Tetrahedra: 7

# Number Field
x^28 + 21*x^27 + 70*x^26 - 460*x^25 - 3678*x^24 - 16157*x^23 + 4149*x^22 + 308474*x^21 + 1401387*x^20 + 2912605*x^19 + 1148093*x^18 - 8003756*x^17 - 18493735*x^16 - 14609244*x^15 + 7624752*x^14 + 27863034*x^13 + 24798547*x^12 + 3979425*x^11 - 12305967*x^10 - 13276744*x^9 - 5809473*x^8 + 168928*x^7 + 1809406*x^6 + 1211687*x^5 + 455589*x^4 + 109061*x^3 + 16374*x^2 + 1386*x + 49 

# Approximate Field Generator
-0.282733766216532 + 0.456104979129285*I

# Shape Parameters
-161141631418466571679754274049160940930368469229535752781005423111768074140523233364828573/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^27 - 226847918467396831422314484686808909941243618087417231227942148817532205248906963384411915/343588896957903674698085108317274918581924398515585921636799013424390257921416452547921548*y^26 - 125461648013844710365473485781549546918787890263371930871500260281724213559663511098585779/85897224239475918674521277079318729645481099628896480409199753356097564480354113136980387*y^25 + 21577791745887043454813848947175338512772894808130268346771008948719582857710389446442182299/1202561139352662861443297879110462215036735394804550725728796546985365902724957583917725418*y^24 + 244997999974185484456042506063169948318533245302825594341403387991416921500760348586736178301/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^23 + 1895025185999469641688045361634468531722540150859263146972041425679215543302298399198296213875/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^22 - 1815859397880627913304300646361104799704303440531115642744383812992057697614465546903043129961/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^21 - 11791430018830601520323507571252822849886190682643595491397142986404564926810460477276768951885/1202561139352662861443297879110462215036735394804550725728796546985365902724957583917725418*y^20 - 162939871392009143290749353628205862694477794068062037265849338613512151016567984346765334901875/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^19 - 26612811380609550347427326540305004389200784448569231889993907937842480951421241833605700343962/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^18 + 275733646963663600670979668206029192481938013388864068944591774059250438152222876372180831198207/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^17 + 1262456850780334449611455611398222659791363822695456109864459867347472645454867494111609156441935/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^16 + 656994205994416647592461373048987099259954612793397072629707410634713335617714409679613982561535/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^15 - 280897196029420899391114088650738365248244079159122862160306739417297564999140850599563737674375/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^14 - 1290705903660487777126464969382913350797879294940297837558755950537431210567811780005819304217099/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^13 - 256193624985949219616834287540837514238591281685710992952243155170339059829916876115910005246306/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^12 + 478262517853507125502261049844642097360338794153680584323989354353817959675834446132369170920665/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^11 + 241328483130403956872859489511396667056399495760189354056964406965512792154528588627709739053477/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^10 + 1225305184864007801079893595728908720040727416012341895447233890920607992391180964822267073577475/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^9 - 75197416689159699317797208572725714776748361515646620919826201658696906760537990452991773407625/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^8 - 69598384913925639250020720772359798565628698744939586688150590676198311222617813558163686422822/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^7 - 41009297107887843413608094212554611451590521643284391208846619135410521819969056011468109694220/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^6 - 21319260355208158405929611979929639562951857626116644237433923177937577730490292500040721819591/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^5 + 49144017566912011649023110818592954517729085492650080400234156383444131006689277000318744920191/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^4 + 16614395568659368833472762945092596638696654312172544387794713624061287648234998552519466639413/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^3 + 9975209023071835680800612414922219865626364918497787958211887218831876679485711490136755194185/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^2 + 1564826944201013308096135192684074861498741050005347298977191362968684978898980931972067808079/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y + 13251569327783442534793574589930832453418779139650326689684908831798695708398104395399779639/687177793915807349396170216634549837163848797031171843273598026848780515842832905095843096

2972289928289495287220134266396753961617694070521757778369405234311583697334408689441930657/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^27 + 31929615742359025501986071345920072660520904631491434600120669725831928426507046272286977931/153927825837140846264742128526139163524702130534982492893285958014126835548794570741468853504*y^26 + 59318268369695223536369008078568188310572452773309132908643292880680611939757176196674120679/76963912918570423132371064263069581762351065267491246446642979007063417774397285370734426752*y^25 - 11498981218866216822232910547232127258820657466152678856888280018913032397402313713181433837/2748711175663229397584680866538199348655395188124687373094392107395122063371331620383372384*y^24 - 5828523515674811467372117059808620004975556568708731934125431475391869707317356714808898599399/153927825837140846264742128526139163524702130534982492893285958014126835548794570741468853504*y^23 - 52806569644271731856651062089834004078674632771867600726224481716994653459677500302572782733451/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^22 - 525858482686083344845031923754243026999301740961485844438235302478526806129464279645357800685/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^21 + 234475892942399751493700006294441889811050007399364310575148201779983206760706928407785436009905/76963912918570423132371064263069581762351065267491246446642979007063417774397285370734426752*y^20 + 4597387084648435169073725281851072589341264755032499018940111775096000786860286796825026072407503/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^19 + 2589706527276473910075054701579623096230107612406986392961961446845840357879202820235421472817731/76963912918570423132371064263069581762351065267491246446642979007063417774397285370734426752*y^18 + 6307388778351163432125518008976946650308700708475684101258803364057987771164589836990954322483433/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^17 - 3498912311381705754869441728267505729766497860464694973454556519449897697102607442719919192546853/43979378810611670361354893864611189578486323009994997969510273718321953013941305926133958144*y^16 - 4744394080736229014248164348767535918140299857862370214633613622113357934754714742809464404559091/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^15 - 30830455673864677075894770212041754368083638801074397494220998688201166470224587460516593230869971/153927825837140846264742128526139163524702130534982492893285958014126835548794570741468853504*y^14 + 8267046900385323228594612146780920310131905278577870544906077394503835879397186918353558416248837/153927825837140846264742128526139163524702130534982492893285958014126835548794570741468853504*y^13 + 3607141039166993701769470795211294825778246676741136103530372543508590921555206977677017410529479/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^12 + 101721139348473572015282010675015495326223125311906751146757574697912301089061700752725712588617719/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^11 + 3084287114852917309792446692274569710468230585042080098453014840284174220216644977598426419584639/38481956459285211566185532131534790881175532633745623223321489503531708887198642685367213376*y^10 - 44404680799597534065407532647063346036072939945331590309283947462110422900111639348485780863276183/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^9 - 53716573008005395729602299254643994781887535559485054129618663422604944319073855180667342238942879/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^8 - 392607567152277237817521514862297572837915629473706466439309486128132946047499358782992880214213/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672*y^7 - 168247912365263409279071152106970891042948241423421184251658483443083439458348014256964607645/1374355587831614698792340433269099674327697594062343686547196053697561031685665810191686192*y^6 + 3672448332619786977183598431464296364279603218297106617690562026829241609847311371685159915294895/153927825837140846264742128526139163524702130534982492893285958014126835548794570741468853504*y^5 + 4996233346276159796465305276445393817602745557936298989818182457917026596300944736945602970553189/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^4 + 131020548205153689804715258662786857070375876032766153499384468914049291405386072080220279905123/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^3 + 409918522795378978497628398445384387769371361574763962722657750868876659057374716377082606068495/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y^2 + 52817495058365036926870290417432589225629679497770298380132279099523558883091010335868718732933/307855651674281692529484257052278327049404261069964985786571916028253671097589141482937707008*y + 486435527119551987629794505471708109157007722088159660619298001021977502275621462299916948057/43979378810611670361354893864611189578486323009994997969510273718321953013941305926133958144

491037768248104644005555731170634971372560129057828066787141750220629731672714739186242043/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^27 + 105238210552733372329887480851919453292328052702545657020325122581827936357277237005240912/85897224239475918674521277079318729645481099628896480409199753356097564480354113136980387*y^26 + 2455752666721149031955049401226014081238231318286150941490087406007429910250484964550268299/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^25 - 113136099077610638121304095886306407283765478742571248612632395811052027025805472005966515103/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^24 - 904085548709202314306952450395840886670660074188397126916890084633068606480654021981872427842/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^23 - 7927154018959363737239314392462671978649321504284278737859116393093285132843638512854489872603/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^22 + 1047839740567088292293241277450121755636003531512150504548774375685897078604152319860498289525/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^21 + 75913120027400863720911093009683062464630239080601720419473743625530474309437273732421870649457/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^20 + 688293997859000161976773084566268610503979651723265542980417320137843658353999093047092127063597/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^19 + 712465823135467301103194448811577273750006993507677503651442437098078920704241460617684091098427/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^18 + 538224911250062364291151782116198453776450954024486889156467441837170783495450506558818607382397/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^17 - 3981562508630376454609208469001624718857515858415216891026836160511158258362616831215493770872287/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^16 - 4543905857307310314226654154506227005170450069002388050244393166087680545332869154356909274024164/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^15 - 3502645293656200868264617617613411306007846738701032394567141176827442843326342305934702092222583/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^14 + 2028790184504366805274034578852630252080942816310390904240641640475480165021967839926296263699007/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^13 + 6919248343824828308355596938687153926533480643688607275824377173262129434571290163239453478652012/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^12 + 11925129399960437303744718401885010654937694714883575984363111819092295675966584350955330184780305/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^11 + 738321848634269028375928062286894202002438942216607987771704103239630925357965649106325022568155/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^10 - 6317863833347399549574721149250112915574477073894845156591326403045669557414237793253203620919987/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^9 - 6436910210415642287772899185920458507728254888537196922631341971492698591239154864571341707071049/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^8 - 1308125242870279032683636530947130809530891847113517514017864649597114823268105245261901403104988/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^7 + 119606776048538195523311487907147155725989874807783049304784022310696162908761548802632105499938/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^6 + 458682139319691288756378980954398732405882061543452427400035960817156574927498846867350549474754/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^5 + 567305065707658500769209282465906017588343814810790461352842253301954229406106012413904829477751/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^4 + 99028723471864003857367735099699683029394338401359117783614271547116824532744319687576356370675/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^3 + 42813839572040939788888776913598387427534590221857408468042553279510205508434329445085183373187/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^2 + 5418265356147333721445018207678448874543688256102927239294254662247612555034487015409422389599/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y + 46414545725990406652186196210999665942612445246498106258289839871541979210938873516725045399/1202561139352662861443297879110462215036735394804550725728796546985365902724957583917725418

-5949041770584057993955164337013178178002337204767719763901033289773392151864715925558354907/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^27 - 61373590881147385176230817047941194039625165876678298642586261012244963459747087511677527993/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^26 - 92841222030230936881766646781599759053487258470576122432459525669125621820133012830308401957/5497422351326458795169361733076398697310790376249374746188784214790244126742663240766744768*y^25 + 179591667527121545037098142979549712159717343822189192167111527976106307281185190512003008879/1374355587831614698792340433269099674327697594062343686547196053697561031685665810191686192*y^24 + 10414043735113612882727940296336071904144229996865967436537472627829616108357206403944171461485/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^23 + 88460676559423383837683745722909903310357315684371586240365601464767399352946825164159087150057/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^22 - 28622914688427725901146427554676378987400079033214093354976211656954664177741588510794677347975/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^21 - 453640878095365483083503393344257825003172774172144903703108225412906736850866437726147615325067/5497422351326458795169361733076398697310790376249374746188784214790244126742663240766744768*y^20 - 7670684939956069508978087996468442420812925470545537632041880124584074132144857911733161390272117/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^19 - 3625795641600190353730582823796940237954153965354757690127486077277715876007988471121187674882457/5497422351326458795169361733076398697310790376249374746188784214790244126742663240766744768*y^18 - 1470668141423557573176114208582653804025203074555549606413962073507468519227803001772601126564883/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^17 + 48219671443377762325521029241332993422940014937357287337045069841988720945413655929675841582874865/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^16 + 46157098173176887283493736411904781433880724048974029640530970110096347302803624517342877065023383/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^15 + 26393200643708030707022084916806346622609451647239024792206787765409103511971012017661295790636881/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^14 - 32569165412074251965436651519455153747187583754826212122370964046511299973270442809891233817749911/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^13 - 35501918391923855848990701468789462097733101649759198225587171468676391976961657415421246811615283/5497422351326458795169361733076398697310790376249374746188784214790244126742663240766744768*y^12 - 95030992449442593891809224240578466201447898701502203444385826320225336308236233870145116132371405/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^11 + 1477611241102491680182123464323214279576049953849090194030909931600652610429813339383332327064179/2748711175663229397584680866538199348655395188124687373094392107395122063371331620383372384*y^10 + 69178036384250975993561305915688315313336209412518143900484642772777022690002223496592002224167885/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^9 + 53448163124639016338534091708989259652908912671658456580268830753653147182478285217716154103903941/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^8 + 228701569159345957970764568083813044603412344785479842012067881084431833979613310582108957675181/343588896957903674698085108317274918581924398515585921636799013424390257921416452547921548*y^7 - 205018273180797620498376320228639985994423847579565139399251491503742592401029489253975076254051/687177793915807349396170216634549837163848797031171843273598026848780515842832905095843096*y^6 - 4190202213235969191586007954127307118475719327014679009311020800885914354051918695418984411123797/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^5 - 4094407337960002845298469658604132002703864398354824045912547968002433780440008813689593180483783/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^4 - 588257594023892128559552473985629879088882167782958528366724873027093717250250265042687220103559/10994844702652917590338723466152797394621580752498749492377568429580488253485326481533489536*y^3 - 204846218833748941704378566364194097659857405558559354765688937701933607503510633671232209909013/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y^2 - 19430363639399663742635764639639244844828148134085044824403576764217302258948542107980089485159/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072*y - 740007690727463290656334817672998189342067704655217167644463798790402081703015371216245372469/21989689405305835180677446932305594789243161504997498984755136859160976506970652963066979072

-6551293734318048654962900900113484495802483352528468267638488909773666908266870488652227287/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^27 - 9814978516026675753421923137913285791871322995288828948927377304479320796085126837484993129/2405122278705325722886595758220924430073470789609101451457593093970731805449915167835450836*y^26 - 8121448314408885375414748177826738101409372583031152947728723374852333112076959212341040712/601280569676331430721648939555231107518367697402275362864398273492682951362478791958862709*y^25 + 757716510778022491503546501003020831420420152822165631633476767127891909405611273791248727035/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^24 + 12017044423114914139678411162696509431553682861618645105843875807871213480484867750020652149295/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^23 + 105097434735546104852048680943075926376431740023040128597579033577214239263906501793646098516161/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^22 - 15401499787931496181400303125113246138085440542153777586617933338293875297257214790781720683411/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^21 - 506002273937179141545447127053389967997602155597066388482199234088924301504787014249262987104121/8417927975468640030103085153773235505257147763631855080101575828897561319074703087424077926*y^20 - 9125571080736033447576112627182843514347478253499833973652759572240974502555503406166198812222481/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^19 - 2345577157023206507662880740218016773819934223815819203254792286691254069554181808392366068178891/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^18 - 6705130131380648527441761082277075766728877537504176320900788836810449826474838904989649982019595/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^17 + 53201707178734790994811594107619890995513750631455768829856931934371659133212456316495099134492253/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^16 + 59865841370411092189186811359167500555635856862635265163833842332781433641020397886605500294956737/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^15 + 45219688386365592425950411304378665916125421812367035535916837139019692046545964797821240039550479/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^14 - 28012902978323596495507338818749773439720664558094222966078546405762105793373782318223398229206325/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^13 - 22839907741823106000571461010050320392610326172697597994957886237668363304504453054514659740005901/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^12 - 154479581696485212661435981324725952401034458813549456488803912658342437253549794753068439523196653/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^11 - 2043711955963544611249274497938786548062594957346846279992927566219421474525114039880991483640173/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^10 + 84174919058468515496866661656877550271719892770579113463045568093059900563264245506431508719858417/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^9 + 83682145375549576632829983594254773470066997894948272394816072061684655654895700110515508223039797/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^8 + 4130492602648332522984913516237095997028646926872662000852745126835776705058404080462430426174834/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^7 - 474488791162978771838320434161344163421243719710375659498074138598882888170209085111028018495808/4208963987734320015051542576886617752628573881815927540050787914448780659537351543712038963*y^6 - 6036596460735614018686566346863781361199322302710265760586379492653689518931009463461140650749493/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^5 - 7287319971412147563743617488779014286716519922893857762007980558316592388638721850584179599012939/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^4 - 1245375103430828069854349827229817863395809353253737027158088480856610876285408726889346416964349/16835855950937280060206170307546471010514295527263710160203151657795122638149406174848155852*y^3 - 523245170214372059514919841279340858140977954857545570247104151062115209313256792491391279149005/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y^2 - 62889866087602119897832787689371855518974727515644600610581011290949696933445156170957938044323/33671711901874560120412340615092942021028591054527420320406303315590245276298812349696311704*y - 460718031127201548033453831779399094976192494036631450795277229961348995154541129513518878027/4810244557410651445773191516441848860146941579218202902915186187941463610899830335670901672

139582791875653725102777451391467156185532907114423259430004504823886536818867028710184640790778579/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^27 + 1433909383906518413632314355910531516559852892418702628455124314783149548406557243315059190439740637/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^26 + 2117772646931232882474540267337887865081949319940579024889468854199500727898394389241896616952406287/51138777764124380684635760659809945322669088549699301501935791535339422652397716060851874615203184*y^25 - 8498838637239105887341607937354273267348851785925901613102973679281517337916338996494080709414908577/25569388882062190342317880329904972661334544274849650750967895767669711326198858030425937307601592*y^24 - 241161938729803634242389445140364022739587595124307421076060557756978466077389891395200005836631301761/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^23 - 2037778492046420117294346934701899241635461838170353102164535646548867073510831504517540433817391388857/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^22 + 747185896197262152557110039328972726559908284698518113760966684517732429312684950903175583021312503895/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^21 + 1511979566419207036412599463899400769281915847184900778365283349784735766954668167554641376204430256653/7305539680589197240662251522829992188952726935671328785990827362191346093199673722978839230743312*y^20 + 176429477219950255820444221586666938490368125091098758678680776238518607321904130077573021448125099585085/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^19 + 81840961863215677977557402276555978627803078783833172195960258058949062379696570567435928725721797675379/51138777764124380684635760659809945322669088549699301501935791535339422652397716060851874615203184*y^18 + 15237017459520503907601152690335451315770950558587502176895919499572991382603559636959781217723168698547/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^17 - 1118089532495974281729576824122313538558812875891210029899408017830772519130315335874849938710877776274489/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^16 - 1037921619833311698897019430124806679644363285857922520064008451677435335900742524536851309002220717160979/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^15 - 560709338981459790350746561507846712697022321885726157649731369423090757152696143627510400889352988002133/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^14 + 109742887452690146462569309801866334157635989501235522039549072817159215519398747795377931906472387433213/14611079361178394481324503045659984377905453871342657571981654724382692186399347445957678461486624*y^13 + 795524517551083702844309535999264885280163649858504708900504999836721748991656717487368610900792050301237/51138777764124380684635760659809945322669088549699301501935791535339422652397716060851874615203184*y^12 + 120976325995490089094182053731019359406602776146978373782519153813336866745262783437422271031059802260173/12032653591558677808149590743484693017098609070517482706337833302432805329975933190788676380047808*y^11 - 40300180170789148603025629579181859324425484102255212525652015065074625553411064544386007143930698415993/25569388882062190342317880329904972661334544274849650750967895767669711326198858030425937307601592*y^10 - 1549070177223034907072273826031217885971333442439016795461181289623693615121223057087195206311513044635589/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^9 - 1167882339000515246765040179473983417118905385244341846555433880226916379057209246812456900956939187987269/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^8 - 4823193207482458675352906240901344962042464480846391869873390402004749947861007837025298554900729381019/3196173610257773792789735041238121582666818034356206343870986970958713915774857253803242163450199*y^7 + 4671515512131019305581844966615193334326109770138985101712864352847553480158360037404402372860731226629/6392347220515547585579470082476243165333636068712412687741973941917427831549714507606484326900398*y^6 + 13163346039091676873473327915990913088311712586047719407672586176995085625132759833868416607165209502747/14611079361178394481324503045659984377905453871342657571981654724382692186399347445957678461486624*y^5 + 89283811883591689396761157515720430759981336032655415038336157094917471632046604728214502010202980721007/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^4 + 12803679144147177068880013238774086356298534220401478418025084874611564926806608166440551443107008315731/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^3 + 637674487194082443565069110839208859828255758512080974603029406138453845529971381032909330501378663395/29222158722356788962649006091319968755810907742685315143963309448765384372798694891915356922973248*y^2 + 426463981675854516528220008224084103973359098559275345833760849112808063153751090811740845504793905055/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y + 2303036906444764821299634350724547313753442979447767596860935128782413916015661466308481181301629603/29222158722356788962649006091319968755810907742685315143963309448765384372798694891915356922973248

-1521509084312987465441697798580656532968124043308786409228798212244403044807503226452723936460329/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^27 - 15835541790490928688161187571144772278811388655837305677977197548705446052210384308147412858848063/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^26 - 25135356606745265933896973321483198993333080429024861811792412395154646288367450674728076316949041/1043648525798456748666035931832856026993246705095904112284403908884478013314239103282691318677616*y^25 + 90115042201798898473232614474503940621394104757348027899425833991357914983841549779945272201221713/521824262899228374333017965916428013496623352547952056142201954442239006657119551641345659338808*y^24 + 2734833714218731423252233202695166111674382094102523011355195498145636104045548247369874800520581099/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^23 + 23511734154104224517854892844817777591186542147935615488803377270936971909822404843259838350109261707/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^22 - 5525199438431988534673866770426378425505549584470113118751599421775635744174492616152522689860879141/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^21 - 117237802439621889224430416605127550681422161242537099379982523463409885316313950708344475570252795025/1043648525798456748666035931832856026993246705095904112284403908884478013314239103282691318677616*y^20 - 2043780465863022392294113055449431449617461760339288934829403672090383630530533527739930358376353232647/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^19 - 1004505360883562376465582672994032159906230484912590069143216818846273758808904374412442321614947104861/1043648525798456748666035931832856026993246705095904112284403908884478013314239103282691318677616*y^18 - 864262523472575600134894915732334533104673634333969939276339372355314106776105585097273021090399438617/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^17 + 12571352665399602253129841274429932219747135473837088284906642403768949932610545556256437219092615345851/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^16 + 12871460758019077250127467370827301808601630807578996149253419733866251081296655338947971670996803012081/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^15 + 8261958742023846099233415351563708832938201269030953056717712989804278935856807523614228941230061798343/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^14 - 8055276597168088362687682773173012579841097442010705366196585995827263190877724146851115724474737548233/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^13 - 9962156186319627337517926778695146329605249277745727090861640429473533490564247290810180442725714359155/1043648525798456748666035931832856026993246705095904112284403908884478013314239103282691318677616*y^12 - 1697878876076428706106052578211012268743873632757616395654879874569828427850743537939708631215259978951/245564359011401587921420219254789653410175695316683320537506802090465414897468024301809722041792*y^11 + 186244316522676781647089418222762702621795849607384130974842968516574055922413398397966644633067427839/521824262899228374333017965916428013496623352547952056142201954442239006657119551641345659338808*y^10 + 19408671418034282767236439440641486415023636026318039876247522290700592764690215805479791091036796677631/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^9 + 15968701450608228442385726909773194852118168191269641529541019187905488710820582139878097130862410282511/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^8 + 74663258293751482442044508149789382854202104148713695210378208291878810907666382735652719984516321329/65228032862403546791627245739553501687077919068494007017775244305279875832139943955168207417351*y^7 - 54383353270114927996065106348584866880837646031632094454413826308508310612888036862010178655541790933/130456065724807093583254491479107003374155838136988014035550488610559751664279887910336414834702*y^6 - 1236448603698095611271236025650348980496788288574603783377608766892632161468965573290426523049495436039/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^5 - 1239372565144677596087941214294743071288176172179614875649512214394664151416240891702051789423267787165/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^4 - 179348960212667840416170260992199034380855419516077986704154981017437978849921372761717451342885531313/2087297051596913497332071863665712053986493410191808224568807817768956026628478206565382637355232*y^3 - 61810123325757203767418793018281420539886193971138010376343037140079365336142253037696964948386854687/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y^2 - 5647011669795969286302136193840822720723077470972519453674675724432583597722611956457977107124255949/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464*y - 200816304812122000875731570307985107274954646115263283210265864268290784811751172866534261515635679/4174594103193826994664143727331424107972986820383616449137615635537912053256956413130765274710464


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

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

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

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

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

# 1 Loop Invariant
-15517228165921055874055415533999628073169674636704576517486618368458633905721821521721920564232989739/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^27 - 22926081975279219711248715018495072225407412754081886098500198289538218517555876890128534078961477691/29222158722356788962649006091319968755810907742685315143963309448765384372798694891915356922973248*y^26 - 35168889110324043539684458491566364549002999591019495325398748946154505413969471387268832431972666605/14611079361178394481324503045659984377905453871342657571981654724382692186399347445957678461486624*y^25 + 931570387143787584277677249523648012204235034874487904833618419413976884384196090698897318675073115687/51138777764124380684635760659809945322669088549699301501935791535339422652397716060851874615203184*y^24 + 27365503908117246476925399426125827059013301165712299975014205568679508081290992457082717223804492644001/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^23 + 233343434577833292027874532345559263620394592062461572439232674807459952270676547105558999284839097747409/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^22 - 69324289320390589237350581649682253738465116590800974338183362723990541015008767766912790155487776244607/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^21 - 1186377370264744937915626723126364853045995595500915040324232905437182103870756252678328510271528282048115/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^20 - 20245198817980536403673957190743528585063056257507371357845659901010901427729754031181079724003967755971237/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^19 - 9687364872751780277144125383213160558966501684285591442392391565687501719510318465408060109466681687973327/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^18 - 5363111490434491203374397923257502757245247767082334925146363978748512327952196864289674279258623339329179/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^17 + 126264763671211548394044746511542993209732317381171437085155126753272969642416408586218996164878968904671297/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^16 + 123510252423015612939164453943290194560817328537681931373713419867501281737013783713752729754392265540052595/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^15 + 73617731127070698362605702570385648825228425941368561709219646249009154186855050305210182531136002398342453/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^14 - 83566496814706710049504164365603246512957931898095346983037171513157561535848712135843744072689891802636443/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^13 - 95090940191053888214012382798387499359562233038209316348674935088479341836086207496838288273891951971928977/102277555528248761369271521319619890645338177099398603003871583070678845304795432121703749230406368*y^12 - 15435150098446700081077017239621245373456835270035225143963932522826719821904363999741880036160737181943365/24065307183117355616299181486969386034197218141034965412675666604865610659951866381577352760095616*y^11 + 3079996242869851203907375030044603129020143668069920926453560706049065424097536559208702950555898909964605/51138777764124380684635760659809945322669088549699301501935791535339422652397716060851874615203184*y^10 + 184797588625621746673501934539268407921406623040693559728864294235484600036008724239400484427957544414622221/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^9 + 146706985823063068202143605780321829836849689306734708034880361865309612682862433298071806334398325138558685/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^8 + 328546300617155251465500992926619046282794953954579433405039980879137637789129850660002512473875265627607/3196173610257773792789735041238121582666818034356206343870986970958713915774857253803242163450199*y^7 - 527864114445836017472926071871839835614319782007713649334510363254828363896866346820425904041411651610433/12784694441031095171158940164952486330667272137424825375483947883834855663099429015212968653800796*y^6 - 11416939898166358336403164824032830074086724912492004678891555776878009042629665851120775405722422606335973/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^5 - 11362147942465509427857129217689552876154468261677933336320433827020425921281616958300876125082583042613063/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^4 - 1654976099967105310066013649307278115991462800067453171310007479389713128176160992423047247800869469142035/204555111056497522738543042639239781290676354198797206007743166141357690609590864243407498460812736*y^3 - 583602954218551737965243286500515364108519006847202914014990903170163366570108512433912785961313886161165/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y^2 - 56145139164748802227393870924237855248046037399339426830254045613323721572188328413866424218948580774551/409110222112995045477086085278479562581352708397594412015486332282715381219181728486814996921625472*y - 311662457765868011563501559883301762739609608787887479283206133617307440557479367802882909303989224267/58444317444713577925298012182639937511621815485370630287926618897530768745597389783830713845946496

# 2 Loop Invariant
532489304698191970246252896286655637671397436330453969333235160912812213599235649352931717356046423550993917290019239427016858902958751180985914032811819164206512869021077212860797469120768154525/10793706014829457161786998531405482798293375266927821004726564429035030832542561639539660041947078611207790640527592590273961294778115412724312590986964945266611988138610170298455325868189386034432*y^27 + 783402656478136753501878089242695369001941128501579300994937680557503852169929111150301487540668180807184070901668652650339871479049638909373072878926666333871463134085731768262133429272393571781/770979001059246940127642752243248771306669661923415786051897459216787916610182974252832860139077043657699331466256613590997235341293958051736613641926067519043713438472155021318237562013527573888*y^26 + 391290059700593151494759162456635904009677057861060108543679576327488788523932676417022543059322157929925691006150332451282436768324503828101854029743765192013031571834798161416668694410889928173/128496500176541156687940458707208128551111610320569297675316243202797986101697162375472143356512840609616555244376102265166205890215659675289435606987677919840618906412025836886372927002254595648*y^25 - 32236464173499303471869467879693305620077602297719381999004764213179749829867220775899605782405074556014503528594457912773403260210751224414708274691796657089713626582232408259702393562134731166355/1349213251853682145223374816425685349786671908365977625590820553629378854067820204942457505243384826400973830065949073784245161847264426590539073873370618158326498517326271287306915733523673254304*y^24 - 926877584910953320550321006694509875993211798427947518777759481243880172566962382658339349822038818879868786795615322341456087178882931696220625633874079573574611306441248316969911061163401825755007/5396853007414728580893499265702741399146687633463910502363282214517515416271280819769830020973539305603895320263796295136980647389057706362156295493482472633305994069305085149227662934094693017216*y^23 - 7863830802080239466058748217445083725001910465966507492254949076948165185668214603613943684656197439331150461218328101394564309179265046325045905509010961231451728187707358273971608686464700788699319/10793706014829457161786998531405482798293375266927821004726564429035030832542561639539660041947078611207790640527592590273961294778115412724312590986964945266611988138610170298455325868189386034432*y^22 + 2665173402891754590552027036347440830212921230469014926001459146877224996477991748967525628567505223114867830724820513275065699592813866191883836905132564250082184534957368993823165157377465087918017/5396853007414728580893499265702741399146687633463910502363282214517515416271280819769830020973539305603895320263796295136980647389057706362156295493482472633305994069305085149227662934094693017216*y^21 + 40477792074408004488938766799332903052978618914934417963578285402133906960237184471712420512589517500983325468447746189324024659804931733742819040655687179429381922343310254853670070038033038235733961/2698426503707364290446749632851370699573343816731955251181641107258757708135640409884915010486769652801947660131898147568490323694528853181078147746741236316652997034652542574613831467047346508608*y^20 + 227066777284675027142674203803024859716807773696915560659943917074195678442742136305551539775001044804254715037629484025279333155289532724093879008925730748831692167851479719860113065736573112810245921/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y^19 + 320199879137155720509566570010028485356005920414124556004320122464382897611942496754886545862043376217284281054036402794185304914046189897152612733398682560934577242074009460098002089958908904568708713/2698426503707364290446749632851370699573343816731955251181641107258757708135640409884915010486769652801947660131898147568490323694528853181078147746741236316652997034652542574613831467047346508608*y^18 + 37413285093709193583491711900404934409435507349192545868128145162896772287277310742258805204732088876669191178132028538948182681116947202896879827885900855359795537394871112270079593200135894526640511/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y^17 - 4278867940004077582509878009567210863937817685808052059162374193669593044518335859054902306673226304758772002820505088672702837507310356780051720270909590367935352936451209360274207762664708567371383575/10793706014829457161786998531405482798293375266927821004726564429035030832542561639539660041947078611207790640527592590273961294778115412724312590986964945266611988138610170298455325868189386034432*y^16 - 1355432061898456574760215037715671078376315755370084144599417299581997686025115653063304816074805699192207763449967090958125770826179048745952749851413871497493418986485706085806964395147545143167530519/1798951002471576193631166421900913799715562544487970167454427404839171805423760273256610006991179768534631773421265431712326882463019235454052098497827490877768664689768361716409220978031564339072*y^15 - 2839574888375815681054415832714946208682781706099434751531970403044326894719518014331706675255074440453598845204447237935132265704260305837245942450187746167175996693955533862574228079019081757320535/6638195581075926913768141778232154242492850717667786595772794851805062012633801746334354269340146747360264846572935172370209898387524854073992983386817309512061493320178456518115206561002082432*y^14 + 2872408526920226973211380546575214188211284627111727971451446618353449078834328267052275796911224614407549529206266973781682407896377685708426214344519095315369358487307624337914115116930484481870530237/5396853007414728580893499265702741399146687633463910502363282214517515416271280819769830020973539305603895320263796295136980647389057706362156295493482472633305994069305085149227662934094693017216*y^13 + 3117667900690945584786481625398248808657788485451785181613157782404616554743180144252336535451823186126247127981715321066523804976742162708303405512803762088969283838961082942098063014103681400916458435/2698426503707364290446749632851370699573343816731955251181641107258757708135640409884915010486769652801947660131898147568490323694528853181078147746741236316652997034652542574613831467047346508608*y^12 + 491894766771101328838878942709484976244145772505886539500083998435383222943566002291073407874001229671813195729785376238967931172051895620838360603870591478378637647568742713148477034471314840060056275/634923883225262185987470501847381341076080898054577706160386142884413578384856567031744708349828153600458272972211328839644782045771494866136034763939114427447764008153539429320901521658199178496*y^11 - 123004166889632274467390501284533521338428055079296368046476909135056079280937380715157848305739971339074414874031889234494536219151290615274877220145966949054286827025086982123915321161988726487084011/1349213251853682145223374816425685349786671908365977625590820553629378854067820204942457505243384826400973830065949073784245161847264426590539073873370618158326498517326271287306915733523673254304*y^10 - 2013743736143847229618477488310149286499647499779338352223089351021918370807842231131325689889148471905618985332231894756002581812875042025259314806457664281820397655148793958967901221926532521681906313/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y^9 - 4713538362944282795402112903698838349991195999891584391857442328078493288094896355080137058637618172831110836489830595810365813431764907405893313768932053252180824932835335195639454176216433067764997115/10793706014829457161786998531405482798293375266927821004726564429035030832542561639539660041947078611207790640527592590273961294778115412724312590986964945266611988138610170298455325868189386034432*y^8 - 82984578305497806890615322394575798522230386312084093234753167523434754074748351306793111271412551792573311784233108293756060027718416967751058003100698596223815483568543331247366236223786025947345221/674606625926841072611687408212842674893335954182988812795410276814689427033910102471228752621692413200486915032974536892122580923632213295269536936685309079163249258663135643653457866761836627152*y^7 + 17275830187667141927520654236266423067279286617446682710329146201138856480221275397245522861503765806217924461071834160012172688421211545354365075498202760412838174992184218674188904122435504386628405/337303312963420536305843704106421337446667977091494406397705138407344713516955051235614376310846206600243457516487268446061290461816106647634768468342654539581624629331567821826728933380918313576*y^6 + 122615431463259946817616895622662525068634600378342431564751020013733410784337987067242262555901959216862136314596295583974478509098455734620490927165130528988696522937346923185395359582704573465874241/1798951002471576193631166421900913799715562544487970167454427404839171805423760273256610006991179768534631773421265431712326882463019235454052098497827490877768664689768361716409220978031564339072*y^5 + 122136635737270876430569230331255735164731205967306969879215645316396107723851419631484593476304069951630328525840098379957525157505707823428166937924843477246530553398298755173426783474983146708357435/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y^4 + 17938619808448712619721102574951623483308437653321243411481347517762598227194417769947638537764522702793479151321723732826483856722381391267114530343832640143785308357567206367673984959321219576433703/1798951002471576193631166421900913799715562544487970167454427404839171805423760273256610006991179768534631773421265431712326882463019235454052098497827490877768664689768361716409220978031564339072*y^3 + 6426275090849298972669791926280205688696031038342847717346178550184630366724671910562322289177980304278484839172779498620073980857957542863250829046538390029422059427920158533153878831385332649987097/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y^2 + 637085810138851796968714153711754611757623100876699304966717538906218616154169674999235619724354163060592497796481145107512233203698361359053407194400200249018291895179174266707237029509766353816459/3597902004943152387262332843801827599431125088975940334908854809678343610847520546513220013982359537069263546842530863424653764926038470908104196995654981755537329379536723432818441956063128678144*y + 10783785422171787064733336640594257227027395053266870778271920814387230095537612721243574652182737496461485265733866499739432220823426146290318962202935242024278140786030197617329017271450314301581/1541958002118493880255285504486497542613339323846831572103794918433575833220365948505665720278154087315398662932513227181994470682587916103473227283852135038087426876944310042636475124027055147776

# 3 Loop Invariant
7468131396795157259319924620438854848242577004099248781226496646407892502456440571777260362156696007601717244919393210307263075195811814363008040550291472451981849028347257005990615250974565481422177410875988660711139664264076769730745022811/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^27 + 11089222071960368201824653875199015145037919521114523983050174133380676984672122880046789479260658837655857863151575023045611770214648509754331044263273073464004755915672644889666131216964191365747654341954808593850814980238382389534001810783/269451621198418461253327042921732368982579055482946887181963637797635164065160314264679853684449936674416910285882827210449033567471884900743833435983463826877264682170495156575191889552839470625682898050684016927530527740056729687709640326848*y^26 + 17497703276186667277209625581902631918528335014786063056055980110351982693687161074840354544772467886159890118519728297681423408193873631037475811629981359472350357495592681166639823243607309924217862268896875358408686951947548077806928109593/134725810599209230626663521460866184491289527741473443590981818898817582032580157132339926842224968337208455142941413605224516783735942450371916717991731913438632341085247578287595944776419735312841449025342008463765263870028364843854820163424*y^25 - 1769070177383465653449949964584835660887030534785576554604037609073696229937505073163504091473162818127554521621550469156440863381361016786907672132200687351184192646271676386174656404261511280883784865032396977864243571952405149940282195231693/1886161348388929228773289300452126582878053388380628210273745464583446148456122199852758975791149556720918372001179790473143234972303194305206834051884246788140852775193466096026343226869876294379780286354788118492713694180397107813967482287936*y^24 - 3339426592762635164426365903731650062246471183009439689531386172507840529443659992295775656711253583852227804853446763564165561239165428735342264686352525096068254564785571801732512288870335845272663466094615683741186864539965932106975006236787/471540337097232307193322325113031645719513347095157052568436366145861537114030549963189743947787389180229593000294947618285808743075798576301708512971061697035213193798366524006585806717469073594945071588697029623178423545099276953491870571984*y^23 - 115026903027763221551317722911512537273450193288758375954777806807016152788621958072360459961414198789720335631596153592200236440720660966967025070544208742154638457276143506442879043296879515244072071962668346951308712488872399859425574584120049/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^22 + 6897384722103355714921997918305535305663363433063700265095641521873282263437232617290169891973273067021529816588957947357684495428749457896195649186646385166740591099893596042279882354080339972026878664017519241861201405506924774530587595413659/471540337097232307193322325113031645719513347095157052568436366145861537114030549963189743947787389180229593000294947618285808743075798576301708512971061697035213193798366524006585806717469073594945071588697029623178423545099276953491870571984*y^21 + 572833407792620593813423267910750225460267764685323374521774508519227551577684420507166449323138339093473820528684951873424127671480018315232457459658114410176363021180350621515775017649875198701426822316373502039849590821869823332887710272420639/943080674194464614386644650226063291439026694190314105136872732291723074228061099926379487895574778360459186000589895236571617486151597152603417025942123394070426387596733048013171613434938147189890143177394059246356847090198553906983741143968*y^20 + 9980861512749748191427810005121661998617077335660264582603663828690994058486617749085963010801092512955556449187769147716079320426816153605564681229301800250284145683685208196725736048582259474217124651511792920635832284614252891436892354164239105/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^19 + 4913103179958709702977631944498839351572903535015223094223380960732912886098361073429648745488021069411836165607920270771699871369338724130397457869931152305534073645299287805086968567153392271520557179306100089848305215081724807733015244327531961/943080674194464614386644650226063291439026694190314105136872732291723074228061099926379487895574778360459186000589895236571617486151597152603417025942123394070426387596733048013171613434938147189890143177394059246356847090198553906983741143968*y^18 + 4473793838235638153989035363812278574829964463758836736083522887554271392990005141584151683960097221119291201833445634628390873928678629377001524730091860608530616219814446201443055940130342468410588932374608389288795655840662397078968552232651261/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^17 - 60604150904439085651229539597162062770484911148027125899371073932251364457246671110036619085869581809516779627517368284193701850211561778249265334365837695373081441762273195483077170055124899828796748282174868045225628816507066018833828081508902847/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^16 - 31318427223239425190661150662476519953085032021114245714906947225872414742486512159437017257310952236871176093423352799500162422697949933867156698022809047465954005380787188249535930052128164385788472197769293838156538965876514990968606061112838421/943080674194464614386644650226063291439026694190314105136872732291723074228061099926379487895574778360459186000589895236571617486151597152603417025942123394070426387596733048013171613434938147189890143177394059246356847090198553906983741143968*y^15 - 41493802290915685808924594017019517540117757812418623202308659630998379680754704492846730676596868776355974607409052405871645566074880735406047394023988014644759610794355275071660900815681891220371777448693333905515016282490222337582298428275178301/1886161348388929228773289300452126582878053388380628210273745464583446148456122199852758975791149556720918372001179790473143234972303194305206834051884246788140852775193466096026343226869876294379780286354788118492713694180397107813967482287936*y^14 + 18439512982762027767594136141839730769212783861357072436024167353533226597692106391591175764857417297837923073399103330106063393988350453655850028511011275800801463916499917495256357095319940881089045733013362412963334818537659201369674486293840633/943080674194464614386644650226063291439026694190314105136872732291723074228061099926379487895574778360459186000589895236571617486151597152603417025942123394070426387596733048013171613434938147189890143177394059246356847090198553906983741143968*y^13 + 96058549808798605549390424746387180958578445873956861463768311518712011215740778012262282980860430132799355900382609484678738465779519215855891664939560384217354311435487389334982853541082681180783159441848082093662446900686052990655502087936147323/1886161348388929228773289300452126582878053388380628210273745464583446148456122199852758975791149556720918372001179790473143234972303194305206834051884246788140852775193466096026343226869876294379780286354788118492713694180397107813967482287936*y^12 + 8541119207921657780197490432409675663630810811494649044783696275425583411246129400824246115661819698345494819373494883739260805872957223320608262302630142960792257182055568983609080405661636426339716118555126614140002055508266889415564229292941711/221901335104579909267445800053191362691535692750662142385146525245111311583073199982677526563664653731872749647197622408605086467329787565318451064927558445663629738258054834826628614925867799338797680747622131587378081668282012683996174386816*y^11 + 22159192043134147554870057642286916983122686516580358017387652733477946044327661062368687236539701544675383084794438760707099001002178760422383083829194563005482175994259323591383967360053057368042665382178502065017444599140965086218769684019559/471540337097232307193322325113031645719513347095157052568436366145861537114030549963189743947787389180229593000294947618285808743075798576301708512971061697035213193798366524006585806717469073594945071588697029623178423545099276953491870571984*y^10 - 91336978244228719253720462502205714359395202871367104273072339033135028049894825997961705902032993220240415319283253520631323673920244434038954845745816270614266963817308017198461934697997864040131567051364732329021358222245371145158959624229081405/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^9 - 80141852224723625079937738029134971760662055438961750262916066010123094118376465267342230976936835277515354791085248029261204811447143364639298390467493302927972827279071676739971579344834637383068929638612753457640427139197938495046434491007662777/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^8 - 1690292252823801353040813723900184623167788777414551411013301907423574942133098734707495178080860653298378253288279059455050674093496007481404348101471329306124871962006027914043284957420624928914074985218819337852637537031100455439007587286540177/235770168548616153596661162556515822859756673547578526284218183072930768557015274981594871973893694590114796500147473809142904371537899288150854256485530848517606596899183262003292903358734536797472535794348514811589211772549638476745935285992*y^7 + 415946011160948225658972648833303971751514819570158455576079033153884925918591835767800373650139486267622895635351059119310070555657660877267447613151629177404469807301852486838677489741903573206848465874868932515599095181290081404646232057648459/235770168548616153596661162556515822859756673547578526284218183072930768557015274981594871973893694590114796500147473809142904371537899288150854256485530848517606596899183262003292903358734536797472535794348514811589211772549638476745935285992*y^6 + 6048524448445737432574864820391752321638058219458658978442490660032027949474241826701737536765093847048112200833292690161632298686024045889200870921187991555572493040573380686494319016007419212185584080839519813231072114031199764575106602357762839/1886161348388929228773289300452126582878053388380628210273745464583446148456122199852758975791149556720918372001179790473143234972303194305206834051884246788140852775193466096026343226869876294379780286354788118492713694180397107813967482287936*y^5 + 6578406284467514889379415942437813127596984267457984980760743841327319573099909639663961907207776696287004872037457185071687270088562699617456127741718252846647729248263844156799903755844019886555372770229805117861163097147086610409434912125626685/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^4 + 1033083262584974239340333204308848241888438104323595187801372163315365972732880842518029685634911253490579802687974674019319264914593242439401096289997326768172119396993114312023806332916889766980869554393582351476184262613064812946093439541406859/1886161348388929228773289300452126582878053388380628210273745464583446148456122199852758975791149556720918372001179790473143234972303194305206834051884246788140852775193466096026343226869876294379780286354788118492713694180397107813967482287936*y^3 + 394336070040987143067529513271026336359364203669566397385420733227845142650213065731702095224721766163235599047116254241160915520503482851073192432189721422681417843147121170367370659495071886436223454447777699993517527335714285105378668241483595/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y^2 + 41451347694699741986320725000443679541373030676679895794598805915805226628521906323866757654933824397607430784798072321324836722518454116529651741468426264651729092111794340559493528747879950502094106325708235078791317408437734338157372429512479/3772322696777858457546578600904253165756106776761256420547490929166892296912244399705517951582299113441836744002359580946286469944606388610413668103768493576281705550386932192052686453739752588759560572709576236985427388360794215627934964575872*y + 254331314531665355923963522722803002162448559857160407222368832758250403812078940618916215956336181292266641545231436384498241071709768630201181122315961861241005853276773676676629726202201800200964589281887770521192324259456283637399170637853/538903242396836922506654085843464737965158110965893774363927275595270328130320628529359707368899873348833820571765654420898067134943769801487666871966927653754529364340990313150383779105678941251365796101368033855061055480113459375419280653696