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