set(auto).

clauses(sos).

  (x v y) v z = x v (y v z).
  x v y = y v x.
  ((x v y')' v (x v y)')' = x      # label(Robbins).

  C v D = C.         % special hypothesis

end_of_list.

assign(max_proofs, -1).

clauses(denials).

  A v A != A # answer(Idempotence).

  (B v A')' v (A' v B')' != A # answer(Huntington_a) # action(in_proof -> exit).

  (A v B')' v (A' v B')' != B # answer(Huntington_b) # action(in_proof -> exit).

end_of_list.