[ Eq(x12, k24 - x6),
  Eq(x16, k27 - x15),
  Eq(x20, k26 - x19),
  Eq(x23, k25 - x24) ]