# Manifold: Census Knot K7_78

# Number of Tetrahedra: 7

# Number Field
x^28 - 8*x^27 - 67*x^26 + 366*x^25 + 973*x^24 - 4875*x^23 + 1189*x^22 + 2938*x^21 - 29832*x^20 + 149302*x^19 - 86648*x^18 - 228050*x^17 + 596570*x^16 - 1064487*x^15 + 41578*x^14 + 787388*x^13 - 47116*x^12 + 536154*x^11 + 71602*x^10 + 114687*x^9 + 168001*x^8 - 319208*x^7 - 204638*x^6 - 3835*x^5 + 4572*x^4 - 785*x^3 - 127*x^2 + 5*x + 1 

# Approximate Field Generator
0.402805807223142 - 0.804818772839237*I

# Shape Parameters
1206231102852273901336066959575379508887865253328632857629873042187435063435805918838644238183/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^27 - 10643958172738112453781944889086630144242828887302487639416844939784147095291849472390678184968/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^26 - 72091262062779429450679830376005975585588987636019574308019359643671581682073078693243834021816/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^25 + 501301788642341203333465327863962973531486359608398445197974153880102459980099259173806250656881/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^24 + 763244377185522000249260067535188188675320699006442370152893356086432291109328956146437048342917/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^23 - 210600701775507426933515454571544842949664473286561979638869859752747876107498183609191266196934/48675464451615136919868724234987809306862931068136682160986300939227094388827976862612838013*y^22 + 6786561208824050281441415207790592887366607336019818490890944710753299951855477740584097060011024/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^21 - 1799214210888665192047604426219178937029848304317302063315943658560427287459123054504116295241436/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^20 - 34771536257560705271085651569320411314970525957590077742777598557572064921175154560278768689263122/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^19 + 208830442620578618590554112631875861414178180280726927178485883189724927270427897102943446247278037/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^18 - 275303798761106120893220005703403303830974056731441777298574433037082453136969618259194929033600700/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^17 - 56205751288927594828202035854421452257905207907476655530126225151594495365274249549061978960717491/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^16 + 776780864671035918794561458556038788293292786508071895686451669751016538759823049389167426695560319/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^15 - 1922557838758581471102871863861449950739995532741747313595254596410305825417999167016499413300074683/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^14 + 1604964914880424582316320040393382838825903277919988519030575056679078371510955002659257685467260700/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^13 - 298369199219773934968698737278753568268201094718166209835536524985147610479817284728431386603212454/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^12 + 124483859896342618609668718626958471560875897551051280421775903512096782904730535739751187360297597/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^11 + 558503948256256664963213326879033804862867641392860945322023754767673811738301257542025173701468990/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^10 - 379441056226789165974824370276264373668106677045861688632038306915934071508066077638252128556443764/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^9 + 430162770878879182064253940645081580008031228240571454097593877504156142244096565096710777310140235/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^8 - 136458098859169818929838521177576132548378287419075972962719367680963238993341994944392003437771584/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^7 - 289647645111462480920908214695805982508214623977436795807562869288006068157226086660743194115033924/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^6 - 67644151885740537539371516289849955358968811034626816861228019543877037714666840297218371671042/48675464451615136919868724234987809306862931068136682160986300939227094388827976862612838013*y^5 + 7839378446551902930980840879700551922014393038066836097124055048608214626847765500271819374735440/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^4 - 1332834374179788278937912322732905479127512653234542855260360708059212626760637083100657473919112/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^3 - 150066318099817150944101723078040273522249111111865495768358903210316821768391538556974234434468/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^2 + 7826813916845597629996549450437362021431630684738000330241120212612917679290492079629018961542/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y + 1504746542274208242950170537859333312236933452914416703747336852297753056087132427980026580533/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403

