# Manifold: Census Knot K8_8

# Number of Tetrahedra: 8

# Number Field
x^31 - 11*x^30 - 119*x^29 + 87*x^28 + 2244*x^27 - 3000*x^26 - 19393*x^25 + 25048*x^24 + 96622*x^23 - 127814*x^22 - 286403*x^21 + 430581*x^20 + 676288*x^19 - 870832*x^18 - 1275222*x^17 + 1270635*x^16 + 1840855*x^15 - 1310144*x^14 - 2226249*x^13 + 215324*x^12 + 1322080*x^11 + 311307*x^10 - 373139*x^9 - 161146*x^8 + 51612*x^7 + 27946*x^6 - 4323*x^5 - 1679*x^4 + 375*x^3 + 18*x^2 - 15*x + 1 

# Approximate Field Generator
0.119026527369743 - 0.143548926514018*I

# Shape Parameters
-2607775359386138818254597134649453552226573264739850788833013288489917621901660974592245/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^30 + 9966300359676737803557426642067174792683328485438554733863248289537284785578400520786501/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^29 + 296664450479060988290002825126999606807328520807568616591406872094177837113348490190110785/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^28 - 367608452558985210481146584573176139776588665005039752408081910552526710509882231132590617/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^27 - 5711284579946211714093539324765382063040496846801462151275563304902609185907817380863579151/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^26 + 5247274005398081805260953820563979602302671184135164326824964112938787119170788087051436851/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^25 + 7708515436289986935052466361800702022712376227876187587248009408916840969711261379452228954/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^24 - 43725162116273357811264612986984478282281453922868621921189285260025484316129252629049085565/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^23 - 12011455936188175040957668191631327021296585493771184993417067352525167512692268482128942649/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^22 + 438866839734909141451058117636734309747642168598804695961832961961525742239008547545902205043/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^21 + 31520416242908608234571435496176882690365677580344353135573110105847375500784928161385113776/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^20 - 235326145788688735666039092526641835633623601169449709943918188102770677695279223471358107779/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^19 - 1180848554509490812543350271809263157376106929810940277344027779457937991126469465656659972037/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^18 + 2905809515090543333743169980527873543368196393273614637500125890225604498598044902587623456841/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^17 + 2152781465902858183414657946435983157698208003412842264936346047754441977938720763049800756323/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^16 - 4475114574642729383334872045694154604594631072914187684932828858797025081009452510013394532327/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^15 - 508372648394978488737247258139601704445501491502602490257380594332863881022168007620702903363/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^14 + 5045774051517259116452011011618150315008061830826738597380028712840234228416511754263606199783/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^13 + 3920617224340724692427794080433957417562729041480649459357372548588600233523002105461344391113/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^12 - 284933489264035954630070800910487112701315100584970772977938163333035870835617074282848919141/175464769563213856933267785565240563619730855314362381727879662504293606194265063188774*y^11 - 1393086466441173096896521665624647885424569269756073627901535237254953035256830372620027596972/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^10 + 187886239516992030412497143337864876012540568390250885461036414513544414094185053559452645367/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^9 + 1020881263652836191375893411229825444455336494985813418585073168365934529594057034030517962811/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^8 + 10698837429028944759483157876780054503266490499154002463561604310576891609085998512606235397/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^7 - 21552141232923944366346306741301737666610117232705004387962122902403040428912885127208714467/175464769563213856933267785565240563619730855314362381727879662504293606194265063188774*y^6 - 13137582303188786346741772017018102107978079310383623441798765497503503922567053358570016123/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^5 + 17936656941935997084267856410571917850454906989018248001843897607148747160010948176542302581/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^4 - 1233094075098240883593205506497106743901336003464668646352542454391217274427918855696923203/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^3 - 653879363909287973169593133554151255736149944633282150305667738214948984550322782628671081/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^2 + 143785531520504371453954757989281477059107917966765813117263390792181423732241379861706505/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y + 10099043575452616138931002038846332948012361914221672805163014787543241765373391346152215/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966

-1007434498672961357409369529948212428530914823793245889973610539063976108126902202809194/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^30 + 7562689302609716533222848373706206648527099105805411744823788681387277645402980644779209/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^29 + 233849593168721307179215942283214128547350214167707943466582831838912672593642002238536543/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^28 - 118026168714224265118068113666106770960515624309028951357884134526475746560805331427429955/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^27 - 2228955368089301490653740041460975997192904035771067190201404043845286623865050669071358527/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^26 + 3603900106049624494864064886417175723633045702837860810209245489050870979459424849611443440/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^25 + 12387884284588253477652724201455981907794641883876767031478561097109680193248900749529824409/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^24 - 30087337560065572463161571014458398471282403558764681621528178492268148039554422028943989478/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^23 - 19848212095133508021452613668171423752778097075517301880181478038568669533211555434189345857/175464769563213856933267785565240563619730855314362381727879662504293606194265063188774*y^22 + 152139388162699210930744976222388913234446598150400141586788727483235066065666629589110223619/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^21 + 55066443906925109953319716262099748879281265567184482061668778777242600529488851215425334045/175464769563213856933267785565240563619730855314362381727879662504293606194265063188774*y^20 - 166262051062739359827755859747549439961858521598073042143132960465168553069125476249080323954/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^19 - 547230986454762539215120196037384104751325093806500630609922293561179247805096142012048762595/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^18 + 2040797059188705836196139376393008896365099261791786909029593339651876046824578727856224790497/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^17 + 1007313172809814816007378285161365232306294046788640452779368310493993260841292594593917377897/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^16 - 1544080917567583749552495832751330978877389591997771776780715357952611506762282250889555079594/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^15 - 953665481008195806342369625173942911284814889925687815089504738580892163071384227680427712345/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^14 + 3394769628433446041605949143538925907192727960552068102525212322174529042610823303111225288169/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^13 + 1769618294599589683414138678094282278386036248051036478419650567898151612138455010116214886286/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^12 - 76332299366623810219468037382572233296636402101066026706134410840536245225789324703560710466/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^11 - 1119678656383286098627110132386977123547586863087776599809982631784206794705046467884578211456/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^10 - 3348473650537008509203522883553872405328564952173394027872953329449703540928655984511887551/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^9 + 366366863936258026940224256716915241215541529590753768621079619020801485984464074398269961408/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^8 + 18666025654074033422786859985561738656618405313843840966198681507489074105898109784739142063/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^7 - 7403096476676352226373813005367036668411642786657277602410991350777900244777682559403413471/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^6 - 8455200039813263842530566256879066385997586926839580021411014769618092128358789160799585305/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^5 + 13304664014424580924153255884295441259395345616767328322690994057896610979756305553541642001/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^4 - 532417726389554989719862887730463891148274739695157002641096115863303332718636798849922733/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^3 - 278751535600128820554001419855082728406793494883396276804245729066565117820026011805812427/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^2 + 51939292768659876229348555283489062316188022104284982371545340119597452772608374988131755/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y + 4780067089897033940161042449351195232433408388176851380431487438435918005044067387199049/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483

