# Manifold: Census Knot K7_22

# Number of Tetrahedra: 7

# Number Field
x^24 - 7*x^23 - 76*x^22 + 361*x^21 + 370*x^20 - 3053*x^19 + 2478*x^18 + 8220*x^17 - 3894*x^16 - 29530*x^15 - 12126*x^14 + 70456*x^13 + 36915*x^12 - 102248*x^11 - 16592*x^10 + 84699*x^9 - 14750*x^8 - 31711*x^7 + 11782*x^6 + 3985*x^5 - 1952*x^4 - 217*x^3 + 108*x^2 + 9*x - 1 

# Approximate Field Generator
0.433825892285090 - 0.143227156553575*I

# Shape Parameters
-9056020221765282150844226988421796508666500195175764900816/59947620076676354677931620854149363289912815578372046638627*y^23 + 55815537785989715119673877312684776703828655734924967755766/59947620076676354677931620854149363289912815578372046638627*y^22 + 738555088728269371324875641551237639170303069642849979345504/59947620076676354677931620854149363289912815578372046638627*y^21 - 2675800186023597422254935003646930977648730493448161980062261/59947620076676354677931620854149363289912815578372046638627*y^20 - 5867457262225479944351185201303886150815093815274266789789042/59947620076676354677931620854149363289912815578372046638627*y^19 + 23979860176992499011179941462190290083208317575425054544966245/59947620076676354677931620854149363289912815578372046638627*y^18 - 833703576149910643532030097573213350586107533813331183281386/59947620076676354677931620854149363289912815578372046638627*y^17 - 85659825017554113169808173780747682243730958360739436515723689/59947620076676354677931620854149363289912815578372046638627*y^16 - 29384899619241631306919725275336717988490706159155334372751003/59947620076676354677931620854149363289912815578372046638627*y^15 + 272478956479924175248829185163828993143049191436103627993376825/59947620076676354677931620854149363289912815578372046638627*y^14 + 330575114988132774810061522921971496367949259623073503104756490/59947620076676354677931620854149363289912815578372046638627*y^13 - 465349330017591175792716694788573540271903126482927736340617384/59947620076676354677931620854149363289912815578372046638627*y^12 - 788983353893063485795569357624276208769365858534227726814304939/59947620076676354677931620854149363289912815578372046638627*y^11 + 492929078236471209114053706393132271610908384867556696247053723/59947620076676354677931620854149363289912815578372046638627*y^10 + 732305665308318836892382384155251637545519900832774408448169107/59947620076676354677931620854149363289912815578372046638627*y^9 - 459184145020455246651301634064398159248956806780165136155610594/59947620076676354677931620854149363289912815578372046638627*y^8 - 348829698298411576557935330859789209809999071186545519193080687/59947620076676354677931620854149363289912815578372046638627*y^7 + 241269073832006668702904569707929544888726073564066285637913122/59947620076676354677931620854149363289912815578372046638627*y^6 + 78078771962446406607509466055451848403750078098099290933576919/59947620076676354677931620854149363289912815578372046638627*y^5 - 56172381409763472549768839918441184160522132905146373763393263/59947620076676354677931620854149363289912815578372046638627*y^4 - 6266406137119457820589383201992051981980522460909440615791577/59947620076676354677931620854149363289912815578372046638627*y^3 + 4399485604518485775605262183559135682885033192869407465979192/59947620076676354677931620854149363289912815578372046638627*y^2 + 417673433290302455186876978181937966757545229096349851098252/59947620076676354677931620854149363289912815578372046638627*y + 40811847750691841311291487407950000454212086212623928404084/59947620076676354677931620854149363289912815578372046638627

