# Manifold: Census Knot K7_123

# Number of Tetrahedra: 7

# Number Field
x^34 + 47/8*x^33 - 515/8*x^32 - 675/2*x^31 + 1574*x^30 + 26179/4*x^29 - 22696*x^28 - 479701/8*x^27 + 838087/4*x^26 + 2121661/8*x^25 - 4847999/4*x^24 - 665297/2*x^23 + 33769461/8*x^22 - 14078427/8*x^21 - 8325897*x^20 + 68247633/8*x^19 + 56671351/8*x^18 - 119742007/8*x^17 + 26254611/8*x^16 + 59020937/8*x^15 - 4117207*x^14 - 11863299/8*x^13 + 10852637/8*x^12 + 175339*x^11 - 1780461/8*x^10 - 239373/8*x^9 + 148411/8*x^8 + 22447/4*x^7 - 1061/8*x^6 - 1783/4*x^5 - 785/8*x^4 - 17/4*x^3 + 5/2*x^2 + x + 1/8 

# Approximate Field Generator
1.12534270728178 + 0.483393910484989*I

# Shape Parameters
-3110768536795143602232330161056200262786614135786029811954416484565587826197264786299311439149400040/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 - 17376624744406165169652897010873941808457174468878829314472503587903378476798823983157088910016919923/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^32 + 205281245322858278126992040890010962412816104067357824055298798898794746169482009814612976545453249687/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^31 + 990569968082735721177697701685785049375470909293487075695415453756866777045478786418014973334262111592/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^30 - 5182835039303126082518120604883013851453967605222644039782271673476569427080312992793554738008192819971/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^29 - 18862314384453061344733783672335086968761007355209851854462407896278761580196691081554094250803865403543/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^28 + 76057455693229178793126574486312326968206306820813313448997356021386473336579794338455578542195399168125/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^27 + 164568766585975644652812973029497504574990405944724498631321792609937597236349115488659908559780151602346/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^26 - 699384629029489794759505221265343203929459359924917967059199254358233952468812262537155874947169520294135/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^25 - 623066535003784305152722628082196622358613910560177641834054986243847049149616396529921350080793411204109/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^24 + 3950733844483938570952281216795561017289299982257690997831631327817756316148026548996793198003323015348434/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^23 - 105985558270498853062784454866222323801523458226813005320845829662743022029836597216972855900481825359334/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^22 - 13102824172872189422852495520587233643987598099482499086748614242125602978893568707562756503805760468828085/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^21 + 9258399216413761665356792496979566148939349362336464163771879447146085029624757056471953094392959505136543/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^20 + 23232568757609801681486471251773285969527424888720056205228208890111797552187349965060187248257408672646527/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^19 - 33249613941447593514851644787419574777443554948776964604551626579337874983145257929801151095989650792356876/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^18 - 12445107607304853395555445565760995576529980446987956793176702217267267534786695800889259554753866353400015/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^17 + 50163318689919227059795454546277847012948564009371061919914454033334469351378973622583547747163930743117366/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^16 - 24686245504622942717405907849946524969968084555953595631120806511907449342373831459755243312661453565943739/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^15 - 15832383980803831657886565840186856218159712895324830215322678288692982510511393548931157768783337295121894/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^14 + 17378684927398729764833097938538909857299037182975458964340568813956106063323471560123746546526205205889107/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^13 - 400939412814716358736983420143137168737405722374591829582201158426879941092914588283832759202418524187638/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^12 - 4104386977708785079816290608253000762497567667162334823115994375825366668660136574626374730988185477683114/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^11 + 638901348479197583629976311607522012935836646523539402794149534596716442191409325631137776173088341031688/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^10 + 507637939041249382327977637571128880498834168057777449552366189681435814753926320966492205809335887201481/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^9 - 53385943547733194018773793901383341985292737577716265296397350505345927401441201259454551848842425737689/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^8 - 42210955791644481796031589041895164669751888465898574155351993121644241899439907933635829679025524330174/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^7 - 5271687514247321372520424224815186239519767706041186678063661548530740420954165336771511760660774044309/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^6 + 1923287141475760773239970052456590075002745086169954653203832522101416992098775095786362926234006101738/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^5 + 829137947515835028778570348201544070542161531264555040013864221201746359123983095633640790995137845853/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^4 + 66163626821266168837756491115373831608636944835461019767732568714520406936759212087352233583591985332/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^3 - 5692309557127781854579270402309468064306857065271187056202240685684705320449337568160183409736586824/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^2 - 6100550128665448300300391239276988627743254474576845249606196961560509070782230573624789688388817300/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y - 1345510594182240593972528574541908694304677768039565517727430210951423494173980907226751800100925398/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659

213676823679195106096132635876820089629098158811067032037994189188212994084010820851920570682993184740/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^33 + 2379880239072444101229476471900407844002963920148651491412207940911097609913307512428254207758249944271/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^32 - 14123056904570625613519964150609313475078872355809154726787847700696918902507936402934904610856681543979/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^31 - 67814513546392914298825458821998734219240856739022379054920217478960444509266321579955330944690347774099/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^30 + 357285968905722438889428813896290295548093392866216188970898008286791611703434195255021387587863033884146/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^29 + 1290348926420238037682200140977412983242618501359005961062845246605462322226375285241405434556019261112873/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^28 - 10497894253889742376849721977155374268692062633388004301474126051370578872563523980525331176243580551306833/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^27 - 11230347682511384752887079059622081258774234351347582034366409689531440099885372105523631321069352247822606/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^26 + 48265442522090874551468344817523546883165794800088175115674224523493587683179040623313438824569161081865697/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^25 + 84254615810745662600056883723258951288793736134463094686076004430683509059799539395806357576462423690697423/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^24 - 544788649814991247839634963802768579830572098224134627230039033381318898253649200665014753296690032029239393/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^23 + 11122343286364255530260214795802950204189165828506749990803385097165319755648685004278710604559123268805273/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^22 + 1803289520756950645615443739592145162636952309457314358308259070710276410624322649707116619118803417809404709/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^21 - 649117997896458142839829390001994068428105144911545227897952795288714227861751017939346869481488761410167548/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^20 - 3183079308733580249250654917419214269030191461503724984999427759518541891956653079153457547560289897667598749/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^19 + 4617933553539989390620910648828473685504219404376451384462916045739015499084217480860940581984400869751618297/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^18 + 830698304183177228684568805121407408519622643773019681253745774033545189374378754295242169810584559791662164/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^17 - 3464681284952325521640386558279203654993717990248934106911793580899172593495256705959273263823414446203882054/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^16 + 3473158113704889284655178623291374014931059231565412766028722784994762818402782891961475793246628241225283657/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^15 + 2147087876292284240933268062944938592105851446357415272360340234660740281014144009091471250163974237974461681/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^14 - 1206538580702807594851655775984702259906282514073630046753039953061541709948263560797787316144550450759058807/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^13 + 75303052524112107005859711175122945192301133844125039601188570802866275838619837480256751545294936597718271/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^12 + 282093129282367709536615330124108087391136572862329868530566244474068886006262223384168163567890200868097526/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^11 - 91406923244622979332203207533837368724271907504474875900611128219658873000922706962259943337570422276567157/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^10 - 69335281901705176112186135437391811447149979944867298499357386286473834336862801877259245013355338050012567/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^9 + 3801733520376368012078600623009457909870921422741216120586415785779357391220017157816427119794454911734593/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^8 + 2899479875595062411420086354069140931960341692286719999953737374641379223231753845392438211287907440252981/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^7 + 356418001472302660890599973387814947328600926132590753817576623937608217348160396796537177721990444107519/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^6 - 134736037843282678514690279426330460762748452029615027860638089686042131705927576080886953277036619845354/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^5 - 113577613735540034762329679287844876682128112187216464785361802978590735353063007921162802230357032627129/378306231776653449339392984921926492190487064816347508417696573347228841672933402147473031850270122*y^4 - 4454450693752084651557286093282700102954440197017396262045081325646765788716749759787708822442613946127/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^3 + 403053752215944501906883505868274370501231987413896954396860489430571272949543151089013602559837781307/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y^2 + 423194048477226808084879125267484155695683300451804494503253788543780333380263857697501094385119493679/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061*y + 91665369966555966335406384637843821625485059990148762630179362792118655917263876169243217052578045012/189153115888326724669696492460963246095243532408173754208848286673614420836466701073736515925135061

