Courtade–Kumar proof module `CKLaneC.RSC2.S01_0164` (transplant)

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

-- ===== source module CKLaneC.RSC2.S01_0164 =====
section

/-! RA-stat cover batch S01_0164 (generated by tools/emit_cover2.py; compact format). -/

namespace CKLaneC.RSC2.S01_0164
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 2005509209063424, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 5908722711110090752, sh := 144115188075855872 }
noncomputable def q0 : Cert := { V0 := [[[1104425774705700103]], [[(-19044235285291417), 156960325982930688], [1853013694332280]], [[116262878461675, (-2678494718422924), (-173534138326311)], [(-31476240712928), 260618886454719], [(-13152815137530)]], [[(-841634997758), 15627453897910, 8932154506297, (-8012191497561)], [194028368045, (-4286027325435), (-869103136573)], [224494343668, (-1856748936705)], [140878174111]], [[7237947721, (-105401769117), (-206621665798), 403757927651, 26517864257], [(-1608499545), 22829693221, 44360265482, (-39285849915)], [(-1387443137), 30923725762, 4729039296], [(-2407820852), 19907511820], [(-1754086688)]]], r0 := 434014145951, V1 := [[[1261204581572193392]], [[(-21713396411468871), 0], [2112724417556025]], [[131674835026498, 0, 0], [(-35715993979100), 0], [(-15004618611134)]], [[(-943833155343), 0, 0, 0], [215800883342, 0, 0], [255164374364, 0], [160737157927]], [[8051416461, 0, 0, 0, 0], [(-1748554471), 0, 0, 0], [(-1553082393), 0, 0], [(-2738047998), 0], [(-2001526633)]]], r1 := 74796976959, V2 := [[[18444134711353006875]], [[(-16829417358289), 26624359644], [(-45708019849586)]], [[14316026026, (-132614359), (-260137)], [(-297333754583), 938093735], [741478694]], [[(-140676607), (-2134154), 4275, 2], [275860495, (-4640656), (-13758)], [(-21950784), 8304467], [(-3395165)]], [[1812663, 3047, 6, 0, 0], [(-2702498), (-75799), 225, 0], [259134, (-40457), (-243)], [100286, 537], [26879]]], r2 := 167881361, V3 := [[[18445459268325324499]], [[(-31336422780269), 26047677775], [(-22540906263355)]], [[7285485, 341389536, (-506924)], [(-549767862092), 917920751], [(-8127952)]], [[1431, (-7285704), (-884), 9], [256662, 12048251, (-26806)], [(-107043), 8128425], [(-538)]], [[(-12), (-1430), 218, 0, 0], [55, (-256675), (-47), 0], [2271, 107043, (-474)], [(-10), 540], [2]]], r3 := 1298257417, Vm := [[[18444134744003619128]], [[(-16829692224516), 0], [(-45706858359934)]], [[14314914439, 0, 0], [(-297343653821), 0], [751975931]], [[(-140679689), 0, 0, 0], [275822128, 0, 0], [(-22042555), 0], [(-3392943)]], [[1812742, 0, 0, 0, 0], [(-2702605), 0, 0, 0], [258809, 0, 0], [100251, 0], [26872]]], rm := 18605332 }
noncomputable def w0 : Wit := { Z0 := { p := [[[1107290609184397605]], [[(-19192750741715258), 158184372740628229], [1867464323115782]], [[119744125433451, (-2741821534530752), 0], [(-32222721801362), 266780617587968], [(-13231012146566)]], [[(-894746844277), 17106303633350, 0, 0], [211522257082, (-4603245971624), 0], [228543961401, (-1890144592367)], [141644703299]], [[7898816368, (-127820977754), 0, 0, 0], [(-1878005854), 30217465297, 0, 0], [(-1482411163), 32649137343, 0], [(-2447535716), 20234957614], [(-1763127661)]]], r := 83706437151, ok := true }, Z1 := { p := [[[1265474981925025834]], [[(-21934572276246009), 0], [2134244940703751]], [[136850429066801, 0, 0], [(-36825967772985), 0], [(-15121156738932)]], [[(-1022567822031), 0, 0, 0], [241739722379, 0, 0], [261193098744, 0], [161879660913]], [[9027218707, 0, 0, 0, 0], [(-2146292405), 0, 0, 0], [(-1694184186), 0, 0], [(-2797183675), 0], [(-2015003041)]]], r := 18857656704, ok := true }, Z2 := { p := [[[17122729118895687115160]], [[(-99989290410305770909), 158184372740628229], [(-271566886334849528765)]], [[702596925922077989, (-2741821534530752), 0], [1587869594216009611, 266780617587968], [4559654486395936513]], [[(-5761581221403049), 17106303633350, 0, 0], [(-10967905423443162), (-4603245971624), 0], [(-26674738933560815), (-1890144592367)], [(-77803048998127844)]], [[55929564129046, (-127820977754), 0, 0, 0], [87663395270058, 30217465297, 0, 0], [183084402865242, 32649137343, 0], [455304298499510, 20234957614], [1337695551387006]]], r := 164031949393638, ok := true }, Z3 := { p := [[[32590402276881109396317]], [[(-724373627630345848881), 602118849800696436], [(-521056221207953625560)]], [[16959816921026092806, (-20303062247922691), 0], [11690369273386847571, 937727311181380], [8775087559400385534]], [[(-403056499209783651), 467136420594492, 0, 0], [(-274680290088483480), (-29588858616651), 0], [(-197576807997858070), (-6765138024581)], [(-150004761953085547)]], [[9646604101970565, (-11047503670109), 0, 0, 0], [6541833879151939, 638671720890, 0, 0], [4648812770236406, 216631874804, 0], [3384673978649531, 72858926237], [2582393907876842]]], r := 5259110910838363, ok := true }, iE := { p := [[[17125345524785040724609]], [[(-99991839659612112790), 0], [(-271562473722105746151)]], [[702629960070127804, 0, 0], [1587865640263293897, 0], [4559623222969862774]], [[(-5761939337650226), 0, 0, 0], [(-10967821443465622), 0, 0], [(-26674710339647982), 0], [(-77802714307277191)]], [[55933827437937, 0, 0, 0, 0], [87662354326247, 0, 0, 0], [183083855698506, 0, 0], [455303990363194, 0], [1337691385310319]]], r := 163980367956280, ok := true }, iHu := { p := [[[32593274453003721913801]], [[(-724389015708066199731), 0], [(-521051748140894541963)]], [[16960234761268516998, 0, 0], [11690354995018013585, 0], [8775055288914406212]], [[(-403066808621697553), 0, 0, 0], [(-274679788382908548), 0, 0], [(-197576689885491491), 0], [(-150004414407632807)]], [[9646855084837716, 0, 0, 0, 0], [6541821207438587, 0, 0, 0], [4648808951252314, 0, 0], [3384672651443863, 0], [2582389566398249]]], r := 5258146561848594, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[19870102266167837]], [[116017984976901, 0], [315087022139338]], [[(-137835315907), 0, 0], [1837113843377, 0], [(-293971795105)]], [[1120573299, 0, 0, 0], [(-2418247649), 0, 0], [(-1739441292), 0], [1718977205]], [[(-13665527), 0, 0, 0, 0], [19659181, 0, 0, 0], [(-1477), 0, 0], [10171463, 0], [(-15078746)]]], r := 11699398, ok := true }, de := { p := [[[(-136593599567874730790)]], [[324560402443326917, 0], [233455728073270238]], [[(-3957915848217201), 0, 0], [198296307306, 0], [(-2047785946707638)]], [[64356355333618, 0, 0, 0], [168432, 0, 0], [121153, 0], [23950712856039]], [[(-1177250402444), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-315140958632)]]], r := 140235112842, ok := true }, dde := { p := [[[(-382120700129026205890307)]], [[9319692504612379513704, 0], [6703638468229957195264]], [[(-227309573558918558913), 0, 0], [(-163503377670507814835), 0], [(-117607692567726088626)]], [[5544135940461219185, 0, 0, 0], [3987887255419142833, 0, 0], [2868480306529574966, 0], [2063292852065300568]], [[(-135222827816103345), 0, 0, 0, 0], [(-97265542815097376), 0, 0, 0], [(-69962934305602789), 0, 0], [(-50324215904025938), 0], [(-36198120211667213)]]], r := 10388062422513721, ok := true }, nJu := { p := [[[(-273187199135749461579)]], [[649120804886653835, 0], [466911456146540477]], [[(-7915831696434402), 0, 0], [396592614612, 0], [(-4095571893415276)]], [[128712710667237, 0, 0, 0], [336865, 0, 0], [242307, 0], [47901425712078]], [[(-2354500804887), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-630281917263)]]], r := 280470225675, ok := true }, Jd1 := { p := [[[(-764241400258052411780613)]], [[18639385009224759027409, 0], [13407276936459914390529]], [[(-454619147117837117825), 0, 0], [(-327006755341015629669), 0], [(-235215385135452177251)]], [[11088271880922438370, 0, 0, 0], [7975774510838285667, 0, 0], [5736960613059149932, 0], [4126585704130601137]], [[(-270445655632206690), 0, 0, 0, 0], [(-194531085630194751), 0, 0, 0], [(-139925868611205577), 0, 0], [(-100648431808051875), 0], [(-72396240423334426)]]], r := 20776124845027431, ok := true }, term0 := { p := [[[10974865231678236663747521015]], [[(-535331317270854799105521741), 0], [(-385041948902885199695926984)]], [[19584951130917729484806923, 0, 0], [18782043582694177460796605, 0], [10132322871587758330029023]], [[(-636903435731304172820171), 0, 0, 0], [(-687141954121293401898623), 0, 0], [(-494251046831655923123860), 0], [(-237009190045580495674199)]], [[19417686257612671144779, 0, 0, 0, 0], [22345982543279098629794, 0, 0, 0], [18082250427488125308066, 0, 0], [11561272932014452900737, 0], [5197514556358121309094]]], r := 2711305302496653841248, ok := true }, r0 := { p := [[[174586013425748831617454]], [[(-3445924275706925221654), 49472177049004630478104], [(-2769229694934836465302)]], [[54292972375645699649, (-962595230702342019497), 3417785721341943619447], [54163505336942061995, (-786072137628375002585)], [46497049803005535645]], [[(-858015357078145129), 14916861626073435551, (-62578079637639680027), (-16259931592655864902)], [(-834705907011629760), 15200223002585237918, (-54690336302402716177)], [(-906250752511343791), 13205918616402598785], [(-793395042349609650)]], [[14813789341732754, (-233272030738745040), 899418567964279353, 856152489240212804, (-527370235526698622)], [12836178589051449, (-231070332852030511), 1008006681418007524, 205439840005584618], [13846979041680885, (-254702567915960431), 920861129404891475], [15430629186160454, (-225408659282779145)], [13641023412615159]]], r := 315560004970585413, ok := true }, r1 := { p := [[[227459193397909382293123]], [[(-4470215883135895420018), 0], [(-3609779929542167700376)]], [[70086070823285203335, 0, 0], [70360536337963536826, 0], [60620561040854610585]], [[(-1104229872845609324), 0, 0, 0], [(-1079904198881170487), 0, 0], [(-1177778508986924570), 0], [(-1034489121365633554)]], [[19060620964597958, 0, 0, 0, 0], [16562896806211995, 0, 0, 0], [17927455763187038, 0, 0], [20059041971159096, 0], [17787387852897717]]], r := 16194286018131360, ok := true }, r2 := { p := [[[1939393192274092671025559968]], [[(-39558265219155354179999655), 67726314313039208870233], [(-66875993634709768959529524)]], [[760593946823561687967088, (-974216946798527050892), 449822075931730926], [1343970162858084733923549, (-1172354977095879710716)], [1741436792013852406987022]], [[(-15711764931857088822870), 15287083509716692321, 79815931365850, (-142875944451060)], [(-25532708666502522877387), 16347659006478450858, (-76674346611680)], [(-34674235852204081433741), 20455491276798782393], [(-40432510014655699066346)]], [[346629273597390876480, (-277175418832987382), (-109547307183582), 3454710572185, (-15759426281835)], [523739038343891990715, (-248809493601561048), 1618061093852, (-133386634903746)], [653763829423929871447, (-281601976575065531), (-44145524978362)], [799714498814362285325, (-357771858297787073)], [881613760473420687726]]], r := 2208300645853489278396, ok := true }, r3 := { p := [[[21945799535787080603778940877]], [[(-1070494102195214047164800452), 780816527961208067431138], [(-770014913898234667501979712)]], [[39164019571902007216930164, (-33510469791094929806754), 1726970182785460842], [37561129737106695064734291, (-13719769120513346509167)], [20263435355158267659523142]], [[(-1273620173444413259483011), 1170172484450288453168, 710309071055025, (-7189518752164464)], [(-1374180686860060935593282), 588620190075750822128, (-6571396951645204)], [(-988450206135267887138409), 240833043769992151014], [(-473997147219620048465537)]], [[38829760732103888642649, (-37155450739944794990), (-4749317325799382), (-6894278641695254), (-760112136944798)], [44688684221942713475325, (-20557965810467719431), (-607363506107470), (-7091629729447592)], [36162685307171503177938, (-10337082939952995410), (-5787376480103631)], [23121629061463105327149, (-4233468000672508379)], [10394649351454939855018]]], r := 254145820717104716062835, ok := true }, eta := { p := [[[(-1940104971546521894905668032)]], [[39578776174136559799370305, 0], [66888338459109470679536794]], [[(-761110009417639624115143), 0, 0], [(-1344325393292690072976061), 0], [(-1741652387494495960090936)]], [[15724414004576538908807, 0, 0, 0], [25541638007837787343523, 0, 0], [34680436094304258381593, 0], [40436281894049629436048]], [[(-346937824081667605352), 0, 0, 0, 0], [(-523957947936908551862), 0, 0, 0], [(-653919657012242242838), 0, 0], [(-799822968976200543161), 0], [(-881679885080828678189)]]], r := 197419317550979914814, ok := true } }
theorem sB_0 : stageB c0 w0 = true := by decide +kernel
theorem s0_0 : stageC0 w0 q0 = true := by decide +kernel
theorem s1_0 : stageC1 w0 q0 = true := by decide +kernel
theorem s2_0 : stageC2 w0 q0 = true := by decide +kernel
theorem s3_0 : stageC3 w0 q0 = true := by decide +kernel
theorem sE_0 : stageE w0 q0 = true := by decide +kernel
theorem sF_0 : stageF w0 = true := by decide +kernel
theorem ok_0 : (domOK c0 && cellCheck c0 q0) = true :=
  staged_check c0 q0 w0 (by decide +kernel) sB_0 s0_0 s1_0 s2_0 s3_0 sE_0 sF_0

