Satisfiable. Model:
  s0 = root(2, x^2 = 59) = 7.6811457478686081... :: Real