3241327546625182887378084094924398779648567186591577329662642284060109491846010113565408588364820116/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 + 36286377722570887856048905683920899400661082578715949474268123643649783951520593736283037114886289251/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^32 - 213641084368142771844221912124633738797958903489317344879138859261781301634191751639498280355428692785/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^31 - 2068592067029134318018616409484017190973702695548003803998954471007555682662577890768651756618574529997/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^30 + 10771235168807170186871195558823620234077652099822240237424723574488683314323974147198042857083565813395/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^29 + 19698416879563896115895969724730115950976095501312656649812636330042422861340980531654819341432564615912/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^28 - 157919502241260638059436543915310199741288455741790506137477974567129548503286812876322432826056204440841/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^27 - 172043962702625058856003017620515162253927438364957487857446299665844845615891324483278471159148817679200/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^26 + 1451807840983739869517852705226574166194073962617672234008151303061083222286490606569874358901764519722795/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^25 + 654352835180243574054378101845035715393112664005457107850162784241123519885859919661648962859630971640823/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^24 - 8202510975105768610868542729388340395633382386995079728592454226000912472171097330037175584666240976540415/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^23 + 158391904922003128145385594280425663792021185444237643062645804853132997291344175634871918205085770600487/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^22 + 27216294361627666075568839523812853647789263003203526583115143806675174923199461196563885877511568310361861/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^21 - 19054144629074550449811510471367940072677285634539527878228989472270324235167868050721390730909263964160099/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^20 - 24153977626950820778460901450419060733880775236896920723925718862117371895290930007249969439776381693509220/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^19 + 34365910088799550271036704527216943647992077463808923788883958586216009453198291122260446261525246941399700/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^18 + 26045692385472988980366165412345552448988158593181157405492303926514432396194906602278518231241366106625657/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^17 - 51911940856543367205884515887634825443707266968699202379229308343599004774597111586212159020975833527101847/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^16 + 25465869580948756391182565749851007756709137737479507020570845294603901963098302616889687363197367494761695/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^15 + 32695742226851006451485761606469356883667951440377592269661108643582808937133807310288198003440796061037113/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^14 - 35811869992661873152199282136343263132945411625021305896027760027250083873760246943808299401042790005077755/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^13 + 841159517860432466879166147328151839690396348551587019429092683912523890798651700259819980187075884565259/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^12 + 8424953100361285143544512430197125275121238341303064222195478682240145172061914992759596143303361824709029/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^11 - 657251644689643214227258868485306833823597177155081767588044330466842373999116235833567187853088969960657/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^10 - 518905807129051892288884019705347455496470120523470312785234702896394894554715471489303748413922350669025/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^9 + 109554061995771989381114184926355127177365928867639719386177300423439381478726079036875001879021164599803/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^8 + 43056030183262321794609851253103127673122951955395659643039990116353635068118512357888738650551058791929/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^7 + 10727871684317931371901654712476410541465331155447989857852087858994890122535511136214978207076422661623/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^6 - 1968529190537503176486163099895332836319672730462550568593937391786217825999599838228291708402284451167/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^5 - 1686592937009195909408240348948078495073284047363627596912970741932592605675960982811781947456989033301/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^4 - 66470157291212773258830821687808182061632733578063766966778636731624505051175931951517064430644772392/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^3 + 11718547963916379248458221101569773151595083821023371120685839656582357134701933914742257918373595121/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^2 + 12462231596474926541600295444457864951567417604509769821811438334935942940455357210812784302936303183/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y + 1372941739845203564511246753964771219603396178956283516953720797468490903156597201948957158261498653/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659