noncomputable def c1 : Cell := { bc := 2075877953241088, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 5908722711110090752, sh := 144115188075855872 }
noncomputable def q1 : Cert := { V0 := [[[1108080290529894199]], [[(-19106308584449859), 157474292156099675], [1802038671155790]], [[116645501598533, (-2686945675218305), (-175253791089027)], [(-30606228394670), 253423103297878], [(-12347829158385)]], [[(-844808011377), 15672441890165, 9019922148634, (-8089910769740)], [188651448450, (-4166196488525), (-850726787482)], [210736441553, (-1742999444729)], [127740618308]], [[7270474171, (-105708379309), (-208633113271), 407581017322, 26954951447], [(-1564968900), 22165394411, 43416485418, (-38441583398)], [(-1302405106), 29022785131, 4463244883], [(-2183111738), 18050022870], [(-1536364843)]]], r0 := 400789481773, V1 := [[[1265371266645654985]], [[(-21783829114604846), 0], [2054572828490598]], [[132100354733162, 0, 0], [(-34727136608542), 0], [(-14086161133670)]], [[(-947281925626), 0, 0, 0], [209782378785, 0, 0], [239519808532, 0], [145746413246]], [[8086381753, 0, 0, 0, 0], [(-1700717170), 0, 0, 0], [(-1457728333), 0, 0], [(-2482455919), 0], [(-1753078029)]]], r1 := 66300067117, V2 := [[[18444043298252482925]], [[(-17424171880789), 28533769254], [(-45705093837324)]], [[14868774148, (-142057480), (-288637)], [(-297420379138), 971317995], [721732265]], [[(-146091279), (-2288484), 4743, 3], [276882998, (-4802459), (-14748)], [(-21367557), 8307648], [(-3190292)]], [[1882488, 3276, 7, 0, 0], [(-2712130), (-78532), 242, 0], [252190, (-40445), (-252)], [94221, 523], [24393]]], r2 := 153582045, V3 := [[[18445414186480281713]], [[(-32435958932700), 27916037272], [(-22540938781553)]], [[7807896, 365914289, (-562452)], [(-549768290378), 950440878], [(-8131133)]], [[1543, (-7808140), (-982), 11], [265749, 12476540, (-28735)], [(-107101), 8131624], [(-523)]], [[(-13), (-1542), 242, 0, 0], [57, (-265762), (-51), 0], [2272, 107101, (-491)], [(-10), 526], [1]]], r3 := 1250193932, Vm := [[[18444043333268081093]], [[(-17424466912854), 0], [(-45703890332287)]], [[14867584528, 0, 0], [(-297430645878), 0], [732242664]], [[(-146094581), 0, 0, 0], [276843332, 0, 0], [(-21459536), 0], [(-3188127)]], [[1882573, 0, 0, 0, 0], [(-2712242), 0, 0, 0], [251865, 0, 0], [94187, 0], [24386]]], rm := 17403033 }
noncomputable def w1 : Wit := { Z0 := { p := [[[1110973719469352981]], [[(-19256301114991038), 158710531352764711], [1816185430024729]], [[120161363755761, (-2750900159284434), 0], [(-31336973067642), 259455061432104], [(-12421634965649)]], [[(-898453159420), 17165909107965, 0, 0], [205776301084, (-4476710438235), 0], [214558548341, (-1774519280807)], [128439265094]], [[7938161391, (-128350451346), 0, 0, 0], [(-1828818550), 29396614440, 0, 0], [(-1392037753), 30651221191, 0], [(-2219308602), 18348466442], [(-1544323705)]]], r := 75271988099, ok := true }, Z1 := { p := [[[1269684250822117692]], [[(-22007201274275472), 0], [2075640491456833]], [[137327272863727, 0, 0], [(-35813683505876), 0], [(-14196154246456)]], [[(-1026803610766), 0, 0, 0], [235172915525, 0, 0], [245209769533, 0], [146787731536]], [[9072184447, 0, 0, 0, 0], [(-2090078343), 0, 0, 0], [(-1590900289), 0, 0], [(-2536352688), 0], [(-1764941377)]]], r := 16713898972, ok := true }, Z2 := { p := [[[16597232228431911820037]], [[(-96916728839571758078), 158710531352764711], [(-254220872953106137718)]], [[681369373755046216, (-2750900159284434), 0], [1486394118715921632, 259455061432104], [4123184388252460743]], [[(-5591861144910299), 17165909107965, 0, 0], [(-10271287066079058), (-4476710438235), 0], [(-24120548790447085), (-1774519280807)], [(-67965183739585388)]], [[54327082356342, (-128350451346), 0, 0, 0], [82148285330146, 29396614440, 0, 0], [165617273265926, 30651221191, 0], [397721059571062, 18348466442], [1128875920857821]]], r := 141123221036076, ok := true }, Z3 := { p := [[[31582230084308060750449]], [[(-701757021393046514461), 603967812562897348], [(-487676719888762462712)]], [[16428435205995240694, (-20361391737143617), 0], [10938888283694306359, 911512893368271], [7933642359693133273]], [[(-390401376802872268), 468395209224796, 0, 0], [(-256999341245815803), (-28749557557844), 0], [(-178592534735707025), (-6348884003578)], [(-131014515837220074)]], [[9343270439373646, (-11076352378538), 0, 0, 0], [6120393324802220, 620313085728, 0, 0], [4201766392849192, 203238518088, 0], [2955577328339947, 66043279259], [2178907286888353]]], r := 4730220670253373, ok := true }, iE := { p := [[[16599857337105666169693]], [[(-96919285884812983341), 0], [(-254216581506745209006)]], [[681402573718841006, 0, 0], [1486390275560408231, 0], [4123155037295620730]], [[(-5592221317001516), 0, 0, 0], [(-10271205208612401), 0, 0], [(-24120521956935714), 0], [(-67964880251732397)]], [[54331372401478, 0, 0, 0, 0], [82147270168376, 0, 0, 0], [165616758655241, 0, 0], [397720780268515, 0], [1128872271790809]]], r := 141076655519225, ok := true }, iHu := { p := [[[31585111080195573421709]], [[(-701772437565408142600), 0], [(-487672371867489499118)]], [[16428854034699914916, 0, 0], [10938874462374076892, 0], [7933612074786679425]], [[(-390411711182962444), 0, 0, 0], [(-256998854329638299), 0, 0], [(-178592424196735442), 0], [(-131014200803186826)]], [[9343522030952552, 0, 0, 0, 0], [6120381024343092, 0, 0, 0], [4201762813172956, 0, 0], [2955576128219236, 0], [2178903485447563]]], r := 4729298818639856, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[20499113938787003]], [[119685334871984, 0], [313931292517019]], [[(-142671817117), 0, 0], [1830275353702, 0], [(-284007554366)]], [[1159891661, 0, 0, 0], [(-2418253559), 0, 0], [(-1680481287), 0], [1604411645]], [[(-14145019), 0, 0, 0, 0], [19659181, 0, 0, 0], [(-1477), 0, 0], [9493560, 0], [(-13596707)]]], r := 11288008, ok := true }, de := { p := [[[(-136134692554548266641)]], [[324560799036426139, 0], [225542250177855453]], [[(-3957915847874427), 0, 0], [198296791919, 0], [(-1911306101774465)]], [[64356355333619, 0, 0, 0], [174343, 0, 0], [121154, 0], [21596679144160]], [[(-1177250402444), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-274534056917)]]], r := 136658427596, ok := true }, dde := { p := [[[(-369167907157065301629476)]], [[9003770724015240705916, 0], [6256857621773302887615]], [[(-219604164285735898676), 0, 0], [(-152606283854493305093), 0], [(-106048434405148522887)]], [[5356199128920165767, 0, 0, 0], [3722104479418757364, 0, 0], [2586547180613024670, 0], [1797431091612607123]], [[(-130639003144371147), 0, 0, 0, 0], [(-90783036083380562), 0, 0, 0], [(-63086516600320425), 0, 0], [(-43839782722252710), 0], [(-30464933756143846)]]], r := 9509818537950168, ok := true }, nJu := { p := [[[(-272269385109096533281)]], [[649121598072852279, 0], [451084500355710907]], [[(-7915831695748854), 0, 0], [396593583838, 0], [(-3822612203548929)]], [[128712710667238, 0, 0, 0], [348687, 0, 0], [242308, 0], [43193358288320]], [[(-2354500804887), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-549068113833)]]], r := 273316855184, ok := true }, Jd1 := { p := [[[(-738335814314130603258951)]], [[18007541448030481411832, 0], [12513715243546605775230]], [[(-439208328571471797352), 0, 0], [(-305212567708986610185), 0], [(-212096868810297045773)]], [[10712398257840331535, 0, 0, 0], [7444208958837514729, 0, 0], [5173094361226049340, 0], [3594862183225214246]], [[(-261278006288742294), 0, 0, 0, 0], [(-181566072166761124), 0, 0, 0], [(-126173033200640849), 0, 0], [(-87679565444505420), 0], [(-60929867512287691)]]], r := 19019637075900328, ok := true }, term0 := { p := [[[10243494348417245888851691590]], [[(-499655636584433900404912507), 0], [(-347198790123883322795918479)]], [[18279754859040732996967639, 0, 0], [16936068528658460520121351, 0], [8826763272835141362125768]], [[(-594458216452603805232195), 0, 0, 0], [(-619606680086833790613102), 0, 0], [(-430566058545538743433457), 0], [(-199471208293775551504884)]], [[18123628132106258581000, 0, 0, 0, 0], [20149719951494467561222, 0, 0, 0], [15752322146281087482915, 0, 0], [9730171324250316448282, 0], [4226038295268595256794]]], r := 2381500656654858893927, ok := true }, r0 := { p := [[[169227406045383928285867]], [[(-3341102920073882672969), 47951113129797902480930], [(-2592343815903918245364)]], [[52677134215471716239, (-933180024194984085193), 3311966776428821789020], [50715544046953088204, (-735834466050783299783)], [42046152547798208356]], [[(-833158192274660709), 14469586942097268296, (-60627809076839742982), (-15861308325892028960)], [(-782009392180308209), 14231211561227273033, (-51187442271581054465)], [(-819677118940754650), 11941408309729157358], [(-693074271612099483)]], [[14394998777782237, (-226453363502309892), 871510323856982505, 835084966323875274, (-514097020279336256)], [12034245438221573, (-216448082875780352), 943350624903380296, 193375159600507480], [12530772056456746, (-230351189394707183), 832576822100256154], [13482279945805083, (-196901053905499186)], [11511622181442038]]], r := 293938201643119608, ok := true }, r1 := { p := [[[220474114967424224475657]], [[(-4334050779053554175433), 0], [(-3379165951408007413749)]], [[67995622396101334228, 0, 0], [65879565830160509951, 0], [54817166490997129721]], [[(-1072156813389781025), 0, 0, 0], [(-1011680297388485759), 0, 0], [(-1065238459682720890), 0], [(-903675104531955928)]], [[18520384790633692, 0, 0, 0, 0], [15527293803151674, 0, 0, 0], [16222706204493269, 0, 0], [17525867051267847, 0], [15010600342912835]]], r := 14082855686316164, ok := true }, r2 := { p := [[[1812297029905385341412493027]], [[(-37002890546406585759482129), 65460662114159672824441], [(-60368633822972650385263912)]], [[712028598274877136670040, (-942610041666723749074), 449883234505504674], [1214342289535859926902762, (-1094632939859434155552)], [1518608086107892534997956]], [[(-14715347579166056219623), 14805744095162760496, 116268340460849, (-125352199876806)], [(-23087745494813724538239), 15277403900309398351, (-44271160168396)], [(-30264996760865991790513), 18451343674952766601], [(-34062283119632517675615)]], [[324715223833146155720, (-268701466216599730), (-80268328447690), 3031440096661, (-13938807519427)], [473800057465506100700, (-232724114383449317), (-102950296694835), (-117768001572773)], [571057752991380155232, (-254274076804537487), (-78769510689568)], [674315964404212106269, (-311731114208434240)], [717514924187749801001]]], r := 1854040129494703330973, ok := true }, r3 := { p := [[[20483191059688405566426543393]], [[(-999148455147648716929909493), 754307668076550651405423], [(-694333194455632090109225066)]], [[36553826480310030195598203, (-32373154821512225598227), 1730155677253109829], [33869376751240266660217774, (-12804875478306175512518)], [17652435132923112587417672]], [[(-1188736059789000994349168), 1130457859344608216935, 2524935141866493, (-6250161502654944)], [(-1239117012788709087402594), 549371041161306291129, (-5545879263897723)], [(-861085329414646860159591), 217152146574765464583], [(-398923919348105288475435)]], [[36241836365535155369593, (-35893328838534249028), (-3266693994295079), (-6079589388406676), (-665223636973190)], [40296380819336309478755, (-19181876937567908465), (-3158586561160619), (-6249750200910853)], [31503005265818859085703, (-9321254283531023645), (-658754705863222)], [19459546291633431375842, (-3687042517710493184)], [8451761559341733831974]]], r := 220358851290807438458655, ok := true }, eta := { p := [[[(-1812984952755602829493229758)]], [[37022715003698244279590648, 0], [60380159504843993531149519]], [[(-712527404173141367696513), 0, 0], [(-1214673961891166043410413), 0], [(-1518802546916264831772118)]], [[14727573779541596234614, 0, 0, 0], [23096082909582003721761, 0, 0], [30270589426019172486649, 0], [34065569872943628750447]], [[(-325013414856780594466), 0, 0, 0, 0], [(-474004387755218163342), 0, 0, 0], [(-571198326790916419802), 0, 0], [(-674410509514114134889), 0], [(-717570538605046139169)]]], r := 165639877090821167467, ok := true } }
theorem sB_1 : stageB c1 w1 = true := by decide +kernel
theorem s0_1 : stageC0 w1 q1 = true := by decide +kernel
theorem s1_1 : stageC1 w1 q1 = true := by decide +kernel
theorem s2_1 : stageC2 w1 q1 = true := by decide +kernel
theorem s3_1 : stageC3 w1 q1 = true := by decide +kernel
theorem sE_1 : stageE w1 q1 = true := by decide +kernel
theorem sF_1 : stageF w1 = true := by decide +kernel
theorem ok_1 : (domOK c1 && cellCheck c1 q1) = true :=
  staged_check c1 q1 w1 (by decide +kernel) sB_1 s0_1 s1_1 s2_1 s3_1 sE_1 sF_1

