12.27/12.32	unsat