1361989497752085305196519600322183981884597919189742041824375897298673907273136476175513261/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^30 - 570362766847155655930019585228469012099234466004297212374354793941493683205435097118060107/21231237117148876688925402053394108197987433493037848189073439163019526349506072645841654*y^29 - 84792899844547136280370194419316229017521490146044569937714831032015317800475235489669468992/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^28 + 13920570378174736966590824915153231132898979541756874363360028666419865617096415522722458754/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^27 + 3064275341623579551129120857208883230064196188826340520528111093189198280914172220598658246997/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^26 - 1226837654809799204386006976347011168955178708723696156641852445416703553982355635011417463654/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^25 - 13793883949523208737436618129468472947401388153512426658346825930397548154411553288803948856393/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^24 + 19278245980723662796751676932054482567445892184331246218872348512460825674833168342399098196057/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^23 + 70388040076510012333857084132781733963047823505038394209729879366393517186343104622928470922447/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^22 - 9778208114613334906947934211746039629330344378115553609440421118165675906655319115438033992257/53078092792872191722313505133485270494968583732594620472683597907548815873765181614604135*y^21 - 218491088181583914191123254201458167247172633078141012550754456367684968257665406928517013154764/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^20 + 31516086446525501110032699686936779334213525836728349590917188439661915175383413264653483542253/48252811629883810656648641030441154995425985211449654975166907188680741703422892376912850*y^19 + 1091532848462698124282523849824471571146784766366756534379270231999400149587273016581949166141481/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^18 - 581647448988377419927242446428757411795712690527515616512154182588127823300984467203613966424661/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^17 - 1007759079443025491247599271747538013221926717219295830521010044575080680449373090456743581790819/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^16 + 612587384178526199926065877966135298466365161452779970099067825210525959156261477104961681990317/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^15 + 1388988634336666139201911461587146081803697801878971497435020610117325799892022112247982475112796/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^14 - 120565053354334069605344915098629901199505230144558338016104590061525927767675154697953834181611/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^13 - 1542934842783888952714519257631885447204096557540897695935069393641747462000177969039232332749203/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^12 - 1413475847827864498409463035442606644606246775543977848339835756780245157411274065794697569411827/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^11 + 480841939064827406353148601018783462092323120532995676072805530809327408014826199980382409114454/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^10 + 8573379273739371540520654263727293740182835687366164193339359348307113980265875103265391417744/4825281162988381065664864103044115499542598521144965497516690718868074170342289237691285*y^9 + 17054763530367591758952122651916943032481814484066972936222337356941479746148876395774992261318/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^8 - 19200189134559128836582930952390571001663856595294601433165399079321874018477194887125946614861/53078092792872191722313505133485270494968583732594620472683597907548815873765181614604135*y^7 - 40142340415705532869312458848422521621044831056111082906559549257105952886742181252824520091653/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^6 + 14127423353766751451853943802584640933246096088684146267227460140231385821827134527573570531923/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y^5 + 100582627717599918291470267187153827733055714844195946421540476316644520884128951604225646093/21231237117148876688925402053394108197987433493037848189073439163019526349506072645841654*y^4 - 421015939179475414284691588519045064629684236210068543195982486555208493230190923266962417322/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^3 + 1484636450475161990336380446725877433668228902457668687496900695120878849804805265669984658/265390463964360958611567525667426352474842918662973102363417989537744079368825908073020675*y^2 + 32670119085415190884547706212473991878167777459476889842982626096863894578351104156393231099/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350*y - 1983134004099880925038128390607557287318169201226867415751950611894427892142944631996688251/530780927928721917223135051334852704949685837325946204726835979075488158737651816146041350

-130149183085339077558744464635764228924931622500691860537505837261491292099810977042058/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^30 + 990732686491940751423617149961409042459803762459759694430169092456548769450620544458325/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^29 + 29921601018495424195079151821600792050503367627682012361786377303530681280656610476645391/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^28 - 37239121241957840917904470484472899633476679341149022302730700996786624372104375310385209/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^27 - 295604145712838774329126218138680583753758515602641035110893808639637021878479183329441217/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^26 + 1042521183875166706347516823027657016635204807987774030241698251545790940965712987759681963/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^25 + 1677445527955316936603916867363315501889632605643176414251132771170683371253759836254343079/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^24 - 4579655972896326255711520704015978879138921488473627878835060521745517466855147032964720866/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^23 - 1384498312862073943389612519053531001345470271634030004956832530975078800393087204379388314/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^22 + 48027022386803139073405064197092398446882252896651249307599760410875402128272900124632586355/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^21 + 4006737659355471628144738635469150597824144598292483449248285678224721732364313230876559548/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^20 - 54644063381473135616069922395801987316106935683946378824413697686268284318800188711418364897/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^19 - 158590862290704163259626712026353805171957781169517726572091230834068577031650222349003653007/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^18 + 182307998992308074506916153786740038381537596170496909656282473766978352619020867095065626911/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^17 + 149653857210941106021753139199653338937219891548570126746997456843739350610777171529032539167/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^16 - 591613083713619147774593111403917902077409038204774084762607055469208905936592211641370669149/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^15 - 75328336143322742014753507375945314839244868113106328185463918712518245924921328489566622270/263197154344820785399901678347860845429596282971543572591819493756440409291397594783161*y^14 + 715389765350240280843626119197515558822265582081793664181038861481959395103955530386475672729/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^13 + 585151839231988443274446795756114883069530453947693069331283481573852397814237941039423128725/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^12 - 26225329628875678316121263753434653784453998773302957684573553320222904197709450855802640746/87732384781606928466633892782620281809865427657181190863939831252146803097132531594387*y^11 - 501588288715135791659871464298079775600647358832790405777041648382116313522097866624288779139/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^10 + 91204740708096281974368354065773347621250323834843700122482828246957815949180288966954771791/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^9 + 106559230796761002180054300501720667302784120458511713444105419288890686398209388077171663700/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^8 + 6155139627790178158052481102965400607980475791024957382571814597634690653603017510719608859/526394308689641570799803356695721690859192565943087145183638987512880818582795189566322*y^7 - 5016762961151956485196825402746891874287066185825310414601864826476853697489844283683761899/175464769563213856933267785565240563619730855314362381727879662504293606194265063188774*y^6 - 2658261265591556312265308848941580747797240013628448412419436007885910606664739905361913281/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y^5 + 4734795675587741282950726164453056765503345186647688010609499527433166630098000699380476225/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^4 - 196596095960280049571181286521441088692404736048822625115185018779227343477324651135034613/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^3 - 192475763655123424346480159742558504282149864938578221169208958877007846749652879110916771/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966*y^2 + 15388595618058162362589472381071534260885215698494936967099374482057131886180449685706057/789591463034462356199705035043582536288788848914630717775458481269321227874192784349483*y + 3111132478284888864297713342769944621896015654490501064941684018516163274549923662817173/1579182926068924712399410070087165072577577697829261435550916962538642455748385568698966

-570869047912737062169564881161117976524637155286784573224627607949575248269160380404374252/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^30 + 6597007086432050957568765329615152567618500956895485006281691903833580575897505828084109433/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^29 + 64260068538353801257414566821762538156980345802140309775625383534656551990488811751617334549/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^28 - 85345119309703764845996659664973628360455346566726822851603260468454955381511152579897818312/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^27 - 1232992109871451326970952061539682186552946512842519320163191166563879562951842131254015903218/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^26 + 2397814576759860622232443664655272499025572188754394075435363714572087030504848867972951759361/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^25 + 9726688729472197664434978840016344356501317552731558692952669294077940382205084595795504428527/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^24 - 19692940732989883754370151664128556435559588354448979477158718144415179403924492234384302432184/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^23 - 44116507408673859657666583584491889003340366268748626848780029625655702989844145081480167518912/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^22 + 97375520070973902115672693475615813912323441062380936440423220987832675635662868899597081963217/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^21 + 108908978710106548097776624645716625944988026141120858396697684641965018592075717307346252875413/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^20 - 305760295437705125470258316533062377585494761490912358110677610252369659976711270479740619323632/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^19 - 214798555668946482488370816071233343958160744268350355789493160663284170543182715924580249806784/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^18 + 614598484555780227320656050220391652986362011392785984619069617925183641398019647672942753483459/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^17 + 383360012129172233536571408923899724867398252600698362661560485337219637998468391457002298185660/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^16 - 934755312932111429659656975508560200007762901436916521329383651726409576875251939672162570249835/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^15 - 525857312926159117974994831225974345321265881233858279120994643132993523513481998487636953663863/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^14 + 1035033825405541152432808224987850477635857023817050285994829259589626811871217743161057536639364/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^13 + 688113441826464274119845952948163074811127645495871682113740457184929377258168830278233964720713/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^12 - 500431986076032557282844925374498633536790637486135910984324861539165157044473733621187928167788/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^11 - 467942359195329009883220319847043965634648803782299302990352180786764469534479913281004930152174/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^10 + 82612329812511112537913469614127471013079032210082217212658191929491941213590987335557006066459/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^9 + 163176977496457454194246109276101484578227915994433917304024945205220018002483237299557574740485/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^8 - 29878612224995233184398820823399576565610229903441187071027594523612692102910050426427580471/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^7 - 28732833214769196342090980509883651402464804077125471952964094214853209066084581068600356610067/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^6 + 376030973147172430799706650436268965491558271626369043002691749127863436763648880573138557538/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^5 + 2195541876319364291103750964241668758931397842166939158763213918911145332862407305882604236940/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^4 - 287657137712062429410049041816192066460934714507610229693616983917241386250294331854795953752/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^3 - 48041656887676286257423519237977259823567059259244083639952877937442576482123076934035485156/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y^2 + 16683678407833888152792153144289275799056480356602749213155435050307040519274944122955048469/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477*y - 978531163235267022457842269734632856670116950113175268295353317212138984117982275789188371/6228999319494091921131006387566040008500445363659864551339728018902423019896409743201477

