1%  Equivalential calculus (EC): YQL is a single axiom.
2%
3%  {EC1, EC2} (Lesniewski) was the first axiomatization of EC.
4%  Show that EC1 and EC2 can be derived from YQL by condensed detachment.
5
6set(hyper_res).
7assign(pick_given_ratio,3).
8clear(back_sub).
9assign(max_proofs,2).
10assign(max_weight, 16).
11clear(print_kept).
12set(order_history).
13
14list(usable).
15-P(e(x,y)) | -P(x) | P(y).  % condensed detachment
16end_of_list.
17
18list(sos).
19P(e(e(x,y),e(e(z,y),e(x,z)))).  % YQL
20end_of_list.
21
22list(passive).
23-P(e(e(e(a,b),e(c,a)),e(b,c))) | $Ans(EC_1).
24-P(e(e(a,e(b,c)),e(e(a,b),c))) | $Ans(EC_2).
25end_of_list.
26
27% The following demodulators discard clauses that contain an
28% instance of e(x,x) as a proper subformula.
29
30list(demodulators).
31e(e(x,x),y) = junk.
32e(y,e(x,x)) = junk.
33e(x,junk) = junk.
34e(junk,x) = junk.
35P(junk) = $T.
36end_of_list.
37
38% For reference, the 13 shortest single axioms for EC:
39%
40% P(e(e(x,y),e(e(z,y),e(x,z)))).    %  YQL  %  Lukasiewicz  P1
41% P(e(e(x,y),e(e(x,z),e(z,y)))).    %  YQF  %  Lukasiewicz  P2
42% P(e(e(x,y),e(e(z,x),e(y,z)))).    %  YQJ  %  Lukasiewicz  P3
43% P(e(e(e(x,y),z),e(y,e(z,x)))).    %  UM   %  Meredith     P4 = P4'
44% P(e(x,e(e(y,e(x,z)),e(z,y)))).    %  XGF  %  Meredith     P5
45% P(e(e(x,e(y,z)),e(z,e(x,y)))).    %  WN   %  Meredith     P7
46% P(e(e(x,y),e(z,e(e(y,z),x)))).    %  YRM  %  Meredith     P8
47% P(e(e(x,y),e(z,e(e(z,y),x)))).    %  YRO  %  Meredith     P9
48% P(e(e(e(x,e(y,z)),z),e(y,x))).    %  PYO  %  Meredith     P10  = P9'
49% P(e(e(e(x,e(y,z)),y),e(z,x))).    %  PYM  %  Meredith     P11  = P8'
50% P(e(x,e(e(y,e(z,x)),e(z,y)))).    %  XGK  %  Kalman
51% P(e(x,e(e(y,z),e(e(x,z),y)))).    %  XHK  %  Winker
52% P(e(x,e(e(y,z),e(e(z,x),y)))).    %  XHN  %  Winker
53