Ist die folgende Schlussregel eine gültige Inferenzregel (Tautologie)?

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

Dies ist die Resolutionsregel, die in der automatischen Theorembeweisführung verwendet wird.