{ 1*x2 + 1*x3 + 1*x4 + 1*x5 + 1*x9 + 1*x10 + 1*x11 = k142 + k141 + k140,
  1*x6 + 1*x7 + 1*x8 = k143,
  1*x12 + 1*x13 = k144,
  1*x14 + 1*x25 = k145,
  1*x16 + 1*x26 + 1*x27 + 1*x28 = k146,
  1*x17 + 1*x19 + 1*x26 + 1*x27 + 1*x28 = k147,
  1*x20 + 1*x22 = k148,
  1*x21 + 1*x23 = k149,
  1*x29 + 1*x67 + 1*x69 + 1*x75 = k150 + k151,
  1*x31 + 1*x32 = k152,
  1*x33 + 1*x68 = k153,
  1*x34 + 1*x57 + 1*x61 = k154,
  1*x35 + 1*x60 + 1*x65 = k155,
  1*x36 + 1*x37 + 1*x38 + 1*x40 + 1*x42 + 1*x44 + 1*x45 + 1*x46 + 1*x47 = k156,
  1*x39 + 1*x66 = k157,
  1*x43 + 1*x44 + 1*x45 + 1*x46 + 1*x47 + 1*x50 + 1*x51 = k158,
  1*x48 + 1*x49 = k159,
  1*x52 + 1*x59 + 1*x70 + 1*x72 + 1*x73 + 1*x74 = k160,
  1*x53 + 1*x55 = k161,
  1*x54 + 1*x56 + 1*x70 + 1*x72 + 1*x73 = k162,
  1*x58 + 1*x62 = k163,
  1*x63 + 1*x64 = k164,
  1*x71 + 1*x73 + 1*x74 = k165 }