8.47/8.55	unsat