-39224335832892961050189456432660897043171275639060400675186/59947620076676354677931620854149363289912815578372046638627*y^23 + 255036160337928803980839975718645942235842084732835673265078/59947620076676354677931620854149363289912815578372046638627*y^22 + 3108249826365906843937271132309624099928546814596198754616057/59947620076676354677931620854149363289912815578372046638627*y^21 - 12613200596912443375030007051332707995812890875162936540166120/59947620076676354677931620854149363289912815578372046638627*y^20 - 20810028639156224098212741274060593736201197014512210127282654/59947620076676354677931620854149363289912815578372046638627*y^19 + 109443986095321716188779437608439114924244271154235615158508987/59947620076676354677931620854149363289912815578372046638627*y^18 - 42566756293239283683951634951964711344197661581589994801740263/59947620076676354677931620854149363289912815578372046638627*y^17 - 344133044435807096308033953654601307183736554717215521488936491/59947620076676354677931620854149363289912815578372046638627*y^16 - 18650349421863338666904189667054263696326682410166281137558775/59947620076676354677931620854149363289912815578372046638627*y^15 + 1150899577847116193985973153791823150475965351279853500590635969/59947620076676354677931620854149363289912815578372046638627*y^14 + 1049363078943920481680518187951440476848189174424163543764328833/59947620076676354677931620854149363289912815578372046638627*y^13 - 2246920712638144595004172702514289344640346981136487415044732056/59947620076676354677931620854149363289912815578372046638627*y^12 - 2573891410668217062954506819665555319330422865892003932714992318/59947620076676354677931620854149363289912815578372046638627*y^11 + 2739246193199059503798605184225538307406148380392186945095157520/59947620076676354677931620854149363289912815578372046638627*y^10 + 2032122239021007102125107343494447079010329297300943441593843014/59947620076676354677931620854149363289912815578372046638627*y^9 - 2322290416893155982593702413218501801409195192874363473116537458/59947620076676354677931620854149363289912815578372046638627*y^8 - 594485724458116784276174316714227450454565440386411619379393685/59947620076676354677931620854149363289912815578372046638627*y^7 + 959966494279661805068366707831542971402956465298736011825223472/59947620076676354677931620854149363289912815578372046638627*y^6 + 23453621640270474876561571506761324079603039972060132826376635/59947620076676354677931620854149363289912815578372046638627*y^5 - 151689064460755410481202842473609240987974295138738408886404130/59947620076676354677931620854149363289912815578372046638627*y^4 + 35969652050594186335139237330240612490667404666384662452019/59947620076676354677931620854149363289912815578372046638627*y^3 + 10245053806014614374037460448151252258813964696076431486437445/59947620076676354677931620854149363289912815578372046638627*y^2 + 668303141428727344897134072715160813186191420432241500137152/59947620076676354677931620854149363289912815578372046638627*y - 77444598671280491414918415778400862899965569908652039628208/59947620076676354677931620854149363289912815578372046638627

-153838708116968648441284559057087244806758521106364872410693/959161921226821674846905933666389812638605049253952746218032*y^23 + 1119820040482749483258577351675400514415962891687346511568951/959161921226821674846905933666389812638605049253952746218032*y^22 + 11373455987571418645391354274653404464818270904674755549082433/959161921226821674846905933666389812638605049253952746218032*y^21 - 29331147561416693214711989596398076022581288079021586357220789/479580960613410837423452966833194906319302524626976373109016*y^20 - 10042833007267778393965981003835760192152162867584344071461249/239790480306705418711726483416597453159651262313488186554508*y^19 + 478107587498833196190183961637478301984050935880358543979634207/959161921226821674846905933666389812638605049253952746218032*y^18 - 128494738370181897744073824927118379092903440833197005587956715/239790480306705418711726483416597453159651262313488186554508*y^17 - 1098567104408217284414261219364426653449224181212674369718357159/959161921226821674846905933666389812638605049253952746218032*y^16 + 433862152450064781776977852509478953512892315813337475685647269/479580960613410837423452966833194906319302524626976373109016*y^15 + 266292827080260695444002381837209078871365416322657721762134276/59947620076676354677931620854149363289912815578372046638627*y^14 + 774375439702979411342468560746943025026814808205557022372458995/959161921226821674846905933666389812638605049253952746218032*y^13 - 10867325812584301230707610400120158839711497761339189254876530305/959161921226821674846905933666389812638605049253952746218032*y^12 - 1412886907567147831240135442456966925844789467943370645383246217/479580960613410837423452966833194906319302524626976373109016*y^11 + 989409665265527812582760742529106234567185267261178540391677115/59947620076676354677931620854149363289912815578372046638627*y^10 - 207354473804253065579822227294533861255695109721404335041138567/119895240153352709355863241708298726579825631156744093277254*y^9 - 11364150841059928610139662120446403695836710623003343524198034089/959161921226821674846905933666389812638605049253952746218032*y^8 + 1277517970043053254171770431076620254122341926153838331958085733/239790480306705418711726483416597453159651262313488186554508*y^7 + 158858290899109840789358563630628219610751367295642605492339004/59947620076676354677931620854149363289912815578372046638627*y^6 - 1043151093791931793233538955429067744751246736300321109343499437/479580960613410837423452966833194906319302524626976373109016*y^5 + 134882126243457291400189409323881013675853552303866279591899517/479580960613410837423452966833194906319302524626976373109016*y^4 + 44758688792585236369885103888581139651877450535569559525167731/959161921226821674846905933666389812638605049253952746218032*y^3 - 5582584767167005833212582656093930057578082483276025130928461/959161921226821674846905933666389812638605049253952746218032*y^2 + 836785870972606675240990004671061129155421911429176627683417/479580960613410837423452966833194906319302524626976373109016*y + 297648088760820156715592443156172660169586811944803307600823/959161921226821674846905933666389812638605049253952746218032

