Er følgende en gyldig inferensregel (tautologi)?

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

Dette er resolusjon-regelen som brukes i automatisk teorembevisning.