854.94/859.72	unsat
