# Manifold: Census Knot K7_76

# Number of Tetrahedra: 7

# Number Field
x^30 - 8*x^29 - 26*x^28 + 240*x^27 - 65*x^26 + 253*x^25 + 2112*x^24 - 26427*x^23 + 35513*x^22 + 817*x^21 - 56808*x^20 + 268237*x^19 - 157384*x^18 - 28850*x^17 - 46167*x^16 - 1092367*x^15 + 491520*x^14 + 409377*x^13 - 53483*x^12 + 736595*x^11 - 344543*x^10 - 250078*x^9 + 109780*x^8 + 39636*x^7 - 57682*x^6 + 9221*x^5 + 4831*x^4 - 1033*x^3 - 101*x^2 + 283*x + 55 

# Approximate Field Generator
-0.276888641560682 + 1.38031954078708*I

# Shape Parameters
1252592749333239819166949071743827616926964575863137326578761111737876864969681292502345908201013583/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^29 - 9635636414731048087864256674167055381283923426168660401508222163489163311741944126242038234142078592/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^28 - 35506251140893018424789415189263168883797086293304118067484779023308529448639675519411104375334821327/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^27 + 289555558657662009224781663012476247943759736909018986493275747036427478783391066320512202486553426133/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^26 + 6695880006291169195447914303219587779850008321403045097178239740450423080566231863822085957937765662/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^25 + 323542265178310133799068758943600933898742898286853248667738271441870190273662014424190746860084421977/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^24 + 2752212426630043337385833960630608474301647824701317346513103915925236889461060993152891825426793028202/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^23 - 32249966614222191721900309738745627616345613462796529772695772786980443997253754412712323556935756655476/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^22 + 34629791917021448816085058141041287029380763584419242456779185199349611214943808528850906533328715398826/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^21 + 11131048103586737316349621391238515523951950199603621895967895129052327600342023140173793053747357188476/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^20 - 67882657994140951583799407708291622754616800510823380026333718543828855736518378572184744997651420495991/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^19 + 316200078580058279958601370714123772997279923531494335257029508624669215784028800863642854043628001963609/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^18 - 101103948171425493230089469900083080495702447040232019838653452115933790812456817278663229126477882622845/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^17 - 62747499942172565873075546147485299223854573981725811236261056291790947967198820835784229541513143071481/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^16 - 71068811007230131189242710115038280089241185698425864146706531410222657724657309362898293191117204148670/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^15 - 1394282851856620796004731650261884644340805999049726168124090125716993967708510320129063824193474874981742/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^14 + 186137979748911564370191100039463183238714328812919446938905178676124693115149219402527476027151318484669/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^13 + 541105478715134196123997958659304874726166811660771918677306430243807216859318452113016158803039952273117/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^12 + 67715465936125001527742790785351100507133207524355424887376192244319548324461705255309256025159606252355/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^11 + 958091933628435913536647583571885302031878612243755720596865442753948782550287240414306228911434182816179/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^10 - 131233745702340618076214800741712844470314632162170509615833719005439405891818208044802191575926384793346/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^9 - 330947622556105724710858094221454166814816492705991639100997226096342783943306629349637230422785733650480/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^8 + 59526617088613611768257788739088918789264007171284110551059849236295595222456172520749198883115802049840/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^7 + 58154562284565725867685985594852187197738671964681630067908481779928910659687729369705941116248868991901/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^6 - 55361219535704282736149108664381040620970509705723975588854352498214286803688905648181633260424392062401/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^5 - 5291006565388900602968918795085415726930875080780312414049415826332103196949850498204055255718277182724/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^4 + 4284593466202988349341582905840297749871169901240774107808783520970332515423447317400725162059461099367/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^3 - 999447825335203654291244959689555962237359170601369017401833793014930912896206998566435178905623078779/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y^2 - 87645634286136784210925465320916923008177469910378494912194559966527322770130718195925309508721829725/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727*y + 200193347201350650533864346954670759447432061064766515129306107332791069902790250225237914694360244759/426455419910370365494675431363319569064874122249426006218879446964892226403069334277811413048584221727

