8.27/8.51	unsat
