808.91/810.47	unsat
