set(auto).
clear(print_given).

assign(max_seconds, 20). % 5 would suffice for all but thesis 25
assign(max_distinct_vars, 3).
assign(max_literals, 1).

include("booleanAx.txt").	% file di assiomi

include("iDef.txt").	% definizione del relatore d'inclusione
include("nDef.txt").	% definizione dell'operatore d'intersezione
include("uzDef.txt").	% definizione dell'operatore d'intersezione

include("booleanLaws.txt").	% file di tesi