s SATISFIABLE
v -1 2 0