32.29/32.36	unsat
