23.26/27.49	unsat
