Проверить выводимость формулы из мн-ва гипотез

[Sleep3r]

$\Gamma\vdash\varphi?$
$ \varphi=A, \Gamma =\left\lbrace B \vee A, C \vee D \vee \neg B, \neg C \vee A, \neg D \vee A \right\rbrace$
Начал делать по теореме о противоречивых множествах, но противоречие найти не получается.

[arseniiv]

По крайней мере, формула $(B\vee A)\wedge(C\vee D\vee\neg B)\wedge(\neg C\vee A)\wedge(\neg D\vee A)\to A$ тождественно истинна. Не теряйте надежды!

-- Пн ноя 06, 2017 00:12:20 --

Вот есть правило резолюций $\dfrac{X\vee Y,\; \neg X\vee Z}{Y\vee Z}$ — если вы им пользуетесь, в этом примере стратегия, по-моему, очевидна. Трудно применить его здесь не так.