-2154765946711999790697209364445404091359280667670173256533396198460974355541294480372491859927069883358/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^29 + 17850478065901262082412870897239141824252517804950483856606224581593007409303165553736211428690768809558/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^28 + 51026568749377743170804964782424589887361415270562849195029024138058236165724677775063244939231758509514/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^27 - 532190902051590163003333888507020282165135498595200101440102662274113832146435673963536750835968012494498/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^26 + 288898424619384398091716355806463271939536560475398718548009961114185864412019650096012385156892112315787/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^25 - 610818272817719503853969081484171491384567832263467584514117322681453495458980016019450843685307243015684/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^24 - 4368940635667862445462947872976069891683566528476871007718763184182650295624954645061215162121780262067663/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^23 + 58206235790141808795806527877571968764984068308976901909563200377144969472906238157343820712812086213116523/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^22 - 92890378172921370978447871341149852655183304314729143826397627119068263548572607127148490033505163602013543/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^21 + 22770429162788214688616235049114433975648862627708604801280053959985756282037909358688031824231703921616891/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^20 + 117140575418272936399270732456000909006311137847781716957592921504708769766185485765977764922657292892532916/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^19 - 609753228786567332641876053150081560390427139924229011360550906680983608081944106909124422809899094474774755/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^18 + 508899777151080186865783333987240411081850757606166108476280383451804623156389250760403036487148175078788567/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^17 - 65404021255185606011740957158499854034930320741316311732832604256769487125171586851086301671855191413018480/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^16 + 120415133791656715673508574548214046319648763698415923194569754734308999045907249636803104363853642966873226/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^15 + 2314178229143351616075149914230565636704354575759309757451695080817617996713098395125472090095491705827937546/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^14 - 1724807188098341660695996384026387812584163267373716322490214218814720131307584701334101763018142029465580495/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^13 - 477877637715601094860027590382398304103327926900790048392438680687434246950749419007658886036178771433735975/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^12 + 223953613294075719498787127244569485198946615865543400185404866079933430604586389226889983460489086771046779/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^11 - 1616044586478096912127730008440880277442363168982596330547733323659554374507849487187133996647751889348533927/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^10 + 1229507767119789374643142816287315273158444281601070128042910373582461587350425643751190949301047507976720998/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^9 + 251362471562456451173570066411523854578561385815918030752814823302782843607088995624718729374098415607022690/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^8 - 291813605351608143964015463933369698791752028000777473852329994943853757406849940984526998609045376374094918/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^7 - 25295800931168499744961861277363753500112788243955659115950667177689774927041488113291842519138685679382634/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^6 + 119340150443108951248063381133030458243227269595148866190024705892191339907165491803784158532868686576575995/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^5 - 49949301128464491858385975404116465763752040249386429999715738053004684843559826414587047950762742768125900/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^4 + 3872392086137939798219317209348037436839903366461565936326463020825464497303737653812708319159008800673951/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^3 + 94481631012660322632070352428009003710393059765153136656249943533513949364336645245975775673193045948529/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^2 + 8323665773338301473282024631033419735231606348667277028827836833541262973079004985842482515076523411833/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y - 37610351696403158228938655348700435916798011884742446813973116663304447005241035386430398263497255350813/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079

35185831769345699173153316381854160313060536667432458900903144592590053029062462129970128143944920966/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^29 - 256806962440117169295416211061917929285829815975766479977812262375800230597905155899403860659030437237/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^28 - 1086690062779531670069512630474001161788304967355223215076974192862088346621177307646072012075347073505/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^27 + 7618490569726117263954773399804245165384031657939030876296251476926589833834834699424690976137789239248/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^26 + 2815529433346344604471550475689545662696076742311809268713335725898945427803105236445822130851816564410/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^25 + 12866167372056952834924705327820183108590450719572010585130700408234347408881533925581440537489636998318/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^24 + 83558229485232503991287372645804465816968233669726076494768050813901110564404757025148483494482088319834/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^23 - 871211146748622615709915280172796201462648194803814868584988701841739132405477119864056972915287317069989/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^22 + 656792763770662014252257552696498893245037456103469250913252300440426709799886246277478467855812260399069/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^21 + 273723816435312461967045295964493954531870836712484123030459202236286093278838788433735920221198607010123/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^20 - 1590092563401356407998344870009296046714724395575388266831616060812164369048721426724839369049666098912073/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^19 + 8620607172841934502174761748179436794971745223472729707735929603520490556596843846077981401707862638312475/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^18 - 218486668320813858713184222687932271830697189459614459864240221673475158665896310245355647971280520298630/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^17 + 876734581906163636502650375562513017227282032440110442835549674473964875634125924708948705798868752984442/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^16 - 1242940173518558285596356679720416141299822358617370784016843760597953127496011130908584275194978249283080/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^15 - 42013931587285869337263424832512272346817404313523035913608973734505707372413090590163529360120007544753173/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^14 - 11621920310175237149024104893732600438298866658063306283508065770659039458368143546257653608243872812548536/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^13 - 2457848694269723934771542951631631944901228860426000668253879584857190798363519071348419668725175217839455/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^12 - 1668400210364048156777654768284251106651451134730881929625931594755348083939983686578145820351038589446854/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^11 + 38172807865849665977666854802729602699608928016578882899027116255656981607931168378604656044258776794422295/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^10 + 12214845931911025384501789071558063580746932982866432604619812151843540514589545646818777394379567237650508/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^9 + 1830839713821069165833028845107485930633371216354082801911695221137533888151164829146309215839875987583763/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^8 + 4173288374645839260913117629443944505840704167597995459803076246849314110160182286126865411802782930842949/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^7 - 4715683892724364583081352462229037039395820251309670281973176904631933294085837115811762898564836727518176/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^6 - 2726237723555730417613572412009675102794260237790220056709687089952937552793199985793040285923551596724127/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^5 + 1471636866831198476211352809851170399629552538068116703627407761359240426397782404119563365328375213344310/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^4 + 45733813864900341376361409504474390428496500526091727375249310569747059221177057659409301100399440568427/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^3 - 297699565812118866248224041743453596717418415373187398964728391270647844905252558834162212431819906710977/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^2 + 56893331760896089335526281472531091233254229586600702050724656353942637144003679896920892936486064077093/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y + 3038647359000433576714942548553617790732995225838853415852847022992674086958879046642125113665504782983/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079

