823.44/824.52	unsat
