a=gettime%3;print(if(1>a,"s SATISFIABLE\nv 1 2 3 -4 5 6 7 8 9 10 -11 12 13 -14 -15 16",if(2>a,"s UNSATISFIABLE","s SATISFIABLE\nv 1 2 -3"))) \q