9.27/9.50	unsat
