s SATISFIABLE
v -1 0