La seguente è una regola di inferenza valida (tautologia)?

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

Questa è la regola di risoluzione usata nella dimostrazione automatica di teoremi.