-5383773284318456840143533916937840191366522631535440175902651142315021246569075391916563643227/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^27 + 43918514898215504617290055984619000447090501768172812031108124015584516908483863422876973681863/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^26 + 353958236594425226593466048828325709686578936066199474694057224659614262455673387398478005089025/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^25 - 506903393099754844016618197393981768339201492709751582138250234392084587828267438049266767634907/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^24 - 52442315875605696260495101525973802658851349147544662433810346108278482445350992802101949505167/3017878796000138489031860902569244177025501726224474293981150658232079852107334565481995956806*y^23 + 873764382736322848845999334850922397720563145110217333931082689303422071526521034494067869849807/9150987316903645740935320156177708149690231040809696246265424576574693745099659650171213546444*y^22 - 5264359423612423653272473250908560892339033793691127845329751825919289417734532681915371175296597/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^21 - 15010052391629647573816661052999967891868652468693094711509334292961834661119359438884718088565813/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^20 + 163442300428612301059908834368057518421345480680887078402914922678470460796196285231154440358589053/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^19 - 414621481141643127792641718650100920148146219705429668046070441413065735054994863110295040709753337/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^18 + 592159790593884414006109320341134970792212647044581940183035574506946040563519807036652299384486127/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^17 + 1160779417460589714264701319764672351571342873175943718833714010205403800570173136088293735478336815/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^16 - 854390048371035388660580091198336942854417158514235889646007299056675777885456542940308490406920409/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^15 + 1559897461339869361935147361795415299579860593507618202436590217095143088453742310258671320817506514/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 - 275052671301826904284474721526298341899333624545172452237101066431858003059617938586543376473665153/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 - 1068858082273614240963903897208930507387627763188698096294075248018917285158554300316063016869264658/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 + 250963675237705565749401314063626984381475568073433622834312096657744193809222850345949806707689062/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^11 - 1473354063440582720320531511644719605170203582653793041285924016997768816861907822100571314490015841/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^10 + 12924110894655863366384877497194666880380805331607805208718241829618150870420029186552614322333546/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 - 532882050109436733775184691470626918226967000459674124359779788306343332395503608962877212254213315/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^8 - 210192881085490274937572457600437842475608432041444738594365645405824117470623600360464434418782673/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^7 + 1878536364278722851660699388669554262769683253356189201484103094361282470120977038247255037657376855/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^6 + 26446364090527648602291491625089567238953441210936477767979167096179833368978900772780536806826975/9150987316903645740935320156177708149690231040809696246265424576574693745099659650171213546444*y^5 - 163751829860319374467835027696154147726148200339328153748955882300487775618860779932893582445354839/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^4 - 4315787938869376272165328063430115805747186306536347576597425237346727503702507983666040986852973/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^3 + 2834902334878905406010330027600894471658876272546970891810122256527955765530214292776183965465443/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 + 46185165499682346069339691822394431496600416212405291701395781453253647069883451519963465832063/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y - 8741993382699650599002489893922349620303841916847723543190163716344201991638072225668057050967/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882

-2011120513287066300805366310162580317627938623228260671902930504233046689676162832725287545382/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^27 + 16015822529112501474499974208873746936199791862875109019965392455905629888386981686779845853920/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^26 + 135532721569480398579906531691213390663082124305701372747050528644747291580905938380721560165729/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^25 - 732966664321761893925424971068819186163949409854920567025576986245056823707719173300120374373322/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^24 - 42459837936569375646617509605041317016836179981096735454139184717897659236000229616012141436120/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^23 + 316705585343489119487667722078461126713263054098738080566507555543637362091620046764311157904469/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^22 - 1910242103731604761339120290205752405042291180136116979707288928794592057454009675861060271368846/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^21 - 7101109823538821538203968787063698163575232356496243932205270425243447422804830926982156555969129/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^20 + 60969811787433763802333835689657745241090012837017162978042259225739312007150246977876579146842618/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^19 - 298401298571197233589909953930385828404580905240133903140023775452231752513728937451129823827211976/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^18 + 157476030034481374012212158257408738132868147092315554133464491231081564702034607970202808888602993/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^17 + 500334102780120829146892965706370979567054692394653823782099627429821416031501352426460251449918711/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^16 - 1230839573871145073526067091683589986344113866349792389758582427421642006777726062728346341730865563/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^15 + 2088763635342111787354978622049375142612105626641133015605616560018230342639454203900576032646221322/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 + 126772297079900512428552191794395993117791147217764820492578908548390488428905854660021503460235730/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 - 1915456302034041939356796428077959543385314658291079723974563264136774821310919917504416835303631376/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 + 317914249210838815360409158900764559536558502314387387990934138581578974712679459775948161268534534/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^11 - 1126641762586733668652428492144124178883413330757153001612615616964287712057351749749793200502762934/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^10 - 169469580878610715203919499071004061083702468030987130862461225741287589957771182098587708652456789/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 - 141302627684527097691006066768162588107886853318099993535204520692710866728242562791266799667664410/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^8 - 415442798347493741489274157946968340173462096006985929216497584905290516690909025520664758330391019/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^7 + 701488170983043172185604329458741922978836594164710611882091822785327656012692713248557062650076791/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^6 + 13253963475025398973068003317559726301585452171020142412180112612540226160581552129158438039251958/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^5 - 27616726983396018023792683347383534884471476107270775158410144229765652244357400760236957777994206/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^4 - 5923025940512511334137565743083750407070726242592829646429870175181628472105120008213679772872111/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^3 + 4245542710785503335553430056603116305975824461733792875806538178372440653887536292379562418577703/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 + 55347207015970916189907213095413759352764643773731030128311427145794980619974703486587951766751/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y + 54312949556761377358043069261118301556174669145500936834372887769541114078257866224368996782725/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941