195418394533343140833851446069444061165476599281411266311015233570712578750213379231726230442534047148/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^33 + 2183981215846842258295846648082788839101067925041786836372532648975237218850002928998573561825167016093/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^32 - 12892666599741596363662553671817085907948425188817753692876586084634753193044637745789494845838190272960/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^31 - 124495635733918215310515669988536135921856826337112699609695804585296394269999944986855347668439078403591/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^30 + 650808565803855458108144850812976319007773278495476015185330965099112020775232536924795140249224850687707/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^29 + 169323065803557006393276706145358839920463459640182380350654187336736319524775085515043981631801449399464/31126462108205663553241194961930660749850201535522263350823135781734018618659077391880692494009567*y^28 - 9548466021169079862129031666965517834430862847807105357742943009588212782016309741232326127183406807392259/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^27 - 795504760799056037267853349601619737954466267749235591702698356432696686097857581954610975729185602694594/16760402673649203451745258825654971172996262365281218727366303882472163871585657057166526727543613*y^26 + 87792375773801358594806936822887726612434510128711586075637828578376627069974810942537725572330453686127639/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^25 + 3013183680111552524806837486357433110091839915150814158288947590014925755192967983441859831681275082939701/16760402673649203451745258825654971172996262365281218727366303882472163871585657057166526727543613*y^24 - 38144397710058187543594662781717268870152162988137515635224197786861828131991306792422672714833130888383959/33520805347298406903490517651309942345992524730562437454732607764944327743171314114333053455087226*y^23 + 12860497632389176539464316441610369896590284789081942517636006408314172089169953366976705888630931650321507/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^22 + 126486519575301909996502193422691936631806641078539576632315051876968116881716291126102433961385542546201611/33520805347298406903490517651309942345992524730562437454732607764944327743171314114333053455087226*y^21 - 1160899671200881603735677264071350859839005581700221425004596887581801354543035131402305993588080002480597013/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^20 - 1457253948921124740005592443836625449477409141859540442994150185026302121536402508507638139296017973942570563/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^19 + 2085001495751098093433113810796075764564618473352999392571616332091459180744828573956662560728707923199942798/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^18 + 1558603073050095478810814745489296636663219074020584415482638678933751546816510705044874789595335320540391473/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^17 - 3144053873899034099810816698148241312411730159930176564037369808220959872439189586803970050731854017355403733/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^16 + 1550279400684834380093723848834873631463725018637671050097739719558941863324269055501113473695105163526702241/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^15 + 1975007139429668262004499911059200869876802477208894893441440314308848068052568343118907186734884819844496141/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^14 - 23903474014426280193720441332587391775458890562008344383966930699660502790369187555511296013802227665457591/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^13 + 7716566859006219935908194583697482776764390052514939773851721692432610568230631886876990471299179277581079/62252924216411327106482389923861321499700403071044526701646271563468037237318154783761384988019134*y^12 + 511572074284037099545441870099559583759442452850884487117850204826596179416968532208099428999508589211432561/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^11 - 40144361239267856565123671915498398256831644408484842022212147678726404052810189116810409350694868344471613/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^10 - 31528852678245773494025276186819362772518629987539553186099380030342449896159982350434734535993386115927768/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^9 + 6686071634418764341088170716107437699147755582865063117340320684761887704088977698852155708039380594722519/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^8 + 2621810041670145919110634354687492079668657553975427769771748552167953483230761307515018087375705654895273/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^7 + 652408718906914066576246409409949873300566392603816509342560894415726690747686232811466369216333238025657/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^6 - 120163007056752361744103409747094822435971548354849413995984636667916321554628996466210010346478299090773/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^5 - 102710464055013869542637796392844805880233267066955617585106366838662879848300552490302546302445910609227/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^4 - 4054035778565383034752016027366624342517520486105101107499545684951134502768398603247500025502497071181/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969*y^3 + 718932907192923846679410539716516245575013680229817256159433410717423444766341089949450169018813948689/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y^2 + 760216839933656019293703728860333551160965083958449030489444890420301310839700660001304628374199195015/435770469514879289745376729467029250497902821497311686911523900944276260661227083486329694916133938*y + 83129917394417449657667097442915525176788333992351515240921903243089638042734588560201074248292137146/217885234757439644872688364733514625248951410748655843455761950472138130330613541743164847458066969

2830895015201756300436204237324030000563864923563274781022068401296186920216954897644906753852129156/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 + 30559129465694953013101330574204624824234185728613131245640294530194114520830262737364555613427929559/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^32 - 190277393845487578380535833757137648390299107771252932239810618206234551891440936867594301486033798386/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^31 - 1738766438564984362454702503740294703195973705640842624662217543371556137647584137885190345663497955143/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^30 + 9830986952549421329400500896459816818761559755195106908985883211976313274566907639563486201185561173323/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^29 + 16457182051035233298145929801845952249916053024220914555382906219154157121169999581561593719927355577288/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^28 - 146177782110479191154668150891181573533496589982061209007138578594034816945815076880332688411845948354383/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^27 - 140242696300344303120251591977792697014474464879738643170217627322030796569751097616017368205281019529081/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^26 + 1346505154051451269099469485783964073094975647381666439790262777065148076712546916455035093595606544657225/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^25 + 480599741123219243548599025083578965823216193758342698783775602169597758827447801546600981239521504368739/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^24 - 7559689916907257200842699481548985980244445707214407400139505911591132820598036347111168077397443454273009/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^23 + 1209838703639576293127586771557600771584523155129120215426780344361243927802259766991309615253155691990085/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^22 + 24727307017876481567297018727627983406176553552423512599713167447925404214812557293902037385103499136469043/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^21 - 20526611845146953699716231387311601154020391706218469191010928830553982374562021480844545045484461280508989/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^20 - 21214938348277785486723821371776331653400634536057263645816181743181342576462204029439115409506874224113961/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^19 + 34138937478019174141242167667806540076378551532471198207197427473452366885299830174260201812212913405234988/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^18 + 18301278332588087888262157736894228706569719261477671818709526305142704169637975150029770708262552594743925/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^17 - 49681700366976397969746214802224863581003337859630470389267322481404222928257921151607281318863870621659466/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^16 + 27347791673384854613679747121221766574577304073786183034645613529661925811677004669198422754289810805708032/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^15 + 29080477854787417592752345247289023603948496784266850726872920861193313110257970838012146876753487865713325/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^14 - 36587515919092698453600755708843587956659754656424331605548595326831396607417597999453817434655856429115851/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^13 + 2125309108104254386400092297954053885332060670710364593524800835986873525415159165923579847504632153145139/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^12 + 8524512380269322085542791084486088460278278571292267374807715765518893712375411969668052039326481827421609/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^11 - 781645355575469627996200495528482551147128987343752394810595747186306448376322098302264738135493705364164/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^10 - 532580591605490385429402901232836916591957934517012265602849246668288988939160081257926418560380047254578/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^9 + 134846807327076157377473176138231512254786024177861415160973187660300831497974724469329127349530642640829/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^8 + 46504825242919899259089645234207578605270629675506964047585720530416281293158602890765450622766453354283/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^7 + 10312882874204377376082474274160860260001066939371514596204722624795964375612829787087393686450308316319/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^6 - 2287271717964356049744285744495372814840641178944491412031875631250099949630404728166013842713616968732/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^5 - 1828417932391957573084471547656833057886108536125997745557849902986298832663817953197092898649921648747/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^4 - 69074492267235885595242773846508636612520498608597719422665182540867917482271934942819662203153305763/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^3 + 15707662689188956969925153555819703888431736283357177728100099942342286671745931394673925766680752963/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^2 + 13923922073353915885544878949707041845364693816130284287361073558861550346893253098234952233764631959/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y + 1469590822275479203440943822499551676104177809014747204251894047821940975277923182469278626868963501/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659

