32.87/32.93	unsat
