30.76/30.80	unsat