135362575098189725343296956920092111122852373343424873254765/239790480306705418711726483416597453159651262313488186554508*y^23 - 946198799749265977391313855077060248019689060597134068668559/239790480306705418711726483416597453159651262313488186554508*y^22 - 10275108265540289445271057312181099138945624568299595052787761/239790480306705418711726483416597453159651262313488186554508*y^21 + 24308376394008741073027093657380486349755921107351760743896119/119895240153352709355863241708298726579825631156744093277254*y^20 + 12218940703923344241667633112096676774896710653840996328769355/59947620076676354677931620854149363289912815578372046638627*y^19 - 405328168363122549459947752912894007912689763843345590031394167/239790480306705418711726483416597453159651262313488186554508*y^18 + 85254163643377240910182828792667206759519263933592568112145685/59947620076676354677931620854149363289912815578372046638627*y^17 + 1052831988431428883393352101592949770091318589541440095269422119/239790480306705418711726483416597453159651262313488186554508*y^16 - 238169468378717625967660685995416786423882011824108581899994241/119895240153352709355863241708298726579825631156744093277254*y^15 - 955558543244998945910404109477425291796536989456511989103019099/59947620076676354677931620854149363289912815578372046638627*y^14 - 1715245145532339437195572496442029487460262333775185884892693939/239790480306705418711726483416597453159651262313488186554508*y^13 + 8893029857833686071106992771164456485138207121597942390118171741/239790480306705418711726483416597453159651262313488186554508*y^12 + 2332588701564238450173592766277642986532288378937321910111794855/119895240153352709355863241708298726579825631156744093277254*y^11 - 3111788359718345922495713812578178886741811048656527281538552441/59947620076676354677931620854149363289912815578372046638627*y^10 - 325052519232738608732829163865393729537999375652876401040591169/59947620076676354677931620854149363289912815578372046638627*y^9 + 9671637228937487671958396953821745384010126551997222163891287873/239790480306705418711726483416597453159651262313488186554508*y^8 - 635302567270479454417899414295780361343512009049717918021633624/59947620076676354677931620854149363289912815578372046638627*y^7 - 720839952562784661191967210701277126640307101177079954368234555/59947620076676354677931620854149363289912815578372046638627*y^6 + 752699981638339341988583577667763586149921578928029918585383243/119895240153352709355863241708298726579825631156744093277254*y^5 + 28106770555336999373523588235727118837362318215774569194056043/119895240153352709355863241708298726579825631156744093277254*y^4 - 142897703602311763435578737352124300050338624332385027787591083/239790480306705418711726483416597453159651262313488186554508*y^3 + 14828750592568523652369097680324662189827288035065211511512133/239790480306705418711726483416597453159651262313488186554508*y^2 + 1486577092962437719156877762744467895185864043575225632053899/119895240153352709355863241708298726579825631156744093277254*y - 595720311388999119364481482036355722883232098829838979882043/239790480306705418711726483416597453159651262313488186554508