-57177788475646410885240050511493389776817426576167305914119573719153085358581954990010740251041/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^27 + 464956094733815469062529684985644410818117837294156527122094619926173114609807956730838905139041/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^26 + 3770035545214125355519752657964050915792387246462954744104661048086400092509179616256224209237163/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^25 - 5356776412011912152698017089626720571001605769058057562572114214046223589637284369604756588247391/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^24 - 562074344885147914301040729379426667188467858548553870353545532891523541443491785782480103070169/12071515184000553956127443610276976708102006904897897175924602632928319408429338261927983827224*y^23 + 9221213200645901821193632055238390974411046179612613965948324129589748518511942978358739534284473/36603949267614582963741280624710832598760924163238784985061698306298774980398638600684854185776*y^22 - 52674846673414411767319956888585503096683760389086729967589714035157027427157692588276433465458545/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^21 - 156160428381981586264472158018870440043321924475165133371970195911438648493007570593623371529014307/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^20 + 1727778442303372000101430444852273326489131929356072303859196061919321035904694719719368020557384003/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^19 - 4381925755248349619040814618126405218584718392320881953802312717041368091595130139516349181937616071/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^18 + 6097248139146629956933227649319336714690753848853676941037096666386802029812745561131559177137806949/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^17 + 12299705929166327837089382299668572995139606399882542134651104071364903331168366113444046600047886205/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^16 - 8949077572463592156679700741527192218280642113138444517827016966506625369427776444398555064412915097/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^15 + 4095082122521674433492989571485760911664674241041847393326425988449749508828441748096504181874675187/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 - 1343347222186887427308306704067365496589962111329518879706300763518618214537491866777879407698560227/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^13 - 5517824411025597939559479598614642308716887706684646376811734153825242036475711613124735408273788089/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^12 + 2195367682355101425731541074302303991181569258611159778433911293418356100365802500152556175680165225/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^11 - 15806066713014917043920415203450607304851894865628385337809283732706377334644757613372466078467274987/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^10 - 2617776228818617601666790447199608024550113313612252753523547416177891579166300392750251330472391/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 - 6318491042092601446872780165831078046993374117614110403788060059987674207432578380382200857488035281/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^8 - 2217638751716998454744812524168903180521684962450982578544989763492049295022966237481738000309211401/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^7 + 19494978813653082379802317608955205805023959793473830349001525274247375525718715898024872818339330869/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^6 + 295232413677345612265487458263611816115423975765590804344706143623832198889173916146029171744775141/36603949267614582963741280624710832598760924163238784985061698306298774980398638600684854185776*y^5 - 1126384518442924317682893618367153733497251970520231602537165665297245353583916301718609420944246113/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y^4 - 32313548236488826700882200148571728617340227489717284399231890926669093812384974084131301488956517/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^3 + 4919565437108095721106770153099034200239556178677262262249465585225990755632724910474935197630075/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 - 797951607443812171903412818584950743004666993659537040282959540921033034475876249483702476968443/1134722427296052071875979699366035810561588649060402334536912647495262024392357796621230479759056*y + 70545082007743292103426715459458297130853730642164130229389360312616876057606104255107209423729/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528

-1415341492627944878716449920083082528839779122464807708914692358743251906956798153324371467865/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^27 + 12922702564380912504446117411271338681880807986688741003642798573587325364292596988720758185680/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^26 + 81927903576799570584127630616271349354566438236166825491151886823015980143126567406041816285597/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^25 - 624389108255424392474353567097710792307053384727205691208730980264229069610263098759143951257652/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^24 - 16702168155262341984788901396994011427982320563932100549557226356747950718030592112087923625637/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^23 + 271561145713019906070936187053949534863311799673566466179087403553092477225638524962503817165062/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^22 - 9572033796936412146526290333887432766733155323674786160903179923216072465010324432191852945168965/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^21 - 1745742090579325679217536113660369597215096178454046876936997179366083204168052157260835034900557/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^20 + 46694589393702953883330194542425212230482378786713575374892647334620003226994936630213053309120568/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^19 - 259311649877561479511368144673761065382860119275606402392219377776535532324253949247780328683236333/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^18 + 364580723613551371954692685407511841253868612219099568242592147194286038898872437681535816980046851/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^17 + 168499373010949342721996318804464479638703892875804112972394152792308272232464637827303674473354349/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^16 - 1197214128210752037848495455846649229890297929291172113103129329386278585460771712940147435971593226/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^15 + 2482052017423439805131585669997602404132419851763392020425455521701367105485910119706057752015048649/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 - 1827165867421590332107148012837067222020926622273632919365989094734498785815602687796230658314480937/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 - 927500410937289568397694416853850936438485802188110399731775694525937964871200104322984249402737886/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 + 1298694634518489046184380159611684215420935655156953330393772184800153338396685651241407121512354232/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^11 - 913256801769254627263484708218960175260876740340170304891878544369513304391967463230242038795795767/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^10 + 781766451262908793946520222350097041284702901078437495133389458891065343726582455166619905597999234/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 - 104845116451482873140374344566560884238580949119678789859152387973396912324431353927229058274617727/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^8 - 49800897587398305379671307283089151751408191759404869803126720759875896848522670642181798153367025/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^7 + 710851145226413524071681278069841121211070893352645321975114224377933941401848122109689474907066829/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^6 - 7635992742530689718417479789119754802770485380444742777870985560539381514320612149751290078433283/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^5 - 285513810843128602920132132559881289148483954387387459757965906550461878702069903713136385626486080/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^4 - 28699809098516391751684828249567398832980832871462263468795907865643881124004721597475230631881/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^3 + 4444311686431551754007367509476292257170118188342772146699094237299270954602087861176219349301654/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 - 989560337652209219124004902092254399793904562771941973264601111420785980653736772859194706637631/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y - 1166366849755629741385140225725983681977230179399336815545125163768087670891509775253160101154/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941

