34.45/34.52	unsat
