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?