2406433253045260791834864199756766001980338397648747705192251817486861174181675950628908842565906272/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 + 13447297408469164022000927758473761514333298664243003008423029922564501338573702590936977048243287420/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^32 - 158762689218466417377512094950057114942056134357109033195391333197106226351636955522492882428228762435/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^31 - 3066205768799514979717309928756334242396876263199604997067068251296615508233459019140735160314781774199/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^30 + 16028307322509226591501246626484712193661176939259809636203503729491106373856379291695960105583079711105/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^29 + 58384027734890312181308580791167403716265173984257516296281591849112897231991185203921017452726936536905/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^28 - 117582429467561227376961969323884958840227612981238126258093093883979483423548612062475417756107524884177/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^27 - 127354324341277620139757366354621515601763688110703017316981219504085145195454066061185571258250936571977/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^26 + 2162251935405800377581380184732400747946455471162616468455038627499844460813726963370452216997851590273493/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^25 + 1929643746298421727214818818930805810347053245495723312295604784980540398129990088727106100044372374968545/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^24 - 12213538616055436115304317117362485225082395980458224825660056824563702994285757671896611565914281745477941/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^23 + 316235142498411867118295678489418206015675697035365344259524131550925775898762719017243183276650876016789/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^22 + 10125707925332328147581009013213505351613803454476460936402192763139002245698893373089912699317335337843988/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^21 - 7148334988869033595603656379617570075769751040127704806086987403306507886001626018258006156332666173013347/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^20 - 17949976186160588421719571906396025205590562551568225194558801592150947110487452192101703488118258427244984/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^19 + 102721353059948963652171080498256356001939574923802122398622622499256567621759901538063471372214873437154793/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^18 + 19211163574305080586186194624348568871758578694517587414434161659622107587474173330259465718593586604499441/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^17 - 38732859386155502108878264200865341532592773648622349851503578438299810814885871526534648885812978604711708/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^16 + 38172168498108757873435883060061148704737917440195707147423730973319692791027371136108066882964067356877123/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^15 + 48737134631220644305922547490144925522230397285468423731897189017744233282913018212250688274228333339239227/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^14 - 53618033283124830479645607940362602998238319891024156820065474729075467360152413015193486081564851058329725/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^13 + 324019530630785913880197017951771283104041888199178198097739179795170766953066877177598139810848941605864/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^12 + 6315360631574984318124885391822057341633105222924895514250992506532746278779612927633934149392646691720869/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^11 - 987352086661153987366986275985437563919239211833847139852250089290811238356042362578005953533041010681553/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^10 - 1560234207851944189435724404569839986561484546715087151967952608331385751699634129885082517432863569373617/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^9 + 82347459081052895421384272916144642896800433788795598547136397087707447439151158424628228646758545772479/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^8 + 64937095679321259181605476713960864199947131919277387322579515516372446640745731331598536728152737674573/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^7 + 4041255072459209079054855202564974369164168376256824735872091882837830955889822798865786544813147661405/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^6 - 5938244228211768641167273953486324495016583735100916096191268356048075228726359530802962435403468710901/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^5 - 636758726007112708132415912309326515880204541691021007710316429027043483238226953328601284289247245587/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^4 - 101055382788420241846095329309544103143888885457001289900277355711424792071799113742922768805172274513/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^3 + 17768566576212876490617456333314915144531177466038615424479046774620486271536620438894187437778521771/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y^2 + 18779376611184203903667656037069128428259308922211261389595125849935174907654048251139062218991909057/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636*y + 4133086412559364821728726036532852784164769464805542507675796401103342624540656399578786795148488635/9577372956370973400997290757517126384569292780160696415637887932841236498048946889809443844310636

-3589942044076694895186866330903475315321162658791751911409168709959114620180217971017697541563526512/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 - 20053875094816670780626308727370993212091862050188899223172931872877555001846530438051482524898828470/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^32 + 473776764495848725823197441558146857758951372808499925877439584783943591014944408998346075595311439629/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^31 + 1143129942791772658393787499724711138280425063913277590801737087208538284033785678031593589303083890158/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^30 - 11960697477242289387166932840017416172706700639867032112762849958589434435666413965269983169833898400673/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^29 - 43530261995892980792816077988883632480231971520425486211122262247872466409050011779540598062435927903035/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^28 + 87754656870416343760872220043484873799809313902638094720703844857295588266470944847805692316992150920854/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^27 + 379724366436810351827728206897204722234797122698840998278410924076966608214369552546421746112929401797735/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^26 - 806879133777893060324941815671794826523097964731141528243358874265986851137662491263768179105777738870896/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^25 - 1437044899988449615541696467208008150001824646983721006518686245938906164822202019851169827758057231357947/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^24 + 4557314994374476425539348791164534615856402572442624155692104232295228243089108649569816314818677987343836/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^23 - 249171454231704282915508516629371172486047746823220049330977429952423202999583382657291974936531569006397/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^22 - 30220985042064572466011610063833551068016712420565955304442182573118243191746044909794637314044936951009359/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^21 + 21374840803779764959820690324935000439007629492086214356195457138550561116721428624448190091980552669413589/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^20 + 53552372365837824146351003015042571230360855580415461286769891705962598545559549920455177923456064097300213/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^19 - 38357578424237221903592725286466072220073604832908428725475151470218233609091473532036923720894347421484937/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^18 - 14297125844727698799434216853935991547713620423824114984403669588627083377554955512652101097599768361422091/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^17 + 115651442311391966447234259510305192674677194458353565267413744058577288788714792333225349533626307371873387/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^16 - 28537114531189445271969460635107353257445855924158342534534870695488608073311663385571686440247294637306838/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^15 - 18166720620550315413829126385179162316905062413606503158432548839995413847348014924900808656561276396267339/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^14 + 40043345244272394257068063779323799425616875647835852640995017256322277889102834041084973441671765320125603/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^13 - 989877809911712112393612169211618963409652172929782670135493401648604339547909498687190672649162544279277/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^12 - 9426796101054072497984265156293871639216242130891112544168984717889253560626503048999991422743065216726557/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^11 + 1477029016295145953621738525405849888527949971482140240277402364228880038754500295058026276506877592505505/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^10 + 582088573223379495523202363753753250697093363004020832884455511717364551494314021502050097584191036188979/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^9 - 61494190173435957876064353061568154675366427038237873168011443662228923573345591546103247150701123493700/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^8 - 96971397388906779284479270912816647230314431612099531499607133669136129799276002009190558741287832479043/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^7 - 6041112333534622935108902887173828795561726230451185184327938428600732865523777777358903433125176356567/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^6 + 4438140264839046537828493011019162589963891748918831984756302248098362411170426187513933941627884528193/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^5 + 951185222447127283808054458164261013388969248882613185362248400637183239095240439675133597587261642318/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^4 + 151332372006749971411453774426314337659322138725260881023235695680486972003673202067084926305477028993/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^3 - 6647464826468791618087821678233548009730319242450221281870778787413008140470109645189555333576421006/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^2 - 14081553476416975680497571802705964513011087859294020002135336767435092569522912022508957583785062973/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y - 3095832115228579692295550422270742223792172194825579585432628199485962155576645096377804428056476709/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318


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

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

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