noncomputable def c2 : Cell := { bc := 2040693581152256, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 6196953087261802496, sh := 144115188075855872 }
noncomputable def q2 : Cert := { V0 := [[[1068573985890467746]], [[(-18619559816086312), 151915376868644263], [3531615672089041]], [[111564394361563, (-2621389740857379), (-157252350984988)], [(-60575399227459), 497205153231771], [(-49243479331154)]], [[(-788086949758), 15036583872510, 8181742607253, (-7274962199736)], [364308071071, (-8273977394477), (-1551850349966)], [848794408943, (-6956947372085)], [1036512886898]], [[6549400359, (-99061690574), (-189915345874), 371098085940, 22520945258], [(-2927683062), 43209711460, 80064506055, (-70387046158)], [(-5124407842), 117197662419, 16569721361], [(-17891286707), 146573487538], [(-25363797128)]]], r0 := 3521016781764, V1 := [[[1220324858560926385]], [[(-21232398709152149), 0], [4027198965923033]], [[126402851085000, 0, 0], [(-68765835152606), 0], [(-56183096663820)]], [[(-884221821595), 0, 0, 0], [405602989878, 0, 0], [965093416062, 0], [1182752247049]], [[7287194855, 0, 0, 0, 0], [(-3185060174), 0, 0, 0], [(-5740872384), 0, 0], [(-20351574197), 0], [(-28944676926)]]], r1 := 1048077488557, V2 := [[[18444054807775570042]], [[(-17070067968205), 27287349621], [(-92600434607668)]], [[13774091483, (-146101207), (-265105)], [(-592606537416), 1889906771], [2756585094]], [[(-129637125), (-2192504), 4528, 2], [521858468, (-10057777), (-27560)], [(-82640488), 32889771], [(-24803404)]], [[1596603, 2890, 5, 0, 0], [(-4895275), (-153015), 470, 0], [967503, (-172683), (-958)], [741438, 4268], [385849]]], r2 := 2525312904, V3 := [[[18445372955059623219]], [[(-31886160554264), 27650626875], [(-47280915256014)]], [[7553064, 323348789, (-535161)], [(-1099534061440), 1915317268], [(-33338420)]], [[1396, (-7553285), (-30), 10], [523067, 22433668, (-55624)], [(-391913), 33340352], [(-4392)]], [[(-11), (-1395), 220, 0, 0], [106, (-523090), (-4), 1], [9100, 391913, (-1933)], [(-73), 4414], [29]]], r3 := 7082677923, Vm := [[[18444054841023831486]], [[(-17070357462365), 0], [(-92598110271477)]], [[13772923918, 0, 0], [(-592627017774), 0], [2797860306]], [[(-129639715), 0, 0, 0], [521779250, 0, 0], [(-83013229), 0], [(-24786409)]], [[1596672, 0, 0, 0, 0], [(-4895451), 0, 0, 0], [966184, 0, 0], [741163, 0], [385740]]], rm := 262269508 }
noncomputable def w2 : Wit := { Z0 := { p := [[[1071168255637537520]], [[(-18755443063148250), 153024036519648217], [3557388966927285]], [[114758103305668, (-2679349009021179), 0], [(-61920131500720), 508198423846755], [(-49517247290498)]], [[(-836449786942), 16394014757952, 0, 0], [395879028929, (-8845733071532), 0], [863117144840, (-7073892470072)], [1041786134639]], [[7141072556, (-119492826706), 0, 0, 0], [(-3409593203), 56554146989, 0, 0], [(-5461072834), 123302449262, 0], [(-18167307492), 148826590662], [(-25486024929)]]], r := 855365541647, ok := true }, Z1 := { p := [[[1224192292157185738]], [[(-21434792072169429), 0], [4065587390774040]], [[131152118063621, 0, 0], [(-70765864572251), 0], [(-56591139760570)]], [[(-955942613648), 0, 0, 0], [452433175919, 0, 0], [986419594103, 0], [1190612725302]], [[8161225779, 0, 0, 0, 0], [(-3896677946), 0, 0, 0], [(-6241226096), 0, 0], [(-20762637133), 0], [(-29126885633)]]], r := 264393431637, ok := true }, Z2 := { p := [[[16661512798493141479253]], [[(-95726801628262654162), 153024036519648217], [(-519291630876341071923)]], [[659030707201259242, (-2679349009021179), 0], [2988810038539412520, 508198423846755], [17136091169934134945]], [[(-5258626301199129), 16394014757952, 0, 0], [(-20240744334871760), (-8845733071532), 0], [(-98697588301926484), (-7073892470072)], [(-574691037912863630)]], [[49219636329114, (-119492826706), 0, 0, 0], [157545416113149, 56554146989, 0, 0], [664344843610506, 123302449262, 0], [3311406526048414, 148826590662], [19420421618323824]]], r := 2116111122996927, ok := true }, Z3 := { p := [[[30715949415241563664393]], [[(-650591655838546019181), 564171628414091126], [(-964699681970921222946)]], [[14520769516028209876, (-18586126475356021), 0], [20628017794724944819, 1736988304088211], [31925893645587254463]], [[(-328998423093581889), 407264744291727, 0, 0], [(-462057212116158231), (-53616048364754), 0], [(-685118453022129596), (-24599626713464)], [(-1072549927895266581)]], [[7507203053225216, (-9179971830376), 0, 0, 0], [10491474337640628, 1100606792188, 0, 0], [15367963933756899, 770442493894, 0], [23066237091147833, 520507320797], [36288768918933081]]], r := 24985773172319366, ok := true }, iE := { p := [[[16664128609376236171721]], [[(-95729226510278837014), 0], [(-519282943672695785628)]], [[659061768123188349, 0, 0], [2988802882568345210, 0], [17135970247984028906]], [[(-5258953407692881), 0, 0, 0], [(-20240590251659897), 0, 0], [(-98697485722380808), 0], [(-574688493853613830)]], [[49223386050896, 0, 0, 0, 0], [157543559973255, 0, 0, 0], [664342868716399, 0, 0], [3311404347594476, 0], [19420359381022612]]], r := 2115641644267882, ok := true }, iHu := { p := [[[30718796822636735959607]], [[(-650605501008709040356), 0], [(-964690915288774707147)]], [[14521131498614217379, 0, 0], [20627993374907611340, 0], [31925769489824194747]], [[(-329006956883219316), 0, 0, 0], [(-462056360020182208), 0, 0], [(-685118051061190456), 0], [(-1072547300864200438)]], [[7507401321874185, 0, 0, 0, 0], [10491453704527552, 0, 0, 0], [15367951174573352, 0, 0], [23066228184614211, 0], [36288704434007459]]], r := 24982449446556206, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[20420051650914122]], [[117305608691838, 0], [636323973476108]], [[(-133730374571), 0, 0], [3648441257887, 0], [(-1169290752186)]], [[1036631043, 0, 0, 0], [(-4611563608), 0, 0], [(-6837835695), 0], [13438884898]], [[(-12053849), 0, 0, 0, 0], [35745898, 0, 0, 0], [(-5910), 0, 0], [78589971, 0], [(-231704913)]]], r := 144346989, ok := true }, de := { p := [[[(-135728381726512112648)]], [[309465293785336911, 0], [458862332164465075]], [[(-3598299913322064), 0, 0], [396594470325, 0], [(-7911125493142088)]], [[55787595632438, 0, 0, 0], [342776, 0, 0], [508255, 0], [181864954116541]], [[(-973039458705), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-4703403985772)]]], r := 764585283860, ok := true }, dde := { p := [[[(-358066626092417585414035)]], [[8326821362563523539189, 0], [12346666158283845228327]], [[(-193647008699190467734), 0, 0], [(-287131771916098541860), 0], [(-425747109494415162745)]], [[4503418806957706164, 0, 0, 0], [6677483058591764545, 0, 0], [9901095569636049993, 0], [14680934810151523465]], [[(-104730669929244582), 0, 0, 0, 0], [(-155290303688192681), 0, 0, 0], [(-230258036503171286), 0, 0], [(-341417088608161648), 0], [(-506239131384528596)]]], r := 50372003780633526, ok := true }, nJu := { p := [[[(-271456763453024225295)]], [[618930587570673822, 0], [917724664328930151]], [[(-7196599826644127), 0, 0], [793188940651, 0], [(-15822250986284176)]], [[111575191264877, 0, 0, 0], [685553, 0, 0], [1016510, 0], [363729908233083]], [[(-1946078917410), 0, 0, 0, 0], [2, 0, 0, 0], [11822, 0, 0], [2, 0], [(-9406807971544)]]], r := 1529170567712, ok := true }, Jd1 := { p := [[[(-716133252184835170828070)]], [[16653642725127047078379, 0], [24693332316567690456655]], [[(-387294017398380935467), 0, 0], [(-574263543832197083719), 0], [(-851494218988830325490)]], [[9006837613915412328, 0, 0, 0], [13354966117183529090, 0, 0], [19802191139272099987, 0], [29361869620303046931]], [[(-209461339858489164), 0, 0, 0, 0], [(-310580607376385361), 0, 0, 0], [(-460516073006342571), 0, 0], [(-682834177216323296), 0], [(-1012478262769057191)]]], r := 100744007561267043, ok := true }, term0 := { p := [[[9636683562117436622028926411]], [[(-448192856539652252775116804), 0], [(-664525068898987541654613291)]], [[15634344059942744668572512, 0, 0], [30907281344179201744162875, 0], [34370714031584272219660048]], [[(-484781358905000115185981), 0, 0, 0], [(-1078150960897846484611211), 0, 0], [(-1598608158647443972300804), 0], [(-1580233466031906060616838)]], [[14092402815514779664197, 0, 0, 0, 0], [33430882256916202276683, 0, 0, 0], [55765055495994142925845, 0, 0], [73498206726961671551193, 0], [68112755051445869474676]]], r := 12192382307075253870028, ok := true }, r0 := { p := [[[165284546558910514563458]], [[(-3188463030772198318106), 46860779267210101888241], [(-5153808957560104624379)]], [[48728933742595742826, (-891523774825973585904), 3244266197292230364153], [98616327720987461145, (-1463564354150174919563)], [170098092261975210788]], [[(-738899741232765541), 13400149378855386223, (-58197082322936840691), (-14452584681326831344)], [(-1475750970121656119), 27696779044257720155, (-101998524895828000930)], [(-3244555888605102836), 48329014425857829585], [(-5705024183826148200)]], [[12120769762370380, (-200900554727725055), 811266594261707010, 761168103589232322, (-471767704050401136)], [21792257432939122, (-408842227093457661), 1842812978414664502, 358546029868332618], [48160121855972134, (-912541041920255294), 3375249649724479585], [108612997191548428, (-1621419285698730183)], [192798672161272115]]], r := 1132349277820919212, ok := true }, r1 := { p := [[[215374671428758248104321]], [[(-4137399738457686785808), 0], [(-6719001363064069789964)]], [[62919923760885803106, 0, 0], [128136360723812092564, 0], [221791145355961328011]], [[(-950945154211680971), 0, 0, 0], [(-1909688731020265793), 0, 0], [(-4217589726806103206), 0], [(-7439462618763405072)]], [[15590477537748057, 0, 0, 0, 0], [28119837598526133, 0, 0, 0], [62365425730663999, 0, 0], [141220544278061039, 0], [251428853396849575]]], r := 188834743485477073, ok := true }, r2 := { p := [[[1800549016780245077128734779]], [[(-35477649077022226246904497), 64715844256595982409256], [(-122100669172694473303331726)]], [[651967600068854342578227, (-901081051917591302967), 450086486362314586], [2371042680634379106293230, (-2203647819857749160127)], [6251381587226429355406525]], [[(-12799435492024223692531), 13529944684931787723, 8190688705362, (-127292706363646)], [(-43050755411060669736256), 29770582000825803842, 7666634186676], [(-120297716754532163337518), 75598745377559191884], [(-285350618005877207703358)]], [[268094570080090118179, (-232832700193813103), (-81508612160236), 3016390933454, (-14018354978635)], [839005008678282790207, (-433771554054020909), (-64348553215116), (-110817181227270)], [2167679069759337398999, (-1008643805667867981), (-42711778797182)], [5455376927461587573764, (-2598738876080044549)], [12231595443073841773797]]], r := 25442064348531355470442, ok := true }, r3 := { p := [[[19269813502479282958648975672]], [[(-896241174706603634056792524), 705793873739095556759410], [(-1328927562438314514463258935)]], [[31263887285665796681667417, (-28737472574546996941121), 1738059576279573690], [61809577369873095664119850, (-24376299660597611988064)], [68737200833306176318093020]], [[(-969417593680972964259069), 954911169070434462756, (-1831642151156812), (-5596021973827604)], [(-2156136341012959469225885), 992179012555495871765, (-1005750806151610)], [(-3197044397000024955593845), 841051223769418947004], [(-3160321159327632523613832)]], [[28180650613148956887063, (-28878938851596858357), (-2755044464572786), (-5443029782355002), (-600314878704750)], [66856755682478502205307, (-32965124962110928764), (-4579387396799679), (-5172996239135214)], [111524398164556845394045, (-34230333062181091924), (-3816468893607532)], [146990482218305487793922, (-29011796523792713142)], [136220481136620390646292]]], r := 1234581193974689869111599, ok := true }, eta := { p := [[[(-1801210273777714613338773119)]], [[35495921815186219461992527, 0], [122123211746277423827193442]], [[(-652407008242689959673655), 0, 0], [(-2371664731195047497853295), 0], [(-6252155412880070136154485)]], [[12809712932544133330985, 0, 0, 0], [43065699421023520975115, 0, 0], [120319057555436546696311, 0], [285377228478417481539609]], [[(-268333663340229166533), 0, 0, 0, 0], [(-839354420343024032897), 0, 0, 0], [(-2168191589766339188283), 0, 0], [(-5456110599810154465626), 0], [(-12232511360281191993161)]]], r := 2391690801893265964990, ok := true } }
theorem sB_2 : stageB c2 w2 = true := by decide +kernel
theorem s0_2 : stageC0 w2 q2 = true := by decide +kernel
theorem s1_2 : stageC1 w2 q2 = true := by decide +kernel
theorem s2_2 : stageC2 w2 q2 = true := by decide +kernel
theorem s3_2 : stageC3 w2 q2 = true := by decide +kernel
theorem sE_2 : stageE w2 q2 = true := by decide +kernel
theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 2181431069507584, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 5908722711110090752, sh := 144115188075855872 }
noncomputable def q3 : Cert := { V0 := [[[1113378605303709685]], [[(-19196287537140817), 158219344887751572], [3462484980559765]], [[117200085971704, (-2699190919717493), (-177766906373408)], [(-58796095960935), 486860180704352], [(-45104151506708)]], [[(-849410818176), 15737534513857, 9148165407857, (-8203441021832)], [362369258010, (-7999657836785), (-1650078707309)], [769681317865, (-6366236562640)], [887742172044]], [[7317704214, (-106151591722), (-211571582107), 413162955824, 27598774912], [(-3008955379), 42487683016, 84194640554, (-74523291356)], [(-4756769368), 105970300539, 16428592860], [(-15169987797), 125429592926], [(-20316489328)]]], r0 := 2893078404804, V1 := [[[1271412008165663026]], [[(-21885919542430955), 0], [3947620994673515]], [[132716976616464, 0, 0], [(-66707932959081), 0], [(-51453207940704)]], [[(-952282884553), 0, 0, 0], [402851502340, 0, 0], [874770448786, 0], [1012862127726]], [[8137132524, 0, 0, 0, 0], [(-3268513861), 0, 0, 0], [(-5323187629), 0, 0], [(-17249416546), 0], [(-23181982261)]]], r1 := 827313996056, V2 := [[[18443906189382344524]], [[(-18316622839107), 31522506073], [(-91401694075768)]], [[15701663244, (-156828814), (-335189)], [(-595092231601), 2042355675], [2777107781]], [[(-154248765), (-2530235), 5507, 3], [556733502, (-10090161), (-32598)], [(-82227125), 33249078], [(-23337920)]], [[1987687, 3637, 8, 0, 0], [(-5452204), (-165273), 534, 0], [970157, (-161715), (-1060)], [689115, 4031], [339452]]], r2 := 2030489687, V3 := [[[18445346563590742867]], [[(-34085264767988), 30840558587], [(-45081975164595)]], [[8625597, 404308073, (-653148)], [(-1099537866465), 1998489285], [(-32543009)]], [[1722, (-8625879), (-1142), 13], [558770, 26238801, (-63509)], [(-428737), 32545072], [(-4028)]], [[(-14), (-1720), 281, 0, 0], [122, (-558798), (-112), 1], [9093, 428740, (-2064)], [(-74), 4050], [25]]], r3 := 6527169001, Vm := [[[18443906228103109326]], [[(-18316949500118), 0], [(-91399160825403)]], [[15700351706, 0, 0], [(-595113870657), 0], [2819225907]], [[(-154252410), 0, 0, 0], [556650278, 0, 0], [(-82596251), 0], [(-23321224)]], [[1987782, 0, 0, 0, 0], [(-5452438), 0, 0, 0], [968861, 0, 0], [688851, 0], [339352]]], rm := 210720873 }
noncomputable def w3 : Wit := { Z0 := { p := [[[1116313828509610368]], [[(-19348438847853733), 159473404072801481], [3489928913512774]], [[120766538156964, (-2764062692550534), 0], [(-60213589560169), 498561273358967], [(-45375840950266)]], [[(-903835488814), 17252362593852, 0, 0], [395587214147, (-8601941365739), 0], [783750482612, (-6482262992896)], [892633761639]], [[7995362013, (-129119355545), 0, 0, 0], [(-3520838307), 56512459163, 0, 0], [(-5086706919), 111964354658, 0], [(-15423411518), 127519108805], [(-20422504043)]]], r := 694844983364, ok := true }, Z1 := { p := [[[1275787232582411849]], [[(-22112501540404266), 0], [3988490186871742]], [[138018900750816, 0, 0], [(-68815530925908), 0], [(-51858103943162)]], [[(-1032954844358), 0, 0, 0], [452099673311, 0, 0], [895714837270, 0], [1020152870444]], [[9137556587, 0, 0, 0, 0], [(-4023815208), 0, 0, 0], [(-5813379336), 0, 0], [(-17626756020), 0], [(-23340004621)]]], r := 208854645964, ok := true }, Z2 := { p := [[[15869930290349439824817]], [[(-92664402648346069127), 159473404072801481], [(-462404202836726034931)]], [[651976095224550521, (-2764062692550534), 0], [2703475598224664799, 498561273358967], [14270918858725591493]], [[(-5356669636436785), 17252362593852, 0, 0], [(-18692904596404895), (-8601941365739), 0], [(-83480753565181745), (-6482262992896)], [(-447658750875663669)]], [[52104497281694, (-129119355545), 0, 0, 0], [149642079212847, 56512459163, 0, 0], [573517726365323, 111964354658, 0], [2619511394877865, 127519108805], [14150202957011917]]], r := 1550446014013374, ok := true }, Z3 := { p := [[[30187233386397791580600]], [[(-670471685875119801309), 606646932332957591], [(-886781666415972440647)]], [[15693463458432670879, (-20445866625557477), 0], [19884262578512396751, 1750241410921513], [27452158984951981754]], [[(-372898869387194344), 470217360577044, 0, 0], [(-467099935162197203), (-55169691787751), 0], [(-617776501813847282), (-23179531471886)], [(-862721725176561251)]], [[8923769343529941, (-11118103676925), 0, 0, 0], [11122986763037284, 1189691531577, 0, 0], [14532681926509104, 741677171046, 0], [19456513124886407, 458759228300], [27305496276140992]]], r := 22341909048577679, ok := true }, iE := { p := [[[15872568017113356621731]], [[(-92666970988830595677), 0], [(-462395956518652890624)]], [[652009536264092737, 0, 0], [2703468219527668932, 0], [14270811640605513607]], [[(-5357032799367011), 0, 0, 0], [(-18692746790172931), 0, 0], [(-83480655602591791), 0], [(-447656641680289287)]], [[52108826242293, 0, 0, 0, 0], [149640120703486, 0, 0, 0], [573515841669514, 0, 0], [2619509454836451, 0], [14150154700881676]]], r := 1550058733799392, ok := true }, iHu := { p := [[[30190127161994552240374]], [[(-670487142547838364409), 0], [(-886773317563265171360)]], [[15693883716657291662, 0, 0], [19884236200587015183, 0], [27452048415922546899]], [[(-372909239884634154), 0, 0, 0], [(-467099002332108597), 0, 0], [(-617776099856649048), 0], [(-862719536842311311)]], [[8924021815659432, 0, 0, 0, 0], [11122963191556606, 0, 0, 0], [14532668880087321, 0, 0], [19456504817879886, 0], [27305446029092963]]], r := 22338733302516336, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[21438393998630567]], [[125161286603169, 0], [624538303350320]], [[(-149926591094), 0, 0], [3640880843014, 0], [(-1081066179892)]], [[1218869202, 0, 0, 0], [(-4836524849), 0, 0], [(-6396694156), 0], [11623219411]], [[(-14864258), 0, 0, 0, 0], [39318362, 0, 0, 0], [(-5910), 0, 0], [68776447, 0], [(-187471281)]]], r := 113075111, ok := true }, de := { p := [[[(-135474705818015617881)]], [[324561393927892274, 0], [429258617775599459]], [[(-3957915847338100), 0, 0], [396595037679, 0], [(-6923263828694430)]], [[64356355333619, 0, 0, 0], [366417, 0, 0], [484616, 0], [148887394379120]], [[(-1177250402444), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-3602114380139)]]], r := 598006961702, ok := true }, dde := { p := [[[(-351305587818666909406413)]], [[8568104397498623747347, 0], [11332009041853018490605]], [[(-208978156336427660435), 0, 0], [(-276390465228659586361), 0], [(-365548679294000977027)]], [[5097028203327254562, 0, 0, 0], [6741230849561105250, 0, 0], [8915821446193711087, 0], [11791892880451030113]], [[(-124317761056740285), 0, 0, 0, 0], [(-164420264623452591), 0, 0, 0], [(-217459059663267177), 0, 0], [(-287607143425626687), 0], [(-380383641304859037)]]], r := 42356359277324457, ok := true }, nJu := { p := [[[(-270949411636031235761)]], [[649122787855784549, 0], [858517235551198918]], [[(-7915831694676200), 0, 0], [793190075359, 0], [(-13846527657388859)]], [[128712710667238, 0, 0, 0], [732835, 0, 0], [969233, 0], [297774788758240]], [[(-2354500804887), 0, 0, 0, 0], [2, 0, 0, 0], [11822, 0, 0], [2, 0], [(-7204228760278)]]], r := 1196013923397, ok := true }, Jd1 := { p := [[[(-702611175637333818812826)]], [[17136208794997247494695, 0], [22664018083706036981210]], [[(-417956312672855320869), 0, 0], [(-552780930457319172721), 0], [(-731097358588001954054)]], [[10194056406654509124, 0, 0, 0], [13482461699122210501, 0, 0], [17831642892387422175, 0], [23583785760902060226]], [[(-248635522113480570), 0, 0, 0, 0], [(-328840529246905181), 0, 0, 0], [(-434918119326534354), 0, 0], [(-575214286851253374), 0], [(-760767282609718073)]]], r := 84712718554648907, ok := true }, term0 := { p := [[[9276275718396271755161671914]], [[(-452475546997013905256570134), 0], [(-598400022887570653833689372)]], [[16553669959488662951557271, 0, 0], [29189415847517241191363618, 0], [28953720881552068113697653]], [[(-538325633361673318047368), 0, 0, 0], [(-1067895345989621744841235), 0, 0], [(-1412349880904055971444686), 0], [(-1245297265107800063975934)]], [[16412273632460793892415, 0, 0, 0, 0], [34728139514356923044020, 0, 0, 0], [51671010917654941951944, 0, 0], [60745345232608349996117, 0], [50213017226983226988176]]], r := 10280752399817166855581, ok := true }, r0 := { p := [[[161810964969671942041713]], [[(-3195986609285347504809), 45846018411725837565568], [(-4715220009247024358639)]], [[50438608590079452869, (-892462016899756666604), 3165544124977859109914], [92277556191721419551, (-1338339816430148064140)], [145527622479714296038]], [[(-798692494424181662), 13850068418902205205, (-57929530925477048510), (-15305904469046657342)], [(-1424032343774854124), 25890193373413174777, (-93079801105269608292)], [(-2837901214298015808), 41328961687531202688], [(-4565001282359769081)]], [[13813871164202030, (-217001088844446858), 832888938826456464, 805732855932147666, (-495611526338604425)], [21936457268774204, (-394059333837099587), 1715149189336323035, 354524444135861731], [43417249095452504, (-797426727736129175), 2880984030912457110], [88828786921071591, (-1296852296788184340)], [144295859224955977]]], r := 972906933134293231, ok := true }, r1 := { p := [[[210806730295927020034973]], [[(-4145548455219578974710), 0], [(-6146273379873528783866)]], [[65099754697112614638, 0, 0], [119863576165693944405, 0], [189727206348380591971]], [[(-1027688874676921192), 0, 0, 0], [(-1842135427125422407), 0, 0], [(-3687949940822304311), 0], [(-5952066531282441106)]], [[17770782970797232, 0, 0, 0, 0], [28301478775989286, 0, 0, 0], [56205841289124544, 0, 0], [115466191780045986, 0], [188152526392401053]]], r := 146851843564363561, ok := true }, r2 := { p := [[[1643993705648092678134079245]], [[(-33615121332012347481873717), 62334816921598564562587], [(-104209335214568554450008568)]], [[647583412803734673794332, (-898955891165147395599), 450059561613056068], [2099080923906976633590497, (-1983609388409198345078)], [4988771234189473853372292]], [[(-13392399955310226889650), 14140359266315285659, 22613764748699, (-104734111521156)], [(-39953057389009583429386), 27719973652142913105, 68114571189104], [(-99554315786353381151315), 63634019389150449342], [(-212954154024903961676380)]], [[295612470792773954956, (-256860786004870762), (-58884692583510), 2522088750203, (-11792884956736)], [820436995754954210924, (-422842991009079625), (-84637971304970), (-92234747208813)], [1880480255514595719835, (-877723827687056705), (-14642698748529)], [4221166619123905777304, (-2045840858832324576)], [8537176148583579309014]]], r := 17985870469135585402950, ok := true }, r3 := { p := [[[18548937609664314196302714305]], [[(-904796156159917913667212219), 717752870987712423636672], [(-1196683435795512043980653633)]], [[33101931736668864368696803, (-30804819535673345970513), 1729997309350314776], [58373832458053069441827638, (-23190006920308900624103)], [57903679710966278802287094]], [[(-1076479625855740359343550), 1075702714958929457117, (-771854952624088), (-5111172661782440)], [(-2135616195448750882514786), 994939035033988238985, (-316878130036070)], [(-2824538481898939795571093), 748501381344479253046], [(-2490473167444508038455369)]], [[32819386876364518916273, (-34150643841317201135), (-956576527616311), (-5056497553480737), (-552599388483116)], [69450741099010929632765, (-34740183456385688246), (-2244709409075506), (-4861180429998604)], [103336387396040641318554, (-32110212934947239730), (-2476178135980499)], [121485487100530174473810, (-24158592736478650985)], [100422116045683129075992]]], r := 1065301960795923930026851, ok := true }, eta := { p := [[[(-1644648717140455908843439136)]], [[33633998678293332251150121, 0], [104230219247211851675544804]], [[(-648058410131061427408316), 0, 0], [(-2099681934693645718453862), 0], [(-4989441816992691365292944)]], [[13404042818654655512651, 0, 0, 0], [39968165795694160514935, 0, 0], [99573602702982453396911, 0], [212975725317548183518596]], [[(-295896478374533367148), 0, 0, 0, 0], [(-820807259226912791687), 0, 0, 0], [(-1880964973719727198972), 0, 0], [(-4221786881397109266017), 0], [(-8537870646865310417239)]]], r := 1677192322626997061836, ok := true } }
theorem sB_3 : stageB c3 w3 = true := by decide +kernel
theorem s0_3 : stageC0 w3 q3 = true := by decide +kernel
theorem s1_3 : stageC1 w3 q3 = true := by decide +kernel
theorem s2_3 : stageC2 w3 q3 = true := by decide +kernel
theorem s3_3 : stageC3 w3 q3 = true := by decide +kernel
theorem sE_3 : stageE w3 q3 = true := by decide +kernel
theorem sF_3 : stageF w3 = true := by decide +kernel
theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

