12.45/12.57	unsat