16390936611231082220450180175171765860027718120319037408545/59947620076676354677931620854149363289912815578372046638627*y^23 - 128932259833205470364631523129035933021632565451160640140349/59947620076676354677931620854149363289912815578372046638627*y^22 - 1149060582849643368007491824198388351404203815822475286460015/59947620076676354677931620854149363289912815578372046638627*y^21 + 7013021509535190406409539748410396969826294492667220215818594/59947620076676354677931620854149363289912815578372046638627*y^20 + 1159934103025282076645254020166839824385569825642016681163731/59947620076676354677931620854149363289912815578372046638627*y^19 - 56117016043698796201217502270471764814726883003736073335268955/59947620076676354677931620854149363289912815578372046638627*y^18 + 82289219871925620430786352344854110332952629461544806938011164/59947620076676354677931620854149363289912815578372046638627*y^17 + 106845132507731479081590914112912808575401465296968648261849267/59947620076676354677931620854149363289912815578372046638627*y^16 - 181552916265329176094779454580283448932686894209667117042079420/59947620076676354677931620854149363289912815578372046638627*y^15 - 453768329228079939649512986829588974558295043616309583849904918/59947620076676354677931620854149363289912815578372046638627*y^14 + 213611516909524811566771584936648614771340097190798851458276018/59947620076676354677931620854149363289912815578372046638627*y^13 + 1407767843343122168413506469394346158491408020228635266772717910/59947620076676354677931620854149363289912815578372046638627*y^12 - 303210830589741605121648667801895065202993725861744825328227478/59947620076676354677931620854149363289912815578372046638627*y^11 - 2342664675931355742667132323576838859182354559944168435982400090/59947620076676354677931620854149363289912815578372046638627*y^10 + 960198049133839406598051558403119844511261495644267703758826884/59947620076676354677931620854149363289912815578372046638627*y^9 + 1780489889539793787944317617676512298313361160741993150693418818/59947620076676354677931620854149363289912815578372046638627*y^8 - 1248509694364574795803515430782127676421604218874086045695036402/59947620076676354677931620854149363289912815578372046638627*y^7 - 450506105639614782939035185184781523691193306854269799449387305/59947620076676354677931620854149363289912815578372046638627*y^6 + 556248083937110465376146279406777361256464851934325975408415153/59947620076676354677931620854149363289912815578372046638627*y^5 - 34729486247659436736618371965965779375711749594895113464338035/59947620076676354677931620854149363289912815578372046638627*y^4 - 69794828056819599358171276842614021784953522001719395770123697/59947620076676354677931620854149363289912815578372046638627*y^3 + 9656110567185909835058025285370112001847725080357045089564520/59947620076676354677931620854149363289912815578372046638627*y^2 + 2698521817009852952137582097903732318649680689326598412649422/59947620076676354677931620854149363289912815578372046638627*y - 105897982508575983956789406464686405933295696837909296833163/59947620076676354677931620854149363289912815578372046638627

6593036102854682142451984759559853863426541035460549597632/59947620076676354677931620854149363289912815578372046638627*y^23 - 47489303255976430963454506276483730999271419162866422815321/59947620076676354677931620854149363289912815578372046638627*y^22 - 490414245369588788798417948715406028832052955319424712332922/59947620076676354677931620854149363289912815578372046638627*y^21 + 2473752255116448886840472553464440339978601823001121698765433/59947620076676354677931620854149363289912815578372046638627*y^20 + 1852112601265982486269394646348502110485474207666572191800158/59947620076676354677931620854149363289912815578372046638627*y^19 - 20239390178604613531694007397418991988419720922654123378152803/59947620076676354677931620854149363289912815578372046638627*y^18 + 21197230588164366898861564897505871175806857482451634335155161/59947620076676354677931620854149363289912815578372046638627*y^17 + 47558656044372188632592067080553572333870297543712054782559947/59947620076676354677931620854149363289912815578372046638627*y^16 - 36057976383420936176357948284920504938169292284358468965616418/59947620076676354677931620854149363289912815578372046638627*y^15 - 178539603307114506439496563401692850903777227571980124307009035/59947620076676354677931620854149363289912815578372046638627*y^14 - 36774336193219453826742144408141553622382954159173149899634457/59947620076676354677931620854149363289912815578372046638627*y^13 + 445915527705184293529739764862458599363564950382242769964221529/59947620076676354677931620854149363289912815578372046638627*y^12 + 105693179757278935988000080152057383489184466368916655055531583/59947620076676354677931620854149363289912815578372046638627*y^11 - 667867691916744935314975019151382177836135736770046773538277741/59947620076676354677931620854149363289912815578372046638627*y^10 + 119177712888056049044886525844400846540048420944629336149689097/59947620076676354677931620854149363289912815578372046638627*y^9 + 525390830344737776816793059502223899909646326393687807503132458/59947620076676354677931620854149363289912815578372046638627*y^8 - 274611064776075539995474225781698833850178452680532921577134002/59947620076676354677931620854149363289912815578372046638627*y^7 - 139252436526447638723153641742796439763147912987915841786545721/59947620076676354677931620854149363289912815578372046638627*y^6 + 139184322015718282992627406022485429906924316269148321690919334/59947620076676354677931620854149363289912815578372046638627*y^5 - 7163944706744576810311769881506923637204241829647186087461304/59947620076676354677931620854149363289912815578372046638627*y^4 - 18493477847311012230390550417232827912549071621197103850175383/59947620076676354677931620854149363289912815578372046638627*y^3 + 2584270724366562382691231361145470589411289570176846513087103/59947620076676354677931620854149363289912815578372046638627*y^2 + 736860007796633445955844515876765412302056298378506289485075/59947620076676354677931620854149363289912815578372046638627*y - 52002138133342128975943253808207342416142291483015159027177/59947620076676354677931620854149363289912815578372046638627

