529.47/529.87	unsat
