857.20/859.62	unsat
