577.71/583.53	unsat
