0:00
Difficulty: ExpertCategory: Logical EquivalenceType: Equivalence Check

Is the following a valid inference rule (tautology)?

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

This is the resolution rule used in automated theorem proving.