12.27/12.33	unsat
