s SATISFIABLE
v -1 2 -3 4 5 0