4574552373425090957998230686942553340853766527418171566186457650456610895248803316574782164223277/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^29 - 37480721446897266103871672915362893544008963917538207762180322412795153983160157873510525603619714/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^28 - 111677764728049371265188600406648407189853173018198567783756653700093497364450528398112148441516930/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^27 + 1119334509977738636920224638047696167490528761015674388177885423754594367258396007986091634172544807/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^26 - 513929301325391607149795536135400493209653754660445802410001179811730305525995547651518054719014317/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^25 + 1261042919723170016523606519148664089291116468501973597504657294904033278933923223482065784379182179/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^24 + 9411017061276106447443479548044432421247280235348359601074081957752754565782049348329760031024549260/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^23 - 122706706270309660023169355588873786608922367330131749138048248754275616850720549388507978443836213819/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^22 + 186201164067862882006947181942662064949672940261945177486832210441180212743482261069806915958430088545/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^21 - 32712956597145144168756445031042896566162124273321355518385963902845093811328051970840434749782334176/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^20 - 252373095666333843022879327741771644810694498990957692072836211829202220681286131884119389346418356927/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^19 + 1275133327810979271031355148141248074083460228610469344336263238579488636222469593601391585876142047615/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^18 - 967374451640039610124743631363794383108466897486748963178167163192608838624114164751387581092148258895/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^17 + 60319398837758382461810460612551786492053024140052078240903065323971031314011923057376865377383567385/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^16 - 231548708085119719159868800428846961883208644018941153027498338848774630775145259021874869096088341988/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^15 - 4950141162828878200367393672488771444901957573349173661906148058912903073625536563250450504518439556324/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^14 + 3204592775853469705942658887519756346351509241462318093948176954616032126597822768113227077180380271850/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^13 + 1238378648062214723891268529127876914186216689318986524547859250322337155517092799312152538919184948435/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^12 - 449279405734635925761726458622118227267830285891686090798780334637455906903451306573866041050584984611/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^11 + 3457539825132101182747652420274017156527180455961722817128878804585507948555764756055337370521352331997/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^10 - 2250511788314121753009951964649583942191861395081085406867202779717855352985635316447673625741889304770/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^9 - 699359595003864306286241662733729906112768427688276329810688067504034831024916731380585872726411886490/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^8 + 611959919611296147510357971266388518684646006053843692656115374649342343725977275591634069098998562509/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^7 + 62617432741967801116697802481324798937246825614888637569216546514720864277486238805770166782599151259/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^6 - 271717992681517471286871253636792461012819408933177374694481523229785302610278090016470941728022209610/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^5 + 94326005787428071634934878154139797432868085447005527409024285732541653595853662656325388462373699151/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^4 + 2847224932126193857731513320568154680050853183953343639741739266154272183641378948337467332671916952/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^3 - 4018573285861155290481477034388545851453474965329632346222359320066884414998333630160033033060215686/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^2 + 293964696102556937051787273959796437860534606081303339897449927017804414812231799769963033937201030/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y + 130524364241485621982292051821608329854924682156184291494350384579977524163991311379875434839505647/7465825526695442402875920088291864096652266631351447037322166050399891920713386220090884491668287

-2154765946711999790697209364445404091359280667670173256533396198460974355541294480372491859927069883358/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^29 + 17850478065901262082412870897239141824252517804950483856606224581593007409303165553736211428690768809558/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^28 + 51026568749377743170804964782424589887361415270562849195029024138058236165724677775063244939231758509514/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^27 - 532190902051590163003333888507020282165135498595200101440102662274113832146435673963536750835968012494498/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^26 + 288898424619384398091716355806463271939536560475398718548009961114185864412019650096012385156892112315787/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^25 - 610818272817719503853969081484171491384567832263467584514117322681453495458980016019450843685307243015684/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^24 - 4368940635667862445462947872976069891683566528476871007718763184182650295624954645061215162121780262067663/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^23 + 58206235790141808795806527877571968764984068308976901909563200377144969472906238157343820712812086213116523/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^22 - 92890378172921370978447871341149852655183304314729143826397627119068263548572607127148490033505163602013543/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^21 + 22770429162788214688616235049114433975648862627708604801280053959985756282037909358688031824231703921616891/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^20 + 117140575418272936399270732456000909006311137847781716957592921504708769766185485765977764922657292892532916/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^19 - 609753228786567332641876053150081560390427139924229011360550906680983608081944106909124422809899094474774755/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^18 + 508899777151080186865783333987240411081850757606166108476280383451804623156389250760403036487148175078788567/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^17 - 65404021255185606011740957158499854034930320741316311732832604256769487125171586851086301671855191413018480/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^16 + 120415133791656715673508574548214046319648763698415923194569754734308999045907249636803104363853642966873226/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^15 + 2314178229143351616075149914230565636704354575759309757451695080817617996713098395125472090095491705827937546/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^14 - 1724807188098341660695996384026387812584163267373716322490214218814720131307584701334101763018142029465580495/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^13 - 477877637715601094860027590382398304103327926900790048392438680687434246950749419007658886036178771433735975/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^12 + 223953613294075719498787127244569485198946615865543400185404866079933430604586389226889983460489086771046779/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^11 - 1616044586478096912127730008440880277442363168982596330547733323659554374507849487187133996647751889348533927/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^10 + 1229507767119789374643142816287315273158444281601070128042910373582461587350425643751190949301047507976720998/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^9 + 251362471562456451173570066411523854578561385815918030752814823302782843607088995624718729374098415607022690/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^8 - 291813605351608143964015463933369698791752028000777473852329994943853757406849940984526998609045376374094918/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^7 - 25295800931168499744961861277363753500112788243955659115950667177689774927041488113291842519138685679382634/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^6 + 119340150443108951248063381133030458243227269595148866190024705892191339907165491803784158532868686576575995/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^5 - 49949301128464491858385975404116465763752040249386429999715738053004684843559826414587047950762742768125900/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^4 + 3872392086137939798219317209348037436839903366461565936326463020825464497303737653812708319159008800673951/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^3 + 94481631012660322632070352428009003710393059765153136656249943533513949364336645245975775673193045948529/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y^2 + 8323665773338301473282024631033419735231606348667277028827836833541262973079004985842482515076523411833/86773699875943940919395006615237530228336708123405391056576586382429208617472576084851471088263774455869*y - 45498869866943516494338201404631120483010439895961118728207351788979829606829451394144168362430325755892/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079

