We study the complexity of proving unsatisfiability for ran- dom,k-CNF formulas with clause density Δ,m n where m is number,of clauses and n is the number,of variables. We prove the first nontrivial general upper bound, giving algorithms that, in particular, for k 3 produce refutations almost certainly in time 2lower bound.