9.47/9.53	unsat