314273825390493354091129998700014629162986308601821945507396482853721632237920439988825472648/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^30 - 1181604273811052417787143135038293036155989941036131440370032488212263019805045968067958845643/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^29 - 72818130716035034650773638039924797488911712784250969734910479118973774538434881339831029321793/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^28 + 37501179710936411193612704381949236718203758269584744091607759852730205864404454520833538709077/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^27 + 1390165288144437555706734498957351693368050244105801389626940405429416329347700518997020098777295/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^26 - 1134484410441581909911273743972904720656417225673066816371564998688714462846914633070353708191271/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^25 - 1926955181010566236499713438255475890863347111750628809538142718748502063285802930350629817079774/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^24 + 18883317931998476650738570110209886566336245728221410506871747707141730348259988458131232650055185/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^23 + 18531938613351216509469077412389547212846045543654457585953809879164961543436941855006693300311867/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^22 - 95080766278881597303525387053875430736278179100904591489499235140561818821412291107490447297776963/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^21 - 51494030542009212312104435070995987172862101282159477381168903118928433615584728530964732698970673/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^20 + 103299036762100969329035817299327817367601227541177555191497518310264856902236514826579811210765609/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^19 + 343327112427963637681022316308603279367097988835504222117333197126643441784233120714029451337872883/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^18 - 315920288131374743508871244165812011180048726887887245363763261961048902267016469837073782861444391/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^17 - 640700357143303551534362135324420300106305415950686419240362672980899663360978508394265722850280255/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^16 + 950033976817977456589463519534414935346921743724623017741449791701370301415880163370942100498401001/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^15 + 153423803823970428662388122688592308329255333026671783349428866113848796856204173862303681828716292/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^14 - 1029415051725401850482100329950012680376732815182896122230907225408040155148794675582104454302307827/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^13 - 574771113163372716745588569167394814466225232657111170390116071812831037379608593573779743660915083/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^12 + 128391804785757636260558482773755946186091048118463449414628282764545236558340301291956158054256529/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^11 + 378012582081610127200478771845080892831328390153280096832970130076459374533302417898735207457770756/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^10 + 34027211834880053265018524936029896678563859867030391892611044224158497622608666458912019722212855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^9 - 236155077650888662558418995220133588882097670332616839967745209328068087457826872619085379695898775/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^8 - 22609731110177776738121119014288386891464357806557186609038491374007685694159350318141197586777809/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^7 + 5537901307536548258387023817702128544028366061070973376931765433184226591200666874764919546166845/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^6 + 5757166465208854725397805564214034909435240766743242906169290493551009872379023731156568385734108/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^5 - 953442868315691254752934050580481781650711706801189377862510218041106956173110522867835163238855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^4 - 386240985902368690587992147892827506745008791341186546202888749852864173818202699887214820675263/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^3 + 37920877284209646582010164587818390740893295658882474914219085423602538419773958097178076053426/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^2 + 905340275771470036447043461323014851008837108289116797568640644835751314760817017497613316293/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y - 989079768483763279503684182898011451318288275861011656135921635833101886065369267859197162178/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123

314273825390493354091129998700014629162986308601821945507396482853721632237920439988825472648/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^30 - 1181604273811052417787143135038293036155989941036131440370032488212263019805045968067958845643/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^29 - 72818130716035034650773638039924797488911712784250969734910479118973774538434881339831029321793/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^28 + 37501179710936411193612704381949236718203758269584744091607759852730205864404454520833538709077/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^27 + 1390165288144437555706734498957351693368050244105801389626940405429416329347700518997020098777295/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^26 - 1134484410441581909911273743972904720656417225673066816371564998688714462846914633070353708191271/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^25 - 1926955181010566236499713438255475890863347111750628809538142718748502063285802930350629817079774/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^24 + 18883317931998476650738570110209886566336245728221410506871747707141730348259988458131232650055185/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^23 + 18531938613351216509469077412389547212846045543654457585953809879164961543436941855006693300311867/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^22 - 95080766278881597303525387053875430736278179100904591489499235140561818821412291107490447297776963/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^21 - 51494030542009212312104435070995987172862101282159477381168903118928433615584728530964732698970673/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^20 + 103299036762100969329035817299327817367601227541177555191497518310264856902236514826579811210765609/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^19 + 343327112427963637681022316308603279367097988835504222117333197126643441784233120714029451337872883/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^18 - 315920288131374743508871244165812011180048726887887245363763261961048902267016469837073782861444391/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^17 - 640700357143303551534362135324420300106305415950686419240362672980899663360978508394265722850280255/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^16 + 950033976817977456589463519534414935346921743724623017741449791701370301415880163370942100498401001/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^15 + 153423803823970428662388122688592308329255333026671783349428866113848796856204173862303681828716292/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^14 - 1029415051725401850482100329950012680376732815182896122230907225408040155148794675582104454302307827/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^13 - 574771113163372716745588569167394814466225232657111170390116071812831037379608593573779743660915083/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^12 + 128391804785757636260558482773755946186091048118463449414628282764545236558340301291956158054256529/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^11 + 378012582081610127200478771845080892831328390153280096832970130076459374533302417898735207457770756/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^10 + 34027211834880053265018524936029896678563859867030391892611044224158497622608666458912019722212855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^9 - 236155077650888662558418995220133588882097670332616839967745209328068087457826872619085379695898775/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^8 - 22609731110177776738121119014288386891464357806557186609038491374007685694159350318141197586777809/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^7 + 5537901307536548258387023817702128544028366061070973376931765433184226591200666874764919546166845/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^6 + 5757166465208854725397805564214034909435240766743242906169290493551009872379023731156568385734108/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^5 - 953442868315691254752934050580481781650711706801189377862510218041106956173110522867835163238855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^4 - 386240985902368690587992147892827506745008791341186546202888749852864173818202699887214820675263/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^3 + 37920877284209646582010164587818390740893295658882474914219085423602538419773958097178076053426/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^2 + 905340275771470036447043461323014851008837108289116797568640644835751314760817017497613316293/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y - 989079768483763279503684182898011451318288275861011656135921635833101886065369267859197162178/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123

