Проверить выводимость в исчислении высказываний методом резолюций: ⊢¬A∨¬B→¬(A&B).
Очень нужна помощь, я просто запуталась.

В чем запутались?

у меня получается при каждом перешивании разные значения:
"Применим к выводимости теорему дедукции. Получим ¬А∨¬В⊢¬(А&В). Преобразуем к множеству предложений гипотезы и отрицание целевой формулы.
¬(¬(А&В))
¬(¬(¬А∨В)
¬(А∨¬В)
¬А&В
Таким образом, получим предложения ¬А∨¬В, А,В.
Теперь производим резольвирование:
1. А
2. В
3. ¬А∨¬В
4. ¬В ПР из 2 и 3
5. ∅ ПР из 2 и 4
Поскольку получено пустое предложение, то исходная формула выводима в ИВ."
правильно то хоть решаю?