s SATISFIABLE
v -1 -2 0