32.39/32.43	unsat
