_='s %sSATISFIABLE';puts eval$<.read.gsub(/.*p.*?(\d+).*?$|\d+/m){$1?%w[?-* +'=-'=~/#{'(-?)'* }-*=(?=]*$1:$&>?0?"\\#$&$|":'$)(?='}+')/x?[_%p%i=0,[*$~].map{|x|x>?-?:v:eval(x+?1)*i-=1}*" "]:_%:UN'