16.27/17.59	unsat
