set(auto).
clear(print_given).

% each of the four theorems proved require
% about seconds of processing

include("nDef.txt").
include("dDef.txt").
include("uzDef.txt").

include("booleanAx.txt").
include("peirceanAx0.txt").
include("peirceanAx2.txt").
include("15_16booleanLaws.txt"). % nedded only for the proof of the 4th
include("i.txt").
include("11booleanLaws.txt").
include("cycleLawC.txt").

include("xix_b_ghost.txt").