Is de volgende inferentieregel geldig (een tautologie)?

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

Dit is de resolutieregel die wordt gebruikt in geautomatiseerd bewijzen.