/-
  第1112コマ — 頭の塊のチャンク 2（228 個・葉 4788）。`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 piecesK2 : List (ℕ × ℕ × ℕ) :=
  [(14, 12, 1), (16, 12, 1),
   (17, 12, 1), (18, 12, 1),
   (21, 12, 1), (24, 12, 1),
   (30, 12, 1), (37, 12, 1),
   (39, 12, 1), (41, 12, 1),
   (42, 12, 1), (45, 12, 1),
   (47, 12, 1), (1, 13, 1),
   (2, 13, 1), (4, 13, 1),
   (5, 13, 1), (9, 13, 1),
   (10, 13, 1), (11, 13, 1),
   (14, 13, 1), (16, 13, 1),
   (17, 13, 1), (18, 13, 1),
   (21, 13, 1), (24, 13, 1),
   (30, 13, 1), (37, 13, 1),
   (39, 13, 1), (41, 13, 1),
   (42, 13, 1), (45, 13, 1),
   (47, 13, 1), (1, 14, 1),
   (2, 14, 1), (4, 14, 1),
   (5, 14, 1), (9, 14, 1),
   (10, 14, 1), (11, 14, 1),
   (14, 14, 1), (16, 14, 1),
   (17, 14, 1), (18, 14, 1),
   (21, 14, 1), (24, 14, 1),
   (30, 14, 1), (37, 14, 1),
   (39, 14, 1), (41, 14, 1),
   (42, 14, 1), (45, 14, 1),
   (47, 14, 1), (1, 15, 1),
   (2, 15, 1), (4, 15, 1),
   (5, 15, 1), (9, 15, 1),
   (10, 15, 1), (11, 15, 1),
   (14, 15, 1), (16, 15, 1),
   (17, 15, 1), (18, 15, 1),
   (21, 15, 1), (24, 15, 1),
   (30, 15, 1), (37, 15, 1),
   (39, 15, 1), (41, 15, 1),
   (42, 15, 1), (45, 15, 1),
   (47, 15, 1), (1, 16, 1),
   (2, 16, 1), (4, 16, 1),
   (5, 16, 1), (9, 16, 1),
   (10, 16, 1), (11, 16, 1),
   (14, 16, 1), (16, 16, 1),
   (17, 16, 1), (18, 16, 1),
   (21, 16, 1), (24, 16, 1),
   (30, 16, 1), (37, 16, 1),
   (39, 16, 1), (41, 16, 1),
   (42, 16, 1), (45, 16, 1),
   (47, 16, 1), (1, 17, 1),
   (2, 17, 1), (4, 17, 1),
   (275, 16, 1), (276, 16, 1),
   (277, 16, 1), (279, 16, 1),
   (280, 16, 1), (284, 16, 1),
   (285, 16, 1), (286, 16, 1),
   (289, 16, 1), (291, 16, 1),
   (292, 16, 1), (293, 16, 1),
   (296, 16, 1), (299, 16, 1),
   (305, 16, 1), (312, 16, 1),
   (314, 16, 1), (316, 16, 1),
   (317, 16, 1), (320, 16, 1),
   (17710, 15, 1), (17711, 15, 1),
   (17712, 15, 1), (17714, 15, 1),
   (17715, 15, 1), (17719, 15, 1),
   (17720, 15, 1), (17721, 15, 1),
   (17724, 15, 1), (17726, 15, 1),
   (17727, 15, 1), (17728, 15, 1),
   (17731, 15, 1), (17734, 15, 1),
   (17740, 15, 1), (17747, 15, 1),
   (17749, 15, 1), (17751, 15, 1),
   (17752, 15, 1), (17755, 15, 1),
   (976635, 14, 1), (976636, 14, 1),
   (976637, 14, 1), (976639, 14, 1),
   (976640, 14, 1), (976644, 14, 1),
   (976645, 14, 1), (976646, 14, 1),
   (976649, 14, 1), (976651, 14, 1),
   (976652, 14, 1), (976653, 14, 1),
   (976656, 14, 1), (976659, 14, 1),
   (976665, 14, 1), (976672, 14, 1),
   (976674, 14, 1), (976676, 14, 1),
   (976677, 14, 1), (976680, 14, 1),
   (53717510, 13, 1), (53717511, 13, 1),
   (53717512, 13, 1), (53717514, 13, 1),
   (53717515, 13, 1), (53717519, 13, 1),
   (53717520, 13, 1), (53717521, 13, 1),
   (53717524, 13, 1), (53717526, 13, 1),
   (53717527, 13, 1), (53717528, 13, 1),
   (53717531, 13, 1), (53717534, 13, 1),
   (53717540, 13, 1), (53717547, 13, 1),
   (53717549, 13, 1), (53717551, 13, 1),
   (53717552, 13, 1), (53717555, 13, 1),
   (2954465635, 12, 1), (2954465636, 12, 1),
   (2954465637, 12, 1), (2954465639, 12, 1),
   (2954465640, 12, 1), (2954465644, 12, 1),
   (2954465645, 12, 1), (2954465646, 12, 1),
   (2954465649, 12, 1), (2954465651, 12, 1),
   (2954465652, 12, 1), (2954465653, 12, 1),
   (2954465656, 12, 1), (2954465659, 12, 1),
   (2954465665, 12, 1), (2954465672, 12, 1),
   (2954465674, 12, 1), (2954465676, 12, 1),
   (2954465677, 12, 1), (2954465680, 12, 1),
   (162495612510, 11, 1), (162495612511, 11, 1),
   (162495612512, 11, 1), (162495612514, 11, 1),
   (162495612515, 11, 1), (162495612519, 11, 1),
   (162495612520, 11, 1), (162495612521, 11, 1),
   (162495612524, 11, 1), (162495612526, 11, 1),
   (162495612527, 11, 1), (162495612528, 11, 1),
   (162495612531, 11, 1), (162495612534, 11, 1),
   (162495612540, 11, 1), (162495612547, 11, 1),
   (162495612549, 11, 1), (162495612551, 11, 1),
   (162495612552, 11, 1), (162495612555, 11, 1),
   (8937258690635, 10, 1), (8937258690636, 10, 1),
   (8937258690637, 10, 1), (8937258690639, 10, 1),
   (8937258690640, 10, 1), (8937258690644, 10, 1),
   (8937258690645, 10, 1), (8937258690646, 10, 1),
   (8937258690649, 10, 1), (8937258690651, 10, 1),
   (8937258690652, 10, 1), (8937258690653, 10, 1)]

theorem piecesK2_num : 188640763786768318528122963427870818792110538961466715909532462162478284610176658102845829232521 ≤ totK 55 (10 ^ 100) 21 433 13899 518857 S55 piecesK2 := by
  decide +kernel

end Shiori1112