Busy Beaver and Kolmogorov-random-string conjectures imply Feige's Hypothesis

Let Feige's Hypothesis be the assertion that no efficient algorithm can prove the unsatisfiability of a random $3$-SAT formula with high probability, even when the formula has a small number of clauses. Let the Busy Beaver proof-size conjecture and the Kolmogorov-random-string proof-size conjecture be the two conjectures stated above. Feige implication conjecture. Either the Busy Beaver proof-size conjecture or the Kolmogorov-random-string proof-size conjecture implies Feige's Hypothesis.