12.28/12.57	unsat
