set(auto).
clear(print_given).

% tests take a couple of seconds each

assign(max_distinct_vars, 3).
assign(max_literals, 1).
assign(max_mem, 64000).
assign(max_weight, 19).

formula_list(usable).
	all x ( x = x ).
end_of_list.

% Boolean axioms and definitions
include("booleanAx.txt").
include("iDef.txt").
include("nDef.txt").
include("dDef.txt").

include("ii.txt").
include("xii.txt"). % Schroeder's equivalences

include("xxix_ghost.txt").