/-
  第1112コマ — 頭の塊のチャンク 3（209 個・葉 3969）。`totK`（4 項の葉・深さ 1）の kernel 評価。
  `erdos1112.py` が生成。sorry 0・native_decide 不使用。
-/
import Shioriproofs.Erdos1112k

namespace Shiori1112

set_option maxRecDepth 100000

/-- 塊 `(P, m, j)`：集合 `1 + P·55^m + KF 55 S55 m`、深さ `j`。 -/
def piecesK3 : List (ℕ × ℕ × ℕ) :=
  [(8937258690656, 10, 1), (8937258690659, 10, 1),
   (8937258690665, 10, 1), (8937258690672, 10, 1),
   (8937258690674, 10, 1), (8937258690676, 10, 1),
   (8937258690677, 10, 1), (8937258690680, 10, 1),
   (491549227987510, 9, 1), (491549227987511, 9, 1),
   (491549227987512, 9, 1), (491549227987514, 9, 1),
   (491549227987515, 9, 1), (491549227987519, 9, 1),
   (491549227987520, 9, 1), (491549227987521, 9, 1),
   (491549227987524, 9, 1), (491549227987526, 9, 1),
   (491549227987527, 9, 1), (491549227987528, 9, 1),
   (491549227987531, 9, 1), (491549227987534, 9, 1),
   (491549227987540, 9, 1), (491549227987547, 9, 1),
   (491549227987549, 9, 1), (491549227987551, 9, 1),
   (491549227987552, 9, 1), (491549227987555, 9, 1),
   (27035207539315635, 8, 1), (27035207539315636, 8, 1),
   (27035207539315637, 8, 1), (27035207539315639, 8, 1),
   (27035207539315640, 8, 1), (27035207539315644, 8, 1),
   (27035207539315645, 8, 1), (27035207539315646, 8, 1),
   (27035207539315649, 8, 1), (27035207539315651, 8, 1),
   (27035207539315652, 8, 1), (27035207539315653, 8, 1),
   (27035207539315656, 8, 1), (27035207539315659, 8, 1),
   (27035207539315665, 8, 1), (27035207539315672, 8, 1),
   (27035207539315674, 8, 1), (27035207539315676, 8, 1),
   (27035207539315677, 8, 1), (27035207539315680, 8, 1),
   (1486936414662362510, 7, 1), (1486936414662362511, 7, 1),
   (1486936414662362512, 7, 1), (1486936414662362514, 7, 1),
   (1486936414662362515, 7, 1), (1486936414662362519, 7, 1),
   (1486936414662362520, 7, 1), (1486936414662362521, 7, 1),
   (1486936414662362524, 7, 1), (1486936414662362526, 7, 1),
   (1486936414662362527, 7, 1), (1486936414662362528, 7, 1),
   (1486936414662362531, 7, 1), (1486936414662362534, 7, 1),
   (1486936414662362540, 7, 1), (1486936414662362547, 7, 1),
   (1486936414662362549, 7, 1), (1486936414662362551, 7, 1),
   (1486936414662362552, 7, 1), (1486936414662362555, 7, 1),
   (81781502806429940635, 6, 1), (81781502806429940636, 6, 1),
   (81781502806429940637, 6, 1), (81781502806429940639, 6, 1),
   (81781502806429940640, 6, 1), (81781502806429940644, 6, 1),
   (81781502806429940645, 6, 1), (81781502806429940646, 6, 1),
   (81781502806429940649, 6, 1), (81781502806429940651, 6, 1),
   (81781502806429940652, 6, 1), (81781502806429940653, 6, 1),
   (81781502806429940656, 6, 1), (81781502806429940659, 6, 1),
   (81781502806429940665, 6, 1), (81781502806429940672, 6, 1),
   (81781502806429940674, 6, 1), (81781502806429940676, 6, 1),
   (81781502806429940677, 6, 1), (81781502806429940680, 6, 1),
   (4497982654353646737510, 5, 1), (4497982654353646737511, 5, 1),
   (4497982654353646737512, 5, 1), (4497982654353646737514, 5, 1),
   (4497982654353646737515, 5, 1), (4497982654353646737519, 5, 1),
   (4497982654353646737520, 5, 1), (4497982654353646737521, 5, 1),
   (4497982654353646737524, 5, 1), (4497982654353646737526, 5, 1),
   (4497982654353646737527, 5, 1), (4497982654353646737528, 5, 1),
   (4497982654353646737531, 5, 1), (4497982654353646737534, 5, 1),
   (4497982654353646737540, 5, 1), (4497982654353646737547, 5, 1),
   (4497982654353646737549, 5, 1), (4497982654353646737551, 5, 1),
   (4497982654353646737552, 5, 1), (4497982654353646737555, 5, 1),
   (247389045989450570565635, 4, 1), (247389045989450570565636, 4, 1),
   (247389045989450570565637, 4, 1), (247389045989450570565639, 4, 1),
   (247389045989450570565640, 4, 1), (247389045989450570565644, 4, 1),
   (247389045989450570565645, 4, 1), (247389045989450570565646, 4, 1),
   (247389045989450570565649, 4, 1), (247389045989450570565651, 4, 1),
   (247389045989450570565652, 4, 1), (247389045989450570565653, 4, 1),
   (247389045989450570565656, 4, 1), (247389045989450570565659, 4, 1),
   (247389045989450570565665, 4, 1), (247389045989450570565672, 4, 1),
   (247389045989450570565674, 4, 1), (247389045989450570565676, 4, 1),
   (247389045989450570565677, 4, 1), (247389045989450570565680, 4, 1),
   (13606397529419781381112510, 3, 1), (13606397529419781381112511, 3, 1),
   (13606397529419781381112512, 3, 1), (13606397529419781381112514, 3, 1),
   (13606397529419781381112515, 3, 1), (13606397529419781381112519, 3, 1),
   (13606397529419781381112520, 3, 1), (13606397529419781381112521, 3, 1),
   (13606397529419781381112524, 3, 1), (13606397529419781381112526, 3, 1),
   (13606397529419781381112527, 3, 1), (13606397529419781381112528, 3, 1),
   (13606397529419781381112531, 3, 1), (13606397529419781381112534, 3, 1),
   (13606397529419781381112540, 3, 1), (13606397529419781381112547, 3, 1),
   (13606397529419781381112549, 3, 1), (13606397529419781381112551, 3, 1),
   (13606397529419781381112552, 3, 1), (13606397529419781381112555, 3, 1),
   (748351864118087975961190635, 2, 1), (748351864118087975961190636, 2, 1),
   (748351864118087975961190637, 2, 1), (748351864118087975961190639, 2, 1),
   (748351864118087975961190640, 2, 1), (748351864118087975961190644, 2, 1),
   (748351864118087975961190645, 2, 1), (748351864118087975961190646, 2, 1),
   (748351864118087975961190649, 2, 1), (748351864118087975961190651, 2, 1),
   (748351864118087975961190652, 2, 1), (748351864118087975961190653, 2, 1),
   (748351864118087975961190656, 2, 1), (748351864118087975961190659, 2, 1),
   (748351864118087975961190665, 2, 1), (748351864118087975961190672, 2, 1),
   (748351864118087975961190674, 2, 1), (748351864118087975961190676, 2, 1),
   (748351864118087975961190677, 2, 1), (748351864118087975961190680, 2, 1),
   (41159352526494838677865487510, 1, 1), (41159352526494838677865487511, 1, 1),
   (41159352526494838677865487512, 1, 1), (41159352526494838677865487514, 1, 1),
   (41159352526494838677865487515, 1, 1), (41159352526494838677865487519, 1, 1),
   (41159352526494838677865487520, 1, 1), (41159352526494838677865487521, 1, 1),
   (41159352526494838677865487524, 1, 1), (41159352526494838677865487526, 1, 1),
   (41159352526494838677865487527, 1, 1), (41159352526494838677865487528, 1, 1),
   (41159352526494838677865487531, 1, 1), (41159352526494838677865487534, 1, 1),
   (41159352526494838677865487540, 1, 1), (41159352526494838677865487547, 1, 1),
   (41159352526494838677865487549, 1, 1), (41159352526494838677865487551, 1, 1),
   (41159352526494838677865487552, 1, 1), (41159352526494838677865487555, 1, 1),
   (2263764388957216127282601815635, 0, 0), (2263764388957216127282601815636, 0, 0),
   (2263764388957216127282601815637, 0, 0), (2263764388957216127282601815639, 0, 0),
   (2263764388957216127282601815640, 0, 0), (2263764388957216127282601815644, 0, 0),
   (2263764388957216127282601815645, 0, 0), (2263764388957216127282601815646, 0, 0),
   (2263764388957216127282601815649, 0, 0), (2263764388957216127282601815651, 0, 0),
   (2263764388957216127282601815652, 0, 0), (2263764388957216127282601815653, 0, 0),
   (2263764388957216127282601815656, 0, 0), (2263764388957216127282601815659, 0, 0),
   (2263764388957216127282601815665, 0, 0), (2263764388957216127282601815672, 0, 0),
   (2263764388957216127282601815674, 0, 0), (2263764388957216127282601815676, 0, 0),
   (2263764388957216127282601815677, 0, 0), (2263764388957216127282601815680, 0, 0),
   (2263764388957216127282601815682, 0, 0)]

theorem piecesK3_num : 663138485331281546505579049487196521380342418893724954557263215288056662032639582518 ≤ totK 55 (10 ^ 100) 21 433 13899 518857 S55 piecesK3 := by
  decide +kernel

end Shiori1112