-265384550218404242854042368760267249777481498150713604213188477129956301327559566296999269630254/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^29 + 2217340008086079163389213646933545110585930755248698210657473306938943664807949623744916807178972/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^28 + 6145573649764355259248693840680928230094823420314032831437467789585396851450192792248923185255590/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^27 - 66125598823324258222173970676714417268741257158818426309489495914494496956656341559978247834372985/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^26 + 39764774242705605461865174682177639393619896258387169299007758783096148358452142859902768879427871/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^25 - 73761218931651557709486779716577640438584337344464409202341396419754098407496172121703058451791285/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^24 - 533125839013473158969085172203509488011722729898330579261380358510534978697998748235496502595183379/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^23 + 7212114977850508773281069872866696041686483919622406978089564432156344795075872297214645082516415643/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^22 - 11912261852875701300574231563376263825556535484785918858461889819738182490829506509553839383641796169/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^21 + 3171691721639071725932136001936735398705309905183256943851444836168473750073224793344607945774446613/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^20 + 14752578818816122006817336585920988822275668888902534491484765744678830970202441258570841121231343027/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^19 - 76094648492821233849753034938112075369704781680480582308071288072851151399581253752350849634800020805/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^18 + 67146283183782223597531082433353689437350593932607586272997818993967154005283163613397965334671924155/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^17 - 8047288740862090293081164430272346548887962352729346499931750539815362162312963241466356343068680797/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^16 + 13444410530947660330753269330146847626095677565897928637087673712727967793890612986928429157699154918/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^15 + 284000549017976572127646037995393773195817280631187774232626329430090112428830505089356949965164383349/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^14 - 233808165464875825952133894693196019923512816954883382108976020855636635804820167852497125342339064650/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^13 - 62968055379848963384047683561129058662349328958696981744347822145830488825882938948591867929231827289/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^12 + 35795913967449552511463282764308062432076021617948586551725719739441184020133343309327505038924021052/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^11 - 197314848975388632541437016612377577991491804277639897051744249574816321058578589949006182280706238843/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^10 + 166115682602450671506309771208166548504267200527271704220115579751355487185842397362797812560063532925/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^9 + 34853179194487137891268222297137340141619188034872346135472225303172568163045415466650981101434000300/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^8 - 39870683399069214843256233436097491749523229738752711154420118640679263746872721302215404380904831876/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^7 - 1786252581736959611725789690429251999740194960113263556054233324410702379329618777592396890056097762/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^6 + 16568471810478662490993199123644674923555255099229984389765606414312450112062564166634028336742142398/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^5 - 7278973149941324291689969775652518905358066242885907123011160916951543700932795061784069598213777520/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^4 - 5963798138745773465788600513394010985439770820526765584126727035264978892467231853967508912822847/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^3 - 36419843566673896760298316641201032123653721689171587247533162527467052340252574412334182070321096/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^2 - 82863196221196703406127680256548646416800553360146094255858302786233056181565344936284783544018663/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y - 3262716377608024997986380972753742896649018478209348431782018772247916251510479734796054311876018/7465825526695442402875920088291864096652266631351447037322166050399891920713386220090884491668287

86226173890058872457937011679413740791550711491405678350170693225537208903387856946628112245479/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^29 - 441706000147201033087072122189727764099922890161615813730367919643425882066301578460068367123927/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^28 - 4022331914678212099661370918913453312363480927949086819353114657366642713223418962675196308947489/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^27 + 2533051014028349609878380337930373224180234871642279477610208908699699940523448693447663564878467/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^26 + 9644602017605018010905806069343862568622320884376155009903754884782865030376114170814310054303997/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^25 + 52896138300755131662326463800955748436154811514231572942734913156079146912369170891446341157131477/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^24 + 243668813627060143766459551379233204093633904020604972121126245151735533723100079353998326201026218/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^23 - 1695633732997477971144584291097157526449197868296371581172020588108827285274539578320217268893024003/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^22 - 3044943001017023800345774918214351575930052270591005070877020584777023034379541371719705272104354393/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^21 + 3615158846088717328045406392005040859983811699977852838150078405206237493618361623939317673410811248/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^20 + 1179101008156924045464506135370493537667239733104090561874910507556444093347517042490886056202475188/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^19 + 9964291850226118439318225916693140113129458353692513029146392954215171789553631156325052676830958848/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^18 + 42421836588443724954794405247048959406006848189776617518545475288527445891720960050566173000742067834/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^17 + 2138631328889193919931868140186697707235037522678417911809307565451216393777046964378801743749316419/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^16 - 30449985295799477047978745597680336688191381337944872652951639354763144933325405698596155156297681318/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^15 - 108642980281608592844342812616913805367074462261221110336108621090006216079067657859286499113832261438/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^14 - 4367554102218764544862317754948098022481105553657556087097348756793574465165269761646253898269059762/7465825526695442402875920088291864096652266631351447037322166050399891920713386220090884491668287*y^13 - 6368413326368311461676061954601783741166824664269348623044256460248789736976229261380374140223640262/37329127633477212014379600441459320483261333156757235186610830251999459603566931100454422458341435*y^12 + 131514182590265189840933258172805586165197856165939238283201989642782628882462344821404967473417274638/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^11 + 21118484023365251594852912138201454379744770225738987186699290035774982029395130543725541246835378023/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^10 + 14039828335089594542464035256106632124189773733286075613354463976056907470774168985181480580876646033/37329127633477212014379600441459320483261333156757235186610830251999459603566931100454422458341435*y^9 + 53701858691647699473721709989066313641843082876524480219413261784177300276627845341308179008962326568/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^8 - 14704607868629994042939867773075495618387442222353198337418434128081925519661091686999003494559887522/82124080793649866431635120971210505063174932944865917410543826554398811127847248420999729408351157*y^7 - 732541922361832210234192948024336871611596047680815425933969698903544446812731391060341484527296526/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^6 + 21223170486632877951833522509087760894415237817575418047390702713539702689258079096348365538241356007/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^5 - 600263833673100652870086161483868091133631313128020089131985440176704664744089519826736891556226891/37329127633477212014379600441459320483261333156757235186610830251999459603566931100454422458341435*y^4 - 648311102229567614498921715446990032141439699159447877272288279861013189094486813811121135566985706/37329127633477212014379600441459320483261333156757235186610830251999459603566931100454422458341435*y^3 + 2972462206669096894890009489232737281062360210330196851763815772459317201350337459218823459604459743/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y^2 - 5549706009763256729567719889785713712977255188791558530594805288507440282419484524022404706731934/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785*y + 333721206052373048253350147053903872168393025199253931819915400909620833162956011149844995076982127/410620403968249332158175604856052525315874664724329587052719132771994055639236242104998647041755785


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

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

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