# f Combinatorial flattening
{-3, 0, -9, 5, -2, -6, -3}

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

# 1 Loop Invariant
-872784710097100736322563438442512223878703265622697105445656887451898091241915880952294401888401362336/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^33 - 4887867742343691626951695626173728490247347050277189806017734615069903536399095855833129088031443355228/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^32 + 57525752294166824487126972137171146597106648818297295535626469783628189931218506543735072602717098082778/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^31 + 557495407122603952717867767551088247841205053783522387436249941347708552335256993645848732961926120981119/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^30 - 1450187533705311497165780844681761249529352511517732648715602614067775391267250414904835598929942544968518/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^29 - 10625831920681272387517784560299141496539138626651768566728353838881214828094374831646140224220959444233433/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^28 + 21264933610539406746811859037788550613376432162018848204401066563151884332717614207476268785823179199761802/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^27 + 46475835378129491893591603072540825945876985473935424193034190642912254405319454160702497965866732236444752/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^26 - 391181998369333548385690891191660088771555677007273439297828325417085508939251025368121144213863279882082027/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^25 - 177577131120129042193272788702174964569141298222302329632815335203397612331586366591703402367634844291085101/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^24 + 2212410961330898834778729702681259858078868347189713411791894544698651743776056871102794166424218598248746587/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^23 - 28727083053634371276746541969241991361479814945069124019590217664795357078978347128716908930774509796928337/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^22 - 7355911579501095454240414830782284744325381656705839241567584914255093663595816653738169319401641641909319387/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^21 + 5096438525895068987137969617475625361800869967703824402820913277256781577273933844996876568914359799516709903/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^20 + 6558486256184340355719265960942088743482374033592672372797901386210877424071462817755292486922944056182462365/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^19 - 9247636454571679602113647257831468841143948448927103617589851640378313936100322375385567327117920364923771215/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^18 - 3625007166848622645997318220789811889003435112471773154593936829637568517266344197816656658193740684512810307/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^17 + 28099513227823051137391552620901459887172970585942310737880120871649782554705248854074736815222070913843599501/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^16 - 13483995212404865722963942470855799504318822744983380077507724388965683674474959123235001827700451377222525615/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^15 - 9130532031461783943801118387217289864682395350959876606018442394339588880638975534699939516350268911666297923/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^14 + 9696858196939238381821094893349301257224426409880143724388297606731592270220819915621040186042951412943057825/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^13 - 97751022810834685481418468686143754246546500216109932620138092907908107726060917016437306446152256282341759/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^12 - 2335072774895156346535326348241705904558153053841403057048123769055896461346439400555737319045145859526124497/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^11 + 170152003722794613092219227268869310095317190505300138759963856790125182824639810115450567209721306150173526/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^10 + 146601813428159557263443675011768245211178188827732371896767253849915567688305847241378273540307667301115793/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^9 - 14489618779782544266763544493117474957501365204023735706789472355477979841803862882249280667101929637653393/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^8 - 24250481170631868563939209138428515090754393249758134336900174633784056790652861486854438392216073839564185/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^7 - 3058927954518972049293779729555550578964933533801675570949451600529461798859319780739414983367656976531433/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^6 + 1075422189853631011920740063997601985745826837923491806151801087236177647856114141933916765162843573757951/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^5 + 238897925597295454209489017545699758782236952848754994950166815541211205658281042922420942869402350643183/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^4 + 19266298908098939836957391601195668549993078522864079040859686451206227479573034609459667405853935367215/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y^3 - 3256570182595334380272258779887328792294068978189788512317776684941400095161251863100786550284785717271/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318*y^2 - 1723123632543666778865079900736437117595894624674858385296119180213884591229417217430156692476395101700/2394343239092743350249322689379281596142323195040174103909471983210309124512236722452360961077659*y - 786038705235648851958177022917796450737622915208964823746642358625774108598687099801979606598861348655/4788686478185486700498645378758563192284646390080348207818943966420618249024473444904721922155318

