#!ruby -pa0
$_=[?s,/b/?'UN%s':['%s
v',*?1..$F[-2]]]*' '%:SATISFIABLE
gsub /3$|4|1[145]/,'-\0'