cat(sample(c("s SATISFIABLE v 1 2 -3","s UNSATISFIABLE","s SATISFIABLE v 1 2 3 -4 5 6 7 8 9 10 -11 12 13 -14 -15 16"),1))