EQUAL_STEP
⊢ ∀a b c. (a ⇒ (b ⇔ c)) ∧ b ⇒ ¬a ∨ c
EXCLUDED_MIDDLE'
⊢ ∀t. ¬t ∨ t
FINALIZE_CLAUSE
⊢ ∀a b. (¬a ⇒ b) ⇒ a ∨ b
HIDE_LITERAL
⊢ ∀a. a ⇒ ¬a ⇒ F
INITIALIZE_CLAUSE
⊢ ∀a b. a ∨ b ⇒ ¬a ⇒ b
RESOLUTION
⊢ ∀a. a ∧ ¬a ⇒ F
SHOW_LITERAL
⊢ ∀x. (¬x ⇒ F) ⇒ x