314273825390493354091129998700014629162986308601821945507396482853721632237920439988825472648/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^30 - 1181604273811052417787143135038293036155989941036131440370032488212263019805045968067958845643/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^29 - 72818130716035034650773638039924797488911712784250969734910479118973774538434881339831029321793/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^28 + 37501179710936411193612704381949236718203758269584744091607759852730205864404454520833538709077/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^27 + 1390165288144437555706734498957351693368050244105801389626940405429416329347700518997020098777295/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^26 - 1134484410441581909911273743972904720656417225673066816371564998688714462846914633070353708191271/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^25 - 1926955181010566236499713438255475890863347111750628809538142718748502063285802930350629817079774/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^24 + 18883317931998476650738570110209886566336245728221410506871747707141730348259988458131232650055185/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^23 + 18531938613351216509469077412389547212846045543654457585953809879164961543436941855006693300311867/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^22 - 95080766278881597303525387053875430736278179100904591489499235140561818821412291107490447297776963/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^21 - 51494030542009212312104435070995987172862101282159477381168903118928433615584728530964732698970673/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^20 + 103299036762100969329035817299327817367601227541177555191497518310264856902236514826579811210765609/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^19 + 343327112427963637681022316308603279367097988835504222117333197126643441784233120714029451337872883/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^18 - 315920288131374743508871244165812011180048726887887245363763261961048902267016469837073782861444391/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^17 - 640700357143303551534362135324420300106305415950686419240362672980899663360978508394265722850280255/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^16 + 950033976817977456589463519534414935346921743724623017741449791701370301415880163370942100498401001/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^15 + 153423803823970428662388122688592308329255333026671783349428866113848796856204173862303681828716292/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^14 - 1029415051725401850482100329950012680376732815182896122230907225408040155148794675582104454302307827/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^13 - 574771113163372716745588569167394814466225232657111170390116071812831037379608593573779743660915083/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^12 + 128391804785757636260558482773755946186091048118463449414628282764545236558340301291956158054256529/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^11 + 378012582081610127200478771845080892831328390153280096832970130076459374533302417898735207457770756/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^10 + 34027211834880053265018524936029896678563859867030391892611044224158497622608666458912019722212855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^9 - 236155077650888662558418995220133588882097670332616839967745209328068087457826872619085379695898775/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^8 - 22609731110177776738121119014288386891464357806557186609038491374007685694159350318141197586777809/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^7 + 5537901307536548258387023817702128544028366061070973376931765433184226591200666874764919546166845/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^6 + 5757166465208854725397805564214034909435240766743242906169290493551009872379023731156568385734108/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^5 - 953442868315691254752934050580481781650711706801189377862510218041106956173110522867835163238855/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^4 - 386240985902368690587992147892827506745008791341186546202888749852864173818202699887214820675263/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y^3 + 37920877284209646582010164587818390740893295658882474914219085423602538419773958097178076053426/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123*y^2 + 905340275771470036447043461323014851008837108289116797568640644835751314760817017497613316293/1814082701561516435877826719389134007071656366033402472479099575243352930875227842476610228246*y - 1896121119264521497442597542592578454854116458877712892375471423454778351502983189097502276301/907041350780758217938913359694567003535828183016701236239549787621676465437613921238305114123


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

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

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

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

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

# 1 Loop Invariant
-178336097737730475793525955360394587698790250993876112953332897686566035032693853689846413796815/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^30 + 2083981619993053006409102478946361273471619407053762841040335622681226161783456197717277075402763/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^29 + 19819789043705070917003506857992579290673959063185068625067628144548783303378952718173834973578873/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^28 - 29402372906364025661703631430493409888817117703396471584928596443508783203851373970161906478693745/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^27 - 383178531634554878957263562983574427974418022423701655784013178065078421323073518936943364422658935/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^26 + 200065750285590137811755322888924259622134237590780245251120945525495063555617790120698898105362356/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^25 + 742173729994253250553270832179925643450061389120575923792665002005520121145676911052829272402977645/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^24 - 1646806147182289881925737616324269477876187726531615459256859803329700791177732658714910419818359326/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^23 - 6604782363732612512898393595579066962471548956335353641360785109094200648262456485627003400442023667/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^22 + 32541080358401332426564640306460118402231423925969139387673512915399163094648929902759904483879119435/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^21 + 15574232297069122715102181978972647670813563089148482253252095932969534360631006514960800599919146061/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^20 - 50792092860610282222772846448390938038624387457841715709372415513757270143350338769639063149115133039/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^19 - 57634548291274934513989691534036846363394913784577998021928353101677804401625257992659905397645001875/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^18 + 205987806167403898392854637741127424783083904642483945400791676237949543263855045126349306514746151715/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^17 + 101363957316678748212838189345695598047342081944131242308554164114649657659591100543187225830117567971/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^16 - 317680491662089566170472029221929933126385454449055990137697704667566160842633077401707106607425306537/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^15 - 69111772633027467573904815306405924278802790853841422809192258733679151466886290173468771852660282203/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^14 + 359026854300778984348468329353394653115025015429959504119494126658990266371986175686983497222591885947/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^13 + 189201644708040110006894835301877821870485677241753678460417614893465965882013465252639122034118558867/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^12 - 198451596135395925350340643059732693737539684452939713374892440223911766360063403111431134713464918211/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^11 - 36309469777926843206675709183638119582156316310849965090698613027278611329764217880148550413009394419/302347116926919405979637786564855667845276061005567078746516595873892155145871307079435038041*y^10 + 23024997578073905191057852388901655839165660830678936336357026410702246608238000945164999131250546925/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^9 + 56700697840072362239715797889882326826561534108751519363812075201727767608483732617491746741240528323/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^8 - 2136855593533897032690905006070680737905183367116643487606748944027997411040952765407301830619458421/604694233853838811959275573129711335690552122011134157493033191747784310291742614158870076082*y^7 - 10760925612614416368545454068226741400157725897557479688805473282045545995006590374442201838846287879/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^6 + 624419367092676916543198723156690744605633458063607820741891522110496686763710329509901286318327169/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^5 + 840824405146795595550488179529589964001018311354140049403818872553974095176191651949488071342174173/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^4 - 138687853409285818383130982610692527121551544467670868316551746821701215552744041406523913922851951/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^3 - 16784423540217071129981108273233319327236704254429702571376344037842304597626622689545503042674453/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y^2 + 7330715936333777877506045968813923262565761472567470804664157176893760245758258751058683552024651/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164*y - 538846636459025698600984648383229974940366424407218268609339316071735855465405457692136782832873/1209388467707677623918551146259422671381104244022268314986066383495568620583485228317740152164

