We investigate the space complexity of refuting 3 -CNFs in Resolution and algebraic systems. No lower bound for refuting any family of 3 -CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3 -CNF in n variables requires, with high probability, ( n log n ) distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation requires, with high probability, ( n log n ) clauses each of width ( n log n ) to be kept at the same time in memory. This gives a ( n 2 log 2 n ) lower bound for the total space needed in Resolution to refute . The main technical innovation is a variant of Hall's theorem. We show that in bipartite graphs G with bipartition ( L R ) and left-degree at most 3, L can be covered by certain families of disjoint paths, called (2 4 ) -matchings, provided that L expands in R by a factor of (2 − ) , for 1 23 .