{ x24 = x1 + x2 + x4,
  x25 = x3 + x4,
  x26 = x5 + x8,
  x27 = x6 + x7 + x8,
  x28 = x10 + x12,
  x29 = x11 + x13,
  x30 = x9 + x12 + x13 + x15 + x19,
  1*k57*x1 + 1*k57*x2 + 1*k57*x4 = k57*k58,
  1*k57*x6 + 1*k57*x7 + 1*k57*x8 = k57*k59 }