A propositional proof system $P$ has the strong feasible disjunction property iff there is a constant $c \geq 1$ such that whenever $P$ admits a size $s$ proof of $\bigvee_i α_i$ with no two $α_i$ sharing an atom then one of $α_i$ has a $P$-proof of size $\le s^c$. We combine the work of Ilango (2025) and Ren et al. (2025) with the gadget proof complexity generator of K. (2007) and rule out the property for strong enough proof systems under the following two hypotheses: - there exists a language in class E that requires exponential size circuits even if they are allowed to query an NP oracle, - there exists a P/poly demi-bit in the sense of Rudich (1997).

翻译：一个命题证明系统 $P$ 具有强可行性析取性质，当且仅当存在常数 $c \geq 1$，使得只要 $P$ 拥有一个大小为 $s$ 的证明证明 $\bigvee_i α_i$，且任意两个 $α_i$ 不共享原子公式，则存在某个 $α_i$ 拥有一个大小不超过 $s^c$ 的 $P$-证明。我们结合 Ilango (2025) 与 Ren 等人 (2025) 的工作以及 K. (2007) 的 gadget 证明复杂度生成器，在以下两个假设下排除了足够强证明系统的该性质：- 存在 E 类语言要求指数级电路规模，即使允许其查询 NP 预言机；- 在 Rudich (1997) 的意义下存在 P/poly 半比特。