# 2 Loop Invariant
96436892039586005192057108274758626896829675053313141821032641875253141511417887521295525232155293700896002822377687599830369688987555395484664541747711654221535481341266609879282864035081308451674114144651/6830725470674200007019875753844208515588305256082072181079338070269300176841704084103504654855896238236389137445711268617972448901358624698070130693506515592182844923716471681972824196823965398902421357832614*y^30 - 2789285231876794573973279020519018767289831787059458065709464209903573357887738499441213025903289958139199204651581627643447165273138375763083685437581317587551244243690414032945314333400756252433395706163909/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^29 - 46535309037923552108776160708913444551519493144321721546559767317896131386029864876634844905207095670125349399666221040010518316906184936502651825280663299999866483221726782090796940543672136432702740424036221/27322901882696800028079503015376834062353221024328288724317352281077200707366816336414018619423584952945556549782845074471889795605434498792280522774026062368731379694865886727891296787295861595609685431330456*y^28 + 13138638192192375152156666828686729423485739503921999286410037177863809211597056987402348144653373654639647744695576852556966848105230327298560389586734931028633975877190837563193412027402159006788328026624089/13661450941348400014039751507688417031176610512164144362158676140538600353683408168207009309711792476472778274891422537235944897802717249396140261387013031184365689847432943363945648393647930797804842715665228*y^27 + 578836022294458517015365738487540510080506562045634978031190445028991892521659411148148828980742750614252093281597306723688190304216587659512884611947135507470509772437077991931315964572655218765066882080420473/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^26 - 127846468304967569384781205220414826045359473037196404838229994677087657730966493467022442209966463323500811824015357930756076726433083965078393483759353353539465160532260550590249679565241645971594306582578735/3415362735337100003509937876922104257794152628041036090539669035134650088420852042051752327427948119118194568722855634308986224450679312349035065346753257796091422461858235840986412098411982699451210678916307*y^25 - 5074447035197660471002232186506841908675346459598743798976291500091673975462718991071294859368924976699292902419289803545602451411570381479788920471634728639474865555606876297724654936859064161866608233370907467/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^24 + 2818988186478264383648054048658075411976510429691183235530168831279235307410886458247581164575679352616341189592957936113023811721716643120405435771856655953981540548825131162829000276874704456542511296864630137/9107633960898933342693167671792278020784407008109429574772450760359066902455605445471339539807861650981852183260948358157296598535144832930760174258008687456243793231621962242630432262431953865203228477110152*y^23 + 76689467882727898005064907424287967783186971154017738221734998840717038402001711938173765009616332310227760373828385574233735896244720732182366817253626559346245279359819238784879217392883051310702427549564792921/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^22 - 28744329246389438284118564971462436946959931376986077221082996072866960852171646201898613704465591378001708744032216936025040508873114493778403419011540806591096026378375256962576504359649805496595986081949575831/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^21 - 77322941581715679069461135556865856699279261581866832198431957186622346116467481464625681503481286649532817773856927468898262443143120138889208949485896975273455931549219011190675496953763977088308082679673265123/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^20 + 146770266742133543032973752062678442242313332086344959123435021886006915661868098418855203089180444352355317535436867467988708569684794524709481946818443402314105128878108677295198671895360464536178633863362200613/27322901882696800028079503015376834062353221024328288724317352281077200707366816336414018619423584952945556549782845074471889795605434498792280522774026062368731379694865886727891296787295861595609685431330456*y^19 + 186767488566670220727269324456485440494693106507791276606753086163909509813159757867797631015404621742880696200426368643104192873432384863051152238715760865203970547882690155056637027248212162679441794193959145209/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^18 - 95939078041036919622693629713351138339929325986001244378489529516536469903724277879237405971711001051568664002945319129864015819708287371284723024225097231556631138965421077845218757406631952051960183120344377847/9107633960898933342693167671792278020784407008109429574772450760359066902455605445471339539807861650981852183260948358157296598535144832930760174258008687456243793231621962242630432262431953865203228477110152*y^17 - 132123007735249681893339375361546506873720260730359618356707100455042168564618999368552329457929193854704419371224414624040865232279424910577862862028450037410734465232574229782766281325373150173423888671390176523/6830725470674200007019875753844208515588305256082072181079338070269300176841704084103504654855896238236389137445711268617972448901358624698070130693506515592182844923716471681972824196823965398902421357832614*y^16 + 797551304083986022566557113693608548586104334601391374433444762283384269265499761092243877066636220345678047011672206222202567749794844587873623801545921149485516635047643186286443121344738385952026423162467318345/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^15 + 1514451505728671243706134432604694172813782631477155273057229615799159350778685034307085473975552555264966762291760172167979214100470186946244560113041997451356569917583143461627685509972624509628244888584049297439/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^14 - 748370725600792648132150017215682096946647887572855532065825224838921711370358689115565855588553954778231256868711457214027204431576256369448524444434787891237232292604202443266731839336845227801607259366663809883/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^13 - 1792477282714348486161492310205371413447541364504817815216812847286635341264065295253016312985692993419983626278809143616700061376282700806265983143386025800903221940294775522727613210331951190408211684841194939989/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^12 - 70118519164969495301277210215347411659394433858965656830551201302898785927239789336116609766762831330341705019277870717270339572884654847589991289490584122842321563250897209818274549610769956731644656625286323085/27322901882696800028079503015376834062353221024328288724317352281077200707366816336414018619423584952945556549782845074471889795605434498792280522774026062368731379694865886727891296787295861595609685431330456*y^11 + 237666688451720719325826896048822838834272662188910324590522901878203569100294760154774290897377264534959202744289770029977755912416087508787699491878634616326836113540533162065738737192758375414471685884659786063/13661450941348400014039751507688417031176610512164144362158676140538600353683408168207009309711792476472778274891422537235944897802717249396140261387013031184365689847432943363945648393647930797804842715665228*y^10 + 49006814831756597664168803037895653022771950397781005952817490453728569260019256716661995160610514536728853940661464244746372611546604445528706652192311910589563761329786243823983633311738535672542842999367837707/6830725470674200007019875753844208515588305256082072181079338070269300176841704084103504654855896238236389137445711268617972448901358624698070130693506515592182844923716471681972824196823965398902421357832614*y^9 - 67288108982716850354237744684858778149733029016231200003363082069174734124026510347620998299331988618339654531466950289063883428393256461827231821361295247107796064518740002836055405405273061800136366864855083263/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^8 - 50355007090603657167309141191622785567343223409898465541153743338379517629990906453307905073642776295416487437563680302628309647360094261263163146222539070565235342027728565550635664981503775388302387091396540229/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^7 + 1596315848523853186476915162479103351849460670718508747470061087676800158632322889133201938995088838350068892705575832730934858122839973015147202712107985761098187439542003847012641576748753442416075805117422193/9107633960898933342693167671792278020784407008109429574772450760359066902455605445471339539807861650981852183260948358157296598535144832930760174258008687456243793231621962242630432262431953865203228477110152*y^6 + 21064016693615293998548028091048430780722699965855174300736428578161769588083669749773187976287847987642444759663386098923603327360279125002552197335062857251611899892986978284901048638798642090382217185843542725/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y^5 + 381774659818821529650065765646372018666365906015263781065237299331497322371200540686239809974519621597621223709762060380057500165639335080696059648934977241790781384888821338847367357249945097688133778519394563/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^4 - 292871241850716829017930438496824792137657922052190285694092884986084618180178619126532461773286103253497141929116908768981483192312198326527022517421653636285168894066869685635812174055364765712421478871111937/18215267921797866685386335343584556041568814016218859149544901520718133804911210890942679079615723301963704366521896716314593197070289665861520348516017374912487586463243924485260864524863907730406456954220304*y^3 - 1754081463931883600423749373251072362563071733199229390672898895542650280678133652388668934815337737120963460896541208017663748667712310311651115995303539388558527161073396490909338824108017017610194870904347/27322901882696800028079503015376834062353221024328288724317352281077200707366816336414018619423584952945556549782845074471889795605434498792280522774026062368731379694865886727891296787295861595609685431330456*y^2 + 16302080471183814808061142901345199432680100369011918483334830704543671856990280485552915571476417767367558984761512200055267275171307429156590521448729793054070078627789722249439411043080498671496571092229227/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912*y + 22952827444556667235163559532814925218294416462339595313737677693915000071220242811475152085674465323860745952997497275587048669047639606597801716336231778961991668745615419853988619074050886252938453283295833/54645803765393600056159006030753668124706442048656577448634704562154401414733632672828037238847169905891113099565690148943779591210868997584561045548052124737462759389731773455782593574591723191219370862660912

