s SATISFIABLE
v 0