Recurrence 5 lookup certificate: B2A3 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.recurrence5B2A3_coeff_218 : Polynomial.coeff recurrence5B2A3 218 = ((16693 * 10 ^ 70 + 4111356529401431157921229186743009128074467097272857615376374379844950) * 10 ^ 70 + 7610200159132735692438523866982373104834512798727008966263729961457582) * 10 ^ 70 + 8837082924762066433853892240346871728710907782205998416838373714146779

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_219 : Polynomial.coeff recurrence5B2A3 219 = -(((7303 * 10 ^ 70 + 8201564871956665786565812301783610332476376730937760114355854407519147) * 10 ^ 70 + 8272664604770562745303241762155293352638667760704241930882527826747891) * 10 ^ 70 + 4675634579226356282175718001486629125114733380242926667990343959980710)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_220 : Polynomial.coeff recurrence5B2A3 220 = ((3075 * 10 ^ 70 + 6893052526572052926124841661385842967539823941741854268395366976808781) * 10 ^ 70 + 3972815772731290297468200211542591991744693462753323283766201572496127) * 10 ^ 70 + 5800008468264202767287929201455395393176384097809292277460877121566453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_221 : Polynomial.coeff recurrence5B2A3 221 = -(((1247 * 10 ^ 70 + 7652263882136714018684707816376011414526423921459154472462927382085062) * 10 ^ 70 + 4658364842346547911902826239775831624476807080660752475703463829064536) * 10 ^ 70 + 7159446925051159889382052201261546727388122358517593193013573758308739)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_222 : Polynomial.coeff recurrence5B2A3 222 = ((487 * 10 ^ 70 + 7897516646932099496105446269894720364330091085327160649312689038956594) * 10 ^ 70 + 3359067849466256850305658809755209346624344912200235970998916000977684) * 10 ^ 70 + 5310089113619714428251176694572980773275359017502863997239990336008839

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_223 : Polynomial.coeff recurrence5B2A3 223 = -(((183 * 10 ^ 70 + 6487233132699722019764106669975978278397906330401612613870776248961163) * 10 ^ 70 + 397492164893615274549925166884262147756629312606845194331126113085912) * 10 ^ 70 + 7305585174473444838091031016559855213306059003706366522726518848899082)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_224 : Polynomial.coeff recurrence5B2A3 224 = ((66 * 10 ^ 70 + 4805067697323113278097910480981455446855801370087296852377168718791710) * 10 ^ 70 + 7938403878206202961090491208602797341844346826891428681021855739115282) * 10 ^ 70 + 1607418798235665299432482464330849630683045523597519113028828468777627

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_225 : Polynomial.coeff recurrence5B2A3 225 = -(((23 * 10 ^ 70 + 710535905253184248937059962009084372674153994695171600326800736436427) * 10 ^ 70 + 9237985652015848257393838612147072337451863328547584225024700653438886) * 10 ^ 70 + 8924920162580287437393042942484687182560339994405152504140231238507310)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_226 : Polynomial.coeff recurrence5B2A3 226 = ((7 * 10 ^ 70 + 6386404700743127576011180206224233594046486763556436385041774939131338) * 10 ^ 70 + 2529635180821945512827760894965779606703524191399622052679836171288463) * 10 ^ 70 + 4695344934035401886991603737929203399605480901599672575034718760563692

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_227 : Polynomial.coeff recurrence5B2A3 227 = -(((2 * 10 ^ 70 + 3944192731882255287563695231602301464075188628977855421286866532147277) * 10 ^ 70 + 495850519993546195715820109788567865318900415821809084191552183006697) * 10 ^ 70 + 9705951830811221051569388179754893658847206948112264991767403499444109)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_228 : Polynomial.coeff recurrence5B2A3 228 = (7015659687336382374457579040535430723840245781317358980830187790516085 * 10 ^ 70 + 2518183560081095346549723709939317805893136055735414936184057184068227) * 10 ^ 70 + 2757491967355695608457236601688937508346265595781657309223061908073049

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_229 : Polynomial.coeff recurrence5B2A3 229 = -((1876982827617314100120492070273098465319273812569911666579506727504859 * 10 ^ 70 + 6726624072913506659756512278375213193153388191490581889555768830574230) * 10 ^ 70 + 7366169638396086385137881739219449995602518677262892864937482388987610)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_230 : Polynomial.coeff recurrence5B2A3 230 = (435750833826197449826475196094972737429416829138114219691046060062141 * 10 ^ 70 + 7828087403568431578564503868437951559577895380380493473823227720005268) * 10 ^ 70 + 1597496039536590221049947120933747899854111903188594198069452500109106

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_231 : Polynomial.coeff recurrence5B2A3 231 = -((75112647360059848111844564559264931652279445602715874470411506413715 * 10 ^ 70 + 8603914948510396600363326546379543206495870416560680164429022072301970) * 10 ^ 70 + 7947865724214729531046564262640427821914383720791559881733725878953602)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_232 : Polynomial.coeff recurrence5B2A3 232 = (1452148910187265514212847998199617466582328953845994350391471495990 * 10 ^ 70 + 776903749082371612030311220561527718244107628272486019208261398613718) * 10 ^ 70 + 255222136166749972200453499636115370271114034298729436609357914599575

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_233 : Polynomial.coeff recurrence5B2A3 233 = (6736860419126748197069495513837266234946982782757384291922001030204 * 10 ^ 70 + 7040933878131643664465334310461524125035900663951641019273819636561724) * 10 ^ 70 + 5616777012900044234875679868327867999403175310363462174643740708346691

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_234 : Polynomial.coeff recurrence5B2A3 234 = -((4227775537378530051198908798926324889666587613391155992832414371242 * 10 ^ 70 + 4482541888591023730097859645383336897624236180643251710660714565436947) * 10 ^ 70 + 5823664376064934338365816683297196292048191361849407059619958336149616)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_235 : Polynomial.coeff recurrence5B2A3 235 = (1874235901269294229145571734931422435067409425150951725998035913427 * 10 ^ 70 + 7905688977040129662336353748454663725743055863703821908342306779056022) * 10 ^ 70 + 3837868450060396771050914762801389928202925284321991575805632012533580

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_236 : Polynomial.coeff recurrence5B2A3 236 = -((703002827691833788639809366349743638846953873869175552650749902355 * 10 ^ 70 + 976706994177380724885871779069252314804333990244053893208997954758925) * 10 ^ 70 + 6682087880150208052404624672564582271148010098242283031224054977082166)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_237 : Polynomial.coeff recurrence5B2A3 237 = (233094381522530729226076402586446808235133940896985483787668699564 * 10 ^ 70 + 6203404148901878572173677094245018971923809732695649003824156503533917) * 10 ^ 70 + 7698105171026362404126732792600342647727458788546304417302830203198433

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_238 : Polynomial.coeff recurrence5B2A3 238 = -((68150734461920570907517511846108596782894572619695413452717878882 * 10 ^ 70 + 8252153369502275728372050879597498309243781071305231490369971029434298) * 10 ^ 70 + 2499311184841639819867024467730195895718628750483374060455739856912511)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_239 : Polynomial.coeff recurrence5B2A3 239 = (16615331225985531838091105971699200417414572353003328835438167990 * 10 ^ 70 + 5844906523910499373185297322855230539953297546796861042801681122925284) * 10 ^ 70 + 6235714307978179231439413834596464141072137314045115188779579460943891

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_240 : Polynomial.coeff recurrence5B2A3 240 = -((2606786093312924645947509993903148834217804144614130237278563686 * 10 ^ 70 + 2478189952986102971685871655579309008054326605707996392081271091965002) * 10 ^ 70 + 4775026610850667293123605734271592725171024597450170968512217884695478)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_241 : Polynomial.coeff recurrence5B2A3 241 = -((372107304811180494298763346069304853331938391305629040909956352 * 10 ^ 70 + 9614389979906458097809480372469283865869967617607010694328977379533676) * 10 ^ 70 + 4855549327221531492656423195961892183183006863039302764349116357601502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_242 : Polynomial.coeff recurrence5B2A3 242 = (609847396187572116610581028421224905463483867311292111261406106 * 10 ^ 70 + 3763466295940162736641632125613177058820420638047939620492964634374014) * 10 ^ 70 + 9891390656916244629828313815129875863288616910392139294582810263407

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_243 : Polynomial.coeff recurrence5B2A3 243 = -((382420224203540197519319026384322470822321898390338177684789689 * 10 ^ 70 + 4203168793659039693412759290957390306101683993930222721336920276211414) * 10 ^ 70 + 5678555948335774960559982914067426058449662659570390594401007896049044)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_244 : Polynomial.coeff recurrence5B2A3 244 = (190080638573161079730022059259217998349154299998548255447920148 * 10 ^ 70 + 7756127181601803415665438021133876810058510610136363546174279521237261) * 10 ^ 70 + 5068663287200328383951004522915861508430209313115612467900245196470898

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_245 : Polynomial.coeff recurrence5B2A3 245 = -((84084474943034166098542127199153276567139248661284948779417390 * 10 ^ 70 + 8973829125404653825519114056655938196100899182760370617594320433078871) * 10 ^ 70 + 2960116508339549753663593296004069149228954631010836719678368258697211)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_246 : Polynomial.coeff recurrence5B2A3 246 = (34483998853563872809908093804431405457473667516581251619917849 * 10 ^ 70 + 4714293927681413745193067660323674435063558702006246586868390327548693) * 10 ^ 70 + 1473284136565613740338330760310915313386676756574747916910809767149663

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_247 : Polynomial.coeff recurrence5B2A3 247 = -((13360240874557270442993378068876465597813416853687659080589625 * 10 ^ 70 + 7766550537798360366500280238567534487969812487358754762090050732987505) * 10 ^ 70 + 8572641074251067775643707952689304653703320156257650963047714726329357)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_248 : Polynomial.coeff recurrence5B2A3 248 = (4938403953460857513977524315553407022088363783812810404223817 * 10 ^ 70 + 8553156582951290873905189453525839009098842354088025439878005679227854) * 10 ^ 70 + 2741834954284277175514939996819145721600935306256787306436318074761294

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_249 : Polynomial.coeff recurrence5B2A3 249 = -((1751017584249474355915265410718548560959754367730164432335350 * 10 ^ 70 + 5360968735000592467971304961593498682088663583309567850793024235527270) * 10 ^ 70 + 5115410975149129701212831765173724206409492717202794441647827549783002)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_250 : Polynomial.coeff recurrence5B2A3 250 = (597276838862391469942837073490379202602529224397220924819628 * 10 ^ 70 + 4345452419090475497449370070218748098323905727040541573753222290774883) * 10 ^ 70 + 8322925191624438247522935706116871295435428288727271011329330127973417

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_251 : Polynomial.coeff recurrence5B2A3 251 = -((196236707572347987085604115409971859528581299679478670000235 * 10 ^ 70 + 7969767456272024922525972595487392281516437688816388224537402601738228) * 10 ^ 70 + 7533633296074237101231313118981396005511262907814069042284457537757973)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_252 : Polynomial.coeff recurrence5B2A3 252 = (62110495426971300381306234594588769728145031617590966623994 * 10 ^ 70 + 3547213232769182967770373490429955403478733156691846382917426370641334) * 10 ^ 70 + 7462631598926751219651243165114289899564720299359006350203425434999901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_253 : Polynomial.coeff recurrence5B2A3 253 = -((18927784846763359532908459178707808246080514928519922404201 * 10 ^ 70 + 7278749029617859098340539619659306397099401126417282649476808072906158) * 10 ^ 70 + 2704299755844933680560140810699107665029946115294225345746403020065083)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_254 : Polynomial.coeff recurrence5B2A3 254 = (5549402654558440100568686101448569829942660373352136793236 * 10 ^ 70 + 1277270950761511854407495395110321693832872236265370457323471309325095) * 10 ^ 70 + 243986389015246941178370257507826946378622913658608334707673769980243

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_255 : Polynomial.coeff recurrence5B2A3 255 = -((1564350050016517104312246379829176891638675811468172394539 * 10 ^ 70 + 5686497958000275964633873713415870389289635507714844741448322145893254) * 10 ^ 70 + 5520419241937665790567003479673468946442685941834387364531639716676370)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_256 : Polynomial.coeff recurrence5B2A3 256 = (423924534070801909912286619779797276280517683336815277618 * 10 ^ 70 + 2652264037212529558234982360476026603019142922542140782315565208783815) * 10 ^ 70 + 4971633245919205624780123804720639712534658929259329339911468945389627

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_257 : Polynomial.coeff recurrence5B2A3 257 = -((110467568428404791705972877587883424398230717435662745547 * 10 ^ 70 + 8510124988178932266765601539158779880569254880805289038545409374040427) * 10 ^ 70 + 8468187357215231607455834809283607339244758735876734062058206893807793)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_258 : Polynomial.coeff recurrence5B2A3 258 = (27687137380522326405024333727788443785338312899766793971 * 10 ^ 70 + 7676809598392084685961177057936870086371967842105389656356713857193449) * 10 ^ 70 + 5763371836906343559612584646493248130334364571862996608085057347098505

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_259 : Polynomial.coeff recurrence5B2A3 259 = -((6667874261771299440645911622469306227176319277794053333 * 10 ^ 70 + 742344839785867133186520551565028737162418543278569918537762484739907) * 10 ^ 70 + 5902702199138835359073376634831682621244199248216998584621343297455197)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_260 : Polynomial.coeff recurrence5B2A3 260 = (1536640895718523693187929548176258359243867471689447880 * 10 ^ 70 + 6364476205021731360052233322904427451364718457848452945746411231473381) * 10 ^ 70 + 7275736117390053967636366367784751854662065653285814168859531878613708

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_261 : Polynomial.coeff recurrence5B2A3 261 = -((335576344839130426214467539885940940449345056789638709 * 10 ^ 70 + 6508318354258600648716579537501749181741203448487021525750028981055612) * 10 ^ 70 + 5297029521645968895234033182809196974284592082394852608748838010093284)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_262 : Polynomial.coeff recurrence5B2A3 262 = (68140590326394272504617709348230240024985409849297633 * 10 ^ 70 + 8488373116270797803370711265231932745946945436856439373147390462186811) * 10 ^ 70 + 7074745916028696008913312084128949568628774114654078456544563060010903

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_263 : Polynomial.coeff recurrence5B2A3 263 = -((12413918291228995925034269344216916615929889745475223 * 10 ^ 70 + 1064602055894295913286179800006908282297529277417980830653478171026021) * 10 ^ 70 + 4332379231838389845195322653448956414172280936341758816597265851314799)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_264 : Polynomial.coeff recurrence5B2A3 264 = (1877008210290334882708220473320612766447773929554440 * 10 ^ 70 + 1026327442211936629215830237873736845091200000411503728061689061473959) * 10 ^ 70 + 775830475078108327732020144682538741051920606805652552945319676443511

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_265 : Polynomial.coeff recurrence5B2A3 265 = -((180025412787013870855251374863036319919100986136751 * 10 ^ 70 + 2403323129324229479589813983262847037605674964012542271361444268168655) * 10 ^ 70 + 1896756817982069992951835774174409130695966650147901745246085465140877)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_266 : Polynomial.coeff recurrence5B2A3 266 = -((13407515729990856752138718817325119507024304344516 * 10 ^ 70 + 4394165740385975562901160075940133260873039111524169246123556395637663) * 10 ^ 70 + 9556508302146683120860245638469604651698212763493619443401076262406008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_267 : Polynomial.coeff recurrence5B2A3 267 = (12633454102324746758534040570856720401468755573653 * 10 ^ 70 + 1975716290528625963461633904761157416658637381697001579404009209999782) * 10 ^ 70 + 6041711051074638054401574661647609925846152321864794812641992969034073

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_268 : Polynomial.coeff recurrence5B2A3 268 = -((3988015154314737472825823788363290898433084126476 * 10 ^ 70 + 8484243177028717421199180712828711114885357042044380153557568226784993) * 10 ^ 70 + 3814105170317233545642746751667424276398574365153299165373761663571853)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_269 : Polynomial.coeff recurrence5B2A3 269 = (884096402456744597860029583361395903683736996297 * 10 ^ 70 + 5219752805914330541361879387765846324663870161575742230155717916113306) * 10 ^ 70 + 5526305348394447455727013693084657170505697077204128256923987476384510

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_270 : Polynomial.coeff recurrence5B2A3 270 = -((144175563803592012456706300663402923076384190854 * 10 ^ 70 + 8476548717533050179050708467036271155022147587554735963275637917300219) * 10 ^ 70 + 2839140294487007447235950211382087748111574550781904124099867081260820)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_271 : Polynomial.coeff recurrence5B2A3 271 = (14109523240114645639070807992829770454378916678 * 10 ^ 70 + 2879066533059221681058013572140663878484332633523586970130453820850805) * 10 ^ 70 + 2629369713819055564238131906923679231199935235211644386596620836885042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_272 : Polynomial.coeff recurrence5B2A3 272 = (751712370621071236892694526708164014802676708 * 10 ^ 70 + 3661354857348807699381914292418904522141485446830806269624465528776717) * 10 ^ 70 + 1006903140383369570842282597733185167941612152021264776496348356143698

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_273 : Polynomial.coeff recurrence5B2A3 273 = -((742596012715101668180121080612369959494196579 * 10 ^ 70 + 4599747522927140295279146097559236943278155795303545255517033699614440) * 10 ^ 70 + 5937470738325353186845271758374865770684716194220065297560273753386799)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_274 : Polynomial.coeff recurrence5B2A3 274 = (206987248452131958758825718987345383799492645 * 10 ^ 70 + 2748313226611879575822861592538846224332992556794716607676686871010616) * 10 ^ 70 + 3670337044145492263973230565003655242666636439196692150689866305346069

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_275 : Polynomial.coeff recurrence5B2A3 275 = -((39934803844003054178005319638272952307537013 * 10 ^ 70 + 6931378180669988670290142309849319939129454527050253738163460574718409) * 10 ^ 70 + 5754779207721971618746643173367829438745309522203997482264105062573954)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_276 : Polynomial.coeff recurrence5B2A3 276 = (5936693106171337959198058522093005013457949 * 10 ^ 70 + 5884804706327172093519130994476009967893654134670247041127751134293748) * 10 ^ 70 + 2949302576133629121450164315733675520807342392672303687398822381409537

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_277 : Polynomial.coeff recurrence5B2A3 277 = -((686840481128940684632784757557129028619818 * 10 ^ 70 + 3444920639037895704466236904293796886410221817815731625189273444783952) * 10 ^ 70 + 2597311853251958798986212896891008217350641722338455107630872765143280)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_278 : Polynomial.coeff recurrence5B2A3 278 = (58807464890362283527441382232166532881684 * 10 ^ 70 + 6888227821097738248072514685024715921446346077765866109938716927462671) * 10 ^ 70 + 5629201908039046198853116334031326947202551309847097082062233068616564

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_279 : Polynomial.coeff recurrence5B2A3 279 = -((3024546340947104787322458598887898132997 * 10 ^ 70 + 3973722404411679542999270076154869724016416886723488781132028571461144) * 10 ^ 70 + 1891116458321873274227768494025039375902852446904261868508945328275141)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_280 : Polynomial.coeff recurrence5B2A3 280 = -((38399691254034170442620943779603885431 * 10 ^ 70 + 6873214653897787393834769047074817003930823914766703925572012553921001) * 10 ^ 70 + 1537024808313266372347783752097079571780141311212483285297687795919159)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_281 : Polynomial.coeff recurrence5B2A3 281 = (25751630150240390325844235320854854039 * 10 ^ 70 + 4135431580730239888420717825923457149130182473416613850917170691900806) * 10 ^ 70 + 6859653455334144137895360674524251023809541407048705420609997141539809

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_282 : Polynomial.coeff recurrence5B2A3 282 = -((2727457516191637195188562662742710990 * 10 ^ 70 + 8397130902142466072930034611847740880054810608054084674411597229110965) * 10 ^ 70 + 2850600336994429110912082958641173350908635087343687434080575841001493)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_283 : Polynomial.coeff recurrence5B2A3 283 = (154996696695594187824517760901087328 * 10 ^ 70 + 4251666093653747811173749020373930312907979409817063196281253612520332) * 10 ^ 70 + 5714004089637561810848722793217456211822388622828642892355587493384944

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_284 : Polynomial.coeff recurrence5B2A3 284 = -((3848870321508211267731086275158339 * 10 ^ 70 + 7539547934385749056072434412083945461569061632936801364224037312817004) * 10 ^ 70 + 1892057625783966587464955636961373250390499292873867226834416451966962)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_285 : Polynomial.coeff recurrence5B2A3 285 = -((86724349149485785721479766228865 * 10 ^ 70 + 8894673320668243673452335473339971012343323295462251270467170484460774) * 10 ^ 70 + 2487459375076124001463007507397576836586234007249244259473011384136649)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_286 : Polynomial.coeff recurrence5B2A3 286 = (8289209665602542532325834173478 * 10 ^ 70 + 7317662408815244272296186937667017941072714223862125981321862882470430) * 10 ^ 70 + 7567354201063270097632237835050268613560036165135296642084505381729102

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_287 : Polynomial.coeff recurrence5B2A3 287 = -((118940211514190040095155839478 * 10 ^ 70 + 6490227751684490519350471969998932185650612176914154657106201912970631) * 10 ^ 70 + 6925207456535516485564063323307878495238958922228569521720324191904523)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_288 : Polynomial.coeff recurrence5B2A3 288 = -((2819891874363770582975333381 * 10 ^ 70 + 9398167970244767844000849779574761027954706037563935550143393388332203) * 10 ^ 70 + 2476702525005906486313387869546262167238516980269689111614366952245287)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_289 : Polynomial.coeff recurrence5B2A3 289 = (25463444655023966774717387 * 10 ^ 70 + 4794455433627505974566208215106050370743706697266650208307567201097725) * 10 ^ 70 + 3589504188543493855408262986302807754645892686413146482465438116151905

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_290 : Polynomial.coeff recurrence5B2A3 290 = (433906456760591289412345 * 10 ^ 70 + 7707486948754950685927348483526229694036477735555445029850015998675463) * 10 ^ 70 + 1395209125435730742785023175262341746701364945679580421841597039795488

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_291 : Polynomial.coeff recurrence5B2A3 291 = (212047891261002068987 * 10 ^ 70 + 6614008385524315487478734260485611915668098797641674648522362928999301) * 10 ^ 70 + 1232733906029912546091777237463543768791129178517481064842161960095683

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_292 : Polynomial.coeff recurrence5B2A3 292 = -((13518408639844330333 * 10 ^ 70 + 4287295760434546308407793749925481283810741518749685405359012507757775) * 10 ^ 70 + 315770001514796050926908506572736886602015194820943115034359577534593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_293 : Polynomial.coeff recurrence5B2A3 293 = -((33226796052068817 * 10 ^ 70 + 8650685262001787930223461494354360896969953253256532601886055163020384) * 10 ^ 70 + 536238348567624821425054050836959724916836142999611057271609152287909)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_294 : Polynomial.coeff recurrence5B2A3 294 = (115939093188888 * 10 ^ 70 + 3252904050868142392310800599099042677834481357144689873692820457908652) * 10 ^ 70 + 541745556940109938183368115744654391209797158636859656199881138803386

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_295 : Polynomial.coeff recurrence5B2A3 295 = (345495533642 * 10 ^ 70 + 4945079459995286747957287153734273847696402534191440414913205128481896) * 10 ^ 70 + 7800124057079819371692834737946686648078121442838776326349827525851545

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_296 : Polynomial.coeff recurrence5B2A3 296 = -((504363852 * 10 ^ 70 + 6791424008057756101522817923971393406476791753198516350277832860503506) * 10 ^ 70 + 2917078978997013238288016798944716777206531770883093050897857668817610)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_297 : Polynomial.coeff recurrence5B2A3 297 = -((1207317 * 10 ^ 70 + 3788100994155306779424877000782852596244807487668003621482898313119298) * 10 ^ 70 + 1625874016889579818950231786412316373192360130433754683042113135500217)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_298 : Polynomial.coeff recurrence5B2A3 298 = (1310 * 10 ^ 70 + 9098849070668636309147327716639100963684329901389085700375849105551109) * 10 ^ 70 + 5345717743997164937257596950351371619606779468637679352772238479132577

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_299 : Polynomial.coeff recurrence5B2A3 299 = 8951339088841467914644878784506154822385514855991002260329596100524233 * 10 ^ 70 + 9146120525868919543766865723479458228116616993928799968270200369976910

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_300 : Polynomial.coeff recurrence5B2A3 300 = -(6728118100740322612864188019863958007441804742355505221892662241619 * 10 ^ 70 + 2016853200722501091551018024328007081019374240132651166459265290188189)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_301 : Polynomial.coeff recurrence5B2A3 301 = -(249064310112960556473423077599439495063463349104725234760057321 * 10 ^ 70 + 9832967718950954697129273699824113685124855830703076031294641410338122)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_302 : Polynomial.coeff recurrence5B2A3 302 = 180393885932545700309053067866379235540490420201272077197215 * 10 ^ 70 + 5812504730409037702652760565720575799627211236073578071011782301377810

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_303 : Polynomial.coeff recurrence5B2A3 303 = -(2426852626663974412487691834743716741164874475667190770 * 10 ^ 70 + 3044172133252466244212738176505640746374030426195730553263822825515064)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_304 : Polynomial.coeff recurrence5B2A3 304 = -(143878255635506536330830636521589905468773759682062 * 10 ^ 70 + 158339181508382232387578101846913438852755992778470433986209034721099)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_305 : Polynomial.coeff recurrence5B2A3 305 = 741114523802669245212167159580587433600289499 * 10 ^ 70 + 142823489141709913029834099925950711517116535446495729388054300755106

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_306 : Polynomial.coeff recurrence5B2A3 306 = 1402682626580096834937252990138841574574 * 10 ^ 70 + 3433116323786234661290594071312924290357215016035187528880876374181271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_307 : Polynomial.coeff recurrence5B2A3 307 = -(1126625880180929358338937166496102 * 10 ^ 70 + 7323701329534353496615714702246744963665555468769230319742889837114922)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_308 : Polynomial.coeff recurrence5B2A3 308 = -(55320214875044707932456221 * 10 ^ 70 + 9966177261641144618850906993931715385802085855417811871517770279883629)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5B2A3_coeff_309 : Polynomial.coeff recurrence5B2A3 309 = 2401281935794764849 * 10 ^ 70 + 1317265882802248857700354994805798043618403265673332774640179025005930