6.1.1.3 Исчисление высказываний

Условие: Используя метод резолюций доказать невыполнимость (или выполнимость) следующих множеств дизъюнктов. Применять произвольный порядок перебора дизъюнктов, a также, по указанию преподавателя, одну из следующих стратегий: предпочтение одночленам, линейную, насыщение уровня. \[ \{(q \vee \neg \tau),(\neg q \vee \neg \tau),(q \vee \tau),(\neg p \vee \neg \tau), \neg q\} \]