-133500143916311122436750130746457622315683586273799620212230/539528580690087192101384587687344269609215340205348419747643*y^23 + 978620159425266849644028188586154599779115482339742293740585/539528580690087192101384587687344269609215340205348419747643*y^22 + 9841594470760433009555878019359073937681734079101404740159679/539528580690087192101384587687344269609215340205348419747643*y^21 - 17190194890604664065208738135477721056465166100449061078346416/179842860230029064033794862562448089869738446735116139915881*y^20 - 33848634019869154411879905781856265705090605978640213920774306/539528580690087192101384587687344269609215340205348419747643*y^19 + 141647444597604800172151183934597577929997922610152509127027451/179842860230029064033794862562448089869738446735116139915881*y^18 - 153888199696855788258471258982580220176563670086310540987879770/179842860230029064033794862562448089869738446735116139915881*y^17 - 332582524729495838847252344162286796228548473357951797317953584/179842860230029064033794862562448089869738446735116139915881*y^16 + 291398329973033881064750458480127216382988969803188278512324080/179842860230029064033794862562448089869738446735116139915881*y^15 + 3813586567025411469321692556203091036909837233098361317116962318/539528580690087192101384587687344269609215340205348419747643*y^14 + 360280839970651515625142097871899974595622746858976510092357607/539528580690087192101384587687344269609215340205348419747643*y^13 - 3355519179777591819728266802691063670234509211019086473359184335/179842860230029064033794862562448089869738446735116139915881*y^12 - 692030935392648240560341117940996441045052817738427543170277285/179842860230029064033794862562448089869738446735116139915881*y^11 + 15397899153210695667647558045950253452727413886656487559133571467/539528580690087192101384587687344269609215340205348419747643*y^10 - 581108318468483267929363878942217089510972599124744081872068304/179842860230029064033794862562448089869738446735116139915881*y^9 - 4009133150048880370889372134786807708714587380181873613697198812/179842860230029064033794862562448089869738446735116139915881*y^8 + 5160568086498633784338770454233331120824933650876668178725739012/539528580690087192101384587687344269609215340205348419747643*y^7 + 3596613679416359568177217967944390438943533459687838712619301290/539528580690087192101384587687344269609215340205348419747643*y^6 - 292045473709170898648821567641994959968458611832815351749329932/59947620076676354677931620854149363289912815578372046638627*y^5 - 57268978217187297273580993383489242339740000192954299796646291/539528580690087192101384587687344269609215340205348419747643*y^4 + 35758940944886365532669574513540781997280302084612102665822255/59947620076676354677931620854149363289912815578372046638627*y^3 - 31829851489004503750776872601000058037111270664964864345963753/539528580690087192101384587687344269609215340205348419747643*y^2 - 10532028670382476122934229649813512115979736639677380507822614/539528580690087192101384587687344269609215340205348419747643*y + 871882763348542281184832563144450242762546148798923847262102/539528580690087192101384587687344269609215340205348419747643


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

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

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

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

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

