Est-ce que la formule suivante est une règle d'inférence valide (tautologie) ?

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

Ceci est la règle de résolution utilisée en démonstration automatique de théorèmes.