8946046342733936629151669879175674544403429403797075426650635906578141509332662131989523683525/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^27 - 72803765379720570078597625947856327158028286003906418759888871251019960286371360520950884890763/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^26 - 589362949275697603949208594284114017581450470084483593403498561173670273776719610080217344015941/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^25 + 1677950034601956668264265289249031524091039792553392106976666489016260637306250163836940612878525/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^24 + 87693031638626828396606052134063327884485906754594437752954107014369462057556972987682240887455/6035757592000276978063721805138488354051003452448948587962301316464159704214669130963991913612*y^23 - 1443948679217508756890677980750927129118654372429194126210492126100117268714637310560067877377553/18301974633807291481870640312355416299380462081619392492530849153149387490199319300342427092888*y^22 + 4197379998077654934044436890415388136274093408750815717958485704969411282504125426260060500867439/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^21 + 24129460155673212453210188911063985670633336733064293430023381716380643615431736655635573744664151/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^20 - 270276912517840585915470860946602165327389845963301660338911554051604270618873075221867066031520857/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^19 + 343213127448673316496777940687951568789783699230921169292909998647211167196571594532867127841695451/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^18 - 963715810859463805314009094088430204822316009399377328316614579130240710820424455873528096614632849/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^17 - 1912009652280779235596737349014542444801781230316719043834851968440753998087071854681723456980484659/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^16 + 2802245981808307957124157089119924522443948381543030075706004180263031452854919690502408589069913891/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^15 - 2572174860065501416359822932320430101045538278164779606503267294089725069257644751056146203621646241/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^14 + 221247650508664090072263064490623962825973839099934993405573927364853699190466822729040141390215118/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 + 854671637058866591352526211741778708306027128508807507377395704877386658895168481719702117967510696/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 - 342141328989469468001195298961064171162670782887311733827917841745134624673126717644870047551658087/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^11 + 2472745596103587882485525973923902930917042167591775497599711076178749837570090124706702524341066695/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^10 - 5160321076810713692294796516286535471613971970224721422802475247873583795671659408585614253576309/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^9 + 1006744624929374172153598479257903735788812047844313722053093313263938416043741367021002119057384789/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^8 + 683434565806437688822949028574191775163680220321134778844546861283414184668636091097886039307703211/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^7 - 3044285109860982223628034623316411050335888311077908447355660912122730101009456923686382106914789085/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^6 - 45709259563893964520122346286495316956536564019789518717390685556626339415363054707860266580058895/18301974633807291481870640312355416299380462081619392492530849153149387490199319300342427092888*y^5 + 175461839767786697000200244081369662391680698454347385321088358896908859701032822244242055892057459/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y^4 + 9948555004364928472531123928172805335112543110850531176186060695890252316328135111688851037233433/283680606824013017968994924841508952640397162265100583634228161873815506098089449155307619939764*y^3 - 3037573107295222315141023239763538828419636530637898337778812163771193478108554929681737812337875/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^2 + 142039345489480601500161383779426399400098228256384266404795096912845460624205356227082028041583/567361213648026035937989849683017905280794324530201167268456323747631012196178898310615239879528*y + 173170530047339297916605284062360481622364303037847826994569902129610640754794064933767465450283/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882

13306986131956199254485639210007521506292695804974836652901756455753007932427115869939569488196/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^27 - 107387140344243309739258335066863973020047344156539851909256246422742979828512653255953137239520/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^26 - 884045580840323278668693167671072506738402328698554438718821878373024204361674690769924177450585/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^25 + 4932184350249513367059101774397567378165123043714216488326363954081780036679511164728913998750094/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^24 + 268125323968842900701568883619016396416933387821120207722431865238559569032333230887848470517389/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^23 - 2121031831703282390984379939284184583488013590958376400269609751151457502809692806891631239650979/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^22 + 20437643338479357098504928307008102646332855169421522094020602391185614946515021707836819312482955/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^21 + 37646031211826634847883808162438213085506888721388076553637055582162757404267354359380854051401789/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^20 - 399693234356303225289559393171340676215240260265873935916461784498215408130460776889008547298507826/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^19 + 2014800738822423687055021663022467943827198273721435215064210271697570638452380021271719891067593979/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^18 - 1294212937237662684340680436498632839922145975006959283488612072552939840776246487540282616699333262/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^17 - 2943545422977661386269835384061566041965004089226808328298976286831085015457087878593298475389879632/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^16 + 8146817082298743062311432529348044616343434412928599493749305319104294259775708361256742509537672216/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^15 - 14739343695609812749813491233796523411717713066699308499897281419136506955476655387547979032803495255/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 + 1585948769938107552118679502690573585061461321791712555016270458470729007409885124298398075596364877/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 + 10370441264857847680228562957308377533726020437256082634022577859649563721297575868564295883355859608/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 - 1375393337401506134535070545668389513888464483830276427382930076000799816196269975184466560780908613/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^11 + 7244889366487200186472182391104617389656011297912917725163097389692151353873770355342601511446012161/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^10 + 454462453303434226585607911910887677215757911886216703197059830130061942154863879459266142377347673/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 + 1496973712314626787867544211758517753959966002867658306731599047219457141551619321004366291016241882/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^8 + 2142031016132833297554114166888628710533538454661648336007399405980399825356943420945503154297974788/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^7 - 4398010571145957152479427483251283388164284630059860714595470048023405576721245282119447186609574346/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^6 - 77755047785560893513588104306203447985386525838411767144547543617742681894526911417479135473648538/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^5 + 117032951375163091478522349731783358441624264149949488661758156028197196963758534176661682833939620/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^4 + 45553545151571522043112833132476183139058753409720686577128753059230085264343421982073055674989215/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^3 - 16102219217577734616180420187391345701855988425656033647186953219707070601274288377610825345949095/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 - 656118351485461094466803044309824089181010553501486179742546167354088306428370410954235001672239/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y - 71979433454532037716643437692903532891834778427186140810925571814295393233566809412044521850428/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941


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

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

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

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

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