# 2 Loop Invariant
316475341766944613526823199854496615607299510807193864355014278867514631424213210847189650236814042445814595354972475990094218902707862713332018885156446180102932123113477915249060745115659878504943997304287484863005433639565/1811359945606238552556881282819172253132436915122112177728918723567983085138332576024286896507473691852427033775876740105301266592580887069268923964359593018309888553045066681308594914506342980933750043725200572553804484844*y^33 + 14163226401781499478621879130725088159704029922772437815852280562236889412096533940452862970762627822364051076582048546954461321160317632697692740536368412145725331964692846348128991152068412603774089737394554440159273541353579/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^32 - 20866800529571604406886780027601198723481924442799474781581554303056300904647441373299109902515950513836090316235915857617919271041668616967739570696259543779432536923684083524410599451546474124373987669153552878658449125025801/1811359945606238552556881282819172253132436915122112177728918723567983085138332576024286896507473691852427033775876740105301266592580887069268923964359593018309888553045066681308594914506342980933750043725200572553804484844*y^31 - 807410665676401895045284766790892590796006546298870089776949756931925343463035160340565136820437388934521573901274932175025855586619296790421402297662800181774912964129621382461067864616670247330352679660105134782488766372157167/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^30 + 4210131186560000740182627515630264430233916030893109446455566829887651483399046076678017688763831631142719266573411770793955833422380057531430362336591970147975112260804965507178008759550075959194007648509689674610106860263575859/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^29 + 23065286309397526565784841053755148921280739368214377555672980885960984198642057926764313462882324861656520183038994289685733694511815106001737975424705816734420641914937750496715282103097577847905419916513460010617748073460583939/21736319347274862630682575393830067037589242981465346132747024682815797021659990912291442758089684302229124405310520881263615199110970644831227087572315116219718662636540800175703138974076115771205000524702406870645653818128*y^28 - 61743204379999969883517986460777005066429925859571776909960314366700131675207325370822949578019923112905660214957535744872145241246263329552946933876141695966214975252431000364928354943845581176216900010269422707196496826263305245/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^27 - 201396213998818543863430315105310710858580194665793669543005147582227121936817008910445071634067667443712506863290361742486746981611723347320067493256738709695561874516653320520683000300528673399491810217638816816029943509464458427/21736319347274862630682575393830067037589242981465346132747024682815797021659990912291442758089684302229124405310520881263615199110970644831227087572315116219718662636540800175703138974076115771205000524702406870645653818128*y^26 + 567675660304751463056687592228320071673240724684904231709833877058242167709833578995708336169523698409201357814706489059475431761679517183276505475734037976441867874948827467916972223859584622627250356910541516120132476630291093445/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^25 + 255018091458015981762359617093915371382456377300762058308498767890615680003751397839424651071880704842630580484890362770384142784745937052423969059108057109024001369560193693604096106983641531791051180991856069263976942830227642523/7245439782424954210227525131276689012529747660488448710915674894271932340553330304097147586029894767409708135103506960421205066370323548277075695857438372073239554212180266725234379658025371923735000174900802290215217939376*y^24 - 3207233456391316694672140213007442849176337049369280523461206947658858118944472784767036396480178992697236481765234472940179104074018929466565717316915467975411060405967033380965251587125854273586308757533462466560690805126882136231/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^23 + 205683450254278048507802679191233714950386714505786338383895730960267925278807052921029600293492373966424832932124056941889931870948037306542306268833980808924802975281848895183017065550177555058656903217204892475738931891887011929/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^22 + 31923113240485242637870041799793645517594391711434260700800053527522810359437593850742461943102592734051269680712929930096562123132326665145971206547428412396997869738483942650960047330344473220014997518322841985186159337176129942901/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^21 - 7468255750743158800144137768170441364745831594839794269078359632081277045127672229557605400381044232149022714572066256411977390432091585552605232434740050177389620068962673236980157382615417551506797892126704541418007129939815725999/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^20 - 4721095069038764473071377712482260460700572621356533209879609514223613066749921253258553066870810721431703395897759328101273465305093425342944254865591808679365154501735576791400146342886883116528848360712522007367412640140972930465/3622719891212477105113762565638344506264873830244224355457837447135966170276665152048573793014947383704854067551753480210602533185161774138537847928719186036619777106090133362617189829012685961867500087450401145107608969688*y^19 + 399633637171541305716593891576716999489167191187425736102431355526995376917525035243159422679211934029154665470662452848881424928843431091979130509037988787698474813828990320196541823639016409456323593267008587521774683568483251291/215211082646285768620619558354753138986032108727379664680663610720948485362970207052390522357323606952763607973371493873897180189217531136942842451211040754650679828084562377977258801723525898724801985393093137333125285328*y^18 + 30510875696981572656046008891712389460710320930544279154169422317562812300080878951195259807917088685833571204881184369009628090367640605367367213335614098578315645011422323789794204824332785628237153987797005142379382286083661040685/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^17 - 30480086508738336486261726679603000829275206818198345203445012972326620064583647649065024343162628421256713552688714899098953436512185543238975161395666867816600584435775851601288588760739747201795182512226295192657205529452528043493/10868159673637431315341287696915033518794621490732673066373512341407898510829995456145721379044842151114562202655260440631807599555485322415613543786157558109859331318270400087851569487038057885602500262351203435322826909064*y^16 + 1869472983605645399395747807766465318857734121673817676539978811871498749744205987782939862763759327887635065153900575470791259367142309237875226510396825805724995619317324080753681776993198829712417177838559947058934206041285200622/1358519959204678914417660962114379189849327686341584133296689042675987313853749432018215172380605268889320275331907555078975949944435665301951692973269694763732416414783800010981446185879757235700312532793900429415353363633*y^15 + 38464541640552888266404507587622734722054365405327216472988504567634880525622745611773259559626243716886441359562609554060650132441549374010001793470851099508064651499375829574297349550822420701611044417363959704828369430747620158251/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^14 - 14037503112510236798692147901924346162854330145306214630312251840896332318675767666278856200754055697687242253771917405083768288805722123518073088625446727570407950789260440514017721375489909040531005227542598995221678723483449788287/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^13 + 962278462865007432498205488361345014866517976915939105478117304906871123561692106039863410635713319516865051695939699832729697834633755237426723402251492676313026410171175561091739047522916826405730863324578284307868007313346489651/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^12 + 3309680896818555687313921026802241569903296832973545559623483780033444507517076424951373804532564825008374742783049217345491789015790517617046583960280569812855077699889214578583269689336464824172001334450782914152883787778926052077/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^11 - 257324220277867743814025766049355813635314959113684805003376670339486407200374733685867364761058974453463470243980137755706582905389381223220411156063270407359801139702936317976767740226735787933074664650173365779425272438058197681/7245439782424954210227525131276689012529747660488448710915674894271932340553330304097147586029894767409708135103506960421205066370323548277075695857438372073239554212180266725234379658025371923735000174900802290215217939376*y^10 - 76623437431824851486559199450292877976641186387378009233599024859787681142664069237686255474295085736926158823597053731867213422755567644744621000933144354878144647704528102087804512840912182360236209531081532910459435645218806749/2717039918409357828835321924228758379698655372683168266593378085351974627707498864036430344761210537778640550663815110157951899888871330603903385946539389527464832829567600021962892371759514471400625065587800858830706727266*y^9 + 129001545671692717926775078431208770750039465447682135553423441186321867330958506135841151978477686290199235687458324994779224991495275136296637352578667346687396004619919137553086630148624143306676607094631700087577113804810419371/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^8 + 25450556490041188234663834596091772500234418260826229790891157254639130721152340572517115098668250701950689062201369095255659740707633418589327263044623948920208854007900088902479711484933608954141326112153611144059975212977787479/10868159673637431315341287696915033518794621490732673066373512341407898510829995456145721379044842151114562202655260440631807599555485322415613543786157558109859331318270400087851569487038057885602500262351203435322826909064*y^7 + 12681706924097938001803776710558841887325068519847954392311868115260069637740322372865343762163583551687607869295465431290644895052259091999767678902826254990443481807957857717014472128414151622435642468405078590084020881978534691/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^6 - 48390970837817521692757308203851394297507871929742603160881075144487200290970415618385703037508784704535659347382769717218439112892996339851427011221366222426756794303485675183440368401285582255226272603426560879199961956020977/452839986401559638139220320704793063283109228780528044432229680891995771284583144006071724126868422963106758443969185026325316648145221767317230991089898254577472138261266670327148728626585745233437510931300143138451121211*y^5 - 1995846665531867302890761513804648899046603772157292412006179343383249199464206362675975394878003108553902138684334637094076396380869861953482238579418492298536129379330648231572132119474333397855992051441979398526379728035263367/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y^4 - 26297933706354281279743450117038589769624091851710152148381185169595417697070315086675943668937901588771932412526084868966882202394457616788831835086640413992771215653031745891482293301643415621854216315219670889516911383637077/7245439782424954210227525131276689012529747660488448710915674894271932340553330304097147586029894767409708135103506960421205066370323548277075695857438372073239554212180266725234379658025371923735000174900802290215217939376*y^3 + 4613829022363032328278447454692604921255202392296347987737525816498488304550899802044534967951817545847976466630345234422171795817341245257298923804691502545460373199091153193408672179637639884860812286728993482109726886278747/14490879564849908420455050262553378025059495320976897421831349788543864681106660608194295172059789534819416270207013920842410132740647096554151391714876744146479108424360533450468759316050743847470000349801604580430435878752*y^2 + 14707564209058881746463336104160035813350170360371337975356011745144881235120923096780437298814793291817110900627144323455730652432278431671944502921475231686575148196868083880437338140640215847370335461271439541956705843107773/43472638694549725261365150787660134075178485962930692265494049365631594043319981824582885516179368604458248810621041762527230398221941289662454175144630232439437325273081600351406277948152231542410001049404813741291307636256*y + 515543075894979479011441401929569753216976974297175273788019447080261618736010586226977676202965782354985700798456713031101265883378202548396818705404477062814236849105004829470048889484518009238989476511133734350280557139891/7245439782424954210227525131276689012529747660488448710915674894271932340553330304097147586029894767409708135103506960421205066370323548277075695857438372073239554212180266725234379658025371923735000174900802290215217939376