# 1 Loop Invariant
-4179844403613727975050515266721787979232706791963651431538629/119895240153352709355863241708298726579825631156744093277254*y^23 + 13666612629488133917056611861533093107047050966250427258889164/59947620076676354677931620854149363289912815578372046638627*y^22 + 165057062490715730578942292444673654215222481041566490210364569/59947620076676354677931620854149363289912815578372046638627*y^21 - 677908441583278431929290137191410632515433494828211285219630913/59947620076676354677931620854149363289912815578372046638627*y^20 - 1080003201135667004883969887845254487985335666849328163356351028/59947620076676354677931620854149363289912815578372046638627*y^19 + 11713538465854547421105725948378876871024921252908308273642260349/119895240153352709355863241708298726579825631156744093277254*y^18 - 5016220030483533392091525910556835350261889520027186165584797855/119895240153352709355863241708298726579825631156744093277254*y^17 - 36229377748982135563175137533606854428729688227177775566102942847/119895240153352709355863241708298726579825631156744093277254*y^16 - 383880724890120907763828672207380913571451505074418037080387911/59947620076676354677931620854149363289912815578372046638627*y^15 + 121905349043502359176505546587874121076835607312844142498596499519/119895240153352709355863241708298726579825631156744093277254*y^14 + 53669715011270511511931910728082534327911766884547402216913240387/59947620076676354677931620854149363289912815578372046638627*y^13 - 120412889081054025866447980246715575327000288344202274171344792046/59947620076676354677931620854149363289912815578372046638627*y^12 - 131634521704532325900757775284454603748690734392253269998459763019/59947620076676354677931620854149363289912815578372046638627*y^11 + 148152945992637535300219877614959978436052263523971984815659883207/59947620076676354677931620854149363289912815578372046638627*y^10 + 100173684319035219284971223696827600111933782165091950728820163962/59947620076676354677931620854149363289912815578372046638627*y^9 - 247983574554120944297319067331769949179398565169604915608215076789/119895240153352709355863241708298726579825631156744093277254*y^8 - 50368292956625487812311599337966818903336365971167258907632174111/119895240153352709355863241708298726579825631156744093277254*y^7 + 49201485701995871697579741122157462381537638885376118982005561559/59947620076676354677931620854149363289912815578372046638627*y^6 - 1758597343437683860834171867555217668217215389561316997130524209/119895240153352709355863241708298726579825631156744093277254*y^5 - 13848776461802295266241641171285181178892382216582099646050353887/119895240153352709355863241708298726579825631156744093277254*y^4 + 283232485614625274654808299375664041986403666010816119048722993/119895240153352709355863241708298726579825631156744093277254*y^3 + 783113281762730464292228810045132288380847103480236277511591055/119895240153352709355863241708298726579825631156744093277254*y^2 + 38850440109246800803045673427553220212214861859407007098126329/59947620076676354677931620854149363289912815578372046638627*y - 60946791684212158166217425390393142899542868241222088092740/59947620076676354677931620854149363289912815578372046638627

