30.27/30.93	unsat