# 1 Loop Invariant
64934433008754476949024420058509618178971561033388920643160427962508829493501028732100951270870/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^27 - 1138263153495076105442396405423609056702323060063087729072279822238280276691031318091949826941313/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^26 - 7896586298675294175353408719394106391375312777574665447828198513272339604544018736952112336690879/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^25 + 54099480549738031336248608416116052682057697918105862906693848560833917409172216054839659659648813/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^24 + 950867254826873399417138276262133109619321648600904105284642359226059029217817544904815563458729/1508939398000069244515930451284622088512750863112237146990575329116039926053667282740997978403*y^23 - 11704784662758399291569433265031212736015436647806368942034145229203928848554045321892737401144907/2287746829225911435233830039044427037422557760202424061566356144143673436274914912542803386611*y^22 + 646264202347328098395239284287456616991989396663123658890863648776528326529099174648708616000528657/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^21 + 104996117894552310072566935651142218943713399191656840483624494366073466834243069473056608754136571/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^20 - 4125616197360548488456238916240734242515844898489855645545772586706107545950825949393199539721319661/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^19 + 22360456353627918384613973836211832291220903449461188086068331832390134143965877247557532896502292549/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^18 - 13192528098852830476050254429420868184652892290251851874832934096801822606049847738982704917191091069/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^17 - 19338449225837942619839895485859273640359938830621171147730133297486018964303854929224280624475666355/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^16 + 98354812770681854819373793680100703364102800917449047971977053096540037412856922108061617924695153731/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^15 - 99424916292292110345952818059916708176806252029632525462726702542474120980513333891103565071812260681/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^14 + 58913421393923589910374212276486232502093410558867791819509454937093063002320610831021471291576448778/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^13 + 41924168708426128614000834391145073685828704551509588211765565555312720802656624800044416671505106481/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^12 - 38134763866402116079174119688954164633174140905652369906482289740527666415227828663398775697228921574/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^11 + 38892613751820485551220881119191279859000951162941729067550647811555737621049871767803482588067052587/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^10 - 22863393743056965691262857864274863859144925894682322696700218367859844108462460605266708710018100498/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^9 + 6848333896245704340205986646908175186807142562522625607005588957620441954010193927489344624592899605/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^8 + 8037145282330103605422349745434451294571430213039836048050251444440509912181741056293797120708471355/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^7 - 27843768903090968707663951441231921123605107025917357040108845790785889153334759593835237971602545208/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^6 + 171365289709058332765706746181607852861979133860461529727020856635976239879409782419154325631539791/4575493658451822870467660078088854074845115520404848123132712288287346872549829825085606773222*y^5 + 16638869674168202360924986489802185238991843826124782994548090331744822025593375558064903472362452803/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^4 + 467643675464854261721639551493335382289147927874112419987257987720707964553706593463467145742357717/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882*y^3 - 134408342676156321497032127326091032858007521921142190967528396290003315794047242962197136168383930/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y^2 + 26374385212080799615488852631996264316474527754392442674546300983313841520654944350184831336034294/70920151706003254492248731210377238160099290566275145908557040468453876524522362288826904984941*y + 2841190764670318096485034132469815805078423965311268330603728219933394460193899888514927693134731/141840303412006508984497462420754476320198581132550291817114080936907753049044724577653809969882

