%%%%%%%%%%%%%%%%%%%%%  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

% See comments after clauses.
%
% assign(max_weight, 24).
% assign(change_limit_after, 50).
% assign(new_max_weight, 17).

%%%%%%%%%%%%%%%%%%%%%  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).

% Absorption laws for LT:
% x ^ (x v y) = x.
% x v (x ^ y) = x.

% Link laws for QLT:
(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) ^ y) v (z ^ x) = (((x v y) ^ z) v y) ^ (z v x).

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

list(passive).
end_of_list.

% This file has been modified by Larry Wos so that a shorter 
% proof is found.  The original proof, found with the above
% commented-out commands, is 183 steps (950 seconds).
% The rest of the file reflects Larry's changes, and leads
% to a shorter, quicker proof.

assign(pick_given_ratio, 6).
assign(max_weight, 15).
  
weight_list(pick_and_purge).
%  Following are proof steps from ...t4a.out20l3, all of them including input, with those before the back_demod before the para given higher weight.
weight(x^x=x,4).
weight(x^y=y^x,4).
weight((x^y)^z=x^ (y^z),4).
weight(x v x=x,4).
weight(x v y=y v x,4).
weight((x v y) v z=x v (y v z),4).
weight((x^ (y v z)) v (x^y)=x^ (y v z),4).
weight((x v (y^z))^ (x v y)=x v (y^z),4).
weight((((x^y) v z)^y) v (z^x)= (((x v y)^z) v y)^ (z v x),4).
weight(x^ (y^z)=y^ (x^z),2).
weight(x^ (x^y)=x^y,2).
weight(x^ (y^z)=z^ (x^y),2).
weight(x^ (y^x)=y^x,2).
weight(x^ (y^ (x^z))=x^ (y^z),2).
weight(x v (y v z)=y v (x v z),2).
weight(x v (x v y)=x v y,2).
weight(x v (y v z)=y v (z v x),2).
weight(x v (y v z)=z v (x v y),2).
weight(x v (y v x)=y v x,2).
weight(x v (y v (x v z))=x v (y v z),2).
weight(x v (y v z)=z v (y v x),2).
weight(x v (y v (z v u))=z v (x v (u v y)),2).
weight((x^ (y v (z v u))) v (x^u)=x^ (u v (y v z)),2).
weight((x^ (y^ (z v u))) v (x^ (y^z))=x^ (y^ (z v u)),2).
weight(((x v y)^z) v (z^x)=z^ (x v y),2).
weight(x v (y v ((x v y)^x))=x v y,2).
weight((x^ ((y^x) v z)) v (y^x)=x^ ((y^x) v z),2).
weight((x^ (y v z)) v (y^x)=x^ (y v z),2).
weight((x^y) v (x^ (y v z))=x^ (y v z),2).
weight(((x^y) v z)^ (z v x)=z v (x^y),2).
weight((x v (y^z))^ (y v x)=x v (y^z),2).
weight((x v (x^y))^x=x v (x^y),2).
weight((x v y)^ (x v (y^z))=x v (y^z),2).
weight(((x v y)^x) v (y^x)= ((x^y) v x)^ (y v x),2).
weight((x^ ((y^x) v z)) v (z^y)= (((y v x)^z) v x)^ (z v y),2).
weight((x^ (y^ (z v u))) v (x^ (y^u))=x^ (y^ (z v u)),2).
weight((x^ (y v z)) v (x^ ((y v z)^y))=x^ (y v z),2).
weight(((x v y)^z) v (z^y)=z^ (x v y),2).
weight((x^y) v (y^x)=y^x,2).
weight((((x^y) v z)^y) v (x^y)=y^ ((x^y) v z),2).
weight(((x v y)^z) v (x^z)=z^ (x v y),2).
weight(((x v y)^x) v x=x^ (x v y),2).
weight((x v y)^ (y v x)=x v y,2).
weight((x^y) v ((y v z)^x)=x^ (y v z),2).
weight(x v (y v ((y v x)^x))=y v x,2).
weight(((x v y)^x) v (x v y)=x v y,2).
weight(x v (y v (z^ (z v x)))=y v (z v x),2).
weight((x^ ((y^x) v z)) v (x^y)=x^ ((y^x) v z),2).
weight((x^y) v (y^ ((x^y) v z))=y^ ((x^y) v z),2).
weight((x^y) v (y^ (x v z))=y^ (x v z),2).
weight((x^y) v (x^ (z v y))=x^ (z v y),2).
weight((x^y) v ((x^ (y v z)) v u)= (x^ (y v z)) v u,2).
weight(((x^y) v z)^ (z v y)=z v (x^y),2).
weight(((x^y) v z)^ (x v z)=z v (x^y),2).
weight(((x^y) v x)^x=x v (x^y),2).
weight(x v (y^ (x v y))=x v y,2).
weight(((x^y) v z)^ (z v x)= (x^y) v z,2).
weight((x v y)^ (y v (x^z))=y v (x^z),2).
weight((x v y)^ (x v (z^y))=x v (z^y),2).
weight(((x^y) v x)^ (x^ (y v z))=x^ (y v z),2).
weight((x^y) v x=x v (y^x),2).
weight(x v (y^x)=x^ (x v y),2).
weight(x^ ((x v y)^ (y v z))=x^ (y v z),2).
weight(x v (x^y)= (x v y)^x,2).
weight((x^y) v x=x^ (x v y),2).
weight((x^ ((y^x) v z)) v (y^z)= (((y v x)^z) v x)^ (z v y),2).
weight((x^ (y^ (z v u))) v (y^ (x^u))=y^ (x^ (z v u)),2).
weight((x^ (y v z)) v (x^ ((z v y)^y))=x^ (y v z),2).
weight(((x v y)^z) v (y^z)=z^ (x v y),2).
weight(((x v y)^y) v y=y^ (x v y),2).
weight((x^y) v ((z v y)^x)=x^ (z v y),2).
weight((x^y) v (z v (y^x))=z v (y^x),2).
weight((x^y) v ((y^x) v z)= (y^x) v z,2).
weight((((x^y) v z)^y) v (y^x)=y^ ((x^y) v z),2).
weight((x^y) v ((x v z)^y)=y^ (x v z),2).
weight((x v y)^ (z^ (y v x))=z^ (y v x),2).
weight(((x v y)^y) v (y v x)=x v y,2).
weight(x v (y v (z^ (x v z)))=y v (x v z),2).
weight(x^ ((y^x) v x)=x^ (y v x),2).
weight(((x^y) v y)^ (y^ (x v z))=y^ (x v z),2).
weight(x^ ((y v z)^ ((y^x) v x))=x^ (y v z),2).
weight(((x^y) v z)^ (z v y)= (x^y) v z,2).
weight(x^ ((y v z)^ (y v (x^ (y v z))))=x^ (y v z),2).
weight(x^ (y v (z^ (z v x)))=x^ (y v z),2).
weight(((x^y) v z)^ (x v z)= (x^y) v z,2).
weight((x^y) v y=y^ (x v y),2).
weight(x^ ((y v z)^ (y v x))=x^ (y v z),2).
weight(x^ ((y v x)^ (y v z))=x^ (y v z),2).
weight(x^ ((x v y)^ ((y^x) v z))=x^ ((y^x) v z),2).
weight((x v y)^ (y v (z^ (x v y)))=y v (z^ (x v y)),2).
weight((x v y)^ (x v (z^ (x v y)))=x v (z^ (x v y)),2).
weight(x^ (y v (x^ (y v z)))=x^ (y v z),2).
weight(x^ ((y^x) v (x^z))= (y^x) v (x^z),2).
weight(x^ ((x v y)^ (z v (u v y)))=x^ (z v (u v y)),2).
weight((((x v y)^z) v y)^ (z v x)= (x^z) v (y^ ((x^y) v z)),2).
weight((x^y) v (z^ (x v z))= (x^y) v z,2).
weight(x v (y^z)= (z^y) v x,2).
weight(x^ (y v (x^ (z v y)))=x^ (z v y),2).
weight((x v y)^ ((z^y) v x)= (z^y) v x,2).
weight((x^y) v ((z v y)^z)= (x^y) v z,2).
weight((x^y) v (z^ (y v z))= (x^y) v z,2).
weight((x v y)^ (z^ ((x^u) v y))=z^ ((x^u) v y),2).
weight((x^y) v (y v z)= (y v z)^ (x v (y v z)),2).
weight(x^ (y^ (z v (x^y)))=x^ (y^ (z v y)),2).
weight((x v y)^ (z^ (x v z))= (x v y)^z,2).
weight(x^ (y v (x v z))=x^ ((x v z)^ (y v x)),2).
weight((((x v y)^z) v y)^ (x v z)= (x^z) v (y^ ((x^y) v z)),2).
weight((x^y) v (z^ (u^ (x v u)))= (x^y) v (z^u),2).
weight(x^ ((y v x)^ ((y^z) v u))=x^ ((y^z) v u),2).
weight(x^ (((y v z)^x) v z)=x^ (y v z),2).
weight(x v ((y^x) v z)= (x v z)^ (y v (x v z)),2).
weight((x^y) v (z^ (u^ (x v z)))= (x^y) v (u^z),2).
weight((x v y)^ (((x v z)^y) v z)= (x v y)^ ((x^y) v z),2).
weight(x^ ((y^x) v z)=x^ (y v z),2).
weight((x^y) v (y^z)=y^ (x v (y^z)),2).
weight(x^ (y v (x^z))=x^ (z v y),2).
end_of_list.

