17.45/17.53	unsat