# 2 Loop Invariant
-1082456644885706745991734812470941994338600246080922574011278810959485396792252846570941851669102639612287509437019581019718569180194093181298112792726856954606761215337317934338773856102751/67451131558678210411472309576712558498129697931159395132648635431249629738993127757400690268035345295275316919181921408827345675834922939807019069634941731185600762249901587837840480854878796*y^27 + 106126787298377318087125203811801221209999410439359789451799079802552476695517917791607128653999554944788734946358088451747089065165957046280695764608248676977666999813883346716540202063245997/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^26 + 852464022391906881762132058924076511600049365991206173757727563341051828711742122367093285280482487426262040718061446143886173988248214995534475791408075914435200607367470819858416432248213487/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^25 - 1633705183245956450573513567933402358859523840041383104616695513703082185722260522365775501041473188337550933282959412621237231107679188288168993347922568607638060503116207735768973874271814329/269804526234712841645889238306850233992518791724637580530594541724998518955972511029602761072141381181101267676727685635309382703339691759228076278539766924742403048999606351351361923419515184*y^24 - 41915261118540974971997475315894325185309143590397289203244777590124592662868771530177335414294042736379645167052274154256510017865556193228210799789588067404063733865955173524311006817546985/2870260917390562145169034450072874829707646720474867877985048316223388499531622457761731500767461501926609230603486017396908326631273316587532726367444328986621309031910705865440020461909736*y^23 + 4088825096657806584325762866426554787819534175184253795825255957130884916390007764585338327445545318426783179030432281028430923188681771722274063761987021313675033062515049371126113695429210448/50588348669008657808604232182534418873597273448369546349486476573437222304244845818050517701026508971456487689386441056620509256876192204855264302226206298389200571687426190878380360641159097*y^22 - 13177449314839460862236437971788732087150237218799762568013538644652752351140868071344436871955284728251719921304693763721860253464708020835730867609284632162771126354532935066573244990627433457/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^21 - 8704697866000838235241201337306912746073926449630230986576039194094714842557949232693491390837148743125882223077980542217493526074720938339630774588044203464052227406310615894909115134817658389/202353394676034631234416928730137675494389093793478185397945906293748889216979383272202070804106035885825950757545764226482037027504768819421057208904825193556802286749704763513521442564636388*y^20 + 98431516410994073698446370692024963551575398499998139009505253969883494089779823452630886194664545771229790967510495627852832307303685643904741878877325614772804788766816909817975337367413639191/202353394676034631234416928730137675494389093793478185397945906293748889216979383272202070804106035885825950757545764226482037027504768819421057208904825193556802286749704763513521442564636388*y^19 - 2005669454615621324787360373995876319477343196770333160903892026083328518974210514460708508347630833561227418808662590763862437468081750749528153834499122263971624579414781203012748203987136893647/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^18 + 729961797514008473847897163623182807505200483089922261834948335575428127144808311792910799421081702242015799220460074844300693436735814663296179943372414490144015107320744381853522773667361967605/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^17 + 1374327992499795252694114065718149524597697792600582575933784497591266943163165381550340932400686395559069754373159315193739013865861765409770225480741080219667670188277936465502381522268433800811/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^16 - 8237761170505864553433894844663854972486099653476395174463387987564831347088950705191862687102677166729839865971264132289477959300772599142874157038702103608012950518152026638649862536576091585387/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^15 + 316164103650971452439540429219314410928199228377556056739968646112124860659523593191531918317323402071609066488830871031804328767976737456444162089785457283422284517372587644569512051444086643008/16862782889669552602868077394178139624532424482789848783162158857812407434748281939350172567008836323818829229795480352206836418958730734951754767408735432796400190562475396959460120213719699*y^14 - 1491214594942967299189673348278114138687313310434042182314432100715250848058104288711777858477627435208850652241559737017915252087779856174317167204417415347005810674943073482385670040981719364915/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^13 - 4985082557232936517702873431703002307509357621006177596947738701240129078480485114263771966863649037545243471720811344384988300072531151209081272198790451479435512663104459056765439942442320350563/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^12 + 2320984291802889524983753976032832922996283497439775508721590504653085915314775746363184539699632457694373944761285694768847749211354598851699161343564816000227840066501406429610927993439236041717/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^11 - 2390035753399569685024524850489864852649796963295046830840831746587737126964811091309280967058644727234631285537369904367276327322795707341718563578219930364611884374417724347135568046921035259223/269804526234712841645889238306850233992518791724637580530594541724998518955972511029602761072141381181101267676727685635309382703339691759228076278539766924742403048999606351351361923419515184*y^10 + 272556659285873368399569511661267141245085917603526252672553755587958209877907018979284904615674226166777072148215857095202534544891760100232297062644370084258044546751165567084763820536884685705/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^9 - 706665831974202052019919229839421573080711979063866640662179063451703421909549965216226968514984570364726676270502266907465808258685986737441178478648809020715054306710687872274137941610970734355/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^8 - 1926837401128628211824239935491333526724681645492932861970732237288112923402653458303138872587535103838237829174803466457367610440332605152787870199023676546085964157762887797619290021479787471835/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^7 + 93705736812566833388430099339507649221814686431272626416240613482574805148125005458873672844586485529762017551543599148886872303263547981648450079328196022492133867081365591124780510582001013154/16862782889669552602868077394178139624532424482789848783162158857812407434748281939350172567008836323818829229795480352206836418958730734951754767408735432796400190562475396959460120213719699*y^6 + 1932164263323572505812124679710676642161145333347145280989486332891859745908082474739279715533118061436456714249184161273493359123903987285087781787496353146013302444157735687666193608445741131923/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^5 - 118402341664711540862012440403400014728139969412185606609421202136149246337962613138286164615066355547546967045178470158080186854737045136408328077820829381532220789075366460781622134215039060299/269804526234712841645889238306850233992518791724637580530594541724998518955972511029602761072141381181101267676727685635309382703339691759228076278539766924742403048999606351351361923419515184*y^4 - 22554761630745469346842121599936994207638106141274645584673848127816133434987349044781475773697209686188770007779796497385066329306547801214969199611002741560040779613835974122402967774817654607/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776*y^3 + 19583938509415546532861259617938191158817807305962193324993050285586754007070738502057591984980052432206260813221260879702348009198867894303820352560732420940360475553210087222393490252388978347/809413578704138524937667714920550701977556375173912741591783625174995556867917533088808283216424143543303803030183056905928148110019075277684228835619300774227209146998819054054085770258545552*y^2 - 88006690076661882389136196898138578621147848505850183552559923493321702750665961639155043999028570236901143069168939932017828194136493304115121421352374252099472984172966411118849254978977505/202353394676034631234416928730137675494389093793478185397945906293748889216979383272202070804106035885825950757545764226482037027504768819421057208904825193556802286749704763513521442564636388*y - 294860245519691470935721972303130204935940345910296462215049146678667648041125123326499201537543732327423669160721720448256277534102763456479124143451505385097547412030898084842624941459629619/404706789352069262468833857460275350988778187586956370795891812587497778433958766544404141608212071771651901515091528452964074055009537638842114417809650387113604573499409527027042885129272776

