# Manifold: Census Knot K7_38 # Number of Tetrahedra: 7 # Number Field x^31 + 12*x^30 - 66*x^29 + 324*x^28 - 334*x^27 + 2420*x^26 - 5691*x^25 - 41915*x^24 - 215830*x^23 - 1301681*x^22 - 1733912*x^21 + 3847329*x^20 + 10496163*x^19 + 2844193*x^18 - 13197105*x^17 - 12353265*x^16 + 3387234*x^15 + 8365711*x^14 + 860236*x^13 - 3689377*x^12 - 1497003*x^11 + 982309*x^10 + 937443*x^9 - 76246*x^8 - 304693*x^7 + 19054*x^6 + 44032*x^5 - 8838*x^4 - 732*x^3 + 286*x^2 - 11*x - 1 # Approximate Field Generator -0.896280533853617 + 0.731611376487629*I # Shape Parameters 1330221005414298106035481714303911559465258682096813403601556724964244310595143211806664333181728714806196311464673033288/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^30 + 16159100643785936173544389604056240904701689791134258273025038107558669983134621352074038260653357951227803360200146464727/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^29 - 85403767706154158064091609643143061215961583819893769257156733339510664740889220522066149632835905341451382299710500753872/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^28 + 32186874412643387824984360279799302785397195046903583233428589802322740956616481892937305858939017435370957982507918870355/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^27 - 382824539301991927961459500793825942935840444995191320344564031216915945548158069709761723150670221231930137149899779834092/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^26 + 3164224604104083394649104642618519616733421558845464603894379993863191257853069077893074839078137014179649625948929016558603/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^25 - 7105431347713952281864159799492544610398567178323200986927219134615720037805700618650643157274411362031955165040219164768035/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^24 - 56793627605043993789147561200064013121058766009310293280250922520380127902385750903786859019558915521584824358426677860966807/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^23 - 22732416044797238016067806589080967485879769491644075057061876724745216289220586927370855514415538011629314228660211692528262/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^22 - 253619110853231641147798788154731649880136029273637994024875872222910942348088604319683874893142912172882090725392864278560551/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^21 - 197654855720270568613629168508926547364308001098847610874166448932889231215632344461445526065612451749417463617938719320870425/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^20 + 4733150311919869608192610220124709654844203792287614021024911301599187132183472071213768881383905758382329716453041910784114012/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^19 + 14657063857649869519379749650008577468957485493507445039806294097755258985057770069219135161713389760895100159611672991286210974/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^18 + 5969090054322384628768632839173022161471854980999494241023201614716145226033707489884529901786192035303880171393281425236852822/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^17 - 16638135582473207043091344970838349540482638266146477822325559382904221426299775071693388515055245047356205501697093276100436610/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^16 - 18902769601625774733809131814230400201685667757421113898145902379632578728070343450176013429805643796711492112889109360732327989/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^15 + 1652004782460955537662903808758014628784416477359823123907745858632804805233476679353866749959973584272040866941753985572692989/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^14 + 11349696364630673095723249074314761330579146989846014153276666091545201682269955548668688417774998350597086283216376694130722541/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^13 + 408653467738573708956689488817409684665633128191339488618432352591115102961687481590405930666243835923652992942534260277644829/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^12 - 4457171953445134656869149598446892516090351788478542044939216636492180223815450845388417350100214095673500248638764836833381438/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^11 - 380125111691940516252775944634720180050792887490909750628351740681287200323854953677556963205813958551601031055728891054222123/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^10 + 897354199747455314771521626692871618724860972875615632270703797599592507163311995718990766068426900018507807209606905942600943/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^9 + 106138946071605324346809890886954333675471587705535412030826661727765611836472011729556926388014379139671369036354643188861485/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^8 + 108847618045136774184563683640268244055454124530048707116702089285081855497493327957346854486471700052232211797802929945251011/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^7 - 55268564927320098015178750954923465894517154363695314490452300745830393229749176505545975689778404601891435303740651604634993/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^6 - 687760125101290657015561620213497720096415823816218461960002073174774241996557750340922292133531209937165225050876813087727/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^5 + 52504120492324973805701468921869807552645345472352781123189357693020045111398827756598873870382423926099926430113734685644773/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^4 - 3506295320283334246727481823089290793646513695503838266298972291194174229310482526660176202432466907077819193335443424585985/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^3 - 1425779774649551975999574236496215101457371106372285278723394585086325239496666621296894008941413550807135062428388952130731/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^2 + 134948766291377585619162829995391019544788708836616066580162318823887783821076019993820189025856765988232414613780188917476/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y + 5055694443272773278697722771353205936899124228618069632583147567948321117536625561329421932874878838228987259298706601446/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081 -745073604307960182803381377448321435910565836423620593448020755142044124641795052094672897691682578144586843723364085586545/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^30 - 702763364934111656684252615922213594659069123074569363884600313181680515533152197836165141617377396980269243143098523229349/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^29 + 6683331677980547993126009737380867484735203056714450368200939493746581458223973384937526861890182419395139004647865067562512/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^28 - 17627472240376620894656435308711554905425066702311491092080126887171769106752701327978304898880774407862685240414137744685886/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^27 + 26980992822558151910103727915567609716720693479264672228288788286297889737650752256400658565944477760969057092014101325890615/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^26 - 1753635915911494354799652776091778600260668210447769983161870867624633616500625390182239808380612355835903542050077949680236229/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^25 + 3781157235684324650893082594395457505168136111941964384914542067676975997763064044205742093153298340537275090830216466089725475/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^24 + 32219581154870015796798428138594753759217681359532562315533627881010868299835895122597556733067975610210809849774170565262642612/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^23 + 169243437721077366182375875428139420327260533078558024490763470244658517067068568826329699056805223882388887840863621712725741323/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^22 + 1014151322142538152396485887695364548958389105806597252293056690721014433447214424722955447592339965824692207261911227686653660618/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^21 + 222481216140717658560266026216872220865252258616221695342887308631117127094976962784930185395332501799274578853807866207356176436/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^20 - 2458874192020199056289048376115102443211270332280159452510524255606498134262374225728901764380346056314536352696973508580841353815/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^19 - 8464096211531952541222069160820733459730823382785571648301145385587893392991611086290200102893544669279493446291502182836724843913/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^18 - 4334790606504342030212526675475930876012577680885851179869731150179131363770225617767337813477994030852084721328846698559086673131/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^17 + 8698154279685464439072742217806893498592283875751599688786294403873605520344244898488068790637993841777414918361670530836087491258/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^16 + 11481084588341657192864970663012197592949785624818362693761641823294004892769505714583271299450649956141650399866809413335905995778/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^15 + 481640176559199542502819606038083799830860212043463459890343955405332943497804335168040185334692297799513887271475878693352654119/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^14 - 6107094324602800603300571513542618487801762513154275847743845392184717467097698011117778079004258361059737367551243200099439107160/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^13 - 2239634871301687711008004346974470354257349316142085470379422333104698964887597066051815740363430885839677866892112676942448448489/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^12 + 2162626980247387805859470790073146673402422219740086825465213870524821738209224110879869731140916292684428751670554588395697354275/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^11 + 1681521453525157294933568783449185871923994852778228783465019275015321857546997970824136523178427169992248440091176879204500285833/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^10 - 22440635813197184832200980077979414819098710448655061539541030454361471560736754915673056473452631804253889859957106010762311848/75954935082517418153986166711611343048006103862851715484402539578011159215257726510303371800098163069948445132579722237*y^9 - 774846558924880796678003137837338697280125388051408290513406075434293282525550554391505549357416964243957723912280427514750950222/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^8 - 146025571510981684403921416687661526309517267366777431386181977435017594739528194847963786439658737019813779427180107194531367932/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^7 + 26971337789260174737172790926110540160387841134892138149147850418033566138319137081578237449319474243221956323535760100035703852/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^6 + 5032604444324581309173674136080418113413628735174254362995651378447935992165934503227449813473377249571906849696811357871497341/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^5 - 23586425307695223548094213894787047420731934078458556826899852555733121946011570964533754132089419566923792241299906048908364824/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^4 + 410197136622912503974088051969429755842627497909194030706740953274366206798252133323134104325865654400024773875816690424925011/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^3 + 652879293817031474336028493703243875672328898584940139811208103923754358198337847838480954550731347391794276752659108235648747/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y^2 - 42171799034747592518973459632497347085907035113408816629097240785626325848736549603513651568575894625383416578618934970846425/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081*y - 2845370571066696199761658137877141574912577965436571038242051537293141123091091671759180251012725134968619897257219902605025/987414156072726436001820167250947459624079350217072301297233014514145069798350444633943833401276119909329786723536389081 13794881734461566953697774481707703398401418172990912972168678551026623270164904977732031465464633830865033138182151471/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^30 + 12874034672527008960509483454847371702747693921468796836106827922400350317332044892202009730201306196767403445562287295/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^29 - 888399117287932264303825189933253764933903196289238136156347776924068154968000841219135527365089102943966026968159141273/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^28 + 334714308802195298965600532432889764928513778318798807540901415397234516751807031391110009731992944399301254932087445814/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^27 - 4028220584812639899341602649705305007690821260659103205686994572515906651927512952235892501485883831128862998628756033940/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^26 + 32831580275815438092117629093168296654008404845559115458573439083945319037902678587690240586370407108491281401111466294140/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^25 - 74151448275171851905158077561521464208179673574546339026719143530528013658659698839157720515367928908988636235124962474958/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^24 - 588166772265888722856375735323217910795088227155539832258777720497727163386816808716886376646207810768828941714452136670511/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^23 - 3054800278639439475667833850186044531927775075412994979666613569629193423431963120042137509293896370070432304204552375362761/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^22 - 18357601923323383842853578867804765687464572525807059127493431914265188447005504276418049834900419306801609868514760501531272/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^21 - 26331301686725113478469561916346263791774787010836896489543436075470310777983215177478949669976775059655513526262785002817196/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^20 + 49681374189390855249199501069257537787914492466458341279281267159700027673851233677892310181574279034104123586406887747952494/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^19 + 151505568674029305233585359462217450178932136965823936529271596502402547310571947725147964976366117892682582314316385338947529/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^18 + 59067981102778155165642692476547000858308103973459534135996041105636172485412451190797014912611007304804612526225016040978881/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^17 - 174995136400690552067703426997970105276047581193357179108571095586893028197212593692650761588478833978773996515382869839325790/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^16 - 193998945916109771619128661951811510794404384502544813152935191805041058743393383311587425777027287663050128828130076352690103/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^15 + 21784855614943642479379498394397968253349313117255774860576353305410700018065119133617548719092953618921895838751211917517599/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^14 + 119348333092188547642856273982454450400043634036509320331640804776280896486905546840485737941104773995181413933570632883047969/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^13 + 27793231156685633595701360058795159168354032643337877545538053658606506628344832822488200114141007922083460400610911723558828/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^12 - 47734644898432521923141030820933686052282299898304138645022318835145093830325233632753257086786271270437885661107714571444435/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^11 - 27205941406417339378246213702935807171561738667971917630202507987561541902059682838231077851991135498489694955578783009564846/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^10 + 778393035692100451383645584411835450088634569198430387360974999430355016524978800368614954532588842849609730236918443799161/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^9 + 14432003268414003657814663396941918002366128876462321986769117737533599416193954916999032618273308505150167812920733906931055/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^8 + 846136812257750540403329191419518387927698265944529442968079243208247101333710147967874860300278288290008348834835216191380/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^7 - 4159872382579896737065288095301028693586392430200488129641525114406664077530630269355944215469520461658958488283011698507984/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^6 - 306205608111082386697942547721136603447363263639811836647825772361358632206239430758791417543358810761407984144187215448436/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^5 + 581587638899544824465952807183952149449439922093905662323065040597854743235581666779770370282904781103822105766165475537802/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^4 - 40563208710499606443656827738812901709953215822959961774064936711934156541680980240272199436935832615596402958916574143231/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^3 - 17263341758545049497024081253772150091475590467533767037733462362134861875813307954391439561649620729712917969586283574162/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^2 + 1507730202219648074992710714517519299255189245356675414699589522831853462311175582058011490724117181176311479446340084957/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y + 126416771085583957512372118544174348581141207414704632094276797936917099280481956374477728530789593485919597654114260589/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369 -16320773838754111661283092460238086422422853328650122509304867511466631288148604588261034796175750958772156961730436593/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^30 - 199933734382226577605827729767730742000303294188044818302336988622861750673624761030888134138499516883952414763849275671/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^29 + 1027312787975482036965570716498508178489635575180990947564578136680693237040734775135855686161996371016811850813627149818/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^28 - 386811196910313132496669180595619321156603939424711291907439323731948971953910710992079088357371681220988593717226349687/10850705011788202593426595244515906149715157694693102212057505654001594173608246644329053114299737581421206447511388891*y^27 + 4182939741816990976819327737871896223099504070147952871554903462091985938835609051757494830564145908239235107045987379718/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^26 - 38402599972818944715270099285248377427619715350986810490223708937726169267557650214151057034411606345907270822262870873728/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^25 + 83264020199770371831068612818112906860846268669907657748470235909941706465528721840972354833220593976320218216714617789232/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^24 + 705298020034942250277662413316568934691709776487248529109117138364235684189144350324495873261540102733328865702208724833481/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^23 + 3698410697276882933602207119781403524271748968278129922624621678936484499630369240470526069465666252240607963070632407044702/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^22 + 3165951404631305304134360620877489115290990577832146917161860424865967941115123588230864899781727624191731064074796106870205/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^21 + 33799964625705077561753526448487347661744330403367049725330787001782105087245477925427276743757756773530216382804143711062574/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^20 - 54598682976500440279854239613922004087564331291339095065646698720563851169390933017131388402262482382427507233696077107119716/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^19 - 185489800240816844903335448686635815185182400018435008623088468566390219231318675339324512364038240552708486784782433526041963/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^18 - 92451883500866637785756658261874577217744027775694352976826391268739667638894995467891451917866392036716027051817792194642812/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^17 + 194690889601025912769034492337190590443466931902623975146122007897380062484128813172682906667435662526656999963274482641863222/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^16 + 19425089861996493302396079404555153408415413215954802677039210514017643750407470675196501205302628824344876572797036041632149/10850705011788202593426595244515906149715157694693102212057505654001594173608246644329053114299737581421206447511388891*y^15 + 6199343019508906114186249085361446520157189186846025944912660919426462994678346995221681861165506745916751295592826045398778/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^14 - 139052840376924599677528408415657216524798295773133393934437860695417020479486142453491554882987015804520973495872990109540709/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^13 - 7182763243946363190782792987784342965096324849928196650766888531592165534938842045620108754583404314826738208706863623526786/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^12 + 49282368217107891137924936202696775951462081001973481542832952991772340873028485987280573952842831646881862523548194143574140/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^11 + 5435539694511340620251266308770550349757638193772950503024980450183909847235127349354311672545696906717838758520573941888661/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^10 - 6885724242657257699405965367564731639096427591283378095813077403523345081756611824024983488297229292153877323173711783506804/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^9 - 17725054419588529020681794684947867137032048022346294739219385586945826572367898752231102866535097866947566938576066780697755/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^8 - 3278039927022236484238705450809289958191980608295411038489557027087324378957198625974042075577853988857851578656812237688278/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^7 + 628425702209968065213834832578190743902968340894767322517568162701722816584356946284609034954613707133383714729817159353416/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^6 + 130194963190201774110306781181982408413892501646562626590506568071549304658673248778931468410255824231823951427557787243349/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^5 - 532640597028781940241406117653805250101280594996838483731989144560104627701812056835179238486196959043063864444154048231457/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^4 - 19223988622929132267772049392970509900892938367409927191469360696651906812194330987769666775872616976201469235992488924436/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^3 + 13727586859003460569385528480065340014612952436686857052122623686936409260821312215555699654195887968001888855531555675655/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y^2 - 99169700852782111458845401490177577901231572354958881358826615622354971574382986489143808228033196520282467139171374360/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583*y + 34893452794404599891082457976828848230199209282684892502970127925771679987344784974305573427067697639232344770860096615/141059165153246633714545738178706779946297050031010328756747573502020724256907206376277690485896588558475683817648055583 -64336730137943723767345229366817654333657586707100553755941485055151917961980454955818393151880069606676650449660452454/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^30 - 3143580883305582853852739201387753658934059456551745142587107092098890840660884785915883965156344070685662299219109653031/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^29 + 4077280194946938844436084354222145996502449272472882939820113285533271025080932822722166496559151100226829631220557806253/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^28 - 1535652071793394200036964250310090559488515282146807868145100249265410174969379242210457900332431474440743861422680765316/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^27 + 68685166487919493322614050714733639294234657673563984926548704679037295912967587715397759405824053502717215413907034918519/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^26 - 607632987431934228339732322867539730187955910028257913660461626294397145337724297625065576402556948539937572697681472082881/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^25 + 1333438087944727635686317348602638107831822238832928100663427618902103032752667401290635796003082186167763195755132084105845/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^24 + 11076576094796123921077139640216593686129551805222712227303366781595718924667938007264514443914321137239014641546981504908241/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^23 + 28961337218469625019452180688308044086164117088246003240057571444074231828504214345328405079038726910940598477907797736234643/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^22 + 86851436171561410211397632277048801350887347715300860087486590341456209864495538818247885665433284665473652499983640687296066/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^21 + 260379556285072159850863413323705152140266581665257255539046979026783543172554399894271112451001295511083006829846311599674227/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^20 - 879566877956601382648494201446566373963259428242760212093965045828753174007615659199710357196979606453779549589724930834188521/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^19 - 1446552721971548643297458503137289192710554162858703861972096163929582644223522943993842036758206673912391937533009312014009107/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^18 - 675603285164538613162222671208342839853172415058290273630584808697972090700096348861753613448833566968526176409016957045174727/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^17 + 3118853081167989071769297988060909157818680849219378954702639443195656975536238967144233379450751309119270343435623228039925313/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^16 + 3858252798139666725675968001752962610332082729797578142532168036008678979525540840403721490490349182754966722007841419602605121/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^15 - 54351077346138685082726754559481213361312686715027803097296224552963475674039343485834105575984968663717840443215157390718071/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^14 - 2183596124695556536265941375009846905360566053451122163186199993452645633883265007349531324891184706447561474096126622034210553/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^13 - 693208141949942953039377188846149560988796404541907912392579991601801185460504639015245221989353543126753970084064109264884955/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^12 + 810038543022297494941146809560081841269031987531563975268897592313923520983432973801284635112713261191294640408190280972258017/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^11 + 563791914108856785039490151222239178455002260381436919126352973023269338591751011779416453774416329121914550955804797378284319/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^10 - 33683400268491291746492149558849067981108153150320075733809432807609305017461864047519929451331724668726595915703304407706005/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^9 - 273161056199497800586619313759077018341883003402316524103984105218966148896749645053370770232018730004722974632057562960621139/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^8 - 19421517770604963624069943752917756610552078757320909017360386782966263382963955213074005126072051438146341497882170576384437/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^7 + 5487242449970772590775167222072447170675699479481416468994732672784690024919103026466737779367976923741495065866311737370673/6200402863878972910529482996866232085551518682681772692604288945143768099204712368188030351028421475097832255720793652*y^6 + 827057641887510709392907525477229821096042479130528891375607819787373937964157174892319830101343464267615326896655409579621/6200402863878972910529482996866232085551518682681772692604288945143768099204712368188030351028421475097832255720793652*y^5 - 2329630952376501278443254645602208465517165331767794323071492557089753973423000983808601814235416947896139505873576711465987/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^4 + 191663850670259629873252292981763786127074291557048108361565141620786654535726766653221919235845758541579285477777681800649/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476*y^3 + 134091732677632411893129819214107523836425568067062841458859278554112003933449442978124737321763556984339560101295402029761/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^2 - 536550543698400824690640992980366583555742324881425871600971108809653553368553503438228110402405472380691355368464376893/3100201431939486455264741498433116042775759341340886346302144472571884049602356184094015175514210737548916127860396826*y - 1774802646876358732059178890038425982712392767177087915857714131449677654538714236213718372627145406552762379853344595167/80605237230426647836883278959261017112169742874863045003855756286868985289661260786444394563369479176271819324370317476 8003710947744671414654351410620765869960965179952639291498845226947662102033709641705039767709558526802481099844011133/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^30 + 98060190995642063541493295775732724919825942086212202907214396005259325139661164751169123176781875945092197956742949422/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^29 - 503649862548181993659980274024140321448666345114108378211121937603746323125674566003116490103993524821226017217067949667/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^28 + 189624840144740225852087454127011140179379630824402721154977842605757995319137088956496465229548326200647247959620168940/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^27 - 2046212018892793647971718225702385174779414632639593110683348787157040943241631846243754952951762871708342646554608159589/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^26 + 1447939110565328377862596351881643756913487301226854624162197116376179174610351120441212953972267910828460732273253272610/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^25 - 40785380767398506056362360470433501232664511321383462236823076245184341097434636085709119689032827171686251169225219770074/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^24 - 345982642555450299147113263404481831527635740177565491941505811275351777958963506994023304580848281042513696637268731601913/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^23 - 1814080618821670704699213877000416241604736230525082783717290584096944226524887390027099520860669055317710186544285897697315/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^22 - 10870761744258142565758082822001517208801639607568235626587086768154953761272526847278125122878255987679054678817274435897862/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^21 - 16592244687429435663220156970749460659466323138697299936359866675567615621716839085129168271438370549232304247578225655382363/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^20 + 26753003477598954322830958088223214337092657848902374559071077510521820928509227947970886512210011706503765495300474566329976/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^19 + 90967223623959878917759496950926274988773801643380101179191961034577367408659974019088113517145378050453528972003271527199692/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^18 + 3489440660726779537085958128983648157993909898959137014507204433146749800921063844900932841415742807885172747808361206161351/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^17 - 95363089848141427755304616999518652419017794053075750371368577954554716891475219607627242508567081960146564775814890297130132/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^16 - 123574681323761567442781309138385128250861846817880759584287104612503927697161851024480223579835823323444233545227394813539896/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^15 - 2917200766018167503853875907701422755043587176993193489771485130272418498466218572294935337109493791526318789339603789934244/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^14 + 67850932056225594967706758185943206411974101379743174990108555049836263493859138731601872616442497429789282950939114971787370/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^13 + 24194880633123554871104494902807895137063011045085090220318846306917718065164034692050160344514574383069049086828946595285048/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^12 - 24217264187360620783751945766978467364677104411969730781710233243783621899179673124211979469022372926219115287274648884674931/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^11 - 18449863760498640680456833995929328460155347568230225455795816101024674833173089935996789271551929330503561154558214766141521/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^10 + 3466471123796827002332196185944684920225949050368003931630990867491026621304274117176808960142190525948587111685747923623637/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^9 + 8622650139988023834041739194591192602406398156413680502273378300076683371011032512572269950615797910886651816220150488971989/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^8 + 1547289832212496292412436632859944209119692064699854319987049017598897374730056593254933499411823981588462692171527501513560/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^7 - 2152550733582497951008318329862350546143456073241684965550593888508348422045982418009141188390594197547260634134568090352266/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^6 - 418648095490564114759876885283293284834187028392706156409822572175005493725728840555193005594531352630463360512763439832894/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^5 + 268906682245041008869204803509634513896746217964561426877902006510332423323923142799814078092237747464220880335894095270663/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^4 + 3718176449926791884286858316662481343189513665851458482518324399435887236450544355281991929908527920092980673231514291372/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^3 - 557757402386835933428307647237353713526324653532449386478513008845717080710839774156535334205782743522542126693421295810/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^2 + 204557793797691596008230316069928054815560231200731689302434555012142967438653191793303919554648870945734481418115385376/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y + 54235280951529420698568634811330730733132019890588913594265587652293874068871747938177256381922899852839734079849276541/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369 18028419089315579272310607038819579694801878671097975018406221669857431265380128996601665308246700895461220143720255361/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^30 + 219325156285800599600271590737935539103303318207785331901683354901779271847417209001478613220597044340600266684789033652/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^29 - 1153638930602988403639981138465181592233072596988278417783217333094758487543497438982998309468122579304379798191054574807/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^28 + 434571329886460435166171105608956016540151924508375399597803551507261432372930143733053017720486955955469137416087070996/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^27 - 5082285949655507168568474664441461687546147224964617651099654052439554764199200598592670090930957212471440891074820421031/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^26 + 42767469123868115762807301254566483120022450173742814602039846030862158877340026304019340475268688410830355721020947345268/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^25 - 7346618262853852345386481642654065939684883302010701749728175368756686228318485806915392442386706064443614707949933947094/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^24 - 771625528884817778606875023585715653578500188899197178043133498296415704736370686128070978577478589919957122432341580749509/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^23 - 4018474769970324443830065165695407682364501606400230112263902409512260708884434465290424444119281382386557926257510665737823/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^22 - 24129482903392983103177418301763581885934650200563818630631075036294637373245137701369178501601022803158995315327754624506218/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^21 - 35238180179079126220653102263491676724146254607716547582034751883733677214595423231324396985586846054810578837054551432770383/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^20 + 63621219619306227206991700914876637612142121030973951232790436508243562688989112700327420483277037050218379190777005921073695/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^19 + 199910647093402289087519955121214774384188583188412530203500449558759427722355479063989506878232843185495946162928383423623093/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^18 + 84165393641647009139696427401458058881863062842950063551878600305893663097680542417738715301812786839119142261178555123784750/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^17 - 224770524145003788922690282492281490081194302277905195902241990988020203746244468042524680203531791239301427209191901625855520/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^16 - 260398085891247750076454197108167259073404241034228781220648164231874589891055347539679503945003882473280939506882165286306860/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^15 + 18673765505711896933219164017656474546748894855009427820282469098650805154178656853001282560288277997559785557880265299286147/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^14 + 155015456867609221565292042947066910156714991854882628170623609690712311145635728925692120874526798258622229007312266975209931/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^13 + 41349883219902987168091943361976263430526192834173972303633678308512954374451337988843933313762785821903755065473308002036616/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^12 - 4629215098233140523832820462498019857621441394450836555216283501917933186218743185228468504278128887998303953194030106343239/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^11 - 37205662289213136052157220274833840918976624116386228002090258882560810327259601607023084536148313245498111194969293363546777/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^10 + 11711635247925520538156474080793890473214863866595829992171894058110788716139773908051978075020433354052940335393064915100861/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^9 + 19005950123398487961601799962609582972822394193387937527737584065616401715391455176464481038982028323313796858887099358277667/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^8 + 1765553014847906567630708934129613233494431042368918558812812904722215242783790817090708524803597547060574138085353082193064/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^7 - 5269357354470068374296696309684873833481156699194428889162057654836573900548428287062465338589636215745291089464008797709060/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^6 - 549226697584199930241868851133106660504584504063483006973414639581948812790348602008618561587582903495633704097035628384915/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^5 + 716930156023501878049340197189275003669152798861494463714101878075172920265642016511099726736534925989342375956904503721036/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^4 - 36153778922207018246404957309961482394580806766217600010737672123225936773374437151886767662670753570194545157916716478886/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^3 - 20835364839551448560795881596635578626128048260422422238458612051394420278968938930200042614996959557702564502687066413724/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^2 + 1555624983614633589712787793936794720515589302658163516409807463295830566062472895836230834981204237305249907257290882183/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y + 185047233033045188358185713662720755595232478901144184088381897098175494788240580803853528924220796016124911678010822018/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369 # A Gluing Matrix {{-1,-1,0,0,0,0,0},{-2,1,0,4,2,-2,2},{0,0,0,-1,0,0,0},{0,2,-1,5,2,-2,2},{0,1,0,2,1,0,0},{0,0,0,0,0,0,1},{0,1,0,2,0,-2,3}} # B Gluing Matrix {{1,0,0,0,0,0,0},{0,2,0,0,0,0,2},{0,0,1,0,0,0,0},{0,0,0,1,0,0,2},{0,0,0,0,1,0,0},{0,0,0,0,0,1,2},{0,0,0,0,0,0,4}} # nu Gluing Vector {-1, 2, 0, 3, 1, 2, 4} # f Combinatorial flattening {-7, 10, -5, 0, -9, 0, -2} # f' Combinatorial flattening {2, 0, 0, 0, 0, 4, 0} # 1 Loop Invariant -4718853259637320930164523798548469679923166712527207075377758881815756042010981745279310095414196919898893023163807368663/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^30 - 57544016404723887185532091833770276104412308228284938286783126004013392436492615733804449868647645510046389174663744211199/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^29 + 150124095964877280214692861184624789791158260999896277063512650871023535305840388618900889643708672160157106220449421194054/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^28 - 113120082884387357085568757490722590351054068078327124548814345663766901692050836054948074957781086805666216644495551006305/3100201431939486455264741498433116042775759341340886346302144472571884049602356184094015175514210737548916127860396826*y^27 + 645203643450204240927499875697878399590486707505261236147609430389399388868523444697736902763912288036741633025368535683890/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^26 - 5585124051491596248948261242957129814123538152292316635466574948461315423916970404920446117193138490410614985219428522932964/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^25 + 12342457763379076418439030103795052680073062360452076340540885705287074677582539501788712156717791967406154287591328846122685/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^24 + 202580401309788736783136917985526524278229294554242877277862250666128659660073127139723642007021418295347646257201112488637265/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^23 + 528951179253787422244778244984450626429160982902350373601948288893362087759287947749235311498611926177547820522798246778125571/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^22 + 244167601072279447735541615435742958248904400184435638502361241584475671565287995984517487496714589387814914560435872190183431/1550100715969743227632370749216558021387879670670443173151072236285942024801178092047007587757105368774458063930198413*y^21 + 9417570653901127985884208100891714184432089737658736944301877519600312090466156221355310056979984114797686614180207380881142111/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^20 - 1255265763160398888303736924885044254426439970443653620928456337580493911432067307333200225924560524029553674171112835747661823/3100201431939486455264741498433116042775759341340886346302144472571884049602356184094015175514210737548916127860396826*y^19 - 26350220320626516296052015538075857993389301855189553633511969204774256895232733899150178192201838535777580593423919292847070437/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^18 - 23693734000557652143454074727998578047264524142014882743688637985828043825132123339472707944552715676209125078354964107259258775/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^17 + 28816553505656665187619660102342905982851417652188237509154127055082937308957541908498696200444605192045436504443663510609712007/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^16 + 34762303687021462009180354573997447500585390142904189957256721065364685990180643202402387797642714792435670775375453740031967690/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^15 - 1195618584666491415798486942746582948897843735137508583245191595451312133385163706199354629246099644018253167686618590456513733/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^14 - 19963397052366018880046089021705333933937011263921554322398505364967221729994717068231602881979994020459390809044274974001104670/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^13 - 5941244361918007081871061087199217940434010206224681447007317928299199243540648547883025817479844885146481118248136586289240430/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^12 + 7532920000249838926463769049674909872410215518151917429700280114798325710192114082470476663381653293944939840173695371791347595/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^11 + 10015038123456842062545267686859774475988625689490216622196893372619007890642587310251057233180709241528541307814486687930299857/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^10 - 2665776714600452333780778520346240964168733134168837157183965521786185177279822015155345276879575897570176169451737425177082373/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^9 - 4945218507572223074980374054448265569030062715844576169573732087832315421715042458390803183107822347387471289985297398718971753/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^8 - 611788072526569864061963336665690037451586060583046568730166277799597814708558735218676865711568000282608092742672248508678515/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^7 + 658322614966399835096684067921448667225999989093574213855769063277882834238971975385700066640123377182549269169202607887356125/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^6 + 169347915441136717594325954833590335430504440839041315454298215632079417131311939970939681865351918288228296473385052787216079/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^5 - 173317180646371916137600069784958715002653305496620324361136553690416800783782754899649026701203428211414880546884267432740383/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^4 + 7147813420984367052013745346448009543507272100190816242069544835602516673667584550200951970377287395784038115813061754355765/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y^3 + 2318144008583258239140365479635990294851074711997837569028536755765541451348650663923670325527302803994884399531021056428892/20151309307606661959220819739815254278042435718715761250963939071717246322415315196611098640842369794067954831092579369*y^2 - 319477382072233358744540830808914241041757356760408880897298633326988157856487356109631039655511948722627306557262200311945/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738*y - 26921062601609684501402529686380290650847096257476152784548490283321795459155888387988584308615800950282595030121961986191/40302618615213323918441639479630508556084871437431522501927878143434492644830630393222197281684739588135909662185158738 # 2 Loop Invariant 38242685662737704863439458537980178863059538608731443365839038174536284721695810087806278202838047518371349575795551655068890299105709689112040249339789630557940394063409533611579021679706312494017011791296547093125178101315999/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^30 + 228647961670832140554218629985488194751808263791488082951248116637240147742223317492224071229661396714110448955981929582507069298158621951744598799498791529258783168013040749269071616725277600106699192035458921983963096447121429/842697566438113278568508814003252332888015551765679654260060212630471258484149803610997200272073236591552791141834522035368303602534004518023588761273145769242978132236288543641963664711124537047006531349344376926822822966504648*y^29 - 3817925556752641280207535085116786906162603582303663246322836725798868952716087505360386975408563463356456197109699871589268152295040779031989794039209288849984993492699346659056712756057871607822529039474711226208517908410935289/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^28 + 2878670385616859989674991142319915369361772171286238040838527288199251597425306689592809084681896612540697394320029997676387758041709277387945230862901947213440087420325273895759648133553183822016603372440690635503282058233998303/388937338356052282416234837232270307486776408507236763504643175060217503915761447820460246279418416888408980527000548631708447816554155931395502505202990355035220676416748558603983229866672863252464552930466635504687456753771376*y^27 - 19771270623306667558827070278791446176131551933622313788928474819896306899325303589052241192047748004219554254292965729632225659219744675125111282450221180212058152251305050162936655462050248341093043292747005689694497419164897075/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^26 + 92519871183387661720252076697430621513294196013959871111446803513902299437322049452397217273717852835092332604837001065122007328466707492390141447653974455335227967749582419131008812065992802439846868651665385023299812911348072593/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^25 - 331674032121624594380617291612116359995065385338675504748175372791863111438355901128901661367489233814439750218541328227576262495594837736123500502335850931744269050788882444553331274220198208090653370642084456720622152619460285277/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^24 - 184397757642349442323626280180377311520237539994164682462449282817169946582715848694116865148209498055533431440507651106314955308737209502021047974961403244575150665684894017671503508421565347825563910526770955443881707530688615255/194468669178026141208117418616135153743388204253618381752321587530108751957880723910230123139709208444204490263500274315854223908277077965697751252601495177517610338208374279301991614933336431626232276465233317752343728376885688*y^23 - 12265468875485112436316538805509881842158318894091287721728821641681677751627677108648612602243243681350787919722731716781225203183350605942190480708948293965455323146923196004036951466983057838762121147274813332087487978324206110893/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^22 - 148048119442384809249979588912747842275877276908564249653532631369377588748586262719417545957375214744645826580638535024280365180427712602229159742199747877999161096418266689363169140378252010415390879883122117391103482684741205179793/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^21 - 191325074311944548920721384446739514917895713238351911715829443696669147837511609655439780013055822108093370941173897628703297860490005730947830329042446308208007402418634350198930644824959953066198787583387785342186281696244648816763/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^20 + 76255115746150476352729262888748404300620610613447081571672984959731427504699108011385885098322331794446126484458239375704008540409113067824620192932223430786586164000796158048964787691788042898487156667941967109138255189790896560409/842697566438113278568508814003252332888015551765679654260060212630471258484149803610997200272073236591552791141834522035368303602534004518023588761273145769242978132236288543641963664711124537047006531349344376926822822966504648*y^19 + 1197803134572330967469709988574543880935362231245615763247008677385618207956448212350397566322524166295650425808813237353688137657915394642667252556960114243733025189949929152716185486756143891729450805049999221690134010547046642414761/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^18 + 257684977403514162076150253392655197668242058391146930350342956235030221913157085624170541499530314180603579080008497282552067380399145525480500887780133508224301495869579425308919198235369825751835786572057878821575839049391395149499/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^17 - 530978847622883040082031641996884011910546481966700194666581976324266871179663928743280219043107944496606663928766444509114911726127112613358216247954052780356622936644220583075615288423531859162387367332653753072352150840237951300971/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^16 - 1390317832247101179917804529505659186819726803066190234612342612259857352402226041110253509254846208099751602420773399422924000135742177753820240067529690967897669936231086395189901617382122214166619140881855949198307170334558970379815/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^15 + 255960561863348486007388182659612918205303351233924519687269871612660120481032507873067800795920448564750291699981805534227363732264381467509067193265540445801548278239349311575782425063570700949216866839159844518714258879432996291555/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^14 + 1034561760680571184230180833428728965556393306195290564937989596090530484885867560468441819646391316747799001813129140899674452815227216145295779393779563379732622790498765937572947440420854885462266014350869398458094326908545513674235/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^13 + 67704296196774057548644167332197759823637118975873595362425805587869635332698628366012865013427375044129475640837632013100163859571747607978924781413607148781243737957550126114197760116335245441083928974591925346063846690677142991077/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^12 - 157831728741932820625087521900981690076324684552783476978359523998440410639299397001628820620293501342911502175700982666984679136587002265658895996174885357787590435524536137835161402007677109731866544045479001928914301884276229628145/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^11 - 58046223503590167349527272365430374369608840765217863534491178826969123373073237719292583219441389452371038333133199787577715552669196887881756916039904612922153655035156276082975545908247753791760755114588532302424036716652522175775/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^10 + 5630656253796850529985202703681850976147735621830588773724079213751156942813576729000375144450369727338975279728406513462271478231551922581487292896160694896355843362201667953218858601697301338437984181817360540460864248820131386599/210674391609528319642127203500813083222003887941419913565015053157617814621037450902749300068018309147888197785458630508842075900633501129505897190318286442310744533059072135910490916177781134261751632837336094231705705741626162*y^9 + 116728956244729893911446700410664379737012741470025372392503111286055449606570575048283799209099358484291461028959276666262893354758416198323232975336633489154395738437914357272788142495752342452976005266718534932809512462836217129421/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^8 - 3646300067075079435418935568975386987634268224597529584999163757831823709173876894654798102474888541065902735828628611079410194211973325254981861502601877235669140766739875275336677595367955125083262524325627349591816360113544685975/1264046349657169917852763221004878499332023327648519481390090318945706887726224705416495800408109854887329186712751783053052455403801006777035383141909718653864467198354432815462945497066686805570509797024016565390234234449756972*y^7 - 40631671439636994509285954891683836565570707866864362460599878619098783449237034461851011336639789794959421816368682704297391931510887517273061201846919087022779588280169692433886110246499782581621553242821912326800125172767328337283/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888*y^6 + 1065311061914437129381717117401649707041011982439438514440407543886729448196276454606945941093103156195092390558779779209318580367260558256958747271082669932324180601905990348727157056449638581976090807432065162296866634130472368891/2528092699314339835705526442009756998664046655297038962780180637891413775452449410832991600816219709774658373425503566106104910807602013554070766283819437307728934396708865630925890994133373611141019594048033130780468468899513944*y^5 + 121483549583958785197764314353783108336710437906596882768581098959266973506921367374059005910134176610570701659099788967734269202666504819728378514630580165851829147368857368883651965851706038870919161345288541447362915168052717683/97234334589013070604058709308067576871694102126809190876160793765054375978940361955115061569854604222102245131750137157927111954138538982848875626300747588758805169104187139650995807466668215813116138232616658876171864188442844*y^4 - 35344373785536622602410624412783728289692970114329829804308355664602694980513824736683472629743237888596560872524952949041350904842796325772231256085583338696925819144190053955847186638103119554917846403443730926900491084717992703/210674391609528319642127203500813083222003887941419913565015053157617814621037450902749300068018309147888197785458630508842075900633501129505897190318286442310744533059072135910490916177781134261751632837336094231705705741626162*y^3 - 66702128338918836106629676859820707506510319610654440041462170841950356632977678415311479800448212376827931141694423346538408719884987229344028741178139379327139847113400131965678735436634559268599821509254457823532236600925009833/1685395132876226557137017628006504665776031103531359308520120425260942516968299607221994400544146473183105582283669044070736607205068009036047177522546291538485956264472577087283927329422249074094013062698688753853645645933009296*y^2 + 3010935741549976323741112147074390081273694828368838596657155335033149257243794635211997473425130957897056921954305136944741329977596475894266414626922301131494536349685352701470031621056347950777793312573073179451554195364058701/632023174828584958926381610502439249666011663824259740695045159472853443863112352708247900204054927443664593356375891526526227701900503388517691570954859326932233599177216407731472748533343402785254898512008282695117117224878486*y + 7670997740922838398533731862467279718966798142509586371760563386443796713932310056015449994511551872589695019645392909958318031966949375763854966421917403248843860100763181849615529962884696174633579913824747565321617484641442211/5056185398628679671411052884019513997328093310594077925560361275782827550904898821665983201632439419549316746851007132212209821615204027108141532567638874615457868793417731261851781988266747222282039188096066261560936937799027888 # 3 Loop Invariant 604786741975302480570613134294778538621426775242468039568947907992853818547261799093630843145609226248607825736608112379534724679491395862929213459062999926609724174524184378382546296700592382169324455256674360040219214527505956273350346556476315085278636375330862844183416864752797/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^30 + 1839917216642603502102996391958796803012402920245125161426190559937127642699326865343027116978810158449013342097132869530864669169431061841988064842993180895652856797284721617971823617326214544907166980676638255101090855646962395822700337704767369757456469789437549406646181090301309/3853372354067338326348886721955170639855203006896280544011393610303730634048478623103989927292728087592673213043132909149210591590134608930451958401163169392915317368459304183718067086681083292646248403203314483226218713436065318182295668090027902393481469745463703436810199709190928*y^29 - 38674035536871815724270276544316372780235246082407744867118198547407508527024042683757918688381489512129663860572406955318091183152699219573142346923037388924563834229498151673784760353954930253604118506294530708569203065806096226714415441464884604660177587141423327851079768468018475/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^28 + 14568254584784449268472269196775538465678542832772223998425944851245580833779546099709829053832950916809634203906605759146516563826541433383450108532614869044890918527600272970249111744076245775326819525798607145073597132178768696670618049346745563900351545537515220098737306214018817/1185653032020719485030426683678514043032370155968086321234274957016532502784147268647381516090070180797745604013271664353603258950810648901677525661896359813204713036449016671913251411286487166968076431754865994838836527211097020979167897873854739197994298383219601057480061448981824*y^27 - 169857817153959279947623587045895884290089286737220197772230783677296610311820899285374636792998136543962038081328644694309047640170073788565853592931105679431718739053273764782606061003953585522443599479123080262604807926423598374812992830203875560537276131269763368793378656089542451/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^26 + 1434243620880539278980970265612047569193563423212289601663318026608258619314640946030368050183118409073820397773464322186719119390393922274869420005395779813879061711130569786239499062680106923294852949943077323845338301664659126968840881600228284107209287975983505049082243087254942095/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^25 - 399874130439434320992099424169904620193762967659399934964131016421379238868329811599267176447332455963104889275682284569771986425042557326363269594864509327782026389708718773027267438931197146426508399972793887198600636866231739067454473042925974047095070691292433833527263992102667621/1926686177033669163174443360977585319927601503448140272005696805151865317024239311551994963646364043796336606521566454574605295795067304465225979200581584696457658684229652091859033543340541646323124201601657241613109356718032659091147834045013951196740734872731851718405099854595464*y^24 - 1991943887502978029656873422228936753119312586486403262499037006169900202480206515772898567802574804178156108287932355741604214560432142201344701675147980033787893979264872211770743492834150069258114421190632621522697638309334953000937528180953667337752795844495221181904142730280783749/1185653032020719485030426683678514043032370155968086321234274957016532502784147268647381516090070180797745604013271664353603258950810648901677525661896359813204713036449016671913251411286487166968076431754865994838836527211097020979167897873854739197994298383219601057480061448981824*y^23 - 8431150489728112233188959318239298610893642951009858156011031651689406234702051698552707209365759354014035310569785551694436828297243498394697702374643616325183105621942923374259605039177644930131723467892884417931223210061770254457178283598080288782295858675859745438626162946462740285/963343088516834581587221680488792659963800751724070136002848402575932658512119655775997481823182021898168303260783227287302647897533652232612989600290792348228829342114826045929516771670270823161562100800828620806554678359016329545573917022506975598370367436365925859202549927297732*y^22 - 101243443131338764684713511983785014355711573719509166083212837148997950639616409263321838871517138062332690475926798094033759963125981810219681343870928959005054775410744403440907247559250230737031519863534548626382020012465377879590682218649968266770762710489941640663216459597548478097/1926686177033669163174443360977585319927601503448140272005696805151865317024239311551994963646364043796336606521566454574605295795067304465225979200581584696457658684229652091859033543340541646323124201601657241613109356718032659091147834045013951196740734872731851718405099854595464*y^21 - 592526709291021046973071983160619139059986994790748638860813709970442820033921679556717999079454453057218474740562572757000086228902108116036986049902046149066982136110198073004309906083748915216063921811042562156378856306703822926734603311924888495221425326737782310963117384657640734607/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856*y^20 + 2129488181263160654074119988810781272376741748110911468926437407625323656692875825225944363545797917741544847442436243909841101978622299739311795390064153114207043421054213397794279818705618194496982933417490953440361057127123975608426349914457912873220040562811974936263382966238997019703/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^19 + 6712887114342745683916340473481053958575634040668526474773438614015398627678486454996407607597592942931702609279637711011377285970855659714167222464729601296817314772527908609240050997175600162090618297227371646206971385049097992115318052541134506618345036066974825894941613465716793472129/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^18 + 356085492917744227495124494928943713851349768325052926555366139870864564864462699036314766524047327591005089277420167828491005414057722331788412675446588610187866005836598314481875859333968412146344471200737386724685857997290179636520493778409903630964507295512773968832466310639468051779/1926686177033669163174443360977585319927601503448140272005696805151865317024239311551994963646364043796336606521566454574605295795067304465225979200581584696457658684229652091859033543340541646323124201601657241613109356718032659091147834045013951196740734872731851718405099854595464*y^17 - 3762627896143912397739951363770013454345644330978322178314735263109260692302438141845678394881560379754631119369018294617808618650432552806838731218915003015416647481853352244067600458752887414131167703201873180234305700192122253657200273552777616865684228418751732782386178260696825347813/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856*y^16 - 2189986066051946396745593099309761513652149677899657241071417198253615086764900315291830310937775681191526954652905238319077045701764948472954237520994909517939649763447421613334627823197440748461029507666907987041641721999108430951487551762441129947592147353018544209501644006736950676161/3853372354067338326348886721955170639855203006896280544011393610303730634048478623103989927292728087592673213043132909149210591590134608930451958401163169392915317368459304183718067086681083292646248403203314483226218713436065318182295668090027902393481469745463703436810199709190928*y^15 + 589902616561661530476424270953522727812978916488347099746096459968395510846891976447679426638717749385015944124361893422449426621406530959775509913063133225801961466675872355940713245501828739357979240414494374642986445273701185562352610334549664212778824555172895929036522081806448521753/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^14 + 5195790833633669565716433492553394761747303120103476581404409505086618686470768015281338488365181304829869515340886213362114872531784381479052840059373124958976620087280456632587161746530763461371881025580492432011034405895978257765870775030770902748054595575212540953418487486997203446115/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^13 + 21966785167106614088706444963263485003276020974766320526506004043042974088381737759641528143644649669079717997178890572644356540054735780051467362914381945163585433810835746129420832135020434177748913110287516449163663711603623377783576374735352492319727759850571977878922332679697817544/240835772129208645396805420122198164990950187931017534000712100643983164628029913943999370455795505474542075815195806821825661974383413058153247400072698087057207335528706511482379192917567705790390525200207155201638669589754082386393479255626743899592591859091481464800637481824433*y^12 - 2009907067611527165720761092262155270287829342163721226900836028861890078014419487692579141131308294973175562691294970934811661206999164259962050041391321964327619709775020329268923527017708652433096357363702844350855870553060886073834479972370097994725576299369662713259505207609238357675/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^11 - 626924540119612656910072997769880532085851389452003416542419763142751816708852775237884366092108703074977400188459658089844941685224310408722407774312554607828114161608055291236250271925434442243288535081313183747589813987988810788958595930116529209233806686501008656298551626914381454747/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856*y^10 + 387147241362778799101979560498490137851876716319072903298113312770782856055576808343729032643597809644725341871396032160004388260597621714335328570494382193593691483775819659425134749234313345819404052556319160623644164449151509588840112312676127048591238278058395539105806535330723986779/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^9 + 637960341813452629828091531252746443053505101370663995360794376254767855447828478244975337195582585363018600185327735973217591281163996261578134393463139466081408669979750482088646858835776968677410068915100069509446685156406888946530610313015695583482535272675758508068236745110244891261/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^8 + 30837696459414265351403140897422238523320429639547962083161064569168459413145843997177663801934730288986861101225618442446466770198344097565980601236680289466038798107344992656745902718945457106395104881011218845627297672651859935431893538133418727598254833142928821722881180925299250691/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856*y^7 - 88026081743652956909861764215697042809320360444530708836727769342224167010133355935220148232441158021877931924672675535366972139791308481738754817685073317284332375261878309300447509761783182915995195342631023434392235317015592704447711125877402665779738682378354276942864097060682797947/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856*y^6 - 4738405474876028579047137100852301255639554820451737512071780358398358809541250630719518207504785424876647120145564140190865342894200429669124373783223810386068306372669624221647057148542946421316205924718353472800975514466923251349413146903098860466698677120587398797045663994626200437/3853372354067338326348886721955170639855203006896280544011393610303730634048478623103989927292728087592673213043132909149210591590134608930451958401163169392915317368459304183718067086681083292646248403203314483226218713436065318182295668090027902393481469745463703436810199709190928*y^5 + 1835838989446892631305164138283871055082890382137648629675260446214931357867667174317514474281584291732926487535634174490395534903100853148116561050061188676087729024973443273609812306369065311487197521295275383483015504582949055556381692334768191914457864649637493273798472577634720639/1185653032020719485030426683678514043032370155968086321234274957016532502784147268647381516090070180797745604013271664353603258950810648901677525661896359813204713036449016671913251411286487166968076431754865994838836527211097020979167897873854739197994298383219601057480061448981824*y^4 - 289994489809923391148921047170601819410918658190074948276754876706287672072556312930093001743294837180158023332406984790966240586756639502685480438332729125316407070686395192377319028028680607077881389935354410578024896882503234852502854356173141881878559318182433079151912167495384477/3853372354067338326348886721955170639855203006896280544011393610303730634048478623103989927292728087592673213043132909149210591590134608930451958401163169392915317368459304183718067086681083292646248403203314483226218713436065318182295668090027902393481469745463703436810199709190928*y^3 - 694048818999062038419245327644934880669673354363079303195176047664098993637646846699250856571971400993992564018081926756825512255427337613563225835287774568984680945599623906728176053465671678580128933902591049987149792034422527606014043080885631516964585994829217765545915585858926757/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y^2 + 51612112272781489241483659153884904834368541528175013757223327718944942361437769648566399461270535786798035758088185941537619519957544318847038564091084793378047850461767885697641800158155785228885381317691361030088765580555340091725797184460161254964223922203956367822055051730488549/15413489416269353305395546887820682559420812027585122176045574441214922536193914492415959709170912350370692852172531636596842366360538435721807833604652677571661269473837216734872268346724333170584993612813257932904874853744261272729182672360111609573925878981854813747240798836763712*y + 1904352808298750815145678751893305586760723066606068722824541637137192308380467248049487773088178187943055228927995629372793579303656653749323931250771141659578104511130274935947674636071328777660203447200271702759101694527632742298163592920214449997951207814461064142458416036100383/7706744708134676652697773443910341279710406013792561088022787220607461268096957246207979854585456175185346426086265818298421183180269217860903916802326338785830634736918608367436134173362166585292496806406628966452437426872130636364591336180055804786962939490927406873620399418381856