Theorem “TP5H20”:
  (s ⇒ u ∧ p) ∧ (s ⇒ w) ∧ ((s ⇒ p) ⇒ t) ∧ (q ∧ r ⇒ s) ∧ (t ⇒ ¬ q) ⇒ (¬(u ∧ p) ∧ q ⇒ ¬ r ∧ ¬(w ⇒ p))
Proof:
  Assuming `s ⇒ u ∧ p`, `s ⇒ w`, `(s ⇒ p) ⇒ t`, `q ∧ r ⇒ s`, `t ⇒ ¬ q`:
    ¬ r ∧ ¬(w ⇒ p)
  ⇐


    ¬(u ∧ p) ∧ q