17.27/17.31	unsat
