809.85/810.85	unsat
