[ Eq(x4, k35 - x5),
  Eq(x10, k36 - x12),
  Eq(x13, k37 - x15) ]