It is NP-complete. The usual formulation is this: "Given a statement S of ZFC and a number n, is there a proof of S that is shorter than n?". It is trivial to solve SAT based on this: Let the statement be that the SAT formula is satisfiable, and choose an n such that the trivial constructive proof is shorter than n.
My understanding was that a search for a proof in first-order logic cannot be reduced to a single SAT problem; rather theorem provers generate a (potentially unbounded) series of SAT problems, one of which is eventually guaranteed to yield a proof if such a proof exists. But perhaps the bound on proof length that you mentioned changes this. How do you construct the SAT problem?
Many experts suspect that there is no polynomial-time solution to the so-called NP-complete problems, though no-one has yet been able to rigorously prove this and there remains the possibility that a polynomial-time algorithm will one day emerge. However unlikely this is, today I would like to invite LW to play a game I played with with some colleagues called what-would-you-do-with-a-polynomial-time-solution-to-3SAT? 3SAT is, of course, one of the most famous of the NP-complete problems and a solution to 3SAT would also constitute a solution to *all* the problems in NP. This includes lots of fun planning problems (e.g. travelling salesman) as well as the problem of performing exact inference in (general) Bayesian networks. What's the most fun you could have?