23.15/24.73	unsat
