23.38/23.44	unsat
