A simple nonconstructive argument shows that most $3$CNF formulas with $cn$ clauses (where $c$ is a sufficiently large constant) are not satisfiable. It is an open question whether there is an efficient refutation algorithm that for most formulas with $cn$ clauses proves that they are not satisfiable. We present a polynomial time algorithm that for most $3$CNF formulas with $cn^{3/2}$ clauses (where $c$ is a sufficiently large constant) finds a subformula with $\Theta(c^2n)$ clauses and then uses spectral techniques to prove that this subformula is not satisfiable (and hence that the original formula is not satisfiable). Previously, it was only known how to efficiently certify the unsatisfiability of random $3$CNF formulas with at least $\text{poly}(\log(n)) \cdot n^{3/2}$ clauses. Our algorithm is simple enough to run in practice. We present some experimental results.