# 2 Loop Invariant
156446467461439071881063002307880021348280218673069700201168236330897662990877658834650653145844483027419780056415185526065698629339297157/3780643577393101263989381037914206351257546392026046115975049759044951761866957913328561906956134547602167474358715213905614426128882028172*y^23 - 7073839876187868257048700968028076139540607085952769093038784350191422490318527593206383863385481761177677148714145083049889364606387075589/22683861464358607583936286227485238107545278352156276695850298554269710571201747479971371441736807285613004846152291283433686556773292169032*y^22 - 45241270298638234019883158670400416483767854193397816146379457284022433809141980860494494486645581788438705259885656160110818615937737554215/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^21 + 188676285963453515545963277834456033403028762006522861154853442966495013014038996903157481560522132116173978016006482899914186442487843088989/11341930732179303791968143113742619053772639176078138347925149277134855285600873739985685720868403642806502423076145641716843278386646084516*y^20 + 112924590178183022251304745265290256883342797397355531068205029987977277512858051323629801675779448777029822824163080673564108010576155384505/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^19 - 1021223094461610129632806025960111240334612518977021753486528522267127563575297554752706981280680682672120479399885278658203291623077469591175/7561287154786202527978762075828412702515092784052092231950099518089903523733915826657123813912269095204334948717430427811228852257764056344*y^18 + 1914035334860750235489825462148357524483110595802068895354672745512372126763087428198336731390689628600646888706769206973743774358866335342729/11341930732179303791968143113742619053772639176078138347925149277134855285600873739985685720868403642806502423076145641716843278386646084516*y^17 + 13156654580624754203265851844578662437733880939517852792641237405555839633574028334154091304159790484560650865956799484618722637215057148428707/45367722928717215167872572454970476215090556704312553391700597108539421142403494959942742883473614571226009692304582566867373113546584338064*y^16 - 5165220160559924292212025956713297855406754506026471903795098213249308023647317379735598010620101464622506842228794421751972500017429080371637/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^15 - 52407094864099400619928575525554481923615383998531356823473055330113369416086527289432733904026363014450248256146692160855605781788291805598439/45367722928717215167872572454970476215090556704312553391700597108539421142403494959942742883473614571226009692304582566867373113546584338064*y^14 + 2128788632245719132888094836615108478399034701441645859668414911481894871484217826291514293049540048397004234078907490725252164296517373293395/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^13 + 24528745316623976081518708495863444605565380232695866524102477672783880659518506114003418980282457788008096525058388574405351149931666959695159/7561287154786202527978762075828412702515092784052092231950099518089903523733915826657123813912269095204334948717430427811228852257764056344*y^12 + 1283852591053366744010698807206577641075228286576574100917476584869192253865525291753848478020809668992976591115410582108945314405563858504125/22683861464358607583936286227485238107545278352156276695850298554269710571201747479971371441736807285613004846152291283433686556773292169032*y^11 - 116496201529728224137975631221662816937240146157976931674462267715564154343421488250575068919761873987758357912460572128322258731582333882958937/22683861464358607583936286227485238107545278352156276695850298554269710571201747479971371441736807285613004846152291283433686556773292169032*y^10 + 15501425735024326342290492639155567979680219010747052043532460123128793411399995229491073689813855992198977026295182284626328042113785404928671/11341930732179303791968143113742619053772639176078138347925149277134855285600873739985685720868403642806502423076145641716843278386646084516*y^9 + 59609762397980241041177450751797835509014404663922735494253470719265172781287943509603934307304400231330547455702641039126770081004878293210691/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^8 - 25743110341585188717239600059074076569251961736754269796827157447290778487899882894094583055944972050836378951595051031200746297460638677657757/11341930732179303791968143113742619053772639176078138347925149277134855285600873739985685720868403642806502423076145641716843278386646084516*y^7 - 11999784574462417369076549158783745276445267818845819368413882335992505892440902353447719058941541864300484262341381505423315200803416612978405/11341930732179303791968143113742619053772639176078138347925149277134855285600873739985685720868403642806502423076145641716843278386646084516*y^6 + 4018016781806984285387345662551384310039963399214972419771875750248340128995636109193861740450490773338044419883864577785735551643619214735387/3780643577393101263989381037914206351257546392026046115975049759044951761866957913328561906956134547602167474358715213905614426128882028172*y^5 - 688703561833714783891834829176946890178383670773040224620306182913594533939235061665349818364650472164450361240467907367409583458592310141343/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^4 - 1983828276009376333917509921223044975218468464622365365821785678807437392586326987709229602927068995454063223180373319859503995582189057036527/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688*y^3 + 401621415899468114188756189155928714080181189505168074430334622720754994545699153795381968328667779493873889833374653759060063111457838011401/22683861464358607583936286227485238107545278352156276695850298554269710571201747479971371441736807285613004846152291283433686556773292169032*y^2 + 220270963049450598618086268692383851355254281769780009751535752034709709821810794640050090268509001933311322688305732393299406557055296057977/45367722928717215167872572454970476215090556704312553391700597108539421142403494959942742883473614571226009692304582566867373113546584338064*y - 3272824395295147004529108177258653247375786379095192585043262917947913600476706656597373657045013727545028005139489801737586167676868703271/15122574309572405055957524151656825405030185568104184463900199036179807047467831653314247627824538190408669897434860855622457704515528112688

