5!d
s/^/s UNSATISFIABLE\n/
/2/s/UN//
P
N
/4/cv 1 2 3 -4 5 6 7 8 9 10 -11 12 13 -14 -15 16
/5/d
cv 1 2 -3