A seguinte regra de inferência é válida (tautologia)?

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

Esta é a regra de resolução usada em prova automática de teoremas.