# 3 Loop Invariant
-22268663522351512551645381875316607071897875704831129563270911635318077170204645266667132276485531223107375484607524629272525966979564615349074127221062944908065693605289258845241399594682431281255093491194756059596178118302888421706373580427797774588173977794019928961701982188497184823/1575483777901147472503614931950332246963744561655909265450526519932550902962648627717922677120054821955330887192009869140333866586771476471928315095627179973011835026498998765001804255386931276791637925179694110111919904140548597365800101904950359331275538143544388378265248884949413976*y^33 - 999178123227992354034583853389485635868219460228688164658411937694006688691438074658509677855732467152614591170734680521112337329837208035470152440880367179441660359484224549817606966328885194858043936947242351135194950322622082618232083323477181669373298470799221126023646441556654949741/12603870223209179780028919455602657975709956493247274123604212159460407223701189021743381416960438575642647097536078953122670932694171811775426520765017439784094680211991990120014434043095450214333103401437552880895359233124388778926400815239602874650204305148355107026121991079595311808*y^32 + 23463879319560599671411628364997763464943271049378141605569906060017780790436420947014828782749340700383352827842116801744398299141871841369237359572378536416113307685149319838978477523831554484933998899278343641583796252451425588062373225431355024761843176510473629294724165543906392761511/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^31 + 14246044335606076276708604501784805373692647607793846918657332596400803845786299913381399304645622636609863432089033662745636087174351617800452605069013859550771660867144819785197657124810736962697584076337415978200939156251292943407064326875420325421654234444115751620185085400763113454981/3150967555802294945007229863900664493927489123311818530901053039865101805925297255435845354240109643910661774384019738280667733173542952943856630191254359946023670052997997530003608510773862553583275850359388220223839808281097194731600203809900718662551076287088776756530497769898827952*y^30 - 590861752680702217237975765651835254696530525372759244302336011640918185054738900953341582190874590210864179805109087015917809298274746529926581101458294907799781305512013340765143275616129823983181375703170194423390439438789851109396732350724589859193609646249448011866958951869989575780921/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^29 - 2172619682557915322833790234556973586687458882296560221718125684556492854617624794915281372517277075386464020577918488740815259509244060836043529465491618862979932475979702014708675425890007109135552484561329572714130463878864862149853945330240878983156366287304442207979792235774114534970345/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^28 + 1082300220151720443782266864326718994254381616570127490664015433955999271481948987518617306169181098545261522816278158861020183273685737115657169024623841580239611982286302631234556070245503050219880101812388117098652664832142597168525703519362152119056984358908166005827966247766923374260787/3150967555802294945007229863900664493927489123311818530901053039865101805925297255435845354240109643910661774384019738280667733173542952943856630191254359946023670052997997530003608510773862553583275850359388220223839808281097194731600203809900718662551076287088776756530497769898827952*y^27 + 19021599109252942015315504870341357341302953641704787290989438069099512995083710329675150154268417245954593004750046543655948471276824250494308896485135784289043355461832599509335095349593482810367658106324025630047045750173444840504461258314570699599109262297298906320401859748493309099955407/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^26 - 39813294069823841799439026713843056649179558588893182087883527013682878479052296993719539513120294171866388186178870711303486768597438304046425401909954308897355339921880166900350493641524721483340195497107701585847817302738265404772041889707987015492163107062292286215483904098920333919347633/12603870223209179780028919455602657975709956493247274123604212159460407223701189021743381416960438575642647097536078953122670932694171811775426520765017439784094680211991990120014434043095450214333103401437552880895359233124388778926400815239602874650204305148355107026121991079595311808*y^25 - 72934773935711318419278137328363437352842533673399944915665245639923346370043474725257320348735677481656930752844649910246379440668125281880682833106409662440029956986737376957382723008411876992120160967977741506064923856843123495022797711824887090962316770972604231711316220168606199328642065/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^24 + 112605736853416458209119844170364218414849204301796168079318825478902682733998471441913920716114759978221295069582574701797121485640568682123295914890201047041738173465586956192180044936815190977357214688131090720848662486796972415545950666239443649700989205549959496081960449406061533585740611/6301935111604589890014459727801328987854978246623637061802106079730203611850594510871690708480219287821323548768039476561335466347085905887713260382508719892047340105995995060007217021547725107166551700718776440447679616562194389463200407619801437325102152574177553513060995539797655904*y^23 - 3198748154035460170883898526138181266494872983364856807623393932080047505038574209216721818550418428196313740695545349783641869140296180578426446328326934647877897659291531243844797209968211678845235939195577285656295428478449060434599459894079419469114107208844441151924048587417164287983617/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^22 - 1498223601135399575408096541815841593591364831705999609433032199744125658936035361794387704177360695228198321109814284410303501452216923994308201941911314045135980872052099524022483784633504019247277149165289192230359859760563827101129380503427744536594305320600197925553063158420217396061944905/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^21 + 1030194766088004717321477980023753772174372437430207108352343758388270938967026744253739192908406695977135838208157084105618299578394182620548888739158841842753940996654943801225279495758862752116948055762934371980094164913337145738001050487120460209603655528313723635465124481611153426551890769/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^20 + 2674302463085793913195685839401811715152269669269048833112172816994797722216972274081216489336516609311817745089278591117752182360106066696056884684401344539594736657519619366609712189487463616967925215256964212150804665297474755192469480490359724753648099305102663642864552603017369190046141665/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^19 - 469030412455627126351523074269351901660668416166176565488673548851448507904954507066027665487936818420001709275309043415513712380513154736812715162597743839511073328249679527835142660517043641008777172508987353527108249024369356231482951094995002047323902656878075111271168114424436745501363771/3150967555802294945007229863900664493927489123311818530901053039865101805925297255435845354240109643910661774384019738280667733173542952943856630191254359946023670052997997530003608510773862553583275850359388220223839808281097194731600203809900718662551076287088776756530497769898827952*y^18 - 371733846408150626760411607004441729847072267638521061165597100467578562846317082145186041355756024478995585626852845998356651027174479862862175821197460743886503458785087081331815990463827274099417631070296686405070534856156122651419162623439837700034683008806791031299014672099204710710303667/6301935111604589890014459727801328987854978246623637061802106079730203611850594510871690708480219287821323548768039476561335466347085905887713260382508719892047340105995995060007217021547725107166551700718776440447679616562194389463200407619801437325102152574177553513060995539797655904*y^17 + 5707328240325033754582235154707108203266662971044940329347789077226056767496745234177188867155283149910687026031191947351281275050594992017413246642182260587902228559048290330760836562972249933524887299511397198278679320229798671180579371750324963058562854293140458228464003040448432463113522065/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^16 - 1364321240397088660135486033099772669324728022150923510925258650432491258880192649704782806049884734527367377259019909533769537960401285836414984839058949337380674160698217335564507579568104950939381696606273283793409129964093233094061465447853695445630165700135930696168447809568397117262850313/12603870223209179780028919455602657975709956493247274123604212159460407223701189021743381416960438575642647097536078953122670932694171811775426520765017439784094680211991990120014434043095450214333103401437552880895359233124388778926400815239602874650204305148355107026121991079595311808*y^15 - 28961252792585570694865666099408944045656408171708834417206954393342307905343329877945993649198693769113397160614030129021971396352244978513800035207736462384658016002482683653574054489114459872206368061228270861645577822083300904672888796502574150750873883698018978346790668469026036552590223/393870944475286868125903732987583061740936140413977316362631629983137725740662156929480669280013705488832721798002467285083466646692869117982078773906794993252958756624749691250451063846732819197909481294923527527979976035137149341450025476237589832818884535886097094566312221237353494*y^14 + 1961956503383490361195304759870632073214936762033914510391942590705126794560467441092028944497890430994463820590043914756121052025334399322013599627877301714357502068655078837368567112357112583511400946972348778822674788334204156974500186858312006384662898150218759539031597592287460900165038065/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^13 - 19534857417736027521911271651807797418847734660293016257412887247229888066340279899011155320634909899660808254684641998099331602901085497174727935883728740426140981327538083226847387373867541375935906667807809306690857340182470437243156309920905002544594209717295534130496784785626668403095109/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^12 - 470779469821942576081888011253004810380449864519048793461677417261941017479505555148943504874572028652842056344648083652087800445148739862116732597582966982156489098304847275654293049992465358051143100775749049112373843016039102725793714191117834830197930964098750504436301571175121164748366801/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^11 + 68504444658523910710616466513317708020204515037809584824104447938275641983086944704710300444553705456242669481659202108831578947619118762885565516657654149145872252718143133223350523516739507184130635635299304184006353910905919461757577757813515195813284336040802640372462632610662646878400633/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^10 + 459036224651966820154115297108569031526526460358971299633954688581754298560381068249119875652033638865932212917408812787340813893114120828214750153466202198193484355742820704150907866546833903244112261394159488763412400575753281355728199756287799472164778443522411656903340075845666615459826/196935472237643434062951866493791530870468070206988658181315814991568862870331078464740334640006852744416360899001233642541733323346434558991039386953397496626479378312374845625225531923366409598954740647461763763989988017568574670725012738118794916409442267943048547283156110618676747*y^9 - 2867770775298568278043430968256111634575136220443883053512423732698394764542931871386908010160850640095117695092667040714433197698039656103033042609147548285070545981798931109286607827575845929763013879911682394441671284147235549446395427962183807210909242114342872080782235296234225297893639/12603870223209179780028919455602657975709956493247274123604212159460407223701189021743381416960438575642647097536078953122670932694171811775426520765017439784094680211991990120014434043095450214333103401437552880895359233124388778926400815239602874650204305148355107026121991079595311808*y^8 - 4831117147365084076502415516999160255998415206179402200003474773187162293718293017965536754171869375739042992494336624365122016195798394585602535917821395441675514151572749294811642183937438770574040726999654441782422043824349147792687766737016564225010077395930343592605845320314018687224921/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^7 - 312984991819514979403291501650475639259717085932069030321385707888887157660926575871278945440320632719418440836309916832939571515636657009361391838704877301564411307102357698034150522434695740644871207774362303831127419263966021640488662023274493510436985976361659332007449490267647381963027/12603870223209179780028919455602657975709956493247274123604212159460407223701189021743381416960438575642647097536078953122670932694171811775426520765017439784094680211991990120014434043095450214333103401437552880895359233124388778926400815239602874650204305148355107026121991079595311808*y^6 + 212453591874887483857809552023313985695561788522068757685292702918338456515460411246063716349247151061035490107162575177869928755973887881989725702886508703721735757427604608989577938204007451773427316001807912671628269262535655519402941304946580260490177282783882307345728255967205426012127/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^5 + 1492123620328888696283092436911105400058657951484790515308112071099962470870554005255367979736901443217995883526447937379594242719265444254293119670194764138769236814342883377508600362037355386122821108817629133158165010054518679260159134166628807968668349680213795457139449256404540610437/393870944475286868125903732987583061740936140413977316362631629983137725740662156929480669280013705488832721798002467285083466646692869117982078773906794993252958756624749691250451063846732819197909481294923527527979976035137149341450025476237589832818884535886097094566312221237353494*y^4 + 7853368630443638391303499822086062385453048797270813045395052528915215038776674118047089930720057495179017596376111868627141428151016120131903840370929111160828960286125909550705072944744747684666414189468328470115360920702679326895593988876566077569536764968282835427836234098801269800537/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y^3 - 36975186337745347380514425415825748194873964030983625501724092686889482189602202928297054431306285286057850675125632665292702525275664199922430885478595176826938306421428447250515798588514949782324551237667567668697814081391794413039698337351188777782233827234112760917927376614920272655/1575483777901147472503614931950332246963744561655909265450526519932550902962648627717922677120054821955330887192009869140333866586771476471928315095627179973011835026498998765001804255386931276791637925179694110111919904140548597365800101904950359331275538143544388378265248884949413976*y^2 - 682927061630793087055447391386762163409490351923891882614383233104334093655289878579050367106249930419890841966658216500626423031364566181103843810944787976454567916823278934115855583516737712010195594726309621587110361186332847959160500970057108707476207747327471793228410733748921046231/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616*y - 154514497645682393210483975501853755655972775335128791935133751863142320073928650076488000434619169741036247279212537592795854370848664626883721881764894045765838165459831317494191942931747339871909134240225123430205504368068420104322257186330843898473405555873652562238314313279023736649/25207740446418359560057838911205315951419912986494548247208424318920814447402378043486762833920877151285294195072157906245341865388343623550853041530034879568189360423983980240028868086190900428666206802875105761790718466248777557852801630479205749300408610296710214052243982159190623616