# 3 Loop Invariant
1239916279955871224148947865044105191634944605472080385645054315114433811615354286148450985471208422554265049874306499276379598157850486000595401638517386439413497478025868074616169068755593427697382175950425572735309473425829612480909092759785724004650007153806299/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^30 - 28183444389034027972334998097108892840245200772638614052152996067322707210062578843777511300164527511982470123413727559550022860803305312773197953834855930088662005925754693046437232240414903630063064017348860387064862903988265622360433830060274914333919502663308651/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^29 - 284769912972211676703794201507555786841543217384831198728701584683016757910362508804699302284629816328026039054524382852337904676262851296680222788298363361914019630071259984358297188084850234287020771096840252292748860938016102270023652575040205452935107672440437991/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^28 + 319269075521483377915517747077756955564930150380309719653257088298607821683002745055883855302999988731860379179018371058470877296291639882064377541478640688391254630320112286887524216231007631078504980021334711163194021615539708080021850907771384219848362620413102477/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^27 + 2721505854887065902030633822986984616294417458975757160166597273876421663286945804847696960200235602375219653136408146654901348552913204993788109186573350587984845664546934234821460690520257099047341173106684592160594093716740677401368744865027460195315456270856331017/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^26 - 4712843177918988455429613848674863028590298996741702694145028871548172161831826887651323719562836816869449209162086297486667958773316918446009600946052035884571690445774781976628071193986124701164457165494376033214704828574029115011246101325940271706653740196236792103/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^25 - 22278258493975798351846380727149799139706683955569357595842371806539266743982833094568112097528957667570494602717835335639684319408358139724016870062149827627381776576017588011330497527022734564650592836154802313800521017755178394720706194834718152602217436448107729015/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^24 + 39153268996823039708405776646262808387685237686476403445532930471354419353214034339606370154192161573753137766344427616586576297880471713463921606755684972383879735199036973806108151657187039570659496402923913641320315654215995080072999165116752428031142002457774030905/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^23 + 105084298876740538644384176088903133044995472074729879182251865625805388714936665723437060918979631402254022442013486895287344261947728343169303336946749509662101085289447687580749636539302596313426709423827289945547214809977750653901051493806023276831660303056200277217/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^22 - 393090477249166838229718882987122428751955045162611596422460092257431270569487701947274797635477951382847543170057585276978512996048966530778422302208977015343223418252989231332025462019563467527487491948671077847722889821886028987952101087448677249775915481923945671177/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^21 - 281177254453327687017711877839123387839094150788847564878132163403844436093181250443071458309454281861013302799688654633852486737774710390821684042007174595651949873347356634164411952740748586797917438416631843639705719320586716793309676559357308160423371652217784699337/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^20 + 317506710417759310067401726576782619321963199700671376378975645068279300564695122677048709901753906805393140834373454964346292072955849871488964451600754135242873219707500348443574481102438676098616893121647228662844876568038053619094285506295466483282834843245664388277/35346013426261659809036744200287778229562164023101716719579190893952299525356248576423283787167521556156037297000029112811503377521614815404435671137293395176755715272672332508346910745317502882747021876465104662188413558425380234120191200252321304166065117085105488*y^19 + 1199724970031645589832007820328445074286753929601933790818683229078996823895594735085177429030727466223809316863469348542617911698887263475936947921041202637798173996856340097594055215282137722047969980578940943924297964652192229295313153282669362663989788301215904291123/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^18 - 2586563919173036909390946014462562238695819934761630654106560090996762337190968283202637931180000483741225861193657192556756703162697648865961940508304584607900560127812037985784795402805207243375928428611652591544877029686699450385316604784356825049302455632789447719819/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^17 - 2183693395347220260340602113635299538201844947807631476373474651192205810969712967608630468106162992018936811368113405614296549252367632459648685117410520682853959560457133600832487985918875946761112363958646544372921199915204755017515661875601459656495404688664426982437/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^16 + 3929167669287696565314816510723011985111660459567225162880942283260743011541216387235462834172918302221529047013357274860359040094545965008767288354684760604729805269493818992791456002144814879955412328744740114798555688543025922068302431734838298130862340799089100164765/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^15 + 1533376142759109970181399537247075493455975071885739848139173835728963419096725595618644943495918593817741610236625470566638055623872907808330205910115920530003159567374067721025489139776609897106442588754202960340518402130374881493866268350056443775005586361659868378883/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^14 - 2173759665013389788645584696828447475597890883617496579330927685922342974367567351521688760450988045323977414196761794810990486456029451047430375973505772514214502322812282078121285233584808493638237084257325837498690825636730491420464867317429364629726896854763657249775/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^13 - 3844735370100249272285290953559380349344753011180251970386532606764197121915144888271019032774575921390507307107502253228709992495186748527900459605570829171530309761246135947756109261700452298616208715800318711786753852716288737502514731965251654726268389814277752535627/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^12 + 1927068853079070706829202352883482811258830677509455480356456177699732166143992427370611785342393643823553823244257344512401639935804452682345713468635825581792123560945345020285591381340230784716383968790768701683291367658067764041571045628199722007990101583515482727035/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^11 + 2475576940399936800194328634314892065959281306413427077468289682387537320257101740818603784658168545789583385128184697945237167255288657061021033764958149706286460791444043742656686531993399739681974597438772414325913859288427277138544917167842633249308038183138924824609/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^10 - 172159348596890115888316200962568406317913271415285153173019615030309530267921776745904770241066528980640856333810480955326030714977699633905144329776529957190362470701525571506415825833900387051294850845647554769807373354183713508272151000624739487789248743389420446177/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^9 - 827543471609051838034892305791764880022960985065348257718547871538915361140879473526271789827260889020916228792798365120391153877116024178345120604669285543667930051767135257186499453597655339483993034834468152071616638593014507304873593198499929020666171454196508510427/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^8 - 67782800531846167066665051727526707590624037488737932128045524486973666977546040487255615491813631709427282975278000916940842795106768535569856961900315563075173402014556416318421603083054990931408242969850753924549032434552700017546308053920165701094401244811198934099/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^7 + 151985798096367474752730764433931917586709572566107605844321304223032741777469364192833889119704785733648400627015961467467041532959137898475662882696243233887593026300201798385925858922909011356845738683749091165205258323471055537533127017130974526999080080411324037731/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^6 + 3527349435147310914281090461094738544497374608008456075910823150706899871163231469203012774446595791904552098462226765489520001418886424967284867659869257549838458092918439758139880416612391965139125223532667502101065916412696847279488475764850425486648933067355217235/70692026852523319618073488400575556459124328046203433439158381787904599050712497152846567574335043112312074594000058225623006755043229630808871342274586790353511430545344665016693821490635005765494043752930209324376827116850760468240382400504642608332130234170210976*y^5 - 14398185382110076744625429197382757317023946953533702102225883890772153483115270843063128814662071427323763931851828341818664884091652506179493275089325615475108754585962139648976017214494615159365642135709382559225074904476225977681523059576852402862380344013445246633/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^4 + 1629046071829076890785156073863581323165985737755851029362588584689378454768132461944312993003435750632610356485232327890445948607796348139258599849036770244504192129910586679119161695260627869016688487454468607395182715293114531105732630232534119650205828986381126365/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^3 + 424355784980856145233800048232511915891150116202138886936157128365770260222526945999635555128869483853177549564172171917993061012082221122702365497222372015578777084937520251556761543906320230264332840970357353714762498620455296755065615664010889922490693652168186297/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y^2 - 122973385693612152366511987770629631619120924775678076718572108980612779148126673101381125694420005777457943607565413676759416412855085170700351560264616805247482432302251513800020752703229339439130012535858698826703812278554417831291714490087885819802898552751880925/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952*y + 8876047828394243088187194585149395116074634704368660966720293063015201002659856159621357519206795408512130601625905898891384774696909766413581272777161706267963834351923297811861320546894932882883299170870920636230727748692514148753033049992519663822448318605750667/141384053705046639236146976801151112918248656092406866878316763575809198101424994305693135148670086224624149188000116451246013510086459261617742684549173580707022861090689330033387642981270011530988087505860418648753654233701520936480764801009285216664260468340421952

