807.44/809.65	unsat