# 3 Loop Invariant
2377050518211297591867976275612777948138563251389618188070669394953809920591138236083610334559339201874404919658513475118461495597199308048939371189700181159246511995629133752915/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^23 - 2146640380702913659227023642432008032890985838182888572437312086186001836337826017432840135984125085699598538924001194539668484371515560229571262270726544435118872887389276030959/30023590689024232039266584949803696525414564885524260457912397201492950588372360292887356276956546164249937637193143223042701030821238000841350825187811334010511725043369482711832*y^22 - 176904340940372533548526664424729727125240174589713813904313203348303947425399233610016673693685939324691876468329547278934784649443080148552665055715885743884200042848492618207913/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^21 + 224639629209924912077161079739320297338204254393795011245335452206208347610680824390855168708260012010859553786647689408145933894936634856482088626486158263213963530652867231985069/60047181378048464078533169899607393050829129771048520915824794402985901176744720585774712553913092328499875274386286446085402061642476001682701650375622668021023450086738965423664*y^20 + 685802408078384135396869916356181533372215408877139600622186929578134366256976639826166729496189350031913832389251468297677676469526618753185785332109374199315656985058172259081861/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^19 - 7447915136073115787121863493492659737956538679625259473032168822056795462117582323074250156999258697257068748155809958840654878306278329707986913690386422056288423885863377449111193/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^18 + 469893865768056524522711057761785866553426560448427235663738364159426567202709166674405413811350723675654735753270009061717097415572961392141588266304268107446126492143792646472921/15011795344512116019633292474901848262707282442762130228956198600746475294186180146443678138478273082124968818596571611521350515410619000420675412593905667005255862521684741355916*y^17 + 1135434406874408457860627741387305234857286307002465266664452741599695889988176765821198583900010772609475696498017962939551268020604281761747913698711727207036616068590710169533641/15011795344512116019633292474901848262707282442762130228956198600746475294186180146443678138478273082124968818596571611521350515410619000420675412593905667005255862521684741355916*y^16 - 3386273246480898530886156530888899431419096550292447163862253127031663751281790479937825101896211825038881629224250921682099911431541522558376452344942637074807809109580338665598359/60047181378048464078533169899607393050829129771048520915824794402985901176744720585774712553913092328499875274386286446085402061642476001682701650375622668021023450086738965423664*y^15 - 17014814312411330463307419023328988554119502364298776536378725684828831620710753318690589905073373653269183749394771902338294249249243765635974847833044835077309212771017869452760015/60047181378048464078533169899607393050829129771048520915824794402985901176744720585774712553913092328499875274386286446085402061642476001682701650375622668021023450086738965423664*y^14 - 3317754931285086599271737560938830659582236946041646308991149815627854071597333380033987351165029628469100037866765098939995218782880473753061451268525519129420012403531026302469639/60047181378048464078533169899607393050829129771048520915824794402985901176744720585774712553913092328499875274386286446085402061642476001682701650375622668021023450086738965423664*y^13 + 43415411941486246876193935990918448305030933426571335097142330788293760198194886532261699454514280185400552432493542600578833091553604947622994295801781721942368582506236209137907351/60047181378048464078533169899607393050829129771048520915824794402985901176744720585774712553913092328499875274386286446085402061642476001682701650375622668021023450086738965423664*y^12 + 50551776197179859650587573787471876915434436532328812119715115223015133767688099101784309582759891863624148693394481080091978879324592205396815992492161117997707118415196371503708491/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^11 - 130869021927434972322099276577352262418460988751462592795904140319618089565806736192347801787547482469076181265073918722558411312366373967972952744747770257121987144761314664475955719/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328*y^10 + 6977303782807456835132629089398977898816999930145930230034318776084477543528617438230870956277247797039227053312023445010439333584993920105763367278485057348687385282868462887106067/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328*y^9 + 208220526889577380771596407975077137745122285100835586903592184854623094381488032251760884376327685913723371395923174804337728220926366096672387671290353289531206941796209588611307895/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^8 - 38910751276911943404379320373858023915527970722732927526606078068261776430115012220542368505253714368088155438997477491776063914178726714838464189712217002595456350202866847887454989/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328*y^7 - 65919237060326885200845958182764079554933310781846803744918264201908977014581468523787301607473288035360139721381370943269991249781453545578165476587743647634951174705064879358593503/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^6 + 5333280569201272749823217300624189429464304774064646023167081648319538249300396752445446836299129217709065694803332242772709444008666252854501691740974381868649636326617262351186109/30023590689024232039266584949803696525414564885524260457912397201492950588372360292887356276956546164249937637193143223042701030821238000841350825187811334010511725043369482711832*y^5 + 3054333923749592245374748613768323036300610052040062249040016541957330358004692991464379716174309194526796943503630727439169327228204895674776142540618390872908013098096693887034749/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^4 - 5791882475203659120484465172385154498898076660321748068160337072222849212359850612270182976077550298552913275440875064217584942169789263896283362463126423759853479209955454763214917/240188725512193856314132679598429572203316519084194083663299177611943604706978882343098850215652369313999501097545145784341608246569904006730806601502490672084093800346955861694656*y^3 + 181958751366616766442994944362641695963443944539338341256577435620962690199378359613828001348296673774524711735849422973405042893721517618058325718363703234305859038021935514705319/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328*y^2 + 112741286656796924970415714590118327291838280713055342442764313325646026929026875271062231995855266358109932308507064159111717468714995820020299208515861120437064532838148475389117/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328*y - 4109087504913075772994336479468213661469095512417748696413064103503981038223333896729011633519921482313786445220497319180693544655805560295052922508532678261807507488762842610293/120094362756096928157066339799214786101658259542097041831649588805971802353489441171549425107826184656999750548772572892170804123284952003365403300751245336042046900173477930847328