23.47/24.55	unsat
