# Manifold: Rolfsen Knot 9_15 # Number of Tetrahedra: 11 # Number Field x^19 - 2*x^18 + 12*x^17 - 16*x^16 + 60*x^15 - 32*x^14 + 43*x^13 + 117*x^12 - 116*x^11 + 206*x^10 - 282*x^9 - 322*x^8 + 410*x^7 + 258*x^6 + 751*x^5 + 1246*x^4 + 1029*x^3 + 743*x^2 + 535*x + 241 # Approximate Field Generator -0.694818085873775 - 2.41095192225465*I # Shape Parameters -3524041890977215491448023453/4504930446491782364535294847091*y^18 + 10303029810484756644403592707/4504930446491782364535294847091*y^17 - 53719673360193561368300836910/4504930446491782364535294847091*y^16 + 114678109025363279167708007710/4504930446491782364535294847091*y^15 - 354024915884633273545516010648/4504930446491782364535294847091*y^14 + 543388551261614461602529622310/4504930446491782364535294847091*y^13 - 911939564701614495617094202149/4504930446491782364535294847091*y^12 + 944249691181322060928336508908/4504930446491782364535294847091*y^11 - 1120310845911652321823913098397/4504930446491782364535294847091*y^10 + 1007025014435516048043406738853/4504930446491782364535294847091*y^9 + 26054320792597655662289550855/4504930446491782364535294847091*y^8 + 669540344368953654587889204084/4504930446491782364535294847091*y^7 + 4504687069781288971103683593/4504930446491782364535294847091*y^6 - 3145225917363977427453104365150/4504930446491782364535294847091*y^5 + 1279856367445505833910100313841/4504930446491782364535294847091*y^4 - 7304821216734232813429335308597/4504930446491782364535294847091*y^3 + 2101683353435062877947444538950/4504930446491782364535294847091*y^2 - 300949613317785205746136234120/4504930446491782364535294847091*y + 2388390906097962703999783266031/4504930446491782364535294847091 -31069068986568342629673253307/4504930446491782364535294847091*y^18 + 85381855714399654514608379388/4504930446491782364535294847091*y^17 - 431208813129043879613787182653/4504930446491782364535294847091*y^16 + 802027867868900319798135018194/4504930446491782364535294847091*y^15 - 2376589378304426893941428196096/4504930446491782364535294847091*y^14 + 2581944807814821210724937390325/4504930446491782364535294847091*y^13 - 2713604655332212382594965185235/4504930446491782364535294847091*y^12 - 2397479770024036959538951053251/4504930446491782364535294847091*y^11 + 6528236774136728204449973864975/4504930446491782364535294847091*y^10 - 11675802528860882653116879050173/4504930446491782364535294847091*y^9 + 17146478212046307560635622435898/4504930446491782364535294847091*y^8 - 658886513887950356993970408346/4504930446491782364535294847091*y^7 - 15922897149992031513248448882252/4504930446491782364535294847091*y^6 + 6555398513792785338773006861848/4504930446491782364535294847091*y^5 - 27155744733147331774673462232757/4504930446491782364535294847091*y^4 - 20370270377982335419400659869298/4504930446491782364535294847091*y^3 - 9471398677360233143146851018049/4504930446491782364535294847091*y^2 - 13998000594152664828999610243619/4504930446491782364535294847091*y - 2164753020859552439414528384127/4504930446491782364535294847091 -3524041890977215491448023453/4504930446491782364535294847091*y^18 + 10303029810484756644403592707/4504930446491782364535294847091*y^17 - 53719673360193561368300836910/4504930446491782364535294847091*y^16 + 114678109025363279167708007710/4504930446491782364535294847091*y^15 - 354024915884633273545516010648/4504930446491782364535294847091*y^14 + 543388551261614461602529622310/4504930446491782364535294847091*y^13 - 911939564701614495617094202149/4504930446491782364535294847091*y^12 + 944249691181322060928336508908/4504930446491782364535294847091*y^11 - 1120310845911652321823913098397/4504930446491782364535294847091*y^10 + 1007025014435516048043406738853/4504930446491782364535294847091*y^9 + 26054320792597655662289550855/4504930446491782364535294847091*y^8 + 669540344368953654587889204084/4504930446491782364535294847091*y^7 + 4504687069781288971103683593/4504930446491782364535294847091*y^6 - 3145225917363977427453104365150/4504930446491782364535294847091*y^5 + 1279856367445505833910100313841/4504930446491782364535294847091*y^4 - 7304821216734232813429335308597/4504930446491782364535294847091*y^3 + 2101683353435062877947444538950/4504930446491782364535294847091*y^2 - 300949613317785205746136234120/4504930446491782364535294847091*y + 2388390906097962703999783266031/4504930446491782364535294847091 38866361908287807368435445356737/1085688237604519549853006058148931*y^18 - 114535944392198211655419252338605/1085688237604519549853006058148931*y^17 + 587083168832270400372541388509554/1085688237604519549853006058148931*y^16 - 1208810840275805346305287071333745/1085688237604519549853006058148931*y^15 + 3636889836316882402358240498793329/1085688237604519549853006058148931*y^14 - 4971471919096513185247288727231887/1085688237604519549853006058148931*y^13 + 7249101535109302046975236562989492/1085688237604519549853006058148931*y^12 - 3234501768247823185275943456377840/1085688237604519549853006058148931*y^11 - 419997185935562548861097728015615/1085688237604519549853006058148931*y^10 + 8806354396517727373191706842952418/1085688237604519549853006058148931*y^9 - 20453838530045718891101968329990207/1085688237604519549853006058148931*y^8 + 9058234708186043728925855640957679/1085688237604519549853006058148931*y^7 + 2700242967086913361541122223254675/1085688237604519549853006058148931*y^6 + 6375985655464465057063662252885473/1085688237604519549853006058148931*y^5 + 28149353890905250161747452030568939/1085688237604519549853006058148931*y^4 + 26304027994413793500871400115517287/1085688237604519549853006058148931*y^3 + 21615882711229475791624989124526986/1085688237604519549853006058148931*y^2 + 15156270001409185672750657604054227/1085688237604519549853006058148931*y + 10581660897713602453932647331512077/1085688237604519549853006058148931 -207790441434060114216759748195/4504930446491782364535294847091*y^18 + 600639823432327752928617244776/4504930446491782364535294847091*y^17 - 3033865619614662086027469555694/4504930446491782364535294847091*y^16 + 6041880159389105962668579633624/4504930446491782364535294847091*y^15 - 17916479133330130658936086126119/4504930446491782364535294847091*y^14 + 22727783438722177219827124753332/4504930446491782364535294847091*y^13 - 29499923278454551835111236601883/4504930446491782364535294847091*y^12 + 2260393851639570643091610540636/4504930446491782364535294847091*y^11 + 22054681502252572267670686178744/4504930446491782364535294847091*y^10 - 63237940450713804861697631807193/4504930446491782364535294847091*y^9 + 116027875620694226311143772061650/4504930446491782364535294847091*y^8 - 37244021157134214556917481099373/4504930446491782364535294847091*y^7 - 50559212595549791242659773396389/4504930446491782364535294847091*y^6 - 7651561779147965104254447742102/4504930446491782364535294847091*y^5 - 153799477132965824248482926714907/4504930446491782364535294847091*y^4 - 121991568645848209603172779327307/4504930446491782364535294847091*y^3 - 101655061723593669912172810212800/4504930446491782364535294847091*y^2 - 64577102102996630896897614498093/4504930446491782364535294847091*y - 54744187507041334037725018777065/4504930446491782364535294847091 875500779862891927893960840936/76583817590360300197100012400547*y^18 - 2631900089339299402206812239695/76583817590360300197100012400547*y^17 + 13050975573919524957970226670240/76583817590360300197100012400547*y^16 - 26886902817957588375253888066862/76583817590360300197100012400547*y^15 + 78271323084875003135781555763422/76583817590360300197100012400547*y^14 - 104530422270162825929863230900206/76583817590360300197100012400547*y^13 + 135921672971404260613852219928456/76583817590360300197100012400547*y^12 - 27637770441063891936843015525676/76583817590360300197100012400547*y^11 - 80120440697637266823979811583046/76583817590360300197100012400547*y^10 + 254469980742656191898392881860045/76583817590360300197100012400547*y^9 - 488651319356721302915878522228777/76583817590360300197100012400547*y^8 + 184845449429640535779510506450860/76583817590360300197100012400547*y^7 + 218870465661505701626474913422583/76583817590360300197100012400547*y^6 + 9788341966698624480880918199334/76583817590360300197100012400547*y^5 + 581596622234577484146446199262212/76583817590360300197100012400547*y^4 + 482722037924464404431431298084591/76583817590360300197100012400547*y^3 + 341341776568850447109997097763078/76583817590360300197100012400547*y^2 + 264238309379430399190348404823782/76583817590360300197100012400547*y + 221549879728228714267446356906250/76583817590360300197100012400547 -2379675568653007520695084318331/171187356966687729852341204189458*y^18 + 6480042242362996863963504500429/171187356966687729852341204189458*y^17 - 32655008853613617826091515617141/171187356966687729852341204189458*y^16 + 59884237951567862788325695131687/171187356966687729852341204189458*y^15 - 177573380104726558603713164097961/171187356966687729852341204189458*y^14 + 187129174474439681011705536868457/171187356966687729852341204189458*y^13 - 94902365343820718330580543998206/85593678483343864926170602094729*y^12 - 201814348948530985965615181829461/171187356966687729852341204189458*y^11 + 480341786943059103212394036629251/171187356966687729852341204189458*y^10 - 807164239100215119590239543799765/171187356966687729852341204189458*y^9 + 1122261138278677849896302458438199/171187356966687729852341204189458*y^8 + 163278657442348681421528498143803/171187356966687729852341204189458*y^7 - 1417546474137820269110000349828869/171187356966687729852341204189458*y^6 + 436612296739599248289419178146347/171187356966687729852341204189458*y^5 - 867850731941165007547282827078308/85593678483343864926170602094729*y^4 - 929448244183640494155553625516648/85593678483343864926170602094729*y^3 - 34517347266173636757914793755901/9009860892983564729070589694182*y^2 - 499337948924550871362484315036861/85593678483343864926170602094729*y - 453879990793218799664750416973337/171187356966687729852341204189458 -1308360136711565811842022927525/153167635180720600394200024801094*y^18 + 3699644350114121785688493999119/153167635180720600394200024801094*y^17 - 18731097711719463963560559059603/153167635180720600394200024801094*y^16 + 37039116788524904164564420208191/153167635180720600394200024801094*y^15 - 110395714271107470894228878741401/153167635180720600394200024801094*y^14 + 141087789141971517524933759355357/153167635180720600394200024801094*y^13 - 92599274837319533286141497663457/76583817590360300197100012400547*y^12 + 42794027733862752196737751954411/153167635180720600394200024801094*y^11 + 75943005130929458006364910169137/153167635180720600394200024801094*y^10 - 286911313214323624007939137767835/153167635180720600394200024801094*y^9 + 633918463630403819873084864404009/153167635180720600394200024801094*y^8 - 150667916396607364074196330155207/153167635180720600394200024801094*y^7 - 347423117160538874233680284026277/153167635180720600394200024801094*y^6 - 259872536019134684086696159944725/153167635180720600394200024801094*y^5 - 433122992158658188882330615135553/76583817590360300197100012400547*y^4 - 298010352410049169473703058844973/76583817590360300197100012400547*y^3 - 477894936188364630104732989779969/153167635180720600394200024801094*y^2 - 126234679370645296314624984974160/76583817590360300197100012400547*y + 4323401123483220689294700560975/153167635180720600394200024801094 -13119054447640276423757760231/4504930446491782364535294847091*y^18 - 5620642789684182211772171307/4504930446491782364535294847091*y^17 - 72853192655837019108815350040/4504930446491782364535294847091*y^16 - 192152340757289231583511307764/4504930446491782364535294847091*y^15 - 82744169520830700169478593609/4504930446491782364535294847091*y^14 - 1540388551298377211201706515398/4504930446491782364535294847091*y^13 + 1202857616314235644926065979414/4504930446491782364535294847091*y^12 - 2027552122869845109885787271169/4504930446491782364535294847091*y^11 - 2948877154260643825863731419280/4504930446491782364535294847091*y^10 + 5299946166870446082566970055468/4504930446491782364535294847091*y^9 - 4816326370689709140355356269222/4504930446491782364535294847091*y^8 + 16281232129458714564094617531375/4504930446491782364535294847091*y^7 + 1589885411312652387113179509140/4504930446491782364535294847091*y^6 - 30239554884494893530678328698442/4504930446491782364535294847091*y^5 - 11727620004655311497215072492203/4504930446491782364535294847091*y^4 - 26823234816534169361128318179642/4504930446491782364535294847091*y^3 - 27540865195885465913324053904007/4504930446491782364535294847091*y^2 - 10796407355254570564613709380277/4504930446491782364535294847091*y - 930962631600003984153400283172/4504930446491782364535294847091 -166454966179646194684197451017/9009860892983564729070589694182*y^18 + 584873463287285103223937181383/9009860892983564729070589694182*y^17 - 2911707644086363785677314382553/9009860892983564729070589694182*y^16 + 6828260639530497203574923369893/9009860892983564729070589694182*y^15 - 19848061337583433745548983427169/9009860892983564729070589694182*y^14 + 31763296028362659190892826098055/9009860892983564729070589694182*y^13 - 24654791203445643831620348216236/4504930446491782364535294847091*y^12 + 33671173867432321496118872211573/9009860892983564729070589694182*y^11 - 7083568731933529241234566214809/9009860892983564729070589694182*y^10 - 54476536443369118243773636780647/9009860892983564729070589694182*y^9 + 123863357680357046378386514302601/9009860892983564729070589694182*y^8 - 105895375465908833422223404446043/9009860892983564729070589694182*y^7 + 40580722385347048246832262687249/9009860892983564729070589694182*y^6 + 25387618039499061471828277839243/9009860892983564729070589694182*y^5 - 81065843986824701378746940573353/4504930446491782364535294847091*y^4 - 53318073043296348261709644271756/4504930446491782364535294847091*y^3 - 101339865042541448348181057114987/9009860892983564729070589694182*y^2 - 56235757760146753369226314462819/4504930446491782364535294847091*y - 85017535386430729885598509526995/9009860892983564729070589694182 -74869392304831781805806729479/4504930446491782364535294847091*y^18 + 203723947570100380225027877424/4504930446491782364535294847091*y^17 - 1064795894760373224556130457606/4504930446491782364535294847091*y^16 + 2036366189190179706763358823430/4504930446491782364535294847091*y^15 - 6277893945244759158086529328631/4504930446491782364535294847091*y^14 + 7679862293544519842476003477598/4504930446491782364535294847091*y^13 - 10755946398934878658691820579911/4504930446491782364535294847091*y^12 + 2227996058535407947086248146286/4504930446491782364535294847091*y^11 + 3161831209484487403773424342492/4504930446491782364535294847091*y^10 - 15598796769484060377609893695869/4504930446491782364535294847091*y^9 + 33891974642620629659661337322924/4504930446491782364535294847091*y^8 - 5738316471653952964739770855621/4504930446491782364535294847091*y^7 - 14624516149543390460717155286127/4504930446491782364535294847091*y^6 - 16638966502588179452945430656768/4504930446491782364535294847091*y^5 - 50806692402016025000745803303656/4504930446491782364535294847091*y^4 - 55546135091088386190585195151049/4504930446491782364535294847091*y^3 - 43033332999332665025786801376522/4504930446491782364535294847091*y^2 - 22720970668038568724250599062157/4504930446491782364535294847091*y - 17535593601215798391593772902072/4504930446491782364535294847091 # A Gluing Matrix {{0,0,0,1,1,-1,0,0,-1,0,0},{0,0,0,0,-1,0,0,0,0,0,0},{0,0,0,1,1,-1,0,0,-1,0,0},{1,0,1,0,0,0,1,0,0,1,0},{1,-1,1,0,0,0,2,0,-1,1,1},{-1,0,-1,0,0,1,-1,0,1,-1,0},{0,0,0,1,2,-1,1,0,-2,1,0},{0,0,0,0,0,0,0,1,1,0,0},{-1,0,-1,0,-1,1,-2,1,3,-2,0},{0,0,0,1,1,-1,1,0,-2,1,1},{0,0,0,0,1,0,0,0,0,1,1}} # B Gluing Matrix {{1,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0},{0,0,1,0,0,0,0,0,0,0,0},{0,0,0,1,0,0,0,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0},{0,0,0,0,0,1,0,0,0,0,0},{0,0,0,0,0,0,1,0,0,0,0},{0,0,0,0,0,0,0,1,0,0,0},{0,0,0,0,0,0,0,0,1,0,0},{0,0,0,0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,0,0,0,1}} # nu Gluing Vector {0, 0, 0, 2, 2, -1, 1, 1, -1, 1, 1} # f Combinatorial flattening {1, 0, 0, 1, 0, 1, 0, 1, 0, 1, 0} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 1189979863187089421063412023909/9009860892983564729070589694182*y^18 - 3574412545097303582731654454093/9009860892983564729070589694182*y^17 + 17797641532514303360694954775597/9009860892983564729070589694182*y^16 - 36809166928792556443641800473181/9009860892983564729070589694182*y^15 + 53784238404700107333471562804919/4504930446491782364535294847091*y^14 - 145424743803251498737099747504399/9009860892983564729070589694182*y^13 + 96773782671606264734383081305831/4504930446491782364535294847091*y^12 - 27787422944168306040029815218155/4504930446491782364535294847091*y^11 - 82947782027320003664217218957183/9009860892983564729070589694182*y^10 + 315183025093897510752623389375117/9009860892983564729070589694182*y^9 - 318913045747663404232757626591126/4504930446491782364535294847091*y^8 + 234574405828227166745700382299265/9009860892983564729070589694182*y^7 + 275129875503647939844294505460495/9009860892983564729070589694182*y^6 + 66135330472540366234429046304699/9009860892983564729070589694182*y^5 + 801173425403304292358040136605051/9009860892983564729070589694182*y^4 + 329737764187810212883710279756989/4504930446491782364535294847091*y^3 + 405240555049319958520635813806549/9009860892983564729070589694182*y^2 + 285851557977443225011966844821381/9009860892983564729070589694182*y + 119043925558762177554068816889182/4504930446491782364535294847091 # 2 Loop Invariant -25912121745451160742744049669297850192405889337998138122441583019855308180961/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^18 + 17712497607712353160606090739812812912917838455496393107902533956862943771823/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^17 - 31198087472594306502113239672919263814987712752858534492883369972998995112795/1242153946415314840674283958684349419682325793764115673678998497616009868097091*y^16 + 725053691933716264730159486763915936771158602859715319295224884655470177517313/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^15 - 562854334702550882733146649402476243962211020229816876672234673939395488905605/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^14 + 707439492525068089113374764600569139828825325954414517032837112150875808015766/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^13 - 4135531727830228705971565305037327760650256251076458484900442576608324393322587/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^12 + 217610432582190308661618673972623722565377803662647741655180837820457105383843/2484307892830629681348567917368698839364651587528231347357996995232019736194182*y^11 + 688692016724149375349585098798300639664709690501180460894832523809212690996997/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^10 - 1417881559741023103470965946085094003344180127363821965591782603673613918513640/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^9 + 12729833120576529137494350237194101326251907209539798431412606392385317454038745/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^8 - 819169703527036214364321962779626888281288657392498406253134831740201379732903/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^7 - 711343201699260857572093458483435434933219092972210249613906038632957254878154/3726461839245944522022851876053048259046977381292347021036995492848029604291273*y^6 - 1007302783648636025019038425104322793390778809579061111253369634843959858742077/2484307892830629681348567917368698839364651587528231347357996995232019736194182*y^5 - 20147558138662968375339176639948366287441472692776749617735919076736297317518435/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^4 - 10288091676952660541360940350194952372981680083332709489142627849165420248921713/7452923678491889044045703752106096518093954762584694042073990985696059208582546*y^3 - 13046665410599201704166008608135771215236536919597277747552205791371186331317579/14905847356983778088091407504212193036187909525169388084147981971392118417165092*y^2 - 3490561444064391492504238721497106005140345501943649497789257454854353693536631/4968615785661259362697135834737397678729303175056462694715993990464039472388364*y - 6731510325648309120079320002781259425897375364343743435884544706798352329029723/14905847356983778088091407504212193036187909525169388084147981971392118417165092 # 3 Loop Invariant -401743863728750230119372911479799605959538113085134919908403684796858823479196407249553732983042309/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^18 + 1487621585658460284023892319932192842402329029983522538799246894898034895386684953771563638680887847/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^17 - 13183936577836140085205472606847649364195438823488741512840592385006282548792817380048556112042266097/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^16 + 31604477385768581332396519993655920020758666848218593472301558527704070911024834971712215559094410575/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^15 - 41297776440409763127483322858811577871322324155285795522804298214305154356119140318134303781858822900/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^14 + 133466222291778555451689293208433437734170810096346868334433793743572598646100677727451126473947310127/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^13 - 79279501205703408481545004892480544271647544901541685371072242175880916346018323146526959570489217262/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^12 + 75665348399506018374042409392842041619402403258262400154821090669842534127306027413420948502481571799/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^11 + 74304920248104821461992417644772145602782151638229753669433183977362739302783956185158630072542037289/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^10 - 112368320948206391790508480474836454729725455230841027477580712251761365175315202822204320696699946271/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^9 + 478419212007326795336999645628925007645000046422079796922968553600068979989403760699924029895702518051/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^8 - 321671084634867859774628242570405014881771738577683392278294679647946522333462746077902580395026019479/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^7 - 151321730654440455232223582417346231225326653506048276872491921726305787961495356854069050788510515650/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^6 + 92463390056733700317631985501623656117533847041054135470119731377746398766115006075904553821060746799/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^5 - 129818118242374333035524044031258000419492487003708089323404184891074367680619541153857842914387656401/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^4 - 49709797770207199139426050820437243339635943785171186977838763043459396280574970457528376116630936654/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341*y^3 + 63333472021020773196437383625165143182551435118767919520120640304526235022687006028203631680168570209/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y^2 + 112099826889199497436621894077238719963362222755579556718319516121512497985253249542008457144935507059/1304515025907775488311966105208073662018707348809763029494108604302732676638570513694196977046067256682*y - 14688178590357188749281779675269021021437773749912199821878024648466016547932128388285424610939187614/652257512953887744155983052604036831009353674404881514747054302151366338319285256847098488523033628341 # 4 Loop Invariant -40182048600462551684932852545661102192788671643161153023725491374185289243165976982981478415980804523508401975304201841792847990399369420168710346143/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^18 + 10725180926111081255842145564194988392740135522006979718206185990760566617897419434691426333558318781086506915939731478958231691789460805674922783579/14387866865747631792266503415109702448516096456760009457631474125880921165274301460745795584586804019904196361577730285625074373869794693539183550267280*y^17 - 76638057596483126357413772195081291304767961007130386515979065882598828101768463785824742463056235350785126667085457670411170685571904316524917612151/16186350223966085766299816341998415254580608513855010639835408391616036310933589143339020032660154522392220906774946571328208670603519030231581494050690*y^16 + 113259149495034629488964116725431443242094478579782343079467122485966243798002431400266639888011936359348675497613521221231289667488278113414248299301/12949080179172868613039853073598732203664486811084008511868326713292829048746871314671216026128123617913776725419957257062566936482815224185265195240552*y^15 - 2041483068102877812184080869365812369280342239377194154098002293317443116731991433978020960992876461571659783894268361819825036171643487840107150953753/64745400895864343065199265367993661018322434055420042559341633566464145243734356573356080130640618089568883627099786285312834682414076120926325976202760*y^14 + 1283862532998757281406240622911388917536653957062021126023472815825328617589112452403673685851483032631053347281696118117368965883119847506404052951959/32372700447932171532599632683996830509161217027710021279670816783232072621867178286678040065320309044784441813549893142656417341207038060463162988101380*y^13 - 3448386085587029863647051660523331097413762759477011417799206562952293111016646731669098292156945745115437980615024112601506236922282354151326762381103/43163600597242895376799510245329107345548289370280028372894422377642763495822904382237386753760412059712589084733190856875223121609384080617550650801840*y^12 + 6519530678085732518625167815377973641496333340154899025088526871559974299632857720809263584780944334318460036233907965826859232198594834431202950517809/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^11 - 5137033641396869098308618185719175674520674970509272199675523329974735908610523038881102387822810103806415915892520748665574568653745364872205388473237/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^10 - 10376162393393629726019756057527166800252191591932339548675870186579875971498105485751418510789612595777935993461934750510192299487069230894326683627689/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^9 + 26091137468348790039511976636627353270526556136866915789800417612842432175934239503501726904639091377394482910916126698806180668118865433325351090411897/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^8 - 7294945079232370104395955592016391718078471502183869205050183738219608067482813245309905058456913506246860918896004672914117886042699109614035526609027/64745400895864343065199265367993661018322434055420042559341633566464145243734356573356080130640618089568883627099786285312834682414076120926325976202760*y^7 + 3857931549187908346575368813010170666190632507605302719020333051861020929764355082451699685312714910701000570591405412606851623343417299624612439304919/21581800298621447688399755122664553672774144685140014186447211188821381747911452191118693376880206029856294542366595428437611560804692040308775325400920*y^6 - 11203042145836688987442380766852010191966295185949106453542442818023216907847918798423439252407843778656893126091335574102098795484074176844528391048443/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^5 - 23741778125548845040155893626605014245968837768072776850640357908350761911377250896274988672882516382143448540143462647578564951020877489160688268037191/43163600597242895376799510245329107345548289370280028372894422377642763495822904382237386753760412059712589084733190856875223121609384080617550650801840*y^4 - 9483959649330932605708475101735309304162459668316362959589435668386454832006277854983140614364841635807779118477296180197376830021546894108624272013349/25898160358345737226079706147197464407328973622168017023736653426585658097493742629342432052256247235827553450839914514125133872965630448370530390481104*y^3 - 56636721665178226296334563255885862306756131967127327949845127672562376784472512590987541534623412017865666339566758252997725895010718399677661623523613/129490801791728686130398530735987322036644868110840085118683267132928290487468713146712160261281236179137767254199572570625669364828152241852651952405520*y^2 - 27975940987345058149571646360518746318228158605599522875041048299918814779563869006551879121059294664821263736717415901854613094608512742811872358749289/64745400895864343065199265367993661018322434055420042559341633566464145243734356573356080130640618089568883627099786285312834682414076120926325976202760*y - 4952241115333200514266441136956865687162226309413453554429462173366832708223002158389172923134566815164794476033518079899414852162392080122870766587949/25898160358345737226079706147197464407328973622168017023736653426585658097493742629342432052256247235827553450839914514125133872965630448370530390481104