# f Combinatorial flattening
{3, -6, 1, -6, -3, 5, 4}

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

# 1 Loop Invariant
2112731205271551021000630216126007546208543834956322136547150736037314497674814012333353026654087064079/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^29 - 34398255139518172120809992377155772250688258967446781818832505640375071468991640348070313137054902983593/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^28 - 52369155712559892848991523910508858430751071365283259590334896773105378987488991993665452371106530971189/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^27 + 1026683821268864538878435397950620141247868896417986050387970331257549621074624719862947582104352868059401/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^26 - 427266114542491426542451410040580869285603388931056586503200321702032386529331041200191370772097820042763/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^25 + 597040676715116222658396816241154515421352809327415681444539243402454471791860406138943498414158344085337/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^24 + 8760973673609366154913586229376638859167136473795508265719193264897161082367284273529499052852835286356103/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^23 - 56410507845647064914500438077949574475383690811336388906953154305050631117209433579591986732159845035837015/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^22 + 83281031419307237253578813091188629130793910653919234213622813262275378506309382843197881715473416049299926/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^21 - 27240456857559930583247736013496002490670376419015965579375337168629203754958545132682951152932636745577517/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^20 - 228754144703226332634219974872714054311523852594213520612875482337334056895069186654815210211241041474842113/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^19 + 1168071188050829019073537709189844293673806849280286603739695803740771265589475917896574487450998577535538443/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^18 - 844109268270265894468858425079864569388841595437956244336260584767947482558970464992033469977607227842250621/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^17 + 33767394117368039340164741663411027941969185612594853795878779217246622487772414825460935930453825362823537/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^16 - 112039810112847231150035968377592044634549618084271798665692614007623391892976935104905426136552614068540152/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^15 - 4594528377728802282217668663772257243646599144792378857269623997221264798464161636239973252567870094334027683/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^14 + 1352731854644463376296584148601985100318183113413806391264270246618431272354766358418367978568164005123943415/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^13 + 517078914251868645618856184414026125535587102129839514211144444471632703238302534005660864896134497311235402/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^12 - 174653544802390046278357176809517878781574454808815355365465351944269891910420052946278816143098479664974433/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^11 + 1631358633253303366758771175565011079324353906893042141109915331617910711407590966347243488973758382293740138/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^10 - 948058547079376435387209401262527531747400758882525953812425061853633306539895810188077522404454108074543198/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^9 - 288994823126633489396990958874677765835615708270402808250639723798236100551212533616690434247437020376823602/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^8 + 525726226941420041988297300304769901182610234726782739388006809434736915571761456036880737825217430125426667/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^7 + 33979715959708516343669085457453086736562268093029487354305629213973785264746069627421037223819426664296483/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^6 - 117711297214382564663050605347048794513549721301498144707799200061099440457551062281431125734191342876029707/7888518170540358265399546055930684566212428011218671914234235125675382601588416007713770098933070405079*y^5 + 91569647973399389801226552074540905715892754843115517343442952278510511622474639916348428639843285843341175/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^4 - 521395227210088817390006157553613012992524387451316057238591309782982872622923512343928611568461418031219/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^3 - 3949336711745937917952071397130672854664632717778649052792475158470659872541240160872349467711293620320627/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y^2 + 699014845954831626919130435945354315234001475935982323020409424330365344843505467954322926988025234035849/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158*y + 799740037050269009915755144065951812029698353281907286302787160841358900429379730301942553011811593808697/15777036341080716530799092111861369132424856022437343828468470251350765203176832015427540197866140810158

