In each example, you will refute a set A of closed PLN formulas. The elements of A are given as axioms. To put each formula on the branch, press the button that says Import Axiom or Lemma and choose the formula to import. (You can ignore "claim false" which will put ¬false on the branch.)