25.40/27.31	unsat
