Đây có phải là một quy tắc suy luận hợp lệ (tautology) không?

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

Đây là quy tắc resolution được sử dụng trong chứng minh định lý tự động.