8.30/8.43	unsat