# 4 Loop Invariant
17529880403834784842958594614841714783006132517222791179815491702204991105423022394835803584949394453269449291146425259788700337531866140371834836588224810657533484436122687686181855516354354030417200425257438264937632875357990025904990639735689066542369895877153674031940078048061866164847787508204587237115435384160774059132138451762894354928319314202850591562187844074762376873/5323658375436428950810390654905582813696478148470492765325089908516110097132828357884940689315663490984690451778965083734821352085168027186500460767505028059557099716192342049271290134456266734435594329759496146149516895263497853844495929117827010770007411909653069279998305527889762048545998587253703187986519224699237939693059710939057584516911047144052051531305094099045663383680*y^30 - 1659858885360529843440213903175912933245615259578842394031841968689156471991528080777348419094786648291013569481976429424496833384389433513851960843023929815182605573948598843098501147402571271934198729045781219332464274563384574548356087107925347001677353932890598363467369635075287830780900688657428861281580278771666906206800682887558781271799204303368872680739989456603096634003/42589267003491431606483125239244662509571825187763942122600719268128880777062626863079525514525307927877523614231720669878570816681344217492003686140040224476456797729538736394170321075650133875484754638075969169196135162107982830755967432942616086160059295277224554239986444223118096388367988698029625503892153797593903517544477687512460676135288377152416412250440752792365307069440*y^29 - 69233803244635803649380518038182505323480001337812175916175030501965646279243717582865774273876322692034575648786916390511109698124346212391899162181691734425405219316161630975995387419920402997366070809468965911408722557017787158942277485197831346411063420593694744576638459266498835521709050790444445164321936816320204357467540751280137687507385202377401385592105466136823708750171/191651701515711442229174063576600981293073213344937739551703236706579963496781820883857864815363885675448856264042743014453568675066048978714016587630181010144055589782924313773766444840425602439681395871341861261382608229485922738401853448241772387720266828747510494079938999004031433747655949141133314767514692089172565828950149593806073042608797697185873855126983387565643881812480*y^28 + 233806549806920735810418976768678529961225401919381899743188361729075782478200371916938763910198215020458335702996238628102774531274213696005705349141905686830794715607480448187041784603156014049078821185565687537784928049620292658662779971743222300462383620670686285572374921741409658454694795944024640261150520617100543162325803599384482735152827110633782800264260320658738968913463/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^27 + 454686508715942868335336735993841394963289699052184139499326242525452086741087460512055035179764159711102756819417038095423793524406820634064886835656601337006652314746989938592871220903633065606460749647808060933150257883372216179169596197000901851183265221684913324631503237848841049362125043353194775212774497823024186670310156033272906228909076529858010012000119979553752488897681/63883900505237147409724687858866993764357737781645913183901078902193321165593940294619288271787961891816285421347581004817856225022016326238005529210060336714685196594308104591255481613475200813227131957113953753794202743161974246133951149413924129240088942915836831359979666334677144582551983047044438255838230696390855276316716531268691014202932565728624618375661129188547960604160*y^26 - 3059593555031659312307805989561168467300708077766630464693447189357644619639162861874380214251473533819729563311716196554657877149591295791072772485763421743837481011064461466705537536426493703244265520942102297715401306129109721985340242297468710002093964564142812724616299844962644755318308682813036222850060129433997298892632943273563797964395823534187590439992246600570367011539911/191651701515711442229174063576600981293073213344937739551703236706579963496781820883857864815363885675448856264042743014453568675066048978714016587630181010144055589782924313773766444840425602439681395871341861261382608229485922738401853448241772387720266828747510494079938999004031433747655949141133314767514692089172565828950149593806073042608797697185873855126983387565643881812480*y^25 - 5263480704975984134438650914847642935543665395374338468285759332131791748716189010331354530777010115147534985464080336319679721940066431561619040576244742908262208025104978730637735142235538014756512981229824561444999944815384486283468026830090372556777655321747693602319276936580128387621192470540482078341175157710255334284570446568395370708915016288252639641721085612643776906107307/95825850757855721114587031788300490646536606672468869775851618353289981748390910441928932407681942837724428132021371507226784337533024489357008293815090505072027794891462156886883222420212801219840697935670930630691304114742961369200926724120886193860133414373755247039969499502015716873827974570566657383757346044586282914475074796903036521304398848592936927563491693782821940906240*y^24 + 51255905276739343394917999632173315792714224843170979108732167394761472754424231142293474984588401395963165573347426555076328798949583186468098846845020883336174137648845605925905602612226421544113275237466975816563322801850317284709317779722376134773908093461832128012101906697192375786852122963478494654312473845769198155491325447242357145480233455993260716519681860426661563219219727/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^23 + 10417630770583368846805952804553970139871641487979805256332862921989575560535354112704489937926104748781524027676056656731426812087475972350449183173461220649760846020445540266054433122495966121060179113567183416272808533246580874536842635882497814950720727151765735430645534175687058684473385834860150454373219091239039390936605051327030460268209371123204193426453647465600690251709339/42589267003491431606483125239244662509571825187763942122600719268128880777062626863079525514525307927877523614231720669878570816681344217492003686140040224476456797729538736394170321075650133875484754638075969169196135162107982830755967432942616086160059295277224554239986444223118096388367988698029625503892153797593903517544477687512460676135288377152416412250440752792365307069440*y^22 - 85450289723456999987957518670953200983601565596338214929901455792104438036441406656130256115928159916488124963373067229801155864709055808147334155631300154165771781015506300363003852238196014764938424991220548373947922174871938231170072509725075931810543670997766616341114858645230981105718008036547977287156025660152236275970825911774770859054062058017071368991010683502110519367046289/127767801010474294819449375717733987528715475563291826367802157804386642331187880589238576543575923783632570842695162009635712450044032652476011058420120673429370393188616209182510963226950401626454263914227907507588405486323948492267902298827848258480177885831673662719959332669354289165103966094088876511676461392781710552633433062537382028405865131457249236751322258377095921208320*y^21 - 219803498787356147621422994448246580117240378082606574785833843198509086731858158269049885515233537771713117265834323504817005378636175284433889881994939408510127383759461109689904149321749676945122594255249605426115071326212106561565643324738213750516980270864003827552729806446731377162310859431158658116742155798242923713342682160275435616320270288361050486762847905866678472186387319/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^20 + 202804861452966035383621042879999219934695856514815449720192651127033729626850504598452318721467169030198992906404589538497058234338854526301674953674016620391472477445919775922187816140471628134960323938616617381385433215692985525358888405688774462764886838484742477466804305042284336191120264588145556416659252298306036931125318732953882456232498740047779798526262046542450710056421823/95825850757855721114587031788300490646536606672468869775851618353289981748390910441928932407681942837724428132021371507226784337533024489357008293815090505072027794891462156886883222420212801219840697935670930630691304114742961369200926724120886193860133414373755247039969499502015716873827974570566657383757346044586282914475074796903036521304398848592936927563491693782821940906240*y^19 + 389402612549480673513662301322754587286923419001658256622028166273407634765965876149002646590408001630345089733178415107049224237105112763526131960909456022539128064893512551157012882914064728669683275777829260199904072880564558262350997270547282474389103378692132908615200532423215037084193481840946225215818623342786977598611588880146417056338011379332554724535649727454362882775717731/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^18 - 5331749515696507847352144303491432708433998472152957954950588053877011310186471903842544695707768545871058935280323345971303247839280111341278709910250202011803209576833324007300053651370017468505858545651722628603624374576769942132422086294270781078510285890276682081564853444310234818604700879440134384161681383248700020811250462585198202136722672607554156122887380644913454605194737/1197823134473196513932337897353756133081707583405860872198145229416124771854886380524111655096024285471555351650267143840334804219162806116962603672688631313400347436143276961086040280252660015248008724195886632883641301434287017115011584051511077423251667679671940587999618743775196460922849682132083217296966825557328536430938434961287956516304985607411711594543646172285274261328*y^17 - 172754229583709662418365256932513039422813530942767796992759592591696056416623140226471516804204703288889398572394338442669944391220857728285601831748428487181980275860823781316941430595282552787683084872943097408245894543005592894811343390236168050244355478347473916766365606459738754717032046677278534877693500766384886591458073279139097213334970739454562597139590452028815888834287881/95825850757855721114587031788300490646536606672468869775851618353289981748390910441928932407681942837724428132021371507226784337533024489357008293815090505072027794891462156886883222420212801219840697935670930630691304114742961369200926724120886193860133414373755247039969499502015716873827974570566657383757346044586282914475074796903036521304398848592936927563491693782821940906240*y^16 + 543667126533429987602748780758467907329657215859168154168900882299054761801985464091771066039335163656134979931575457715587364569576162341421299452783912585202029747416676704577353739383261674724315974923532375297081003099985104191025425055591561804511616161273225303651111558660303848215535104649132875332823113978221908207193662951326420665305355302032080858800383900153098759645610015/76660680606284576891669625430640392517229285337975095820681294682631985398712728353543145926145554270179542505617097205781427470026419591485606635052072404057622235913169725509506577936170240975872558348536744504553043291794369095360741379296708955088106731499004197631975599601612573499062379656453325907005876835669026331580059837522429217043519078874349542050793355026257552724992*y^15 + 61766388102098012812320846515473966977540952441767183717076786651784382095702569625987495938582083644525051791350476903795283919040675546880307494193870997530785119768840243868231523343389932756768309774457910523635133735158419124616186672237027722734301539851273190726009218673565169771285573625260389143789543896936555710463015239423503498387849499939498684055812398277795997411478361/23956462689463930278646757947075122661634151668117217443962904588322495437097727610482233101920485709431107033005342876806696084383256122339252073453772626268006948722865539221720805605053200304960174483917732657672826028685740342300231681030221548465033353593438811759992374875503929218456993642641664345939336511146570728618768699225759130326099712148234231890872923445705485226560*y^14 - 535353198166999676481719924320276990868249618877755470024216902185151557915504692025899992651662747812136083487119025164875596711205749978774006837727864497552833949877925233461045276947873610513546834582558973844530682726102119568096988805947907446563413551979737665149382587985245722161693522912959074521170332469183627803445858027859044003719216635131405097749666598542334237073341747/63883900505237147409724687858866993764357737781645913183901078902193321165593940294619288271787961891816285421347581004817856225022016326238005529210060336714685196594308104591255481613475200813227131957113953753794202743161974246133951149413924129240088942915836831359979666334677144582551983047044438255838230696390855276316716531268691014202932565728624618375661129188547960604160*y^13 - 19875911973366593601903544207810805127947197447458800684880702918647017593238153175862639758574692492119347057175041584772174020880878579718526988343366433163080890055738973795984651902595941935340266038035477147218181537569237974856595416924133323256636370626845631592137623639864193826816566711270898713467021792202056084661457903686428529483444143310135785700683218549941296665511747/5323658375436428950810390654905582813696478148470492765325089908516110097132828357884940689315663490984690451778965083734821352085168027186500460767505028059557099716192342049271290134456266734435594329759496146149516895263497853844495929117827010770007411909653069279998305527889762048545998587253703187986519224699237939693059710939057584516911047144052051531305094099045663383680*y^12 + 535677717699680877761962701438145133099813829095766888205230323998822231786404554310621624152978271814641383754663983838636683863331379371248423029666332788747092521592575008043512145460038937591752275735222022973096262564298261984120709654657522011834044582836407018771082939287649321132162707904829808213383719130517319007685177863257038917649482235012077962828664781931103646675731841/95825850757855721114587031788300490646536606672468869775851618353289981748390910441928932407681942837724428132021371507226784337533024489357008293815090505072027794891462156886883222420212801219840697935670930630691304114742961369200926724120886193860133414373755247039969499502015716873827974570566657383757346044586282914475074796903036521304398848592936927563491693782821940906240*y^11 + 7750726832162098151860637222421731499770603274602927461672520190871194175078664952147852491578659834828301100142567266906808720635772208075960481893175097225695543082319043407186818648441708137833142019752275835164912275100477540731096021049652698055106278304753932738535905347307377171001833011617760198151871854338907706259111097921704337651565351166840753490827844194775563842262903/2129463350174571580324156261962233125478591259388197106130035963406444038853131343153976275726265396393876180711586033493928540834067210874600184307002011223822839886476936819708516053782506693774237731903798458459806758105399141537798371647130804308002964763861227711999322211155904819418399434901481275194607689879695175877223884375623033806764418857620820612522037639618265353472*y^10 - 30049131104474270825240045731189758861376814317269219121242503625594777568048949293575052378428855446905542410835641647141980820057376780435353537514924339819444012077454113143883163698180900280342241360219334552637991620558346819417056556442692180249686240282728605259218537053097657842072851684659755000518683660904335634134952973574613545872115947270039904919244692521231576066261893/19165170151571144222917406357660098129307321334493773955170323670657996349678182088385786481536388567544885626404274301445356867506604897871401658763018101014405558978292431377376644484042560243968139587134186126138260822948592273840185344824177238772026682874751049407993899900403143374765594914113331476751469208917256582895014959380607304260879769718587385512698338756564388181248*y^9 - 161332796224384366543620716528299468502923365979149426427157913858520157258440639277343609865727349941722569418787955617093197018082647691577271589448640475518347140250223992371608301999438380667615937149086933477876315003716062097124200562691125405845799901457712185716052855685352697281653668693986066776882678602014086065120229703962839776352839021897239717710377696459634844001206973/95825850757855721114587031788300490646536606672468869775851618353289981748390910441928932407681942837724428132021371507226784337533024489357008293815090505072027794891462156886883222420212801219840697935670930630691304114742961369200926724120886193860133414373755247039969499502015716873827974570566657383757346044586282914475074796903036521304398848592936927563491693782821940906240*y^8 + 23668451953673154783525742888258454834407779566780935411645311066760959405909691555871968732879771389717770528313167322587762605660043072490481492808560559296099141445304315412429593367573725362517076624673758573070651211432065570604647918746697975357625520703094493830576546725243532876238930282978706846227819014130849065836064363501561429232807467776826368864619394304549664539497583/191651701515711442229174063576600981293073213344937739551703236706579963496781820883857864815363885675448856264042743014453568675066048978714016587630181010144055589782924313773766444840425602439681395871341861261382608229485922738401853448241772387720266828747510494079938999004031433747655949141133314767514692089172565828950149593806073042608797697185873855126983387565643881812480*y^7 + 69188621573444350352444146308541295946357778942715029872809793293165088332224150922428651596536017711550174446762904552274284426513052599672227200762767429458014253800008876550103417599889212773863537394189987158736260977823462793252319904962952178508364741675775723306261452028826383809866598783643850428702407893926311651999229332667369301734235233202011980043369736194241515323262009/191651701515711442229174063576600981293073213344937739551703236706579963496781820883857864815363885675448856264042743014453568675066048978714016587630181010144055589782924313773766444840425602439681395871341861261382608229485922738401853448241772387720266828747510494079938999004031433747655949141133314767514692089172565828950149593806073042608797697185873855126983387565643881812480*y^6 - 490372621239120359619850238782820501840821844624975406853307015727950879204646011781131484162651364076952973526904775641060563340187338906030783137232741337878831277545878001993394197423905003499724391060702408283329394530050390246920159216673202227770090460549298319041533192971208833306616527310104962137321839294164549463910744812022016880065276041037979610997999099773709255617637/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^5 - 6299069128892701911354102162178533119874898140272095100093254310345247178594909074485929807434116820976447289084288094828957557377799183954453173557811249222423958919541649655838089566076809410867853134060776490081358231455147082962096725737651611030068828315134091409028834769751302177890358752756752452611185330456534376751381021893166309412532220303011814096371735491551218571256667/191651701515711442229174063576600981293073213344937739551703236706579963496781820883857864815363885675448856264042743014453568675066048978714016587630181010144055589782924313773766444840425602439681395871341861261382608229485922738401853448241772387720266828747510494079938999004031433747655949141133314767514692089172565828950149593806073042608797697185873855126983387565643881812480*y^4 + 1204256817259256027552845294411593662606816132875088767722157579269353177807294294252634085948216155270493429092027605853457977684042554080034315365633137698842216390437432452076090532143670413910172804138857406463524598788645665268049370945408488680847213629685375953513665401914181291376692874087933581972104197216621526743584908905669434671677123325911194980339311259228393396024461/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y^3 + 51509277847953172509284992753755744155949590476367534366325569425001835649027561011209012538639962385029743638037503336734943130158091148959998491912418530610029249005272289635034239842554111558294903366218507607288570674943883899260714721447833918510555754377083465082854436200178356034202903118943108467148056212237250944149564492471711277088176536885764381434555641752736329889893/63883900505237147409724687858866993764357737781645913183901078902193321165593940294619288271787961891816285421347581004817856225022016326238005529210060336714685196594308104591255481613475200813227131957113953753794202743161974246133951149413924129240088942915836831359979666334677144582551983047044438255838230696390855276316716531268691014202932565728624618375661129188547960604160*y^2 - 93231092921160381625018113303892265474962561980185891918192973238280270031599800767316998676466270860627462509484912357950500754967609760867645710648412553481649962538445142910778177286058531813011895951803038424567673720325911892365656737601218402049257424412345833330693252408328137004031465248709760833117433238890363108245259180149529241713941385221419944526387753652457446262669/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960*y + 5168871732107109212176963841984700264019784523122500721077303597817137515748722336418818199340633033299032747805406465122471902349071337421135137526684800772035093225684771180159983816529342752877628990207681176266101049704087115299961444771911177672288500136682287791121256062626327624929728474383751858592838865394469500201988651672398468350551574867612860208289184840955678715781/383303403031422884458348127153201962586146426689875479103406473413159926993563641767715729630727771350897712528085486028907137350132097957428033175260362020288111179565848627547532889680851204879362791742683722522765216458971845476803706896483544775440533657495020988159877998008062867495311898282266629535029384178345131657900299187612146085217595394371747710253966775131287763624960