noncomputable def c4 : Cell := { bc := 2181431069507584, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 6196953087261802496, sh := 144115188075855872 }
noncomputable def q4 : Cert := { V0 := [[[1075448149977392115]], [[(-18737451908832587), 152883077439643754], [3346318676521087]], [[112273337228286, (-2637487802512406), (-160292215447525)], [(-57381767144331), 471028544093735], [(-43583513535539)]], [[(-793787730992), 15120558107949, 8338557796049, (-7412796519722)], [345027867131, (-7833094408230), (-1489181764093)], [751104928386, (-6156610619368)], [857771352883]], [[6605625474, (-99615939151), (-193519947337), 377967610690, 23247547380], [(-2776161385), 40813990014, 76811361762, (-67501177906)], [(-4534322849), 103671465616, 14816952769], [(-14803729568), 121285174662], [(-19630042905)]]], r0 := 2784238126076, V1 := [[[1228163546265178926]], [[(-21366225242593044), 0], [3815790904970494]], [[127192018636479, 0, 0], [(-65134718656760), 0], [(-49724627522562)]], [[(-890421950931), 0, 0, 0], [384005631346, 0, 0], [853972915998, 0], [978777265844]], [[7347607432, 0, 0, 0, 0], [(-3018447710), 0, 0, 0], [(-5078730768), 0, 0], [(-16838640146), 0], [(-22401105113)]]], r1 := 793453093239, V2 := [[[18443869617740211848]], [[(-18255605851546), 31198755949], [(-92589694130154)]], [[14821610525, (-166907403), (-324146)], [(-592928554936), 2021516194], [2616462944]], [[(-139461854), (-2509371), 5534, 3], [525627635, (-10748376), (-31526)], [(-78452424), 32914729], [(-21991884)]], [[1717696, 3325, 5, 0, 0], [(-4929154), (-163856), 537, 0], [918077, (-172617), (-1025)], [657219, 4056], [319831]]], r2 := 2028579526, V3 := [[[18445278393095722839]], [[(-34085230245367), 31614657676], [(-47281048661480)]], [[8635608, 369784350, (-654321)], [(-1099535629947), 2048730735], [(-33364092)]], [[1617, (-8635878), (-39), 13], [559481, 24002176, (-63626)], [(-392338), 33366160], [(-4171)]], [[(-13), (-1615), 269, 0, 0], [115, (-559508), (-5), 1], [9107, 392338, (-2068)], [(-69), 4193], [26]]], r3 := 6174198384, Vm := [[[18443869655802380772]], [[(-18255937799560), 0], [(-92587204492571)]], [[14820279251, 0, 0], [(-592950529506), 0], [2657837605]], [[(-139464809), 0, 0, 0], [525543147, 0, 0], [(-78826776), 0], [(-21975713)]], [[1717774, 0, 0, 0, 0], [(-4929343), 0, 0, 0], [916761, 0, 0], [656957, 0], [319734]]], rm := 210635719 }
noncomputable def w4 : Wit := { Z0 := { p := [[[1078092911567246410]], [[(-18875969440221924), 154013273081035201], [3371056501310127]], [[115528891047814, (-2696567062888847), 0], [(-58672328190570), 481579500187161], [(-43828344930504)]], [[(-843094669393), 16504127292544, 0, 0], [375325504378, (-8381761170082), 0], [763913060655, (-6261192132930)], [862179157256]], [[7209137751, (-120442095628), 0, 0, 0], [(-3238712671), 53617929196, 0, 0], [(-4835382095), 109130437236, 0], [(-15034437368), 123168451036], [(-19725569711)]]], r := 670520185448, ok := true }, Z1 := { p := [[[1232106184648281611]], [[(-21572536503110770), 0], [3852636001497288]], [[132033018340359, 0, 0], [(-67054089360652), 0], [(-50089537063433)]], [[(-963536765020), 0, 0, 0], [428943433575, 0, 0], [873043497892, 0], [985347608292]], [[8239014573, 0, 0, 0, 0], [(-3701385910), 0, 0, 0], [(-5526150966), 0, 0], [(-17182214135), 0], [(-22543508241)]]], r := 200175083289, ok := true }, Z2 := { p := [[[15687167350930102535572]], [[(-90119157758011314755), 154013273081035201], [(-457070848260827221515)]], [[621040153626184337, (-2696567062888847), 0], [2630455650265345807, 481579500187161], [14106215720959148422]], [[(-4962747787951326), 16504127292544, 0, 0], [(-17827777298667074), (-8381761170082), 0], [(-81239909579392774), (-6261192132930)], [(-442490325361321556)]], [[46523726760833, (-120442095628), 0, 0, 0], [138931080119050, 53617929196, 0, 0], [547226134867357, 109130437236, 0], [2549458743751536, 123168451036], [13986789755625132]]], r := 1508289428792002, ok := true }, Z3 := { p := [[[28906216911368926742032]], [[(-611903273567509079728), 567551176432911330], [(-848796626732379078058)]], [[13654247211670227132, (-18690401726589346), 0], [18141292816012197189, 1644452475418897], [26272092604340252099]], [[(-309324241907638380), 409404424843304, 0, 0], [(-406281821500061902), (-50718755665134), 0], [(-563551442027393098), (-21758177516658)], [(-825557682266969306)]], [[7057604496366203, (-9226686551666), 0, 0, 0], [9224012701808701, 1040318910239, 0, 0], [12638948491382419, 681040317330, 0], [17747315830289102, 430492829244], [26127475635369029]]], r := 19244255609943139, ok := true }, iE := { p := [[[15689800071939358349075]], [[(-90121596558264896327), 0], [(-457062616084194610397)]], [[621071515123387446, 0, 0], [2630448880078919843, 0], [14106108691404217294]], [[(-4963078517088923), 0, 0, 0], [(-17827630659414055), 0, 0], [(-81239818889681679), 0], [(-442488219905329130)]], [[46527521904538, 0, 0, 0, 0], [138929311890128, 0, 0, 0], [547224380933271, 0, 0], [2549456942757506, 0], [13986741585452378]]], r := 1507915531310920, ok := true }, iHu := { p := [[[28909081375541746965102]], [[(-611917166037307388278), 0], [(-848788327084003140330)]], [[13654610849509913531, 0, 0], [18141269903888944572, 0], [26271982789538432732]], [[(-309332815786662790), 0, 0, 0], [(-406281017342419733), 0, 0], [(-563551088565608406), 0], [(-825555509544337003)]], [[7057803698891565, 0, 0, 0, 0], [9223993221543502, 0, 0, 0], [12638937233353487, 0, 0], [17747308501694813, 0], [26127425756127565]]], r := 19241450117217917, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[21688126385340066]], [[124575747762392, 0], [631801026029447]], [[(-142953525428), 0, 0], [3621991760504, 0], [(-1093859591845)]], [[1108122838, 0, 0, 0], [(-4611587247), 0, 0], [(-6396717796), 0], [11760772304]], [[(-12885148), 0, 0, 0, 0], [35745898, 0, 0, 0], [(-5910), 0, 0], [68776447, 0], [(-189689876)]]], r := 112737441, ok := true }, de := { p := [[[(-134840917972331673674)]], [[309466086976310584, 0], [429259410967140488]], [[(-3598299912612869), 0, 0], [396596503351, 0], [(-6923263827701555)]], [[55787595632439, 0, 0, 0], [366419, 0, 0], [508259, 0], [148887394379120]], [[(-973039458705), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-3602114380139)]]], r := 572952346086, ok := true }, dde := { p := [[[(-334966411992022551093128)]], [[7789607079572544905268, 0], [10804938852310304228685]], [[(-181153653299244749717), 0, 0], [(-251277648521371108012), 0], [(-348546415140794543658)]], [[4212875658121718417, 0, 0, 0], [5843666235458419435, 0, 0], [8105730584668149852, 0], [11243432746476566821]], [[(-97973852514454454), 0, 0, 0, 0], [(-135899214778112789), 0, 0, 0], [(-188505362434163231), 0, 0], [(-261475180150606061), 0], [(-362691378918586627)]]], r := 37300081901111928, ok := true }, nJu := { p := [[[(-269681835944663347348)]], [[618932173952621168, 0], [858518821934280976]], [[(-7196599825225737), 0, 0], [793193006703, 0], [(-13846527655403110)]], [[111575191264879, 0, 0, 0], [732839, 0, 0], [1016518, 0], [297774788758241]], [[(-1946078917410), 0, 0, 0, 0], [2, 0, 0, 0], [11822, 0, 0], [2, 0], [(-7204228760278)]]], r := 1145904692167, ok := true }, Jd1 := { p := [[[(-669932823984045102186256)]], [[15579214159145089810537, 0], [21609877704620608457371]], [[(-362307306598489499434), 0, 0], [(-502555297042742216024), 0], [(-697092830281589087315)]], [[8425751316243436835, 0, 0, 0], [11687332470916838870, 0, 0], [16211461169336299705, 0], [22486865492953133642]], [[(-195947705028908907), 0, 0, 0, 0], [(-271798429556225578), 0, 0, 0], [(-377010724868326462), 0, 0], [(-522950360301212121), 0], [(-725382757837173253)]]], r := 74600163802223848, ok := true }, term0 := { p := [[[8433480752678922465991137624]], [[(-392231546813253693688742071), 0], [(-544030949782700759711644241)]], [[13682224088590041850233995, 0, 0], [25303011273233720584909192, 0], [26323036628915161310365135]], [[(-424250797623258476056761), 0, 0, 0], [(-882654418450563960884097), 0, 0], [(-1224302967874069125066978), 0], [(-1132151218740865772029967)]], [[12332798543542349468924, 0, 0, 0, 0], [27368993355065947673734, 0, 0, 0], [42707960307330121487140, 0, 0], [52657411794964394410316, 0], [45650716891798045063208]]], r := 8557337521324894462250, ok := true }, r0 := { p := [[[155614569531356188243777]], [[(-3003394619459835839896), 44114816420069823468330], [(-4536191240974606727641)]], [[45958047280177905163, (-839551267661959425925), 3052920605829260521850], [86833354449384136449, (-1288089107797377132018)], [140020366828418414262]], [[(-697955671035446910), 12632617479637216083, (-54740409284977762783), (-13776294431530464694)], [(-1300769345775259245), 24383041639929452574, (-89744932062691944379)], [(-2671833387433692191), 39780875965339315792], [(-4392592562175114732)]], [[11465238566140757, (-189668972742871612), 763227387147505343, 725409257489430966, (-449146524047724294)], [19233658988532678, (-360256159844045938), 1621066370776017349, 318960246946169537], [39697356680790907, (-751340799616784198), 2777596041361615888], [83656630136071235, (-1248347157163869568)], [138853933508452024]]], r := 892229928279667597, ok := true }, r1 := { p := [[[202768084742644320283743]], [[(-3896939036962565055024), 0], [(-5913695717483972977263)]], [[59334429994344385446, 0, 0], [112820065021108385121, 0], [182569515647202860368]], [[(-898115376667309287), 0, 0, 0], [(-1683103374507106120), 0, 0], [(-3472941801649273453), 0], [(-5727932442612552735)]], [[14745102957926142, 0, 0, 0, 0], [24815687757247277, 0, 0, 0], [51402383645866864, 0, 0], [108766984084865028, 0], [181076692171643708]]], r := 134974897592135529, ok := true }, r2 := { p := [[[1579251179584704589069881113]], [[(-31176551352397142288212120), 60591493123216973321296], [(-100164698251339716534839156)]], [[573816119213281244321118, (-845316519805552760394), 450274427294634510], [1948567683606898522778028, (-1929802742710583340805)], [4796889897035248316525347]], [[(-11275685584971940962941), 12716855841126097137, 76118562371555, (-99581566534812)], [(-35432702104819344792638), 26114362397272018661, 13921696750414], [(-92468160840024533778915), 61929590531159342254], [(-204816606749619086608935)]], [[236283525621501002952, (-219146399305904018), (-59730603063550), 2357270788875, (-11021647318031)], [691165483110496527425, (-381114945473118170), (-70484872588249), (-87542953757976)], [1668636217431875567032, (-827606398759030344), (-56248820500353)], [3922313029629095531034, (-1991460857270292898)], [8212596593006521052700]]], r := 16758636730507153450339, ok := true }, r3 := { p := [[[16863637216383431053044532621]], [[(-784327882558664626753480850), 660188380053115791822693], [(-1087954631861704275463002455)]], [[27359957142331174759301929, (-26881188895243306208690), 1735542002621254758], [50601659798928803089488628, (-21330752453500615579040)], [52642612595626370352607444]], [[(-848365836885255819109402), 893237219960231821934, 1271324081009901, (-4275297914276718)], [(-1765163934169267548063057), 868231073789749652492, (-784093679108195)], [(-2448465190307332858716670), 688495701079390644835], [(-2264190797858117389923689)]], [[24661710498125451363436, (-27010156599168146883), (-679286535057553), (-4253786629993308), (-467496811846331)], [54733603017509541507734, (-28848889067742534529), (-2610301707902165), (-4074384012516936)], [85411243195531454051338, (-28021585820423954923), (-1464753212157855)], [105310282136960135530369, (-22220198058245059119)], [91297828545299366499507]]], r := 870010982624772180839656, ok := true }, eta := { p := [[[(-1579870247561940455502188401)]], [[31193659861802305325900080, 0], [100184437872632521589336493]], [[(-574227557467613105022143), 0, 0], [(-1949112430633578882685115), 0], [(-4797523754093678958349870)]], [[11285309039925093548279, 0, 0, 0], [35445789528317294767900, 0, 0], [92485642762525172628011, 0], [204836997118295319967748]], [[(-236507357612428421607), 0, 0, 0, 0], [(-691471477501684812892), 0, 0, 0], [(-1669056107275230306369), 0, 0], [(-3922875225778068963816), 0], [(-8213253067220216743513)]]], r := 1581457549478135241229, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

theorem region : RegionPosI 1970324836974592 2251799813685248 13835058055282163712 18446744073709551616 5764607523034234880 6341068275337658368 :=
  (RegionPosI.split_b 2111062325329920 (RegionPosI.split_s 6052837899185946624 (RegionPosI.split_b 2040693581152256 (RegionPosI.of_check c0 q0 ok_0 1970324836974592 2040693581152256 13835058055282163712 18446744073709551616 5764607523034234880 6052837899185946624 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2040693581152256 2111062325329920 13835058055282163712 18446744073709551616 5764607523034234880 6052837899185946624 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 1970324836974592 2111062325329920 13835058055282163712 18446744073709551616 6052837899185946624 6341068275337658368 (by decide +kernel))) (RegionPosI.split_s 6052837899185946624 (RegionPosI.of_check c3 q3 ok_3 2111062325329920 2251799813685248 13835058055282163712 18446744073709551616 5764607523034234880 6052837899185946624 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 2111062325329920 2251799813685248 13835058055282163712 18446744073709551616 6052837899185946624 6341068275337658368 (by decide +kernel))))

end CKLaneC.RSC2.S01_0164

end