23.56/23.64	unsat
