% This is an example of the input used with the candidates that
% pass the semantic filters.  Search for 10 seconds, trying to
% prove Boolean properties.

% This was applied automatically to hundreds of thousands of candidates.

set(knuth_bendix).
assign(pick_given_ratio,3).

assign(max_mem,200000).
assign(max_weight,120).
assign(max_proofs,10).
assign(max_seconds,10).

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).

list(usable).
x = x.
or(or(X,Y),Z) != or(X,or(Y,Z)) | $Ans(Assoc).
or(not(or(X,not(Y))),not(or(not(X),not(Y)))) != Y | $Ans(Huntington).
not(or(not(or(X,Y)),not(or(not(X),Y)))) != Y | $Ans(Robbins).
or(not(or(not(X),Y)),X) != X | $Ans(Meredith_1a).
or(not(or(not(X),X)),Y) != Y | $Ans(Meredith_1b).
or(not(or(not(X),Y)),or(Z,Y)) != or(Y,or(Z,X)) | $Ans(Meredith_2).
end_of_list.

list(passive).
or(X,X) != X | $Ans(Idempotence).
not(not(X)) != X | $Ans(Not_not).
or(Y,X) != or(X,Y) | $Ans(Commutativity).
or(X,not(X)) != or(Y,not(Y)) | $Ans(One_a).
or(not(X),X) != or(not(Y),Y) | $Ans(One_b).
or(not(X),X) != or(Y,not(Y)) | $Ans(One_c).
or(X,not(X)) != or(not(Y),Y) | $Ans(One_d).
end_of_list.

list(sos).

% Candidate single axiom.

% This example is a single axiom, but this search proves
% only two of the properties.

or(not(or(not(or(v0,v1)),not(v2))),not(or(not(or(not(v3),v3)),or(not(v2),v0)))) = v2.  % Job 13345

end_of_list.