669.29/673.31	unsat
