А, ага, просто раскрываем скобки и получаем

правую скобку из

можно получить методом резолюций, но
как из тождеств булевой алгебры получить метод резолюций?
- это мы преобразовываем слева направо.
Справа налево:

тут наверно тоже аналог метода резолюций, и для него тот же вопрос.