s SATISFIABLE
v -1 2 3 0