set(auto).
clear(print_given).

% three out of four of the theorems proved require
% about 1 minute of processing each

assign(max_distinct_vars,3).

include("iDef.txt").
include("uzDef.txt").

include("booleanAx.txt").
include("15_16booleanLaws.txt").
include("i.txt").

include("xii.txt").

include("xix_a_ghost.txt").