Recurrence 5 lookup certificate: Scalar0Main coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_364 : Polynomial.coeff recurrence5Scalar0Main 364 = (((7146962727707921861272116329089706666677 * 10 ^ 70 + 5674481770291097356689484383319573621959357568893276086818884011675141) * 10 ^ 70 + 7592008919944187740858831372177715788485326055325663494829024460953625) * 10 ^ 70 + 7150990330381802117625038655658318293800234259752926606659129713410318) * 10 ^ 70 + 5058691574665509889410267256641965996804448071051977631285720604706256

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_365 : Polynomial.coeff recurrence5Scalar0Main 365 = -((((2623227210370648518776016836441982555192 * 10 ^ 70 + 8427682998399430926933350944524079124473100189569064350500260073316270) * 10 ^ 70 + 255207547219281832043507633136881531346668097885877074044883957505446) * 10 ^ 70 + 8144246193912657440324261490595258709691891963158953141070104642346326) * 10 ^ 70 + 4134184864715396623137293788868493709700854197416249991114594667921577)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_366 : Polynomial.coeff recurrence5Scalar0Main 366 = (((942940802097640824588296022276186037777 * 10 ^ 70 + 9813448873106028194639129963688857965778540272636300223558369373811190) * 10 ^ 70 + 9769854942143274325506027872918360925075265124402535821650554310274189) * 10 ^ 70 + 9345349079668337075583859666331392816109063026542097951686324064230308) * 10 ^ 70 + 1604418124907613400495961696233638267236586406601928649231818566209341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_367 : Polynomial.coeff recurrence5Scalar0Main 367 = -((((332245373275882828910455485489707299352 * 10 ^ 70 + 8264473105894075738939482634401807996715304777785288635910920762293203) * 10 ^ 70 + 7572189720676336116743063741647984465374001144383788125272463272849412) * 10 ^ 70 + 7670208560475012947499798793088577479287921835662206270816551463119148) * 10 ^ 70 + 1662274794953837217714321128011684287535930911212511476223561907242657)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_368 : Polynomial.coeff recurrence5Scalar0Main 368 = (((114764279843929015650833732212103062930 * 10 ^ 70 + 7702681413886189291684167381163150172949291674574039928313422728697236) * 10 ^ 70 + 261651458309960622577760003862426424525417324295175647141765819120880) * 10 ^ 70 + 9175480047563430639004428011867016197301494632504093125519082999808419) * 10 ^ 70 + 8855616944527233182358466537481764162719822731326994737170463984013386

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_369 : Polynomial.coeff recurrence5Scalar0Main 369 = -((((38848948815364981371013855561560867677 * 10 ^ 70 + 7884477997024173863285582379886220808334584982280998248323319496975179) * 10 ^ 70 + 5961962640510462759371778186331495935457950984389221489207796881677794) * 10 ^ 70 + 6247411808904497820535048501895464653117958054115298471739481547349917) * 10 ^ 70 + 8594094212404809452743270148446596751624048945876932629383471517645466)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_370 : Polynomial.coeff recurrence5Scalar0Main 370 = (((12880282337589060428082414555392521714 * 10 ^ 70 + 3733848828784335745041469494612623401228401861926662418962998367266302) * 10 ^ 70 + 9998828475134733074425367328542810246781151038688874157697691488160490) * 10 ^ 70 + 5831848173858712094065567099994539457378363483637183547267039177296275) * 10 ^ 70 + 1960810007308809372775289760836172511284802360055520545114465115868743

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_371 : Polynomial.coeff recurrence5Scalar0Main 371 = -((((4179720295307195820341333329092103279 * 10 ^ 70 + 5035287453777001843456433611758734602096906436475669448412205766497500) * 10 ^ 70 + 1021706724701049605063844369967944282924436601786450858910102232999535) * 10 ^ 70 + 9689261991525791551056825619357292514098744252822910536098201311446769) * 10 ^ 70 + 4013946625336697390110968819089249811138869282487428136376220648381457)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_372 : Polynomial.coeff recurrence5Scalar0Main 372 = (((1326568029668631628914708280255312152 * 10 ^ 70 + 6172508061529661803531455127698200434575815587923153176243534618455944) * 10 ^ 70 + 5298675737168562414127341031538666795190648238075597896612479487054423) * 10 ^ 70 + 794368637724032966523192686955382794097197845630503858950786506978724) * 10 ^ 70 + 7772452505530942816429793104797742905863636294503286764197574220935818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_373 : Polynomial.coeff recurrence5Scalar0Main 373 = -((((411480143879523214272993041304987560 * 10 ^ 70 + 3167458453669120330640932765420983799628718405055722585355045958828475) * 10 ^ 70 + 6281074219128369660159191131297317591032530890513693665729516879592838) * 10 ^ 70 + 5461324228768351598281165480643906251935695122983198235067656662578491) * 10 ^ 70 + 4907928867915542661306358191400333799033511587146077473010723213647865)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_374 : Polynomial.coeff recurrence5Scalar0Main 374 = (((124642927944712374963857532190788475 * 10 ^ 70 + 6588380848989715872764583701251831798242065850024615332265267099915148) * 10 ^ 70 + 5867638848817907798214366082688580604908680330704138468517093238148921) * 10 ^ 70 + 9210892897699196063172489983360025752494174732789231631418695312347403) * 10 ^ 70 + 3433203562355743278513639354012556617899999980991433874543646218505218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_375 : Polynomial.coeff recurrence5Scalar0Main 375 = -((((36839748153129565568938132749434003 * 10 ^ 70 + 774229000276526695889951880478396078499497662682519021640928389783760) * 10 ^ 70 + 4281528248727273030413759098284103323018390134136722715278339333031470) * 10 ^ 70 + 7050447852641349674175248070449085888307524581304102935890064881837014) * 10 ^ 70 + 7606646689175143701194666049220988881183049925569757812557917564253631)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_376 : Polynomial.coeff recurrence5Scalar0Main 376 = (((10613806361813187693736929826066649 * 10 ^ 70 + 2707416648643549177461558067667055014143309649163796157411780451428626) * 10 ^ 70 + 5534858807465909002517827980552311558928735781767182501704422044457831) * 10 ^ 70 + 1963072251777552942133670173274134435220818771878075539187669377399952) * 10 ^ 70 + 7184051033678559059546168836392377262112196499837764497904915640779994

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_377 : Polynomial.coeff recurrence5Scalar0Main 377 = -((((2977317226242300327864037051435895 * 10 ^ 70 + 6444344551360624392609287652406275117069190979061592850515458354354639) * 10 ^ 70 + 3792601172959914999286724065823893920407179738682200398137517858417889) * 10 ^ 70 + 4577106555516716399751820851582566036086444884686238637204356126708498) * 10 ^ 70 + 112299937285778146407133863697958683344036793534433095025714079955652)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_378 : Polynomial.coeff recurrence5Scalar0Main 378 = (((812026096738758273535431824200792 * 10 ^ 70 + 9948170206014855438529835624066156971610446885160747312971751901992668) * 10 ^ 70 + 9121668760307916575174801379939063558312968448011134857050255707230492) * 10 ^ 70 + 2357090555920904158591443490864774376235623435215280313356276064513578) * 10 ^ 70 + 5853149015456318162154148358218178665855814014197957345063156212610501

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_379 : Polynomial.coeff recurrence5Scalar0Main 379 = -((((214973562088816272115360285163399 * 10 ^ 70 + 932657483364217268634372384655104545183189115774833910730110029509076) * 10 ^ 70 + 3105569121152420747456832052031316724108950371023722011152142473109022) * 10 ^ 70 + 8702031114848101611188265808891056817777333157400767467491233096706883) * 10 ^ 70 + 456378951783990203041147120268909795661093633534904486762649816365964)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_380 : Polynomial.coeff recurrence5Scalar0Main 380 = (((55137424235682532992506501633856 * 10 ^ 70 + 9480722263271310721025992382952517212981975114749480702151502041846117) * 10 ^ 70 + 4088026042495298784022042225479907828234945878829150653645152434867528) * 10 ^ 70 + 6516807840339811418289861839104043226899571264635817285041803233171823) * 10 ^ 70 + 4736248367748953926860815958244858872691835911317217048504316584718365

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_381 : Polynomial.coeff recurrence5Scalar0Main 381 = -((((13673011224297711244294400855240 * 10 ^ 70 + 5865236873672214531588740623114593653374989508688277988246651419091963) * 10 ^ 70 + 4134817350563610201068875496483495194359021030192773347646750800981942) * 10 ^ 70 + 4409729215864744843754614811935814197959016696604552580789874531694908) * 10 ^ 70 + 5813104155633307973934043733933160587852474563389074117295734660378840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_382 : Polynomial.coeff recurrence5Scalar0Main 382 = (((3271592590047326942517227805356 * 10 ^ 70 + 4884217424255607609632846000680437155995939403784725440051148715356208) * 10 ^ 70 + 8342962438824763971609107941378375052037780210853514000570709017625869) * 10 ^ 70 + 5590034776177537222077165637164528348383284837437094490792885379322353) * 10 ^ 70 + 5720225120821320367486043199749698050431880349327084825894375168185227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_383 : Polynomial.coeff recurrence5Scalar0Main 383 = -((((754057295857586083273922327987 * 10 ^ 70 + 2558806870934222495871284668919280746075119289651152090389513934503675) * 10 ^ 70 + 8586175184819965684451250460103653089384112551904439441960615000954955) * 10 ^ 70 + 5605509775136621492789571805325806494368674009219928246272960885670636) * 10 ^ 70 + 555022298839410176862693005678633026438528442844671440044377701576169)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_384 : Polynomial.coeff recurrence5Scalar0Main 384 = (((167289937038198780582979926980 * 10 ^ 70 + 6478492485436929350172297934087493541549486739727706212994261046638438) * 10 ^ 70 + 8924547283028582941135287929354815895930397446859782906041970925618277) * 10 ^ 70 + 3368955943947671121410991207778060133351507580854908852564411030967832) * 10 ^ 70 + 710379626806775109937420184147574817100320429304748641789592979696067

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_385 : Polynomial.coeff recurrence5Scalar0Main 385 = -((((35764239849705524005096649250 * 10 ^ 70 + 1054535093863385335228704095327973966697976653307728921292443439542256) * 10 ^ 70 + 7112350477271331441325435431632105825653269369867868341650473219532857) * 10 ^ 70 + 5200188499366184928274403763088318034639488866229934340239482943090146) * 10 ^ 70 + 5352404266188604418256846025719980616308622405693616110108881118288297)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_386 : Polynomial.coeff recurrence5Scalar0Main 386 = (((7402344305072828995584062010 * 10 ^ 70 + 4771912664115116163708668935209373183966345387396904831281531556494961) * 10 ^ 70 + 1397947639288492356465342727015915871166206095772352584887090232958007) * 10 ^ 70 + 7585514653792984811841910034163113718795931490743170169415027860688886) * 10 ^ 70 + 3289287157730861632861285215896532296843834427786939021139441176095067

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_387 : Polynomial.coeff recurrence5Scalar0Main 387 = -((((1499152984519948466088175529 * 10 ^ 70 + 9878561838237756157152796670123175432809096469443315712246791365827670) * 10 ^ 70 + 127133521590075600404369344257970562364179603234901371384665617490734) * 10 ^ 70 + 2077797845433609270576675105966939454294815572918339546933243325781264) * 10 ^ 70 + 324798689992417220838608177669846060848730951282491604279356876956355)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_388 : Polynomial.coeff recurrence5Scalar0Main 388 = (((302808491172372464514240385 * 10 ^ 70 + 1802421090799160576643523892500199263818926855527141382063518807317695) * 10 ^ 70 + 9482342409741156951619052359672821265240932258037748887732399727220728) * 10 ^ 70 + 3438971239015000255950434535303349994577781567927104148611816279108952) * 10 ^ 70 + 5463452187475609824188674796138971353528344824076823687052654811300091

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_389 : Polynomial.coeff recurrence5Scalar0Main 389 = -((((62674700576660066642970278 * 10 ^ 70 + 2909353090380673312565040611377219094377204443355513025700999183990327) * 10 ^ 70 + 1134480090494043304525381385578328131636220897831171387060018451247738) * 10 ^ 70 + 6449378362779971822137925412409806873308639005682955896181509472418334) * 10 ^ 70 + 8397772631935942953301709984736585624708115589282434997368269392061503)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_390 : Polynomial.coeff recurrence5Scalar0Main 390 = (((13649816359377534571037456 * 10 ^ 70 + 9088537087886186632676095623003848439480192137667343229358177159147933) * 10 ^ 70 + 5424410309381288405453080043180498133687090957522238729395296838755331) * 10 ^ 70 + 3510352897309828641088539232595932955662137842559919712688637701382834) * 10 ^ 70 + 483497040662889093160834485714623600813165505895862270835120006076782

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_391 : Polynomial.coeff recurrence5Scalar0Main 391 = -((((3159939386108625948815919 * 10 ^ 70 + 7515151287449363284894383151719512874873906456609789652884797532593782) * 10 ^ 70 + 5109438101505133978992132137723695438614072403196136005332824940543587) * 10 ^ 70 + 2740220681611148453734027010588767764101194353883806961902004681891008) * 10 ^ 70 + 8777532372730257456775377549213239529710873057447027972769080417433757)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_392 : Polynomial.coeff recurrence5Scalar0Main 392 = (((766319224235183960115476 * 10 ^ 70 + 2719764781070493828774694014858712456989567609105510874478302294036884) * 10 ^ 70 + 8171705594741164560940329790313594106043006158157760774822630164149049) * 10 ^ 70 + 7298396521078417415382268963178020972357258491999602344569383880545631) * 10 ^ 70 + 4740779783422302813591856889846207978139297245376256922701785218773663

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_393 : Polynomial.coeff recurrence5Scalar0Main 393 = -((((189001235557261530176071 * 10 ^ 70 + 6785848366090202135117900137057024684455035143638155488282336692508992) * 10 ^ 70 + 728617378915301045649989939039888959275871576853184119843248652831942) * 10 ^ 70 + 2989964832210599045361191418428948496843833446382183125665560822438989) * 10 ^ 70 + 8853281281296585641348474558708554585443407459886400847963303127888012)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_394 : Polynomial.coeff recurrence5Scalar0Main 394 = (((46090698967703818114807 * 10 ^ 70 + 2801138556376002549636840834193149937182488666751515524680713126088268) * 10 ^ 70 + 8159400847343748481531315383266923886086545453760652525522762036748978) * 10 ^ 70 + 1370176974223084296748250054887952413684942335396961310528389007426179) * 10 ^ 70 + 3263802138563418523057501269765957346160511749669440888722383308070009

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_395 : Polynomial.coeff recurrence5Scalar0Main 395 = -((((10920473915592416082687 * 10 ^ 70 + 3647199216302693302576452549620238664458484929375210390507691263068445) * 10 ^ 70 + 7894992009314093621486987926733821986576227332929720962661025339630554) * 10 ^ 70 + 6020102958675426232196994028726906100840412363765631871065875558549074) * 10 ^ 70 + 1888317320373643558089878138539793408534631325758710599640352390679850)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_396 : Polynomial.coeff recurrence5Scalar0Main 396 = (((2500107150456819600997 * 10 ^ 70 + 8149976371440611203998532954631265238753905532272247211848059034341422) * 10 ^ 70 + 1151202094794812177728559271083667624032432942255633850670808996847628) * 10 ^ 70 + 1396832825388288968092612414747973930919346187527653377488764578255977) * 10 ^ 70 + 1555802987630661570107897694020202544743015832070291668562789072784563

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_397 : Polynomial.coeff recurrence5Scalar0Main 397 = -((((555311819374579146618 * 10 ^ 70 + 3835303960165322592839942087080245607826642748310630282705135098402447) * 10 ^ 70 + 9754574502551645765201572816397136639397808322533523928937320411484785) * 10 ^ 70 + 6500497803695553130788917413200639635974132108394307184201944578912826) * 10 ^ 70 + 2684062440563475767943484606597594243690588656650257049774456966166880)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_398 : Polynomial.coeff recurrence5Scalar0Main 398 = (((120640162950606750132 * 10 ^ 70 + 3097909175957900720716000856633735851111604181652343230749792520483926) * 10 ^ 70 + 3987565843749062946861190888816117128166883076257157964662065152937553) * 10 ^ 70 + 9897642685633600999076756445138766352873598325434061556821054637198637) * 10 ^ 70 + 2669472400553511831933796075322970313436809468332104263343009039658103

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_399 : Polynomial.coeff recurrence5Scalar0Main 399 = -((((25701625645714149100 * 10 ^ 70 + 3880580380998636470549940127957252115548329657430810978518629400084291) * 10 ^ 70 + 7805338961629077908445038105523675176820570932540276318787600928374036) * 10 ^ 70 + 5731305653785907952447765697663252058312277406243479601437077018718216) * 10 ^ 70 + 6368833437328097249505084250649171139923477867001804397500930964168771)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_400 : Polynomial.coeff recurrence5Scalar0Main 400 = (((5296879527006933665 * 10 ^ 70 + 9885130827995060264086875486110631858855679932582017223979817343547939) * 10 ^ 70 + 6805075386021644865080640455951941921150325507627416829940583402561143) * 10 ^ 70 + 7719267227822943087740511999755766875139749106430154038760792544717266) * 10 ^ 70 + 9116966441983438081907960721624846369093218571604741931872323879994377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_401 : Polynomial.coeff recurrence5Scalar0Main 401 = -((((1017332262402784585 * 10 ^ 70 + 1710982409430354942375147193556409488877079346792596054481687610811476) * 10 ^ 70 + 9637256415355022357760080881222110451343416031521204327873207992545455) * 10 ^ 70 + 6476036749627992321196009093259912530023111663986174358453809286620504) * 10 ^ 70 + 8724260780258409647353155831704640843994835203088709888350367945044542)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_402 : Polynomial.coeff recurrence5Scalar0Main 402 = (((169524541197688461 * 10 ^ 70 + 2836954851038039002768485893176686673579544844471307745359283264759146) * 10 ^ 70 + 291416108077576282896836033573760485360512118806416401087280070776742) * 10 ^ 70 + 4615473818302557399728964317377136415899020569285592670983365141519108) * 10 ^ 70 + 4092320700438912465114257518420872620221078938780530256514328679047575

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_403 : Polynomial.coeff recurrence5Scalar0Main 403 = -((((20643876190427402 * 10 ^ 70 + 2976498636051615735479975871887196759816418749923275532006610173934032) * 10 ^ 70 + 9365206296838787058021706819979157220818140963630069191772061264101855) * 10 ^ 70 + 1368149916529335581587838771239410203864960418694607399248309492439312) * 10 ^ 70 + 4799637380455523690561051897069994655741376004547030737851371688607405)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_404 : Polynomial.coeff recurrence5Scalar0Main 404 = (((374139836899938 * 10 ^ 70 + 8184575585117403718251174824605200871957337596719462933148390927153833) * 10 ^ 70 + 3787957114060857598281827027137296229778188994920511678599009682850493) * 10 ^ 70 + 6551041991069660166771806611710285666082790637674646404509689800225183) * 10 ^ 70 + 7753358038465561301080454885668682400426703828073707893296847018832264

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_405 : Polynomial.coeff recurrence5Scalar0Main 405 = (((742486097889676 * 10 ^ 70 + 7719330783048619436974702206383044916431002923403522971050493926920454) * 10 ^ 70 + 2754049417933885462634996503465839437493204621802786235456628680905556) * 10 ^ 70 + 7925122953770234125794916154996523944767454045798204515377321034730112) * 10 ^ 70 + 786705157185599538163161410426570268658437156438858982864204961519303

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_406 : Polynomial.coeff recurrence5Scalar0Main 406 = -((((280836470138840 * 10 ^ 70 + 6794975729544039585396882413202769529640724717403389292940676146492036) * 10 ^ 70 + 7545392910124614840399800568113826146462960501628192635451107494066052) * 10 ^ 70 + 2569930973677815826367007218393554135219803871160975977481850759902682) * 10 ^ 70 + 4052798979356619480849001989537120807173757060059512479416067120216707)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_407 : Polynomial.coeff recurrence5Scalar0Main 407 = (((68912979107681 * 10 ^ 70 + 871619481280341615131505787180395858090123770067716593381175206550248) * 10 ^ 70 + 1360954948679185161457803829912593388040480798417290305928694616007148) * 10 ^ 70 + 7640420584196034133500797497611385384712768665260510452039132883014152) * 10 ^ 70 + 501784376850554804059578148848032346261491762621223280843349179565431

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_408 : Polynomial.coeff recurrence5Scalar0Main 408 = -((((13127087900858 * 10 ^ 70 + 7964239204235184567373756144698973117759979633408814082064375441413889) * 10 ^ 70 + 7471321432238241285901818214075292971795772184856395962691595337224940) * 10 ^ 70 + 2156669918293472961709547986036493699669396986999481072140550209354455) * 10 ^ 70 + 1181982484562921500364278292424517233780987126363196575904188603246354)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_409 : Polynomial.coeff recurrence5Scalar0Main 409 = (((2007622379995 * 10 ^ 70 + 3815575652915288394847991501154340080477235438532722578638671825683801) * 10 ^ 70 + 7745816334450176213056115681379211275299738947481751725496303597840828) * 10 ^ 70 + 7371317128395477763275445007461347785050355230010287045471807503163329) * 10 ^ 70 + 6609476431755190028903428149972387316380265645505575512686253718354471

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_410 : Polynomial.coeff recurrence5Scalar0Main 410 = -((((240763502040 * 10 ^ 70 + 2914866868965240233572377503729213332398160877585942135000908330626806) * 10 ^ 70 + 4700467336818905014073747072917072530687653260312884929992865795403112) * 10 ^ 70 + 3176940838932640318576183244719434521266586795034855320617208254779699) * 10 ^ 70 + 7917660794294471786900075893515473835496958659291939023848953904584482)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_411 : Polynomial.coeff recurrence5Scalar0Main 411 = (((19894142804 * 10 ^ 70 + 9362699332014876430469941173338235033881643286226833655081113855911472) * 10 ^ 70 + 5699552164268971723702139750965048476729683919255849206818993459343835) * 10 ^ 70 + 2100029964885351113707671243378868779095467794887121489421787148161959) * 10 ^ 70 + 8970872721146798221983876484313632428401804023870816043688803139020381

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_412 : Polynomial.coeff recurrence5Scalar0Main 412 = -((((292935991 * 10 ^ 70 + 1156973556808095126341374961372044328867130485899583656996934424933000) * 10 ^ 70 + 3770597487034849343669313741011232315541548474449047060100178734302400) * 10 ^ 70 + 9870673842471820480992334276180538968494584304427530084775275123536784) * 10 ^ 70 + 3034508257784821778290512847739468500367973330182073975569985738437023)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_413 : Polynomial.coeff recurrence5Scalar0Main 413 = -((((284162870 * 10 ^ 70 + 4604093229409557446516073600259888866023628205817229347626164122848463) * 10 ^ 70 + 9426307833491395557361904632335615275849039009679215782858984804584112) * 10 ^ 70 + 1716777376641117295210393810989253099401532682683986693426451311763004) * 10 ^ 70 + 1613406866554863026505251237286823015082301410817417704078480244280952)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_414 : Polynomial.coeff recurrence5Scalar0Main 414 = (((72194434 * 10 ^ 70 + 4206615586423639917672237258977965145620927092032464922259950677906699) * 10 ^ 70 + 7303012221490962432768567122632861821929658305181773227794914096136250) * 10 ^ 70 + 1504939120931407666488854464172614754483461128327688585589649832330537) * 10 ^ 70 + 1573959821565459003960686104703387740296611865761273159892902821578878

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_415 : Polynomial.coeff recurrence5Scalar0Main 415 = -((((12349303 * 10 ^ 70 + 805464130608440363356542459634018096675249147268120303221811372166464) * 10 ^ 70 + 3765869547239461925419530834363686328330255773414377825638855088654242) * 10 ^ 70 + 6477266868474373769588234200844420706886062381013983373199881687551217) * 10 ^ 70 + 9592043845875305068299789302579907489796135587987293633916835569197997)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_416 : Polynomial.coeff recurrence5Scalar0Main 416 = (((1715474 * 10 ^ 70 + 569212200162762532799884558212144578166413955370957203707250946109232) * 10 ^ 70 + 6417630792613638388192091425990132865035016333755875691821739671221571) * 10 ^ 70 + 437898472488611849289584928209813148171890479358821391378596001885177) * 10 ^ 70 + 7566543667070888362283703619027849127089945515012151011295644866512378

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_417 : Polynomial.coeff recurrence5Scalar0Main 417 = -((((191623 * 10 ^ 70 + 8528849666220634846245550256261473071885683969460971201938161738392598) * 10 ^ 70 + 5245025661512643821649114708020652990206505372451009921843183649021180) * 10 ^ 70 + 8867938276372895267093632819306291045950091625635153638128083891072994) * 10 ^ 70 + 8518837525063930141789752882390275643390583063789904560235807924489881)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_418 : Polynomial.coeff recurrence5Scalar0Main 418 = (((14354 * 10 ^ 70 + 1041931183374738437455929287889847018229248945103335030549523483601492) * 10 ^ 70 + 3671179730222411035806664660744826759479303961371193362305154704242491) * 10 ^ 70 + 7790293354014596235661200969584595230180149784105346912027347592399079) * 10 ^ 70 + 9939822624654740796570156042854790957829198861765561837599133909826907

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_419 : Polynomial.coeff recurrence5Scalar0Main 419 = (((22 * 10 ^ 70 + 1580308792253018023983433983974060760140882189121604762655313527294832) * 10 ^ 70 + 8292682888792993868254058584127109063976778863611618804680762560861732) * 10 ^ 70 + 4874023166524416240545876962741790362857866411408738805124541845409905) * 10 ^ 70 + 2701537027948319791781102751086711343359357881880328833947417019603265

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_420 : Polynomial.coeff recurrence5Scalar0Main 420 = -((((213 * 10 ^ 70 + 957849459399531544047880449247225562194145548418490786580026976206330) * 10 ^ 70 + 3797140615479878502908494138419220865637468793933081777941477578372737) * 10 ^ 70 + 259936438924759244779004916192216136310109193355541423461510144420563) * 10 ^ 70 + 4772783850182740400567745120037492230854596997082152812054650275473513)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_421 : Polynomial.coeff recurrence5Scalar0Main 421 = (((37 * 10 ^ 70 + 1348531445816456734595017895239336943510846500364194956429545247438018) * 10 ^ 70 + 5940834695510220195853906614797630875819921855756154587362258300909446) * 10 ^ 70 + 2622083115657939451137245541406644514142276420156971941207519213614115) * 10 ^ 70 + 3866912598652946040715155814877687207391185293798434955525445865503422

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_422 : Polynomial.coeff recurrence5Scalar0Main 422 = -((((3 * 10 ^ 70 + 4387750614173072496695495999827346809497644443406394976565971153811777) * 10 ^ 70 + 6305620415683838170067433110690447832200768210124835112189608656203565) * 10 ^ 70 + 7333242640472533917368859187733058747434243433750018945308579182939737) * 10 ^ 70 + 9860230328208464589616782226325528824515442852724405634296712843251326)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_423 : Polynomial.coeff recurrence5Scalar0Main 423 = ((1178907545003459933460828229733192025666557167131207746519089297321234 * 10 ^ 70 + 1063661783885405728426126564257169064140590123742772185958161875759543) * 10 ^ 70 + 6271460100193490439213868728735408557186322279538294968577489002562296) * 10 ^ 70 + 6050267969911246229785018906817539084335808949826563568413463539815689

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_424 : Polynomial.coeff recurrence5Scalar0Main 424 = ((145073768332093958737135373081402555646026547690150393927014665499061 * 10 ^ 70 + 5740262499402209769740210557497852888612143357237776246549422794021710) * 10 ^ 70 + 7629730321737013693806960383189854864456203941952367453147047937496338) * 10 ^ 70 + 9717829302482856059018551250843714824187806116493896421652195845302509

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_425 : Polynomial.coeff recurrence5Scalar0Main 425 = -(((24399334884394609226008394464764168890870745800324188011941350248362 * 10 ^ 70 + 4794759628667562363351750819501048537941077290572664955919088205387750) * 10 ^ 70 + 7450890670956139856231366775526953417202589252962561288639200733396888) * 10 ^ 70 + 5143127183272176979867045750946114653801503845987788452370945288056472)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_426 : Polynomial.coeff recurrence5Scalar0Main 426 = ((1413251311749934080010744168724600519764918393045336261126460775788 * 10 ^ 70 + 1115510247416741178472641239625346049427740196188298964522353260095180) * 10 ^ 70 + 2737019698951811200263462022410791986300021879356060251389885040271911) * 10 ^ 70 + 8072670275348680386545321705290942386710402807580575391644888919829769

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_427 : Polynomial.coeff recurrence5Scalar0Main 427 = ((13043895314869956326299340222520273456235654544873697545294278072 * 10 ^ 70 + 6091028833255895307280104154031183931962526615677761660824081925903120) * 10 ^ 70 + 1928050901525392035764279245949449543684978071197407442109312010665988) * 10 ^ 70 + 7522341468431040942742974533930089260524624562345974964511959129783624

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_428 : Polynomial.coeff recurrence5Scalar0Main 428 = -(((7100030297621151701298878198833823940374013485886570535449378737 * 10 ^ 70 + 7404542569950107578837036544397629625229811340562778242325000368825778) * 10 ^ 70 + 6015567979549285754754442132040093919771932669482513116241709624421226) * 10 ^ 70 + 1871994767611712410972930401281874474274023286885051875676192524033667)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_429 : Polynomial.coeff recurrence5Scalar0Main 429 = ((354859713190620957183639863703682086260869637762674249500481455 * 10 ^ 70 + 4583543845526814640223695853376525542080905848014387503608566935540832) * 10 ^ 70 + 3940825416988323701688130611580284151292456994586416748650553048272305) * 10 ^ 70 + 9294309334952787435354653912419776803545045558569050568572785472485786

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_430 : Polynomial.coeff recurrence5Scalar0Main 430 = ((4599224409608284838395756061932888394299605501299939500930205 * 10 ^ 70 + 7009387067143409236213830403520985866098275085436787289383586725879582) * 10 ^ 70 + 7696840176593766404774066934768265239347057521368870004311328230623186) * 10 ^ 70 + 4638832782613692422820928868048083007029905818468978384961655314245153

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_431 : Polynomial.coeff recurrence5Scalar0Main 431 = -(((940736638966834073161746083217311299338435193437319004916016 * 10 ^ 70 + 6622071472798788859650170677758636600828394033748412512784964278242274) * 10 ^ 70 + 2684510455305645401153927939593683155020551467875751085702277279438051) * 10 ^ 70 + 695641706496132043254128702843729126958573399005012714852503720465564)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_432 : Polynomial.coeff recurrence5Scalar0Main 432 = ((11148808951195943806840171742219979248380297860200967960782 * 10 ^ 70 + 9729289594007753807953181802862839533135951813405024146411443376432768) * 10 ^ 70 + 746421604112012274788047486159240011591995815183968215551627819447537) * 10 ^ 70 + 2839697616468821638797754863034743116772551014896334032835805578306325

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_433 : Polynomial.coeff recurrence5Scalar0Main 433 = ((1138425479016568633224877366728305648192691518497086285746 * 10 ^ 70 + 5205875974599793661831517986280284154431621495250514971417160791160773) * 10 ^ 70 + 7703399331734148940196310875871895352999721274546329431522345870436895) * 10 ^ 70 + 853493450487400808721650117532756377362178054674174061926788291816138

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_434 : Polynomial.coeff recurrence5Scalar0Main 434 = -(((11262806645747517109642305174607713209337387366558460356 * 10 ^ 70 + 4640333238429894640651250100186954407035220685529391716774886375870933) * 10 ^ 70 + 3536236383114340311890734587982050901384476534382713186316378585120885) * 10 ^ 70 + 4220110506803306965006863730987074289034977898746411602355265532262817)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_435 : Polynomial.coeff recurrence5Scalar0Main 435 = -(((883017438806098136631808898532201937552066929449162008 * 10 ^ 70 + 9673214507231920904035217182379744567672378752579049068487562892678544) * 10 ^ 70 + 865145488130275832629315944002105869666277171902196251571587525305341) * 10 ^ 70 + 8049901596659794233375338344276121075329024253444666794810990732386302)