23.15/25.50	unsat