# 2 Loop Invariant
-3920515688169541796261830472320303740105023172834810681483684636488756104229452827636210636532061390566120691535220189412127206477580568459754185385478824215519272906735017501158521402673098675021917129900529/2060713504121843471777778609127500246489982914587689350374736387742600395260909727037610443216629589258918902375101033692945860517681054716392984283526506985791023795269352078835992355507132364804306050496208596*y^29 + 48547619619566245690974688495237446520053959324660973895728755855652076431701330094468702840546444651989931642649927337467854643072203699667607312955207212539627701064979144048677059816786506055917981887093855/3091070256182765207666667913691250369734974371881534025562104581613900592891364590556415664824944383888378353562651550539418790776521582074589476425289760478686535692904028118253988533260698547206459075744312894*y^28 + 1125257053847875263310661977337750307567976123225412227540579857569630243273260668014637946937358160558790922844393160020764418745210476573685436321009247378914029001085366864176988273886953432452932503677962933/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^27 - 11586051660185316493082889828512759992465510670515975030114362615459800203990631679343594588993297505819687804983908383745394213727872543437311266324014601354361102363521886712959165513260421302048681598418048779/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^26 + 1492210586809124514603788468232187217603426812735949722805179873216293171822368645007212846198593359388456674382170221296115103418678116675252043106071014317390924060413196706789693430838778184496765317241330975/6182140512365530415333335827382500739469948743763068051124209163227801185782729181112831329649888767776756707125303101078837581553043164149178952850579520957373071385808056236507977066521397094412918151488625788*y^25 - 4397854923455612481444101595605257667135765789059258235041538204006274442309438249658594973903568323389880671510360401540128091741142126846550508529067788682576737289415124354873939558479354044394828526754601191/8242854016487373887111114436510000985959931658350757401498945550970401581043638908150441772866518357035675609500404134771783442070724218865571937134106027943164095181077408315343969422028529459217224201984834384*y^24 - 95600741411375731010309492471358558749851049802930086844053577461290812409587168381379550073587230864171380815092139759265285045978418819006799983237911213585292939986396625655934193681126775573088194776498052807/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^23 + 1268033869354670177938608835955391174261535152400149542249233905315506733358347742462561326932781855414763979300840362518386407168431615871500149191489725695422296703646904738197346404751679570924436958188218536151/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^22 - 1991437657077749565892181152853178588452748139212740053840661729018438998923317563022527171945189682193258910126650370052449049026684306209713408156315184548826536842550745776861078650453607006684804033233190504579/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^21 + 442381772849406817078515885680056960457287606413975769384988331763131084747068605834180897040799656382507519689784431788982941669680444030961210031272842596286862542703983761075705304237108591827268193112493146491/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^20 + 2550319414998711525168089801786197953612997192097111093610077007378247495081627294404523839021747277324370544168093775468685492877959463099642442533600923422967311006332861883767104085705933331538091231037390251437/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^19 - 13215052086176633154267074769073694394124088248381726379114752014243159519845604607458032679846580707343589451310261611973158210007891417611783643141307942455422235166976616923833294325387568466063602334322206372911/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^18 + 10732899671992755480440158022723636531792562060962662127766661246479149856381525987183645241784484731940006921081404379913876603613850512623372678578756331754572765076410908955795826810528147381272882544510910923167/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^17 - 1169286115796607183564034175293245007619670092901294010148716759168881479952958483134482738145860856330624370120551991565143284328839352413326537943062732499158435251018271013553713527330116356091584071638631395775/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^16 + 929348781760174234185787768615375585977669132046456339841761500452577508088310199437181481839625246134190003559548857675749093319844827033376347740512215529084888667587775230485272511737218444322687688260721023731/8242854016487373887111114436510000985959931658350757401498945550970401581043638908150441772866518357035675609500404134771783442070724218865571937134106027943164095181077408315343969422028529459217224201984834384*y^15 + 6312625849782095829194228049130681271783757008801920334547960719500231348663274604354091075020333344292243307969276932254263608172808194468067181922718787311678575492636400315207458348933897048322137401382997856995/3091070256182765207666667913691250369734974371881534025562104581613900592891364590556415664824944383888378353562651550539418790776521582074589476425289760478686535692904028118253988533260698547206459075744312894*y^14 - 12072012320666799489464760714311099041030483721032550039455368412957801079636019013582731119956431968918085342853140039245854989025302051084937462503402272024627426856942389525509567229531796784378923254159911052039/8242854016487373887111114436510000985959931658350757401498945550970401581043638908150441772866518357035675609500404134771783442070724218865571937134106027943164095181077408315343969422028529459217224201984834384*y^13 - 11468904560844652982736314228773002751625332740906864847229521549649529999134211143237426845493290314315273826898860829514514085115386760218791511103030857282459946075014305902007203880123369253303339668237302592513/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^12 + 1258673304257322574092161496387610277526423649918684841701024833570349197294746411740088687601481830824953565425011703736908280257845975169279663605866190715561943903098360158103730692536765129498165940691829584911/8242854016487373887111114436510000985959931658350757401498945550970401581043638908150441772866518357035675609500404134771783442070724218865571937134106027943164095181077408315343969422028529459217224201984834384*y^11 - 11620441959045496942989161233517442106467871410967271795673188351555524382176535736427331029177582465432039581892968460133456228895587940205094360765952290184496256483570173513453676433204434093049512188709117289275/8242854016487373887111114436510000985959931658350757401498945550970401581043638908150441772866518357035675609500404134771783442070724218865571937134106027943164095181077408315343969422028529459217224201984834384*y^10 + 6530559998172302023098517273030532211563511630949375032044944160384129507995987981119768431771510685236597750808568599069145377051193170022045814503729477494588797053518027940746414900479372331188472099919910940499/6182140512365530415333335827382500739469948743763068051124209163227801185782729181112831329649888767776756707125303101078837581553043164149178952850579520957373071385808056236507977066521397094412918151488625788*y^9 + 517792775389826431668945759739653737184078927487248591381978677685679279390088868762524133274927052744226434777147967714868611619093990629451377177403176207122443419990033540390615657149426635815617501247793934095/2060713504121843471777778609127500246489982914587689350374736387742600395260909727037610443216629589258918902375101033692945860517681054716392984283526506985791023795269352078835992355507132364804306050496208596*y^8 - 1415666093414710572712119875765493019372329888202949514364392011801195395986702975316527637795685285050894778865242189845692433972127854590600891799512517404237793546824758062404678874276052067158032770607493600903/6182140512365530415333335827382500739469948743763068051124209163227801185782729181112831329649888767776756707125303101078837581553043164149178952850579520957373071385808056236507977066521397094412918151488625788*y^7 - 956777440113191882810010956402379489696098160312641865873768168797649238916360989456048541508951325155504726952592379732138510393733645595011817947307033614401002749809077281548127634737101776406789632853523979413/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^6 + 2401095702893759332677969873062611310070036501088703536134835364554115487439494040715975004821492762577461447002575619747713973028492054310101571306058027394479843952381014460177892706099164439131627299341675435613/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^5 - 974730042006218788538067088607880990004760856575847416082517576430951043555052229876578059733903030832856494325512473963387757215494425619104418330579021403814631143344055622372790123846444962768389637205633898683/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^4 + 90223950538825303975823883725241868717652177389098508381971414471852405060754474238401254902954429729855873955668683338373781286446694299570330376267485907476487434624212769838872666340362704569352366834149195149/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^3 - 19835740119975647575329315694056114042717129551980928408900687357999557734718119901710738597776335678315462677049595548965774882633967165890923847116627929018341050509957517745733572781995317037843754533574223591/24728562049462121661333343309530002957879794975052272204496836652911204743130916724451325318599555071107026828501212404315350326212172656596715811402318083829492285543232224946031908266085588377651672605954503152*y^2 + 434821895812015397136095573133587589231705438507514017119882299057076481623366297489299610243667980873427671289144742055960756168153214795085603552459637655706985603795102096784555649677315671184640934999003771/4121427008243686943555557218255000492979965829175378700749472775485200790521819454075220886433259178517837804750202067385891721035362109432785968567053013971582047590538704157671984711014264729608612100992417192*y + 987077716257443155304396132098871944118787174736796974334809806081996553756983216322693098789823208105868745430730140611294695959194578554919144699108345200373465985099816477458879284748752308707172442137279651/281006386925705927969697083062840942703179488352866729596554961964900053899214962777855969529540398535307123051150140958128980979683780188599043311389978225335139608445820738023089866660063504291496279613119354

