x=n="";r=[] $<.read.split(/ *0?\n */).map{|l|l<?c?x<<"(#{l.gsub(/ +|\-|\d+/){["1-","a[#$&]",?|][$&<=>?-]}})&":n=l[/\d+/].to_i} f=eval"->a{#{x}1}" (2**n*2).times{|w|f[w]>0&&r<<w} puts"s %sSATISFIABLE%s"%(r!=[]?[""," v "+(r=r.sort_by{|q|q.to_s(2).split(?0).map(&:size).sort.reverse}[-1];(1..n).map{|k|?-*-~-r[k]+k.to_s}*" ")]:[:UN,""])
Note that non-ascii characters in the above source code will be escaped (such as \x9f).