set(auto).

assign(max_weight, 50).

assign(constant_weight, 0).

terms(weights).
x ' ' = 1000.
end_of_list.

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).

  x v y != x # answer(Winker1a).
  x v y != y # answer(Winker1b).

  (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.