%%%%%%%%%%%%%%%%%%%%%  Basic options

op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator

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

assign(pick_given_ratio, 4).
assign(max_mem, 20000).

%%%%%%%%%%%%%%%%%%%%%  Standard for equational problems

set(knuth_bendix).
set(build_proof_object).

%%%%%%%%%%%%%%%%%%%%%  Modifications to strategy

assign(max_weight, 23).
set(control_memory).
  
%%%%%%%%%%%%%%%%%%%%%  Clauses

list(usable).
x = x.
end_of_list.

list(sos).
x ^ x = x.
x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).

x v x = x.
x v y = y v x.
(x v y) v z = x v (y v z).

(x ^ (y v z)) v (x ^ y) = x ^ (y v z).
(x v (y ^ z)) ^ (x v y) = x v (y ^ z).

(x ^ y) v (z ^ (x v y)) = (x v y) ^ (z v (x ^ y)).

A ^ (B v (A ^ C)) != (A ^ B) v (A ^ C).

end_of_list.

list(passive).
end_of_list.

% End of ordinary input, which leads to a 125-step proof in 914 seconds.
% The rest of the file is contributed by Larry Wos, and leads quickly to a
% 30-step proof.

clear(control_memory).
assign(pick_given_ratio, 9).
assign(max_weight, 15).

list(hot).
x v x=x.
x v y=y v x.
end_of_list.

weight_list(pick_and_purge).
% Following are positive proof steps from qlt3.test.out2
% (now called qlt5 in nice.proofs) beginning with first para, 33 of them.
weight(x v (y v ((x v y)^x))=x v y,2).
weight((x^ (x v y)) v x=x^ (x v y),2).
weight(x v (((y v x)^y) v y)=y v x,2).
weight(((x v y)^x) v x=x^ (x v y),2).
weight(x v (y^ (y v x))=y v x,2).
weight((x v y)^ (x v (y^z))=x v (y^z),2).
weight((x v y)^ (x v (z^y))=x v (y^z),2).
weight(x v (y^z)= (x v y)^ (x v (z^y)),2).
weight((x v y)^ (x v (z^y))=x v (z^y),2).
weight((x v (y^z))^ (x v z)=x v (z^y),2).
weight(x v (y^z)= (x v (z^y))^ (x v y),2).
weight((x v (y^z))^ (z v x)=x v (z^y),2).
weight((x v (y^z))^ (x v z)=x v (y^z),2).
weight(x v (y^z)= (x v (z^y))^ (y v x),2).
weight((x v (y^z))^ (z v x)=x v (y^z),2).
weight((x^y) v (x^ (y v z))=x^ (y v z),2).
weight((x^y) v (x^ (z v y))=x^ (y v z),2).
weight((x^ (y v z)) v (x^z)=x^ (y v z),2).
weight(x^ (x^y)=x^y,2).
weight((x v (y^z))^ ((x v z)^u)= (x v (y^z))^u,2).
weight((x v (y^z))^ ((z v x)^u)= (x v (y^z))^u,2).
weight((x^ (y v (x^z))) v (x^z)=x^ (y v (x^z)),2).
weight((x^y) v (z^ (u^ (x v y)))= (x v y)^ ((z^u) v (x^y)),2).
weight(x^ (y v x)=x v (x^y),2).
weight((x v y)^ ((z^u) v (x^y))= (x^y) v (z^ (u^ (x v y))),2).
weight(x v (x^y)=x^ (x v y),2).
weight((x^y) v (z^ (u^ (x v y)))= (x v y)^ ((x^y) v (z^u)),2).
weight(((x^y) v (z^u))^ (u v y)= (x^y) v (z^u),2).
weight((x v y)^ ((z^y) v (u^x))= (z^y) v (u^x),2).
weight((x^y) v (z^x)=x^ ((x v y)^ (z v (x^y))),2).
weight((x^y) v (x^z)=x^ ((x v y)^ (z v (x^y))),2).
weight((x^y) v (x^z)=x^ ((x v z)^ (y v (x^z))),2).
weight(x^ ((x v y)^ (z v (x^y)))=x^ (z v (x^y)),2).
end_of_list.

