Initial premises
From (p ∧ q) ∨ r you may derive p ∨ r or q ∨ r.
From r → s you may derive ¬r ∨ s.
From (X ∨ r) and (¬r ∨ Y) derive (X ∨ Y).