# 3 Loop Invariant
-50303847094065456755709120502292646518929949985111743675076693085423940712289584259883407740411160946924500539344487992458853222855493250133379478998853362227434609119778749047908105121621632574247159150999840654327806926362416893941794123/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^27 + 393332338078181577124790891121448191335435265166739812519277442744671479021667897350941313235909784602717265056058504321389525166795602261821924115745221292308595012923272189821521619988507207055278107263965232094706416411531446629771600325/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^26 + 430005715124099836206165659150870279264555224898123617148993405845041433183053831948272543604852986986083725509112029087478459721893343537445877876879857121589895281149159992532390727679336016974926242002474030892395385060533943472622242417/11353808698022231172191433312701075166811304627379971335364119546595345358824942824249518300965869520041383757179705576859820265279678639121858961293738193467615094724619918130721363965361758847682904287066821092843369305196437664631914349544*y^25 - 8887817199047651709272391006076720791112173648830858754587921405844841005523282329218338600759429039045504026248447198819708588417703487972662217186994880311305771444224396922923038314695639444740072992054167507130749277888413082442496493199/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^24 - 1108042103215827867801713968062129600018569715033303005256284307956754405869855061626610734848797286941762172468457428428391450634313289153627651388874687301338302574012000206638820151363349257689513273240217124496753815062047368743039540677/1932563182642081901649605670246991517755115681256165333678999071760909848310628565829705242717594811921937660796545630103799194090158066233507908305317139313636611868020411596718530036657320654924749665883714228569084137054712793979900314816*y^23 + 3793051490166383658917765026562733091106000547153578972789460416644039452444253086180327730886546706628948674206194799811106616811582982741495813511618816217148857258960450367916363769303050843724573662709928172363377753523495153508883946489/1465007573938352409315023653251751634427265113210318881982467038270367143074186170870905587221402518715017258990929751852880034229635953435078575650804928189369689641886441049125337285853130173894568295105396270044305716799540343823472819296*y^22 - 9003080704478465759778307630609521953861237500963579767833849683945349165006313123454210210095617030226379522389714415450622889352805448809399037391740000937661779690653240165601382525839587214389734054358150802087620269883195853394162452687/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^21 - 142551906222887069047734390653370039175646141502914482508872101471095178067223686262588312737302505670902942717487571935008283973853326577841367933598083207598765509046896377173986057584168212495106123048079810362965124393045875419617256217857/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^20 + 732022628389449162813279338042095669677087240955090230309040510849428019094375570459837052043704311962693347724075796699037088224958297653203435932371966945882929972595873164327409723079032355212245167710306399504800282482248194218055029361371/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^19 - 3622033404739162270362561267779859660267467816489133027552336813019051224487539870633638221369244255721901796894384900074588514538279297135697177278144729999917343883061953548155871657697013463223885476661341242710557989337522962340199362563479/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^18 + 386843577948740441006328341199032720783650931425736004293095567542871625679500188606154011530028932083822770259503673800250276014509340746966917385368401027182785995271360304926348906469443324871569310442720922823841760712887494422976305205521/11353808698022231172191433312701075166811304627379971335364119546595345358824942824249518300965869520041383757179705576859820265279678639121858961293738193467615094724619918130721363965361758847682904287066821092843369305196437664631914349544*y^17 + 11761199049830953962634211735615698424416922760806222551311104446064366674735340210686333061195916687237197400827163085055626850748484542093623714006375769086423700854247378013671377304596334607488068069986284409064703699535332877454590542232281/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^16 - 3434256983960673401089182946217999583486218735665517176342218966329745436979296791538579924189668553503275160300059820407598592126352653266611593424529144410633006243939050432536328117766855633963718680666354606185905776490661412092283211956559/11353808698022231172191433312701075166811304627379971335364119546595345358824942824249518300965869520041383757179705576859820265279678639121858961293738193467615094724619918130721363965361758847682904287066821092843369305196437664631914349544*y^15 + 24320704432429155417634660207656117275923219126053461605937165372723511115664533649809015928446870863908235705572699757083034189932306219190987975214847104078728607528311924066946066888831699917732535449257898441176383208225931386833055860548647/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^14 + 1386913917133580912854669954760688934258215927312180828647802213741149349019004422036270616639547825467447585269057058662387546564221190797843165550880636342114026395142174592663334233441907741608516683004670574832271350589477774167225580733597/22707617396044462344382866625402150333622609254759942670728239093190690717649885648499036601931739040082767514359411153719640530559357278243717922587476386935230189449239836261442727930723517695365808574133642185686738610392875329263828699088*y^13 - 17945334814212960548553434129352680203630685530726282603566886653724477792062763934449518330775060743720665701171744641386590221733089342870063126066510866034788629962531582649142734565497145362908060193901144610947721712967732930676541488993617/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^12 - 3259099741485454690459145770849027965757961982262777760506983405001843658042232356806179999448664730283202579971461197905884485151985217329915381415392373637942361135694172164720279839724140893765133747279457748776288935518742841567214162145569/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^11 - 28265460656056656068987553524662567096812524413603132271912244391803737118502766013485738440286554038918794095027859393546631832166355859465132758162540740986744579900991910529789371538706019949373169455132989276976548562136856274173909450161215/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^10 - 3827918002822579917407597205477375605191119163101792423972832059559244242098882355053864019894376632374302020518326687408729638791403209697822489715105669385647797114959743023460549433744485367371393616943734649365869299650711406886897820483939/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^9 - 527314742800944147693642857836931474616378170010465022553593863104904543061177397391026852597704502078503197807708683760780981778790748675723121405138606013257512795159277928687879345145587049566605060059507482074778793194808803782600006832787/5676904349011115586095716656350537583405652313689985667682059773297672679412471412124759150482934760020691878589852788429910132639839319560929480646869096733807547362309959065360681982680879423841452143533410546421684652598218832315957174772*y^8 - 1121683930344322262654415291974007703017075932712622300613998140257392843696913605554998043020714715867881692843457528014799350159864913089951708607591381149142268491928320513496228474614018428312994094886646957164423215649879952933584428508029/11353808698022231172191433312701075166811304627379971335364119546595345358824942824249518300965869520041383757179705576859820265279678639121858961293738193467615094724619918130721363965361758847682904287066821092843369305196437664631914349544*y^7 + 6964293138314065722825260013425958160078881568465623945399051819665957050428968713991299966904893431432860036140116216918819402168060517607724979717441532966017823497468513287798590779293814026950650353338469599789951650484888422126091517139605/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^6 + 415826546828487398567902230397030540404673424566099719109074912693431906514959392494173069837948665556413161467088996224224881780736612795161991335417730608632007086725055479744937304559253745034890698609965215213940521664806194069855912801749/2930015147876704818630047306503503268854530226420637763964934076540734286148372341741811174442805037430034517981859503705760068459271906870157151301609856378739379283772882098250674571706260347789136590210792540088611433599080687646945638592*y^5 + 3140879006164494140151323839561815954624379320042780939451330334262016496541828938329265498576037486256310061997961916706189937362060088587269495235323256818649953405197263242473656419300894735686773915712023955851163541155907872817579647966289/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^4 + 5711234898233734001819772501575537771774499386723955310462635287071826204203898594564880311336418008653253758696568500822035975390859079572503529517405064543521672997317723361864024534797032988773045658444265137060346953625560813056098396967/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176*y^3 - 53470032943365020895157036514559247544170042045372784959194542211965905495852709399240297589712212662050415225904940186792578013998777297893332789958581549635506877949028845439189230210721453058766538701061027375376555199345250656700824522967/90830469584177849377531466501608601334490437019039770682912956372762762870599542593996146407726956160331070057437644614878562122237429112974871690349905547740920757796959345045770911722894070781463234296534568742746954441571501317055314796352*y^2 + 10150656776154553642269532057058837205410700693683695741870853125440766272376307648068593751805682686264588282017416395617156562347672205346479229721668176159171122739124525168892291377666337674853301870893015449949802006702090235026066901493/22707617396044462344382866625402150333622609254759942670728239093190690717649885648499036601931739040082767514359411153719640530559357278243717922587476386935230189449239836261442727930723517695365808574133642185686738610392875329263828699088*y + 1634793070274246818862524566265182779113787222012457085538275383469516183830021704002229854995020176665074045011485835731652675076601141300798063076913575352094621885789289644174807961028716628242264085750068791861091543638963246038955074531/45415234792088924688765733250804300667245218509519885341456478186381381435299771296998073203863478080165535028718822307439281061118714556487435845174952773870460378898479672522885455861447035390731617148267284371373477220785750658527657398176