This depends on the precise proof system, and notion of proof length, that you use. But for any reasonable one, the answer will be yes: as long as the question "Is there a proof of $\varphi$ from $A$ of length $\le n$?" is uniformly decidable in $\varphi, A, n$ (where $A$ ranges over finite sets of sentences), there will be arbitrarily hard-to-find inconsistencies.
This follows immediately from the fact that the set of validities of first-order logic (with equality) in one binary relation symbol is undecidable. This, in turn, follows since we can convert an arbitrary (finite-language) structure into a directed graph in a natural way.