s SATISFIABLE
v -1 -2 -3 0