ยง Resolution algorithm for propositional logic

F \/ l; G \/ not(l)
-------------------
  F \/ G