Recurrence 5 lookup certificate: B1A3 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.recurrence5B1A3_coeff_219 : Polynomial.coeff recurrence5B1A3 219 = ((35951 * 10 ^ 70 + 3118675644860620319225091479549013132107584358666302394984941168722911) * 10 ^ 70 + 3032956186719212211918777841462795937904475017141234177762537877871920) * 10 ^ 70 + 4183203191266750708426957004966634747738409509516853575241795253500681

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_220 : Polynomial.coeff recurrence5B1A3 220 = -(((12544 * 10 ^ 70 + 5802096953116866652678962306672942973594221143320558275263690971470329) * 10 ^ 70 + 6955558849429970588269868835269789503675975357708088298443997306057317) * 10 ^ 70 + 587362053479474232615860245317548126162520875892368763535416375528349)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_221 : Polynomial.coeff recurrence5B1A3 221 = ((4315 * 10 ^ 70 + 9818466504075883589036845643209886948801551887317126722933946548581588) * 10 ^ 70 + 4880075929843660877884508788475088574236111068764898354174189702636384) * 10 ^ 70 + 1688710275540048251597882638620964796517719675698443512794459488757671

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_222 : Polynomial.coeff recurrence5B1A3 222 = -(((1552 * 10 ^ 70 + 8557354242219947629874973674511936322378626938767140336255212084187980) * 10 ^ 70 + 2576872519109749265604728723995683075241660302467585647249213458567121) * 10 ^ 70 + 6928044234584701112585027839091526431272019570262852774960250178697471)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_223 : Polynomial.coeff recurrence5B1A3 223 = ((611 * 10 ^ 70 + 3480169978689023373046416890263292502835060961606302546397466425093874) * 10 ^ 70 + 7535383884168204448372781245257190985860283943410707027052101871238733) * 10 ^ 70 + 6981987294849212285823587456722252623445955773531893425078419550468075

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_224 : Polynomial.coeff recurrence5B1A3 224 = -(((262 * 10 ^ 70 + 256561621415979361047330410342763940777236062191268625737410289660808) * 10 ^ 70 + 9602210117554102800432482878388422727218848495856269870584494314165853) * 10 ^ 70 + 47454167096911174689107599741478838885189417684682380413714601118591)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_225 : Polynomial.coeff recurrence5B1A3 225 = ((116 * 10 ^ 70 + 5129716151385273179220081614999270447961421794704310372398640625348765) * 10 ^ 70 + 3698189057899938547064252660827236146033671097872574584791781657283725) * 10 ^ 70 + 5575884424035952352620229693143869179796365817633933528962053878730902

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_226 : Polynomial.coeff recurrence5B1A3 226 = -(((51 * 10 ^ 70 + 923954443775438820476598297355664784214491101104886318808999868743177) * 10 ^ 70 + 7209873000629790736399632852120565017463841333305255096008744578010210) * 10 ^ 70 + 2542693524696463434403968248147910303614540099579767912079917402867923)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_227 : Polynomial.coeff recurrence5B1A3 227 = ((21 * 10 ^ 70 + 3880916150814198567586987364572496961431850885499482367059568038487036) * 10 ^ 70 + 9154381398972914337455624875033487509074147064144387549109419211610506) * 10 ^ 70 + 5358693351895151198000620307940039659076802453669248816929145894418151

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_228 : Polynomial.coeff recurrence5B1A3 228 = -(((8 * 10 ^ 70 + 4061536160283592427177415873922911931755860521843181676371789027654666) * 10 ^ 70 + 6401737175640957882236609888596626462405464306549948923911281743642165) * 10 ^ 70 + 8602275986093369092627749666519643874589626879589680781228605310791776)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_229 : Polynomial.coeff recurrence5B1A3 229 = ((3 * 10 ^ 70 + 763881109877504823943549245346599066981631102282016092944574744997005) * 10 ^ 70 + 5021397477710226741358232203302878787668543404670070378581792787871051) * 10 ^ 70 + 9162915799584579724324205442528699576495700600028670399769694060329441

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_230 : Polynomial.coeff recurrence5B1A3 230 = -(((1 * 10 ^ 70 + 426469233724267973650248229204817656494317684298414165278099141254526) * 10 ^ 70 + 3183327058893288339133218411657616316658807968640278009020473659427804) * 10 ^ 70 + 4365294609060355419227084985394374070490641865205450799972871992816884)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_231 : Polynomial.coeff recurrence5B1A3 231 = (3251844503781042287943583140459955720839225600755400582089327429289963 * 10 ^ 70 + 1937980981785545954360552385926835863730211558079110699875526077520839) * 10 ^ 70 + 4151570230489482099767855954367279107633794722770518255073464256089287

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_232 : Polynomial.coeff recurrence5B1A3 232 = -((923040751412546974342642955460150684495817313057679631329600991291227 * 10 ^ 70 + 5833719114913825788218489458394660840200958932493304509025690040701977) * 10 ^ 70 + 2652259407864002904143891821440069125534395847485450350334783323857197)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_233 : Polynomial.coeff recurrence5B1A3 233 = (232989721236876376503676837485093108360721051507667739339023237101933 * 10 ^ 70 + 3724148369671614706554411483088365386645106313330367293544102689353070) * 10 ^ 70 + 6007698197649876553430914818205263115723418181020535374362011126691258

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_234 : Polynomial.coeff recurrence5B1A3 234 = -((49310114580512913318516730391498355201595932347078299150901401591898 * 10 ^ 70 + 5919154669117887751281921697687180725328560999881949911123341293373871) * 10 ^ 70 + 4731145015356504169548461427634113917610216427375567813301987364953905)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_235 : Polynomial.coeff recurrence5B1A3 235 = (7018237985084526268570713850161856309491701638916566661920603249633 * 10 ^ 70 + 70654227464787426857827761679532481299095354892251007105539685781739) * 10 ^ 70 + 277200561018344332797549524683157861246455256477740494244602498476005

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_236 : Polynomial.coeff recurrence5B1A3 236 = (489614818401720676169121317839849405701209857805474344789130721253 * 10 ^ 70 + 8184749042557964466212967600000891739101973108763628858963949935737409) * 10 ^ 70 + 3780926495793422174592573329093147807369324058934668279925403815001018

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_237 : Polynomial.coeff recurrence5B1A3 237 = -((950903621692018595437334231641734223245750407472586205293641883362 * 10 ^ 70 + 6313083469670326395296319108361928223583952110184019450871268521441489) * 10 ^ 70 + 5573478702846059991433669522965415145438490143397182384225162640639928)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_238 : Polynomial.coeff recurrence5B1A3 238 = (525715659494047063481696746511244550334356314951122179464252116949 * 10 ^ 70 + 6105334328912167074118907019808740130283230484587543927622105602696778) * 10 ^ 70 + 4615761842989487465193924291094705780273250997549607531604494100174625

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_239 : Polynomial.coeff recurrence5B1A3 239 = -((229282645424757351963784283268312003106416672022318999725291167708 * 10 ^ 70 + 9955494200651637152711949084733732268315471972204143103019935647126137) * 10 ^ 70 + 8376738382838011987989399791268324685428798822605095291295189478968366)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_240 : Polynomial.coeff recurrence5B1A3 240 = (90127677547455537796580514874498453838767271880054562658357399722 * 10 ^ 70 + 9253874603493813084642547123284153159139022445170667461918330021373115) * 10 ^ 70 + 6339616597134254385384742191007476054228138564301445968919358943049603

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_241 : Polynomial.coeff recurrence5B1A3 241 = -((33173473854275275089690699159822270983269855765991711815594204283 * 10 ^ 70 + 6946182271357785143039444478625275792018443269899010124578199839593839) * 10 ^ 70 + 6133895729674018730502849511080524979749798145583071401417295700378770)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_242 : Polynomial.coeff recurrence5B1A3 242 = (11466826372692799700755837295663083394133959045819233208296848170 * 10 ^ 70 + 1995015958645885299475080622380170103476929885474562788692068036323930) * 10 ^ 70 + 4081531957591936825760260134361007617817342621564685266712167111553341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_243 : Polynomial.coeff recurrence5B1A3 243 = -((3645113703147113321394905243093900478117525207907628236445325946 * 10 ^ 70 + 2048166783976689743498372047902494971282362841593393076233480712487541) * 10 ^ 70 + 6329619831798832547236894046219587618536399518578639181645266007894821)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_244 : Polynomial.coeff recurrence5B1A3 244 = (1010240319841801871861621035749438380421221668122351530522432818 * 10 ^ 70 + 8378387762761993490163766463420708247266284487754328878429764196854670) * 10 ^ 70 + 2682336553320304638793487728616134666465628284163163219244631479188888

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_245 : Polynomial.coeff recurrence5B1A3 245 = -((208959655280479353996173629970585109686075290653894987859230658 * 10 ^ 70 + 511308859606580179144802520643969945843801432509756640982865682273552) * 10 ^ 70 + 3603595836206238877786304918895592852513634275532019806103281773081202)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_246 : Polynomial.coeff recurrence5B1A3 246 = (6302348766471834381199600983900926704164586084485254398759090 * 10 ^ 70 + 1776363309636702671648056442721581798355122848818532669595790860958381) * 10 ^ 70 + 9548211710917565863636775269363799371214974569546824684917464713321277

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_247 : Polynomial.coeff recurrence5B1A3 247 = (24988081459147572477704718330338381322052952727468766238355952 * 10 ^ 70 + 9188661199405780237303888373505976119169426566830629392671010605875562) * 10 ^ 70 + 3644007278302418583113294546550267956716984710334304156901498397935892

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_248 : Polynomial.coeff recurrence5B1A3 248 = -((18652565855021311832565117627247790656941819116770945439699642 * 10 ^ 70 + 6957995390988853114698168756686718061559717169019215326608558472072772) * 10 ^ 70 + 8809597053795625482399260850468075674528071658821636863219273877263885)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_249 : Polynomial.coeff recurrence5B1A3 249 = (9787882877166086042803163413686281492011554005093507034525303 * 10 ^ 70 + 9131598193056849923165331054620019065573984421292190224619501652196062) * 10 ^ 70 + 9164531577998027320021144195178293534952733764629772763341324106372335

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_250 : Polynomial.coeff recurrence5B1A3 250 = -((4396224080611218279190953374315844860314459971755934074354241 * 10 ^ 70 + 1570132643944625066515912884928376082221212877186731832094040589511385) * 10 ^ 70 + 6386868378060280243624763481200694545271160327547991995085480711092053)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_251 : Polynomial.coeff recurrence5B1A3 251 = (1796872365988712913361594128185947804275644092099863039340322 * 10 ^ 70 + 1674064231966056268837555397618887549751242279047544534331107341062260) * 10 ^ 70 + 3333229719555363967324903479686299655390011090174796140328906200908407

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_252 : Polynomial.coeff recurrence5B1A3 252 = -((686785680737208259588380231048787337002041443338010506073198 * 10 ^ 70 + 3105047114815716842115335351643342724364478750828995896931482847074319) * 10 ^ 70 + 8610916875720089436376254435030967267277499557357191594990476134264945)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_253 : Polynomial.coeff recurrence5B1A3 253 = (248619770863465526384534297640206343602867012686060172413715 * 10 ^ 70 + 9368067480808235899875048595349541433127956041067775987009276251654245) * 10 ^ 70 + 6484705719693195284110796571135988823642093419057589312628036915764550

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_254 : Polynomial.coeff recurrence5B1A3 254 = -((85654133995425191919049075860460654518078679416729451031426 * 10 ^ 70 + 5428088628495058556598659311112459775222271901468137728861358991043626) * 10 ^ 70 + 1053205744686272190745369989374270852559823618543309579553759644147045)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_255 : Polynomial.coeff recurrence5B1A3 255 = (28105257502745943342400847112543300014456703233581558542467 * 10 ^ 70 + 9123208334465934586551634420049506620889392841617394410489418289115570) * 10 ^ 70 + 85870111179113421363398550641151215873576604063982265706936013170753

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_256 : Polynomial.coeff recurrence5B1A3 256 = -((8784803782284297966793976967043370702708333301215332154426 * 10 ^ 70 + 1617463971556573117641978507162303434702924733727772327044726422295097) * 10 ^ 70 + 8062011017482514394075841979942209041733357556280831630116307997671142)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_257 : Polynomial.coeff recurrence5B1A3 257 = (2622549227548208764684738597070899531207457026016751164909 * 10 ^ 70 + 1962058750279721193524488162519735674368337634742413422004751781455795) * 10 ^ 70 + 2428158698089018258749388184428557832507564620420551255322304139864684

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_258 : Polynomial.coeff recurrence5B1A3 258 = -((752789863039568591776032006247531582071257123341134639654 * 10 ^ 70 + 8566584500194606915165186464423977931000355997245142585832598067664759) * 10 ^ 70 + 9447511638393500630418335628430781529208087442018605293771121569826039)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_259 : Polynomial.coeff recurrence5B1A3 259 = (209695049450279403120231047875219031723001199379027412215 * 10 ^ 70 + 2977329129811734702422680487562545719557706583754753089939735217699340) * 10 ^ 70 + 4970870464735266477482311044356932264216510663158500501711214168534149

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_260 : Polynomial.coeff recurrence5B1A3 260 = -((56980031439122655163269634911747546607529584512773458876 * 10 ^ 70 + 5711449771695118323860205884662086895418997321540733864015336847965491) * 10 ^ 70 + 8847842019086255901354490146659311383273241006608494501236106085851049)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_261 : Polynomial.coeff recurrence5B1A3 261 = (14962250971449136005810656541096266701603961041658521044 * 10 ^ 70 + 1570029946936408813627824691683467068248464504779756179308578160157247) * 10 ^ 70 + 5782334683456796067669614320949410539125169005831843525255969099268075

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_262 : Polynomial.coeff recurrence5B1A3 262 = -((3666949657715607900748033124219921040963603538529346476 * 10 ^ 70 + 1921763646364603891230907549427350085120249097521586256932112697588517) * 10 ^ 70 + 7330919651085843680473564947319885775006542967582115874458708528084943)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_263 : Polynomial.coeff recurrence5B1A3 263 = (776158142179262978525418330327028409396544395172929782 * 10 ^ 70 + 2184380724006963934498731747138601315257288234621459065135948370515295) * 10 ^ 70 + 2343136160504162068788390026854937877725519287428614939610313499570159

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_264 : Polynomial.coeff recurrence5B1A3 264 = -((113942802637748792721812962758256529210816930076386302 * 10 ^ 70 + 6977226363310218691006818216670028659181344083585272906764011170510417) * 10 ^ 70 + 3387936651896918523062321439835382751597550088973368103253430594240898)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_265 : Polynomial.coeff recurrence5B1A3 265 = -((3779385106731543662677591497146079448556787981746563 * 10 ^ 70 + 8841725451619111620978226523523508613516010237585494822809700104652146) * 10 ^ 70 + 9811363609811993563600500624185116322964149602636942981457540358100249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_266 : Polynomial.coeff recurrence5B1A3 266 = (11125669438942822075913624119863805583701827355514186 * 10 ^ 70 + 4073218751605446931516597679504099388271060042141570717321693816988453) * 10 ^ 70 + 3450352808797243873845117283554665499978206016213014256547696767759964

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_267 : Polynomial.coeff recurrence5B1A3 267 = -((5308183387112132258165918602485522534303594800346540 * 10 ^ 70 + 8306719330035716980218144930494375576536862244415161956200490365245604) * 10 ^ 70 + 4685484171530338964673089688120588697597592711436642430444363233683238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_268 : Polynomial.coeff recurrence5B1A3 268 = (1779720437340663989105845447660270622839867522789036 * 10 ^ 70 + 5443556688384962482136467351343574108038525776139492263907507198035183) * 10 ^ 70 + 9446946710989200216854366754878672419465904142097048234745324277581388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_269 : Polynomial.coeff recurrence5B1A3 269 = -((477608412082865821567382613135624880351582135474384 * 10 ^ 70 + 298652756299786546080731305308848105893774326657486738831121366543599) * 10 ^ 70 + 8947390601285130467422022548437498716332195268807974375174209313606856)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_270 : Polynomial.coeff recurrence5B1A3 270 = (104535147508478177595575186191842693036209370970312 * 10 ^ 70 + 1437648287868424324412100942423303337674175232699519442519162173452726) * 10 ^ 70 + 8085617760795728635143070298347418865562522950195789434958469175911793

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_271 : Polynomial.coeff recurrence5B1A3 271 = -((17848309834517362711885843980296130355908021716516 * 10 ^ 70 + 2099491440799990786852922408372906752421953753347117629589199760076011) * 10 ^ 70 + 2622525814923420186509109398431773608806290624841840621935880326854613)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_272 : Polynomial.coeff recurrence5B1A3 272 = (1916974133109029056796063624141372888218272403570 * 10 ^ 70 + 4728846838734473307510973989112620616413294380948983722263459787437536) * 10 ^ 70 + 393914578729398850773241809001557361816265119024665808192717362487700

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_273 : Polynomial.coeff recurrence5B1A3 273 = (84763215901586602806071944165662650349182824650 * 10 ^ 70 + 6235205481709839389014955949363228981129668104273915960927612449276761) * 10 ^ 70 + 5891334280803680672620440258705060174506361333414609848527016805988359

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_274 : Polynomial.coeff recurrence5B1A3 274 = -((109896183989224809397330889211773567591928558166 * 10 ^ 70 + 6930108157039595693491351630803748771858761651881806925949335857906532) * 10 ^ 70 + 1379645620360540802283247668550894959214986976856238439518707547005740)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_275 : Polynomial.coeff recurrence5B1A3 275 = (34290419424637060702301959246401603463021975775 * 10 ^ 70 + 7022222513895178166107389466037537911387173979286318501461208435293636) * 10 ^ 70 + 6671805484285387415738803681767533427437472774107574633246050782980121

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_276 : Polynomial.coeff recurrence5B1A3 276 = -((7340156291606014285980642098696442742152959125 * 10 ^ 70 + 4066422400240118944777197482482604115584108032226540606354206303193941) * 10 ^ 70 + 8949759604050024101691817079345318176438337443423510570447398113773642)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_277 : Polynomial.coeff recurrence5B1A3 277 = (1197226914672921332829147419046622444155060166 * 10 ^ 70 + 5795183430908128141438645965791801825792726877263860951435689399776315) * 10 ^ 70 + 9181816607356230294283467082823538537908046457552499887781008220375339

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_278 : Polynomial.coeff recurrence5B1A3 278 = -((146960024950009233814831152882057112522302729 * 10 ^ 70 + 4095126289908869583613890439636590553370093772617787250054982833948611) * 10 ^ 70 + 6241847080381727975877565826113379623546570395407086042010639572760029)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_279 : Polynomial.coeff recurrence5B1A3 279 = (11752250781501416886315757953530086692782529 * 10 ^ 70 + 3956715524688269072293386068840775112572291030015889497221596352119231) * 10 ^ 70 + 8885202431421630352786202767868590363633049982210052126806943645051951

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_280 : Polynomial.coeff recurrence5B1A3 280 = -((91023144751545565069002976788696585112925 * 10 ^ 70 + 503453540696676288686040059804116224948270950872849439850582144268479) * 10 ^ 70 + 4755290000703346772800135567508575946266096375217033715881073918494196)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_281 : Polynomial.coeff recurrence5B1A3 281 = -((151511515096175992175654008867533885743534 * 10 ^ 70 + 4724409286237010461959172196661289591623371316904581580674771161181091) * 10 ^ 70 + 5242190740846091763921059978182659744103459811160750511496749332877977)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_282 : Polynomial.coeff recurrence5B1A3 282 = (28322529162538561339605513948916308644870 * 10 ^ 70 + 9906118074037943778958592057876017945103280929153104683638153421644591) * 10 ^ 70 + 9398407176887822976845217547181911928998481733012784314405071680538395

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_283 : Polynomial.coeff recurrence5B1A3 283 = -((3005783595527446424334224393852130847987 * 10 ^ 70 + 830584679449162054156245236785196790898066794829521398645062353648893) * 10 ^ 70 + 5666185919506075027370246745415976912646889705664040765512035998265703)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_284 : Polynomial.coeff recurrence5B1A3 284 = (189709517692873298673756037290286697679 * 10 ^ 70 + 7131799231192801935969905292057508824784475599182254883470154598296867) * 10 ^ 70 + 1863017736172288420058543050022312151000856574465855497797249912400437

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_285 : Polynomial.coeff recurrence5B1A3 285 = -((3181042501523791694361784089755705919 * 10 ^ 70 + 8669632713429795022100632993713873655355107130719366014800345506653668) * 10 ^ 70 + 2150357353658087015688673745525386170640912424413163047839213253845927)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_286 : Polynomial.coeff recurrence5B1A3 286 = -((670328115877349173312697496792508977 * 10 ^ 70 + 5531512241572101107017387368283076505853293094746100651761226463589212) * 10 ^ 70 + 7845325135011856946168229844868549027455393667283631593422011947129375)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_287 : Polynomial.coeff recurrence5B1A3 287 = (71590980495994071922533935956020078 * 10 ^ 70 + 682860149257635287281162587700479956056630031051582490660014466640293) * 10 ^ 70 + 7139827419348769213465926870275675878681432070940106359804009774405624

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_288 : Polynomial.coeff recurrence5B1A3 288 = -((3027533570916477639929408606902976 * 10 ^ 70 + 7197788563485756982978707820735240830337962987805578641033979926130723) * 10 ^ 70 + 6413474243365004720616424783195743615249736998298566684436426176708467)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_289 : Polynomial.coeff recurrence5B1A3 289 = (12294322996422638500307801529064 * 10 ^ 70 + 5150456713503566848702383371035939592544946533038854751832635040413015) * 10 ^ 70 + 3245069895940509785374364059600486705854726880917264948421471929196122

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_290 : Polynomial.coeff recurrence5B1A3 290 = (3609668825832431999660680359487 * 10 ^ 70 + 9500696446761927088624180513542684013424847768501816854052489506214027) * 10 ^ 70 + 3124129521824637174481791907080321097507449048964417025047410360740450

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_291 : Polynomial.coeff recurrence5B1A3 291 = -((82014777860819581889282478452 * 10 ^ 70 + 9838450430020613385680942113269226265417956619410412084138825921681241) * 10 ^ 70 + 9627438926358239669037709561214746837000071628257305700732458900851174)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_292 : Polynomial.coeff recurrence5B1A3 292 = -((1165483899498461129077160968 * 10 ^ 70 + 6830007306698892250537132398349875182812014594840795977049374339344096) * 10 ^ 70 + 8886498281097903259477108790366818865588390770120276462266139341372270)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_293 : Polynomial.coeff recurrence5B1A3 293 = (15884072902681779161632498 * 10 ^ 70 + 108470172076277866197695016784597222609610317290382164798869677856614) * 10 ^ 70 + 4651755114106010905081544525669227809289939052761380421390623448725181

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_294 : Polynomial.coeff recurrence5B1A3 294 = (200650488224102264202256 * 10 ^ 70 + 1338001855996970271426370917232917068813499379233110349575564103834575) * 10 ^ 70 + 4408694611227243423181640503801512723500181086332461489761595978331156

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_295 : Polynomial.coeff recurrence5B1A3 295 = -((76609740528066331346 * 10 ^ 70 + 6159409570030755241190174036136442616664236350986206683760812403279859) * 10 ^ 70 + 180148591796618403047183040560803694093249129123217790318150232742592)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_296 : Polynomial.coeff recurrence5B1A3 296 = -((6476795519958517763 * 10 ^ 70 + 4843240478644887619790389666960421607036521182494022195247395174640356) * 10 ^ 70 + 9126938465417477457188640783752833232491115417120867582452736567623067)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_297 : Polynomial.coeff recurrence5B1A3 297 = -((12351241368713734 * 10 ^ 70 + 2451950017655881776714177853121003447480790647411004520950703276309109) * 10 ^ 70 + 7782384148955723409326134986072161607360732262268638302091129729666807)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_298 : Polynomial.coeff recurrence5B1A3 298 = (57915773350426 * 10 ^ 70 + 9944193120989440904409484793789081760511792238046829347170657559204139) * 10 ^ 70 + 3569802927378436589976780916681454506836358807379262528309522147174938

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_299 : Polynomial.coeff recurrence5B1A3 299 = (134724563757 * 10 ^ 70 + 2229277478365174689052227125927571510565093550925090748127642056848639) * 10 ^ 70 + 3542805442627489341024143574540235695432825945441546238744369036020253

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_300 : Polynomial.coeff recurrence5B1A3 300 = -((255714932 * 10 ^ 70 + 8148266865856813201377244413530297796139641552277041268188581680001955) * 10 ^ 70 + 3710919517794335327150804626282475752019543032501824603279218843887460)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_301 : Polynomial.coeff recurrence5B1A3 301 = -((454113 * 10 ^ 70 + 8623732074313474460771831203176534712132431293013772408701477794210962) * 10 ^ 70 + 6156594973932941437495027654678561554352651027821703053706166186848775)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_302 : Polynomial.coeff recurrence5B1A3 302 = (614 * 10 ^ 70 + 8087206497370945598287405693839182008022659631500952351850032883635476) * 10 ^ 70 + 1567110350725248293194109058502648991500277492438515900530629191467536

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_303 : Polynomial.coeff recurrence5B1A3 303 = 2733547569229180702934422067726889200566060827284897081026568213384736 * 10 ^ 70 + 1189157103770620711057012235176138187322936295166111372291820878922584

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_304 : Polynomial.coeff recurrence5B1A3 304 = -(2644492595546306892211628890844981106951915344699932289702745134134 * 10 ^ 70 + 6809610095172233234748914778831986421141456324176420888352272279385068)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_305 : Polynomial.coeff recurrence5B1A3 305 = 7666190964088414772699155564738811924719889583017140011278415 * 10 ^ 70 + 9824838106834250852128276016413390484840644769093337325788589406513543

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_306 : Polynomial.coeff recurrence5B1A3 306 = 57347160067525136976372805740083259450918883536138618109236 * 10 ^ 70 + 9038921800502905353606449662866629199371351376427436935943618082672000

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_307 : Polynomial.coeff recurrence5B1A3 307 = -(1155231654492364480394069936679724423954047942491747136 * 10 ^ 70 + 2513897210411721683768322908134836534686327983560691503720693086878460)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_308 : Polynomial.coeff recurrence5B1A3 308 = -(34398705033879381097982418830509391086909523573532 * 10 ^ 70 + 748233718868526224641492539107056795552034307690829696956241359055801)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_309 : Polynomial.coeff recurrence5B1A3 309 = 215015399502368050795659987526356979941521567 * 10 ^ 70 + 824288257470526709720318319317340098626360046981476500260988775227353

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_310 : Polynomial.coeff recurrence5B1A3 310 = 206967408019792044053139986914498949691 * 10 ^ 70 + 7426372909971919893693141609140417938600952774111519574727313424586321

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_311 : Polynomial.coeff recurrence5B1A3 311 = -(215841817127047757417089589817969 * 10 ^ 70 + 6534773939361196324091995033050905916047127618514255444111813367865914)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_312 : Polynomial.coeff recurrence5B1A3 312 = -(2983748584247354453598460 * 10 ^ 70 + 7044222996973995346056732224350565306593598213239436843820748594142133)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_313 : Polynomial.coeff recurrence5B1A3 313 = 248126233697070452 * 10 ^ 70 + 7087092616189355522336704302718340073582840467932303636082363886151610