gets"f "
m=gets.to_i
a=$<.map &:split
w=(0...1<<m).find{|b|a.all?{|l|l.any?{|v|(-v=v.to_i)[m]^b[m-v.abs]>0}}}
puts"s #{w ?'': :UN}SATISFIABLE"
puts"v "+(1..m).map{|i|i.*1-2*w[m-i]}*' 'if w
Note that non-ascii characters in the above source code will be escaped (such as \x9f).