30.47/30.56	unsat
