32.30/33.44	unsat
