Является ли следующее правило вывода корректным (тавтологией)?

((A ∨ B) ∧ (¬B ∨ C)) → (A ∨ C)

Это правило резолюции, используемое в автоматическом доказательстве теорем.