# 3 Loop Invariant
1902576428515814065325107009206776990109558076616507310542105080699899636718475051874390763668032051714672295810828921852982751159665898989386107902249765725304699201653921936028739279792618591744488302731968037657012228850124763855429184990071202959172212070433/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^29 - 31040815832626351153377291585412309912875480372321347175617849388448714989660100747048159297322501535421870916354363397188781398860056744586468880295856449102443089502423266176184776989497247213762961147134414933415087051223198091083236298427807524570679987930359/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^28 - 46974536578906465956889925190545205865955012568520661755369094940009874052139970830869274243165102146560599253636864453962050715148582458043774298268802963378544692682085418150628394914421013241862638319925102914125182929930174504076016785492747084559788992465693/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^27 + 927326278740716023110574170154250831674445206527797616750310365428084626240679465387224912925648771527262201112048234270305922196067387229982258338909769301811736157570732595471816464877260081163458150350845778220587898385902417618124426645744409877976421654865287/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^26 - 396156208641506152568018661291517666479070674926491456518834912195654047472466134505736273954254464583286292185494497962508061690575323461341764375148911850983904291846258833482550585348295137724820272719288245821620564110867993606615125640667074280642144064648587/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^25 + 130821019470019038161354517928218518782856033443017530045574529128352400198434092528145388462524733781928966236801510249441097837467889967008889204489094565153302644204917961000949542204873115162958941597988585123565658415752111727084767314379559220491270621146227/317564807495827735482079897934872054735594172048363150704448982525423700130976588781562757610111498556734447223129841198990362098323853574644971809466772014548312167936398480983417493652907030496409462216456113324547215964367614918260319377341306922292894540162888*y^24 + 3936686588593779611814724906868932531470406868088727137807584333089231724666215855146463078811070881960161859874614695505107604496021824693078195243946384779449108756874603643008556478443909782379823583615521327726322554365697630122252172808515713908189452851569207/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^23 - 50887048301957395602393578631302036181112530070663849609343744890259782733027357948056643359738543066627133181466393939117048747287644641180329615672714745766982127512427648856117536459513126062577764822746576929046898947851444539020234552888439624120312257719898369/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^22 + 75688584843366470649509770856474148162541742141165492631390728928182176175115404253158807212901728853992487593704698400320174234501459486568270188954223499423051119921396550150169158623869049054003436117365515479082703093675647975600587567966919932421297310755559167/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^21 - 11570473648291004764560243945439172110525401125373922246449008094771363983020675452032117642389965330979902738229360748962206265222214922940491664194160209668372784326446328477515860227185266519736711733771424084785494581869878206545426157357792990124838611725568257/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^20 - 210077525060418371324798692485209590475769839497097117583924111818037929868536621304375463104241289193800892387799853061931452606340991682449878620587367612433681035128779377705063823554514892960242237596927615695843966004384319910942684637181466429276500110720164289/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^19 + 263667209706503579433310955537322395550072112076340931196125922891111855042623951912772930289725149052816345175009889269870227572727396417328689548546544763845828475323144881410009396906011727897394053180104348632275422299947451988995641715272766049606560710899631911/635129614991655470964159795869744109471188344096726301408897965050847400261953177563125515220222997113468894446259682397980724196647707149289943618933544029096624335872796961966834987305814060992818924432912226649094431928735229836520638754682613844585789080325776*y^18 - 192495756769844135488006192066100629804503157939900325875931985605014654329060551051413483150747299623032126158299943100659103070895826350782670915817257384301393867124835568199088355600665901497937593734715654329328275123769597791626692664103962406472869689967044927/635129614991655470964159795869744109471188344096726301408897965050847400261953177563125515220222997113468894446259682397980724196647707149289943618933544029096624335872796961966834987305814060992818924432912226649094431928735229836520638754682613844585789080325776*y^17 + 34931026932228848560793797132758825434789545234628138510397620068819800720928789171256232512704853944462692646226943449815921169604432511117265552074270644813862179742295490509987336096541098182675936646408735938154841272312801321851685639290725142325893162123208635/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^16 - 187378992011796634454172813147637707748201889635206121655837000201335873233544303869571727653482152588094351674438753408785545590563141176883567444111610053791343420030647862854870314771304312521743472124356668736453043442846310096164402033775024400472348593878933313/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^15 - 2065576115311159869653152640741627417406337549056068074479443761950262230060179658760381419009772374386348565571344394143574201955176338033555154601686824768029338682428168722718694851522457250533519097046007752663791148879047220283050982885059760359732889180641765373/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^14 + 2515605610107119127557676028747733024334721904901071616161652243519134538551630889280776279139806639445562705651567551346939438897341161794261441747237162427368683065891502272473099711412792005449412261822415234668325629415529232444586967168198311318054825635437323579/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^13 + 1056508917557894598477959171038491365502153299758488546792488472726304357381554038352214568018405002612383583750211029665092788459174413614519008473627556299965190319599907264297729883886104393282042070401807744629384073354377778855646279552994888319052976696011190947/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^12 - 363592715295249577955130978913250518531204991763561088498495828404579102202619687494285429262260227391345097354071843137211701844358548367850213042861603251581037768308211731023685658201874165119197348320448697116650189955157069038752698222682742535195994332146540121/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^11 + 724012360167243823375042556553245207131822523622254110616134172791614416283990543318163678677755719985578543290995814381766577165094141555336683141039720321322122412305345808581019274914119043351588160535308019797881910495115665266587890267537584970315155727248068463/635129614991655470964159795869744109471188344096726301408897965050847400261953177563125515220222997113468894446259682397980724196647707149289943618933544029096624335872796961966834987305814060992818924432912226649094431928735229836520638754682613844585789080325776*y^10 - 220074937955898644337615247897343598669535493571079134353480835578251452202779171819618900040960624934994570091978034599218123254071749293396867626034758148125116814276578637883466607199205514353011661566894348621942047124038236150999191148671179866859451451727518263/317564807495827735482079897934872054735594172048363150704448982525423700130976588781562757610111498556734447223129841198990362098323853574644971809466772014548312167936398480983417493652907030496409462216456113324547215964367614918260319377341306922292894540162888*y^9 - 300195899787335398353820923685006436287310709517494747054386712445047398773064253628239603294035025500990796305918757596003449271348633951564807826163325611146610985776855796820785897117561150590823203693954328148108200808084506200063349670296167728319237932731683483/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^8 + 254458837822102137916680566213032278408879601078762059731796670946306652557840668106503763380990408362959363400498545272039034633029340467333269483023527426194161021019788644840621138972910423997643489658324915781863706164796167862886120636780961138558206460198862671/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^7 + 24459361081652974986303335464925691510477154042164329987446798382416379839032955256174162687274469978874643377499578503555931070506057323729416630746198907544728849325207091097055129286437806633189622982997177274322455397842252521751912307288632428636521886280617193/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^6 - 223944081045338486667995174060499355142180466288620570310251867448672510259631729710206437417468867553887674327202537353836536020862738011423660047620574557806545455014599425665512026373920680561312271124960373263504365492468222154472024659605857544099542499070888787/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y^5 + 9240722653984389639778813659677699947843455118334568378330332753334385074366986412511845062082870576075403311710452350408154296458149110616809224893737771992882309261819583988350012321241461965276422632321813989239662382960281153320859651131193010752642860165796279/317564807495827735482079897934872054735594172048363150704448982525423700130976588781562757610111498556734447223129841198990362098323853574644971809466772014548312167936398480983417493652907030496409462216456113324547215964367614918260319377341306922292894540162888*y^4 + 1119752094706254186792553136636461312835088717484736110859742114583047505923353744429314817546560692798134011877913598142397868610959941708736458467519178393533347946282143380703376935050377079517175818650499825892303683217430094473163462614924321877849469558560749/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^3 - 2230220588642307588506022515968217656293180526678987552708814200930594753317495313457558588546179697315577734263953409368996345053606813778883687213135679367096551583500947135217612929610383955139241737963094432395807282293266244211982808258411597799523139300410817/1270259229983310941928319591739488218942376688193452602817795930101694800523906355126251030440445994226937788892519364795961448393295414298579887237867088058193248671745593923933669974611628121985637848865824453298188863857470459673041277509365227689171578160651552*y^2 + 550537032279924455676112734226897380932039537709580898918259735385230197133697827243594837042405396162058564912510925192370971134939718625787757614293248607742709030614303613647555119626722544401192659897088958151055151112292978152615701534620873108065307528024037/2540518459966621883856639183478976437884753376386905205635591860203389601047812710252502060880891988453875577785038729591922896786590828597159774475734176116386497343491187847867339949223256243971275697731648906596377727714940919346082555018730455378343156321303104*y + 77170448458559314941456641143594659883049827799396456171877554172696320429180179894973365820236062765416048978401920241459766192260975995983948315823011532812484283236145046797982749919546436528537606297416624707592911192814315043815143070933350127359908597582523/230956223633329262168785380316270585262250306944264109603235623654853600095255700932045641898262908041261416162276248144720263344235529872469070406884925101489681576681017077078849086293023294906479608884695355145125247974085538122371141365339132307122105120118464