Дивлюсь початок курсу із логіки на Курсері, і там давали квіз на перевірку формул, зокрема такої:

((¬r ⇒ ¬p ∧ ¬q) ∨ s) ⇔ (p ∨ q ⇒ r ∨ s)

Виписувати таблицю істиності на 16 комбінацій мені стало страшно. Я схитрив і побачив, що для s=1 ця формула тавтологічна, а от для s=0 довелось попереписувати:

(¬r ⇒ ¬p ∧ ¬q) ⇔ (p ∨ q ⇒ r)

помітити, що ¬p ∧ ¬q ⇔ ¬(p ∨ q) за де Морганом, отже

(¬r ⇒ ¬(p ∨ q)) ⇔ (p ∨ q ⇒ r)

довелось ще помітити, що, оскільки (¬x ⇒ ¬y) ⇔ (y ⇒ x), то формула при s=0 також вироджується в тавтологію.

А потім згадав, що є такі чудові штуки, як SMT-солвери, і, розчехливши цю гармату, таки вистрілив по горобцях:

$ rlwrap z3 -smt2 -in
;; описуємо наші змінні:
(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool) 

;; ((¬r ⇒ ¬p ∧ ¬q) ∨ s) ⇔ (p ∨ q ⇒ r ∨ s)
(define-fun lhs () Bool
  (or (=> (not r) (and (not p) (not q))) s))
(define-fun rhs () Bool
  (=> (or p q) (or r s)))
(define-fun conjecture () Bool
  (= lhs rhs))

(push) ;; зберігаємо стан без припущень
(assert conjecture)  ;; робимо припущення, що формула conjecture задовольняється
(check-sat) ;sat    ;; так, існують truth assignments, за яких це так

(pop) ;; позбавляємось припущення істинності conjecture
(assert (not conjecture))
(check-sat) ;unsat   ;; не існує truth assignment, за яких формула заперечується 

;; `conjecture` is satisfiable and its negation is not,
;; so it's valid.(exit)

Спробувати це онлайн можна тут: http://rise4fun.com/z3.