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_85 : Polynomial.coeff recurrence5B1A3 85 = -(((583 * 10 ^ 70 + 4112284198351127095233566696718057505994875879832374911719914649152247) * 10 ^ 70 + 4656005696401653886811004260597414059341717154855161588851056611039959) * 10 ^ 70 + 8693981687757376891966040958710902012537209088039616994075040950947389)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_86 : Polynomial.coeff recurrence5B1A3 86 = ((2728 * 10 ^ 70 + 1963733205860919506352356929592271520326579548728700792570676679183047) * 10 ^ 70 + 1456477118850293743545424813800809229063994494429396298342429196367957) * 10 ^ 70 + 7911618217584595934652142672075523248804108049500883921189005526131825

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_87 : Polynomial.coeff recurrence5B1A3 87 = -(((12359 * 10 ^ 70 + 8568507677795312482920369090650721135988273592512529923533136602501859) * 10 ^ 70 + 3979687683213270259837035133185935603763255716724805274865848028109582) * 10 ^ 70 + 2729063287015525337342058254988180840462847858098558318612398297156675)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_88 : Polynomial.coeff recurrence5B1A3 88 = ((54268 * 10 ^ 70 + 5080485608589324972252045511974460612469892088717365779269270659325407) * 10 ^ 70 + 2731866254473611134749244729483962329876850312842406170171211187577870) * 10 ^ 70 + 4943867545765318824027756834617007572125352612748207100798522489154179

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_89 : Polynomial.coeff recurrence5B1A3 89 = -(((231010 * 10 ^ 70 + 3042515716170651694572806161872911465777997575966022927410997515377008) * 10 ^ 70 + 6004926731771845125635746978204644955064358780704783617910961520101875) * 10 ^ 70 + 2726223355596659003265709557467840548046107747954673989032372111414916)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_90 : Polynomial.coeff recurrence5B1A3 90 = ((953694 * 10 ^ 70 + 5747777633109735922391804146150870384615760510351089394994678499387412) * 10 ^ 70 + 7983962212039696066037500258249001177344330583444059286235967977391870) * 10 ^ 70 + 1076916168900851040663182637324790491896910221631109466407242462505222

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_91 : Polynomial.coeff recurrence5B1A3 91 = -(((3819623 * 10 ^ 70 + 7010926166662361659455533500579114190053573902431803006820751404061707) * 10 ^ 70 + 1967775808872558317668286694523085816016313005740139856824169760902186) * 10 ^ 70 + 5403080412180401046632726695526055787553834912331329476258783423218904)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_92 : Polynomial.coeff recurrence5B1A3 92 = ((14845594 * 10 ^ 70 + 9133780704681239976933351378832663191492349559084918820170145164285049) * 10 ^ 70 + 5855063591517999613663632162138126891537032110311449837554442243278377) * 10 ^ 70 + 3891496354617303825153856940995588870073923101826547120362810448077771

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_93 : Polynomial.coeff recurrence5B1A3 93 = -(((56010150 * 10 ^ 70 + 4585178307140978260110368865779579879867602896296588261872432557915053) * 10 ^ 70 + 2195583512201271622021678278032340477976136622933436429984689362992246) * 10 ^ 70 + 3634453083496116622015905424486112042473113270399527907163875369709144)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_94 : Polynomial.coeff recurrence5B1A3 94 = ((205186352 * 10 ^ 70 + 7466699874722272464147607838519662180823605886087953622604451339749716) * 10 ^ 70 + 8371230329216172398547437658140787306908261978193054754414364502333815) * 10 ^ 70 + 4872012627411620936147472472297510499515055901294791680610678552115685

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_95 : Polynomial.coeff recurrence5B1A3 95 = -(((730058521 * 10 ^ 70 + 9873842703708054348813940608418627769518053746473498137676124474619393) * 10 ^ 70 + 6397930781439403838339695826603905290384949315072594067679840904642686) * 10 ^ 70 + 9416278942959382136052840594536772472470590103306084361787824704200461)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_96 : Polynomial.coeff recurrence5B1A3 96 = ((2523502978 * 10 ^ 70 + 5918249168749644197080535478485286434228729556513373620663264243781966) * 10 ^ 70 + 6680490579791237865527163161870123168057054681571381256889941523829916) * 10 ^ 70 + 7259454778095095067095204141837330267679257716073381607933291834980210

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_97 : Polynomial.coeff recurrence5B1A3 97 = -(((8476004890 * 10 ^ 70 + 1586269579490959465027993577011922592036741397944446633410613765255630) * 10 ^ 70 + 6633214514446584215675679468277602746031188934921055252568175475310821) * 10 ^ 70 + 218746686285605258136291892694092311628300160436477437282563635029720)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_98 : Polynomial.coeff recurrence5B1A3 98 = ((27670633668 * 10 ^ 70 + 1774731392431133683778655268578558754308608770650713598097833232228233) * 10 ^ 70 + 4544244026549548548660007687518655762667581863026079238576972001504938) * 10 ^ 70 + 3834772320792353397916444201199775851459993455249912826410430919587278

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_99 : Polynomial.coeff recurrence5B1A3 99 = -(((87817696447 * 10 ^ 70 + 3865385470916618609125362790950984989133766978332579799851112011474148) * 10 ^ 70 + 7135382398641059092048519008350327204648042338535423943957294122467421) * 10 ^ 70 + 7163245812605770629085035831887786466019961835554187812043816846198500)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_100 : Polynomial.coeff recurrence5B1A3 100 = ((271000371901 * 10 ^ 70 + 7282260954538285220057174633068475990265980505597392412684566584088850) * 10 ^ 70 + 2893376102148893692601430364462045174643617706453561779866903885752132) * 10 ^ 70 + 495253548368774977382432736808646139030713387981545103183829291912454

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_101 : Polynomial.coeff recurrence5B1A3 101 = -(((813332389978 * 10 ^ 70 + 9238631139470732566987807729087880805373256292696676688401247994337786) * 10 ^ 70 + 2562414504489681444312851197457402669319249495095713004587327086033883) * 10 ^ 70 + 8168690733807389940061417455319546983328513295404645142215719714203409)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_102 : Polynomial.coeff recurrence5B1A3 102 = ((2374420916745 * 10 ^ 70 + 4189897722676056939009669386305691230387955631385808730865390615097656) * 10 ^ 70 + 9806693791328676896881089049377007795841044634557743632727937391834640) * 10 ^ 70 + 5346099704321615632547819688805088816070177715610312402510339050117123

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_103 : Polynomial.coeff recurrence5B1A3 103 = -(((6743972333277 * 10 ^ 70 + 7983677500625395210610366665457571350207879721727362602978845138721232) * 10 ^ 70 + 274749375564550397573651528789223581321106381753044867515773791528688) * 10 ^ 70 + 6793869079309497195045988085815388537550006206695470729784123477318075)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_104 : Polynomial.coeff recurrence5B1A3 104 = ((18638683001599 * 10 ^ 70 + 6749996190913969612056993083568491293362996970710201778001610875923891) * 10 ^ 70 + 4420129325093929120423279828917186712433146896074969457343323315712777) * 10 ^ 70 + 6797745773362743451229792359382035786312615927223759270677222182774216

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_105 : Polynomial.coeff recurrence5B1A3 105 = -(((50133158923891 * 10 ^ 70 + 1016060546787566434019322448864287547170732179469645625189824532311935) * 10 ^ 70 + 3895119378084566631690908270525510593659545594584063258778992860725609) * 10 ^ 70 + 5682624289348641218804947106843446484054040433960450596520253755904204)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_106 : Polynomial.coeff recurrence5B1A3 106 = ((131253398679735 * 10 ^ 70 + 4548312108063435553054865105248293464560217982204423694767448996789060) * 10 ^ 70 + 7840533665673454977470652198237490943603699073643717873722283585921100) * 10 ^ 70 + 9289871888409068903880606710658838666753751285288658951171073657435069

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_107 : Polynomial.coeff recurrence5B1A3 107 = -(((334528563034022 * 10 ^ 70 + 7139366397313332660814983158585273049580851776192035767686823813978292) * 10 ^ 70 + 697676478593283434144587752106555020130395071658971379274876030264169) * 10 ^ 70 + 5348353955673332659566532481459790657721757197749079664403762757276308)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_108 : Polynomial.coeff recurrence5B1A3 108 = ((830139157663667 * 10 ^ 70 + 1002734817031623608032885289486681541452052265560566647102977854977923) * 10 ^ 70 + 8924712410983318828986647246169898493367556698160972271058257502129277) * 10 ^ 70 + 4522594283889808451496305425296588484172679891526267949771961213261413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_109 : Polynomial.coeff recurrence5B1A3 109 = -(((2005940097441560 * 10 ^ 70 + 5634643029097873256343308823543434325420321157969141568036484977389798) * 10 ^ 70 + 1259528868497399521720556746055087271159240596021637658594241125381286) * 10 ^ 70 + 9664482180722534546853119507708116293019927917650242400626439662394211)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_110 : Polynomial.coeff recurrence5B1A3 110 = ((4720469294229664 * 10 ^ 70 + 4854059497186039265369633611025259793363891703607950510337455199668520) * 10 ^ 70 + 6191770313822747919038158573892113350480068191770324962853571365917615) * 10 ^ 70 + 3654001362228064476917608108319783492401780715429883945825228141090844

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_111 : Polynomial.coeff recurrence5B1A3 111 = -(((10819317128116350 * 10 ^ 70 + 1194966071691940207114141405318361457870317305304906295395679841272137) * 10 ^ 70 + 6546453369633917900635737742181659518269755361528404962354627393300516) * 10 ^ 70 + 2888210977500204244737769971829933946170817093346918921174496304325827)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_112 : Polynomial.coeff recurrence5B1A3 112 = ((24154930843241183 * 10 ^ 70 + 4868594366690770324902883916483320810358211170924603418962301206412914) * 10 ^ 70 + 3402956774012382684452431833142384699479448326829419730941245307891815) * 10 ^ 70 + 815849949303610505146162169101854489963204749969285223782099641657627

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_113 : Polynomial.coeff recurrence5B1A3 113 = -(((52534348337817039 * 10 ^ 70 + 5718490747005623282664991730005530573833862970707426615541920142527297) * 10 ^ 70 + 9767398106786606751645290383348231810897124988291693827541013959496811) * 10 ^ 70 + 4135353354236421263192257264699927897690990029334802801862106789361598)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_114 : Polynomial.coeff recurrence5B1A3 114 = ((111313879094694684 * 10 ^ 70 + 4225575178569581419737987312125762417845645797671760985317704347918509) * 10 ^ 70 + 1812658736908550105559613916772917302914265047796270341392362958198665) * 10 ^ 70 + 8901851597606974666637293279167447431607636007115473840812139109611451

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_115 : Polynomial.coeff recurrence5B1A3 115 = -(((229803664757689476 * 10 ^ 70 + 1668618784413633148850822440143912037039081602221403144414536465418845) * 10 ^ 70 + 6945740079564378864669885047241794452401981707729846423018042215546250) * 10 ^ 70 + 8204030345970559351060573023156347144927093500011977012078793552946530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_116 : Polynomial.coeff recurrence5B1A3 116 = ((462270153898985568 * 10 ^ 70 + 5720011692475793234194453048210328235435628709390720706345649391956535) * 10 ^ 70 + 7372477583439638892691670584429270135990854403513068987675038446214625) * 10 ^ 70 + 7835025131779127757839106494199580374644837016332726820539693398901606

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_117 : Polynomial.coeff recurrence5B1A3 117 = -(((906132884641168452 * 10 ^ 70 + 3195931967411118228086846852272073126813012205907857046213594882643256) * 10 ^ 70 + 3959150888961850565674358459050707788437509619283559214468361244700710) * 10 ^ 70 + 8486990199558089320005962277500300252820890727522047244269724047537501)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_118 : Polynomial.coeff recurrence5B1A3 118 = ((1730880333520674344 * 10 ^ 70 + 6757801695263960620475798265939987102807545510351248818989896181433287) * 10 ^ 70 + 4246118173249056664140804530741288021908418113773712172160768749982078) * 10 ^ 70 + 3494518885198321494688560460903432948055590852259137617425949407206736

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_119 : Polynomial.coeff recurrence5B1A3 119 = -(((3222101660118811915 * 10 ^ 70 + 8407177923953419166191155246454074837537884441269139747025102462848930) * 10 ^ 70 + 3994766806928157879150268913834477963756695545155884622197867678387620) * 10 ^ 70 + 1820368313878818160089127078365548504577036315403894134575775050343286)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_120 : Polynomial.coeff recurrence5B1A3 120 = ((5845506400938865747 * 10 ^ 70 + 6513660998880034980635149084749798174289591177010629707612888641154437) * 10 ^ 70 + 1825076144631376893071846130232269613744035408973253176109526731416223) * 10 ^ 70 + 7041254805968089188268954662198826696482597675902338582658004022402278

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_121 : Polynomial.coeff recurrence5B1A3 121 = -(((10335342721377850998 * 10 ^ 70 + 5035154702534862572923991896111619582240492552520556950728222000286842) * 10 ^ 70 + 8483265232140750003333137755623540326132083213167695977594682257133256) * 10 ^ 70 + 3918765460260986930708961569827538481615188106270324870171012736765786)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_122 : Polynomial.coeff recurrence5B1A3 122 = ((17809500887309972773 * 10 ^ 70 + 389537295589012124768544618132760749961740344933447663722581336937568) * 10 ^ 70 + 7387373647853664956362895583078879890637156871615970982046496090811442) * 10 ^ 70 + 2530558322819145636410410882102518046683154865010155560392793247892800

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_123 : Polynomial.coeff recurrence5B1A3 123 = -(((29908992374299325751 * 10 ^ 70 + 3239743640880328259124141046919891436565252014648307913426074074578669) * 10 ^ 70 + 500752680102770679157157809191766578770308602564865165739952184761001) * 10 ^ 70 + 5173153221975314055056498604882195929958180367505236950583391464066971)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_124 : Polynomial.coeff recurrence5B1A3 124 = ((48951760269600012349 * 10 ^ 70 + 5874292031210545949279580903183675682565133935479537407191653392981596) * 10 ^ 70 + 189780706625666451904790599280570945487105744640210113292995962827063) * 10 ^ 70 + 3044280728043999258952540598961769158231287532380023765075282888744220

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_125 : Polynomial.coeff recurrence5B1A3 125 = -(((78079744847778631115 * 10 ^ 70 + 5821830394698950312050733849783578984864801402317684683670387043125693) * 10 ^ 70 + 8678422786636027772065327009531877573100628460324585006465897741623155) * 10 ^ 70 + 3869665026403211982307883206550595543515982581399848335593776420680104)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_126 : Polynomial.coeff recurrence5B1A3 126 = ((121364607585998657837 * 10 ^ 70 + 5958862001490954440904388510258798462711746816330232989441514068214060) * 10 ^ 70 + 6492624315705155760783140295148204192089193265008489113014575291529511) * 10 ^ 70 + 3225437658990032415234113899180482050050897165104763880945732695932851

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_127 : Polynomial.coeff recurrence5B1A3 127 = -(((183823717773467894923 * 10 ^ 70 + 3393688469398932450897173900274709046814366899001066530203793551170051) * 10 ^ 70 + 2427014054569189786508244642928304445474122346729439349744259918139416) * 10 ^ 70 + 9864177069980175360268080945421040134115832813200432507692270330353257)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_128 : Polynomial.coeff recurrence5B1A3 128 = ((271287755121519960626 * 10 ^ 70 + 7342764257172210909155037617179723803734311036353976017045333411142195) * 10 ^ 70 + 14823386406181447120381954121303543200563069105296447692663711249960) * 10 ^ 70 + 400413975950091750675222164503737787594433856699066148951689852516812

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_129 : Polynomial.coeff recurrence5B1A3 129 = -(((390059772774559461023 * 10 ^ 70 + 5071872746750954249240076329609452001809903077933333952812289931814916) * 10 ^ 70 + 354359117772907676365080030134145249375540393881227691726586782779228) * 10 ^ 70 + 5349127910595413846839138251518236869443121607370604695683654974388376)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_130 : Polynomial.coeff recurrence5B1A3 130 = ((546318435729620505400 * 10 ^ 70 + 3724998613128822706658276597349097648684690615869368398454775569087079) * 10 ^ 70 + 1091922735999417772010410869884767475042856611144822276194488230895768) * 10 ^ 70 + 6834501271251049910351418894784708512048559288470785262920882870979977

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_131 : Polynomial.coeff recurrence5B1A3 131 = -(((745249834384894173271 * 10 ^ 70 + 2472806428589243535725012552077609466662253902652287164645055547166483) * 10 ^ 70 + 4190395134111322859582954416623939869087995198686165442345050806466492) * 10 ^ 70 + 6023301237138156344832794525063443157375180949121996224705649965079815)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_132 : Polynomial.coeff recurrence5B1A3 132 = ((989943849148034203165 * 10 ^ 70 + 4423451444075916750793927011747503704641602577292229580898463474069650) * 10 ^ 70 + 6791104705765759050631915693709737980334693385708021615084810088702608) * 10 ^ 70 + 3599819620639341499624794696106787928730335229377186286559995126460575

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_133 : Polynomial.coeff recurrence5B1A3 133 = -(((1280158126502989283134 * 10 ^ 70 + 1726888523800262021938978216671146409967984516089545653377201802741562) * 10 ^ 70 + 4252597530908789726321119261855249996993419485583698616329627876487725) * 10 ^ 70 + 1921004841600522252281860752275785332834681359589926373579962214089569)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_134 : Polynomial.coeff recurrence5B1A3 134 = ((1611124254425567643514 * 10 ^ 70 + 346469575680168794347845754984212683221562481363654312796389289755080) * 10 ^ 70 + 4003224139736643245736126531983779168641116414090546428061806718199555) * 10 ^ 70 + 1216349503894157942067511922700780695403973329847321360302201111930312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_135 : Polynomial.coeff recurrence5B1A3 135 = -(((1972629497573415750960 * 10 ^ 70 + 244341727301535940580371818056161420435576364032844111716695232966589) * 10 ^ 70 + 1389605678092831028728272466462472190269685793709666736788776859291385) * 10 ^ 70 + 4158681345864962325579206561964824377778286188347956537332303010600655)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_136 : Polynomial.coeff recurrence5B1A3 136 = ((2348633050168285183677 * 10 ^ 70 + 8117451808024821331180575771159473556226133097842950729809396289466187) * 10 ^ 70 + 6947554741506310901642883003208319100510057106429475138043104366792607) * 10 ^ 70 + 5822247759172530530787376644668523431706327224117656670150946211961004

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_137 : Polynomial.coeff recurrence5B1A3 137 = -(((2717649726443993347434 * 10 ^ 70 + 1515573334363795861255852385271253010778850342004540928174172323824777) * 10 ^ 70 + 9373328737736251789784852363978070837816168718661388378972827433376923) * 10 ^ 70 + 1019846845878413242277020683178924864478493689433185050271455166319524)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_138 : Polynomial.coeff recurrence5B1A3 138 = ((3054046270775505497919 * 10 ^ 70 + 1318441712448865336851405874885812432417836093987697507437109386261256) * 10 ^ 70 + 9627566182456178193647452896797907442889232210586558435232956250214752) * 10 ^ 70 + 7387092921513363276124428699794725954326795150657836717180591289689992

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_139 : Polynomial.coeff recurrence5B1A3 139 = -(((3330250179936225517783 * 10 ^ 70 + 8763004371543385488050424444742130933103256158505566054450109340087802) * 10 ^ 70 + 9087615377683021990978519871921179156921717425352170369198614608277250) * 10 ^ 70 + 7842243468436521550757827665598622806751320845366594104687644983536403)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_140 : Polynomial.coeff recurrence5B1A3 140 = ((3519689370485187054435 * 10 ^ 70 + 4432602002262252154898692212117007298523293139962039305059375074918047) * 10 ^ 70 + 6790585125319774591609272371495414156770585047501515795787050811361305) * 10 ^ 70 + 3035636838716140799102387077978297015043319544787826016798144626484252

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_141 : Polynomial.coeff recurrence5B1A3 141 = -(((3600099762236623198376 * 10 ^ 70 + 6534571386600595380908059356992907505936113522918217864304949238063961) * 10 ^ 70 + 9896745054917929476136720192272616166032614966648419260414009575095069) * 10 ^ 70 + 1752943795295242863510056035617752412811417487616390868069321153574969)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_142 : Polynomial.coeff recurrence5B1A3 142 = ((3556701495990147550057 * 10 ^ 70 + 5680367418722054912216464244698213717306105251263467761403452731699698) * 10 ^ 70 + 26976130672103878793278796631138347778153340040335775303596402020712) * 10 ^ 70 + 5848164561698402787130881874449072211050574263679935494656221375556425

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_143 : Polynomial.coeff recurrence5B1A3 143 = -(((3384694301551762836723 * 10 ^ 70 + 4567049769922282952521000258621897674085516170814701758445283334816275) * 10 ^ 70 + 5941363747889741683532780140053724485209526483472171711459191139541688) * 10 ^ 70 + 6501660788342600050972515678346600057300147009546621341857260288049250)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_144 : Polynomial.coeff recurrence5B1A3 144 = ((3090583771640835470501 * 10 ^ 70 + 8316424717687908245546049307448572597862523675228644573866260532377944) * 10 ^ 70 + 8750511790874227734430881624703257066403092219399795929581676133847779) * 10 ^ 70 + 1256509104241441492232960117212073453017017267820719942483390755039508

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_145 : Polynomial.coeff recurrence5B1A3 145 = -(((2692022593218959453998 * 10 ^ 70 + 4748822075571308564213074927054545764823354973474979343890055301967263) * 10 ^ 70 + 5500973950806113521136735598839085827551088064216606310680346333106782) * 10 ^ 70 + 515710178288645788807810765558772609681294029870589188687027240130930)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B1A3_coeff_146 : Polynomial.coeff recurrence5B1A3 146 = ((2216104882931336144643 * 10 ^ 70 + 8976694059654915158070403012114179343309106186651066982148453835506915) * 10 ^ 70 + 8356550929927589729829570492642282556276277230628693777764264380838614) * 10 ^ 70 + 5736688750375168951848958756053562242400360546720824597428067795720509