%  Equivalential calculus (EC): YQL is a single axiom.
%
%  {EC1, EC2} (Lesniewski) was the first axiomatization of EC.
%  Show that EC1 and EC2 can be derived from YQL by condensed detachment.

set(hyper_res).
assign(pick_given_ratio,3).
clear(back_sub).
assign(max_proofs,2).
assign(max_weight, 16).
clear(print_kept).
set(order_history).

list(usable).
-P(e(x,y)) | -P(x) | P(y).  % condensed detachment
end_of_list.

list(sos).
P(e(e(x,y),e(e(z,y),e(x,z)))).  % YQL
end_of_list.

list(passive).
-P(e(e(e(a,b),e(c,a)),e(b,c))) | $Ans(EC_1).
-P(e(e(a,e(b,c)),e(e(a,b),c))) | $Ans(EC_2).
end_of_list.

% The following demodulators discard clauses that contain an
% instance of e(x,x) as a proper subformula.

list(demodulators).
e(e(x,x),y) = junk.
e(y,e(x,x)) = junk.
e(x,junk) = junk.
e(junk,x) = junk.
P(junk) = $T.
end_of_list.

% For reference, the 13 shortest single axioms for EC:
%
% P(e(e(x,y),e(e(z,y),e(x,z)))).    %  YQL  %  Lukasiewicz  P1
% P(e(e(x,y),e(e(x,z),e(z,y)))).    %  YQF  %  Lukasiewicz  P2
% P(e(e(x,y),e(e(z,x),e(y,z)))).    %  YQJ  %  Lukasiewicz  P3
% P(e(e(e(x,y),z),e(y,e(z,x)))).    %  UM   %  Meredith     P4 = P4'
% P(e(x,e(e(y,e(x,z)),e(z,y)))).    %  XGF  %  Meredith     P5
% P(e(e(x,e(y,z)),e(z,e(x,y)))).    %  WN   %  Meredith     P7
% P(e(e(x,y),e(z,e(e(y,z),x)))).    %  YRM  %  Meredith     P8
% P(e(e(x,y),e(z,e(e(z,y),x)))).    %  YRO  %  Meredith     P9
% P(e(e(e(x,e(y,z)),z),e(y,x))).    %  PYO  %  Meredith     P10  = P9'
% P(e(e(e(x,e(y,z)),y),e(z,x))).    %  PYM  %  Meredith     P11  = P8'
% P(e(x,e(e(y,e(z,x)),e(z,y)))).    %  XGK  %  Kalman
% P(e(x,e(e(y,z),e(e(x,z),y)))).    %  XHK  %  Winker
% P(e(x,e(e(y,z),e(e(z,x),y)))).    %  XHN  %  Winker